%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG062+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:21:02 AM UTC 2026
% Result : Theorem 0.20s 0.32s
% Output : Refutation 0.20s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
( op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& op(unit,e4) = e4
& op(e4,unit) = e4
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3
| unit = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f5,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e0 != e4
& e1 != e2
& e1 != e3
& e1 != e4
& e2 != e3
& e2 != e4
& e3 != e4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( e0 = op(e1,op(op(e1,e1),op(e1,e1)))
& e2 = op(op(e1,e1),op(e1,e1))
& e3 = op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1)))
& e4 = op(e1,e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,conjecture,
~ ( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( ( ( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit ) )
& ( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit ) )
& ( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit ) )
& ( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit ) )
& ( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit ) )
& ( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit ) )
& ( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit ) )
& ( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit ) )
& ( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit ) )
& ( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit ) )
& ( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit ) )
& ( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit ) )
& ( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit ) )
& ( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit ) )
& ( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit ) )
& ( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit ) )
& ( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit ) )
& ( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit ) )
& ( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit ) )
& ( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit ) )
& ( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit ) )
& ( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit ) )
& ( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit ) )
& ( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit ) )
& ( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit ) ) )
| ( ( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit ) )
& ( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit ) )
& ( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit ) )
& ( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit ) )
& ( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit ) )
& ( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit ) )
& ( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit ) )
& ( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit ) )
& ( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit ) )
& ( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit ) )
& ( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit ) )
& ( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit ) )
& ( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit ) )
& ( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit ) )
& ( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit ) )
& ( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit ) )
& ( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit ) )
& ( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit ) )
& ( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit ) )
& ( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit ) )
& ( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit ) )
& ( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit ) )
& ( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit ) )
& ( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit ) )
& ( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit ) ) )
| ( ( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit ) )
& ( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit ) )
& ( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit ) )
& ( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit ) )
& ( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit ) )
& ( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit ) )
& ( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit ) )
& ( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit ) )
& ( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit ) )
& ( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit ) )
& ( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit ) )
& ( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit ) )
& ( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit ) )
& ( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit ) )
& ( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit ) )
& ( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit ) )
& ( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit ) )
& ( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit ) )
& ( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit ) )
& ( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit ) )
& ( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit ) )
& ( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit ) )
& ( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit ) )
& ( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit ) )
& ( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit ) ) )
| ( ( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit ) )
& ( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit ) )
& ( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit ) )
& ( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit ) )
& ( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit ) )
& ( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit ) )
& ( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit ) )
& ( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit ) )
& ( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit ) )
& ( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit ) )
& ( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit ) )
& ( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit ) )
& ( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit ) )
& ( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit ) )
& ( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit ) )
& ( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit ) )
& ( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit ) )
& ( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit ) )
& ( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit ) )
& ( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit ) )
& ( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit ) )
& ( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit ) )
& ( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit ) )
& ( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit ) )
& ( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit ) ) )
| ( ( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit ) )
& ( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit ) )
& ( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit ) )
& ( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit ) )
& ( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit ) )
& ( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit ) )
& ( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit ) )
& ( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit ) )
& ( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit ) )
& ( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit ) )
& ( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit ) )
& ( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit ) )
& ( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit ) )
& ( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit ) )
& ( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit ) )
& ( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit ) )
& ( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit ) )
& ( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit ) )
& ( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit ) )
& ( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit ) )
& ( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit ) )
& ( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit ) )
& ( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit ) )
& ( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit ) )
& ( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f8,negated_conjecture,
~ ~ ( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( ( ( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit ) )
& ( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit ) )
& ( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit ) )
& ( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit ) )
& ( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit ) )
& ( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit ) )
& ( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit ) )
& ( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit ) )
& ( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit ) )
& ( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit ) )
& ( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit ) )
& ( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit ) )
& ( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit ) )
& ( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit ) )
& ( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit ) )
& ( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit ) )
& ( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit ) )
& ( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit ) )
& ( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit ) )
& ( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit ) )
& ( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit ) )
& ( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit ) )
& ( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit ) )
& ( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit ) )
& ( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit ) ) )
| ( ( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit ) )
& ( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit ) )
& ( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit ) )
& ( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit ) )
& ( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit ) )
& ( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit ) )
& ( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit ) )
& ( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit ) )
& ( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit ) )
& ( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit ) )
& ( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit ) )
& ( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit ) )
& ( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit ) )
& ( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit ) )
& ( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit ) )
& ( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit ) )
& ( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit ) )
& ( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit ) )
& ( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit ) )
& ( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit ) )
& ( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit ) )
& ( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit ) )
& ( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit ) )
& ( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit ) )
& ( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit ) ) )
| ( ( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit ) )
& ( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit ) )
& ( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit ) )
& ( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit ) )
& ( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit ) )
& ( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit ) )
& ( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit ) )
& ( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit ) )
& ( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit ) )
& ( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit ) )
& ( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit ) )
& ( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit ) )
& ( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit ) )
& ( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit ) )
& ( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit ) )
& ( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit ) )
& ( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit ) )
& ( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit ) )
& ( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit ) )
& ( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit ) )
& ( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit ) )
& ( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit ) )
& ( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit ) )
& ( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit ) )
& ( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit ) ) )
| ( ( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit ) )
& ( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit ) )
& ( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit ) )
& ( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit ) )
& ( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit ) )
& ( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit ) )
& ( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit ) )
& ( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit ) )
& ( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit ) )
& ( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit ) )
& ( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit ) )
& ( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit ) )
& ( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit ) )
& ( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit ) )
& ( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit ) )
& ( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit ) )
& ( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit ) )
& ( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit ) )
& ( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit ) )
& ( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit ) )
& ( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit ) )
& ( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit ) )
& ( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit ) )
& ( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit ) )
& ( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit ) ) )
| ( ( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit ) )
& ( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit ) )
& ( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit ) )
& ( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit ) )
& ( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit ) )
& ( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit ) )
& ( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit ) )
& ( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit ) )
& ( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit ) )
& ( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit ) )
& ( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit ) )
& ( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit ) )
& ( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit ) )
& ( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit ) )
& ( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit ) )
& ( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit ) )
& ( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit ) )
& ( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit ) )
& ( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit ) )
& ( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit ) )
& ( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit ) )
& ( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit ) )
& ( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit ) )
& ( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit ) )
& ( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f9,plain,
( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( ( ( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit ) )
& ( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit ) )
& ( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit ) )
& ( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit ) )
& ( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit ) )
& ( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit ) )
& ( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit ) )
& ( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit ) )
& ( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit ) )
& ( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit ) )
& ( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit ) )
& ( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit ) )
& ( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit ) )
& ( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit ) )
& ( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit ) )
& ( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit ) )
& ( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit ) )
& ( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit ) )
& ( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit ) )
& ( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit ) )
& ( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit ) )
& ( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit ) )
& ( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit ) )
& ( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit ) )
& ( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit ) ) )
| ( ( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit ) )
& ( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit ) )
& ( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit ) )
& ( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit ) )
& ( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit ) )
& ( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit ) )
& ( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit ) )
& ( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit ) )
& ( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit ) )
& ( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit ) )
& ( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit ) )
& ( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit ) )
& ( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit ) )
& ( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit ) )
& ( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit ) )
& ( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit ) )
& ( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit ) )
& ( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit ) )
& ( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit ) )
& ( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit ) )
& ( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit ) )
& ( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit ) )
& ( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit ) )
& ( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit ) )
& ( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit ) ) )
| ( ( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit ) )
& ( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit ) )
& ( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit ) )
& ( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit ) )
& ( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit ) )
& ( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit ) )
& ( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit ) )
& ( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit ) )
& ( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit ) )
& ( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit ) )
& ( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit ) )
& ( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit ) )
& ( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit ) )
& ( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit ) )
& ( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit ) )
& ( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit ) )
& ( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit ) )
& ( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit ) )
& ( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit ) )
& ( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit ) )
& ( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit ) )
& ( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit ) )
& ( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit ) )
& ( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit ) )
& ( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit ) ) )
| ( ( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit ) )
& ( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit ) )
& ( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit ) )
& ( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit ) )
& ( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit ) )
& ( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit ) )
& ( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit ) )
& ( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit ) )
& ( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit ) )
& ( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit ) )
& ( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit ) )
& ( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit ) )
& ( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit ) )
& ( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit ) )
& ( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit ) )
& ( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit ) )
& ( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit ) )
& ( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit ) )
& ( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit ) )
& ( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit ) )
& ( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit ) )
& ( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit ) )
& ( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit ) )
& ( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit ) )
& ( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit ) ) )
| ( ( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit ) )
& ( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit ) )
& ( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit ) )
& ( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit ) )
& ( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit ) )
& ( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit ) )
& ( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit ) )
& ( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit ) )
& ( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit ) )
& ( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit ) )
& ( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit ) )
& ( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit ) )
& ( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit ) )
& ( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit ) )
& ( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit ) )
& ( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit ) )
& ( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit ) )
& ( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit ) )
& ( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit ) )
& ( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit ) )
& ( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit ) )
& ( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit ) )
& ( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit ) )
& ( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit ) )
& ( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit ) ) ) ) ),
inference(flattening,[],[f8]) ).
fof(f10,definition,
( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11,definition,
( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f12,definition,
( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f13,definition,
( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f14,definition,
( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f15,definition,
( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f16,definition,
( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f17,definition,
( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f18,definition,
( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f19,definition,
( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f20,definition,
( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f21,definition,
( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f22,definition,
( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f23,definition,
( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f24,definition,
( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f25,definition,
( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f26,definition,
( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f27,definition,
( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f28,definition,
( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f29,definition,
( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f30,definition,
( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f31,definition,
( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f32,definition,
( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f33,definition,
( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit )
| ~ sP23 ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f34,definition,
( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit )
| ~ sP24 ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f35,definition,
( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit )
| ~ sP25 ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f36,definition,
( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit )
| ~ sP26 ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f37,definition,
( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit )
| ~ sP27 ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f38,definition,
( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit )
| ~ sP28 ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f39,definition,
( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit )
| ~ sP29 ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f40,definition,
( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit )
| ~ sP30 ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f41,definition,
( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit )
| ~ sP31 ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f42,definition,
( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit )
| ~ sP32 ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f43,definition,
( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit )
| ~ sP33 ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f44,definition,
( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit )
| ~ sP34 ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f45,definition,
( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit )
| ~ sP35 ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f46,definition,
( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit )
| ~ sP36 ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f47,definition,
( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit )
| ~ sP37 ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f48,definition,
( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit )
| ~ sP38 ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f49,definition,
( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit )
| ~ sP39 ),
introduced(definition,[new_symbols(definition,[sP39])],[predicate_definition_introduction]) ).
fof(f50,definition,
( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit )
| ~ sP40 ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f51,definition,
( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit )
| ~ sP41 ),
introduced(definition,[new_symbols(definition,[sP41])],[predicate_definition_introduction]) ).
fof(f52,definition,
( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit )
| ~ sP42 ),
introduced(definition,[new_symbols(definition,[sP42])],[predicate_definition_introduction]) ).
fof(f53,definition,
( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit )
| ~ sP43 ),
introduced(definition,[new_symbols(definition,[sP43])],[predicate_definition_introduction]) ).
fof(f54,definition,
( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit )
| ~ sP44 ),
introduced(definition,[new_symbols(definition,[sP44])],[predicate_definition_introduction]) ).
fof(f55,definition,
( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit )
| ~ sP45 ),
introduced(definition,[new_symbols(definition,[sP45])],[predicate_definition_introduction]) ).
fof(f56,definition,
( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit )
| ~ sP46 ),
introduced(definition,[new_symbols(definition,[sP46])],[predicate_definition_introduction]) ).
fof(f57,definition,
( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit )
| ~ sP47 ),
introduced(definition,[new_symbols(definition,[sP47])],[predicate_definition_introduction]) ).
fof(f58,definition,
( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit )
| ~ sP48 ),
introduced(definition,[new_symbols(definition,[sP48])],[predicate_definition_introduction]) ).
fof(f59,definition,
( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit )
| ~ sP49 ),
introduced(definition,[new_symbols(definition,[sP49])],[predicate_definition_introduction]) ).
fof(f60,definition,
( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit )
| ~ sP50 ),
introduced(definition,[new_symbols(definition,[sP50])],[predicate_definition_introduction]) ).
fof(f61,definition,
( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit )
| ~ sP51 ),
introduced(definition,[new_symbols(definition,[sP51])],[predicate_definition_introduction]) ).
fof(f62,definition,
( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit )
| ~ sP52 ),
introduced(definition,[new_symbols(definition,[sP52])],[predicate_definition_introduction]) ).
fof(f63,definition,
( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit )
| ~ sP53 ),
introduced(definition,[new_symbols(definition,[sP53])],[predicate_definition_introduction]) ).
fof(f64,definition,
( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit )
| ~ sP54 ),
introduced(definition,[new_symbols(definition,[sP54])],[predicate_definition_introduction]) ).
fof(f65,definition,
( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit )
| ~ sP55 ),
introduced(definition,[new_symbols(definition,[sP55])],[predicate_definition_introduction]) ).
fof(f66,definition,
( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit )
| ~ sP56 ),
introduced(definition,[new_symbols(definition,[sP56])],[predicate_definition_introduction]) ).
fof(f67,definition,
( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit )
| ~ sP57 ),
introduced(definition,[new_symbols(definition,[sP57])],[predicate_definition_introduction]) ).
fof(f68,definition,
( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit )
| ~ sP58 ),
introduced(definition,[new_symbols(definition,[sP58])],[predicate_definition_introduction]) ).
fof(f69,definition,
( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit )
| ~ sP59 ),
introduced(definition,[new_symbols(definition,[sP59])],[predicate_definition_introduction]) ).
fof(f70,definition,
( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit )
| ~ sP60 ),
introduced(definition,[new_symbols(definition,[sP60])],[predicate_definition_introduction]) ).
fof(f71,definition,
( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit )
| ~ sP61 ),
introduced(definition,[new_symbols(definition,[sP61])],[predicate_definition_introduction]) ).
fof(f72,definition,
( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit )
| ~ sP62 ),
introduced(definition,[new_symbols(definition,[sP62])],[predicate_definition_introduction]) ).
fof(f73,definition,
( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit )
| ~ sP63 ),
introduced(definition,[new_symbols(definition,[sP63])],[predicate_definition_introduction]) ).
fof(f74,definition,
( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit )
| ~ sP64 ),
introduced(definition,[new_symbols(definition,[sP64])],[predicate_definition_introduction]) ).
fof(f75,definition,
( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit )
| ~ sP65 ),
introduced(definition,[new_symbols(definition,[sP65])],[predicate_definition_introduction]) ).
fof(f76,definition,
( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit )
| ~ sP66 ),
introduced(definition,[new_symbols(definition,[sP66])],[predicate_definition_introduction]) ).
fof(f77,definition,
( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit )
| ~ sP67 ),
introduced(definition,[new_symbols(definition,[sP67])],[predicate_definition_introduction]) ).
fof(f78,definition,
( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit )
| ~ sP68 ),
introduced(definition,[new_symbols(definition,[sP68])],[predicate_definition_introduction]) ).
fof(f79,definition,
( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit )
| ~ sP69 ),
introduced(definition,[new_symbols(definition,[sP69])],[predicate_definition_introduction]) ).
fof(f80,definition,
( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit )
| ~ sP70 ),
introduced(definition,[new_symbols(definition,[sP70])],[predicate_definition_introduction]) ).
fof(f81,definition,
( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit )
| ~ sP71 ),
introduced(definition,[new_symbols(definition,[sP71])],[predicate_definition_introduction]) ).
fof(f82,definition,
( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit )
| ~ sP72 ),
introduced(definition,[new_symbols(definition,[sP72])],[predicate_definition_introduction]) ).
fof(f83,definition,
( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit )
| ~ sP73 ),
introduced(definition,[new_symbols(definition,[sP73])],[predicate_definition_introduction]) ).
fof(f84,definition,
( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit )
| ~ sP74 ),
introduced(definition,[new_symbols(definition,[sP74])],[predicate_definition_introduction]) ).
fof(f85,definition,
( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit )
| ~ sP75 ),
introduced(definition,[new_symbols(definition,[sP75])],[predicate_definition_introduction]) ).
fof(f86,definition,
( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit )
| ~ sP76 ),
introduced(definition,[new_symbols(definition,[sP76])],[predicate_definition_introduction]) ).
fof(f87,definition,
( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit )
| ~ sP77 ),
introduced(definition,[new_symbols(definition,[sP77])],[predicate_definition_introduction]) ).
fof(f88,definition,
( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit )
| ~ sP78 ),
introduced(definition,[new_symbols(definition,[sP78])],[predicate_definition_introduction]) ).
fof(f89,definition,
( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit )
| ~ sP79 ),
introduced(definition,[new_symbols(definition,[sP79])],[predicate_definition_introduction]) ).
fof(f90,definition,
( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit )
| ~ sP80 ),
introduced(definition,[new_symbols(definition,[sP80])],[predicate_definition_introduction]) ).
fof(f91,definition,
( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit )
| ~ sP81 ),
introduced(definition,[new_symbols(definition,[sP81])],[predicate_definition_introduction]) ).
fof(f92,definition,
( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit )
| ~ sP82 ),
introduced(definition,[new_symbols(definition,[sP82])],[predicate_definition_introduction]) ).
fof(f93,definition,
( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit )
| ~ sP83 ),
introduced(definition,[new_symbols(definition,[sP83])],[predicate_definition_introduction]) ).
fof(f94,definition,
( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit )
| ~ sP84 ),
introduced(definition,[new_symbols(definition,[sP84])],[predicate_definition_introduction]) ).
fof(f95,definition,
( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit )
| ~ sP85 ),
introduced(definition,[new_symbols(definition,[sP85])],[predicate_definition_introduction]) ).
fof(f96,definition,
( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit )
| ~ sP86 ),
introduced(definition,[new_symbols(definition,[sP86])],[predicate_definition_introduction]) ).
fof(f97,definition,
( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit )
| ~ sP87 ),
introduced(definition,[new_symbols(definition,[sP87])],[predicate_definition_introduction]) ).
fof(f98,definition,
( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit )
| ~ sP88 ),
introduced(definition,[new_symbols(definition,[sP88])],[predicate_definition_introduction]) ).
fof(f99,definition,
( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit )
| ~ sP89 ),
introduced(definition,[new_symbols(definition,[sP89])],[predicate_definition_introduction]) ).
fof(f100,definition,
( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit )
| ~ sP90 ),
introduced(definition,[new_symbols(definition,[sP90])],[predicate_definition_introduction]) ).
fof(f101,definition,
( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit )
| ~ sP91 ),
introduced(definition,[new_symbols(definition,[sP91])],[predicate_definition_introduction]) ).
fof(f102,definition,
( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit )
| ~ sP92 ),
introduced(definition,[new_symbols(definition,[sP92])],[predicate_definition_introduction]) ).
fof(f103,definition,
( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit )
| ~ sP93 ),
introduced(definition,[new_symbols(definition,[sP93])],[predicate_definition_introduction]) ).
fof(f104,definition,
( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit )
| ~ sP94 ),
introduced(definition,[new_symbols(definition,[sP94])],[predicate_definition_introduction]) ).
fof(f105,definition,
( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit )
| ~ sP95 ),
introduced(definition,[new_symbols(definition,[sP95])],[predicate_definition_introduction]) ).
fof(f106,definition,
( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit )
| ~ sP96 ),
introduced(definition,[new_symbols(definition,[sP96])],[predicate_definition_introduction]) ).
fof(f107,definition,
( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit )
| ~ sP97 ),
introduced(definition,[new_symbols(definition,[sP97])],[predicate_definition_introduction]) ).
fof(f108,definition,
( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit )
| ~ sP98 ),
introduced(definition,[new_symbols(definition,[sP98])],[predicate_definition_introduction]) ).
fof(f109,definition,
( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit )
| ~ sP99 ),
introduced(definition,[new_symbols(definition,[sP99])],[predicate_definition_introduction]) ).
fof(f110,definition,
( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit )
| ~ sP100 ),
introduced(definition,[new_symbols(definition,[sP100])],[predicate_definition_introduction]) ).
fof(f111,definition,
( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit )
| ~ sP101 ),
introduced(definition,[new_symbols(definition,[sP101])],[predicate_definition_introduction]) ).
fof(f112,definition,
( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit )
| ~ sP102 ),
introduced(definition,[new_symbols(definition,[sP102])],[predicate_definition_introduction]) ).
fof(f113,definition,
( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit )
| ~ sP103 ),
introduced(definition,[new_symbols(definition,[sP103])],[predicate_definition_introduction]) ).
fof(f114,definition,
( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit )
| ~ sP104 ),
introduced(definition,[new_symbols(definition,[sP104])],[predicate_definition_introduction]) ).
fof(f115,definition,
( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit )
| ~ sP105 ),
introduced(definition,[new_symbols(definition,[sP105])],[predicate_definition_introduction]) ).
fof(f116,definition,
( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit )
| ~ sP106 ),
introduced(definition,[new_symbols(definition,[sP106])],[predicate_definition_introduction]) ).
fof(f117,definition,
( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit )
| ~ sP107 ),
introduced(definition,[new_symbols(definition,[sP107])],[predicate_definition_introduction]) ).
fof(f118,definition,
( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit )
| ~ sP108 ),
introduced(definition,[new_symbols(definition,[sP108])],[predicate_definition_introduction]) ).
fof(f119,definition,
( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit )
| ~ sP109 ),
introduced(definition,[new_symbols(definition,[sP109])],[predicate_definition_introduction]) ).
fof(f120,definition,
( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit )
| ~ sP110 ),
introduced(definition,[new_symbols(definition,[sP110])],[predicate_definition_introduction]) ).
fof(f121,definition,
( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit )
| ~ sP111 ),
introduced(definition,[new_symbols(definition,[sP111])],[predicate_definition_introduction]) ).
fof(f122,definition,
( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit )
| ~ sP112 ),
introduced(definition,[new_symbols(definition,[sP112])],[predicate_definition_introduction]) ).
fof(f123,definition,
( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit )
| ~ sP113 ),
introduced(definition,[new_symbols(definition,[sP113])],[predicate_definition_introduction]) ).
fof(f124,definition,
( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit )
| ~ sP114 ),
introduced(definition,[new_symbols(definition,[sP114])],[predicate_definition_introduction]) ).
fof(f125,definition,
( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit )
| ~ sP115 ),
introduced(definition,[new_symbols(definition,[sP115])],[predicate_definition_introduction]) ).
fof(f126,definition,
( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit )
| ~ sP116 ),
introduced(definition,[new_symbols(definition,[sP116])],[predicate_definition_introduction]) ).
fof(f127,definition,
( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit )
| ~ sP117 ),
introduced(definition,[new_symbols(definition,[sP117])],[predicate_definition_introduction]) ).
fof(f128,definition,
( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit )
| ~ sP118 ),
introduced(definition,[new_symbols(definition,[sP118])],[predicate_definition_introduction]) ).
fof(f129,definition,
( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit )
| ~ sP119 ),
introduced(definition,[new_symbols(definition,[sP119])],[predicate_definition_introduction]) ).
fof(f130,definition,
( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit )
| ~ sP120 ),
introduced(definition,[new_symbols(definition,[sP120])],[predicate_definition_introduction]) ).
fof(f131,definition,
( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit )
| ~ sP121 ),
introduced(definition,[new_symbols(definition,[sP121])],[predicate_definition_introduction]) ).
fof(f132,definition,
( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit )
| ~ sP122 ),
introduced(definition,[new_symbols(definition,[sP122])],[predicate_definition_introduction]) ).
fof(f133,definition,
( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit )
| ~ sP123 ),
introduced(definition,[new_symbols(definition,[sP123])],[predicate_definition_introduction]) ).
fof(f134,definition,
( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit )
| ~ sP124 ),
introduced(definition,[new_symbols(definition,[sP124])],[predicate_definition_introduction]) ).
fof(f135,definition,
( ( sP24
& sP23
& sP22
& sP21
& sP20
& sP19
& sP18
& sP17
& sP16
& sP15
& sP14
& sP13
& sP12
& sP11
& sP10
& sP9
& sP8
& sP7
& sP6
& sP5
& sP4
& sP3
& sP2
& sP1
& sP0 )
| ~ sP125 ),
introduced(definition,[new_symbols(definition,[sP125])],[predicate_definition_introduction]) ).
fof(f136,definition,
( ( sP49
& sP48
& sP47
& sP46
& sP45
& sP44
& sP43
& sP42
& sP41
& sP40
& sP39
& sP38
& sP37
& sP36
& sP35
& sP34
& sP33
& sP32
& sP31
& sP30
& sP29
& sP28
& sP27
& sP26
& sP25 )
| ~ sP126 ),
introduced(definition,[new_symbols(definition,[sP126])],[predicate_definition_introduction]) ).
fof(f137,definition,
( ( sP74
& sP73
& sP72
& sP71
& sP70
& sP69
& sP68
& sP67
& sP66
& sP65
& sP64
& sP63
& sP62
& sP61
& sP60
& sP59
& sP58
& sP57
& sP56
& sP55
& sP54
& sP53
& sP52
& sP51
& sP50 )
| ~ sP127 ),
introduced(definition,[new_symbols(definition,[sP127])],[predicate_definition_introduction]) ).
fof(f138,definition,
( ( sP99
& sP98
& sP97
& sP96
& sP95
& sP94
& sP93
& sP92
& sP91
& sP90
& sP89
& sP88
& sP87
& sP86
& sP85
& sP84
& sP83
& sP82
& sP81
& sP80
& sP79
& sP78
& sP77
& sP76
& sP75 )
| ~ sP128 ),
introduced(definition,[new_symbols(definition,[sP128])],[predicate_definition_introduction]) ).
fof(f139,definition,
( ( sP124
& sP123
& sP122
& sP121
& sP120
& sP119
& sP118
& sP117
& sP116
& sP115
& sP114
& sP113
& sP112
& sP111
& sP110
& sP109
& sP108
& sP107
& sP106
& sP105
& sP104
& sP103
& sP102
& sP101
& sP100 )
| ~ sP129 ),
introduced(definition,[new_symbols(definition,[sP129])],[predicate_definition_introduction]) ).
fof(f140,plain,
( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( sP129
| sP128
| sP127
| sP126
| sP125 ) ),
inference(definition_folding,[],[f9,f139,f138,f137,f136,f135,f134,f133,f132,f131,f130,f129,f128,f127,f126,f125,f124,f123,f122,f121,f120,f119,f118,f117,f116,f115,f114,f113,f112,f111,f110,f109,f108,f107,f106,f105,f104,f103,f102,f101,f100,f99,f98,f97,f96,f95,f94,f93,f92,f91,f90,f89,f88,f87,f86,f85,f84,f83,f82,f81,f80,f79,f78,f77,f76,f75,f74,f73,f72,f71,f70,f69,f68,f67,f66,f65,f64,f63,f62,f61,f60,f59,f58,f57,f56,f55,f54,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]) ).
fof(f141,plain,
( ( sP124
& sP123
& sP122
& sP121
& sP120
& sP119
& sP118
& sP117
& sP116
& sP115
& sP114
& sP113
& sP112
& sP111
& sP110
& sP109
& sP108
& sP107
& sP106
& sP105
& sP104
& sP103
& sP102
& sP101
& sP100 )
| ~ sP129 ),
inference(nnf_transformation,[],[f139]) ).
fof(f142,plain,
( ( sP99
& sP98
& sP97
& sP96
& sP95
& sP94
& sP93
& sP92
& sP91
& sP90
& sP89
& sP88
& sP87
& sP86
& sP85
& sP84
& sP83
& sP82
& sP81
& sP80
& sP79
& sP78
& sP77
& sP76
& sP75 )
| ~ sP128 ),
inference(nnf_transformation,[],[f138]) ).
fof(f143,plain,
( ( sP74
& sP73
& sP72
& sP71
& sP70
& sP69
& sP68
& sP67
& sP66
& sP65
& sP64
& sP63
& sP62
& sP61
& sP60
& sP59
& sP58
& sP57
& sP56
& sP55
& sP54
& sP53
& sP52
& sP51
& sP50 )
| ~ sP127 ),
inference(nnf_transformation,[],[f137]) ).
fof(f144,plain,
( ( sP49
& sP48
& sP47
& sP46
& sP45
& sP44
& sP43
& sP42
& sP41
& sP40
& sP39
& sP38
& sP37
& sP36
& sP35
& sP34
& sP33
& sP32
& sP31
& sP30
& sP29
& sP28
& sP27
& sP26
& sP25 )
| ~ sP126 ),
inference(nnf_transformation,[],[f136]) ).
fof(f145,plain,
( ( sP24
& sP23
& sP22
& sP21
& sP20
& sP19
& sP18
& sP17
& sP16
& sP15
& sP14
& sP13
& sP12
& sP11
& sP10
& sP9
& sP8
& sP7
& sP6
& sP5
& sP4
& sP3
& sP2
& sP1
& sP0 )
| ~ sP125 ),
inference(nnf_transformation,[],[f135]) ).
fof(f146,plain,
( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit )
| ~ sP124 ),
inference(nnf_transformation,[],[f134]) ).
fof(f148,plain,
( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit )
| ~ sP122 ),
inference(nnf_transformation,[],[f132]) ).
fof(f149,plain,
( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit )
| ~ sP121 ),
inference(nnf_transformation,[],[f131]) ).
fof(f176,plain,
( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit )
| ~ sP94 ),
inference(nnf_transformation,[],[f104]) ).
fof(f178,plain,
( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit )
| ~ sP92 ),
inference(nnf_transformation,[],[f102]) ).
fof(f179,plain,
( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit )
| ~ sP91 ),
inference(nnf_transformation,[],[f101]) ).
fof(f206,plain,
( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit )
| ~ sP64 ),
inference(nnf_transformation,[],[f74]) ).
fof(f208,plain,
( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit )
| ~ sP62 ),
inference(nnf_transformation,[],[f72]) ).
fof(f209,plain,
( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit )
| ~ sP61 ),
inference(nnf_transformation,[],[f71]) ).
fof(f236,plain,
( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit )
| ~ sP34 ),
inference(nnf_transformation,[],[f44]) ).
fof(f238,plain,
( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit )
| ~ sP32 ),
inference(nnf_transformation,[],[f42]) ).
fof(f239,plain,
( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit )
| ~ sP31 ),
inference(nnf_transformation,[],[f41]) ).
fof(f252,plain,
( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit )
| ~ sP18 ),
inference(nnf_transformation,[],[f28]) ).
fof(f266,plain,
( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit )
| ~ sP4 ),
inference(nnf_transformation,[],[f14]) ).
fof(f268,plain,
( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit )
| ~ sP2 ),
inference(nnf_transformation,[],[f12]) ).
fof(f269,plain,
( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit )
| ~ sP1 ),
inference(nnf_transformation,[],[f11]) ).
fof(f296,plain,
( e0 = unit
| e1 = unit
| e2 = unit
| e3 = unit
| e4 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f297,plain,
e4 = op(e4,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f298,plain,
e4 = op(unit,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f299,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f300,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f301,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f303,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f305,plain,
e0 = op(e0,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f457,plain,
e3 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f458,plain,
e2 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f459,plain,
e2 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f460,plain,
e1 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f461,plain,
e1 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f462,plain,
e1 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f464,plain,
e0 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f465,plain,
e0 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f466,plain,
e0 != e1,
inference(cnf_transformation,[],[f5]) ).
fof(f467,plain,
e4 = op(e1,e1),
inference(cnf_transformation,[],[f6]) ).
fof(f492,plain,
( sP121
| ~ sP129 ),
inference(cnf_transformation,[],[f141]) ).
fof(f493,plain,
( sP122
| ~ sP129 ),
inference(cnf_transformation,[],[f141]) ).
fof(f495,plain,
( sP124
| ~ sP129 ),
inference(cnf_transformation,[],[f141]) ).
fof(f512,plain,
( sP91
| ~ sP128 ),
inference(cnf_transformation,[],[f142]) ).
fof(f513,plain,
( sP92
| ~ sP128 ),
inference(cnf_transformation,[],[f142]) ).
fof(f515,plain,
( sP94
| ~ sP128 ),
inference(cnf_transformation,[],[f142]) ).
fof(f532,plain,
( sP61
| ~ sP127 ),
inference(cnf_transformation,[],[f143]) ).
fof(f533,plain,
( sP62
| ~ sP127 ),
inference(cnf_transformation,[],[f143]) ).
fof(f535,plain,
( sP64
| ~ sP127 ),
inference(cnf_transformation,[],[f143]) ).
fof(f552,plain,
( sP31
| ~ sP126 ),
inference(cnf_transformation,[],[f144]) ).
fof(f553,plain,
( sP32
| ~ sP126 ),
inference(cnf_transformation,[],[f144]) ).
fof(f555,plain,
( sP34
| ~ sP126 ),
inference(cnf_transformation,[],[f144]) ).
fof(f572,plain,
( sP1
| ~ sP125 ),
inference(cnf_transformation,[],[f145]) ).
fof(f573,plain,
( sP2
| ~ sP125 ),
inference(cnf_transformation,[],[f145]) ).
fof(f575,plain,
( sP4
| ~ sP125 ),
inference(cnf_transformation,[],[f145]) ).
fof(f589,plain,
( sP18
| ~ sP125 ),
inference(cnf_transformation,[],[f145]) ).
fof(f596,plain,
( e0 != op(e0,e0)
| e0 != unit
| ~ sP124 ),
inference(cnf_transformation,[],[f146]) ).
fof(f601,plain,
( e0 != op(e0,e2)
| op(e0,e0) = e2
| ~ sP122 ),
inference(cnf_transformation,[],[f148]) ).
fof(f603,plain,
( e0 != op(e0,e3)
| op(e0,e0) = e3
| ~ sP121 ),
inference(cnf_transformation,[],[f149]) ).
fof(f657,plain,
( e1 != op(e1,e0)
| e0 = op(e1,e1)
| ~ sP94 ),
inference(cnf_transformation,[],[f176]) ).
fof(f661,plain,
( e1 != op(e1,e2)
| e2 = op(e1,e1)
| ~ sP92 ),
inference(cnf_transformation,[],[f178]) ).
fof(f663,plain,
( e1 != op(e1,e3)
| e3 = op(e1,e1)
| ~ sP91 ),
inference(cnf_transformation,[],[f179]) ).
fof(f717,plain,
( e2 != op(e2,e0)
| e0 = op(e2,e2)
| ~ sP64 ),
inference(cnf_transformation,[],[f206]) ).
fof(f720,plain,
( e2 != op(e2,e2)
| e2 != unit
| ~ sP62 ),
inference(cnf_transformation,[],[f208]) ).
fof(f723,plain,
( e2 != op(e2,e3)
| e3 = op(e2,e2)
| ~ sP61 ),
inference(cnf_transformation,[],[f209]) ).
fof(f777,plain,
( e3 != op(e3,e0)
| e0 = op(e3,e3)
| ~ sP34 ),
inference(cnf_transformation,[],[f236]) ).
fof(f781,plain,
( e3 != op(e3,e2)
| e2 = op(e3,e3)
| ~ sP32 ),
inference(cnf_transformation,[],[f238]) ).
fof(f782,plain,
( e3 != op(e3,e3)
| e3 != unit
| ~ sP31 ),
inference(cnf_transformation,[],[f239]) ).
fof(f808,plain,
( e4 != op(e1,e1)
| e4 != unit
| ~ sP18 ),
inference(cnf_transformation,[],[f252]) ).
fof(f837,plain,
( e4 != op(e4,e0)
| e0 = op(e4,e4)
| ~ sP4 ),
inference(cnf_transformation,[],[f266]) ).
fof(f841,plain,
( e4 != op(e4,e2)
| e2 = op(e4,e4)
| ~ sP2 ),
inference(cnf_transformation,[],[f268]) ).
fof(f843,plain,
( e4 != op(e4,e3)
| e3 = op(e4,e4)
| ~ sP1 ),
inference(cnf_transformation,[],[f269]) ).
fof(f846,plain,
( sP129
| sP128
| sP127
| sP126
| sP125 ),
inference(cnf_transformation,[],[f140]) ).
fof(f848,plain,
( op(e0,e0) = e3
| e3 = op(e1,e1)
| e3 = op(e2,e2)
| e3 = op(e3,e3)
| e3 = op(e4,e4) ),
inference(cnf_transformation,[],[f140]) ).
fof(f849,plain,
( op(e0,e0) = e2
| e2 = op(e1,e1)
| e2 = op(e2,e2)
| e2 = op(e3,e3)
| e2 = op(e4,e4) ),
inference(cnf_transformation,[],[f140]) ).
fof(f850,plain,
( op(e0,e0) = e1
| e1 = op(e1,e1)
| e1 = op(e2,e2)
| e1 = op(e3,e3)
| e1 = op(e4,e4) ),
inference(cnf_transformation,[],[f140]) ).
fof(f851,plain,
( e0 = op(e0,e0)
| e0 = op(e1,e1)
| e0 = op(e2,e2)
| e0 = op(e3,e3)
| e0 = op(e4,e4) ),
inference(cnf_transformation,[],[f140]) ).
fof(f852,plain,
( ~ sP124
| sP129 ),
inference(consistent_polarity_flipping,[],[f495]) ).
fof(f854,plain,
( sP122
| sP129 ),
inference(consistent_polarity_flipping,[],[f493]) ).
fof(f855,plain,
( sP121
| sP129 ),
inference(consistent_polarity_flipping,[],[f492]) ).
fof(f889,plain,
( ~ sP64
| ~ sP127 ),
inference(consistent_polarity_flipping,[],[f535]) ).
fof(f890,plain,
( ~ sP61
| ~ sP127 ),
inference(consistent_polarity_flipping,[],[f532]) ).
fof(f911,plain,
( sP34
| sP126 ),
inference(consistent_polarity_flipping,[],[f555]) ).
fof(f913,plain,
( ~ sP32
| sP126 ),
inference(consistent_polarity_flipping,[],[f553]) ).
fof(f914,plain,
( sP31
| sP126 ),
inference(consistent_polarity_flipping,[],[f552]) ).
fof(f927,plain,
( ~ sP18
| sP125 ),
inference(consistent_polarity_flipping,[],[f589]) ).
fof(f941,plain,
( ~ sP4
| sP125 ),
inference(consistent_polarity_flipping,[],[f575]) ).
fof(f943,plain,
( sP2
| sP125 ),
inference(consistent_polarity_flipping,[],[f573]) ).
fof(f944,plain,
( sP1
| sP125 ),
inference(consistent_polarity_flipping,[],[f572]) ).
fof(f947,plain,
( e0 != op(e0,e0)
| e0 != unit
| sP124 ),
inference(consistent_polarity_flipping,[],[f596]) ).
fof(f986,plain,
( e2 != op(e2,e0)
| e0 = op(e2,e2)
| sP64 ),
inference(consistent_polarity_flipping,[],[f717]) ).
fof(f988,plain,
( e2 != op(e2,e3)
| e3 = op(e2,e2)
| sP61 ),
inference(consistent_polarity_flipping,[],[f723]) ).
fof(f1018,plain,
( e3 != op(e3,e2)
| e2 = op(e3,e3)
| sP32 ),
inference(consistent_polarity_flipping,[],[f781]) ).
fof(f1035,plain,
( e4 != op(e1,e1)
| e4 != unit
| sP18 ),
inference(consistent_polarity_flipping,[],[f808]) ).
fof(f1054,plain,
( e4 != op(e4,e0)
| e0 = op(e4,e4)
| sP4 ),
inference(consistent_polarity_flipping,[],[f837]) ).
fof(f1060,plain,
( ~ sP129
| sP128
| sP127
| ~ sP126
| ~ sP125 ),
inference(consistent_polarity_flipping,[],[f846]) ).
fof(f1062,definition,
( spl130_1
<=> sP125 ),
introduced(definition,[new_symbols(definition,[spl130_1])],[avatar_definition]) ).
fof(f1066,definition,
( spl130_2
<=> sP126 ),
introduced(definition,[new_symbols(definition,[spl130_2])],[avatar_definition]) ).
fof(f1070,definition,
( spl130_3
<=> sP127 ),
introduced(definition,[new_symbols(definition,[spl130_3])],[avatar_definition]) ).
fof(f1074,definition,
( spl130_4
<=> sP128 ),
introduced(definition,[new_symbols(definition,[spl130_4])],[avatar_definition]) ).
fof(f1078,definition,
( spl130_5
<=> sP129 ),
introduced(definition,[new_symbols(definition,[spl130_5])],[avatar_definition]) ).
fof(f1081,plain,
( ~ spl130_1
| ~ spl130_2
| spl130_3
| spl130_4
| ~ spl130_5 ),
inference(avatar_split_clause,[],[f1060,f1078,f1074,f1070,f1066,f1062]) ).
fof(f1083,definition,
( spl130_6
<=> e4 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl130_6])],[avatar_definition]) ).
fof(f1085,plain,
( e4 = op(e4,e4)
| ~ spl130_6 ),
inference(avatar_component_clause,[],[f1083]) ).
fof(f1095,definition,
( spl130_9
<=> e4 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl130_9])],[avatar_definition]) ).
fof(f1097,plain,
( e4 = op(e1,e1)
| ~ spl130_9 ),
inference(avatar_component_clause,[],[f1095]) ).
fof(f1104,definition,
( spl130_11
<=> e3 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl130_11])],[avatar_definition]) ).
fof(f1105,plain,
( e3 != op(e4,e4)
| spl130_11 ),
inference(avatar_component_clause,[],[f1104]) ).
fof(f1106,plain,
( e3 = op(e4,e4)
| ~ spl130_11 ),
inference(avatar_component_clause,[],[f1104]) ).
fof(f1108,definition,
( spl130_12
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl130_12])],[avatar_definition]) ).
fof(f1109,plain,
( e3 != op(e3,e3)
| spl130_12 ),
inference(avatar_component_clause,[],[f1108]) ).
fof(f1110,plain,
( e3 = op(e3,e3)
| ~ spl130_12 ),
inference(avatar_component_clause,[],[f1108]) ).
fof(f1112,definition,
( spl130_13
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl130_13])],[avatar_definition]) ).
fof(f1114,plain,
( e3 = op(e2,e2)
| ~ spl130_13 ),
inference(avatar_component_clause,[],[f1112]) ).
fof(f1116,definition,
( spl130_14
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl130_14])],[avatar_definition]) ).
fof(f1118,plain,
( e3 = op(e1,e1)
| ~ spl130_14 ),
inference(avatar_component_clause,[],[f1116]) ).
fof(f1120,definition,
( spl130_15
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl130_15])],[avatar_definition]) ).
fof(f1122,plain,
( op(e0,e0) = e3
| ~ spl130_15 ),
inference(avatar_component_clause,[],[f1120]) ).
fof(f1123,plain,
( spl130_11
| spl130_12
| spl130_13
| spl130_14
| spl130_15 ),
inference(avatar_split_clause,[],[f848,f1120,f1116,f1112,f1108,f1104]) ).
fof(f1125,definition,
( spl130_16
<=> e2 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl130_16])],[avatar_definition]) ).
fof(f1127,plain,
( e2 = op(e4,e4)
| ~ spl130_16 ),
inference(avatar_component_clause,[],[f1125]) ).
fof(f1129,definition,
( spl130_17
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl130_17])],[avatar_definition]) ).
fof(f1131,plain,
( e2 = op(e3,e3)
| ~ spl130_17 ),
inference(avatar_component_clause,[],[f1129]) ).
fof(f1133,definition,
( spl130_18
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl130_18])],[avatar_definition]) ).
fof(f1134,plain,
( e2 != op(e2,e2)
| spl130_18 ),
inference(avatar_component_clause,[],[f1133]) ).
fof(f1135,plain,
( e2 = op(e2,e2)
| ~ spl130_18 ),
inference(avatar_component_clause,[],[f1133]) ).
fof(f1137,definition,
( spl130_19
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl130_19])],[avatar_definition]) ).
fof(f1139,plain,
( e2 = op(e1,e1)
| ~ spl130_19 ),
inference(avatar_component_clause,[],[f1137]) ).
fof(f1141,definition,
( spl130_20
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl130_20])],[avatar_definition]) ).
fof(f1143,plain,
( op(e0,e0) = e2
| ~ spl130_20 ),
inference(avatar_component_clause,[],[f1141]) ).
fof(f1144,plain,
( spl130_16
| spl130_17
| spl130_18
| spl130_19
| spl130_20 ),
inference(avatar_split_clause,[],[f849,f1141,f1137,f1133,f1129,f1125]) ).
fof(f1146,definition,
( spl130_21
<=> e1 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl130_21])],[avatar_definition]) ).
fof(f1147,plain,
( e1 != op(e4,e4)
| spl130_21 ),
inference(avatar_component_clause,[],[f1146]) ).
fof(f1148,plain,
( e1 = op(e4,e4)
| ~ spl130_21 ),
inference(avatar_component_clause,[],[f1146]) ).
fof(f1150,definition,
( spl130_22
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl130_22])],[avatar_definition]) ).
fof(f1152,plain,
( e1 = op(e3,e3)
| ~ spl130_22 ),
inference(avatar_component_clause,[],[f1150]) ).
fof(f1154,definition,
( spl130_23
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl130_23])],[avatar_definition]) ).
fof(f1156,plain,
( e1 = op(e2,e2)
| ~ spl130_23 ),
inference(avatar_component_clause,[],[f1154]) ).
fof(f1158,definition,
( spl130_24
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl130_24])],[avatar_definition]) ).
fof(f1159,plain,
( e1 != op(e1,e1)
| spl130_24 ),
inference(avatar_component_clause,[],[f1158]) ).
fof(f1160,plain,
( e1 = op(e1,e1)
| ~ spl130_24 ),
inference(avatar_component_clause,[],[f1158]) ).
fof(f1162,definition,
( spl130_25
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl130_25])],[avatar_definition]) ).
fof(f1164,plain,
( op(e0,e0) = e1
| ~ spl130_25 ),
inference(avatar_component_clause,[],[f1162]) ).
fof(f1165,plain,
( spl130_21
| spl130_22
| spl130_23
| spl130_24
| spl130_25 ),
inference(avatar_split_clause,[],[f850,f1162,f1158,f1154,f1150,f1146]) ).
fof(f1167,definition,
( spl130_26
<=> e0 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl130_26])],[avatar_definition]) ).
fof(f1168,plain,
( e0 != op(e4,e4)
| spl130_26 ),
inference(avatar_component_clause,[],[f1167]) ).
fof(f1169,plain,
( e0 = op(e4,e4)
| ~ spl130_26 ),
inference(avatar_component_clause,[],[f1167]) ).
fof(f1171,definition,
( spl130_27
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl130_27])],[avatar_definition]) ).
fof(f1172,plain,
( e0 != op(e3,e3)
| spl130_27 ),
inference(avatar_component_clause,[],[f1171]) ).
fof(f1173,plain,
( e0 = op(e3,e3)
| ~ spl130_27 ),
inference(avatar_component_clause,[],[f1171]) ).
fof(f1175,definition,
( spl130_28
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl130_28])],[avatar_definition]) ).
fof(f1177,plain,
( e0 = op(e2,e2)
| ~ spl130_28 ),
inference(avatar_component_clause,[],[f1175]) ).
fof(f1179,definition,
( spl130_29
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl130_29])],[avatar_definition]) ).
fof(f1181,plain,
( e0 = op(e1,e1)
| ~ spl130_29 ),
inference(avatar_component_clause,[],[f1179]) ).
fof(f1183,definition,
( spl130_30
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl130_30])],[avatar_definition]) ).
fof(f1185,plain,
( e0 = op(e0,e0)
| ~ spl130_30 ),
inference(avatar_component_clause,[],[f1183]) ).
fof(f1186,plain,
( spl130_26
| spl130_27
| spl130_28
| spl130_29
| spl130_30 ),
inference(avatar_split_clause,[],[f851,f1183,f1179,f1175,f1171,f1167]) ).
fof(f1192,definition,
( spl130_32
<=> e4 = unit ),
introduced(definition,[new_symbols(definition,[spl130_32])],[avatar_definition]) ).
fof(f1193,plain,
( e4 = unit
| ~ spl130_32 ),
inference(avatar_component_clause,[],[f1192]) ).
fof(f1197,definition,
( spl130_33
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl130_33])],[avatar_definition]) ).
fof(f1201,definition,
( spl130_34
<=> e4 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl130_34])],[avatar_definition]) ).
fof(f1205,plain,
( ~ spl130_33
| spl130_11
| ~ spl130_34 ),
inference(avatar_split_clause,[],[f843,f1201,f1104,f1197]) ).
fof(f1207,definition,
( spl130_35
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl130_35])],[avatar_definition]) ).
fof(f1211,definition,
( spl130_36
<=> e4 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl130_36])],[avatar_definition]) ).
fof(f1215,plain,
( ~ spl130_35
| spl130_16
| ~ spl130_36 ),
inference(avatar_split_clause,[],[f841,f1211,f1125,f1207]) ).
fof(f1227,definition,
( spl130_39
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl130_39])],[avatar_definition]) ).
fof(f1231,definition,
( spl130_40
<=> e4 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl130_40])],[avatar_definition]) ).
fof(f1235,plain,
( spl130_39
| spl130_26
| ~ spl130_40 ),
inference(avatar_split_clause,[],[f1054,f1231,f1167,f1227]) ).
fof(f1396,definition,
( spl130_75
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl130_75])],[avatar_definition]) ).
fof(f1399,plain,
( spl130_75
| ~ spl130_32
| ~ spl130_9 ),
inference(avatar_split_clause,[],[f1035,f1095,f1192,f1396]) ).
fof(f1485,definition,
( spl130_94
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl130_94])],[avatar_definition]) ).
fof(f1486,plain,
( e3 = unit
| ~ spl130_94 ),
inference(avatar_component_clause,[],[f1485]) ).
fof(f1548,definition,
( spl130_107
<=> sP31 ),
introduced(definition,[new_symbols(definition,[spl130_107])],[avatar_definition]) ).
fof(f1551,plain,
( ~ spl130_107
| ~ spl130_94
| ~ spl130_12 ),
inference(avatar_split_clause,[],[f782,f1108,f1485,f1548]) ).
fof(f1553,definition,
( spl130_108
<=> sP32 ),
introduced(definition,[new_symbols(definition,[spl130_108])],[avatar_definition]) ).
fof(f1557,definition,
( spl130_109
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl130_109])],[avatar_definition]) ).
fof(f1561,plain,
( spl130_108
| spl130_17
| ~ spl130_109 ),
inference(avatar_split_clause,[],[f1018,f1557,f1129,f1553]) ).
fof(f1573,definition,
( spl130_112
<=> sP34 ),
introduced(definition,[new_symbols(definition,[spl130_112])],[avatar_definition]) ).
fof(f1577,definition,
( spl130_113
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl130_113])],[avatar_definition]) ).
fof(f1581,plain,
( ~ spl130_112
| spl130_27
| ~ spl130_113 ),
inference(avatar_split_clause,[],[f777,f1577,f1171,f1573]) ).
fof(f1603,definition,
( spl130_118
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl130_118])],[avatar_definition]) ).
fof(f1670,definition,
( spl130_132
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl130_132])],[avatar_definition]) ).
fof(f1737,definition,
( spl130_146
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl130_146])],[avatar_definition]) ).
fof(f1746,definition,
( spl130_148
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl130_148])],[avatar_definition]) ).
fof(f1747,plain,
( e2 = unit
| ~ spl130_148 ),
inference(avatar_component_clause,[],[f1746]) ).
fof(f1850,definition,
( spl130_169
<=> sP61 ),
introduced(definition,[new_symbols(definition,[spl130_169])],[avatar_definition]) ).
fof(f1854,plain,
( spl130_169
| spl130_13
| ~ spl130_118 ),
inference(avatar_split_clause,[],[f988,f1603,f1112,f1850]) ).
fof(f1856,definition,
( spl130_170
<=> sP62 ),
introduced(definition,[new_symbols(definition,[spl130_170])],[avatar_definition]) ).
fof(f1859,plain,
( ~ spl130_170
| ~ spl130_148
| ~ spl130_18 ),
inference(avatar_split_clause,[],[f720,f1133,f1746,f1856]) ).
fof(f1871,definition,
( spl130_173
<=> sP64 ),
introduced(definition,[new_symbols(definition,[spl130_173])],[avatar_definition]) ).
fof(f1875,definition,
( spl130_174
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl130_174])],[avatar_definition]) ).
fof(f1879,plain,
( spl130_173
| spl130_28
| ~ spl130_174 ),
inference(avatar_split_clause,[],[f986,f1875,f1175,f1871]) ).
fof(f1907,definition,
( spl130_180
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl130_180])],[avatar_definition]) ).
fof(f1966,definition,
( spl130_192
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl130_192])],[avatar_definition]) ).
fof(f1975,definition,
( spl130_194
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl130_194])],[avatar_definition]) ).
fof(f1976,plain,
( e1 = unit
| ~ spl130_194 ),
inference(avatar_component_clause,[],[f1975]) ).
fof(f2104,definition,
( spl130_219
<=> sP91 ),
introduced(definition,[new_symbols(definition,[spl130_219])],[avatar_definition]) ).
fof(f2108,plain,
( ~ spl130_219
| spl130_14
| ~ spl130_132 ),
inference(avatar_split_clause,[],[f663,f1670,f1116,f2104]) ).
fof(f2110,definition,
( spl130_220
<=> sP92 ),
introduced(definition,[new_symbols(definition,[spl130_220])],[avatar_definition]) ).
fof(f2114,plain,
( ~ spl130_220
| spl130_19
| ~ spl130_180 ),
inference(avatar_split_clause,[],[f661,f1907,f1137,f2110]) ).
fof(f2121,definition,
( spl130_222
<=> sP94 ),
introduced(definition,[new_symbols(definition,[spl130_222])],[avatar_definition]) ).
fof(f2125,definition,
( spl130_223
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl130_223])],[avatar_definition]) ).
fof(f2129,plain,
( ~ spl130_222
| spl130_29
| ~ spl130_223 ),
inference(avatar_split_clause,[],[f657,f2125,f1179,f2121]) ).
fof(f2172,definition,
( spl130_232
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl130_232])],[avatar_definition]) ).
fof(f2173,plain,
( e0 = unit
| ~ spl130_232 ),
inference(avatar_component_clause,[],[f2172]) ).
fof(f2310,definition,
( spl130_257
<=> sP121 ),
introduced(definition,[new_symbols(definition,[spl130_257])],[avatar_definition]) ).
fof(f2314,plain,
( ~ spl130_257
| spl130_15
| ~ spl130_146 ),
inference(avatar_split_clause,[],[f603,f1737,f1120,f2310]) ).
fof(f2316,definition,
( spl130_258
<=> sP122 ),
introduced(definition,[new_symbols(definition,[spl130_258])],[avatar_definition]) ).
fof(f2320,plain,
( ~ spl130_258
| spl130_20
| ~ spl130_192 ),
inference(avatar_split_clause,[],[f601,f1966,f1141,f2316]) ).
fof(f2328,definition,
( spl130_260
<=> sP124 ),
introduced(definition,[new_symbols(definition,[spl130_260])],[avatar_definition]) ).
fof(f2331,plain,
( spl130_260
| ~ spl130_232
| ~ spl130_30 ),
inference(avatar_split_clause,[],[f947,f1183,f2172,f2328]) ).
fof(f2333,plain,
( spl130_1
| spl130_33 ),
inference(avatar_split_clause,[],[f944,f1197,f1062]) ).
fof(f2334,plain,
( spl130_1
| spl130_35 ),
inference(avatar_split_clause,[],[f943,f1207,f1062]) ).
fof(f2336,plain,
( spl130_1
| ~ spl130_39 ),
inference(avatar_split_clause,[],[f941,f1227,f1062]) ).
fof(f2350,plain,
( spl130_1
| ~ spl130_75 ),
inference(avatar_split_clause,[],[f927,f1396,f1062]) ).
fof(f2363,plain,
( spl130_2
| spl130_107 ),
inference(avatar_split_clause,[],[f914,f1548,f1066]) ).
fof(f2364,plain,
( spl130_2
| ~ spl130_108 ),
inference(avatar_split_clause,[],[f913,f1553,f1066]) ).
fof(f2366,plain,
( spl130_2
| spl130_112 ),
inference(avatar_split_clause,[],[f911,f1573,f1066]) ).
fof(f2393,plain,
( ~ spl130_3
| ~ spl130_169 ),
inference(avatar_split_clause,[],[f890,f1850,f1070]) ).
fof(f2394,plain,
( ~ spl130_3
| spl130_170 ),
inference(avatar_split_clause,[],[f533,f1856,f1070]) ).
fof(f2396,plain,
( ~ spl130_3
| ~ spl130_173 ),
inference(avatar_split_clause,[],[f889,f1871,f1070]) ).
fof(f2423,plain,
( ~ spl130_4
| spl130_219 ),
inference(avatar_split_clause,[],[f512,f2104,f1074]) ).
fof(f2424,plain,
( ~ spl130_4
| spl130_220 ),
inference(avatar_split_clause,[],[f513,f2110,f1074]) ).
fof(f2426,plain,
( ~ spl130_4
| spl130_222 ),
inference(avatar_split_clause,[],[f515,f2121,f1074]) ).
fof(f2453,plain,
( spl130_5
| spl130_257 ),
inference(avatar_split_clause,[],[f855,f2310,f1078]) ).
fof(f2454,plain,
( spl130_5
| spl130_258 ),
inference(avatar_split_clause,[],[f854,f2316,f1078]) ).
fof(f2456,plain,
( spl130_5
| ~ spl130_260 ),
inference(avatar_split_clause,[],[f852,f2328,f1078]) ).
fof(f2457,plain,
spl130_9,
inference(avatar_split_clause,[],[f467,f1095]) ).
fof(f2508,plain,
( spl130_32
| spl130_94
| spl130_148
| spl130_194
| spl130_232 ),
inference(avatar_split_clause,[],[f296,f2172,f1975,f1746,f1485,f1192]) ).
fof(f2535,plain,
( e3 = e4
| ~ spl130_6
| ~ spl130_11 ),
inference(superposition,[],[f1085,f1106]) ).
fof(f2536,plain,
( e3 = op(e3,e3)
| ~ spl130_6
| ~ spl130_11 ),
inference(superposition,[],[f1106,f2535]) ).
fof(f2541,plain,
( e3 = e4
| ~ spl130_9
| ~ spl130_14 ),
inference(superposition,[],[f1097,f1118]) ).
fof(f2549,plain,
( e2 = e3
| ~ spl130_11
| ~ spl130_16 ),
inference(superposition,[],[f1106,f1127]) ).
fof(f2550,plain,
( e2 = e4
| ~ spl130_6
| ~ spl130_16 ),
inference(superposition,[],[f1085,f1127]) ).
fof(f2552,plain,
( e2 = e3
| ~ spl130_12
| ~ spl130_17 ),
inference(superposition,[],[f1110,f1131]) ).
fof(f2561,plain,
( e2 = op(e2,e2)
| ~ spl130_6
| ~ spl130_16 ),
inference(superposition,[],[f1085,f2550]) ).
fof(f2562,plain,
( e2 = e3
| ~ spl130_13
| ~ spl130_18 ),
inference(superposition,[],[f1135,f1114]) ).
fof(f2566,plain,
( e2 = e4
| ~ spl130_9
| ~ spl130_19 ),
inference(superposition,[],[f1139,f1097]) ).
fof(f2574,plain,
( e1 = e2
| ~ spl130_16
| ~ spl130_21 ),
inference(superposition,[],[f1127,f1148]) ).
fof(f2575,plain,
( e1 = e3
| ~ spl130_11
| ~ spl130_21 ),
inference(superposition,[],[f1106,f1148]) ).
fof(f2576,plain,
( e1 = e4
| ~ spl130_6
| ~ spl130_21 ),
inference(superposition,[],[f1085,f1148]) ).
fof(f2591,plain,
( e1 = op(e1,e1)
| ~ spl130_6
| ~ spl130_21 ),
inference(superposition,[],[f1148,f2576]) ).
fof(f2611,plain,
( e1 = e2
| ~ spl130_17
| ~ spl130_22 ),
inference(superposition,[],[f1131,f1152]) ).
fof(f2612,plain,
( e1 = e3
| ~ spl130_12
| ~ spl130_22 ),
inference(superposition,[],[f1110,f1152]) ).
fof(f2618,plain,
( e1 = e2
| ~ spl130_18
| ~ spl130_23 ),
inference(superposition,[],[f1135,f1156]) ).
fof(f2619,plain,
( e1 = e3
| ~ spl130_13
| ~ spl130_23 ),
inference(superposition,[],[f1114,f1156]) ).
fof(f2625,plain,
( e1 = e4
| ~ spl130_9
| ~ spl130_24 ),
inference(superposition,[],[f1097,f1160]) ).
fof(f2669,plain,
( e1 = op(e1,e1)
| ~ spl130_12
| ~ spl130_22 ),
inference(superposition,[],[f1110,f2612]) ).
fof(f2686,plain,
( spl130_24
| ~ spl130_12
| ~ spl130_22 ),
inference(avatar_split_clause,[],[f2669,f1150,f1108,f1158]) ).
fof(f2688,plain,
( e1 = op(e1,e1)
| ~ spl130_18
| ~ spl130_23 ),
inference(superposition,[],[f1135,f2618]) ).
fof(f2689,plain,
( spl130_24
| ~ spl130_18
| ~ spl130_23 ),
inference(avatar_split_clause,[],[f2688,f1154,f1133,f1158]) ).
fof(f2693,plain,
( spl130_18
| ~ spl130_6
| ~ spl130_16 ),
inference(avatar_split_clause,[],[f2561,f1125,f1083,f1133]) ).
fof(f2738,plain,
( e0 = e4
| ~ spl130_9
| ~ spl130_29 ),
inference(superposition,[],[f1097,f1181]) ).
fof(f2749,plain,
( e0 = op(e0,e0)
| ~ spl130_6
| ~ spl130_9
| ~ spl130_29 ),
inference(superposition,[],[f1085,f2738]) ).
fof(f2750,plain,
( op(e0,e0) = e3
| ~ spl130_9
| ~ spl130_11
| ~ spl130_29 ),
inference(superposition,[],[f1106,f2738]) ).
fof(f2751,plain,
( op(e0,e0) = e2
| ~ spl130_9
| ~ spl130_16
| ~ spl130_29 ),
inference(superposition,[],[f1127,f2738]) ).
fof(f2752,plain,
( op(e0,e0) != e1
| ~ spl130_9
| spl130_21
| ~ spl130_29 ),
inference(superposition,[],[f1147,f2738]) ).
fof(f2753,plain,
( e0 != op(e0,e0)
| ~ spl130_9
| spl130_26
| ~ spl130_29 ),
inference(superposition,[],[f1168,f2738]) ).
fof(f2756,plain,
( ~ spl130_30
| ~ spl130_9
| spl130_26
| ~ spl130_29 ),
inference(avatar_split_clause,[],[f2753,f1179,f1167,f1095,f1183]) ).
fof(f2757,plain,
( ~ spl130_25
| ~ spl130_9
| spl130_21
| ~ spl130_29 ),
inference(avatar_split_clause,[],[f2752,f1179,f1146,f1095,f1162]) ).
fof(f2758,plain,
( spl130_20
| ~ spl130_9
| ~ spl130_16
| ~ spl130_29 ),
inference(avatar_split_clause,[],[f2751,f1179,f1125,f1095,f1141]) ).
fof(f2759,plain,
( spl130_15
| ~ spl130_9
| ~ spl130_11
| ~ spl130_29 ),
inference(avatar_split_clause,[],[f2750,f1179,f1104,f1095,f1120]) ).
fof(f2763,plain,
( e0 = e1
| ~ spl130_25
| ~ spl130_30 ),
inference(superposition,[],[f1164,f1185]) ).
fof(f2769,plain,
( e0 != op(e0,e0)
| spl130_24
| ~ spl130_25
| ~ spl130_30 ),
inference(superposition,[],[f1159,f2763]) ).
fof(f2773,plain,
( ~ spl130_30
| spl130_24
| ~ spl130_25
| ~ spl130_30 ),
inference(avatar_split_clause,[],[f2769,f1183,f1162,f1158,f1183]) ).
fof(f2805,plain,
( e0 = e2
| ~ spl130_17
| ~ spl130_27 ),
inference(superposition,[],[f1131,f1173]) ).
fof(f2806,plain,
( e0 = e3
| ~ spl130_12
| ~ spl130_27 ),
inference(superposition,[],[f1110,f1173]) ).
fof(f2824,plain,
( e1 = e3
| ~ spl130_15
| ~ spl130_25 ),
inference(superposition,[],[f1164,f1122]) ).
fof(f2858,plain,
( e0 = e4
| ~ spl130_6
| ~ spl130_26 ),
inference(superposition,[],[f1085,f1169]) ).
fof(f2863,plain,
( e0 = op(e0,e0)
| ~ spl130_6
| ~ spl130_26 ),
inference(superposition,[],[f1169,f2858]) ).
fof(f2864,plain,
( spl130_30
| ~ spl130_6
| ~ spl130_26 ),
inference(avatar_split_clause,[],[f2863,f1167,f1083,f1183]) ).
fof(f2872,plain,
( e2 != e2
| ~ spl130_12
| ~ spl130_17 ),
inference(superposition,[],[f459,f2552]) ).
fof(f2873,plain,
( $false
| ~ spl130_12
| ~ spl130_17 ),
inference(trivial_inequality_removal,[],[f2872]) ).
fof(f2874,plain,
( ~ spl130_12
| ~ spl130_17 ),
inference(avatar_contradiction_clause,[],[f2873]) ).
fof(f2875,plain,
( e3 != e3
| ~ spl130_9
| ~ spl130_14 ),
inference(superposition,[],[f457,f2541]) ).
fof(f2882,plain,
( $false
| ~ spl130_9
| ~ spl130_14 ),
inference(trivial_inequality_removal,[],[f2875]) ).
fof(f2883,plain,
( ~ spl130_9
| ~ spl130_14 ),
inference(avatar_contradiction_clause,[],[f2882]) ).
fof(f2888,plain,
( e0 = e3
| ~ spl130_11
| ~ spl130_26 ),
inference(superposition,[],[f1169,f1106]) ).
fof(f2925,plain,
( e0 = e2
| ~ spl130_18
| ~ spl130_28 ),
inference(superposition,[],[f1135,f1177]) ).
fof(f2935,plain,
( e2 != e2
| ~ spl130_9
| ~ spl130_19 ),
inference(superposition,[],[f458,f2566]) ).
fof(f2940,plain,
( $false
| ~ spl130_9
| ~ spl130_19 ),
inference(trivial_inequality_removal,[],[f2935]) ).
fof(f2941,plain,
( ~ spl130_9
| ~ spl130_19 ),
inference(avatar_contradiction_clause,[],[f2940]) ).
fof(f2956,plain,
( e0 = e3
| ~ spl130_15
| ~ spl130_30 ),
inference(superposition,[],[f1122,f1185]) ).
fof(f2961,plain,
( e0 != op(e0,e0)
| spl130_12
| ~ spl130_15
| ~ spl130_30 ),
inference(superposition,[],[f1109,f2956]) ).
fof(f2964,plain,
( e0 != op(e0,e0)
| ~ spl130_15
| spl130_27
| ~ spl130_30 ),
inference(superposition,[],[f1172,f2956]) ).
fof(f2965,plain,
( ~ spl130_30
| ~ spl130_15
| spl130_27
| ~ spl130_30 ),
inference(avatar_split_clause,[],[f2964,f1183,f1171,f1120,f1183]) ).
fof(f2967,plain,
( ~ spl130_30
| spl130_12
| ~ spl130_15
| ~ spl130_30 ),
inference(avatar_split_clause,[],[f2961,f1183,f1120,f1108,f1183]) ).
fof(f2971,plain,
( op(e0,e0) != e3
| ~ spl130_9
| spl130_11
| ~ spl130_29 ),
inference(superposition,[],[f1105,f2738]) ).
fof(f2973,plain,
( op(e0,e0) = e1
| ~ spl130_9
| ~ spl130_21
| ~ spl130_29 ),
inference(superposition,[],[f1148,f2738]) ).
fof(f2975,plain,
( spl130_25
| ~ spl130_9
| ~ spl130_21
| ~ spl130_29 ),
inference(avatar_split_clause,[],[f2973,f1179,f1146,f1095,f1162]) ).
fof(f2976,plain,
( ~ spl130_15
| ~ spl130_9
| spl130_11
| ~ spl130_29 ),
inference(avatar_split_clause,[],[f2971,f1179,f1104,f1095,f1120]) ).
fof(f2978,plain,
( e0 = e1
| ~ spl130_21
| ~ spl130_26 ),
inference(superposition,[],[f1148,f1169]) ).
fof(f3005,plain,
( e2 = op(e2,e2)
| ~ spl130_148 ),
inference(superposition,[],[f301,f1747]) ).
fof(f3006,plain,
( spl130_18
| ~ spl130_148 ),
inference(avatar_split_clause,[],[f3005,f1746,f1133]) ).
fof(f3007,plain,
( e4 = op(e4,e3)
| ~ spl130_94 ),
inference(superposition,[],[f297,f1486]) ).
fof(f3010,plain,
( e3 = op(e3,e3)
| ~ spl130_94 ),
inference(superposition,[],[f300,f1486]) ).
fof(f3015,plain,
( spl130_12
| ~ spl130_94 ),
inference(avatar_split_clause,[],[f3010,f1485,f1108]) ).
fof(f3016,plain,
( spl130_34
| ~ spl130_94 ),
inference(avatar_split_clause,[],[f3007,f1485,f1201]) ).
fof(f3033,plain,
( e4 = op(e4,e4)
| ~ spl130_32 ),
inference(superposition,[],[f298,f1193]) ).
fof(f3042,plain,
( spl130_6
| ~ spl130_32 ),
inference(avatar_split_clause,[],[f3033,f1192,f1083]) ).
fof(f3057,plain,
( e1 = op(e1,e1)
| ~ spl130_194 ),
inference(superposition,[],[f303,f1976]) ).
fof(f3058,plain,
( spl130_24
| ~ spl130_194 ),
inference(avatar_split_clause,[],[f3057,f1975,f1158]) ).
fof(f3061,plain,
( e3 = op(e3,e0)
| ~ spl130_232 ),
inference(superposition,[],[f299,f2173]) ).
fof(f3063,plain,
( e2 = op(e2,e0)
| ~ spl130_232 ),
inference(superposition,[],[f301,f2173]) ).
fof(f3065,plain,
( e1 = op(e1,e0)
| ~ spl130_232 ),
inference(superposition,[],[f303,f2173]) ).
fof(f3070,plain,
( spl130_223
| ~ spl130_232 ),
inference(avatar_split_clause,[],[f3065,f2172,f2125]) ).
fof(f3072,plain,
( spl130_174
| ~ spl130_232 ),
inference(avatar_split_clause,[],[f3063,f2172,f1875]) ).
fof(f3074,plain,
( spl130_113
| ~ spl130_232 ),
inference(avatar_split_clause,[],[f3061,f2172,f1577]) ).
fof(f3078,plain,
( e0 = op(e0,e0)
| ~ spl130_232 ),
inference(superposition,[],[f305,f2173]) ).
fof(f3079,plain,
( spl130_30
| ~ spl130_232 ),
inference(avatar_split_clause,[],[f3078,f2172,f1183]) ).
fof(f3083,plain,
( e1 != e1
| ~ spl130_13
| ~ spl130_23 ),
inference(superposition,[],[f461,f2619]) ).
fof(f3090,plain,
( $false
| ~ spl130_13
| ~ spl130_23 ),
inference(trivial_inequality_removal,[],[f3083]) ).
fof(f3091,plain,
( ~ spl130_13
| ~ spl130_23 ),
inference(avatar_contradiction_clause,[],[f3090]) ).
fof(f3096,plain,
( e1 != e1
| ~ spl130_17
| ~ spl130_22 ),
inference(superposition,[],[f462,f2611]) ).
fof(f3101,plain,
( $false
| ~ spl130_17
| ~ spl130_22 ),
inference(trivial_inequality_removal,[],[f3096]) ).
fof(f3102,plain,
( ~ spl130_17
| ~ spl130_22 ),
inference(avatar_contradiction_clause,[],[f3101]) ).
fof(f3109,plain,
( e1 != e1
| ~ spl130_9
| ~ spl130_24 ),
inference(superposition,[],[f460,f2625]) ).
fof(f3115,plain,
( $false
| ~ spl130_9
| ~ spl130_24 ),
inference(trivial_inequality_removal,[],[f3109]) ).
fof(f3116,plain,
( ~ spl130_9
| ~ spl130_24 ),
inference(avatar_contradiction_clause,[],[f3115]) ).
fof(f3125,plain,
( e0 != e0
| ~ spl130_17
| ~ spl130_27 ),
inference(superposition,[],[f465,f2805]) ).
fof(f3127,plain,
( e0 != op(e0,e0)
| ~ spl130_17
| spl130_18
| ~ spl130_27 ),
inference(superposition,[],[f1134,f2805]) ).
fof(f3128,plain,
( $false
| ~ spl130_17
| ~ spl130_27 ),
inference(trivial_inequality_removal,[],[f3125]) ).
fof(f3129,plain,
( ~ spl130_17
| ~ spl130_27 ),
inference(avatar_contradiction_clause,[],[f3128]) ).
fof(f3130,plain,
( ~ spl130_30
| ~ spl130_17
| spl130_18
| ~ spl130_27 ),
inference(avatar_split_clause,[],[f3127,f1171,f1133,f1129,f1183]) ).
fof(f3145,plain,
( e0 = e1
| ~ spl130_23
| ~ spl130_28 ),
inference(superposition,[],[f1156,f1177]) ).
fof(f3151,plain,
( e0 != e0
| ~ spl130_23
| ~ spl130_28 ),
inference(superposition,[],[f466,f3145]) ).
fof(f3155,plain,
( e0 != op(e0,e0)
| ~ spl130_23
| spl130_24
| ~ spl130_28 ),
inference(superposition,[],[f1159,f3145]) ).
fof(f3157,plain,
( $false
| ~ spl130_23
| ~ spl130_28 ),
inference(trivial_inequality_removal,[],[f3151]) ).
fof(f3158,plain,
( ~ spl130_23
| ~ spl130_28 ),
inference(avatar_contradiction_clause,[],[f3157]) ).
fof(f3160,plain,
( ~ spl130_30
| ~ spl130_23
| spl130_24
| ~ spl130_28 ),
inference(avatar_split_clause,[],[f3155,f1175,f1158,f1154,f1183]) ).
fof(f3165,plain,
( e0 = e2
| ~ spl130_20
| ~ spl130_30 ),
inference(superposition,[],[f1143,f1185]) ).
fof(f3172,plain,
( e0 != e0
| ~ spl130_20
| ~ spl130_30 ),
inference(superposition,[],[f465,f3165]) ).
fof(f3178,plain,
( $false
| ~ spl130_20
| ~ spl130_30 ),
inference(trivial_inequality_removal,[],[f3172]) ).
fof(f3179,plain,
( ~ spl130_20
| ~ spl130_30 ),
inference(avatar_contradiction_clause,[],[f3178]) ).
fof(f3186,plain,
( e0 = e2
| ~ spl130_16
| ~ spl130_26 ),
inference(superposition,[],[f1169,f1127]) ).
fof(f3191,plain,
( e0 != e0
| ~ spl130_16
| ~ spl130_26 ),
inference(superposition,[],[f465,f3186]) ).
fof(f3197,plain,
( $false
| ~ spl130_16
| ~ spl130_26 ),
inference(trivial_inequality_removal,[],[f3191]) ).
fof(f3198,plain,
( ~ spl130_16
| ~ spl130_26 ),
inference(avatar_contradiction_clause,[],[f3197]) ).
fof(f3211,plain,
( e2 = op(e2,e3)
| ~ spl130_94 ),
inference(superposition,[],[f301,f1486]) ).
fof(f3213,plain,
( e1 = op(e1,e3)
| ~ spl130_94 ),
inference(superposition,[],[f303,f1486]) ).
fof(f3215,plain,
( e0 = op(e0,e3)
| ~ spl130_94 ),
inference(superposition,[],[f305,f1486]) ).
fof(f3220,plain,
( spl130_118
| ~ spl130_94 ),
inference(avatar_split_clause,[],[f3211,f1485,f1603]) ).
fof(f3222,plain,
( spl130_146
| ~ spl130_94 ),
inference(avatar_split_clause,[],[f3215,f1485,f1737]) ).
fof(f3223,plain,
( spl130_132
| ~ spl130_94 ),
inference(avatar_split_clause,[],[f3213,f1485,f1670]) ).
fof(f3226,plain,
( e2 = e3
| ~ spl130_15
| ~ spl130_20 ),
inference(superposition,[],[f1143,f1122]) ).
fof(f3231,plain,
( e2 != e2
| ~ spl130_15
| ~ spl130_20 ),
inference(superposition,[],[f459,f3226]) ).
fof(f3235,plain,
( e2 = op(e2,e2)
| ~ spl130_12
| ~ spl130_15
| ~ spl130_20 ),
inference(superposition,[],[f1110,f3226]) ).
fof(f3239,plain,
( $false
| ~ spl130_15
| ~ spl130_20 ),
inference(trivial_inequality_removal,[],[f3231]) ).
fof(f3240,plain,
( ~ spl130_15
| ~ spl130_20 ),
inference(avatar_contradiction_clause,[],[f3239]) ).
fof(f3242,plain,
( spl130_18
| ~ spl130_12
| ~ spl130_15
| ~ spl130_20 ),
inference(avatar_split_clause,[],[f3235,f1141,f1120,f1108,f1133]) ).
fof(f3248,plain,
( e0 != e0
| ~ spl130_11
| ~ spl130_26 ),
inference(superposition,[],[f464,f2888]) ).
fof(f3254,plain,
( $false
| ~ spl130_11
| ~ spl130_26 ),
inference(trivial_inequality_removal,[],[f3248]) ).
fof(f3255,plain,
( ~ spl130_11
| ~ spl130_26 ),
inference(avatar_contradiction_clause,[],[f3254]) ).
fof(f3260,plain,
( e0 != e0
| ~ spl130_21
| ~ spl130_26 ),
inference(superposition,[],[f466,f2978]) ).
fof(f3266,plain,
( $false
| ~ spl130_21
| ~ spl130_26 ),
inference(trivial_inequality_removal,[],[f3260]) ).
fof(f3267,plain,
( ~ spl130_21
| ~ spl130_26 ),
inference(avatar_contradiction_clause,[],[f3266]) ).
fof(f3299,plain,
( e4 = op(e4,e2)
| ~ spl130_148 ),
inference(superposition,[],[f297,f1747]) ).
fof(f3301,plain,
( e3 = op(e3,e2)
| ~ spl130_148 ),
inference(superposition,[],[f299,f1747]) ).
fof(f3305,plain,
( e1 = op(e1,e2)
| ~ spl130_148 ),
inference(superposition,[],[f303,f1747]) ).
fof(f3307,plain,
( e0 = op(e0,e2)
| ~ spl130_148 ),
inference(superposition,[],[f305,f1747]) ).
fof(f3312,plain,
( spl130_109
| ~ spl130_148 ),
inference(avatar_split_clause,[],[f3301,f1746,f1557]) ).
fof(f3313,plain,
( spl130_36
| ~ spl130_148 ),
inference(avatar_split_clause,[],[f3299,f1746,f1211]) ).
fof(f3314,plain,
( spl130_192
| ~ spl130_148 ),
inference(avatar_split_clause,[],[f3307,f1746,f1966]) ).
fof(f3315,plain,
( spl130_180
| ~ spl130_148 ),
inference(avatar_split_clause,[],[f3305,f1746,f1907]) ).
fof(f3324,plain,
( e1 = e2
| ~ spl130_20
| ~ spl130_25 ),
inference(superposition,[],[f1143,f1164]) ).
fof(f3330,plain,
( e1 != e1
| ~ spl130_20
| ~ spl130_25 ),
inference(superposition,[],[f462,f3324]) ).
fof(f3337,plain,
( $false
| ~ spl130_20
| ~ spl130_25 ),
inference(trivial_inequality_removal,[],[f3330]) ).
fof(f3338,plain,
( ~ spl130_20
| ~ spl130_25 ),
inference(avatar_contradiction_clause,[],[f3337]) ).
fof(f3343,plain,
( e2 != e2
| ~ spl130_13
| ~ spl130_18 ),
inference(superposition,[],[f459,f2562]) ).
fof(f3351,plain,
( $false
| ~ spl130_13
| ~ spl130_18 ),
inference(trivial_inequality_removal,[],[f3343]) ).
fof(f3352,plain,
( ~ spl130_13
| ~ spl130_18 ),
inference(avatar_contradiction_clause,[],[f3351]) ).
fof(f3370,plain,
( e0 != e0
| ~ spl130_12
| ~ spl130_27 ),
inference(superposition,[],[f464,f2806]) ).
fof(f3375,plain,
( $false
| ~ spl130_12
| ~ spl130_27 ),
inference(trivial_inequality_removal,[],[f3370]) ).
fof(f3376,plain,
( ~ spl130_12
| ~ spl130_27 ),
inference(avatar_contradiction_clause,[],[f3375]) ).
fof(f3379,plain,
( spl130_24
| ~ spl130_6
| ~ spl130_21 ),
inference(avatar_split_clause,[],[f2591,f1146,f1083,f1158]) ).
fof(f3383,plain,
( e1 != e1
| ~ spl130_15
| ~ spl130_25 ),
inference(superposition,[],[f461,f2824]) ).
fof(f3387,plain,
( $false
| ~ spl130_15
| ~ spl130_25 ),
inference(trivial_inequality_removal,[],[f3383]) ).
fof(f3388,plain,
( ~ spl130_15
| ~ spl130_25 ),
inference(avatar_contradiction_clause,[],[f3387]) ).
fof(f3413,plain,
( e0 = e1
| ~ spl130_22
| ~ spl130_27 ),
inference(superposition,[],[f1152,f1173]) ).
fof(f3419,plain,
( e0 != e0
| ~ spl130_22
| ~ spl130_27 ),
inference(superposition,[],[f466,f3413]) ).
fof(f3425,plain,
( $false
| ~ spl130_22
| ~ spl130_27 ),
inference(trivial_inequality_removal,[],[f3419]) ).
fof(f3426,plain,
( ~ spl130_22
| ~ spl130_27 ),
inference(avatar_contradiction_clause,[],[f3425]) ).
fof(f3432,plain,
( e1 != e1
| ~ spl130_11
| ~ spl130_21 ),
inference(superposition,[],[f461,f2575]) ).
fof(f3438,plain,
( $false
| ~ spl130_11
| ~ spl130_21 ),
inference(trivial_inequality_removal,[],[f3432]) ).
fof(f3439,plain,
( ~ spl130_11
| ~ spl130_21 ),
inference(avatar_contradiction_clause,[],[f3438]) ).
fof(f3442,plain,
( spl130_12
| ~ spl130_6
| ~ spl130_11 ),
inference(avatar_split_clause,[],[f2536,f1104,f1083,f1108]) ).
fof(f3444,plain,
( spl130_30
| ~ spl130_6
| ~ spl130_9
| ~ spl130_29 ),
inference(avatar_split_clause,[],[f2749,f1179,f1095,f1083,f1183]) ).
fof(f3447,plain,
( e2 != e2
| ~ spl130_11
| ~ spl130_16 ),
inference(superposition,[],[f459,f2549]) ).
fof(f3453,plain,
( $false
| ~ spl130_11
| ~ spl130_16 ),
inference(trivial_inequality_removal,[],[f3447]) ).
fof(f3454,plain,
( ~ spl130_11
| ~ spl130_16 ),
inference(avatar_contradiction_clause,[],[f3453]) ).
fof(f3470,plain,
( e4 = op(e4,e0)
| ~ spl130_232 ),
inference(superposition,[],[f297,f2173]) ).
fof(f3483,plain,
( spl130_40
| ~ spl130_232 ),
inference(avatar_split_clause,[],[f3470,f2172,f1231]) ).
fof(f3487,plain,
( e0 != e0
| ~ spl130_18
| ~ spl130_28 ),
inference(superposition,[],[f465,f2925]) ).
fof(f3492,plain,
( $false
| ~ spl130_18
| ~ spl130_28 ),
inference(trivial_inequality_removal,[],[f3487]) ).
fof(f3493,plain,
( ~ spl130_18
| ~ spl130_28 ),
inference(avatar_contradiction_clause,[],[f3492]) ).
fof(f3496,plain,
( e1 != e1
| ~ spl130_16
| ~ spl130_21 ),
inference(superposition,[],[f462,f2574]) ).
fof(f3500,plain,
( $false
| ~ spl130_16
| ~ spl130_21 ),
inference(trivial_inequality_removal,[],[f3496]) ).
fof(f3501,plain,
( ~ spl130_16
| ~ spl130_21 ),
inference(avatar_contradiction_clause,[],[f3500]) ).
fof(f3515,plain,
( e0 = e3
| ~ spl130_13
| ~ spl130_28 ),
inference(superposition,[],[f1114,f1177]) ).
fof(f3522,plain,
( e0 != e0
| ~ spl130_13
| ~ spl130_28 ),
inference(superposition,[],[f464,f3515]) ).
fof(f3528,plain,
( $false
| ~ spl130_13
| ~ spl130_28 ),
inference(trivial_inequality_removal,[],[f3522]) ).
fof(f3529,plain,
( ~ spl130_13
| ~ spl130_28 ),
inference(avatar_contradiction_clause,[],[f3528]) ).
cnf(s1,plain,
( ~ spl130_1
| ~ spl130_2
| spl130_3
| spl130_4
| ~ spl130_5 ),
inference(sat_conversion,[],[f1081]) ).
cnf(s3,plain,
( spl130_11
| spl130_12
| spl130_13
| spl130_14
| spl130_15 ),
inference(sat_conversion,[],[f1123]) ).
cnf(s4,plain,
( spl130_16
| spl130_17
| spl130_18
| spl130_19
| spl130_20 ),
inference(sat_conversion,[],[f1144]) ).
cnf(s5,plain,
( spl130_21
| spl130_22
| spl130_23
| spl130_24
| spl130_25 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s6,plain,
( spl130_26
| spl130_27
| spl130_28
| spl130_29
| spl130_30 ),
inference(sat_conversion,[],[f1186]) ).
cnf(s9,plain,
( spl130_11
| ~ spl130_33
| ~ spl130_34 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s11,plain,
( spl130_16
| ~ spl130_35
| ~ spl130_36 ),
inference(sat_conversion,[],[f1215]) ).
cnf(s15,plain,
( spl130_26
| spl130_39
| ~ spl130_40 ),
inference(sat_conversion,[],[f1235]) ).
cnf(s39,plain,
( ~ spl130_9
| ~ spl130_32
| spl130_75 ),
inference(sat_conversion,[],[f1399]) ).
cnf(s63,plain,
( ~ spl130_12
| ~ spl130_94
| ~ spl130_107 ),
inference(sat_conversion,[],[f1551]) ).
cnf(s65,plain,
( spl130_17
| spl130_108
| ~ spl130_109 ),
inference(sat_conversion,[],[f1561]) ).
cnf(s69,plain,
( spl130_27
| ~ spl130_112
| ~ spl130_113 ),
inference(sat_conversion,[],[f1581]) ).
cnf(s118,plain,
( spl130_13
| ~ spl130_118
| spl130_169 ),
inference(sat_conversion,[],[f1854]) ).
cnf(s119,plain,
( ~ spl130_18
| ~ spl130_148
| ~ spl130_170 ),
inference(sat_conversion,[],[f1859]) ).
cnf(s123,plain,
( spl130_28
| spl130_173
| ~ spl130_174 ),
inference(sat_conversion,[],[f1879]) ).
cnf(s172,plain,
( spl130_14
| ~ spl130_132
| ~ spl130_219 ),
inference(sat_conversion,[],[f2108]) ).
cnf(s174,plain,
( spl130_19
| ~ spl130_180
| ~ spl130_220 ),
inference(sat_conversion,[],[f2114]) ).
cnf(s177,plain,
( spl130_29
| ~ spl130_222
| ~ spl130_223 ),
inference(sat_conversion,[],[f2129]) ).
cnf(s226,plain,
( spl130_15
| ~ spl130_146
| ~ spl130_257 ),
inference(sat_conversion,[],[f2314]) ).
cnf(s228,plain,
( spl130_20
| ~ spl130_192
| ~ spl130_258 ),
inference(sat_conversion,[],[f2320]) ).
cnf(s231,plain,
( ~ spl130_30
| ~ spl130_232
| spl130_260 ),
inference(sat_conversion,[],[f2331]) ).
cnf(s233,plain,
( spl130_1
| spl130_33 ),
inference(sat_conversion,[],[f2333]) ).
cnf(s234,plain,
( spl130_1
| spl130_35 ),
inference(sat_conversion,[],[f2334]) ).
cnf(s236,plain,
( spl130_1
| ~ spl130_39 ),
inference(sat_conversion,[],[f2336]) ).
cnf(s250,plain,
( spl130_1
| ~ spl130_75 ),
inference(sat_conversion,[],[f2350]) ).
cnf(s263,plain,
( spl130_2
| spl130_107 ),
inference(sat_conversion,[],[f2363]) ).
cnf(s264,plain,
( spl130_2
| ~ spl130_108 ),
inference(sat_conversion,[],[f2364]) ).
cnf(s266,plain,
( spl130_2
| spl130_112 ),
inference(sat_conversion,[],[f2366]) ).
cnf(s293,plain,
( ~ spl130_3
| ~ spl130_169 ),
inference(sat_conversion,[],[f2393]) ).
cnf(s294,plain,
( ~ spl130_3
| spl130_170 ),
inference(sat_conversion,[],[f2394]) ).
cnf(s296,plain,
( ~ spl130_3
| ~ spl130_173 ),
inference(sat_conversion,[],[f2396]) ).
cnf(s323,plain,
( ~ spl130_4
| spl130_219 ),
inference(sat_conversion,[],[f2423]) ).
cnf(s324,plain,
( ~ spl130_4
| spl130_220 ),
inference(sat_conversion,[],[f2424]) ).
cnf(s326,plain,
( ~ spl130_4
| spl130_222 ),
inference(sat_conversion,[],[f2426]) ).
cnf(s353,plain,
( spl130_5
| spl130_257 ),
inference(sat_conversion,[],[f2453]) ).
cnf(s354,plain,
( spl130_5
| spl130_258 ),
inference(sat_conversion,[],[f2454]) ).
cnf(s356,plain,
( spl130_5
| ~ spl130_260 ),
inference(sat_conversion,[],[f2456]) ).
cnf(s357,plain,
spl130_9,
inference(sat_conversion,[],[f2457]) ).
cnf(s408,plain,
( spl130_32
| spl130_94
| spl130_148
| spl130_194
| spl130_232 ),
inference(sat_conversion,[],[f2508]) ).
cnf(s449,plain,
( ~ spl130_12
| ~ spl130_22
| spl130_24 ),
inference(sat_conversion,[],[f2686]) ).
cnf(s451,plain,
( ~ spl130_18
| ~ spl130_23
| spl130_24 ),
inference(sat_conversion,[],[f2689]) ).
cnf(s457,plain,
( ~ spl130_6
| ~ spl130_16
| spl130_18 ),
inference(sat_conversion,[],[f2693]) ).
cnf(s464,plain,
( ~ spl130_9
| spl130_26
| ~ spl130_29
| ~ spl130_30 ),
inference(sat_conversion,[],[f2756]) ).
cnf(s465,plain,
( ~ spl130_9
| spl130_21
| ~ spl130_25
| ~ spl130_29 ),
inference(sat_conversion,[],[f2757]) ).
cnf(s466,plain,
( ~ spl130_9
| ~ spl130_16
| spl130_20
| ~ spl130_29 ),
inference(sat_conversion,[],[f2758]) ).
cnf(s467,plain,
( ~ spl130_9
| ~ spl130_11
| spl130_15
| ~ spl130_29 ),
inference(sat_conversion,[],[f2759]) ).
cnf(s469,plain,
( ~ spl130_30
| ~ spl130_25
| spl130_24
| ~ spl130_30 ),
inference(sat_conversion,[],[f2773]) ).
cnf(s470,plain,
( spl130_24
| ~ spl130_25
| ~ spl130_30 ),
inference(rat,[],[s469]) ).
cnf(s491,plain,
( ~ spl130_6
| ~ spl130_26
| spl130_30 ),
inference(sat_conversion,[],[f2864]) ).
cnf(s494,plain,
( ~ spl130_12
| ~ spl130_17 ),
inference(sat_conversion,[],[f2874]) ).
cnf(s495,plain,
( ~ spl130_9
| ~ spl130_14 ),
inference(sat_conversion,[],[f2883]) ).
cnf(s513,plain,
( ~ spl130_9
| ~ spl130_19 ),
inference(sat_conversion,[],[f2941]) ).
cnf(s517,plain,
( ~ spl130_30
| spl130_27
| ~ spl130_15
| ~ spl130_30 ),
inference(sat_conversion,[],[f2965]) ).
cnf(s518,plain,
( ~ spl130_15
| spl130_27
| ~ spl130_30 ),
inference(rat,[],[s517]) ).
cnf(s520,plain,
( ~ spl130_30
| ~ spl130_15
| spl130_12
| ~ spl130_30 ),
inference(sat_conversion,[],[f2967]) ).
cnf(s521,plain,
( spl130_12
| ~ spl130_15
| ~ spl130_30 ),
inference(rat,[],[s520]) ).
cnf(s523,plain,
( ~ spl130_9
| ~ spl130_21
| spl130_25
| ~ spl130_29 ),
inference(sat_conversion,[],[f2975]) ).
cnf(s524,plain,
( ~ spl130_9
| spl130_11
| ~ spl130_15
| ~ spl130_29 ),
inference(sat_conversion,[],[f2976]) ).
cnf(s529,plain,
( spl130_18
| ~ spl130_148 ),
inference(sat_conversion,[],[f3006]) ).
cnf(s530,plain,
( spl130_12
| ~ spl130_94 ),
inference(sat_conversion,[],[f3015]) ).
cnf(s532,plain,
( spl130_34
| ~ spl130_94 ),
inference(sat_conversion,[],[f3016]) ).
cnf(s538,plain,
( spl130_6
| ~ spl130_32 ),
inference(sat_conversion,[],[f3042]) ).
cnf(s544,plain,
( spl130_24
| ~ spl130_194 ),
inference(sat_conversion,[],[f3058]) ).
cnf(s545,plain,
( spl130_223
| ~ spl130_232 ),
inference(sat_conversion,[],[f3070]) ).
cnf(s547,plain,
( spl130_174
| ~ spl130_232 ),
inference(sat_conversion,[],[f3072]) ).
cnf(s549,plain,
( spl130_113
| ~ spl130_232 ),
inference(sat_conversion,[],[f3074]) ).
cnf(s552,plain,
( spl130_30
| ~ spl130_232 ),
inference(sat_conversion,[],[f3079]) ).
cnf(s553,plain,
( ~ spl130_13
| ~ spl130_23 ),
inference(sat_conversion,[],[f3091]) ).
cnf(s556,plain,
( ~ spl130_17
| ~ spl130_22 ),
inference(sat_conversion,[],[f3102]) ).
cnf(s559,plain,
( ~ spl130_9
| ~ spl130_24 ),
inference(sat_conversion,[],[f3116]) ).
cnf(s567,plain,
( ~ spl130_17
| ~ spl130_27 ),
inference(sat_conversion,[],[f3129]) ).
cnf(s568,plain,
( ~ spl130_17
| spl130_18
| ~ spl130_27
| ~ spl130_30 ),
inference(sat_conversion,[],[f3130]) ).
cnf(s569,plain,
( ~ spl130_23
| ~ spl130_28 ),
inference(sat_conversion,[],[f3158]) ).
cnf(s571,plain,
( ~ spl130_23
| spl130_24
| ~ spl130_28
| ~ spl130_30 ),
inference(sat_conversion,[],[f3160]) ).
cnf(s574,plain,
( ~ spl130_20
| ~ spl130_30 ),
inference(sat_conversion,[],[f3179]) ).
cnf(s580,plain,
( ~ spl130_16
| ~ spl130_26 ),
inference(sat_conversion,[],[f3198]) ).
cnf(s585,plain,
( ~ spl130_94
| spl130_118 ),
inference(sat_conversion,[],[f3220]) ).
cnf(s587,plain,
( ~ spl130_94
| spl130_146 ),
inference(sat_conversion,[],[f3222]) ).
cnf(s588,plain,
( ~ spl130_94
| spl130_132 ),
inference(sat_conversion,[],[f3223]) ).
cnf(s589,plain,
( ~ spl130_15
| ~ spl130_20 ),
inference(sat_conversion,[],[f3240]) ).
cnf(s591,plain,
( ~ spl130_12
| ~ spl130_15
| spl130_18
| ~ spl130_20 ),
inference(sat_conversion,[],[f3242]) ).
cnf(s593,plain,
( ~ spl130_11
| ~ spl130_26 ),
inference(sat_conversion,[],[f3255]) ).
cnf(s596,plain,
( ~ spl130_21
| ~ spl130_26 ),
inference(sat_conversion,[],[f3267]) ).
cnf(s600,plain,
( spl130_109
| ~ spl130_148 ),
inference(sat_conversion,[],[f3312]) ).
cnf(s601,plain,
( spl130_36
| ~ spl130_148 ),
inference(sat_conversion,[],[f3313]) ).
cnf(s602,plain,
( ~ spl130_148
| spl130_192 ),
inference(sat_conversion,[],[f3314]) ).
cnf(s603,plain,
( ~ spl130_148
| spl130_180 ),
inference(sat_conversion,[],[f3315]) ).
cnf(s604,plain,
( ~ spl130_20
| ~ spl130_25 ),
inference(sat_conversion,[],[f3338]) ).
cnf(s607,plain,
( ~ spl130_13
| ~ spl130_18 ),
inference(sat_conversion,[],[f3352]) ).
cnf(s613,plain,
( ~ spl130_12
| ~ spl130_27 ),
inference(sat_conversion,[],[f3376]) ).
cnf(s616,plain,
( ~ spl130_6
| ~ spl130_21
| spl130_24 ),
inference(sat_conversion,[],[f3379]) ).
cnf(s618,plain,
( ~ spl130_15
| ~ spl130_25 ),
inference(sat_conversion,[],[f3388]) ).
cnf(s620,plain,
( ~ spl130_22
| ~ spl130_27 ),
inference(sat_conversion,[],[f3426]) ).
cnf(s623,plain,
( ~ spl130_11
| ~ spl130_21 ),
inference(sat_conversion,[],[f3439]) ).
cnf(s626,plain,
( ~ spl130_6
| ~ spl130_11
| spl130_12 ),
inference(sat_conversion,[],[f3442]) ).
cnf(s629,plain,
( ~ spl130_6
| ~ spl130_9
| ~ spl130_29
| spl130_30 ),
inference(sat_conversion,[],[f3444]) ).
cnf(s634,plain,
( ~ spl130_11
| ~ spl130_16 ),
inference(sat_conversion,[],[f3454]) ).
cnf(s637,plain,
( spl130_40
| ~ spl130_232 ),
inference(sat_conversion,[],[f3483]) ).
cnf(s638,plain,
( ~ spl130_18
| ~ spl130_28 ),
inference(sat_conversion,[],[f3493]) ).
cnf(s639,plain,
( ~ spl130_16
| ~ spl130_21 ),
inference(sat_conversion,[],[f3501]) ).
cnf(s640,plain,
( ~ spl130_13
| ~ spl130_28 ),
inference(sat_conversion,[],[f3529]) ).
cnf(s644,plain,
~ spl130_24,
inference(rat,[],[s559,s357]) ).
cnf(s645,plain,
~ spl130_19,
inference(rat,[],[s513,s357]) ).
cnf(s646,plain,
~ spl130_14,
inference(rat,[],[s495,s357]) ).
cnf(s647,plain,
~ spl130_194,
inference(rat,[],[s544,s644]) ).
cnf(s648,plain,
( ~ spl130_180
| ~ spl130_220 ),
inference(rat,[],[s174,s645]) ).
cnf(s649,plain,
( ~ spl130_132
| ~ spl130_219 ),
inference(rat,[],[s172,s646]) ).
cnf(s651,plain,
( ~ spl130_32
| spl130_75 ),
inference(rat,[],[s39,s357]) ).
cnf(s652,plain,
( spl130_21
| spl130_22
| spl130_23
| spl130_25 ),
inference(rat,[],[s5,s644]) ).
cnf(s653,plain,
( spl130_16
| spl130_17
| spl130_18
| spl130_20 ),
inference(rat,[],[s4,s645]) ).
cnf(s654,plain,
( spl130_11
| spl130_12
| spl130_13
| spl130_15 ),
inference(rat,[],[s3,s646]) ).
cnf(s655,plain,
( ~ spl130_15
| spl130_12
| spl130_94
| ~ spl130_258
| spl130_32 ),
inference(rat,[],[s408,s602,s552,s228,s521,s589,s647]) ).
cnf(s656,plain,
( ~ spl130_232
| spl130_260 ),
inference(rat,[],[s231,s552]) ).
cnf(s662,plain,
( ~ spl130_13
| spl130_16
| spl130_21
| spl130_25
| spl130_20 ),
inference(rat,[],[s556,s652,s653,s553,s607]) ).
cnf(s663,plain,
( spl130_12
| spl130_13
| spl130_11
| ~ spl130_30 ),
inference(rat,[],[s654,s521]) ).
cnf(s664,plain,
( ~ spl130_232
| spl130_39 ),
inference(rat,[],[s451,s652,s653,s449,s494,s663,s662,s580,s593,s596,s470,s574,s15,s552,s637,s644]) ).
cnf(s665,plain,
( spl130_12
| spl130_26
| spl130_11
| spl130_21
| spl130_23
| spl130_13
| spl130_28 ),
inference(rat,[],[s620,s6,s652,s524,s618,s663,s654,s357]) ).
cnf(s666,plain,
( spl130_26
| spl130_28
| spl130_11
| spl130_21
| spl130_23
| spl130_13 ),
inference(rat,[],[s6,s465,s470,s652,s449,s613,s665,s644,s357]) ).
cnf(s667,plain,
( ~ spl130_148
| ~ spl130_35 ),
inference(rat,[],[s666,s580,s634,s639,s451,s607,s638,s11,s529,s601,s644]) ).
cnf(s668,plain,
( spl130_18
| spl130_30
| spl130_1 ),
inference(rat,[],[s569,s6,s652,s467,s604,s591,s653,s613,s494,s449,s530,s634,s623,s593,s9,s532,s408,s667,s234,s664,s236,s651,s250,s233,s357,s647,s644]) ).
cnf(s669,plain,
( spl130_30
| spl130_1 ),
inference(rat,[],[s465,s652,s6,s451,s638,s668,s613,s449,s530,s623,s593,s9,s532,s408,s667,s234,s664,s236,s651,s250,s233,s357,s644,s647]) ).
cnf(s670,plain,
spl130_1,
inference(rat,[],[s451,s652,s653,s470,s574,s669,s623,s634,s449,s494,s9,s530,s532,s408,s667,s664,s651,s233,s234,s236,s250,s644,s647]) ).
cnf(s671,plain,
( ~ spl130_22
| spl130_12
| spl130_26
| spl130_18
| spl130_30
| spl130_11 ),
inference(rat,[],[s654,s589,s640,s653,s6,s556,s620,s629,s457,s538,s408,s530,s552,s529,s647,s357]) ).
cnf(s672,plain,
( spl130_12
| spl130_23
| spl130_26
| spl130_18
| spl130_30
| spl130_11
| spl130_21 ),
inference(rat,[],[s6,s567,s640,s653,s654,s604,s618,s652,s671,s457,s629,s538,s408,s530,s552,s529,s357,s647]) ).
cnf(s673,plain,
( spl130_23
| spl130_26
| spl130_18
| spl130_30
| spl130_11
| spl130_21 ),
inference(rat,[],[s1,s293,s353,s323,s263,s118,s226,s649,s63,s585,s587,s588,s408,s538,s640,s457,s6,s653,s465,s604,s618,s652,s449,s494,s613,s672,s552,s529,s670,s647,s357,s644]) ).
cnf(s674,plain,
( spl130_12
| spl130_13
| spl130_28
| spl130_26
| spl130_18
| spl130_30
| spl130_11 ),
inference(rat,[],[s653,s567,s457,s6,s538,s524,s589,s408,s654,s530,s552,s529,s357,s647]) ).
cnf(s675,plain,
( spl130_26
| spl130_18
| spl130_30
| spl130_11
| spl130_21 ),
inference(rat,[],[s1,s293,s353,s323,s263,s118,s226,s649,s63,s585,s587,s588,s408,s538,s524,s629,s6,s613,s674,s553,s569,s673,s552,s529,s670,s647,s357]) ).
cnf(s676,plain,
( spl130_18
| spl130_30
| spl130_11
| spl130_21 ),
inference(rat,[],[s293,s1,s118,s353,s553,s226,s652,s589,s604,s653,s323,s263,s449,s494,s649,s63,s530,s585,s587,s588,s408,s538,s491,s580,s675,s529,s552,s670,s644,s647]) ).
cnf(s677,plain,
( spl130_12
| spl130_30
| spl130_11
| spl130_21 ),
inference(rat,[],[s264,s1,s65,s324,s556,s294,s648,s354,s652,s119,s600,s603,s655,s618,s408,s654,s530,s552,s538,s491,s666,s607,s638,s451,s676,s670,s647,s644]) ).
cnf(s678,plain,
( ~ spl130_94
| spl130_15
| ~ spl130_12
| spl130_13 ),
inference(rat,[],[s1,s293,s353,s323,s263,s118,s226,s649,s63,s585,s587,s588,s670]) ).
cnf(s679,plain,
( spl130_30
| spl130_11
| spl130_21 ),
inference(rat,[],[s1,s264,s354,s324,s294,s65,s228,s648,s119,s600,s602,s603,s408,s678,s604,s618,s652,s449,s494,s677,s538,s491,s666,s451,s607,s638,s676,s552,s670,s647,s644]) ).
cnf(s680,plain,
( ~ spl130_22
| spl130_18
| ~ spl130_30
| spl130_11 ),
inference(rat,[],[s1,s326,s296,s266,s356,s177,s123,s69,s656,s545,s547,s549,s408,s538,s640,s466,s457,s663,s530,s653,s449,s556,s620,s574,s529,s670,s647,s357,s644]) ).
cnf(s681,plain,
( spl130_18
| spl130_11
| spl130_21 ),
inference(rat,[],[s1,s326,s296,s266,s356,s177,s123,s69,s656,s545,s547,s549,s408,s538,s466,s457,s678,s653,s518,s494,s613,s663,s553,s571,s652,s680,s529,s574,s470,s679,s670,s647,s357,s644]) ).
cnf(s682,plain,
( spl130_11
| spl130_21 ),
inference(rat,[],[s449,s652,s663,s451,s607,s681,s470,s679,s644]) ).
cnf(s683,plain,
( spl130_12
| spl130_148
| spl130_232
| ~ spl130_11 ),
inference(rat,[],[s538,s408,s626,s530,s647]) ).
cnf(s684,plain,
( spl130_18
| spl130_30
| spl130_21 ),
inference(rat,[],[s569,s6,s652,s467,s604,s589,s653,s449,s494,s613,s683,s529,s634,s593,s682,s552,s357,s644]) ).
cnf(s685,plain,
( ~ spl130_22
| spl130_3
| spl130_12
| spl130_28
| spl130_30
| ~ spl130_11 ),
inference(rat,[],[s354,s1,s655,s264,s467,s65,s6,s556,s620,s593,s530,s538,s626,s600,s324,s648,s603,s683,s552,s670,s357]) ).
cnf(s686,plain,
( spl130_12
| spl130_30
| spl130_21 ),
inference(rat,[],[s264,s65,s1,s567,s354,s6,s228,s465,s604,s652,s685,s324,s294,s648,s119,s600,s602,s603,s683,s593,s682,s552,s638,s451,s684,s670,s357,s644]) ).
cnf(s687,plain,
( spl130_30
| spl130_21 ),
inference(rat,[],[s465,s652,s6,s449,s613,s686,s451,s638,s684,s593,s682,s357,s644]) ).
cnf(s688,plain,
( spl130_18
| spl130_21 ),
inference(rat,[],[s1,s326,s296,s266,s356,s177,s123,s69,s656,s545,s547,s549,s571,s683,s652,s494,s556,s568,s653,s529,s634,s574,s470,s464,s687,s593,s682,s670,s644,s357]) ).
cnf(s689,plain,
( ~ spl130_232
| spl130_21 ),
inference(rat,[],[s1,s326,s296,s266,s356,s177,s123,s69,s656,s545,s547,s549,s464,s593,s682,s638,s620,s652,s451,s688,s470,s687,s670,s644,s357]) ).
cnf(s690,plain,
spl130_21,
inference(rat,[],[s1,s264,s354,s324,s294,s65,s228,s648,s119,s600,s602,s603,s683,s689,s449,s556,s652,s451,s688,s470,s574,s687,s682,s670,s644]) ).
cnf(s691,plain,
~ spl130_16,
inference(rat,[],[s639,s690]) ).
cnf(s692,plain,
~ spl130_11,
inference(rat,[],[s623,s690]) ).
cnf(s693,plain,
~ spl130_6,
inference(rat,[],[s616,s644,s690]) ).
cnf(s694,plain,
~ spl130_26,
inference(rat,[],[s596,s690]) ).
cnf(s695,plain,
~ spl130_32,
inference(rat,[],[s538,s693]) ).
cnf(s696,plain,
( spl130_30
| spl130_12 ),
inference(rat,[],[s264,s65,s1,s567,s354,s6,s655,s524,s654,s324,s294,s607,s638,s648,s119,s529,s600,s603,s408,s552,s530,s670,s694,s695,s357,s692,s647]) ).
cnf(s697,plain,
spl130_12,
inference(rat,[],[s1,s326,s296,s266,s356,s177,s123,s69,s656,s545,s547,s549,s568,s408,s653,s529,s607,s640,s663,s464,s574,s696,s530,s670,s647,s695,s691,s692,s357,s694]) ).
cnf(s698,plain,
~ spl130_27,
inference(rat,[],[s613,s697]) ).
cnf(s699,plain,
~ spl130_17,
inference(rat,[],[s494,s697]) ).
cnf(s702,plain,
( spl130_18
| spl130_30 ),
inference(rat,[],[s640,s6,s678,s523,s589,s604,s408,s653,s529,s552,s694,s698,s697,s357,s690,s647,s695,s691,s699]) ).
cnf(s703,plain,
spl130_30,
inference(rat,[],[s1,s264,s354,s324,s294,s65,s228,s648,s119,s600,s602,s603,s408,s678,s604,s524,s523,s6,s607,s638,s702,s552,s670,s699,s647,s695,s697,s357,s692,s690,s694,s698]) ).
cnf(s704,plain,
~ spl130_20,
inference(rat,[],[s574,s703]) ).
cnf(s706,plain,
~ spl130_29,
inference(rat,[],[s464,s694,s357,s703]) ).
cnf(s707,plain,
~ spl130_15,
inference(rat,[],[s518,s698,s703]) ).
cnf(s708,plain,
spl130_18,
inference(rat,[],[s653,s699,s691,s704]) ).
cnf(s709,plain,
~ spl130_28,
inference(rat,[],[s638,s708]) ).
cnf(s711,plain,
~ spl130_13,
inference(rat,[],[s607,s708]) ).
cnf(s713,plain,
~ spl130_94,
inference(rat,[],[s678,s707,s697,s711]) ).
cnf(s714,plain,
~ spl130_232,
inference(rat,[],[s1,s326,s296,s266,s356,s177,s123,s69,s656,s545,s547,s549,s670,s706,s709,s698]) ).
cnf(s715,plain,
spl130_148,
inference(rat,[],[s408,s695,s647,s713,s714]) ).
cnf(s716,plain,
spl130_180,
inference(rat,[],[s603,s715]) ).
cnf(s717,plain,
spl130_192,
inference(rat,[],[s602,s715]) ).
cnf(s719,plain,
spl130_109,
inference(rat,[],[s600,s715]) ).
cnf(s724,plain,
~ spl130_170,
inference(rat,[],[s119,s708,s715]) ).
cnf(s725,plain,
~ spl130_220,
inference(rat,[],[s648,s716]) ).
cnf(s726,plain,
~ spl130_258,
inference(rat,[],[s228,s704,s717]) ).
cnf(s727,plain,
spl130_108,
inference(rat,[],[s65,s699,s719]) ).
cnf(s728,plain,
~ spl130_3,
inference(rat,[],[s294,s724]) ).
cnf(s729,plain,
~ spl130_4,
inference(rat,[],[s324,s725]) ).
cnf(s730,plain,
spl130_5,
inference(rat,[],[s354,s726]) ).
cnf(s731,plain,
spl130_2,
inference(rat,[],[s264,s727]) ).
cnf(s732,plain,
$false,
inference(rat,[],[s1,s729,s728,s670,s730,s731]) ).
fof(f3533,plain,
$false,
inference(avatar_sat_refutation,[],[s732]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG062+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 % Computer : n001.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Mon Sep 28 19:28:27 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 Running first-order model finding
% 0.10/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.32 % (649537)Will run a generic schedule for satisfiability detection.
% 0.20/0.32 % (649543)% WARNING: option uhcvi not known.
% 0.20/0.32 % (649543)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=195228956:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.32 % (649542)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=432091292_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.32 % (649544)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3011971426:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.32 % (649545)dis+10_1_sil=32000:sp=arity:random_seed=279771571:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.32 % (649546)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3369407601:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.32 % (649547)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3028167117:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.32 % (649548)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1799176382:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.32 % Detected minimum model sizes of [5]
% 0.20/0.32 % Detected maximum model sizes of [max]
% 0.20/0.32 % TRYING [5]
% 0.20/0.32 % (649548) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-649537-649548"...
% 0.20/0.32 % TRYING [6]
% 0.20/0.32 % (649548)...printing done.
% 0.20/0.32 % (649548)Refutation found. Thanks to Tanya!
% 0.20/0.32 % SZS status Theorem for theBenchmark
% 0.20/0.32 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/0.33 % (649548)------------------------------
% 0.20/0.33 % (649548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.33 % (649548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.33 % (649548)CaDiCaL version: 2.1.3
% 0.20/0.33 % (649548)Termination reason: Refutation
% 0.20/0.33 % (649548)Time elapsed: 0.051 s
% 0.20/0.33 % (649548)Peak memory usage: 14 MB
% 0.20/0.33 % (649548)Instructions burned: 96 (million)
% 0.20/0.33 % (649537)Success in time 0.096 s
% 0.20/0.33 % Vampire exiting
%------------------------------------------------------------------------------