tptp-0.1.0.0: test-data/tstp/fof/ALG043+1---Vampire---4.3.THM-Ref.s
%------------------------------------------------------------------------------
% File : Vampire---4.3
% Problem : ALG043+1 : TPTP v7.1.0. Released v2.7.0.
% Transform : none
% Format : tptp:raw
% Command : vampire --mode casc -t %d %s
% Computer : n157.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.625MB
% OS : Linux 3.10.0-693.2.2.el7.x86_64
% CPULimit : 300s
% DateTime : Tue Sep 4 10:09:56 EDT 2018
% Result : Theorem 0.08s
% Output : Refutation 0.08s
% Verified :
% Statistics : Number of formulae : 324 ( 567 expanded)
% Number of leaves : 50 ( 198 expanded)
% Depth : 68
% Number of atoms : 3266 (4219 expanded)
% Number of equality atoms : 1660 (2566 expanded)
% Maximal formula depth : 65 ( 9 average)
% Maximal term depth : 2 ( 1 average)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Vampire---4.3 format not known, defaulting to TPTP
fof(f2,axiom,
( e0 = op(e3,e3)
& e1 = op(e3,e2)
& e2 = op(e3,e1)
& e3 = op(e3,e0)
& e1 = op(e2,e3)
& e0 = op(e2,e2)
& e3 = op(e2,e1)
& e2 = op(e2,e0)
& e2 = op(e1,e3)
& e3 = op(e1,e2)
& e0 = op(e1,e1)
& e1 = op(e1,e0)
& e3 = op(e0,e3)
& e2 = op(e0,e2)
& e1 = op(e0,e1)
& e0 = op(e0,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2)).
fof(f3,axiom,(
e0 = unit ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3)).
fof(f4,conjecture,
( ( e3 = op(e3,e3)
| e3 = op(e2,e3)
| e3 = op(e1,e3)
| e3 = op(e0,e3) )
& ( e3 = op(e3,e3)
| e3 = op(e3,e2)
| e3 = op(e3,e1)
| e3 = op(e3,e0) )
& ( e2 = op(e3,e3)
| e2 = op(e2,e3)
| e2 = op(e1,e3)
| e2 = op(e0,e3) )
& ( e2 = op(e3,e3)
| e2 = op(e3,e2)
| e2 = op(e3,e1)
| e2 = op(e3,e0) )
& ( e1 = op(e3,e3)
| e1 = op(e2,e3)
| e1 = op(e1,e3)
| e1 = op(e0,e3) )
& ( e1 = op(e3,e3)
| e1 = op(e3,e2)
| e1 = op(e3,e1)
| e1 = op(e3,e0) )
& ( e0 = op(e3,e3)
| e0 = op(e2,e3)
| e0 = op(e1,e3)
| e0 = op(e0,e3) )
& ( e0 = op(e3,e3)
| e0 = op(e3,e2)
| e0 = op(e3,e1)
| e0 = op(e3,e0) )
& ( e3 = op(e3,e2)
| e3 = op(e2,e2)
| e3 = op(e1,e2)
| e3 = op(e0,e2) )
& ( e3 = op(e2,e3)
| e3 = op(e2,e2)
| e3 = op(e2,e1)
| e3 = op(e2,e0) )
& ( e2 = op(e3,e2)
| e2 = op(e2,e2)
| e2 = op(e1,e2)
| e2 = op(e0,e2) )
& ( e2 = op(e2,e3)
| e2 = op(e2,e2)
| e2 = op(e2,e1)
| e2 = op(e2,e0) )
& ( e1 = op(e3,e2)
| e1 = op(e2,e2)
| e1 = op(e1,e2)
| e1 = op(e0,e2) )
& ( e1 = op(e2,e3)
| e1 = op(e2,e2)
| e1 = op(e2,e1)
| e1 = op(e2,e0) )
& ( e0 = op(e3,e2)
| e0 = op(e2,e2)
| e0 = op(e1,e2)
| e0 = op(e0,e2) )
& ( e0 = op(e2,e3)
| e0 = op(e2,e2)
| e0 = op(e2,e1)
| e0 = op(e2,e0) )
& ( e3 = op(e3,e1)
| e3 = op(e2,e1)
| e3 = op(e1,e1)
| e3 = op(e0,e1) )
& ( e3 = op(e1,e3)
| e3 = op(e1,e2)
| e3 = op(e1,e1)
| e3 = op(e1,e0) )
& ( e2 = op(e3,e1)
| e2 = op(e2,e1)
| e2 = op(e1,e1)
| e2 = op(e0,e1) )
& ( e2 = op(e1,e3)
| e2 = op(e1,e2)
| e2 = op(e1,e1)
| e2 = op(e1,e0) )
& ( e1 = op(e3,e1)
| e1 = op(e2,e1)
| e1 = op(e1,e1)
| e1 = op(e0,e1) )
& ( e1 = op(e1,e3)
| e1 = op(e1,e2)
| e1 = op(e1,e1)
| e1 = op(e1,e0) )
& ( e0 = op(e3,e1)
| e0 = op(e2,e1)
| e0 = op(e1,e1)
| e0 = op(e0,e1) )
& ( e0 = op(e1,e3)
| e0 = op(e1,e2)
| e0 = op(e1,e1)
| e0 = op(e1,e0) )
& ( e3 = op(e3,e0)
| e3 = op(e2,e0)
| e3 = op(e1,e0)
| e3 = op(e0,e0) )
& ( e3 = op(e0,e3)
| e3 = op(e0,e2)
| e3 = op(e0,e1)
| e3 = op(e0,e0) )
& ( e2 = op(e3,e0)
| e2 = op(e2,e0)
| e2 = op(e1,e0)
| e2 = op(e0,e0) )
& ( e2 = op(e0,e3)
| e2 = op(e0,e2)
| e2 = op(e0,e1)
| e2 = op(e0,e0) )
& ( e1 = op(e3,e0)
| e1 = op(e2,e0)
| e1 = op(e1,e0)
| e1 = op(e0,e0) )
& ( e1 = op(e0,e3)
| e1 = op(e0,e2)
| e1 = op(e0,e1)
| e1 = op(e0,e0) )
& ( e0 = op(e3,e0)
| e0 = op(e2,e0)
| e0 = op(e1,e0)
| e0 = op(e0,e0) )
& ( e0 = op(e0,e3)
| e0 = op(e0,e2)
| e0 = op(e0,e1)
| e0 = op(e0,e0) )
& ( e3 = unit
| e2 = unit
| e1 = unit
| e0 = unit )
& e3 = op(e3,unit)
& e3 = op(unit,e3)
& e2 = op(e2,unit)
& e2 = op(unit,e2)
& e1 = op(e1,unit)
& e1 = op(unit,e1)
& e0 = op(e0,unit)
& e0 = op(unit,e0)
& ( e3 = op(e3,e3)
| e2 = op(e3,e3)
| e1 = op(e3,e3)
| e0 = op(e3,e3) )
& ( e3 = op(e3,e2)
| e2 = op(e3,e2)
| e1 = op(e3,e2)
| e0 = op(e3,e2) )
& ( e3 = op(e3,e1)
| e2 = op(e3,e1)
| e1 = op(e3,e1)
| e0 = op(e3,e1) )
& ( e3 = op(e3,e0)
| e2 = op(e3,e0)
| e1 = op(e3,e0)
| e0 = op(e3,e0) )
& ( e3 = op(e2,e3)
| e2 = op(e2,e3)
| e1 = op(e2,e3)
| e0 = op(e2,e3) )
& ( e3 = op(e2,e2)
| e2 = op(e2,e2)
| e1 = op(e2,e2)
| e0 = op(e2,e2) )
& ( e3 = op(e2,e1)
| e2 = op(e2,e1)
| e1 = op(e2,e1)
| e0 = op(e2,e1) )
& ( e3 = op(e2,e0)
| e2 = op(e2,e0)
| e1 = op(e2,e0)
| e0 = op(e2,e0) )
& ( e3 = op(e1,e3)
| e2 = op(e1,e3)
| e1 = op(e1,e3)
| e0 = op(e1,e3) )
& ( e3 = op(e1,e2)
| e2 = op(e1,e2)
| e1 = op(e1,e2)
| e0 = op(e1,e2) )
& ( e3 = op(e1,e1)
| e2 = op(e1,e1)
| e1 = op(e1,e1)
| e0 = op(e1,e1) )
& ( e3 = op(e1,e0)
| e2 = op(e1,e0)
| e1 = op(e1,e0)
| e0 = op(e1,e0) )
& ( e3 = op(e0,e3)
| e2 = op(e0,e3)
| e1 = op(e0,e3)
| e0 = op(e0,e3) )
& ( e3 = op(e0,e2)
| e2 = op(e0,e2)
| e1 = op(e0,e2)
| e0 = op(e0,e2) )
& ( e3 = op(e0,e1)
| e2 = op(e0,e1)
| e1 = op(e0,e1)
| e0 = op(e0,e1) )
& ( e3 = op(e0,e0)
| e2 = op(e0,e0)
| e1 = op(e0,e0)
| e0 = op(e0,e0) )
& ( ( e3 = op(e3,e3)
& e3 = op(e2,e2)
& e3 = op(e1,e1)
& e3 = op(e0,e0) )
| ( e2 = op(e3,e3)
& e2 = op(e2,e2)
& e2 = op(e1,e1)
& e2 = op(e0,e0) )
| ( e1 = op(e3,e3)
& e1 = op(e2,e2)
& e1 = op(e1,e1)
& e1 = op(e0,e0) )
| ( e0 = op(e3,e3)
& e0 = op(e2,e2)
& e0 = op(e1,e1)
& e0 = op(e0,e0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1)).
fof(f5,negated_conjecture,(
~ ( ( e3 = op(e3,e3)
| e3 = op(e2,e3)
| e3 = op(e1,e3)
| e3 = op(e0,e3) )
& ( e3 = op(e3,e3)
| e3 = op(e3,e2)
| e3 = op(e3,e1)
| e3 = op(e3,e0) )
& ( e2 = op(e3,e3)
| e2 = op(e2,e3)
| e2 = op(e1,e3)
| e2 = op(e0,e3) )
& ( e2 = op(e3,e3)
| e2 = op(e3,e2)
| e2 = op(e3,e1)
| e2 = op(e3,e0) )
& ( e1 = op(e3,e3)
| e1 = op(e2,e3)
| e1 = op(e1,e3)
| e1 = op(e0,e3) )
& ( e1 = op(e3,e3)
| e1 = op(e3,e2)
| e1 = op(e3,e1)
| e1 = op(e3,e0) )
& ( e0 = op(e3,e3)
| e0 = op(e2,e3)
| e0 = op(e1,e3)
| e0 = op(e0,e3) )
& ( e0 = op(e3,e3)
| e0 = op(e3,e2)
| e0 = op(e3,e1)
| e0 = op(e3,e0) )
& ( e3 = op(e3,e2)
| e3 = op(e2,e2)
| e3 = op(e1,e2)
| e3 = op(e0,e2) )
& ( e3 = op(e2,e3)
| e3 = op(e2,e2)
| e3 = op(e2,e1)
| e3 = op(e2,e0) )
& ( e2 = op(e3,e2)
| e2 = op(e2,e2)
| e2 = op(e1,e2)
| e2 = op(e0,e2) )
& ( e2 = op(e2,e3)
| e2 = op(e2,e2)
| e2 = op(e2,e1)
| e2 = op(e2,e0) )
& ( e1 = op(e3,e2)
| e1 = op(e2,e2)
| e1 = op(e1,e2)
| e1 = op(e0,e2) )
& ( e1 = op(e2,e3)
| e1 = op(e2,e2)
| e1 = op(e2,e1)
| e1 = op(e2,e0) )
& ( e0 = op(e3,e2)
| e0 = op(e2,e2)
| e0 = op(e1,e2)
| e0 = op(e0,e2) )
& ( e0 = op(e2,e3)
| e0 = op(e2,e2)
| e0 = op(e2,e1)
| e0 = op(e2,e0) )
& ( e3 = op(e3,e1)
| e3 = op(e2,e1)
| e3 = op(e1,e1)
| e3 = op(e0,e1) )
& ( e3 = op(e1,e3)
| e3 = op(e1,e2)
| e3 = op(e1,e1)
| e3 = op(e1,e0) )
& ( e2 = op(e3,e1)
| e2 = op(e2,e1)
| e2 = op(e1,e1)
| e2 = op(e0,e1) )
& ( e2 = op(e1,e3)
| e2 = op(e1,e2)
| e2 = op(e1,e1)
| e2 = op(e1,e0) )
& ( e1 = op(e3,e1)
| e1 = op(e2,e1)
| e1 = op(e1,e1)
| e1 = op(e0,e1) )
& ( e1 = op(e1,e3)
| e1 = op(e1,e2)
| e1 = op(e1,e1)
| e1 = op(e1,e0) )
& ( e0 = op(e3,e1)
| e0 = op(e2,e1)
| e0 = op(e1,e1)
| e0 = op(e0,e1) )
& ( e0 = op(e1,e3)
| e0 = op(e1,e2)
| e0 = op(e1,e1)
| e0 = op(e1,e0) )
& ( e3 = op(e3,e0)
| e3 = op(e2,e0)
| e3 = op(e1,e0)
| e3 = op(e0,e0) )
& ( e3 = op(e0,e3)
| e3 = op(e0,e2)
| e3 = op(e0,e1)
| e3 = op(e0,e0) )
& ( e2 = op(e3,e0)
| e2 = op(e2,e0)
| e2 = op(e1,e0)
| e2 = op(e0,e0) )
& ( e2 = op(e0,e3)
| e2 = op(e0,e2)
| e2 = op(e0,e1)
| e2 = op(e0,e0) )
& ( e1 = op(e3,e0)
| e1 = op(e2,e0)
| e1 = op(e1,e0)
| e1 = op(e0,e0) )
& ( e1 = op(e0,e3)
| e1 = op(e0,e2)
| e1 = op(e0,e1)
| e1 = op(e0,e0) )
& ( e0 = op(e3,e0)
| e0 = op(e2,e0)
| e0 = op(e1,e0)
| e0 = op(e0,e0) )
& ( e0 = op(e0,e3)
| e0 = op(e0,e2)
| e0 = op(e0,e1)
| e0 = op(e0,e0) )
& ( e3 = unit
| e2 = unit
| e1 = unit
| e0 = unit )
& e3 = op(e3,unit)
& e3 = op(unit,e3)
& e2 = op(e2,unit)
& e2 = op(unit,e2)
& e1 = op(e1,unit)
& e1 = op(unit,e1)
& e0 = op(e0,unit)
& e0 = op(unit,e0)
& ( e3 = op(e3,e3)
| e2 = op(e3,e3)
| e1 = op(e3,e3)
| e0 = op(e3,e3) )
& ( e3 = op(e3,e2)
| e2 = op(e3,e2)
| e1 = op(e3,e2)
| e0 = op(e3,e2) )
& ( e3 = op(e3,e1)
| e2 = op(e3,e1)
| e1 = op(e3,e1)
| e0 = op(e3,e1) )
& ( e3 = op(e3,e0)
| e2 = op(e3,e0)
| e1 = op(e3,e0)
| e0 = op(e3,e0) )
& ( e3 = op(e2,e3)
| e2 = op(e2,e3)
| e1 = op(e2,e3)
| e0 = op(e2,e3) )
& ( e3 = op(e2,e2)
| e2 = op(e2,e2)
| e1 = op(e2,e2)
| e0 = op(e2,e2) )
& ( e3 = op(e2,e1)
| e2 = op(e2,e1)
| e1 = op(e2,e1)
| e0 = op(e2,e1) )
& ( e3 = op(e2,e0)
| e2 = op(e2,e0)
| e1 = op(e2,e0)
| e0 = op(e2,e0) )
& ( e3 = op(e1,e3)
| e2 = op(e1,e3)
| e1 = op(e1,e3)
| e0 = op(e1,e3) )
& ( e3 = op(e1,e2)
| e2 = op(e1,e2)
| e1 = op(e1,e2)
| e0 = op(e1,e2) )
& ( e3 = op(e1,e1)
| e2 = op(e1,e1)
| e1 = op(e1,e1)
| e0 = op(e1,e1) )
& ( e3 = op(e1,e0)
| e2 = op(e1,e0)
| e1 = op(e1,e0)
| e0 = op(e1,e0) )
& ( e3 = op(e0,e3)
| e2 = op(e0,e3)
| e1 = op(e0,e3)
| e0 = op(e0,e3) )
& ( e3 = op(e0,e2)
| e2 = op(e0,e2)
| e1 = op(e0,e2)
| e0 = op(e0,e2) )
& ( e3 = op(e0,e1)
| e2 = op(e0,e1)
| e1 = op(e0,e1)
| e0 = op(e0,e1) )
& ( e3 = op(e0,e0)
| e2 = op(e0,e0)
| e1 = op(e0,e0)
| e0 = op(e0,e0) )
& ( ( e3 = op(e3,e3)
& e3 = op(e2,e2)
& e3 = op(e1,e1)
& e3 = op(e0,e0) )
| ( e2 = op(e3,e3)
& e2 = op(e2,e2)
& e2 = op(e1,e1)
& e2 = op(e0,e0) )
| ( e1 = op(e3,e3)
& e1 = op(e2,e2)
& e1 = op(e1,e1)
& e1 = op(e0,e0) )
| ( e0 = op(e3,e3)
& e0 = op(e2,e2)
& e0 = op(e1,e1)
& e0 = op(e0,e0) ) ) ) ),
inference(negated_conjecture,[],[f4])).
fof(f6,plain,
( ( e3 != op(e3,e3)
& e3 != op(e2,e3)
& e3 != op(e1,e3)
& e3 != op(e0,e3) )
| ( e3 != op(e3,e3)
& e3 != op(e3,e2)
& e3 != op(e3,e1)
& e3 != op(e3,e0) )
| ( e2 != op(e3,e3)
& e2 != op(e2,e3)
& e2 != op(e1,e3)
& e2 != op(e0,e3) )
| ( e2 != op(e3,e3)
& e2 != op(e3,e2)
& e2 != op(e3,e1)
& e2 != op(e3,e0) )
| ( e1 != op(e3,e3)
& e1 != op(e2,e3)
& e1 != op(e1,e3)
& e1 != op(e0,e3) )
| ( e1 != op(e3,e3)
& e1 != op(e3,e2)
& e1 != op(e3,e1)
& e1 != op(e3,e0) )
| ( e0 != op(e3,e3)
& e0 != op(e2,e3)
& e0 != op(e1,e3)
& e0 != op(e0,e3) )
| ( e0 != op(e3,e3)
& e0 != op(e3,e2)
& e0 != op(e3,e1)
& e0 != op(e3,e0) )
| ( e3 != op(e3,e2)
& e3 != op(e2,e2)
& e3 != op(e1,e2)
& e3 != op(e0,e2) )
| ( e3 != op(e2,e3)
& e3 != op(e2,e2)
& e3 != op(e2,e1)
& e3 != op(e2,e0) )
| ( e2 != op(e3,e2)
& e2 != op(e2,e2)
& e2 != op(e1,e2)
& e2 != op(e0,e2) )
| ( e2 != op(e2,e3)
& e2 != op(e2,e2)
& e2 != op(e2,e1)
& e2 != op(e2,e0) )
| ( e1 != op(e3,e2)
& e1 != op(e2,e2)
& e1 != op(e1,e2)
& e1 != op(e0,e2) )
| ( e1 != op(e2,e3)
& e1 != op(e2,e2)
& e1 != op(e2,e1)
& e1 != op(e2,e0) )
| ( e0 != op(e3,e2)
& e0 != op(e2,e2)
& e0 != op(e1,e2)
& e0 != op(e0,e2) )
| ( e0 != op(e2,e3)
& e0 != op(e2,e2)
& e0 != op(e2,e1)
& e0 != op(e2,e0) )
| ( e3 != op(e3,e1)
& e3 != op(e2,e1)
& e3 != op(e1,e1)
& e3 != op(e0,e1) )
| ( e3 != op(e1,e3)
& e3 != op(e1,e2)
& e3 != op(e1,e1)
& e3 != op(e1,e0) )
| ( e2 != op(e3,e1)
& e2 != op(e2,e1)
& e2 != op(e1,e1)
& e2 != op(e0,e1) )
| ( e2 != op(e1,e3)
& e2 != op(e1,e2)
& e2 != op(e1,e1)
& e2 != op(e1,e0) )
| ( e1 != op(e3,e1)
& e1 != op(e2,e1)
& e1 != op(e1,e1)
& e1 != op(e0,e1) )
| ( e1 != op(e1,e3)
& e1 != op(e1,e2)
& e1 != op(e1,e1)
& e1 != op(e1,e0) )
| ( e0 != op(e3,e1)
& e0 != op(e2,e1)
& e0 != op(e1,e1)
& e0 != op(e0,e1) )
| ( e0 != op(e1,e3)
& e0 != op(e1,e2)
& e0 != op(e1,e1)
& e0 != op(e1,e0) )
| ( e3 != op(e3,e0)
& e3 != op(e2,e0)
& e3 != op(e1,e0)
& e3 != op(e0,e0) )
| ( e3 != op(e0,e3)
& e3 != op(e0,e2)
& e3 != op(e0,e1)
& e3 != op(e0,e0) )
| ( e2 != op(e3,e0)
& e2 != op(e2,e0)
& e2 != op(e1,e0)
& e2 != op(e0,e0) )
| ( e2 != op(e0,e3)
& e2 != op(e0,e2)
& e2 != op(e0,e1)
& e2 != op(e0,e0) )
| ( e1 != op(e3,e0)
& e1 != op(e2,e0)
& e1 != op(e1,e0)
& e1 != op(e0,e0) )
| ( e1 != op(e0,e3)
& e1 != op(e0,e2)
& e1 != op(e0,e1)
& e1 != op(e0,e0) )
| ( e0 != op(e3,e0)
& e0 != op(e2,e0)
& e0 != op(e1,e0)
& e0 != op(e0,e0) )
| ( e0 != op(e0,e3)
& e0 != op(e0,e2)
& e0 != op(e0,e1)
& e0 != op(e0,e0) )
| ( e3 != unit
& e2 != unit
& e1 != unit
& e0 != unit )
| e3 != op(e3,unit)
| e3 != op(unit,e3)
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| e0 != op(e0,unit)
| e0 != op(unit,e0)
| ( e3 != op(e3,e3)
& e2 != op(e3,e3)
& e1 != op(e3,e3)
& e0 != op(e3,e3) )
| ( e3 != op(e3,e2)
& e2 != op(e3,e2)
& e1 != op(e3,e2)
& e0 != op(e3,e2) )
| ( e3 != op(e3,e1)
& e2 != op(e3,e1)
& e1 != op(e3,e1)
& e0 != op(e3,e1) )
| ( e3 != op(e3,e0)
& e2 != op(e3,e0)
& e1 != op(e3,e0)
& e0 != op(e3,e0) )
| ( e3 != op(e2,e3)
& e2 != op(e2,e3)
& e1 != op(e2,e3)
& e0 != op(e2,e3) )
| ( e3 != op(e2,e2)
& e2 != op(e2,e2)
& e1 != op(e2,e2)
& e0 != op(e2,e2) )
| ( e3 != op(e2,e1)
& e2 != op(e2,e1)
& e1 != op(e2,e1)
& e0 != op(e2,e1) )
| ( e3 != op(e2,e0)
& e2 != op(e2,e0)
& e1 != op(e2,e0)
& e0 != op(e2,e0) )
| ( e3 != op(e1,e3)
& e2 != op(e1,e3)
& e1 != op(e1,e3)
& e0 != op(e1,e3) )
| ( e3 != op(e1,e2)
& e2 != op(e1,e2)
& e1 != op(e1,e2)
& e0 != op(e1,e2) )
| ( e3 != op(e1,e1)
& e2 != op(e1,e1)
& e1 != op(e1,e1)
& e0 != op(e1,e1) )
| ( e3 != op(e1,e0)
& e2 != op(e1,e0)
& e1 != op(e1,e0)
& e0 != op(e1,e0) )
| ( e3 != op(e0,e3)
& e2 != op(e0,e3)
& e1 != op(e0,e3)
& e0 != op(e0,e3) )
| ( e3 != op(e0,e2)
& e2 != op(e0,e2)
& e1 != op(e0,e2)
& e0 != op(e0,e2) )
| ( e3 != op(e0,e1)
& e2 != op(e0,e1)
& e1 != op(e0,e1)
& e0 != op(e0,e1) )
| ( e3 != op(e0,e0)
& e2 != op(e0,e0)
& e1 != op(e0,e0)
& e0 != op(e0,e0) )
| ( ( e3 != op(e3,e3)
| e3 != op(e2,e2)
| e3 != op(e1,e1)
| e3 != op(e0,e0) )
& ( e2 != op(e3,e3)
| e2 != op(e2,e2)
| e2 != op(e1,e1)
| e2 != op(e0,e0) )
& ( e1 != op(e3,e3)
| e1 != op(e2,e2)
| e1 != op(e1,e1)
| e1 != op(e0,e0) )
& ( e0 != op(e3,e3)
| e0 != op(e2,e2)
| e0 != op(e1,e1)
| e0 != op(e0,e0) ) ) ),
inference(ennf_transformation,[],[f5])).
fof(f7,plain,
( ( ( e3 != op(e3,e3)
| e3 != op(e2,e2)
| e3 != op(e1,e1)
| e3 != op(e0,e0) )
& ( e2 != op(e3,e3)
| e2 != op(e2,e2)
| e2 != op(e1,e1)
| e2 != op(e0,e0) )
& ( e1 != op(e3,e3)
| e1 != op(e2,e2)
| e1 != op(e1,e1)
| e1 != op(e0,e0) )
& ( e0 != op(e3,e3)
| e0 != op(e2,e2)
| e0 != op(e1,e1)
| e0 != op(e0,e0) ) )
| ~ sP0 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP0])])).
fof(f8,plain,
( ( e3 != op(e0,e0)
& e2 != op(e0,e0)
& e1 != op(e0,e0)
& e0 != op(e0,e0) )
| ~ sP1 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP1])])).
fof(f9,plain,
( ( e3 != op(e0,e1)
& e2 != op(e0,e1)
& e1 != op(e0,e1)
& e0 != op(e0,e1) )
| ~ sP2 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP2])])).
fof(f10,plain,
( ( e3 != op(e0,e2)
& e2 != op(e0,e2)
& e1 != op(e0,e2)
& e0 != op(e0,e2) )
| ~ sP3 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP3])])).
fof(f11,plain,
( ( e3 != op(e0,e3)
& e2 != op(e0,e3)
& e1 != op(e0,e3)
& e0 != op(e0,e3) )
| ~ sP4 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP4])])).
fof(f12,plain,
( ( e3 != op(e1,e0)
& e2 != op(e1,e0)
& e1 != op(e1,e0)
& e0 != op(e1,e0) )
| ~ sP5 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP5])])).
fof(f13,plain,
( ( e3 != op(e1,e1)
& e2 != op(e1,e1)
& e1 != op(e1,e1)
& e0 != op(e1,e1) )
| ~ sP6 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP6])])).
fof(f14,plain,
( ( e3 != op(e1,e2)
& e2 != op(e1,e2)
& e1 != op(e1,e2)
& e0 != op(e1,e2) )
| ~ sP7 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP7])])).
fof(f15,plain,
( ( e3 != op(e1,e3)
& e2 != op(e1,e3)
& e1 != op(e1,e3)
& e0 != op(e1,e3) )
| ~ sP8 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP8])])).
fof(f16,plain,
( ( e3 != op(e2,e0)
& e2 != op(e2,e0)
& e1 != op(e2,e0)
& e0 != op(e2,e0) )
| ~ sP9 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP9])])).
fof(f17,plain,
( ( e3 != op(e2,e1)
& e2 != op(e2,e1)
& e1 != op(e2,e1)
& e0 != op(e2,e1) )
| ~ sP10 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP10])])).
fof(f18,plain,
( ( e3 != op(e2,e2)
& e2 != op(e2,e2)
& e1 != op(e2,e2)
& e0 != op(e2,e2) )
| ~ sP11 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP11])])).
fof(f19,plain,
( ( e3 != op(e2,e3)
& e2 != op(e2,e3)
& e1 != op(e2,e3)
& e0 != op(e2,e3) )
| ~ sP12 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP12])])).
fof(f20,plain,
( ( e3 != op(e3,e0)
& e2 != op(e3,e0)
& e1 != op(e3,e0)
& e0 != op(e3,e0) )
| ~ sP13 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP13])])).
fof(f21,plain,
( ( e3 != op(e3,e1)
& e2 != op(e3,e1)
& e1 != op(e3,e1)
& e0 != op(e3,e1) )
| ~ sP14 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP14])])).
fof(f22,plain,
( ( e3 != op(e3,e2)
& e2 != op(e3,e2)
& e1 != op(e3,e2)
& e0 != op(e3,e2) )
| ~ sP15 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP15])])).
fof(f23,plain,
( ( e3 != op(e3,e3)
& e2 != op(e3,e3)
& e1 != op(e3,e3)
& e0 != op(e3,e3) )
| ~ sP16 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP16])])).
fof(f24,plain,
( ( e3 != unit
& e2 != unit
& e1 != unit
& e0 != unit )
| ~ sP17 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP17])])).
fof(f25,plain,
( ( e0 != op(e0,e3)
& e0 != op(e0,e2)
& e0 != op(e0,e1)
& e0 != op(e0,e0) )
| ~ sP18 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP18])])).
fof(f26,plain,
( ( e0 != op(e3,e0)
& e0 != op(e2,e0)
& e0 != op(e1,e0)
& e0 != op(e0,e0) )
| ~ sP19 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP19])])).
fof(f27,plain,
( ( e1 != op(e0,e3)
& e1 != op(e0,e2)
& e1 != op(e0,e1)
& e1 != op(e0,e0) )
| ~ sP20 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP20])])).
fof(f28,plain,
( ( e1 != op(e3,e0)
& e1 != op(e2,e0)
& e1 != op(e1,e0)
& e1 != op(e0,e0) )
| ~ sP21 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP21])])).
fof(f29,plain,
( ( e2 != op(e0,e3)
& e2 != op(e0,e2)
& e2 != op(e0,e1)
& e2 != op(e0,e0) )
| ~ sP22 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP22])])).
fof(f30,plain,
( ( e2 != op(e3,e0)
& e2 != op(e2,e0)
& e2 != op(e1,e0)
& e2 != op(e0,e0) )
| ~ sP23 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP23])])).
fof(f31,plain,
( ( e3 != op(e0,e3)
& e3 != op(e0,e2)
& e3 != op(e0,e1)
& e3 != op(e0,e0) )
| ~ sP24 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP24])])).
fof(f32,plain,
( ( e3 != op(e3,e0)
& e3 != op(e2,e0)
& e3 != op(e1,e0)
& e3 != op(e0,e0) )
| ~ sP25 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP25])])).
fof(f33,plain,
( ( e0 != op(e1,e3)
& e0 != op(e1,e2)
& e0 != op(e1,e1)
& e0 != op(e1,e0) )
| ~ sP26 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP26])])).
fof(f34,plain,
( ( e0 != op(e3,e1)
& e0 != op(e2,e1)
& e0 != op(e1,e1)
& e0 != op(e0,e1) )
| ~ sP27 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP27])])).
fof(f35,plain,
( ( e1 != op(e1,e3)
& e1 != op(e1,e2)
& e1 != op(e1,e1)
& e1 != op(e1,e0) )
| ~ sP28 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP28])])).
fof(f36,plain,
( ( e1 != op(e3,e1)
& e1 != op(e2,e1)
& e1 != op(e1,e1)
& e1 != op(e0,e1) )
| ~ sP29 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP29])])).
fof(f37,plain,
( ( e2 != op(e1,e3)
& e2 != op(e1,e2)
& e2 != op(e1,e1)
& e2 != op(e1,e0) )
| ~ sP30 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP30])])).
fof(f38,plain,
( ( e2 != op(e3,e1)
& e2 != op(e2,e1)
& e2 != op(e1,e1)
& e2 != op(e0,e1) )
| ~ sP31 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP31])])).
fof(f39,plain,
( ( e3 != op(e1,e3)
& e3 != op(e1,e2)
& e3 != op(e1,e1)
& e3 != op(e1,e0) )
| ~ sP32 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP32])])).
fof(f40,plain,
( ( e3 != op(e3,e1)
& e3 != op(e2,e1)
& e3 != op(e1,e1)
& e3 != op(e0,e1) )
| ~ sP33 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP33])])).
fof(f41,plain,
( ( e0 != op(e2,e3)
& e0 != op(e2,e2)
& e0 != op(e2,e1)
& e0 != op(e2,e0) )
| ~ sP34 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP34])])).
fof(f42,plain,
( ( e0 != op(e3,e2)
& e0 != op(e2,e2)
& e0 != op(e1,e2)
& e0 != op(e0,e2) )
| ~ sP35 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP35])])).
fof(f43,plain,
( ( e1 != op(e2,e3)
& e1 != op(e2,e2)
& e1 != op(e2,e1)
& e1 != op(e2,e0) )
| ~ sP36 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP36])])).
fof(f44,plain,
( ( e1 != op(e3,e2)
& e1 != op(e2,e2)
& e1 != op(e1,e2)
& e1 != op(e0,e2) )
| ~ sP37 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP37])])).
fof(f45,plain,
( ( e2 != op(e2,e3)
& e2 != op(e2,e2)
& e2 != op(e2,e1)
& e2 != op(e2,e0) )
| ~ sP38 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP38])])).
fof(f46,plain,
( ( e2 != op(e3,e2)
& e2 != op(e2,e2)
& e2 != op(e1,e2)
& e2 != op(e0,e2) )
| ~ sP39 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP39])])).
fof(f47,plain,
( ( e3 != op(e2,e3)
& e3 != op(e2,e2)
& e3 != op(e2,e1)
& e3 != op(e2,e0) )
| ~ sP40 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP40])])).
fof(f48,plain,
( ( e3 != op(e3,e2)
& e3 != op(e2,e2)
& e3 != op(e1,e2)
& e3 != op(e0,e2) )
| ~ sP41 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP41])])).
fof(f49,plain,
( ( e0 != op(e3,e3)
& e0 != op(e3,e2)
& e0 != op(e3,e1)
& e0 != op(e3,e0) )
| ~ sP42 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP42])])).
fof(f50,plain,
( ( e0 != op(e3,e3)
& e0 != op(e2,e3)
& e0 != op(e1,e3)
& e0 != op(e0,e3) )
| ~ sP43 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP43])])).
fof(f51,plain,
( ( e1 != op(e3,e3)
& e1 != op(e3,e2)
& e1 != op(e3,e1)
& e1 != op(e3,e0) )
| ~ sP44 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP44])])).
fof(f52,plain,
( ( e1 != op(e3,e3)
& e1 != op(e2,e3)
& e1 != op(e1,e3)
& e1 != op(e0,e3) )
| ~ sP45 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP45])])).
fof(f53,plain,
( ( e2 != op(e3,e3)
& e2 != op(e3,e2)
& e2 != op(e3,e1)
& e2 != op(e3,e0) )
| ~ sP46 ),
introduced(predicate_definition_introduction,[new_symbols(naming,[sP46])])).
fof(f54,plain,
( ( e3 != op(e3,e3)
& e3 != op(e2,e3)
& e3 != op(e1,e3)
& e3 != op(e0,e3) )
| ( e3 != op(e3,e3)
& e3 != op(e3,e2)
& e3 != op(e3,e1)
& e3 != op(e3,e0) )
| ( e2 != op(e3,e3)
& e2 != op(e2,e3)
& e2 != op(e1,e3)
& e2 != op(e0,e3) )
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP29
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| e3 != op(e3,unit)
| e3 != op(unit,e3)
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| e0 != op(e0,unit)
| e0 != op(unit,e0)
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(definition_folding,[],[f6,f53,f52,f51,f50,f49,f48,f47,f46,f45,f44,f43,f42,f41,f40,f39,f38,f37,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7])).
fof(f55,plain,
( ( e2 != op(e3,e3)
& e2 != op(e3,e2)
& e2 != op(e3,e1)
& e2 != op(e3,e0) )
| ~ sP46 ),
inference(nnf_transformation,[],[f53])).
fof(f56,plain,
( ( e1 != op(e3,e3)
& e1 != op(e2,e3)
& e1 != op(e1,e3)
& e1 != op(e0,e3) )
| ~ sP45 ),
inference(nnf_transformation,[],[f52])).
fof(f57,plain,
( ( e1 != op(e3,e3)
& e1 != op(e3,e2)
& e1 != op(e3,e1)
& e1 != op(e3,e0) )
| ~ sP44 ),
inference(nnf_transformation,[],[f51])).
fof(f58,plain,
( ( e0 != op(e3,e3)
& e0 != op(e2,e3)
& e0 != op(e1,e3)
& e0 != op(e0,e3) )
| ~ sP43 ),
inference(nnf_transformation,[],[f50])).
fof(f59,plain,
( ( e0 != op(e3,e3)
& e0 != op(e3,e2)
& e0 != op(e3,e1)
& e0 != op(e3,e0) )
| ~ sP42 ),
inference(nnf_transformation,[],[f49])).
fof(f60,plain,
( ( e3 != op(e3,e2)
& e3 != op(e2,e2)
& e3 != op(e1,e2)
& e3 != op(e0,e2) )
| ~ sP41 ),
inference(nnf_transformation,[],[f48])).
fof(f61,plain,
( ( e3 != op(e2,e3)
& e3 != op(e2,e2)
& e3 != op(e2,e1)
& e3 != op(e2,e0) )
| ~ sP40 ),
inference(nnf_transformation,[],[f47])).
fof(f62,plain,
( ( e2 != op(e3,e2)
& e2 != op(e2,e2)
& e2 != op(e1,e2)
& e2 != op(e0,e2) )
| ~ sP39 ),
inference(nnf_transformation,[],[f46])).
fof(f63,plain,
( ( e2 != op(e2,e3)
& e2 != op(e2,e2)
& e2 != op(e2,e1)
& e2 != op(e2,e0) )
| ~ sP38 ),
inference(nnf_transformation,[],[f45])).
fof(f64,plain,
( ( e1 != op(e3,e2)
& e1 != op(e2,e2)
& e1 != op(e1,e2)
& e1 != op(e0,e2) )
| ~ sP37 ),
inference(nnf_transformation,[],[f44])).
fof(f65,plain,
( ( e1 != op(e2,e3)
& e1 != op(e2,e2)
& e1 != op(e2,e1)
& e1 != op(e2,e0) )
| ~ sP36 ),
inference(nnf_transformation,[],[f43])).
fof(f66,plain,
( ( e0 != op(e3,e2)
& e0 != op(e2,e2)
& e0 != op(e1,e2)
& e0 != op(e0,e2) )
| ~ sP35 ),
inference(nnf_transformation,[],[f42])).
fof(f67,plain,
( ( e0 != op(e2,e3)
& e0 != op(e2,e2)
& e0 != op(e2,e1)
& e0 != op(e2,e0) )
| ~ sP34 ),
inference(nnf_transformation,[],[f41])).
fof(f68,plain,
( ( e3 != op(e3,e1)
& e3 != op(e2,e1)
& e3 != op(e1,e1)
& e3 != op(e0,e1) )
| ~ sP33 ),
inference(nnf_transformation,[],[f40])).
fof(f69,plain,
( ( e3 != op(e1,e3)
& e3 != op(e1,e2)
& e3 != op(e1,e1)
& e3 != op(e1,e0) )
| ~ sP32 ),
inference(nnf_transformation,[],[f39])).
fof(f70,plain,
( ( e2 != op(e3,e1)
& e2 != op(e2,e1)
& e2 != op(e1,e1)
& e2 != op(e0,e1) )
| ~ sP31 ),
inference(nnf_transformation,[],[f38])).
fof(f71,plain,
( ( e2 != op(e1,e3)
& e2 != op(e1,e2)
& e2 != op(e1,e1)
& e2 != op(e1,e0) )
| ~ sP30 ),
inference(nnf_transformation,[],[f37])).
fof(f72,plain,
( ( e1 != op(e3,e1)
& e1 != op(e2,e1)
& e1 != op(e1,e1)
& e1 != op(e0,e1) )
| ~ sP29 ),
inference(nnf_transformation,[],[f36])).
fof(f73,plain,
( ( e1 != op(e1,e3)
& e1 != op(e1,e2)
& e1 != op(e1,e1)
& e1 != op(e1,e0) )
| ~ sP28 ),
inference(nnf_transformation,[],[f35])).
fof(f74,plain,
( ( e0 != op(e3,e1)
& e0 != op(e2,e1)
& e0 != op(e1,e1)
& e0 != op(e0,e1) )
| ~ sP27 ),
inference(nnf_transformation,[],[f34])).
fof(f75,plain,
( ( e0 != op(e1,e3)
& e0 != op(e1,e2)
& e0 != op(e1,e1)
& e0 != op(e1,e0) )
| ~ sP26 ),
inference(nnf_transformation,[],[f33])).
fof(f76,plain,
( ( e3 != op(e3,e0)
& e3 != op(e2,e0)
& e3 != op(e1,e0)
& e3 != op(e0,e0) )
| ~ sP25 ),
inference(nnf_transformation,[],[f32])).
fof(f77,plain,
( ( e3 != op(e0,e3)
& e3 != op(e0,e2)
& e3 != op(e0,e1)
& e3 != op(e0,e0) )
| ~ sP24 ),
inference(nnf_transformation,[],[f31])).
fof(f78,plain,
( ( e2 != op(e3,e0)
& e2 != op(e2,e0)
& e2 != op(e1,e0)
& e2 != op(e0,e0) )
| ~ sP23 ),
inference(nnf_transformation,[],[f30])).
fof(f79,plain,
( ( e2 != op(e0,e3)
& e2 != op(e0,e2)
& e2 != op(e0,e1)
& e2 != op(e0,e0) )
| ~ sP22 ),
inference(nnf_transformation,[],[f29])).
fof(f80,plain,
( ( e1 != op(e3,e0)
& e1 != op(e2,e0)
& e1 != op(e1,e0)
& e1 != op(e0,e0) )
| ~ sP21 ),
inference(nnf_transformation,[],[f28])).
fof(f81,plain,
( ( e1 != op(e0,e3)
& e1 != op(e0,e2)
& e1 != op(e0,e1)
& e1 != op(e0,e0) )
| ~ sP20 ),
inference(nnf_transformation,[],[f27])).
fof(f82,plain,
( ( e0 != op(e3,e0)
& e0 != op(e2,e0)
& e0 != op(e1,e0)
& e0 != op(e0,e0) )
| ~ sP19 ),
inference(nnf_transformation,[],[f26])).
fof(f83,plain,
( ( e0 != op(e0,e3)
& e0 != op(e0,e2)
& e0 != op(e0,e1)
& e0 != op(e0,e0) )
| ~ sP18 ),
inference(nnf_transformation,[],[f25])).
fof(f84,plain,
( ( e3 != unit
& e2 != unit
& e1 != unit
& e0 != unit )
| ~ sP17 ),
inference(nnf_transformation,[],[f24])).
fof(f85,plain,
( ( e3 != op(e3,e3)
& e2 != op(e3,e3)
& e1 != op(e3,e3)
& e0 != op(e3,e3) )
| ~ sP16 ),
inference(nnf_transformation,[],[f23])).
fof(f86,plain,
( ( e3 != op(e3,e2)
& e2 != op(e3,e2)
& e1 != op(e3,e2)
& e0 != op(e3,e2) )
| ~ sP15 ),
inference(nnf_transformation,[],[f22])).
fof(f87,plain,
( ( e3 != op(e3,e1)
& e2 != op(e3,e1)
& e1 != op(e3,e1)
& e0 != op(e3,e1) )
| ~ sP14 ),
inference(nnf_transformation,[],[f21])).
fof(f88,plain,
( ( e3 != op(e3,e0)
& e2 != op(e3,e0)
& e1 != op(e3,e0)
& e0 != op(e3,e0) )
| ~ sP13 ),
inference(nnf_transformation,[],[f20])).
fof(f89,plain,
( ( e3 != op(e2,e3)
& e2 != op(e2,e3)
& e1 != op(e2,e3)
& e0 != op(e2,e3) )
| ~ sP12 ),
inference(nnf_transformation,[],[f19])).
fof(f90,plain,
( ( e3 != op(e2,e2)
& e2 != op(e2,e2)
& e1 != op(e2,e2)
& e0 != op(e2,e2) )
| ~ sP11 ),
inference(nnf_transformation,[],[f18])).
fof(f91,plain,
( ( e3 != op(e2,e1)
& e2 != op(e2,e1)
& e1 != op(e2,e1)
& e0 != op(e2,e1) )
| ~ sP10 ),
inference(nnf_transformation,[],[f17])).
fof(f92,plain,
( ( e3 != op(e2,e0)
& e2 != op(e2,e0)
& e1 != op(e2,e0)
& e0 != op(e2,e0) )
| ~ sP9 ),
inference(nnf_transformation,[],[f16])).
fof(f93,plain,
( ( e3 != op(e1,e3)
& e2 != op(e1,e3)
& e1 != op(e1,e3)
& e0 != op(e1,e3) )
| ~ sP8 ),
inference(nnf_transformation,[],[f15])).
fof(f94,plain,
( ( e3 != op(e1,e2)
& e2 != op(e1,e2)
& e1 != op(e1,e2)
& e0 != op(e1,e2) )
| ~ sP7 ),
inference(nnf_transformation,[],[f14])).
fof(f95,plain,
( ( e3 != op(e1,e1)
& e2 != op(e1,e1)
& e1 != op(e1,e1)
& e0 != op(e1,e1) )
| ~ sP6 ),
inference(nnf_transformation,[],[f13])).
fof(f96,plain,
( ( e3 != op(e1,e0)
& e2 != op(e1,e0)
& e1 != op(e1,e0)
& e0 != op(e1,e0) )
| ~ sP5 ),
inference(nnf_transformation,[],[f12])).
fof(f97,plain,
( ( e3 != op(e0,e3)
& e2 != op(e0,e3)
& e1 != op(e0,e3)
& e0 != op(e0,e3) )
| ~ sP4 ),
inference(nnf_transformation,[],[f11])).
fof(f98,plain,
( ( e3 != op(e0,e2)
& e2 != op(e0,e2)
& e1 != op(e0,e2)
& e0 != op(e0,e2) )
| ~ sP3 ),
inference(nnf_transformation,[],[f10])).
fof(f99,plain,
( ( e3 != op(e0,e1)
& e2 != op(e0,e1)
& e1 != op(e0,e1)
& e0 != op(e0,e1) )
| ~ sP2 ),
inference(nnf_transformation,[],[f9])).
fof(f100,plain,
( ( e3 != op(e0,e0)
& e2 != op(e0,e0)
& e1 != op(e0,e0)
& e0 != op(e0,e0) )
| ~ sP1 ),
inference(nnf_transformation,[],[f8])).
fof(f101,plain,
( ( ( e3 != op(e3,e3)
| e3 != op(e2,e2)
| e3 != op(e1,e1)
| e3 != op(e0,e0) )
& ( e2 != op(e3,e3)
| e2 != op(e2,e2)
| e2 != op(e1,e1)
| e2 != op(e0,e0) )
& ( e1 != op(e3,e3)
| e1 != op(e2,e2)
| e1 != op(e1,e1)
| e1 != op(e0,e0) )
& ( e0 != op(e3,e3)
| e0 != op(e2,e2)
| e0 != op(e1,e1)
| e0 != op(e0,e0) ) )
| ~ sP0 ),
inference(nnf_transformation,[],[f7])).
fof(f103,plain,
( e2 != op(e3,e1)
| ~ sP46 ),
inference(cnf_transformation,[],[f55])).
fof(f108,plain,
( e1 != op(e2,e3)
| ~ sP45 ),
inference(cnf_transformation,[],[f56])).
fof(f112,plain,
( e1 != op(e3,e2)
| ~ sP44 ),
inference(cnf_transformation,[],[f57])).
fof(f117,plain,
( e0 != op(e3,e3)
| ~ sP43 ),
inference(cnf_transformation,[],[f58])).
fof(f121,plain,
( e0 != op(e3,e3)
| ~ sP42 ),
inference(cnf_transformation,[],[f59])).
fof(f123,plain,
( e3 != op(e1,e2)
| ~ sP41 ),
inference(cnf_transformation,[],[f60])).
fof(f127,plain,
( e3 != op(e2,e1)
| ~ sP40 ),
inference(cnf_transformation,[],[f61])).
fof(f130,plain,
( e2 != op(e0,e2)
| ~ sP39 ),
inference(cnf_transformation,[],[f62])).
fof(f134,plain,
( e2 != op(e2,e0)
| ~ sP38 ),
inference(cnf_transformation,[],[f63])).
fof(f141,plain,
( e1 != op(e3,e2)
| ~ sP37 ),
inference(cnf_transformation,[],[f64])).
fof(f145,plain,
( e1 != op(e2,e3)
| ~ sP36 ),
inference(cnf_transformation,[],[f65])).
fof(f148,plain,
( e0 != op(e2,e2)
| ~ sP35 ),
inference(cnf_transformation,[],[f66])).
fof(f152,plain,
( e0 != op(e2,e2)
| ~ sP34 ),
inference(cnf_transformation,[],[f67])).
fof(f156,plain,
( e3 != op(e2,e1)
| ~ sP33 ),
inference(cnf_transformation,[],[f68])).
fof(f160,plain,
( e3 != op(e1,e2)
| ~ sP32 ),
inference(cnf_transformation,[],[f69])).
fof(f165,plain,
( e2 != op(e3,e1)
| ~ sP31 ),
inference(cnf_transformation,[],[f70])).
fof(f169,plain,
( e2 != op(e1,e3)
| ~ sP30 ),
inference(cnf_transformation,[],[f71])).
fof(f170,plain,
( e1 != op(e0,e1)
| ~ sP29 ),
inference(cnf_transformation,[],[f72])).
fof(f174,plain,
( e1 != op(e1,e0)
| ~ sP28 ),
inference(cnf_transformation,[],[f73])).
fof(f179,plain,
( e0 != op(e1,e1)
| ~ sP27 ),
inference(cnf_transformation,[],[f74])).
fof(f183,plain,
( e0 != op(e1,e1)
| ~ sP26 ),
inference(cnf_transformation,[],[f75])).
fof(f189,plain,
( e3 != op(e3,e0)
| ~ sP25 ),
inference(cnf_transformation,[],[f76])).
fof(f193,plain,
( e3 != op(e0,e3)
| ~ sP24 ),
inference(cnf_transformation,[],[f77])).
fof(f196,plain,
( e2 != op(e2,e0)
| ~ sP23 ),
inference(cnf_transformation,[],[f78])).
fof(f200,plain,
( e2 != op(e0,e2)
| ~ sP22 ),
inference(cnf_transformation,[],[f79])).
fof(f203,plain,
( e1 != op(e1,e0)
| ~ sP21 ),
inference(cnf_transformation,[],[f80])).
fof(f207,plain,
( e1 != op(e0,e1)
| ~ sP20 ),
inference(cnf_transformation,[],[f81])).
fof(f210,plain,
( e0 != op(e0,e0)
| ~ sP19 ),
inference(cnf_transformation,[],[f82])).
fof(f214,plain,
( e0 != op(e0,e0)
| ~ sP18 ),
inference(cnf_transformation,[],[f83])).
fof(f218,plain,
( e0 != unit
| ~ sP17 ),
inference(cnf_transformation,[],[f84])).
fof(f222,plain,
( e0 != op(e3,e3)
| ~ sP16 ),
inference(cnf_transformation,[],[f85])).
fof(f227,plain,
( e1 != op(e3,e2)
| ~ sP15 ),
inference(cnf_transformation,[],[f86])).
fof(f232,plain,
( e2 != op(e3,e1)
| ~ sP14 ),
inference(cnf_transformation,[],[f87])).
fof(f237,plain,
( e3 != op(e3,e0)
| ~ sP13 ),
inference(cnf_transformation,[],[f88])).
fof(f239,plain,
( e1 != op(e2,e3)
| ~ sP12 ),
inference(cnf_transformation,[],[f89])).
fof(f242,plain,
( e0 != op(e2,e2)
| ~ sP11 ),
inference(cnf_transformation,[],[f90])).
fof(f249,plain,
( e3 != op(e2,e1)
| ~ sP10 ),
inference(cnf_transformation,[],[f91])).
fof(f252,plain,
( e2 != op(e2,e0)
| ~ sP9 ),
inference(cnf_transformation,[],[f92])).
fof(f256,plain,
( e2 != op(e1,e3)
| ~ sP8 ),
inference(cnf_transformation,[],[f93])).
fof(f261,plain,
( e3 != op(e1,e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f94])).
fof(f262,plain,
( e0 != op(e1,e1)
| ~ sP6 ),
inference(cnf_transformation,[],[f95])).
fof(f267,plain,
( e1 != op(e1,e0)
| ~ sP5 ),
inference(cnf_transformation,[],[f96])).
fof(f273,plain,
( e3 != op(e0,e3)
| ~ sP4 ),
inference(cnf_transformation,[],[f97])).
fof(f276,plain,
( e2 != op(e0,e2)
| ~ sP3 ),
inference(cnf_transformation,[],[f98])).
fof(f279,plain,
( e1 != op(e0,e1)
| ~ sP2 ),
inference(cnf_transformation,[],[f99])).
fof(f282,plain,
( e0 != op(e0,e0)
| ~ sP1 ),
inference(cnf_transformation,[],[f100])).
fof(f286,plain,
( e0 != op(e3,e3)
| e0 != op(e2,e2)
| e0 != op(e1,e1)
| e0 != op(e0,e0)
| ~ sP0 ),
inference(cnf_transformation,[],[f101])).
fof(f291,plain,
( e3 != op(e0,e3)
| e3 != op(e3,e0)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP29
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| e3 != op(e3,unit)
| e3 != op(unit,e3)
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| e0 != op(e0,unit)
| e0 != op(unit,e0)
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f54])).
fof(f354,plain,(
e0 = unit ),
inference(cnf_transformation,[],[f3])).
fof(f361,plain,(
e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f2])).
fof(f362,plain,(
e1 = op(e0,e1) ),
inference(cnf_transformation,[],[f2])).
fof(f363,plain,(
e2 = op(e0,e2) ),
inference(cnf_transformation,[],[f2])).
fof(f364,plain,(
e3 = op(e0,e3) ),
inference(cnf_transformation,[],[f2])).
fof(f365,plain,(
e1 = op(e1,e0) ),
inference(cnf_transformation,[],[f2])).
fof(f366,plain,(
e0 = op(e1,e1) ),
inference(cnf_transformation,[],[f2])).
fof(f367,plain,(
e3 = op(e1,e2) ),
inference(cnf_transformation,[],[f2])).
fof(f368,plain,(
e2 = op(e1,e3) ),
inference(cnf_transformation,[],[f2])).
fof(f369,plain,(
e2 = op(e2,e0) ),
inference(cnf_transformation,[],[f2])).
fof(f370,plain,(
e3 = op(e2,e1) ),
inference(cnf_transformation,[],[f2])).
fof(f371,plain,(
e0 = op(e2,e2) ),
inference(cnf_transformation,[],[f2])).
fof(f372,plain,(
e1 = op(e2,e3) ),
inference(cnf_transformation,[],[f2])).
fof(f373,plain,(
e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f2])).
fof(f374,plain,(
e2 = op(e3,e1) ),
inference(cnf_transformation,[],[f2])).
fof(f375,plain,(
e1 = op(e3,e2) ),
inference(cnf_transformation,[],[f2])).
fof(f376,plain,(
e0 = op(e3,e3) ),
inference(cnf_transformation,[],[f2])).
fof(f380,plain,
( op(e3,e3) != unit
| ~ sP43 ),
inference(definition_unfolding,[],[f117,f354])).
fof(f384,plain,
( op(e3,e3) != unit
| ~ sP42 ),
inference(definition_unfolding,[],[f121,f354])).
fof(f390,plain,
( e2 != op(unit,e2)
| ~ sP39 ),
inference(definition_unfolding,[],[f130,f354])).
fof(f391,plain,
( e2 != op(e2,unit)
| ~ sP38 ),
inference(definition_unfolding,[],[f134,f354])).
fof(f395,plain,
( op(e2,e2) != unit
| ~ sP35 ),
inference(definition_unfolding,[],[f148,f354])).
fof(f399,plain,
( op(e2,e2) != unit
| ~ sP34 ),
inference(definition_unfolding,[],[f152,f354])).
fof(f406,plain,
( e1 != op(unit,e1)
| ~ sP29 ),
inference(definition_unfolding,[],[f170,f354])).
fof(f407,plain,
( e1 != op(e1,unit)
| ~ sP28 ),
inference(definition_unfolding,[],[f174,f354])).
fof(f410,plain,
( op(e1,e1) != unit
| ~ sP27 ),
inference(definition_unfolding,[],[f179,f354])).
fof(f414,plain,
( op(e1,e1) != unit
| ~ sP26 ),
inference(definition_unfolding,[],[f183,f354])).
fof(f416,plain,
( e3 != op(e3,unit)
| ~ sP25 ),
inference(definition_unfolding,[],[f189,f354])).
fof(f420,plain,
( e3 != op(unit,e3)
| ~ sP24 ),
inference(definition_unfolding,[],[f193,f354])).
fof(f425,plain,
( e2 != op(e2,unit)
| ~ sP23 ),
inference(definition_unfolding,[],[f196,f354])).
fof(f429,plain,
( e2 != op(unit,e2)
| ~ sP22 ),
inference(definition_unfolding,[],[f200,f354])).
fof(f434,plain,
( e1 != op(e1,unit)
| ~ sP21 ),
inference(definition_unfolding,[],[f203,f354])).
fof(f438,plain,
( e1 != op(unit,e1)
| ~ sP20 ),
inference(definition_unfolding,[],[f207,f354])).
fof(f443,plain,
( op(unit,unit) != unit
| ~ sP19 ),
inference(definition_unfolding,[],[f210,f354,f354,f354])).
fof(f447,plain,
( op(unit,unit) != unit
| ~ sP18 ),
inference(definition_unfolding,[],[f214,f354,f354,f354])).
fof(f448,plain,
( unit != unit
| ~ sP17 ),
inference(definition_unfolding,[],[f218,f354])).
fof(f449,plain,
( op(e3,e3) != unit
| ~ sP16 ),
inference(definition_unfolding,[],[f222,f354])).
fof(f452,plain,
( e3 != op(e3,unit)
| ~ sP13 ),
inference(definition_unfolding,[],[f237,f354])).
fof(f457,plain,
( op(e2,e2) != unit
| ~ sP11 ),
inference(definition_unfolding,[],[f242,f354])).
fof(f460,plain,
( e2 != op(e2,unit)
| ~ sP9 ),
inference(definition_unfolding,[],[f252,f354])).
fof(f465,plain,
( op(e1,e1) != unit
| ~ sP6 ),
inference(definition_unfolding,[],[f262,f354])).
fof(f468,plain,
( e1 != op(e1,unit)
| ~ sP5 ),
inference(definition_unfolding,[],[f267,f354])).
fof(f470,plain,
( e3 != op(unit,e3)
| ~ sP4 ),
inference(definition_unfolding,[],[f273,f354])).
fof(f475,plain,
( e2 != op(unit,e2)
| ~ sP3 ),
inference(definition_unfolding,[],[f276,f354])).
fof(f480,plain,
( e1 != op(unit,e1)
| ~ sP2 ),
inference(definition_unfolding,[],[f279,f354])).
fof(f485,plain,
( op(unit,unit) != unit
| ~ sP1 ),
inference(definition_unfolding,[],[f282,f354,f354,f354])).
fof(f489,plain,
( op(e3,e3) != unit
| op(e2,e2) != unit
| op(e1,e1) != unit
| op(unit,unit) != unit
| ~ sP0 ),
inference(definition_unfolding,[],[f286,f354,f354,f354,f354,f354,f354])).
fof(f552,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP29
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| e3 != op(e3,unit)
| e3 != op(unit,e3)
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(definition_unfolding,[],[f291,f354,f354,f354,f354,f354,f354])).
fof(f557,plain,(
op(e3,e3) = unit ),
inference(definition_unfolding,[],[f376,f354])).
fof(f558,plain,(
e3 = op(e3,unit) ),
inference(definition_unfolding,[],[f373,f354])).
fof(f559,plain,(
op(e2,e2) = unit ),
inference(definition_unfolding,[],[f371,f354])).
fof(f560,plain,(
e2 = op(e2,unit) ),
inference(definition_unfolding,[],[f369,f354])).
fof(f561,plain,(
op(e1,e1) = unit ),
inference(definition_unfolding,[],[f366,f354])).
fof(f562,plain,(
e1 = op(e1,unit) ),
inference(definition_unfolding,[],[f365,f354])).
fof(f563,plain,(
e3 = op(unit,e3) ),
inference(definition_unfolding,[],[f364,f354])).
fof(f564,plain,(
e2 = op(unit,e2) ),
inference(definition_unfolding,[],[f363,f354])).
fof(f565,plain,(
e1 = op(unit,e1) ),
inference(definition_unfolding,[],[f362,f354])).
fof(f566,plain,(
op(unit,unit) = unit ),
inference(definition_unfolding,[],[f361,f354,f354,f354])).
fof(f568,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP29
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(duplicate_literal_removal,[],[f552])).
fof(f631,plain,(
~ sP17 ),
inference(trivial_inequality_removal,[],[f448])).
fof(f1912,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP29
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(subsumption_resolution,[],[f568,f631])).
fof(f1913,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP29
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP0 ),
inference(subsumption_resolution,[],[f1912,f485])).
fof(f1914,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP29
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| sP19
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP0 ),
inference(subsumption_resolution,[],[f1913,f447])).
fof(f1915,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP29
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP0 ),
inference(subsumption_resolution,[],[f1914,f443])).
fof(f1916,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP0 ),
inference(subsumption_resolution,[],[f1915,f406])).
fof(f1917,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP0 ),
inference(subsumption_resolution,[],[f1916,f438])).
fof(f1918,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP0 ),
inference(subsumption_resolution,[],[f1917,f480])).
fof(f1919,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP0 ),
inference(subsumption_resolution,[],[f1918,f407])).
fof(f1920,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP0 ),
inference(subsumption_resolution,[],[f1919,f434])).
fof(f1921,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP4
| sP3
| sP0 ),
inference(subsumption_resolution,[],[f1920,f468])).
fof(f1922,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP4
| sP3
| sP0 ),
inference(subsumption_resolution,[],[f1921,f390])).
fof(f1923,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP27
| sP26
| sP25
| sP24
| sP23
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP4
| sP3
| sP0 ),
inference(subsumption_resolution,[],[f1922,f429])).
fof(f1924,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP27
| sP26
| sP25
| sP24
| sP23
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP4
| sP0 ),
inference(subsumption_resolution,[],[f1923,f475])).
fof(f1925,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP27
| sP26
| sP25
| sP24
| sP23
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP4
| sP0 ),
inference(subsumption_resolution,[],[f1924,f391])).
fof(f1926,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP27
| sP26
| sP25
| sP24
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP4
| sP0 ),
inference(subsumption_resolution,[],[f1925,f425])).
fof(f1927,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP27
| sP26
| sP25
| sP24
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP8
| sP7
| sP6
| sP4
| sP0 ),
inference(subsumption_resolution,[],[f1926,f460])).
fof(f1928,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP27
| sP26
| sP25
| sP24
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP8
| sP7
| sP6
| sP4
| sP0 ),
inference(subsumption_resolution,[],[f1927,f169])).
fof(f1929,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP27
| sP26
| sP25
| sP24
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP7
| sP6
| sP4
| sP0 ),
inference(subsumption_resolution,[],[f1928,f256])).
fof(f1930,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP27
| sP26
| sP24
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP7
| sP6
| sP4
| sP0 ),
inference(subsumption_resolution,[],[f1929,f416])).
fof(f1931,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP27
| sP26
| sP24
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP12
| sP11
| sP10
| sP7
| sP6
| sP4
| sP0 ),
inference(subsumption_resolution,[],[f1930,f452])).
fof(f1932,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP27
| sP26
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP12
| sP11
| sP10
| sP7
| sP6
| sP4
| sP0 ),
inference(subsumption_resolution,[],[f1931,f420])).
fof(f1933,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP27
| sP26
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f1932,f470])).
fof(f1963,plain,
( unit != unit
| ~ sP43 ),
inference(backward_demodulation,[],[f557,f380])).
fof(f1964,plain,
( unit != unit
| ~ sP42 ),
inference(backward_demodulation,[],[f557,f384])).
fof(f1965,plain,
( unit != unit
| ~ sP16 ),
inference(backward_demodulation,[],[f557,f449])).
fof(f1969,plain,
( unit != unit
| op(e2,e2) != unit
| op(e1,e1) != unit
| op(unit,unit) != unit
| ~ sP0 ),
inference(backward_demodulation,[],[f557,f489])).
fof(f1981,plain,
( op(e2,e2) != unit
| op(e1,e1) != unit
| op(unit,unit) != unit
| ~ sP0 ),
inference(trivial_inequality_removal,[],[f1969])).
fof(f1982,plain,(
~ sP16 ),
inference(trivial_inequality_removal,[],[f1965])).
fof(f1983,plain,(
~ sP42 ),
inference(trivial_inequality_removal,[],[f1964])).
fof(f1984,plain,(
~ sP43 ),
inference(trivial_inequality_removal,[],[f1963])).
fof(f1986,plain,
( e1 != e1
| ~ sP44 ),
inference(backward_demodulation,[],[f375,f112])).
fof(f1989,plain,
( e1 != e1
| ~ sP37 ),
inference(backward_demodulation,[],[f375,f141])).
fof(f1990,plain,
( e1 != e1
| ~ sP15 ),
inference(backward_demodulation,[],[f375,f227])).
fof(f2000,plain,(
~ sP15 ),
inference(trivial_inequality_removal,[],[f1990])).
fof(f2001,plain,(
~ sP37 ),
inference(trivial_inequality_removal,[],[f1989])).
fof(f2002,plain,(
~ sP44 ),
inference(trivial_inequality_removal,[],[f1986])).
fof(f2003,plain,
( e2 != e2
| ~ sP46 ),
inference(backward_demodulation,[],[f374,f103])).
fof(f2006,plain,
( e2 != e2
| ~ sP31 ),
inference(backward_demodulation,[],[f374,f165])).
fof(f2009,plain,
( e2 != e2
| ~ sP14 ),
inference(backward_demodulation,[],[f374,f232])).
fof(f2018,plain,(
~ sP14 ),
inference(trivial_inequality_removal,[],[f2009])).
fof(f2019,plain,(
~ sP31 ),
inference(trivial_inequality_removal,[],[f2006])).
fof(f2020,plain,(
~ sP46 ),
inference(trivial_inequality_removal,[],[f2003])).
fof(f2035,plain,
( e3 != e3
| e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP27
| sP26
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(backward_demodulation,[],[f558,f1933])).
fof(f2036,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP27
| sP26
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(trivial_inequality_removal,[],[f2035])).
fof(f2069,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP27
| sP26
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2036,f2020])).
fof(f2070,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP45
| sP43
| sP42
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP27
| sP26
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2069,f2002])).
fof(f2071,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP45
| sP42
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP27
| sP26
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2070,f1984])).
fof(f2072,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP45
| sP41
| sP40
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP27
| sP26
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2071,f1983])).
fof(f2073,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP45
| sP41
| sP40
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP27
| sP26
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2072,f2001])).
fof(f2074,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP45
| sP41
| sP40
| sP36
| sP35
| sP34
| sP33
| sP32
| sP27
| sP26
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP16
| sP15
| sP14
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2073,f2019])).
fof(f2075,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP45
| sP41
| sP40
| sP36
| sP35
| sP34
| sP33
| sP32
| sP27
| sP26
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP15
| sP14
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2074,f1982])).
fof(f2076,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP45
| sP41
| sP40
| sP36
| sP35
| sP34
| sP33
| sP32
| sP27
| sP26
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP14
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2075,f2000])).
fof(f2077,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP45
| sP41
| sP40
| sP36
| sP35
| sP34
| sP33
| sP32
| sP27
| sP26
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2076,f2018])).
fof(f2078,plain,
( e1 != e1
| ~ sP45 ),
inference(backward_demodulation,[],[f372,f108])).
fof(f2081,plain,
( e1 != e1
| ~ sP36 ),
inference(backward_demodulation,[],[f372,f145])).
fof(f2082,plain,
( e1 != e1
| ~ sP12 ),
inference(backward_demodulation,[],[f372,f239])).
fof(f2091,plain,(
~ sP12 ),
inference(trivial_inequality_removal,[],[f2082])).
fof(f2092,plain,(
~ sP36 ),
inference(trivial_inequality_removal,[],[f2081])).
fof(f2093,plain,(
~ sP45 ),
inference(trivial_inequality_removal,[],[f2078])).
fof(f2103,plain,
( unit != unit
| ~ sP35 ),
inference(backward_demodulation,[],[f559,f395])).
fof(f2104,plain,
( unit != unit
| ~ sP34 ),
inference(backward_demodulation,[],[f559,f399])).
fof(f2105,plain,
( unit != unit
| ~ sP11 ),
inference(backward_demodulation,[],[f559,f457])).
fof(f2114,plain,
( unit != unit
| op(e1,e1) != unit
| op(unit,unit) != unit
| ~ sP0 ),
inference(backward_demodulation,[],[f559,f1981])).
fof(f2115,plain,
( op(e1,e1) != unit
| op(unit,unit) != unit
| ~ sP0 ),
inference(trivial_inequality_removal,[],[f2114])).
fof(f2116,plain,(
~ sP11 ),
inference(trivial_inequality_removal,[],[f2105])).
fof(f2117,plain,(
~ sP34 ),
inference(trivial_inequality_removal,[],[f2104])).
fof(f2118,plain,(
~ sP35 ),
inference(trivial_inequality_removal,[],[f2103])).
fof(f2119,plain,
( e3 != e3
| ~ sP40 ),
inference(backward_demodulation,[],[f370,f127])).
fof(f2122,plain,
( e3 != e3
| ~ sP33 ),
inference(backward_demodulation,[],[f370,f156])).
fof(f2127,plain,
( e3 != e3
| ~ sP10 ),
inference(backward_demodulation,[],[f370,f249])).
fof(f2135,plain,(
~ sP10 ),
inference(trivial_inequality_removal,[],[f2127])).
fof(f2136,plain,(
~ sP33 ),
inference(trivial_inequality_removal,[],[f2122])).
fof(f2137,plain,(
~ sP40 ),
inference(trivial_inequality_removal,[],[f2119])).
fof(f2152,plain,
( e2 != e2
| e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP45
| sP41
| sP40
| sP36
| sP35
| sP34
| sP33
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(backward_demodulation,[],[f560,f2077])).
fof(f2153,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP45
| sP41
| sP40
| sP36
| sP35
| sP34
| sP33
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(trivial_inequality_removal,[],[f2152])).
fof(f2159,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP41
| sP40
| sP36
| sP35
| sP34
| sP33
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2153,f2093])).
fof(f2160,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP41
| sP36
| sP35
| sP34
| sP33
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2159,f2137])).
fof(f2161,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP41
| sP35
| sP34
| sP33
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2160,f2092])).
fof(f2162,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP41
| sP34
| sP33
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2161,f2118])).
fof(f2163,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP41
| sP33
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2162,f2117])).
fof(f2164,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP41
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP12
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2163,f2136])).
fof(f2165,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP41
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP11
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2164,f2091])).
fof(f2166,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP41
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP10
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2165,f2116])).
fof(f2167,plain,
( e3 != op(unit,e3)
| e2 != op(e1,e3)
| sP41
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2166,f2135])).
fof(f2178,plain,
( e2 != e2
| e3 != op(unit,e3)
| sP41
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP7
| sP6
| sP0 ),
inference(backward_demodulation,[],[f368,f2167])).
fof(f2179,plain,
( e3 != op(unit,e3)
| sP41
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP7
| sP6
| sP0 ),
inference(trivial_inequality_removal,[],[f2178])).
fof(f2182,plain,
( e3 != e3
| ~ sP41 ),
inference(backward_demodulation,[],[f367,f123])).
fof(f2185,plain,
( e3 != e3
| ~ sP32 ),
inference(backward_demodulation,[],[f367,f160])).
fof(f2190,plain,
( e3 != e3
| ~ sP7 ),
inference(backward_demodulation,[],[f367,f261])).
fof(f2194,plain,(
~ sP7 ),
inference(trivial_inequality_removal,[],[f2190])).
fof(f2195,plain,(
~ sP32 ),
inference(trivial_inequality_removal,[],[f2185])).
fof(f2196,plain,(
~ sP41 ),
inference(trivial_inequality_removal,[],[f2182])).
fof(f2206,plain,
( unit != unit
| ~ sP27 ),
inference(backward_demodulation,[],[f561,f410])).
fof(f2207,plain,
( unit != unit
| ~ sP26 ),
inference(backward_demodulation,[],[f561,f414])).
fof(f2208,plain,
( unit != unit
| ~ sP6 ),
inference(backward_demodulation,[],[f561,f465])).
fof(f2209,plain,
( unit != unit
| op(unit,unit) != unit
| ~ sP0 ),
inference(backward_demodulation,[],[f561,f2115])).
fof(f2210,plain,
( op(unit,unit) != unit
| ~ sP0 ),
inference(trivial_inequality_removal,[],[f2209])).
fof(f2211,plain,(
~ sP6 ),
inference(trivial_inequality_removal,[],[f2208])).
fof(f2212,plain,(
~ sP26 ),
inference(trivial_inequality_removal,[],[f2207])).
fof(f2213,plain,(
~ sP27 ),
inference(trivial_inequality_removal,[],[f2206])).
fof(f2226,plain,
( e1 != e1
| e3 != op(unit,e3)
| sP41
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP7
| sP6
| sP0 ),
inference(backward_demodulation,[],[f562,f2179])).
fof(f2227,plain,
( e3 != op(unit,e3)
| sP41
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP7
| sP6
| sP0 ),
inference(trivial_inequality_removal,[],[f2226])).
fof(f2231,plain,
( e3 != op(unit,e3)
| sP32
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2227,f2196])).
fof(f2232,plain,
( e3 != op(unit,e3)
| sP27
| sP26
| e2 != op(unit,e2)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2231,f2195])).
fof(f2233,plain,
( e3 != op(unit,e3)
| sP26
| e2 != op(unit,e2)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2232,f2213])).
fof(f2234,plain,
( e3 != op(unit,e3)
| e2 != op(unit,e2)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP7
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2233,f2212])).
fof(f2235,plain,
( e3 != op(unit,e3)
| e2 != op(unit,e2)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP6
| sP0 ),
inference(subsumption_resolution,[],[f2234,f2194])).
fof(f2236,plain,
( e3 != op(unit,e3)
| e2 != op(unit,e2)
| e1 != op(unit,e1)
| op(unit,unit) != unit
| sP0 ),
inference(subsumption_resolution,[],[f2235,f2211])).
fof(f2237,plain,
( e3 != op(unit,e3)
| e2 != op(unit,e2)
| e1 != op(unit,e1)
| op(unit,unit) != unit ),
inference(subsumption_resolution,[],[f2236,f2210])).
fof(f2248,plain,
( e3 != e3
| e2 != op(unit,e2)
| e1 != op(unit,e1)
| op(unit,unit) != unit ),
inference(backward_demodulation,[],[f563,f2237])).
fof(f2249,plain,
( e2 != op(unit,e2)
| e1 != op(unit,e1)
| op(unit,unit) != unit ),
inference(trivial_inequality_removal,[],[f2248])).
fof(f2264,plain,
( e2 != e2
| e1 != op(unit,e1)
| op(unit,unit) != unit ),
inference(backward_demodulation,[],[f564,f2249])).
fof(f2265,plain,
( e1 != op(unit,e1)
| op(unit,unit) != unit ),
inference(trivial_inequality_removal,[],[f2264])).
fof(f2281,plain,
( e1 != e1
| op(unit,unit) != unit ),
inference(backward_demodulation,[],[f565,f2265])).
fof(f2282,plain,(
op(unit,unit) != unit ),
inference(trivial_inequality_removal,[],[f2281])).
fof(f2286,plain,(
$false ),
inference(subsumption_resolution,[],[f566,f2282])).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG043+1 : TPTP v7.1.0. Released v2.7.0.
% 0.00/0.04 % Command : vampire --mode casc -t %d %s
% 0.03/0.24 % Computer : n157.star.cs.uiowa.edu
% 0.03/0.24 % Model : x86_64 x86_64
% 0.03/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.24 % Memory : 32218.625MB
% 0.03/0.24 % OS : Linux 3.10.0-693.2.2.el7.x86_64
% 0.03/0.24 % CPULimit : 300
% 0.03/0.24 % DateTime : Wed Aug 29 18:25:56 CDT 2018
% 0.03/0.24 % CPUTime :
% 0.08/0.28 % ott+1002_2_av=off:bd=preordered:irw=on:lma=on:nm=64:nwc=10:sp=reverse_arity:updr=off_2 on theBenchmark
% 0.08/0.45 % Refutation found. Thanks to Tanya!
% 0.08/0.45 % SZS status Theorem for theBenchmark
% 0.08/0.45 % SZS output start Proof for theBenchmark
% 0.08/0.45 fof(f2,axiom,(
% 0.08/0.45 e0 = op(e3,e3) & e1 = op(e3,e2) & e2 = op(e3,e1) & e3 = op(e3,e0) & e1 = op(e2,e3) & e0 = op(e2,e2) & e3 = op(e2,e1) & e2 = op(e2,e0) & e2 = op(e1,e3) & e3 = op(e1,e2) & e0 = op(e1,e1) & e1 = op(e1,e0) & e3 = op(e0,e3) & e2 = op(e0,e2) & e1 = op(e0,e1) & e0 = op(e0,e0)),
% 0.08/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2)).
% 0.08/0.45 fof(f3,axiom,(
% 0.08/0.45 e0 = unit),
% 0.08/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3)).
% 0.08/0.45 fof(f4,conjecture,(
% 0.08/0.45 (e3 = op(e3,e3) | e3 = op(e2,e3) | e3 = op(e1,e3) | e3 = op(e0,e3)) & (e3 = op(e3,e3) | e3 = op(e3,e2) | e3 = op(e3,e1) | e3 = op(e3,e0)) & (e2 = op(e3,e3) | e2 = op(e2,e3) | e2 = op(e1,e3) | e2 = op(e0,e3)) & (e2 = op(e3,e3) | e2 = op(e3,e2) | e2 = op(e3,e1) | e2 = op(e3,e0)) & (e1 = op(e3,e3) | e1 = op(e2,e3) | e1 = op(e1,e3) | e1 = op(e0,e3)) & (e1 = op(e3,e3) | e1 = op(e3,e2) | e1 = op(e3,e1) | e1 = op(e3,e0)) & (e0 = op(e3,e3) | e0 = op(e2,e3) | e0 = op(e1,e3) | e0 = op(e0,e3)) & (e0 = op(e3,e3) | e0 = op(e3,e2) | e0 = op(e3,e1) | e0 = op(e3,e0)) & (e3 = op(e3,e2) | e3 = op(e2,e2) | e3 = op(e1,e2) | e3 = op(e0,e2)) & (e3 = op(e2,e3) | e3 = op(e2,e2) | e3 = op(e2,e1) | e3 = op(e2,e0)) & (e2 = op(e3,e2) | e2 = op(e2,e2) | e2 = op(e1,e2) | e2 = op(e0,e2)) & (e2 = op(e2,e3) | e2 = op(e2,e2) | e2 = op(e2,e1) | e2 = op(e2,e0)) & (e1 = op(e3,e2) | e1 = op(e2,e2) | e1 = op(e1,e2) | e1 = op(e0,e2)) & (e1 = op(e2,e3) | e1 = op(e2,e2) | e1 = op(e2,e1) | e1 = op(e2,e0)) & (e0 = op(e3,e2) | e0 = op(e2,e2) | e0 = op(e1,e2) | e0 = op(e0,e2)) & (e0 = op(e2,e3) | e0 = op(e2,e2) | e0 = op(e2,e1) | e0 = op(e2,e0)) & (e3 = op(e3,e1) | e3 = op(e2,e1) | e3 = op(e1,e1) | e3 = op(e0,e1)) & (e3 = op(e1,e3) | e3 = op(e1,e2) | e3 = op(e1,e1) | e3 = op(e1,e0)) & (e2 = op(e3,e1) | e2 = op(e2,e1) | e2 = op(e1,e1) | e2 = op(e0,e1)) & (e2 = op(e1,e3) | e2 = op(e1,e2) | e2 = op(e1,e1) | e2 = op(e1,e0)) & (e1 = op(e3,e1) | e1 = op(e2,e1) | e1 = op(e1,e1) | e1 = op(e0,e1)) & (e1 = op(e1,e3) | e1 = op(e1,e2) | e1 = op(e1,e1) | e1 = op(e1,e0)) & (e0 = op(e3,e1) | e0 = op(e2,e1) | e0 = op(e1,e1) | e0 = op(e0,e1)) & (e0 = op(e1,e3) | e0 = op(e1,e2) | e0 = op(e1,e1) | e0 = op(e1,e0)) & (e3 = op(e3,e0) | e3 = op(e2,e0) | e3 = op(e1,e0) | e3 = op(e0,e0)) & (e3 = op(e0,e3) | e3 = op(e0,e2) | e3 = op(e0,e1) | e3 = op(e0,e0)) & (e2 = op(e3,e0) | e2 = op(e2,e0) | e2 = op(e1,e0) | e2 = op(e0,e0)) & (e2 = op(e0,e3) | e2 = op(e0,e2) | e2 = op(e0,e1) | e2 = op(e0,e0)) & (e1 = op(e3,e0) | e1 = op(e2,e0) | e1 = op(e1,e0) | e1 = op(e0,e0)) & (e1 = op(e0,e3) | e1 = op(e0,e2) | e1 = op(e0,e1) | e1 = op(e0,e0)) & (e0 = op(e3,e0) | e0 = op(e2,e0) | e0 = op(e1,e0) | e0 = op(e0,e0)) & (e0 = op(e0,e3) | e0 = op(e0,e2) | e0 = op(e0,e1) | e0 = op(e0,e0)) & (e3 = unit | e2 = unit | e1 = unit | e0 = unit) & e3 = op(e3,unit) & e3 = op(unit,e3) & e2 = op(e2,unit) & e2 = op(unit,e2) & e1 = op(e1,unit) & e1 = op(unit,e1) & e0 = op(e0,unit) & e0 = op(unit,e0) & (e3 = op(e3,e3) | e2 = op(e3,e3) | e1 = op(e3,e3) | e0 = op(e3,e3)) & (e3 = op(e3,e2) | e2 = op(e3,e2) | e1 = op(e3,e2) | e0 = op(e3,e2)) & (e3 = op(e3,e1) | e2 = op(e3,e1) | e1 = op(e3,e1) | e0 = op(e3,e1)) & (e3 = op(e3,e0) | e2 = op(e3,e0) | e1 = op(e3,e0) | e0 = op(e3,e0)) & (e3 = op(e2,e3) | e2 = op(e2,e3) | e1 = op(e2,e3) | e0 = op(e2,e3)) & (e3 = op(e2,e2) | e2 = op(e2,e2) | e1 = op(e2,e2) | e0 = op(e2,e2)) & (e3 = op(e2,e1) | e2 = op(e2,e1) | e1 = op(e2,e1) | e0 = op(e2,e1)) & (e3 = op(e2,e0) | e2 = op(e2,e0) | e1 = op(e2,e0) | e0 = op(e2,e0)) & (e3 = op(e1,e3) | e2 = op(e1,e3) | e1 = op(e1,e3) | e0 = op(e1,e3)) & (e3 = op(e1,e2) | e2 = op(e1,e2) | e1 = op(e1,e2) | e0 = op(e1,e2)) & (e3 = op(e1,e1) | e2 = op(e1,e1) | e1 = op(e1,e1) | e0 = op(e1,e1)) & (e3 = op(e1,e0) | e2 = op(e1,e0) | e1 = op(e1,e0) | e0 = op(e1,e0)) & (e3 = op(e0,e3) | e2 = op(e0,e3) | e1 = op(e0,e3) | e0 = op(e0,e3)) & (e3 = op(e0,e2) | e2 = op(e0,e2) | e1 = op(e0,e2) | e0 = op(e0,e2)) & (e3 = op(e0,e1) | e2 = op(e0,e1) | e1 = op(e0,e1) | e0 = op(e0,e1)) & (e3 = op(e0,e0) | e2 = op(e0,e0) | e1 = op(e0,e0) | e0 = op(e0,e0)) & ((e3 = op(e3,e3) & e3 = op(e2,e2) & e3 = op(e1,e1) & e3 = op(e0,e0)) | (e2 = op(e3,e3) & e2 = op(e2,e2) & e2 = op(e1,e1) & e2 = op(e0,e0)) | (e1 = op(e3,e3) & e1 = op(e2,e2) & e1 = op(e1,e1) & e1 = op(e0,e0)) | (e0 = op(e3,e3) & e0 = op(e2,e2) & e0 = op(e1,e1) & e0 = op(e0,e0)))),
% 0.08/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1)).
% 0.08/0.45 fof(f5,negated_conjecture,(
% 0.08/0.45 ~((e3 = op(e3,e3) | e3 = op(e2,e3) | e3 = op(e1,e3) | e3 = op(e0,e3)) & (e3 = op(e3,e3) | e3 = op(e3,e2) | e3 = op(e3,e1) | e3 = op(e3,e0)) & (e2 = op(e3,e3) | e2 = op(e2,e3) | e2 = op(e1,e3) | e2 = op(e0,e3)) & (e2 = op(e3,e3) | e2 = op(e3,e2) | e2 = op(e3,e1) | e2 = op(e3,e0)) & (e1 = op(e3,e3) | e1 = op(e2,e3) | e1 = op(e1,e3) | e1 = op(e0,e3)) & (e1 = op(e3,e3) | e1 = op(e3,e2) | e1 = op(e3,e1) | e1 = op(e3,e0)) & (e0 = op(e3,e3) | e0 = op(e2,e3) | e0 = op(e1,e3) | e0 = op(e0,e3)) & (e0 = op(e3,e3) | e0 = op(e3,e2) | e0 = op(e3,e1) | e0 = op(e3,e0)) & (e3 = op(e3,e2) | e3 = op(e2,e2) | e3 = op(e1,e2) | e3 = op(e0,e2)) & (e3 = op(e2,e3) | e3 = op(e2,e2) | e3 = op(e2,e1) | e3 = op(e2,e0)) & (e2 = op(e3,e2) | e2 = op(e2,e2) | e2 = op(e1,e2) | e2 = op(e0,e2)) & (e2 = op(e2,e3) | e2 = op(e2,e2) | e2 = op(e2,e1) | e2 = op(e2,e0)) & (e1 = op(e3,e2) | e1 = op(e2,e2) | e1 = op(e1,e2) | e1 = op(e0,e2)) & (e1 = op(e2,e3) | e1 = op(e2,e2) | e1 = op(e2,e1) | e1 = op(e2,e0)) & (e0 = op(e3,e2) | e0 = op(e2,e2) | e0 = op(e1,e2) | e0 = op(e0,e2)) & (e0 = op(e2,e3) | e0 = op(e2,e2) | e0 = op(e2,e1) | e0 = op(e2,e0)) & (e3 = op(e3,e1) | e3 = op(e2,e1) | e3 = op(e1,e1) | e3 = op(e0,e1)) & (e3 = op(e1,e3) | e3 = op(e1,e2) | e3 = op(e1,e1) | e3 = op(e1,e0)) & (e2 = op(e3,e1) | e2 = op(e2,e1) | e2 = op(e1,e1) | e2 = op(e0,e1)) & (e2 = op(e1,e3) | e2 = op(e1,e2) | e2 = op(e1,e1) | e2 = op(e1,e0)) & (e1 = op(e3,e1) | e1 = op(e2,e1) | e1 = op(e1,e1) | e1 = op(e0,e1)) & (e1 = op(e1,e3) | e1 = op(e1,e2) | e1 = op(e1,e1) | e1 = op(e1,e0)) & (e0 = op(e3,e1) | e0 = op(e2,e1) | e0 = op(e1,e1) | e0 = op(e0,e1)) & (e0 = op(e1,e3) | e0 = op(e1,e2) | e0 = op(e1,e1) | e0 = op(e1,e0)) & (e3 = op(e3,e0) | e3 = op(e2,e0) | e3 = op(e1,e0) | e3 = op(e0,e0)) & (e3 = op(e0,e3) | e3 = op(e0,e2) | e3 = op(e0,e1) | e3 = op(e0,e0)) & (e2 = op(e3,e0) | e2 = op(e2,e0) | e2 = op(e1,e0) | e2 = op(e0,e0)) & (e2 = op(e0,e3) | e2 = op(e0,e2) | e2 = op(e0,e1) | e2 = op(e0,e0)) & (e1 = op(e3,e0) | e1 = op(e2,e0) | e1 = op(e1,e0) | e1 = op(e0,e0)) & (e1 = op(e0,e3) | e1 = op(e0,e2) | e1 = op(e0,e1) | e1 = op(e0,e0)) & (e0 = op(e3,e0) | e0 = op(e2,e0) | e0 = op(e1,e0) | e0 = op(e0,e0)) & (e0 = op(e0,e3) | e0 = op(e0,e2) | e0 = op(e0,e1) | e0 = op(e0,e0)) & (e3 = unit | e2 = unit | e1 = unit | e0 = unit) & e3 = op(e3,unit) & e3 = op(unit,e3) & e2 = op(e2,unit) & e2 = op(unit,e2) & e1 = op(e1,unit) & e1 = op(unit,e1) & e0 = op(e0,unit) & e0 = op(unit,e0) & (e3 = op(e3,e3) | e2 = op(e3,e3) | e1 = op(e3,e3) | e0 = op(e3,e3)) & (e3 = op(e3,e2) | e2 = op(e3,e2) | e1 = op(e3,e2) | e0 = op(e3,e2)) & (e3 = op(e3,e1) | e2 = op(e3,e1) | e1 = op(e3,e1) | e0 = op(e3,e1)) & (e3 = op(e3,e0) | e2 = op(e3,e0) | e1 = op(e3,e0) | e0 = op(e3,e0)) & (e3 = op(e2,e3) | e2 = op(e2,e3) | e1 = op(e2,e3) | e0 = op(e2,e3)) & (e3 = op(e2,e2) | e2 = op(e2,e2) | e1 = op(e2,e2) | e0 = op(e2,e2)) & (e3 = op(e2,e1) | e2 = op(e2,e1) | e1 = op(e2,e1) | e0 = op(e2,e1)) & (e3 = op(e2,e0) | e2 = op(e2,e0) | e1 = op(e2,e0) | e0 = op(e2,e0)) & (e3 = op(e1,e3) | e2 = op(e1,e3) | e1 = op(e1,e3) | e0 = op(e1,e3)) & (e3 = op(e1,e2) | e2 = op(e1,e2) | e1 = op(e1,e2) | e0 = op(e1,e2)) & (e3 = op(e1,e1) | e2 = op(e1,e1) | e1 = op(e1,e1) | e0 = op(e1,e1)) & (e3 = op(e1,e0) | e2 = op(e1,e0) | e1 = op(e1,e0) | e0 = op(e1,e0)) & (e3 = op(e0,e3) | e2 = op(e0,e3) | e1 = op(e0,e3) | e0 = op(e0,e3)) & (e3 = op(e0,e2) | e2 = op(e0,e2) | e1 = op(e0,e2) | e0 = op(e0,e2)) & (e3 = op(e0,e1) | e2 = op(e0,e1) | e1 = op(e0,e1) | e0 = op(e0,e1)) & (e3 = op(e0,e0) | e2 = op(e0,e0) | e1 = op(e0,e0) | e0 = op(e0,e0)) & ((e3 = op(e3,e3) & e3 = op(e2,e2) & e3 = op(e1,e1) & e3 = op(e0,e0)) | (e2 = op(e3,e3) & e2 = op(e2,e2) & e2 = op(e1,e1) & e2 = op(e0,e0)) | (e1 = op(e3,e3) & e1 = op(e2,e2) & e1 = op(e1,e1) & e1 = op(e0,e0)) | (e0 = op(e3,e3) & e0 = op(e2,e2) & e0 = op(e1,e1) & e0 = op(e0,e0))))),
% 0.08/0.45 inference(negated_conjecture,[],[f4])).
% 0.08/0.45 fof(f6,plain,(
% 0.08/0.45 (e3 != op(e3,e3) & e3 != op(e2,e3) & e3 != op(e1,e3) & e3 != op(e0,e3)) | (e3 != op(e3,e3) & e3 != op(e3,e2) & e3 != op(e3,e1) & e3 != op(e3,e0)) | (e2 != op(e3,e3) & e2 != op(e2,e3) & e2 != op(e1,e3) & e2 != op(e0,e3)) | (e2 != op(e3,e3) & e2 != op(e3,e2) & e2 != op(e3,e1) & e2 != op(e3,e0)) | (e1 != op(e3,e3) & e1 != op(e2,e3) & e1 != op(e1,e3) & e1 != op(e0,e3)) | (e1 != op(e3,e3) & e1 != op(e3,e2) & e1 != op(e3,e1) & e1 != op(e3,e0)) | (e0 != op(e3,e3) & e0 != op(e2,e3) & e0 != op(e1,e3) & e0 != op(e0,e3)) | (e0 != op(e3,e3) & e0 != op(e3,e2) & e0 != op(e3,e1) & e0 != op(e3,e0)) | (e3 != op(e3,e2) & e3 != op(e2,e2) & e3 != op(e1,e2) & e3 != op(e0,e2)) | (e3 != op(e2,e3) & e3 != op(e2,e2) & e3 != op(e2,e1) & e3 != op(e2,e0)) | (e2 != op(e3,e2) & e2 != op(e2,e2) & e2 != op(e1,e2) & e2 != op(e0,e2)) | (e2 != op(e2,e3) & e2 != op(e2,e2) & e2 != op(e2,e1) & e2 != op(e2,e0)) | (e1 != op(e3,e2) & e1 != op(e2,e2) & e1 != op(e1,e2) & e1 != op(e0,e2)) | (e1 != op(e2,e3) & e1 != op(e2,e2) & e1 != op(e2,e1) & e1 != op(e2,e0)) | (e0 != op(e3,e2) & e0 != op(e2,e2) & e0 != op(e1,e2) & e0 != op(e0,e2)) | (e0 != op(e2,e3) & e0 != op(e2,e2) & e0 != op(e2,e1) & e0 != op(e2,e0)) | (e3 != op(e3,e1) & e3 != op(e2,e1) & e3 != op(e1,e1) & e3 != op(e0,e1)) | (e3 != op(e1,e3) & e3 != op(e1,e2) & e3 != op(e1,e1) & e3 != op(e1,e0)) | (e2 != op(e3,e1) & e2 != op(e2,e1) & e2 != op(e1,e1) & e2 != op(e0,e1)) | (e2 != op(e1,e3) & e2 != op(e1,e2) & e2 != op(e1,e1) & e2 != op(e1,e0)) | (e1 != op(e3,e1) & e1 != op(e2,e1) & e1 != op(e1,e1) & e1 != op(e0,e1)) | (e1 != op(e1,e3) & e1 != op(e1,e2) & e1 != op(e1,e1) & e1 != op(e1,e0)) | (e0 != op(e3,e1) & e0 != op(e2,e1) & e0 != op(e1,e1) & e0 != op(e0,e1)) | (e0 != op(e1,e3) & e0 != op(e1,e2) & e0 != op(e1,e1) & e0 != op(e1,e0)) | (e3 != op(e3,e0) & e3 != op(e2,e0) & e3 != op(e1,e0) & e3 != op(e0,e0)) | (e3 != op(e0,e3) & e3 != op(e0,e2) & e3 != op(e0,e1) & e3 != op(e0,e0)) | (e2 != op(e3,e0) & e2 != op(e2,e0) & e2 != op(e1,e0) & e2 != op(e0,e0)) | (e2 != op(e0,e3) & e2 != op(e0,e2) & e2 != op(e0,e1) & e2 != op(e0,e0)) | (e1 != op(e3,e0) & e1 != op(e2,e0) & e1 != op(e1,e0) & e1 != op(e0,e0)) | (e1 != op(e0,e3) & e1 != op(e0,e2) & e1 != op(e0,e1) & e1 != op(e0,e0)) | (e0 != op(e3,e0) & e0 != op(e2,e0) & e0 != op(e1,e0) & e0 != op(e0,e0)) | (e0 != op(e0,e3) & e0 != op(e0,e2) & e0 != op(e0,e1) & e0 != op(e0,e0)) | (e3 != unit & e2 != unit & e1 != unit & e0 != unit) | e3 != op(e3,unit) | e3 != op(unit,e3) | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | e0 != op(e0,unit) | e0 != op(unit,e0) | (e3 != op(e3,e3) & e2 != op(e3,e3) & e1 != op(e3,e3) & e0 != op(e3,e3)) | (e3 != op(e3,e2) & e2 != op(e3,e2) & e1 != op(e3,e2) & e0 != op(e3,e2)) | (e3 != op(e3,e1) & e2 != op(e3,e1) & e1 != op(e3,e1) & e0 != op(e3,e1)) | (e3 != op(e3,e0) & e2 != op(e3,e0) & e1 != op(e3,e0) & e0 != op(e3,e0)) | (e3 != op(e2,e3) & e2 != op(e2,e3) & e1 != op(e2,e3) & e0 != op(e2,e3)) | (e3 != op(e2,e2) & e2 != op(e2,e2) & e1 != op(e2,e2) & e0 != op(e2,e2)) | (e3 != op(e2,e1) & e2 != op(e2,e1) & e1 != op(e2,e1) & e0 != op(e2,e1)) | (e3 != op(e2,e0) & e2 != op(e2,e0) & e1 != op(e2,e0) & e0 != op(e2,e0)) | (e3 != op(e1,e3) & e2 != op(e1,e3) & e1 != op(e1,e3) & e0 != op(e1,e3)) | (e3 != op(e1,e2) & e2 != op(e1,e2) & e1 != op(e1,e2) & e0 != op(e1,e2)) | (e3 != op(e1,e1) & e2 != op(e1,e1) & e1 != op(e1,e1) & e0 != op(e1,e1)) | (e3 != op(e1,e0) & e2 != op(e1,e0) & e1 != op(e1,e0) & e0 != op(e1,e0)) | (e3 != op(e0,e3) & e2 != op(e0,e3) & e1 != op(e0,e3) & e0 != op(e0,e3)) | (e3 != op(e0,e2) & e2 != op(e0,e2) & e1 != op(e0,e2) & e0 != op(e0,e2)) | (e3 != op(e0,e1) & e2 != op(e0,e1) & e1 != op(e0,e1) & e0 != op(e0,e1)) | (e3 != op(e0,e0) & e2 != op(e0,e0) & e1 != op(e0,e0) & e0 != op(e0,e0)) | ((e3 != op(e3,e3) | e3 != op(e2,e2) | e3 != op(e1,e1) | e3 != op(e0,e0)) & (e2 != op(e3,e3) | e2 != op(e2,e2) | e2 != op(e1,e1) | e2 != op(e0,e0)) & (e1 != op(e3,e3) | e1 != op(e2,e2) | e1 != op(e1,e1) | e1 != op(e0,e0)) & (e0 != op(e3,e3) | e0 != op(e2,e2) | e0 != op(e1,e1) | e0 != op(e0,e0)))),
% 0.08/0.45 inference(ennf_transformation,[],[f5])).
% 0.08/0.45 fof(f7,plain,(
% 0.08/0.45 ((e3 != op(e3,e3) | e3 != op(e2,e2) | e3 != op(e1,e1) | e3 != op(e0,e0)) & (e2 != op(e3,e3) | e2 != op(e2,e2) | e2 != op(e1,e1) | e2 != op(e0,e0)) & (e1 != op(e3,e3) | e1 != op(e2,e2) | e1 != op(e1,e1) | e1 != op(e0,e0)) & (e0 != op(e3,e3) | e0 != op(e2,e2) | e0 != op(e1,e1) | e0 != op(e0,e0))) | ~sP0),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP0])])).
% 0.08/0.45 fof(f8,plain,(
% 0.08/0.45 (e3 != op(e0,e0) & e2 != op(e0,e0) & e1 != op(e0,e0) & e0 != op(e0,e0)) | ~sP1),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP1])])).
% 0.08/0.45 fof(f9,plain,(
% 0.08/0.45 (e3 != op(e0,e1) & e2 != op(e0,e1) & e1 != op(e0,e1) & e0 != op(e0,e1)) | ~sP2),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP2])])).
% 0.08/0.45 fof(f10,plain,(
% 0.08/0.45 (e3 != op(e0,e2) & e2 != op(e0,e2) & e1 != op(e0,e2) & e0 != op(e0,e2)) | ~sP3),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP3])])).
% 0.08/0.45 fof(f11,plain,(
% 0.08/0.45 (e3 != op(e0,e3) & e2 != op(e0,e3) & e1 != op(e0,e3) & e0 != op(e0,e3)) | ~sP4),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP4])])).
% 0.08/0.45 fof(f12,plain,(
% 0.08/0.45 (e3 != op(e1,e0) & e2 != op(e1,e0) & e1 != op(e1,e0) & e0 != op(e1,e0)) | ~sP5),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP5])])).
% 0.08/0.45 fof(f13,plain,(
% 0.08/0.45 (e3 != op(e1,e1) & e2 != op(e1,e1) & e1 != op(e1,e1) & e0 != op(e1,e1)) | ~sP6),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP6])])).
% 0.08/0.45 fof(f14,plain,(
% 0.08/0.45 (e3 != op(e1,e2) & e2 != op(e1,e2) & e1 != op(e1,e2) & e0 != op(e1,e2)) | ~sP7),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP7])])).
% 0.08/0.45 fof(f15,plain,(
% 0.08/0.45 (e3 != op(e1,e3) & e2 != op(e1,e3) & e1 != op(e1,e3) & e0 != op(e1,e3)) | ~sP8),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP8])])).
% 0.08/0.45 fof(f16,plain,(
% 0.08/0.45 (e3 != op(e2,e0) & e2 != op(e2,e0) & e1 != op(e2,e0) & e0 != op(e2,e0)) | ~sP9),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP9])])).
% 0.08/0.45 fof(f17,plain,(
% 0.08/0.45 (e3 != op(e2,e1) & e2 != op(e2,e1) & e1 != op(e2,e1) & e0 != op(e2,e1)) | ~sP10),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP10])])).
% 0.08/0.45 fof(f18,plain,(
% 0.08/0.45 (e3 != op(e2,e2) & e2 != op(e2,e2) & e1 != op(e2,e2) & e0 != op(e2,e2)) | ~sP11),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP11])])).
% 0.08/0.45 fof(f19,plain,(
% 0.08/0.45 (e3 != op(e2,e3) & e2 != op(e2,e3) & e1 != op(e2,e3) & e0 != op(e2,e3)) | ~sP12),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP12])])).
% 0.08/0.45 fof(f20,plain,(
% 0.08/0.45 (e3 != op(e3,e0) & e2 != op(e3,e0) & e1 != op(e3,e0) & e0 != op(e3,e0)) | ~sP13),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP13])])).
% 0.08/0.45 fof(f21,plain,(
% 0.08/0.45 (e3 != op(e3,e1) & e2 != op(e3,e1) & e1 != op(e3,e1) & e0 != op(e3,e1)) | ~sP14),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP14])])).
% 0.08/0.45 fof(f22,plain,(
% 0.08/0.45 (e3 != op(e3,e2) & e2 != op(e3,e2) & e1 != op(e3,e2) & e0 != op(e3,e2)) | ~sP15),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP15])])).
% 0.08/0.45 fof(f23,plain,(
% 0.08/0.45 (e3 != op(e3,e3) & e2 != op(e3,e3) & e1 != op(e3,e3) & e0 != op(e3,e3)) | ~sP16),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP16])])).
% 0.08/0.45 fof(f24,plain,(
% 0.08/0.45 (e3 != unit & e2 != unit & e1 != unit & e0 != unit) | ~sP17),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP17])])).
% 0.08/0.45 fof(f25,plain,(
% 0.08/0.45 (e0 != op(e0,e3) & e0 != op(e0,e2) & e0 != op(e0,e1) & e0 != op(e0,e0)) | ~sP18),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP18])])).
% 0.08/0.45 fof(f26,plain,(
% 0.08/0.45 (e0 != op(e3,e0) & e0 != op(e2,e0) & e0 != op(e1,e0) & e0 != op(e0,e0)) | ~sP19),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP19])])).
% 0.08/0.45 fof(f27,plain,(
% 0.08/0.45 (e1 != op(e0,e3) & e1 != op(e0,e2) & e1 != op(e0,e1) & e1 != op(e0,e0)) | ~sP20),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP20])])).
% 0.08/0.45 fof(f28,plain,(
% 0.08/0.45 (e1 != op(e3,e0) & e1 != op(e2,e0) & e1 != op(e1,e0) & e1 != op(e0,e0)) | ~sP21),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP21])])).
% 0.08/0.45 fof(f29,plain,(
% 0.08/0.45 (e2 != op(e0,e3) & e2 != op(e0,e2) & e2 != op(e0,e1) & e2 != op(e0,e0)) | ~sP22),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP22])])).
% 0.08/0.45 fof(f30,plain,(
% 0.08/0.45 (e2 != op(e3,e0) & e2 != op(e2,e0) & e2 != op(e1,e0) & e2 != op(e0,e0)) | ~sP23),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP23])])).
% 0.08/0.45 fof(f31,plain,(
% 0.08/0.45 (e3 != op(e0,e3) & e3 != op(e0,e2) & e3 != op(e0,e1) & e3 != op(e0,e0)) | ~sP24),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP24])])).
% 0.08/0.45 fof(f32,plain,(
% 0.08/0.45 (e3 != op(e3,e0) & e3 != op(e2,e0) & e3 != op(e1,e0) & e3 != op(e0,e0)) | ~sP25),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP25])])).
% 0.08/0.45 fof(f33,plain,(
% 0.08/0.45 (e0 != op(e1,e3) & e0 != op(e1,e2) & e0 != op(e1,e1) & e0 != op(e1,e0)) | ~sP26),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP26])])).
% 0.08/0.45 fof(f34,plain,(
% 0.08/0.45 (e0 != op(e3,e1) & e0 != op(e2,e1) & e0 != op(e1,e1) & e0 != op(e0,e1)) | ~sP27),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP27])])).
% 0.08/0.45 fof(f35,plain,(
% 0.08/0.45 (e1 != op(e1,e3) & e1 != op(e1,e2) & e1 != op(e1,e1) & e1 != op(e1,e0)) | ~sP28),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP28])])).
% 0.08/0.45 fof(f36,plain,(
% 0.08/0.45 (e1 != op(e3,e1) & e1 != op(e2,e1) & e1 != op(e1,e1) & e1 != op(e0,e1)) | ~sP29),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP29])])).
% 0.08/0.45 fof(f37,plain,(
% 0.08/0.45 (e2 != op(e1,e3) & e2 != op(e1,e2) & e2 != op(e1,e1) & e2 != op(e1,e0)) | ~sP30),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP30])])).
% 0.08/0.45 fof(f38,plain,(
% 0.08/0.45 (e2 != op(e3,e1) & e2 != op(e2,e1) & e2 != op(e1,e1) & e2 != op(e0,e1)) | ~sP31),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP31])])).
% 0.08/0.45 fof(f39,plain,(
% 0.08/0.45 (e3 != op(e1,e3) & e3 != op(e1,e2) & e3 != op(e1,e1) & e3 != op(e1,e0)) | ~sP32),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP32])])).
% 0.08/0.45 fof(f40,plain,(
% 0.08/0.45 (e3 != op(e3,e1) & e3 != op(e2,e1) & e3 != op(e1,e1) & e3 != op(e0,e1)) | ~sP33),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP33])])).
% 0.08/0.45 fof(f41,plain,(
% 0.08/0.45 (e0 != op(e2,e3) & e0 != op(e2,e2) & e0 != op(e2,e1) & e0 != op(e2,e0)) | ~sP34),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP34])])).
% 0.08/0.45 fof(f42,plain,(
% 0.08/0.45 (e0 != op(e3,e2) & e0 != op(e2,e2) & e0 != op(e1,e2) & e0 != op(e0,e2)) | ~sP35),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP35])])).
% 0.08/0.45 fof(f43,plain,(
% 0.08/0.45 (e1 != op(e2,e3) & e1 != op(e2,e2) & e1 != op(e2,e1) & e1 != op(e2,e0)) | ~sP36),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP36])])).
% 0.08/0.45 fof(f44,plain,(
% 0.08/0.45 (e1 != op(e3,e2) & e1 != op(e2,e2) & e1 != op(e1,e2) & e1 != op(e0,e2)) | ~sP37),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP37])])).
% 0.08/0.45 fof(f45,plain,(
% 0.08/0.45 (e2 != op(e2,e3) & e2 != op(e2,e2) & e2 != op(e2,e1) & e2 != op(e2,e0)) | ~sP38),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP38])])).
% 0.08/0.45 fof(f46,plain,(
% 0.08/0.45 (e2 != op(e3,e2) & e2 != op(e2,e2) & e2 != op(e1,e2) & e2 != op(e0,e2)) | ~sP39),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP39])])).
% 0.08/0.45 fof(f47,plain,(
% 0.08/0.45 (e3 != op(e2,e3) & e3 != op(e2,e2) & e3 != op(e2,e1) & e3 != op(e2,e0)) | ~sP40),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP40])])).
% 0.08/0.45 fof(f48,plain,(
% 0.08/0.45 (e3 != op(e3,e2) & e3 != op(e2,e2) & e3 != op(e1,e2) & e3 != op(e0,e2)) | ~sP41),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP41])])).
% 0.08/0.45 fof(f49,plain,(
% 0.08/0.45 (e0 != op(e3,e3) & e0 != op(e3,e2) & e0 != op(e3,e1) & e0 != op(e3,e0)) | ~sP42),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP42])])).
% 0.08/0.45 fof(f50,plain,(
% 0.08/0.45 (e0 != op(e3,e3) & e0 != op(e2,e3) & e0 != op(e1,e3) & e0 != op(e0,e3)) | ~sP43),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP43])])).
% 0.08/0.45 fof(f51,plain,(
% 0.08/0.45 (e1 != op(e3,e3) & e1 != op(e3,e2) & e1 != op(e3,e1) & e1 != op(e3,e0)) | ~sP44),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP44])])).
% 0.08/0.45 fof(f52,plain,(
% 0.08/0.45 (e1 != op(e3,e3) & e1 != op(e2,e3) & e1 != op(e1,e3) & e1 != op(e0,e3)) | ~sP45),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP45])])).
% 0.08/0.45 fof(f53,plain,(
% 0.08/0.45 (e2 != op(e3,e3) & e2 != op(e3,e2) & e2 != op(e3,e1) & e2 != op(e3,e0)) | ~sP46),
% 0.08/0.45 introduced(predicate_definition_introduction,[new_symbols(naming,[sP46])])).
% 0.08/0.45 fof(f54,plain,(
% 0.08/0.45 (e3 != op(e3,e3) & e3 != op(e2,e3) & e3 != op(e1,e3) & e3 != op(e0,e3)) | (e3 != op(e3,e3) & e3 != op(e3,e2) & e3 != op(e3,e1) & e3 != op(e3,e0)) | (e2 != op(e3,e3) & e2 != op(e2,e3) & e2 != op(e1,e3) & e2 != op(e0,e3)) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | sP17 | e3 != op(e3,unit) | e3 != op(unit,e3) | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | e0 != op(e0,unit) | e0 != op(unit,e0) | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0),
% 0.08/0.45 inference(definition_folding,[],[f6,f53,f52,f51,f50,f49,f48,f47,f46,f45,f44,f43,f42,f41,f40,f39,f38,f37,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7])).
% 0.08/0.45 fof(f55,plain,(
% 0.08/0.45 (e2 != op(e3,e3) & e2 != op(e3,e2) & e2 != op(e3,e1) & e2 != op(e3,e0)) | ~sP46),
% 0.08/0.45 inference(nnf_transformation,[],[f53])).
% 0.08/0.45 fof(f56,plain,(
% 0.08/0.45 (e1 != op(e3,e3) & e1 != op(e2,e3) & e1 != op(e1,e3) & e1 != op(e0,e3)) | ~sP45),
% 0.08/0.45 inference(nnf_transformation,[],[f52])).
% 0.08/0.45 fof(f57,plain,(
% 0.08/0.45 (e1 != op(e3,e3) & e1 != op(e3,e2) & e1 != op(e3,e1) & e1 != op(e3,e0)) | ~sP44),
% 0.08/0.45 inference(nnf_transformation,[],[f51])).
% 0.08/0.45 fof(f58,plain,(
% 0.08/0.45 (e0 != op(e3,e3) & e0 != op(e2,e3) & e0 != op(e1,e3) & e0 != op(e0,e3)) | ~sP43),
% 0.08/0.45 inference(nnf_transformation,[],[f50])).
% 0.08/0.45 fof(f59,plain,(
% 0.08/0.45 (e0 != op(e3,e3) & e0 != op(e3,e2) & e0 != op(e3,e1) & e0 != op(e3,e0)) | ~sP42),
% 0.08/0.45 inference(nnf_transformation,[],[f49])).
% 0.08/0.46 fof(f60,plain,(
% 0.08/0.46 (e3 != op(e3,e2) & e3 != op(e2,e2) & e3 != op(e1,e2) & e3 != op(e0,e2)) | ~sP41),
% 0.08/0.46 inference(nnf_transformation,[],[f48])).
% 0.08/0.46 fof(f61,plain,(
% 0.08/0.46 (e3 != op(e2,e3) & e3 != op(e2,e2) & e3 != op(e2,e1) & e3 != op(e2,e0)) | ~sP40),
% 0.08/0.46 inference(nnf_transformation,[],[f47])).
% 0.08/0.46 fof(f62,plain,(
% 0.08/0.46 (e2 != op(e3,e2) & e2 != op(e2,e2) & e2 != op(e1,e2) & e2 != op(e0,e2)) | ~sP39),
% 0.08/0.46 inference(nnf_transformation,[],[f46])).
% 0.08/0.46 fof(f63,plain,(
% 0.08/0.46 (e2 != op(e2,e3) & e2 != op(e2,e2) & e2 != op(e2,e1) & e2 != op(e2,e0)) | ~sP38),
% 0.08/0.46 inference(nnf_transformation,[],[f45])).
% 0.08/0.46 fof(f64,plain,(
% 0.08/0.46 (e1 != op(e3,e2) & e1 != op(e2,e2) & e1 != op(e1,e2) & e1 != op(e0,e2)) | ~sP37),
% 0.08/0.46 inference(nnf_transformation,[],[f44])).
% 0.08/0.46 fof(f65,plain,(
% 0.08/0.46 (e1 != op(e2,e3) & e1 != op(e2,e2) & e1 != op(e2,e1) & e1 != op(e2,e0)) | ~sP36),
% 0.08/0.46 inference(nnf_transformation,[],[f43])).
% 0.08/0.46 fof(f66,plain,(
% 0.08/0.46 (e0 != op(e3,e2) & e0 != op(e2,e2) & e0 != op(e1,e2) & e0 != op(e0,e2)) | ~sP35),
% 0.08/0.46 inference(nnf_transformation,[],[f42])).
% 0.08/0.46 fof(f67,plain,(
% 0.08/0.46 (e0 != op(e2,e3) & e0 != op(e2,e2) & e0 != op(e2,e1) & e0 != op(e2,e0)) | ~sP34),
% 0.08/0.46 inference(nnf_transformation,[],[f41])).
% 0.08/0.46 fof(f68,plain,(
% 0.08/0.46 (e3 != op(e3,e1) & e3 != op(e2,e1) & e3 != op(e1,e1) & e3 != op(e0,e1)) | ~sP33),
% 0.08/0.46 inference(nnf_transformation,[],[f40])).
% 0.08/0.46 fof(f69,plain,(
% 0.08/0.46 (e3 != op(e1,e3) & e3 != op(e1,e2) & e3 != op(e1,e1) & e3 != op(e1,e0)) | ~sP32),
% 0.08/0.46 inference(nnf_transformation,[],[f39])).
% 0.08/0.46 fof(f70,plain,(
% 0.08/0.46 (e2 != op(e3,e1) & e2 != op(e2,e1) & e2 != op(e1,e1) & e2 != op(e0,e1)) | ~sP31),
% 0.08/0.46 inference(nnf_transformation,[],[f38])).
% 0.08/0.46 fof(f71,plain,(
% 0.08/0.46 (e2 != op(e1,e3) & e2 != op(e1,e2) & e2 != op(e1,e1) & e2 != op(e1,e0)) | ~sP30),
% 0.08/0.46 inference(nnf_transformation,[],[f37])).
% 0.08/0.46 fof(f72,plain,(
% 0.08/0.46 (e1 != op(e3,e1) & e1 != op(e2,e1) & e1 != op(e1,e1) & e1 != op(e0,e1)) | ~sP29),
% 0.08/0.46 inference(nnf_transformation,[],[f36])).
% 0.08/0.46 fof(f73,plain,(
% 0.08/0.46 (e1 != op(e1,e3) & e1 != op(e1,e2) & e1 != op(e1,e1) & e1 != op(e1,e0)) | ~sP28),
% 0.08/0.46 inference(nnf_transformation,[],[f35])).
% 0.08/0.46 fof(f74,plain,(
% 0.08/0.46 (e0 != op(e3,e1) & e0 != op(e2,e1) & e0 != op(e1,e1) & e0 != op(e0,e1)) | ~sP27),
% 0.08/0.46 inference(nnf_transformation,[],[f34])).
% 0.08/0.46 fof(f75,plain,(
% 0.08/0.46 (e0 != op(e1,e3) & e0 != op(e1,e2) & e0 != op(e1,e1) & e0 != op(e1,e0)) | ~sP26),
% 0.08/0.46 inference(nnf_transformation,[],[f33])).
% 0.08/0.46 fof(f76,plain,(
% 0.08/0.46 (e3 != op(e3,e0) & e3 != op(e2,e0) & e3 != op(e1,e0) & e3 != op(e0,e0)) | ~sP25),
% 0.08/0.46 inference(nnf_transformation,[],[f32])).
% 0.08/0.46 fof(f77,plain,(
% 0.08/0.46 (e3 != op(e0,e3) & e3 != op(e0,e2) & e3 != op(e0,e1) & e3 != op(e0,e0)) | ~sP24),
% 0.08/0.46 inference(nnf_transformation,[],[f31])).
% 0.08/0.46 fof(f78,plain,(
% 0.08/0.46 (e2 != op(e3,e0) & e2 != op(e2,e0) & e2 != op(e1,e0) & e2 != op(e0,e0)) | ~sP23),
% 0.08/0.46 inference(nnf_transformation,[],[f30])).
% 0.08/0.46 fof(f79,plain,(
% 0.08/0.46 (e2 != op(e0,e3) & e2 != op(e0,e2) & e2 != op(e0,e1) & e2 != op(e0,e0)) | ~sP22),
% 0.08/0.46 inference(nnf_transformation,[],[f29])).
% 0.08/0.46 fof(f80,plain,(
% 0.08/0.46 (e1 != op(e3,e0) & e1 != op(e2,e0) & e1 != op(e1,e0) & e1 != op(e0,e0)) | ~sP21),
% 0.08/0.46 inference(nnf_transformation,[],[f28])).
% 0.08/0.46 fof(f81,plain,(
% 0.08/0.46 (e1 != op(e0,e3) & e1 != op(e0,e2) & e1 != op(e0,e1) & e1 != op(e0,e0)) | ~sP20),
% 0.08/0.46 inference(nnf_transformation,[],[f27])).
% 0.08/0.46 fof(f82,plain,(
% 0.08/0.46 (e0 != op(e3,e0) & e0 != op(e2,e0) & e0 != op(e1,e0) & e0 != op(e0,e0)) | ~sP19),
% 0.08/0.46 inference(nnf_transformation,[],[f26])).
% 0.08/0.46 fof(f83,plain,(
% 0.08/0.46 (e0 != op(e0,e3) & e0 != op(e0,e2) & e0 != op(e0,e1) & e0 != op(e0,e0)) | ~sP18),
% 0.08/0.46 inference(nnf_transformation,[],[f25])).
% 0.08/0.46 fof(f84,plain,(
% 0.08/0.46 (e3 != unit & e2 != unit & e1 != unit & e0 != unit) | ~sP17),
% 0.08/0.46 inference(nnf_transformation,[],[f24])).
% 0.08/0.46 fof(f85,plain,(
% 0.08/0.46 (e3 != op(e3,e3) & e2 != op(e3,e3) & e1 != op(e3,e3) & e0 != op(e3,e3)) | ~sP16),
% 0.08/0.46 inference(nnf_transformation,[],[f23])).
% 0.08/0.46 fof(f86,plain,(
% 0.08/0.46 (e3 != op(e3,e2) & e2 != op(e3,e2) & e1 != op(e3,e2) & e0 != op(e3,e2)) | ~sP15),
% 0.08/0.46 inference(nnf_transformation,[],[f22])).
% 0.08/0.46 fof(f87,plain,(
% 0.08/0.46 (e3 != op(e3,e1) & e2 != op(e3,e1) & e1 != op(e3,e1) & e0 != op(e3,e1)) | ~sP14),
% 0.08/0.46 inference(nnf_transformation,[],[f21])).
% 0.08/0.46 fof(f88,plain,(
% 0.08/0.46 (e3 != op(e3,e0) & e2 != op(e3,e0) & e1 != op(e3,e0) & e0 != op(e3,e0)) | ~sP13),
% 0.08/0.46 inference(nnf_transformation,[],[f20])).
% 0.08/0.46 fof(f89,plain,(
% 0.08/0.46 (e3 != op(e2,e3) & e2 != op(e2,e3) & e1 != op(e2,e3) & e0 != op(e2,e3)) | ~sP12),
% 0.08/0.46 inference(nnf_transformation,[],[f19])).
% 0.08/0.46 fof(f90,plain,(
% 0.08/0.46 (e3 != op(e2,e2) & e2 != op(e2,e2) & e1 != op(e2,e2) & e0 != op(e2,e2)) | ~sP11),
% 0.08/0.46 inference(nnf_transformation,[],[f18])).
% 0.08/0.46 fof(f91,plain,(
% 0.08/0.46 (e3 != op(e2,e1) & e2 != op(e2,e1) & e1 != op(e2,e1) & e0 != op(e2,e1)) | ~sP10),
% 0.08/0.46 inference(nnf_transformation,[],[f17])).
% 0.08/0.46 fof(f92,plain,(
% 0.08/0.46 (e3 != op(e2,e0) & e2 != op(e2,e0) & e1 != op(e2,e0) & e0 != op(e2,e0)) | ~sP9),
% 0.08/0.46 inference(nnf_transformation,[],[f16])).
% 0.08/0.46 fof(f93,plain,(
% 0.08/0.46 (e3 != op(e1,e3) & e2 != op(e1,e3) & e1 != op(e1,e3) & e0 != op(e1,e3)) | ~sP8),
% 0.08/0.46 inference(nnf_transformation,[],[f15])).
% 0.08/0.46 fof(f94,plain,(
% 0.08/0.46 (e3 != op(e1,e2) & e2 != op(e1,e2) & e1 != op(e1,e2) & e0 != op(e1,e2)) | ~sP7),
% 0.08/0.46 inference(nnf_transformation,[],[f14])).
% 0.08/0.46 fof(f95,plain,(
% 0.08/0.46 (e3 != op(e1,e1) & e2 != op(e1,e1) & e1 != op(e1,e1) & e0 != op(e1,e1)) | ~sP6),
% 0.08/0.46 inference(nnf_transformation,[],[f13])).
% 0.08/0.46 fof(f96,plain,(
% 0.08/0.46 (e3 != op(e1,e0) & e2 != op(e1,e0) & e1 != op(e1,e0) & e0 != op(e1,e0)) | ~sP5),
% 0.08/0.46 inference(nnf_transformation,[],[f12])).
% 0.08/0.46 fof(f97,plain,(
% 0.08/0.46 (e3 != op(e0,e3) & e2 != op(e0,e3) & e1 != op(e0,e3) & e0 != op(e0,e3)) | ~sP4),
% 0.08/0.46 inference(nnf_transformation,[],[f11])).
% 0.08/0.46 fof(f98,plain,(
% 0.08/0.46 (e3 != op(e0,e2) & e2 != op(e0,e2) & e1 != op(e0,e2) & e0 != op(e0,e2)) | ~sP3),
% 0.08/0.46 inference(nnf_transformation,[],[f10])).
% 0.08/0.46 fof(f99,plain,(
% 0.08/0.46 (e3 != op(e0,e1) & e2 != op(e0,e1) & e1 != op(e0,e1) & e0 != op(e0,e1)) | ~sP2),
% 0.08/0.46 inference(nnf_transformation,[],[f9])).
% 0.08/0.46 fof(f100,plain,(
% 0.08/0.46 (e3 != op(e0,e0) & e2 != op(e0,e0) & e1 != op(e0,e0) & e0 != op(e0,e0)) | ~sP1),
% 0.08/0.46 inference(nnf_transformation,[],[f8])).
% 0.08/0.46 fof(f101,plain,(
% 0.08/0.46 ((e3 != op(e3,e3) | e3 != op(e2,e2) | e3 != op(e1,e1) | e3 != op(e0,e0)) & (e2 != op(e3,e3) | e2 != op(e2,e2) | e2 != op(e1,e1) | e2 != op(e0,e0)) & (e1 != op(e3,e3) | e1 != op(e2,e2) | e1 != op(e1,e1) | e1 != op(e0,e0)) & (e0 != op(e3,e3) | e0 != op(e2,e2) | e0 != op(e1,e1) | e0 != op(e0,e0))) | ~sP0),
% 0.08/0.46 inference(nnf_transformation,[],[f7])).
% 0.08/0.46 fof(f103,plain,(
% 0.08/0.46 e2 != op(e3,e1) | ~sP46),
% 0.08/0.46 inference(cnf_transformation,[],[f55])).
% 0.08/0.46 fof(f108,plain,(
% 0.08/0.46 e1 != op(e2,e3) | ~sP45),
% 0.08/0.46 inference(cnf_transformation,[],[f56])).
% 0.08/0.46 fof(f112,plain,(
% 0.08/0.46 e1 != op(e3,e2) | ~sP44),
% 0.08/0.46 inference(cnf_transformation,[],[f57])).
% 0.08/0.46 fof(f117,plain,(
% 0.08/0.46 e0 != op(e3,e3) | ~sP43),
% 0.08/0.46 inference(cnf_transformation,[],[f58])).
% 0.08/0.46 fof(f121,plain,(
% 0.08/0.46 e0 != op(e3,e3) | ~sP42),
% 0.08/0.46 inference(cnf_transformation,[],[f59])).
% 0.08/0.46 fof(f123,plain,(
% 0.08/0.46 e3 != op(e1,e2) | ~sP41),
% 0.08/0.46 inference(cnf_transformation,[],[f60])).
% 0.08/0.46 fof(f127,plain,(
% 0.08/0.46 e3 != op(e2,e1) | ~sP40),
% 0.08/0.46 inference(cnf_transformation,[],[f61])).
% 0.08/0.46 fof(f130,plain,(
% 0.08/0.46 e2 != op(e0,e2) | ~sP39),
% 0.08/0.46 inference(cnf_transformation,[],[f62])).
% 0.08/0.46 fof(f134,plain,(
% 0.08/0.46 e2 != op(e2,e0) | ~sP38),
% 0.08/0.46 inference(cnf_transformation,[],[f63])).
% 0.08/0.46 fof(f141,plain,(
% 0.08/0.46 e1 != op(e3,e2) | ~sP37),
% 0.08/0.46 inference(cnf_transformation,[],[f64])).
% 0.08/0.46 fof(f145,plain,(
% 0.08/0.46 e1 != op(e2,e3) | ~sP36),
% 0.08/0.46 inference(cnf_transformation,[],[f65])).
% 0.08/0.46 fof(f148,plain,(
% 0.08/0.46 e0 != op(e2,e2) | ~sP35),
% 0.08/0.46 inference(cnf_transformation,[],[f66])).
% 0.08/0.46 fof(f152,plain,(
% 0.08/0.46 e0 != op(e2,e2) | ~sP34),
% 0.08/0.46 inference(cnf_transformation,[],[f67])).
% 0.08/0.46 fof(f156,plain,(
% 0.08/0.46 e3 != op(e2,e1) | ~sP33),
% 0.08/0.46 inference(cnf_transformation,[],[f68])).
% 0.08/0.46 fof(f160,plain,(
% 0.08/0.46 e3 != op(e1,e2) | ~sP32),
% 0.08/0.46 inference(cnf_transformation,[],[f69])).
% 0.08/0.46 fof(f165,plain,(
% 0.08/0.46 e2 != op(e3,e1) | ~sP31),
% 0.08/0.46 inference(cnf_transformation,[],[f70])).
% 0.08/0.46 fof(f169,plain,(
% 0.08/0.46 e2 != op(e1,e3) | ~sP30),
% 0.08/0.46 inference(cnf_transformation,[],[f71])).
% 0.08/0.46 fof(f170,plain,(
% 0.08/0.46 e1 != op(e0,e1) | ~sP29),
% 0.08/0.46 inference(cnf_transformation,[],[f72])).
% 0.08/0.46 fof(f174,plain,(
% 0.08/0.46 e1 != op(e1,e0) | ~sP28),
% 0.08/0.46 inference(cnf_transformation,[],[f73])).
% 0.08/0.46 fof(f179,plain,(
% 0.08/0.46 e0 != op(e1,e1) | ~sP27),
% 0.08/0.46 inference(cnf_transformation,[],[f74])).
% 0.08/0.46 fof(f183,plain,(
% 0.08/0.46 e0 != op(e1,e1) | ~sP26),
% 0.08/0.46 inference(cnf_transformation,[],[f75])).
% 0.08/0.46 fof(f189,plain,(
% 0.08/0.46 e3 != op(e3,e0) | ~sP25),
% 0.08/0.46 inference(cnf_transformation,[],[f76])).
% 0.08/0.46 fof(f193,plain,(
% 0.08/0.46 e3 != op(e0,e3) | ~sP24),
% 0.08/0.46 inference(cnf_transformation,[],[f77])).
% 0.08/0.46 fof(f196,plain,(
% 0.08/0.46 e2 != op(e2,e0) | ~sP23),
% 0.08/0.46 inference(cnf_transformation,[],[f78])).
% 0.08/0.46 fof(f200,plain,(
% 0.08/0.46 e2 != op(e0,e2) | ~sP22),
% 0.08/0.46 inference(cnf_transformation,[],[f79])).
% 0.08/0.46 fof(f203,plain,(
% 0.08/0.46 e1 != op(e1,e0) | ~sP21),
% 0.08/0.46 inference(cnf_transformation,[],[f80])).
% 0.08/0.46 fof(f207,plain,(
% 0.08/0.46 e1 != op(e0,e1) | ~sP20),
% 0.08/0.46 inference(cnf_transformation,[],[f81])).
% 0.08/0.46 fof(f210,plain,(
% 0.08/0.46 e0 != op(e0,e0) | ~sP19),
% 0.08/0.46 inference(cnf_transformation,[],[f82])).
% 0.08/0.46 fof(f214,plain,(
% 0.08/0.46 e0 != op(e0,e0) | ~sP18),
% 0.08/0.46 inference(cnf_transformation,[],[f83])).
% 0.08/0.46 fof(f218,plain,(
% 0.08/0.46 e0 != unit | ~sP17),
% 0.08/0.46 inference(cnf_transformation,[],[f84])).
% 0.08/0.46 fof(f222,plain,(
% 0.08/0.46 e0 != op(e3,e3) | ~sP16),
% 0.08/0.46 inference(cnf_transformation,[],[f85])).
% 0.08/0.46 fof(f227,plain,(
% 0.08/0.46 e1 != op(e3,e2) | ~sP15),
% 0.08/0.46 inference(cnf_transformation,[],[f86])).
% 0.08/0.46 fof(f232,plain,(
% 0.08/0.46 e2 != op(e3,e1) | ~sP14),
% 0.08/0.46 inference(cnf_transformation,[],[f87])).
% 0.08/0.46 fof(f237,plain,(
% 0.08/0.46 e3 != op(e3,e0) | ~sP13),
% 0.08/0.46 inference(cnf_transformation,[],[f88])).
% 0.08/0.46 fof(f239,plain,(
% 0.08/0.46 e1 != op(e2,e3) | ~sP12),
% 0.08/0.46 inference(cnf_transformation,[],[f89])).
% 0.08/0.46 fof(f242,plain,(
% 0.08/0.46 e0 != op(e2,e2) | ~sP11),
% 0.08/0.46 inference(cnf_transformation,[],[f90])).
% 0.08/0.46 fof(f249,plain,(
% 0.08/0.46 e3 != op(e2,e1) | ~sP10),
% 0.08/0.46 inference(cnf_transformation,[],[f91])).
% 0.08/0.46 fof(f252,plain,(
% 0.08/0.46 e2 != op(e2,e0) | ~sP9),
% 0.08/0.46 inference(cnf_transformation,[],[f92])).
% 0.08/0.46 fof(f256,plain,(
% 0.08/0.46 e2 != op(e1,e3) | ~sP8),
% 0.08/0.46 inference(cnf_transformation,[],[f93])).
% 0.08/0.46 fof(f261,plain,(
% 0.08/0.46 e3 != op(e1,e2) | ~sP7),
% 0.08/0.46 inference(cnf_transformation,[],[f94])).
% 0.08/0.46 fof(f262,plain,(
% 0.08/0.46 e0 != op(e1,e1) | ~sP6),
% 0.08/0.46 inference(cnf_transformation,[],[f95])).
% 0.08/0.46 fof(f267,plain,(
% 0.08/0.46 e1 != op(e1,e0) | ~sP5),
% 0.08/0.46 inference(cnf_transformation,[],[f96])).
% 0.08/0.46 fof(f273,plain,(
% 0.08/0.46 e3 != op(e0,e3) | ~sP4),
% 0.08/0.46 inference(cnf_transformation,[],[f97])).
% 0.08/0.46 fof(f276,plain,(
% 0.08/0.46 e2 != op(e0,e2) | ~sP3),
% 0.08/0.46 inference(cnf_transformation,[],[f98])).
% 0.08/0.46 fof(f279,plain,(
% 0.08/0.46 e1 != op(e0,e1) | ~sP2),
% 0.08/0.46 inference(cnf_transformation,[],[f99])).
% 0.08/0.46 fof(f282,plain,(
% 0.08/0.46 e0 != op(e0,e0) | ~sP1),
% 0.08/0.46 inference(cnf_transformation,[],[f100])).
% 0.08/0.46 fof(f286,plain,(
% 0.08/0.46 e0 != op(e3,e3) | e0 != op(e2,e2) | e0 != op(e1,e1) | e0 != op(e0,e0) | ~sP0),
% 0.08/0.46 inference(cnf_transformation,[],[f101])).
% 0.08/0.46 fof(f291,plain,(
% 0.08/0.46 e3 != op(e0,e3) | e3 != op(e3,e0) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | sP17 | e3 != op(e3,unit) | e3 != op(unit,e3) | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | e0 != op(e0,unit) | e0 != op(unit,e0) | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0),
% 0.08/0.46 inference(cnf_transformation,[],[f54])).
% 0.08/0.46 fof(f354,plain,(
% 0.08/0.46 e0 = unit),
% 0.08/0.46 inference(cnf_transformation,[],[f3])).
% 0.08/0.46 fof(f361,plain,(
% 0.08/0.46 e0 = op(e0,e0)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f362,plain,(
% 0.08/0.46 e1 = op(e0,e1)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f363,plain,(
% 0.08/0.46 e2 = op(e0,e2)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f364,plain,(
% 0.08/0.46 e3 = op(e0,e3)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f365,plain,(
% 0.08/0.46 e1 = op(e1,e0)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f366,plain,(
% 0.08/0.46 e0 = op(e1,e1)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f367,plain,(
% 0.08/0.46 e3 = op(e1,e2)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f368,plain,(
% 0.08/0.46 e2 = op(e1,e3)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f369,plain,(
% 0.08/0.46 e2 = op(e2,e0)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f370,plain,(
% 0.08/0.46 e3 = op(e2,e1)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f371,plain,(
% 0.08/0.46 e0 = op(e2,e2)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f372,plain,(
% 0.08/0.46 e1 = op(e2,e3)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f373,plain,(
% 0.08/0.46 e3 = op(e3,e0)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f374,plain,(
% 0.08/0.46 e2 = op(e3,e1)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f375,plain,(
% 0.08/0.46 e1 = op(e3,e2)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f376,plain,(
% 0.08/0.46 e0 = op(e3,e3)),
% 0.08/0.46 inference(cnf_transformation,[],[f2])).
% 0.08/0.46 fof(f380,plain,(
% 0.08/0.46 op(e3,e3) != unit | ~sP43),
% 0.08/0.46 inference(definition_unfolding,[],[f117,f354])).
% 0.08/0.46 fof(f384,plain,(
% 0.08/0.46 op(e3,e3) != unit | ~sP42),
% 0.08/0.46 inference(definition_unfolding,[],[f121,f354])).
% 0.08/0.46 fof(f390,plain,(
% 0.08/0.46 e2 != op(unit,e2) | ~sP39),
% 0.08/0.46 inference(definition_unfolding,[],[f130,f354])).
% 0.08/0.46 fof(f391,plain,(
% 0.08/0.46 e2 != op(e2,unit) | ~sP38),
% 0.08/0.46 inference(definition_unfolding,[],[f134,f354])).
% 0.08/0.46 fof(f395,plain,(
% 0.08/0.46 op(e2,e2) != unit | ~sP35),
% 0.08/0.46 inference(definition_unfolding,[],[f148,f354])).
% 0.08/0.46 fof(f399,plain,(
% 0.08/0.46 op(e2,e2) != unit | ~sP34),
% 0.08/0.46 inference(definition_unfolding,[],[f152,f354])).
% 0.08/0.46 fof(f406,plain,(
% 0.08/0.46 e1 != op(unit,e1) | ~sP29),
% 0.08/0.46 inference(definition_unfolding,[],[f170,f354])).
% 0.08/0.46 fof(f407,plain,(
% 0.08/0.46 e1 != op(e1,unit) | ~sP28),
% 0.08/0.46 inference(definition_unfolding,[],[f174,f354])).
% 0.08/0.46 fof(f410,plain,(
% 0.08/0.46 op(e1,e1) != unit | ~sP27),
% 0.08/0.46 inference(definition_unfolding,[],[f179,f354])).
% 0.08/0.46 fof(f414,plain,(
% 0.08/0.46 op(e1,e1) != unit | ~sP26),
% 0.08/0.46 inference(definition_unfolding,[],[f183,f354])).
% 0.08/0.46 fof(f416,plain,(
% 0.08/0.46 e3 != op(e3,unit) | ~sP25),
% 0.08/0.46 inference(definition_unfolding,[],[f189,f354])).
% 0.08/0.46 fof(f420,plain,(
% 0.08/0.46 e3 != op(unit,e3) | ~sP24),
% 0.08/0.46 inference(definition_unfolding,[],[f193,f354])).
% 0.08/0.46 fof(f425,plain,(
% 0.08/0.46 e2 != op(e2,unit) | ~sP23),
% 0.08/0.46 inference(definition_unfolding,[],[f196,f354])).
% 0.08/0.46 fof(f429,plain,(
% 0.08/0.46 e2 != op(unit,e2) | ~sP22),
% 0.08/0.46 inference(definition_unfolding,[],[f200,f354])).
% 0.08/0.46 fof(f434,plain,(
% 0.08/0.46 e1 != op(e1,unit) | ~sP21),
% 0.08/0.46 inference(definition_unfolding,[],[f203,f354])).
% 0.08/0.46 fof(f438,plain,(
% 0.08/0.46 e1 != op(unit,e1) | ~sP20),
% 0.08/0.46 inference(definition_unfolding,[],[f207,f354])).
% 0.08/0.46 fof(f443,plain,(
% 0.08/0.46 op(unit,unit) != unit | ~sP19),
% 0.08/0.46 inference(definition_unfolding,[],[f210,f354,f354,f354])).
% 0.08/0.46 fof(f447,plain,(
% 0.08/0.46 op(unit,unit) != unit | ~sP18),
% 0.08/0.46 inference(definition_unfolding,[],[f214,f354,f354,f354])).
% 0.08/0.46 fof(f448,plain,(
% 0.08/0.46 unit != unit | ~sP17),
% 0.08/0.46 inference(definition_unfolding,[],[f218,f354])).
% 0.08/0.46 fof(f449,plain,(
% 0.08/0.46 op(e3,e3) != unit | ~sP16),
% 0.08/0.46 inference(definition_unfolding,[],[f222,f354])).
% 0.08/0.46 fof(f452,plain,(
% 0.08/0.46 e3 != op(e3,unit) | ~sP13),
% 0.08/0.46 inference(definition_unfolding,[],[f237,f354])).
% 0.08/0.46 fof(f457,plain,(
% 0.08/0.46 op(e2,e2) != unit | ~sP11),
% 0.08/0.46 inference(definition_unfolding,[],[f242,f354])).
% 0.08/0.46 fof(f460,plain,(
% 0.08/0.46 e2 != op(e2,unit) | ~sP9),
% 0.08/0.46 inference(definition_unfolding,[],[f252,f354])).
% 0.08/0.46 fof(f465,plain,(
% 0.08/0.46 op(e1,e1) != unit | ~sP6),
% 0.08/0.46 inference(definition_unfolding,[],[f262,f354])).
% 0.08/0.46 fof(f468,plain,(
% 0.08/0.46 e1 != op(e1,unit) | ~sP5),
% 0.08/0.46 inference(definition_unfolding,[],[f267,f354])).
% 0.08/0.46 fof(f470,plain,(
% 0.08/0.46 e3 != op(unit,e3) | ~sP4),
% 0.08/0.46 inference(definition_unfolding,[],[f273,f354])).
% 0.08/0.46 fof(f475,plain,(
% 0.08/0.46 e2 != op(unit,e2) | ~sP3),
% 0.08/0.46 inference(definition_unfolding,[],[f276,f354])).
% 0.08/0.46 fof(f480,plain,(
% 0.08/0.46 e1 != op(unit,e1) | ~sP2),
% 0.08/0.46 inference(definition_unfolding,[],[f279,f354])).
% 0.08/0.46 fof(f485,plain,(
% 0.08/0.46 op(unit,unit) != unit | ~sP1),
% 0.08/0.46 inference(definition_unfolding,[],[f282,f354,f354,f354])).
% 0.08/0.46 fof(f489,plain,(
% 0.08/0.46 op(e3,e3) != unit | op(e2,e2) != unit | op(e1,e1) != unit | op(unit,unit) != unit | ~sP0),
% 0.08/0.46 inference(definition_unfolding,[],[f286,f354,f354,f354,f354,f354,f354])).
% 0.08/0.46 fof(f552,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | sP17 | e3 != op(e3,unit) | e3 != op(unit,e3) | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0),
% 0.08/0.46 inference(definition_unfolding,[],[f291,f354,f354,f354,f354,f354,f354])).
% 0.08/0.46 fof(f557,plain,(
% 0.08/0.46 op(e3,e3) = unit),
% 0.08/0.46 inference(definition_unfolding,[],[f376,f354])).
% 0.08/0.46 fof(f558,plain,(
% 0.08/0.46 e3 = op(e3,unit)),
% 0.08/0.46 inference(definition_unfolding,[],[f373,f354])).
% 0.08/0.46 fof(f559,plain,(
% 0.08/0.46 op(e2,e2) = unit),
% 0.08/0.46 inference(definition_unfolding,[],[f371,f354])).
% 0.08/0.46 fof(f560,plain,(
% 0.08/0.46 e2 = op(e2,unit)),
% 0.08/0.46 inference(definition_unfolding,[],[f369,f354])).
% 0.08/0.46 fof(f561,plain,(
% 0.08/0.46 op(e1,e1) = unit),
% 0.08/0.46 inference(definition_unfolding,[],[f366,f354])).
% 0.08/0.46 fof(f562,plain,(
% 0.08/0.46 e1 = op(e1,unit)),
% 0.08/0.46 inference(definition_unfolding,[],[f365,f354])).
% 0.08/0.46 fof(f563,plain,(
% 0.08/0.46 e3 = op(unit,e3)),
% 0.08/0.46 inference(definition_unfolding,[],[f364,f354])).
% 0.08/0.46 fof(f564,plain,(
% 0.08/0.46 e2 = op(unit,e2)),
% 0.08/0.46 inference(definition_unfolding,[],[f363,f354])).
% 0.08/0.46 fof(f565,plain,(
% 0.08/0.46 e1 = op(unit,e1)),
% 0.08/0.46 inference(definition_unfolding,[],[f362,f354])).
% 0.08/0.46 fof(f566,plain,(
% 0.08/0.46 op(unit,unit) = unit),
% 0.08/0.46 inference(definition_unfolding,[],[f361,f354,f354,f354])).
% 0.08/0.46 fof(f568,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | sP17 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0),
% 0.08/0.46 inference(duplicate_literal_removal,[],[f552])).
% 0.08/0.46 fof(f631,plain,(
% 0.08/0.46 ~sP17),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f448])).
% 0.08/0.46 fof(f1912,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f568,f631])).
% 0.08/0.46 fof(f1913,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1912,f485])).
% 0.08/0.46 fof(f1914,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1913,f447])).
% 0.08/0.46 fof(f1915,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1914,f443])).
% 0.08/0.46 fof(f1916,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1915,f406])).
% 0.08/0.46 fof(f1917,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1916,f438])).
% 0.08/0.46 fof(f1918,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1917,f480])).
% 0.08/0.46 fof(f1919,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1918,f407])).
% 0.08/0.46 fof(f1920,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1919,f434])).
% 0.08/0.46 fof(f1921,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP3 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1920,f468])).
% 0.08/0.46 fof(f1922,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP3 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1921,f390])).
% 0.08/0.46 fof(f1923,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP3 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1922,f429])).
% 0.08/0.46 fof(f1924,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1923,f475])).
% 0.08/0.46 fof(f1925,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1924,f391])).
% 0.08/0.46 fof(f1926,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1925,f425])).
% 0.08/0.46 fof(f1927,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP8 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1926,f460])).
% 0.08/0.46 fof(f1928,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | sP25 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP8 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1927,f169])).
% 0.08/0.46 fof(f1929,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | sP25 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1928,f256])).
% 0.08/0.46 fof(f1930,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1929,f416])).
% 0.08/0.46 fof(f1931,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1930,f452])).
% 0.08/0.46 fof(f1932,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1931,f420])).
% 0.08/0.46 fof(f1933,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f1932,f470])).
% 0.08/0.46 fof(f1963,plain,(
% 0.08/0.46 unit != unit | ~sP43),
% 0.08/0.46 inference(backward_demodulation,[],[f557,f380])).
% 0.08/0.46 fof(f1964,plain,(
% 0.08/0.46 unit != unit | ~sP42),
% 0.08/0.46 inference(backward_demodulation,[],[f557,f384])).
% 0.08/0.46 fof(f1965,plain,(
% 0.08/0.46 unit != unit | ~sP16),
% 0.08/0.46 inference(backward_demodulation,[],[f557,f449])).
% 0.08/0.46 fof(f1969,plain,(
% 0.08/0.46 unit != unit | op(e2,e2) != unit | op(e1,e1) != unit | op(unit,unit) != unit | ~sP0),
% 0.08/0.46 inference(backward_demodulation,[],[f557,f489])).
% 0.08/0.46 fof(f1981,plain,(
% 0.08/0.46 op(e2,e2) != unit | op(e1,e1) != unit | op(unit,unit) != unit | ~sP0),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f1969])).
% 0.08/0.46 fof(f1982,plain,(
% 0.08/0.46 ~sP16),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f1965])).
% 0.08/0.46 fof(f1983,plain,(
% 0.08/0.46 ~sP42),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f1964])).
% 0.08/0.46 fof(f1984,plain,(
% 0.08/0.46 ~sP43),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f1963])).
% 0.08/0.46 fof(f1986,plain,(
% 0.08/0.46 e1 != e1 | ~sP44),
% 0.08/0.46 inference(backward_demodulation,[],[f375,f112])).
% 0.08/0.46 fof(f1989,plain,(
% 0.08/0.46 e1 != e1 | ~sP37),
% 0.08/0.46 inference(backward_demodulation,[],[f375,f141])).
% 0.08/0.46 fof(f1990,plain,(
% 0.08/0.46 e1 != e1 | ~sP15),
% 0.08/0.46 inference(backward_demodulation,[],[f375,f227])).
% 0.08/0.46 fof(f2000,plain,(
% 0.08/0.46 ~sP15),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f1990])).
% 0.08/0.46 fof(f2001,plain,(
% 0.08/0.46 ~sP37),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f1989])).
% 0.08/0.46 fof(f2002,plain,(
% 0.08/0.46 ~sP44),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f1986])).
% 0.08/0.46 fof(f2003,plain,(
% 0.08/0.46 e2 != e2 | ~sP46),
% 0.08/0.46 inference(backward_demodulation,[],[f374,f103])).
% 0.08/0.46 fof(f2006,plain,(
% 0.08/0.46 e2 != e2 | ~sP31),
% 0.08/0.46 inference(backward_demodulation,[],[f374,f165])).
% 0.08/0.46 fof(f2009,plain,(
% 0.08/0.46 e2 != e2 | ~sP14),
% 0.08/0.46 inference(backward_demodulation,[],[f374,f232])).
% 0.08/0.46 fof(f2018,plain,(
% 0.08/0.46 ~sP14),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2009])).
% 0.08/0.46 fof(f2019,plain,(
% 0.08/0.46 ~sP31),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2006])).
% 0.08/0.46 fof(f2020,plain,(
% 0.08/0.46 ~sP46),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2003])).
% 0.08/0.46 fof(f2035,plain,(
% 0.08/0.46 e3 != e3 | e3 != op(unit,e3) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(backward_demodulation,[],[f558,f1933])).
% 0.08/0.46 fof(f2036,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2035])).
% 0.08/0.46 fof(f2069,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2036,f2020])).
% 0.08/0.46 fof(f2070,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2069,f2002])).
% 0.08/0.46 fof(f2071,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2070,f1984])).
% 0.08/0.46 fof(f2072,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2071,f1983])).
% 0.08/0.46 fof(f2073,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2072,f2001])).
% 0.08/0.46 fof(f2074,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2073,f2019])).
% 0.08/0.46 fof(f2075,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2074,f1982])).
% 0.08/0.46 fof(f2076,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2075,f2000])).
% 0.08/0.46 fof(f2077,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2076,f2018])).
% 0.08/0.46 fof(f2078,plain,(
% 0.08/0.46 e1 != e1 | ~sP45),
% 0.08/0.46 inference(backward_demodulation,[],[f372,f108])).
% 0.08/0.46 fof(f2081,plain,(
% 0.08/0.46 e1 != e1 | ~sP36),
% 0.08/0.46 inference(backward_demodulation,[],[f372,f145])).
% 0.08/0.46 fof(f2082,plain,(
% 0.08/0.46 e1 != e1 | ~sP12),
% 0.08/0.46 inference(backward_demodulation,[],[f372,f239])).
% 0.08/0.46 fof(f2091,plain,(
% 0.08/0.46 ~sP12),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2082])).
% 0.08/0.46 fof(f2092,plain,(
% 0.08/0.46 ~sP36),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2081])).
% 0.08/0.46 fof(f2093,plain,(
% 0.08/0.46 ~sP45),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2078])).
% 0.08/0.46 fof(f2103,plain,(
% 0.08/0.46 unit != unit | ~sP35),
% 0.08/0.46 inference(backward_demodulation,[],[f559,f395])).
% 0.08/0.46 fof(f2104,plain,(
% 0.08/0.46 unit != unit | ~sP34),
% 0.08/0.46 inference(backward_demodulation,[],[f559,f399])).
% 0.08/0.46 fof(f2105,plain,(
% 0.08/0.46 unit != unit | ~sP11),
% 0.08/0.46 inference(backward_demodulation,[],[f559,f457])).
% 0.08/0.46 fof(f2114,plain,(
% 0.08/0.46 unit != unit | op(e1,e1) != unit | op(unit,unit) != unit | ~sP0),
% 0.08/0.46 inference(backward_demodulation,[],[f559,f1981])).
% 0.08/0.46 fof(f2115,plain,(
% 0.08/0.46 op(e1,e1) != unit | op(unit,unit) != unit | ~sP0),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2114])).
% 0.08/0.46 fof(f2116,plain,(
% 0.08/0.46 ~sP11),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2105])).
% 0.08/0.46 fof(f2117,plain,(
% 0.08/0.46 ~sP34),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2104])).
% 0.08/0.46 fof(f2118,plain,(
% 0.08/0.46 ~sP35),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2103])).
% 0.08/0.46 fof(f2119,plain,(
% 0.08/0.46 e3 != e3 | ~sP40),
% 0.08/0.46 inference(backward_demodulation,[],[f370,f127])).
% 0.08/0.46 fof(f2122,plain,(
% 0.08/0.46 e3 != e3 | ~sP33),
% 0.08/0.46 inference(backward_demodulation,[],[f370,f156])).
% 0.08/0.46 fof(f2127,plain,(
% 0.08/0.46 e3 != e3 | ~sP10),
% 0.08/0.46 inference(backward_demodulation,[],[f370,f249])).
% 0.08/0.46 fof(f2135,plain,(
% 0.08/0.46 ~sP10),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2127])).
% 0.08/0.46 fof(f2136,plain,(
% 0.08/0.46 ~sP33),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2122])).
% 0.08/0.46 fof(f2137,plain,(
% 0.08/0.46 ~sP40),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2119])).
% 0.08/0.46 fof(f2152,plain,(
% 0.08/0.46 e2 != e2 | e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(backward_demodulation,[],[f560,f2077])).
% 0.08/0.46 fof(f2153,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2152])).
% 0.08/0.46 fof(f2159,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2153,f2093])).
% 0.08/0.46 fof(f2160,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2159,f2137])).
% 0.08/0.46 fof(f2161,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2160,f2092])).
% 0.08/0.46 fof(f2162,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2161,f2118])).
% 0.08/0.46 fof(f2163,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2162,f2117])).
% 0.08/0.46 fof(f2164,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2163,f2136])).
% 0.08/0.46 fof(f2165,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2164,f2091])).
% 0.08/0.46 fof(f2166,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2165,f2116])).
% 0.08/0.46 fof(f2167,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2166,f2135])).
% 0.08/0.46 fof(f2178,plain,(
% 0.08/0.46 e2 != e2 | e3 != op(unit,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46 inference(backward_demodulation,[],[f368,f2167])).
% 0.08/0.46 fof(f2179,plain,(
% 0.08/0.46 e3 != op(unit,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2178])).
% 0.08/0.46 fof(f2182,plain,(
% 0.08/0.46 e3 != e3 | ~sP41),
% 0.08/0.46 inference(backward_demodulation,[],[f367,f123])).
% 0.08/0.46 fof(f2185,plain,(
% 0.08/0.46 e3 != e3 | ~sP32),
% 0.08/0.46 inference(backward_demodulation,[],[f367,f160])).
% 0.08/0.46 fof(f2190,plain,(
% 0.08/0.46 e3 != e3 | ~sP7),
% 0.08/0.46 inference(backward_demodulation,[],[f367,f261])).
% 0.08/0.46 fof(f2194,plain,(
% 0.08/0.46 ~sP7),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2190])).
% 0.08/0.46 fof(f2195,plain,(
% 0.08/0.46 ~sP32),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2185])).
% 0.08/0.46 fof(f2196,plain,(
% 0.08/0.46 ~sP41),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2182])).
% 0.08/0.46 fof(f2206,plain,(
% 0.08/0.46 unit != unit | ~sP27),
% 0.08/0.46 inference(backward_demodulation,[],[f561,f410])).
% 0.08/0.46 fof(f2207,plain,(
% 0.08/0.46 unit != unit | ~sP26),
% 0.08/0.46 inference(backward_demodulation,[],[f561,f414])).
% 0.08/0.46 fof(f2208,plain,(
% 0.08/0.46 unit != unit | ~sP6),
% 0.08/0.46 inference(backward_demodulation,[],[f561,f465])).
% 0.08/0.46 fof(f2209,plain,(
% 0.08/0.46 unit != unit | op(unit,unit) != unit | ~sP0),
% 0.08/0.46 inference(backward_demodulation,[],[f561,f2115])).
% 0.08/0.46 fof(f2210,plain,(
% 0.08/0.46 op(unit,unit) != unit | ~sP0),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2209])).
% 0.08/0.46 fof(f2211,plain,(
% 0.08/0.46 ~sP6),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2208])).
% 0.08/0.46 fof(f2212,plain,(
% 0.08/0.46 ~sP26),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2207])).
% 0.08/0.46 fof(f2213,plain,(
% 0.08/0.46 ~sP27),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2206])).
% 0.08/0.46 fof(f2226,plain,(
% 0.08/0.46 e1 != e1 | e3 != op(unit,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46 inference(backward_demodulation,[],[f562,f2179])).
% 0.08/0.46 fof(f2227,plain,(
% 0.08/0.46 e3 != op(unit,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2226])).
% 0.08/0.46 fof(f2231,plain,(
% 0.08/0.46 e3 != op(unit,e3) | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2227,f2196])).
% 0.08/0.46 fof(f2232,plain,(
% 0.08/0.46 e3 != op(unit,e3) | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2231,f2195])).
% 0.08/0.46 fof(f2233,plain,(
% 0.08/0.46 e3 != op(unit,e3) | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2232,f2213])).
% 0.08/0.46 fof(f2234,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2233,f2212])).
% 0.08/0.46 fof(f2235,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP6 | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2234,f2194])).
% 0.08/0.46 fof(f2236,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP0),
% 0.08/0.46 inference(subsumption_resolution,[],[f2235,f2211])).
% 0.08/0.46 fof(f2237,plain,(
% 0.08/0.46 e3 != op(unit,e3) | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit),
% 0.08/0.46 inference(subsumption_resolution,[],[f2236,f2210])).
% 0.08/0.46 fof(f2248,plain,(
% 0.08/0.46 e3 != e3 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit),
% 0.08/0.46 inference(backward_demodulation,[],[f563,f2237])).
% 0.08/0.46 fof(f2249,plain,(
% 0.08/0.46 e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2248])).
% 0.08/0.46 fof(f2264,plain,(
% 0.08/0.46 e2 != e2 | e1 != op(unit,e1) | op(unit,unit) != unit),
% 0.08/0.46 inference(backward_demodulation,[],[f564,f2249])).
% 0.08/0.46 fof(f2265,plain,(
% 0.08/0.46 e1 != op(unit,e1) | op(unit,unit) != unit),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2264])).
% 0.08/0.46 fof(f2281,plain,(
% 0.08/0.46 e1 != e1 | op(unit,unit) != unit),
% 0.08/0.46 inference(backward_demodulation,[],[f565,f2265])).
% 0.08/0.46 fof(f2282,plain,(
% 0.08/0.46 op(unit,unit) != unit),
% 0.08/0.46 inference(trivial_inequality_removal,[],[f2281])).
% 0.08/0.46 fof(f2286,plain,(
% 0.08/0.46 $false),
% 0.08/0.46 inference(subsumption_resolution,[],[f566,f2282])).
% 0.08/0.46 % SZS output end Proof for theBenchmark
% 0.08/0.46 % ------------------------------
% 0.08/0.46 % Version: Vampire 4.2.2 (commit 552c234 on 2018-07-02 14:53:33 +0100)
% 0.08/0.46 % Termination reason: Refutation
% 0.08/0.46
% 0.08/0.46 % Memory used [KB]: 1535
% 0.08/0.46 % Time elapsed: 0.178 s
% 0.08/0.46 % ------------------------------
% 0.08/0.46 % ------------------------------
% 0.08/0.46 % Success in time 0.214 s
%------------------------------------------------------------------------------