%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG059+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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:09:05 AM UTC 2026
% Result : Theorem 2.20s 1.20s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 310
% Syntax : Number of formulae : 1155 ( 193 unt; 303 def)
% Number of atoms : 5006 (2901 equ)
% Maximal formula atoms : 450 ( 4 avg)
% Number of connectives : 6483 (2632 ~;2138 |;1564 &)
% ( 149 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 305 ( 303 usr; 304 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e4 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e4 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3
| op(e0,e2) = e4 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3
| op(e0,e3) = e4 )
& ( op(e0,e4) = e0
| op(e0,e4) = e1
| op(e0,e4) = e2
| op(e0,e4) = e3
| op(e0,e4) = e4 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3
| op(e1,e0) = e4 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3
| op(e1,e1) = e4 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3
| op(e1,e2) = e4 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3
| op(e1,e3) = e4 )
& ( op(e1,e4) = e0
| op(e1,e4) = e1
| op(e1,e4) = e2
| op(e1,e4) = e3
| op(e1,e4) = e4 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3
| op(e2,e0) = e4 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3
| op(e2,e1) = e4 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3
| op(e2,e2) = e4 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3
| op(e2,e3) = e4 )
& ( op(e2,e4) = e0
| op(e2,e4) = e1
| op(e2,e4) = e2
| op(e2,e4) = e3
| op(e2,e4) = e4 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3
| op(e3,e0) = e4 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3
| op(e3,e1) = e4 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3
| op(e3,e2) = e4 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3
| op(e3,e3) = e4 )
& ( op(e3,e4) = e0
| op(e3,e4) = e1
| op(e3,e4) = e2
| op(e3,e4) = e3
| op(e3,e4) = e4 )
& ( op(e4,e0) = e0
| op(e4,e0) = e1
| op(e4,e0) = e2
| op(e4,e0) = e3
| op(e4,e0) = e4 )
& ( op(e4,e1) = e0
| op(e4,e1) = e1
| op(e4,e1) = e2
| op(e4,e1) = e3
| op(e4,e1) = e4 )
& ( op(e4,e2) = e0
| op(e4,e2) = e1
| op(e4,e2) = e2
| op(e4,e2) = e3
| op(e4,e2) = e4 )
& ( op(e4,e3) = e0
| op(e4,e3) = e1
| op(e4,e3) = e2
| op(e4,e3) = e3
| op(e4,e3) = e4 )
& ( op(e4,e4) = e0
| op(e4,e4) = e1
| op(e4,e4) = e2
| op(e4,e4) = e3
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
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(f3,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0
| op(e0,e4) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0
| op(e4,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| op(e0,e4) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e4,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| op(e0,e4) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2
| op(e4,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3
| op(e0,e4) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3
| op(e4,e0) = e3 )
& ( op(e0,e0) = e4
| op(e0,e1) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e4) = e4 )
& ( op(e0,e0) = e4
| op(e1,e0) = e4
| op(e2,e0) = e4
| op(e3,e0) = e4
| op(e4,e0) = e4 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0
| op(e1,e4) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0
| op(e4,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1
| op(e1,e4) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1
| op(e4,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2
| op(e1,e4) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| op(e4,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3
| op(e1,e4) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3
| op(e4,e1) = e3 )
& ( op(e1,e0) = e4
| op(e1,e1) = e4
| op(e1,e2) = e4
| op(e1,e3) = e4
| op(e1,e4) = e4 )
& ( op(e0,e1) = e4
| op(e1,e1) = e4
| op(e2,e1) = e4
| op(e3,e1) = e4
| op(e4,e1) = e4 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0
| op(e2,e4) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0
| op(e4,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1
| op(e2,e4) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1
| op(e4,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2
| op(e2,e4) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2
| op(e4,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| op(e2,e4) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3
| op(e4,e2) = e3 )
& ( op(e2,e0) = e4
| op(e2,e1) = e4
| op(e2,e2) = e4
| op(e2,e3) = e4
| op(e2,e4) = e4 )
& ( op(e0,e2) = e4
| op(e1,e2) = e4
| op(e2,e2) = e4
| op(e3,e2) = e4
| op(e4,e2) = e4 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0
| op(e3,e4) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0
| op(e4,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1
| op(e3,e4) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1
| op(e4,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| op(e3,e4) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2
| op(e4,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3
| op(e3,e4) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3
| op(e4,e3) = e3 )
& ( op(e3,e0) = e4
| op(e3,e1) = e4
| op(e3,e2) = e4
| op(e3,e3) = e4
| op(e3,e4) = e4 )
& ( op(e0,e3) = e4
| op(e1,e3) = e4
| op(e2,e3) = e4
| op(e3,e3) = e4
| op(e4,e3) = e4 )
& ( op(e4,e0) = e0
| op(e4,e1) = e0
| op(e4,e2) = e0
| op(e4,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e4) = e0
| op(e1,e4) = e0
| op(e2,e4) = e0
| op(e3,e4) = e0
| op(e4,e4) = e0 )
& ( op(e4,e0) = e1
| op(e4,e1) = e1
| op(e4,e2) = e1
| op(e4,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e4) = e1
| op(e1,e4) = e1
| op(e2,e4) = e1
| op(e3,e4) = e1
| op(e4,e4) = e1 )
& ( op(e4,e0) = e2
| op(e4,e1) = e2
| op(e4,e2) = e2
| op(e4,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e4) = e2
| op(e1,e4) = e2
| op(e2,e4) = e2
| op(e3,e4) = e2
| op(e4,e4) = e2 )
& ( op(e4,e0) = e3
| op(e4,e1) = e3
| op(e4,e2) = e3
| op(e4,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e4) = e3
| op(e1,e4) = e3
| op(e2,e4) = e3
| op(e3,e4) = e3
| op(e4,e4) = e3 )
& ( op(e4,e0) = e4
| op(e4,e1) = e4
| op(e4,e2) = e4
| op(e4,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e4) = e4
| op(e1,e4) = e4
| op(e2,e4) = e4
| op(e3,e4) = e4
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e4,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e4,e0)
& op(e2,e0) != op(e3,e0)
& op(e2,e0) != op(e4,e0)
& op(e3,e0) != op(e4,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e4,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e4,e1)
& op(e2,e1) != op(e3,e1)
& op(e2,e1) != op(e4,e1)
& op(e3,e1) != op(e4,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e4,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e4,e2)
& op(e2,e2) != op(e3,e2)
& op(e2,e2) != op(e4,e2)
& op(e3,e2) != op(e4,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e4,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e4,e3)
& op(e2,e3) != op(e3,e3)
& op(e2,e3) != op(e4,e3)
& op(e3,e3) != op(e4,e3)
& op(e0,e4) != op(e1,e4)
& op(e0,e4) != op(e2,e4)
& op(e0,e4) != op(e3,e4)
& op(e0,e4) != op(e4,e4)
& op(e1,e4) != op(e2,e4)
& op(e1,e4) != op(e3,e4)
& op(e1,e4) != op(e4,e4)
& op(e2,e4) != op(e3,e4)
& op(e2,e4) != op(e4,e4)
& op(e3,e4) != op(e4,e4)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e4)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e4)
& op(e0,e2) != op(e0,e3)
& op(e0,e2) != op(e0,e4)
& op(e0,e3) != op(e0,e4)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e4)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e4)
& op(e1,e2) != op(e1,e3)
& op(e1,e2) != op(e1,e4)
& op(e1,e3) != op(e1,e4)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e4)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e4)
& op(e2,e2) != op(e2,e3)
& op(e2,e2) != op(e2,e4)
& op(e2,e3) != op(e2,e4)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e4)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e4)
& op(e3,e2) != op(e3,e3)
& op(e3,e2) != op(e3,e4)
& op(e3,e3) != op(e3,e4)
& op(e4,e0) != op(e4,e1)
& op(e4,e0) != op(e4,e2)
& op(e4,e0) != op(e4,e3)
& op(e4,e0) != op(e4,e4)
& op(e4,e1) != op(e4,e2)
& op(e4,e1) != op(e4,e3)
& op(e4,e1) != op(e4,e4)
& op(e4,e2) != op(e4,e3)
& op(e4,e2) != op(e4,e4)
& op(e4,e3) != op(e4,e4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
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(op(op(e2,e2),e2),op(op(e2,e2),e2))
& e1 = op(op(e2,e2),e2)
& e3 = op(e2,e2)
& e4 = op(op(e2,e2),op(e2,e2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,conjecture,
~ ( ( ( ( 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 ) ) ) )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f8,negated_conjecture,
~ ~ ( ( ( ( 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 ) ) ) )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 ) ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f9,plain,
( ( ( ( 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 ) ) ) )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 ) ) ),
inference(flattening,[],[f8]) ).
fof(f10,definition,
( ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11,definition,
( ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f12,definition,
( ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f13,definition,
( ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f17,definition,
( ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f18,definition,
( ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f19,definition,
( ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f20,definition,
( ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f21,definition,
( ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f22,definition,
( ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f25,definition,
( ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f26,definition,
( ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f27,definition,
( ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f29,definition,
( ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f30,definition,
( ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f31,definition,
( ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f32,definition,
( ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f33,definition,
( ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ~ sP23 ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f34,definition,
( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit )
| ~ sP24 ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f35,definition,
( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit )
| ~ sP25 ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f36,definition,
( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit )
| ~ sP26 ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f37,definition,
( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit )
| ~ sP27 ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f38,definition,
( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit )
| ~ sP28 ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f39,definition,
( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit )
| ~ sP29 ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f40,definition,
( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit )
| ~ sP30 ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f41,definition,
( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit )
| ~ sP31 ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f42,definition,
( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit )
| ~ sP32 ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f43,definition,
( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit )
| ~ sP33 ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f44,definition,
( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit )
| ~ sP34 ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f45,definition,
( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit )
| ~ sP35 ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f46,definition,
( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit )
| ~ sP36 ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f47,definition,
( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit )
| ~ sP37 ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f48,definition,
( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit )
| ~ sP38 ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f49,definition,
( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit )
| ~ sP39 ),
introduced(definition,[new_symbols(definition,[sP39])],[predicate_definition_introduction]) ).
fof(f50,definition,
( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit )
| ~ sP40 ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f51,definition,
( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit )
| ~ sP41 ),
introduced(definition,[new_symbols(definition,[sP41])],[predicate_definition_introduction]) ).
fof(f52,definition,
( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit )
| ~ sP42 ),
introduced(definition,[new_symbols(definition,[sP42])],[predicate_definition_introduction]) ).
fof(f53,definition,
( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit )
| ~ sP43 ),
introduced(definition,[new_symbols(definition,[sP43])],[predicate_definition_introduction]) ).
fof(f54,definition,
( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit )
| ~ sP44 ),
introduced(definition,[new_symbols(definition,[sP44])],[predicate_definition_introduction]) ).
fof(f55,definition,
( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit )
| ~ sP45 ),
introduced(definition,[new_symbols(definition,[sP45])],[predicate_definition_introduction]) ).
fof(f56,definition,
( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit )
| ~ sP46 ),
introduced(definition,[new_symbols(definition,[sP46])],[predicate_definition_introduction]) ).
fof(f57,definition,
( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit )
| ~ sP47 ),
introduced(definition,[new_symbols(definition,[sP47])],[predicate_definition_introduction]) ).
fof(f58,definition,
( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit )
| ~ sP48 ),
introduced(definition,[new_symbols(definition,[sP48])],[predicate_definition_introduction]) ).
fof(f59,definition,
( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit )
| ~ sP49 ),
introduced(definition,[new_symbols(definition,[sP49])],[predicate_definition_introduction]) ).
fof(f60,definition,
( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit )
| ~ sP50 ),
introduced(definition,[new_symbols(definition,[sP50])],[predicate_definition_introduction]) ).
fof(f61,definition,
( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit )
| ~ sP51 ),
introduced(definition,[new_symbols(definition,[sP51])],[predicate_definition_introduction]) ).
fof(f62,definition,
( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit )
| ~ sP52 ),
introduced(definition,[new_symbols(definition,[sP52])],[predicate_definition_introduction]) ).
fof(f63,definition,
( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit )
| ~ sP53 ),
introduced(definition,[new_symbols(definition,[sP53])],[predicate_definition_introduction]) ).
fof(f64,definition,
( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit )
| ~ sP54 ),
introduced(definition,[new_symbols(definition,[sP54])],[predicate_definition_introduction]) ).
fof(f65,definition,
( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit )
| ~ sP55 ),
introduced(definition,[new_symbols(definition,[sP55])],[predicate_definition_introduction]) ).
fof(f66,definition,
( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit )
| ~ sP56 ),
introduced(definition,[new_symbols(definition,[sP56])],[predicate_definition_introduction]) ).
fof(f67,definition,
( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit )
| ~ sP57 ),
introduced(definition,[new_symbols(definition,[sP57])],[predicate_definition_introduction]) ).
fof(f68,definition,
( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit )
| ~ sP58 ),
introduced(definition,[new_symbols(definition,[sP58])],[predicate_definition_introduction]) ).
fof(f69,definition,
( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit )
| ~ sP59 ),
introduced(definition,[new_symbols(definition,[sP59])],[predicate_definition_introduction]) ).
fof(f70,definition,
( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit )
| ~ sP60 ),
introduced(definition,[new_symbols(definition,[sP60])],[predicate_definition_introduction]) ).
fof(f71,definition,
( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit )
| ~ sP61 ),
introduced(definition,[new_symbols(definition,[sP61])],[predicate_definition_introduction]) ).
fof(f72,definition,
( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit )
| ~ sP62 ),
introduced(definition,[new_symbols(definition,[sP62])],[predicate_definition_introduction]) ).
fof(f73,definition,
( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit )
| ~ sP63 ),
introduced(definition,[new_symbols(definition,[sP63])],[predicate_definition_introduction]) ).
fof(f74,definition,
( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit )
| ~ sP64 ),
introduced(definition,[new_symbols(definition,[sP64])],[predicate_definition_introduction]) ).
fof(f75,definition,
( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit )
| ~ sP65 ),
introduced(definition,[new_symbols(definition,[sP65])],[predicate_definition_introduction]) ).
fof(f76,definition,
( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit )
| ~ sP66 ),
introduced(definition,[new_symbols(definition,[sP66])],[predicate_definition_introduction]) ).
fof(f77,definition,
( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit )
| ~ sP67 ),
introduced(definition,[new_symbols(definition,[sP67])],[predicate_definition_introduction]) ).
fof(f78,definition,
( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit )
| ~ sP68 ),
introduced(definition,[new_symbols(definition,[sP68])],[predicate_definition_introduction]) ).
fof(f79,definition,
( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit )
| ~ sP69 ),
introduced(definition,[new_symbols(definition,[sP69])],[predicate_definition_introduction]) ).
fof(f80,definition,
( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit )
| ~ sP70 ),
introduced(definition,[new_symbols(definition,[sP70])],[predicate_definition_introduction]) ).
fof(f81,definition,
( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit )
| ~ sP71 ),
introduced(definition,[new_symbols(definition,[sP71])],[predicate_definition_introduction]) ).
fof(f82,definition,
( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit )
| ~ sP72 ),
introduced(definition,[new_symbols(definition,[sP72])],[predicate_definition_introduction]) ).
fof(f83,definition,
( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit )
| ~ sP73 ),
introduced(definition,[new_symbols(definition,[sP73])],[predicate_definition_introduction]) ).
fof(f84,definition,
( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit )
| ~ sP74 ),
introduced(definition,[new_symbols(definition,[sP74])],[predicate_definition_introduction]) ).
fof(f85,definition,
( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit )
| ~ sP75 ),
introduced(definition,[new_symbols(definition,[sP75])],[predicate_definition_introduction]) ).
fof(f86,definition,
( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit )
| ~ sP76 ),
introduced(definition,[new_symbols(definition,[sP76])],[predicate_definition_introduction]) ).
fof(f87,definition,
( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit )
| ~ sP77 ),
introduced(definition,[new_symbols(definition,[sP77])],[predicate_definition_introduction]) ).
fof(f88,definition,
( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit )
| ~ sP78 ),
introduced(definition,[new_symbols(definition,[sP78])],[predicate_definition_introduction]) ).
fof(f89,definition,
( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit )
| ~ sP79 ),
introduced(definition,[new_symbols(definition,[sP79])],[predicate_definition_introduction]) ).
fof(f90,definition,
( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit )
| ~ sP80 ),
introduced(definition,[new_symbols(definition,[sP80])],[predicate_definition_introduction]) ).
fof(f91,definition,
( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit )
| ~ sP81 ),
introduced(definition,[new_symbols(definition,[sP81])],[predicate_definition_introduction]) ).
fof(f92,definition,
( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit )
| ~ sP82 ),
introduced(definition,[new_symbols(definition,[sP82])],[predicate_definition_introduction]) ).
fof(f93,definition,
( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit )
| ~ sP83 ),
introduced(definition,[new_symbols(definition,[sP83])],[predicate_definition_introduction]) ).
fof(f94,definition,
( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit )
| ~ sP84 ),
introduced(definition,[new_symbols(definition,[sP84])],[predicate_definition_introduction]) ).
fof(f95,definition,
( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit )
| ~ sP85 ),
introduced(definition,[new_symbols(definition,[sP85])],[predicate_definition_introduction]) ).
fof(f96,definition,
( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit )
| ~ sP86 ),
introduced(definition,[new_symbols(definition,[sP86])],[predicate_definition_introduction]) ).
fof(f97,definition,
( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit )
| ~ sP87 ),
introduced(definition,[new_symbols(definition,[sP87])],[predicate_definition_introduction]) ).
fof(f98,definition,
( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit )
| ~ sP88 ),
introduced(definition,[new_symbols(definition,[sP88])],[predicate_definition_introduction]) ).
fof(f99,definition,
( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit )
| ~ sP89 ),
introduced(definition,[new_symbols(definition,[sP89])],[predicate_definition_introduction]) ).
fof(f100,definition,
( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit )
| ~ sP90 ),
introduced(definition,[new_symbols(definition,[sP90])],[predicate_definition_introduction]) ).
fof(f101,definition,
( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit )
| ~ sP91 ),
introduced(definition,[new_symbols(definition,[sP91])],[predicate_definition_introduction]) ).
fof(f102,definition,
( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit )
| ~ sP92 ),
introduced(definition,[new_symbols(definition,[sP92])],[predicate_definition_introduction]) ).
fof(f103,definition,
( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit )
| ~ sP93 ),
introduced(definition,[new_symbols(definition,[sP93])],[predicate_definition_introduction]) ).
fof(f104,definition,
( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit )
| ~ sP94 ),
introduced(definition,[new_symbols(definition,[sP94])],[predicate_definition_introduction]) ).
fof(f105,definition,
( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit )
| ~ sP95 ),
introduced(definition,[new_symbols(definition,[sP95])],[predicate_definition_introduction]) ).
fof(f106,definition,
( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit )
| ~ sP96 ),
introduced(definition,[new_symbols(definition,[sP96])],[predicate_definition_introduction]) ).
fof(f107,definition,
( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit )
| ~ sP97 ),
introduced(definition,[new_symbols(definition,[sP97])],[predicate_definition_introduction]) ).
fof(f108,definition,
( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit )
| ~ sP98 ),
introduced(definition,[new_symbols(definition,[sP98])],[predicate_definition_introduction]) ).
fof(f109,definition,
( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit )
| ~ sP99 ),
introduced(definition,[new_symbols(definition,[sP99])],[predicate_definition_introduction]) ).
fof(f110,definition,
( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit )
| ~ sP100 ),
introduced(definition,[new_symbols(definition,[sP100])],[predicate_definition_introduction]) ).
fof(f111,definition,
( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit )
| ~ sP101 ),
introduced(definition,[new_symbols(definition,[sP101])],[predicate_definition_introduction]) ).
fof(f112,definition,
( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit )
| ~ sP102 ),
introduced(definition,[new_symbols(definition,[sP102])],[predicate_definition_introduction]) ).
fof(f113,definition,
( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit )
| ~ sP103 ),
introduced(definition,[new_symbols(definition,[sP103])],[predicate_definition_introduction]) ).
fof(f114,definition,
( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit )
| ~ sP104 ),
introduced(definition,[new_symbols(definition,[sP104])],[predicate_definition_introduction]) ).
fof(f115,definition,
( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit )
| ~ sP105 ),
introduced(definition,[new_symbols(definition,[sP105])],[predicate_definition_introduction]) ).
fof(f116,definition,
( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit )
| ~ sP106 ),
introduced(definition,[new_symbols(definition,[sP106])],[predicate_definition_introduction]) ).
fof(f117,definition,
( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit )
| ~ sP107 ),
introduced(definition,[new_symbols(definition,[sP107])],[predicate_definition_introduction]) ).
fof(f118,definition,
( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit )
| ~ sP108 ),
introduced(definition,[new_symbols(definition,[sP108])],[predicate_definition_introduction]) ).
fof(f119,definition,
( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit )
| ~ sP109 ),
introduced(definition,[new_symbols(definition,[sP109])],[predicate_definition_introduction]) ).
fof(f120,definition,
( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit )
| ~ sP110 ),
introduced(definition,[new_symbols(definition,[sP110])],[predicate_definition_introduction]) ).
fof(f121,definition,
( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit )
| ~ sP111 ),
introduced(definition,[new_symbols(definition,[sP111])],[predicate_definition_introduction]) ).
fof(f122,definition,
( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit )
| ~ sP112 ),
introduced(definition,[new_symbols(definition,[sP112])],[predicate_definition_introduction]) ).
fof(f123,definition,
( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit )
| ~ sP113 ),
introduced(definition,[new_symbols(definition,[sP113])],[predicate_definition_introduction]) ).
fof(f124,definition,
( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit )
| ~ sP114 ),
introduced(definition,[new_symbols(definition,[sP114])],[predicate_definition_introduction]) ).
fof(f125,definition,
( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit )
| ~ sP115 ),
introduced(definition,[new_symbols(definition,[sP115])],[predicate_definition_introduction]) ).
fof(f126,definition,
( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit )
| ~ sP116 ),
introduced(definition,[new_symbols(definition,[sP116])],[predicate_definition_introduction]) ).
fof(f127,definition,
( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit )
| ~ sP117 ),
introduced(definition,[new_symbols(definition,[sP117])],[predicate_definition_introduction]) ).
fof(f128,definition,
( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit )
| ~ sP118 ),
introduced(definition,[new_symbols(definition,[sP118])],[predicate_definition_introduction]) ).
fof(f129,definition,
( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit )
| ~ sP119 ),
introduced(definition,[new_symbols(definition,[sP119])],[predicate_definition_introduction]) ).
fof(f130,definition,
( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit )
| ~ sP120 ),
introduced(definition,[new_symbols(definition,[sP120])],[predicate_definition_introduction]) ).
fof(f131,definition,
( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit )
| ~ sP121 ),
introduced(definition,[new_symbols(definition,[sP121])],[predicate_definition_introduction]) ).
fof(f132,definition,
( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit )
| ~ sP122 ),
introduced(definition,[new_symbols(definition,[sP122])],[predicate_definition_introduction]) ).
fof(f133,definition,
( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit )
| ~ sP123 ),
introduced(definition,[new_symbols(definition,[sP123])],[predicate_definition_introduction]) ).
fof(f134,definition,
( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit )
| ~ sP124 ),
introduced(definition,[new_symbols(definition,[sP124])],[predicate_definition_introduction]) ).
fof(f135,definition,
( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit )
| ~ sP125 ),
introduced(definition,[new_symbols(definition,[sP125])],[predicate_definition_introduction]) ).
fof(f136,definition,
( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit )
| ~ sP126 ),
introduced(definition,[new_symbols(definition,[sP126])],[predicate_definition_introduction]) ).
fof(f137,definition,
( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit )
| ~ sP127 ),
introduced(definition,[new_symbols(definition,[sP127])],[predicate_definition_introduction]) ).
fof(f138,definition,
( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit )
| ~ sP128 ),
introduced(definition,[new_symbols(definition,[sP128])],[predicate_definition_introduction]) ).
fof(f139,definition,
( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit )
| ~ sP129 ),
introduced(definition,[new_symbols(definition,[sP129])],[predicate_definition_introduction]) ).
fof(f140,definition,
( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit )
| ~ sP130 ),
introduced(definition,[new_symbols(definition,[sP130])],[predicate_definition_introduction]) ).
fof(f141,definition,
( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit )
| ~ sP131 ),
introduced(definition,[new_symbols(definition,[sP131])],[predicate_definition_introduction]) ).
fof(f142,definition,
( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit )
| ~ sP132 ),
introduced(definition,[new_symbols(definition,[sP132])],[predicate_definition_introduction]) ).
fof(f143,definition,
( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit )
| ~ sP133 ),
introduced(definition,[new_symbols(definition,[sP133])],[predicate_definition_introduction]) ).
fof(f144,definition,
( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit )
| ~ sP134 ),
introduced(definition,[new_symbols(definition,[sP134])],[predicate_definition_introduction]) ).
fof(f145,definition,
( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit )
| ~ sP135 ),
introduced(definition,[new_symbols(definition,[sP135])],[predicate_definition_introduction]) ).
fof(f146,definition,
( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit )
| ~ sP136 ),
introduced(definition,[new_symbols(definition,[sP136])],[predicate_definition_introduction]) ).
fof(f147,definition,
( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit )
| ~ sP137 ),
introduced(definition,[new_symbols(definition,[sP137])],[predicate_definition_introduction]) ).
fof(f148,definition,
( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit )
| ~ sP138 ),
introduced(definition,[new_symbols(definition,[sP138])],[predicate_definition_introduction]) ).
fof(f149,definition,
( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit )
| ~ sP139 ),
introduced(definition,[new_symbols(definition,[sP139])],[predicate_definition_introduction]) ).
fof(f150,definition,
( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit )
| ~ sP140 ),
introduced(definition,[new_symbols(definition,[sP140])],[predicate_definition_introduction]) ).
fof(f151,definition,
( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit )
| ~ sP141 ),
introduced(definition,[new_symbols(definition,[sP141])],[predicate_definition_introduction]) ).
fof(f152,definition,
( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit )
| ~ sP142 ),
introduced(definition,[new_symbols(definition,[sP142])],[predicate_definition_introduction]) ).
fof(f153,definition,
( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit )
| ~ sP143 ),
introduced(definition,[new_symbols(definition,[sP143])],[predicate_definition_introduction]) ).
fof(f154,definition,
( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit )
| ~ sP144 ),
introduced(definition,[new_symbols(definition,[sP144])],[predicate_definition_introduction]) ).
fof(f155,definition,
( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit )
| ~ sP145 ),
introduced(definition,[new_symbols(definition,[sP145])],[predicate_definition_introduction]) ).
fof(f156,definition,
( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit )
| ~ sP146 ),
introduced(definition,[new_symbols(definition,[sP146])],[predicate_definition_introduction]) ).
fof(f157,definition,
( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit )
| ~ sP147 ),
introduced(definition,[new_symbols(definition,[sP147])],[predicate_definition_introduction]) ).
fof(f158,definition,
( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit )
| ~ sP148 ),
introduced(definition,[new_symbols(definition,[sP148])],[predicate_definition_introduction]) ).
fof(f159,definition,
( ( sP48
& sP47
& sP46
& sP45
& sP44
& sP43
& sP42
& sP41
& sP40
& sP39
& sP38
& sP37
& sP36
& sP35
& sP34
& sP33
& sP32
& sP31
& sP30
& sP29
& sP28
& sP27
& sP26
& sP25
& sP24 )
| ~ sP149 ),
introduced(definition,[new_symbols(definition,[sP149])],[predicate_definition_introduction]) ).
fof(f160,definition,
( ( sP73
& sP72
& sP71
& sP70
& sP69
& sP68
& sP67
& sP66
& sP65
& sP64
& sP63
& sP62
& sP61
& sP60
& sP59
& sP58
& sP57
& sP56
& sP55
& sP54
& sP53
& sP52
& sP51
& sP50
& sP49 )
| ~ sP150 ),
introduced(definition,[new_symbols(definition,[sP150])],[predicate_definition_introduction]) ).
fof(f161,definition,
( ( sP98
& sP97
& sP96
& sP95
& sP94
& sP93
& sP92
& sP91
& sP90
& sP89
& sP88
& sP87
& sP86
& sP85
& sP84
& sP83
& sP82
& sP81
& sP80
& sP79
& sP78
& sP77
& sP76
& sP75
& sP74 )
| ~ sP151 ),
introduced(definition,[new_symbols(definition,[sP151])],[predicate_definition_introduction]) ).
fof(f162,definition,
( ( sP123
& sP122
& sP121
& sP120
& sP119
& sP118
& sP117
& sP116
& sP115
& sP114
& sP113
& sP112
& sP111
& sP110
& sP109
& sP108
& sP107
& sP106
& sP105
& sP104
& sP103
& sP102
& sP101
& sP100
& sP99 )
| ~ sP152 ),
introduced(definition,[new_symbols(definition,[sP152])],[predicate_definition_introduction]) ).
fof(f163,definition,
( ( sP148
& sP147
& sP146
& sP145
& sP144
& sP143
& sP142
& sP141
& sP140
& sP139
& sP138
& sP137
& sP136
& sP135
& sP134
& sP133
& sP132
& sP131
& sP130
& sP129
& sP128
& sP127
& sP126
& sP125
& sP124 )
| ~ sP153 ),
introduced(definition,[new_symbols(definition,[sP153])],[predicate_definition_introduction]) ).
fof(f164,plain,
( ( sP153
| sP152
| sP151
| sP150
| sP149 )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ) ),
inference(definition_folding,[],[f9,f163,f162,f161,f160,f159,f158,f157,f156,f155,f154,f153,f152,f151,f150,f149,f148,f147,f146,f145,f144,f143,f142,f141,f140,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(f165,plain,
( ( sP148
& sP147
& sP146
& sP145
& sP144
& sP143
& sP142
& sP141
& sP140
& sP139
& sP138
& sP137
& sP136
& sP135
& sP134
& sP133
& sP132
& sP131
& sP130
& sP129
& sP128
& sP127
& sP126
& sP125
& sP124 )
| ~ sP153 ),
inference(nnf_transformation,[],[f163]) ).
fof(f166,plain,
( ( sP123
& sP122
& sP121
& sP120
& sP119
& sP118
& sP117
& sP116
& sP115
& sP114
& sP113
& sP112
& sP111
& sP110
& sP109
& sP108
& sP107
& sP106
& sP105
& sP104
& sP103
& sP102
& sP101
& sP100
& sP99 )
| ~ sP152 ),
inference(nnf_transformation,[],[f162]) ).
fof(f167,plain,
( ( sP98
& sP97
& sP96
& sP95
& sP94
& sP93
& sP92
& sP91
& sP90
& sP89
& sP88
& sP87
& sP86
& sP85
& sP84
& sP83
& sP82
& sP81
& sP80
& sP79
& sP78
& sP77
& sP76
& sP75
& sP74 )
| ~ sP151 ),
inference(nnf_transformation,[],[f161]) ).
fof(f168,plain,
( ( sP73
& sP72
& sP71
& sP70
& sP69
& sP68
& sP67
& sP66
& sP65
& sP64
& sP63
& sP62
& sP61
& sP60
& sP59
& sP58
& sP57
& sP56
& sP55
& sP54
& sP53
& sP52
& sP51
& sP50
& sP49 )
| ~ sP150 ),
inference(nnf_transformation,[],[f160]) ).
fof(f169,plain,
( ( sP48
& sP47
& sP46
& sP45
& sP44
& sP43
& sP42
& sP41
& sP40
& sP39
& sP38
& sP37
& sP36
& sP35
& sP34
& sP33
& sP32
& sP31
& sP30
& sP29
& sP28
& sP27
& sP26
& sP25
& sP24 )
| ~ sP149 ),
inference(nnf_transformation,[],[f159]) ).
fof(f176,plain,
( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit )
| ~ sP142 ),
inference(nnf_transformation,[],[f152]) ).
fof(f198,plain,
( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit )
| ~ sP120 ),
inference(nnf_transformation,[],[f130]) ).
fof(f199,plain,
( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit )
| ~ sP119 ),
inference(nnf_transformation,[],[f129]) ).
fof(f203,plain,
( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit )
| ~ sP115 ),
inference(nnf_transformation,[],[f125]) ).
fof(f204,plain,
( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit )
| ~ sP114 ),
inference(nnf_transformation,[],[f124]) ).
fof(f212,plain,
( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit )
| ~ sP106 ),
inference(nnf_transformation,[],[f116]) ).
fof(f218,plain,
( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit )
| ~ sP100 ),
inference(nnf_transformation,[],[f110]) ).
fof(f219,plain,
( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit )
| ~ sP99 ),
inference(nnf_transformation,[],[f109]) ).
fof(f223,plain,
( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit )
| ~ sP95 ),
inference(nnf_transformation,[],[f105]) ).
fof(f230,plain,
( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit )
| ~ sP88 ),
inference(nnf_transformation,[],[f98]) ).
fof(f234,plain,
( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit )
| ~ sP84 ),
inference(nnf_transformation,[],[f94]) ).
fof(f235,plain,
( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit )
| ~ sP83 ),
inference(nnf_transformation,[],[f93]) ).
fof(f238,plain,
( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit )
| ~ sP80 ),
inference(nnf_transformation,[],[f90]) ).
fof(f239,plain,
( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit )
| ~ sP79 ),
inference(nnf_transformation,[],[f89]) ).
fof(f241,plain,
( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit )
| ~ sP77 ),
inference(nnf_transformation,[],[f87]) ).
fof(f243,plain,
( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit )
| ~ sP75 ),
inference(nnf_transformation,[],[f85]) ).
fof(f257,plain,
( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit )
| ~ sP61 ),
inference(nnf_transformation,[],[f71]) ).
fof(f288,plain,
( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit )
| ~ sP30 ),
inference(nnf_transformation,[],[f40]) ).
fof(f295,plain,
( ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ~ sP23 ),
inference(nnf_transformation,[],[f33]) ).
fof(f296,plain,
( ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ~ sP22 ),
inference(nnf_transformation,[],[f32]) ).
fof(f297,plain,
( ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ~ sP21 ),
inference(nnf_transformation,[],[f31]) ).
fof(f298,plain,
( ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ~ sP20 ),
inference(nnf_transformation,[],[f30]) ).
fof(f299,plain,
( ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ~ sP19 ),
inference(nnf_transformation,[],[f29]) ).
fof(f300,plain,
( ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ~ sP18 ),
inference(nnf_transformation,[],[f28]) ).
fof(f301,plain,
( ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ~ sP17 ),
inference(nnf_transformation,[],[f27]) ).
fof(f302,plain,
( ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ~ sP16 ),
inference(nnf_transformation,[],[f26]) ).
fof(f303,plain,
( ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ~ sP15 ),
inference(nnf_transformation,[],[f25]) ).
fof(f304,plain,
( ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ~ sP14 ),
inference(nnf_transformation,[],[f24]) ).
fof(f305,plain,
( ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ~ sP13 ),
inference(nnf_transformation,[],[f23]) ).
fof(f306,plain,
( ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ~ sP12 ),
inference(nnf_transformation,[],[f22]) ).
fof(f307,plain,
( ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ~ sP11 ),
inference(nnf_transformation,[],[f21]) ).
fof(f308,plain,
( ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ~ sP10 ),
inference(nnf_transformation,[],[f20]) ).
fof(f309,plain,
( ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ~ sP9 ),
inference(nnf_transformation,[],[f19]) ).
fof(f310,plain,
( ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ~ sP8 ),
inference(nnf_transformation,[],[f18]) ).
fof(f311,plain,
( ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ~ sP7 ),
inference(nnf_transformation,[],[f17]) ).
fof(f312,plain,
( ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ~ sP6 ),
inference(nnf_transformation,[],[f16]) ).
fof(f313,plain,
( ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ~ sP5 ),
inference(nnf_transformation,[],[f15]) ).
fof(f314,plain,
( ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ~ sP4 ),
inference(nnf_transformation,[],[f14]) ).
fof(f315,plain,
( ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ~ sP3 ),
inference(nnf_transformation,[],[f13]) ).
fof(f316,plain,
( ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ~ sP2 ),
inference(nnf_transformation,[],[f12]) ).
fof(f317,plain,
( ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ~ sP1 ),
inference(nnf_transformation,[],[f11]) ).
fof(f318,plain,
( ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 )
| ~ sP0 ),
inference(nnf_transformation,[],[f10]) ).
fof(f319,plain,
( e0 = op(e4,e4)
| e1 = op(e4,e4)
| e2 = op(e4,e4)
| e3 = op(e4,e4)
| e4 = op(e4,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f320,plain,
( e0 = op(e4,e3)
| e1 = op(e4,e3)
| e2 = op(e4,e3)
| e3 = op(e4,e3)
| e4 = op(e4,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f321,plain,
( e0 = op(e4,e2)
| e1 = op(e4,e2)
| e2 = op(e4,e2)
| e3 = op(e4,e2)
| e4 = op(e4,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f322,plain,
( e0 = op(e4,e1)
| e1 = op(e4,e1)
| e2 = op(e4,e1)
| e3 = op(e4,e1)
| e4 = op(e4,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f324,plain,
( e0 = op(e3,e4)
| e1 = op(e3,e4)
| e2 = op(e3,e4)
| e3 = op(e3,e4)
| e4 = op(e3,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f329,plain,
( e0 = op(e2,e4)
| e1 = op(e2,e4)
| e2 = op(e2,e4)
| e3 = op(e2,e4)
| e4 = op(e2,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f330,plain,
( e0 = op(e2,e3)
| e1 = op(e2,e3)
| e2 = op(e2,e3)
| e3 = op(e2,e3)
| e4 = op(e2,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f335,plain,
( e0 = op(e1,e3)
| e1 = op(e1,e3)
| e2 = op(e1,e3)
| e3 = op(e1,e3)
| e4 = op(e1,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f344,plain,
( e0 = unit
| e1 = unit
| e2 = unit
| e3 = unit
| e4 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f345,plain,
e4 = op(e4,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f346,plain,
e4 = op(unit,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f347,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f348,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f349,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f350,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f351,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f352,plain,
e1 = op(unit,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f354,plain,
e0 = op(unit,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f357,plain,
( e3 = op(e0,e4)
| e3 = op(e1,e4)
| e3 = op(e2,e4)
| e3 = op(e3,e4)
| e3 = op(e4,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f361,plain,
( e1 = op(e0,e4)
| e1 = op(e1,e4)
| e1 = op(e2,e4)
| e1 = op(e3,e4)
| e1 = op(e4,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f369,plain,
( e2 = op(e0,e3)
| e2 = op(e1,e3)
| e2 = op(e2,e3)
| e2 = op(e3,e3)
| e2 = op(e4,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f370,plain,
( e2 = op(e3,e0)
| e2 = op(e3,e1)
| e2 = op(e3,e2)
| e2 = op(e3,e3)
| e2 = op(e3,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f371,plain,
( e1 = op(e0,e3)
| e1 = op(e1,e3)
| e1 = op(e2,e3)
| e1 = op(e3,e3)
| e1 = op(e4,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f376,plain,
( e4 = op(e2,e0)
| e4 = op(e2,e1)
| e4 = op(e2,e2)
| e4 = op(e2,e3)
| e4 = op(e2,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f386,plain,
( e4 = op(e1,e0)
| e4 = op(e1,e1)
| e4 = op(e1,e2)
| e4 = op(e1,e3)
| e4 = op(e1,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f405,plain,
op(e4,e3) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f406,plain,
op(e4,e2) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f407,plain,
op(e4,e2) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f408,plain,
op(e4,e1) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f409,plain,
op(e4,e1) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f411,plain,
op(e4,e0) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f413,plain,
op(e4,e0) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f414,plain,
op(e4,e0) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f416,plain,
op(e3,e2) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f417,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f418,plain,
op(e3,e1) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f419,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f421,plain,
op(e3,e0) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f425,plain,
op(e2,e3) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f426,plain,
op(e2,e2) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f431,plain,
op(e2,e0) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f432,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f435,plain,
op(e1,e3) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f436,plain,
op(e1,e2) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f439,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f441,plain,
op(e1,e0) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f444,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f446,plain,
op(e0,e2) != op(e0,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f447,plain,
op(e0,e2) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f449,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f455,plain,
op(e3,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f456,plain,
op(e2,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f457,plain,
op(e2,e4) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f462,plain,
op(e0,e4) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f463,plain,
op(e0,e4) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f464,plain,
op(e0,e4) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f465,plain,
op(e3,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f466,plain,
op(e2,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f467,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f468,plain,
op(e1,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f469,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f471,plain,
op(e0,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f473,plain,
op(e0,e3) != op(e2,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f474,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f476,plain,
op(e2,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f482,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f488,plain,
op(e1,e1) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f496,plain,
op(e2,e0) != op(e4,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f498,plain,
op(e1,e0) != op(e4,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f505,plain,
e3 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f508,plain,
e1 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f509,plain,
e1 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f511,plain,
e0 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f512,plain,
e0 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f515,plain,
e4 = op(op(e2,e2),op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f516,plain,
e3 = op(e2,e2),
inference(cnf_transformation,[],[f6]) ).
fof(f517,plain,
e1 = op(op(e2,e2),e2),
inference(cnf_transformation,[],[f6]) ).
fof(f518,plain,
e0 = op(op(op(e2,e2),e2),op(op(e2,e2),e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f537,plain,
( sP142
| ~ sP153 ),
inference(cnf_transformation,[],[f165]) ).
fof(f544,plain,
( sP99
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f545,plain,
( sP100
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f551,plain,
( sP106
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f559,plain,
( sP114
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f560,plain,
( sP115
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f564,plain,
( sP119
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f565,plain,
( sP120
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f570,plain,
( sP75
| ~ sP151 ),
inference(cnf_transformation,[],[f167]) ).
fof(f572,plain,
( sP77
| ~ sP151 ),
inference(cnf_transformation,[],[f167]) ).
fof(f574,plain,
( sP79
| ~ sP151 ),
inference(cnf_transformation,[],[f167]) ).
fof(f575,plain,
( sP80
| ~ sP151 ),
inference(cnf_transformation,[],[f167]) ).
fof(f578,plain,
( sP83
| ~ sP151 ),
inference(cnf_transformation,[],[f167]) ).
fof(f579,plain,
( sP84
| ~ sP151 ),
inference(cnf_transformation,[],[f167]) ).
fof(f583,plain,
( sP88
| ~ sP151 ),
inference(cnf_transformation,[],[f167]) ).
fof(f590,plain,
( sP95
| ~ sP151 ),
inference(cnf_transformation,[],[f167]) ).
fof(f606,plain,
( sP61
| ~ sP150 ),
inference(cnf_transformation,[],[f168]) ).
fof(f625,plain,
( sP30
| ~ sP149 ),
inference(cnf_transformation,[],[f169]) ).
fof(f656,plain,
( e0 != op(e1,e1)
| e0 != unit
| ~ sP142 ),
inference(cnf_transformation,[],[f176]) ).
fof(f657,plain,
( e0 != op(e1,e1)
| e1 = op(e1,e0)
| ~ sP142 ),
inference(cnf_transformation,[],[f176]) ).
fof(f701,plain,
( e1 != op(e0,e3)
| e3 = op(e0,e1)
| ~ sP120 ),
inference(cnf_transformation,[],[f198]) ).
fof(f703,plain,
( e1 != op(e0,e4)
| e4 = op(e0,e1)
| ~ sP119 ),
inference(cnf_transformation,[],[f199]) ).
fof(f711,plain,
( e1 != op(e1,e3)
| e3 = op(e1,e1)
| ~ sP115 ),
inference(cnf_transformation,[],[f203]) ).
fof(f713,plain,
( e1 != op(e1,e4)
| e4 = op(e1,e1)
| ~ sP114 ),
inference(cnf_transformation,[],[f204]) ).
fof(f729,plain,
( e1 != op(e3,e2)
| e2 = op(e3,e1)
| ~ sP106 ),
inference(cnf_transformation,[],[f212]) ).
fof(f741,plain,
( e1 != op(e4,e3)
| e3 = op(e4,e1)
| ~ sP100 ),
inference(cnf_transformation,[],[f218]) ).
fof(f743,plain,
( e1 != op(e4,e4)
| e4 = op(e4,e1)
| ~ sP99 ),
inference(cnf_transformation,[],[f219]) ).
fof(f751,plain,
( e2 != op(e0,e3)
| e3 = op(e0,e2)
| ~ sP95 ),
inference(cnf_transformation,[],[f223]) ).
fof(f765,plain,
( e2 != op(e2,e0)
| e0 = op(e2,e2)
| ~ sP88 ),
inference(cnf_transformation,[],[f230]) ).
fof(f773,plain,
( e2 != op(e2,e4)
| e4 = op(e2,e2)
| ~ sP84 ),
inference(cnf_transformation,[],[f234]) ).
fof(f775,plain,
( e2 != op(e3,e0)
| e0 = op(e3,e2)
| ~ sP83 ),
inference(cnf_transformation,[],[f235]) ).
fof(f781,plain,
( e2 != op(e3,e3)
| e3 = op(e3,e2)
| ~ sP80 ),
inference(cnf_transformation,[],[f238]) ).
fof(f783,plain,
( e2 != op(e3,e4)
| e4 = op(e3,e2)
| ~ sP79 ),
inference(cnf_transformation,[],[f239]) ).
fof(f787,plain,
( e2 != op(e4,e1)
| e1 = op(e4,e2)
| ~ sP77 ),
inference(cnf_transformation,[],[f241]) ).
fof(f791,plain,
( e2 != op(e4,e3)
| e3 = op(e4,e2)
| ~ sP75 ),
inference(cnf_transformation,[],[f243]) ).
fof(f819,plain,
( e3 != op(e2,e2)
| e2 = op(e2,e3)
| ~ sP61 ),
inference(cnf_transformation,[],[f257]) ).
fof(f880,plain,
( e4 != op(e3,e3)
| e4 != unit
| ~ sP30 ),
inference(cnf_transformation,[],[f288]) ).
fof(f881,plain,
( e4 != op(e3,e3)
| e3 = op(e3,e4)
| ~ sP30 ),
inference(cnf_transformation,[],[f288]) ).
fof(f896,plain,
( op(e0,e1) != op(e1,e0)
| ~ sP23 ),
inference(cnf_transformation,[],[f295]) ).
fof(f899,plain,
( op(e0,e2) != op(e2,e0)
| ~ sP22 ),
inference(cnf_transformation,[],[f296]) ).
fof(f902,plain,
( op(e0,e3) != op(e3,e0)
| ~ sP21 ),
inference(cnf_transformation,[],[f297]) ).
fof(f905,plain,
( op(e0,e4) != op(e4,e0)
| ~ sP20 ),
inference(cnf_transformation,[],[f298]) ).
fof(f908,plain,
( op(e0,e1) != op(e1,e0)
| ~ sP19 ),
inference(cnf_transformation,[],[f299]) ).
fof(f911,plain,
( op(e1,e1) != op(e1,e1)
| ~ sP18 ),
inference(cnf_transformation,[],[f300]) ).
fof(f914,plain,
( op(e1,e2) != op(e2,e1)
| ~ sP17 ),
inference(cnf_transformation,[],[f301]) ).
fof(f917,plain,
( op(e1,e3) != op(e3,e1)
| ~ sP16 ),
inference(cnf_transformation,[],[f302]) ).
fof(f920,plain,
( op(e1,e4) != op(e4,e1)
| ~ sP15 ),
inference(cnf_transformation,[],[f303]) ).
fof(f923,plain,
( op(e0,e2) != op(e2,e0)
| ~ sP14 ),
inference(cnf_transformation,[],[f304]) ).
fof(f926,plain,
( op(e1,e2) != op(e2,e1)
| ~ sP13 ),
inference(cnf_transformation,[],[f305]) ).
fof(f929,plain,
( op(e2,e2) != op(e2,e2)
| ~ sP12 ),
inference(cnf_transformation,[],[f306]) ).
fof(f931,plain,
( e2 = op(op(e2,e3),e3)
| ~ sP11 ),
inference(cnf_transformation,[],[f307]) ).
fof(f932,plain,
( op(e2,e3) != op(e3,e2)
| ~ sP11 ),
inference(cnf_transformation,[],[f307]) ).
fof(f933,plain,
( e4 != op(op(e2,e4),e2)
| ~ sP10 ),
inference(cnf_transformation,[],[f308]) ).
fof(f938,plain,
( op(e0,e3) != op(e3,e0)
| ~ sP9 ),
inference(cnf_transformation,[],[f309]) ).
fof(f941,plain,
( op(e1,e3) != op(e3,e1)
| ~ sP8 ),
inference(cnf_transformation,[],[f310]) ).
fof(f943,plain,
( e3 = op(op(e3,e2),e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f311]) ).
fof(f947,plain,
( op(e3,e3) != op(e3,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f312]) ).
fof(f949,plain,
( e3 = op(op(e3,e4),e4)
| ~ sP5 ),
inference(cnf_transformation,[],[f313]) ).
fof(f953,plain,
( op(e0,e4) != op(e4,e0)
| ~ sP4 ),
inference(cnf_transformation,[],[f314]) ).
fof(f955,plain,
( e4 = op(op(e4,e1),e1)
| ~ sP3 ),
inference(cnf_transformation,[],[f315]) ).
fof(f958,plain,
( e4 = op(op(e4,e2),e2)
| ~ sP2 ),
inference(cnf_transformation,[],[f316]) ).
fof(f961,plain,
( e4 = op(op(e4,e3),e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f317]) ).
fof(f965,plain,
( op(e4,e4) != op(e4,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f318]) ).
fof(f968,plain,
( op(e0,e0) != op(e0,e0)
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f164]) ).
fof(f969,plain,
( sP153
| sP152
| sP151
| sP150
| sP149 ),
inference(cnf_transformation,[],[f164]) ).
fof(f970,plain,
( sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(trivial_inequality_removal,[],[f968]) ).
fof(f971,plain,
~ sP0,
inference(trivial_inequality_removal,[],[f965]) ).
fof(f972,plain,
~ sP6,
inference(trivial_inequality_removal,[],[f947]) ).
fof(f973,plain,
~ sP12,
inference(trivial_inequality_removal,[],[f929]) ).
fof(f974,plain,
~ sP18,
inference(trivial_inequality_removal,[],[f911]) ).
fof(f976,definition,
( spl154_1
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl154_1])],[avatar_definition]) ).
fof(f980,definition,
( spl154_2
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl154_2])],[avatar_definition]) ).
fof(f984,definition,
( spl154_3
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl154_3])],[avatar_definition]) ).
fof(f988,definition,
( spl154_4
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl154_4])],[avatar_definition]) ).
fof(f992,definition,
( spl154_5
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl154_5])],[avatar_definition]) ).
fof(f996,definition,
( spl154_6
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl154_6])],[avatar_definition]) ).
fof(f1000,definition,
( spl154_7
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl154_7])],[avatar_definition]) ).
fof(f1004,definition,
( spl154_8
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl154_8])],[avatar_definition]) ).
fof(f1008,definition,
( spl154_9
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl154_9])],[avatar_definition]) ).
fof(f1012,definition,
( spl154_10
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl154_10])],[avatar_definition]) ).
fof(f1016,definition,
( spl154_11
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl154_11])],[avatar_definition]) ).
fof(f1020,definition,
( spl154_12
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl154_12])],[avatar_definition]) ).
fof(f1024,definition,
( spl154_13
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl154_13])],[avatar_definition]) ).
fof(f1028,definition,
( spl154_14
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl154_14])],[avatar_definition]) ).
fof(f1032,definition,
( spl154_15
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl154_15])],[avatar_definition]) ).
fof(f1036,definition,
( spl154_16
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl154_16])],[avatar_definition]) ).
fof(f1040,definition,
( spl154_17
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl154_17])],[avatar_definition]) ).
fof(f1044,definition,
( spl154_18
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl154_18])],[avatar_definition]) ).
fof(f1048,definition,
( spl154_19
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl154_19])],[avatar_definition]) ).
fof(f1052,definition,
( spl154_20
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl154_20])],[avatar_definition]) ).
fof(f1056,definition,
( spl154_21
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl154_21])],[avatar_definition]) ).
fof(f1060,definition,
( spl154_22
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl154_22])],[avatar_definition]) ).
fof(f1064,definition,
( spl154_23
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl154_23])],[avatar_definition]) ).
fof(f1068,definition,
( spl154_24
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl154_24])],[avatar_definition]) ).
fof(f1077,plain,
( spl154_1
| spl154_2
| spl154_3
| spl154_4
| spl154_5
| spl154_6
| spl154_7
| spl154_8
| spl154_9
| spl154_10
| spl154_11
| spl154_12
| spl154_13
| spl154_14
| spl154_15
| spl154_16
| spl154_17
| spl154_18
| spl154_19
| spl154_20
| spl154_21
| spl154_22
| spl154_23
| spl154_24 ),
inference(avatar_split_clause,[],[f970,f1068,f1064,f1060,f1056,f1052,f1048,f1044,f1040,f1036,f1032,f1028,f1024,f1020,f1016,f1012,f1008,f1004,f1000,f996,f992,f988,f984,f980,f976]) ).
fof(f1079,definition,
( spl154_26
<=> sP149 ),
introduced(definition,[new_symbols(definition,[spl154_26])],[avatar_definition]) ).
fof(f1083,definition,
( spl154_27
<=> sP150 ),
introduced(definition,[new_symbols(definition,[spl154_27])],[avatar_definition]) ).
fof(f1087,definition,
( spl154_28
<=> sP151 ),
introduced(definition,[new_symbols(definition,[spl154_28])],[avatar_definition]) ).
fof(f1091,definition,
( spl154_29
<=> sP152 ),
introduced(definition,[new_symbols(definition,[spl154_29])],[avatar_definition]) ).
fof(f1095,definition,
( spl154_30
<=> sP153 ),
introduced(definition,[new_symbols(definition,[spl154_30])],[avatar_definition]) ).
fof(f1098,plain,
( spl154_26
| spl154_27
| spl154_28
| spl154_29
| spl154_30 ),
inference(avatar_split_clause,[],[f969,f1095,f1091,f1087,f1083,f1079]) ).
fof(f1105,plain,
~ spl154_1,
inference(avatar_split_clause,[],[f971,f976]) ).
fof(f1112,definition,
( spl154_33
<=> e4 = op(op(e4,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl154_33])],[avatar_definition]) ).
fof(f1114,plain,
( e4 = op(op(e4,e3),e3)
| ~ spl154_33 ),
inference(avatar_component_clause,[],[f1112]) ).
fof(f1115,plain,
( ~ spl154_2
| spl154_33 ),
inference(avatar_split_clause,[],[f961,f1112,f980]) ).
fof(f1127,definition,
( spl154_36
<=> e4 = op(op(e4,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl154_36])],[avatar_definition]) ).
fof(f1129,plain,
( e4 = op(op(e4,e2),e2)
| ~ spl154_36 ),
inference(avatar_component_clause,[],[f1127]) ).
fof(f1130,plain,
( ~ spl154_3
| spl154_36 ),
inference(avatar_split_clause,[],[f958,f1127,f984]) ).
fof(f1142,definition,
( spl154_39
<=> e4 = op(op(e4,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl154_39])],[avatar_definition]) ).
fof(f1144,plain,
( e4 = op(op(e4,e1),e1)
| ~ spl154_39 ),
inference(avatar_component_clause,[],[f1142]) ).
fof(f1145,plain,
( ~ spl154_4
| spl154_39 ),
inference(avatar_split_clause,[],[f955,f1142,f988]) ).
fof(f1147,definition,
( spl154_40
<=> op(e1,e4) = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl154_40])],[avatar_definition]) ).
fof(f1149,plain,
( op(e1,e4) != op(e4,e1)
| spl154_40 ),
inference(avatar_component_clause,[],[f1147]) ).
fof(f1162,definition,
( spl154_43
<=> op(e0,e4) = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl154_43])],[avatar_definition]) ).
fof(f1164,plain,
( op(e0,e4) != op(e4,e0)
| spl154_43 ),
inference(avatar_component_clause,[],[f1162]) ).
fof(f1165,plain,
( ~ spl154_5
| ~ spl154_43 ),
inference(avatar_split_clause,[],[f953,f1162,f992]) ).
fof(f1172,definition,
( spl154_45
<=> e3 = op(op(e3,e4),e4) ),
introduced(definition,[new_symbols(definition,[spl154_45])],[avatar_definition]) ).
fof(f1174,plain,
( e3 = op(op(e3,e4),e4)
| ~ spl154_45 ),
inference(avatar_component_clause,[],[f1172]) ).
fof(f1175,plain,
( ~ spl154_6
| spl154_45 ),
inference(avatar_split_clause,[],[f949,f1172,f996]) ).
fof(f1183,plain,
~ spl154_7,
inference(avatar_split_clause,[],[f972,f1000]) ).
fof(f1190,definition,
( spl154_48
<=> e3 = op(op(e3,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl154_48])],[avatar_definition]) ).
fof(f1192,plain,
( e3 = op(op(e3,e2),e2)
| ~ spl154_48 ),
inference(avatar_component_clause,[],[f1190]) ).
fof(f1193,plain,
( ~ spl154_8
| spl154_48 ),
inference(avatar_split_clause,[],[f943,f1190,f1004]) ).
fof(f1195,definition,
( spl154_49
<=> op(e2,e3) = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl154_49])],[avatar_definition]) ).
fof(f1197,plain,
( op(e2,e3) != op(e3,e2)
| spl154_49 ),
inference(avatar_component_clause,[],[f1195]) ).
fof(f1210,definition,
( spl154_52
<=> op(e1,e3) = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl154_52])],[avatar_definition]) ).
fof(f1212,plain,
( op(e1,e3) != op(e3,e1)
| spl154_52 ),
inference(avatar_component_clause,[],[f1210]) ).
fof(f1213,plain,
( ~ spl154_9
| ~ spl154_52 ),
inference(avatar_split_clause,[],[f941,f1210,f1008]) ).
fof(f1225,definition,
( spl154_55
<=> op(e0,e3) = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl154_55])],[avatar_definition]) ).
fof(f1227,plain,
( op(e0,e3) != op(e3,e0)
| spl154_55 ),
inference(avatar_component_clause,[],[f1225]) ).
fof(f1228,plain,
( ~ spl154_10
| ~ spl154_55 ),
inference(avatar_split_clause,[],[f938,f1225,f1012]) ).
fof(f1230,definition,
( spl154_56
<=> e4 = op(op(e2,e4),e2) ),
introduced(definition,[new_symbols(definition,[spl154_56])],[avatar_definition]) ).
fof(f1232,plain,
( e4 != op(op(e2,e4),e2)
| spl154_56 ),
inference(avatar_component_clause,[],[f1230]) ).
fof(f1233,plain,
( ~ spl154_11
| ~ spl154_56 ),
inference(avatar_split_clause,[],[f933,f1230,f1016]) ).
fof(f1246,definition,
( spl154_59
<=> e2 = op(op(e2,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl154_59])],[avatar_definition]) ).
fof(f1248,plain,
( e2 = op(op(e2,e3),e3)
| ~ spl154_59 ),
inference(avatar_component_clause,[],[f1246]) ).
fof(f1249,plain,
( ~ spl154_12
| spl154_59 ),
inference(avatar_split_clause,[],[f931,f1246,f1020]) ).
fof(f1250,plain,
( ~ spl154_12
| ~ spl154_49 ),
inference(avatar_split_clause,[],[f932,f1195,f1020]) ).
fof(f1257,plain,
~ spl154_13,
inference(avatar_split_clause,[],[f973,f1024]) ).
fof(f1269,definition,
( spl154_63
<=> op(e1,e2) = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl154_63])],[avatar_definition]) ).
fof(f1271,plain,
( op(e1,e2) != op(e2,e1)
| spl154_63 ),
inference(avatar_component_clause,[],[f1269]) ).
fof(f1272,plain,
( ~ spl154_14
| ~ spl154_63 ),
inference(avatar_split_clause,[],[f926,f1269,f1028]) ).
fof(f1284,definition,
( spl154_66
<=> op(e0,e2) = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl154_66])],[avatar_definition]) ).
fof(f1286,plain,
( op(e0,e2) != op(e2,e0)
| spl154_66 ),
inference(avatar_component_clause,[],[f1284]) ).
fof(f1287,plain,
( ~ spl154_15
| ~ spl154_66 ),
inference(avatar_split_clause,[],[f923,f1284,f1032]) ).
fof(f1298,plain,
( ~ spl154_16
| ~ spl154_40 ),
inference(avatar_split_clause,[],[f920,f1147,f1036]) ).
fof(f1309,plain,
( ~ spl154_17
| ~ spl154_52 ),
inference(avatar_split_clause,[],[f917,f1210,f1040]) ).
fof(f1320,plain,
( ~ spl154_18
| ~ spl154_63 ),
inference(avatar_split_clause,[],[f914,f1269,f1044]) ).
fof(f1327,plain,
~ spl154_19,
inference(avatar_split_clause,[],[f974,f1048]) ).
fof(f1339,definition,
( spl154_76
<=> op(e0,e1) = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl154_76])],[avatar_definition]) ).
fof(f1341,plain,
( op(e0,e1) != op(e1,e0)
| spl154_76 ),
inference(avatar_component_clause,[],[f1339]) ).
fof(f1342,plain,
( ~ spl154_20
| ~ spl154_76 ),
inference(avatar_split_clause,[],[f908,f1339,f1052]) ).
fof(f1353,plain,
( ~ spl154_21
| ~ spl154_43 ),
inference(avatar_split_clause,[],[f905,f1162,f1056]) ).
fof(f1364,plain,
( ~ spl154_22
| ~ spl154_55 ),
inference(avatar_split_clause,[],[f902,f1225,f1060]) ).
fof(f1375,plain,
( ~ spl154_23
| ~ spl154_66 ),
inference(avatar_split_clause,[],[f899,f1284,f1064]) ).
fof(f1386,plain,
( ~ spl154_24
| ~ spl154_76 ),
inference(avatar_split_clause,[],[f896,f1339,f1068]) ).
fof(f1392,definition,
( spl154_86
<=> e4 = unit ),
introduced(definition,[new_symbols(definition,[spl154_86])],[avatar_definition]) ).
fof(f1393,plain,
( e4 = unit
| ~ spl154_86 ),
inference(avatar_component_clause,[],[f1392]) ).
fof(f1396,definition,
( spl154_87
<=> e4 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl154_87])],[avatar_definition]) ).
fof(f1397,plain,
( e4 = op(e4,e4)
| ~ spl154_87 ),
inference(avatar_component_clause,[],[f1396]) ).
fof(f1405,definition,
( spl154_89
<=> e4 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl154_89])],[avatar_definition]) ).
fof(f1406,plain,
( e4 = op(e4,e3)
| ~ spl154_89 ),
inference(avatar_component_clause,[],[f1405]) ).
fof(f1410,definition,
( spl154_90
<=> e3 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl154_90])],[avatar_definition]) ).
fof(f1412,plain,
( e3 = op(e4,e4)
| ~ spl154_90 ),
inference(avatar_component_clause,[],[f1410]) ).
fof(f1419,definition,
( spl154_92
<=> e4 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl154_92])],[avatar_definition]) ).
fof(f1424,definition,
( spl154_93
<=> e2 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl154_93])],[avatar_definition]) ).
fof(f1426,plain,
( e2 = op(e4,e4)
| ~ spl154_93 ),
inference(avatar_component_clause,[],[f1424]) ).
fof(f1433,definition,
( spl154_95
<=> e4 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl154_95])],[avatar_definition]) ).
fof(f1434,plain,
( e4 = op(e4,e1)
| ~ spl154_95 ),
inference(avatar_component_clause,[],[f1433]) ).
fof(f1438,definition,
( spl154_96
<=> e1 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl154_96])],[avatar_definition]) ).
fof(f1440,plain,
( e1 = op(e4,e4)
| ~ spl154_96 ),
inference(avatar_component_clause,[],[f1438]) ).
fof(f1447,definition,
( spl154_98
<=> e4 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl154_98])],[avatar_definition]) ).
fof(f1448,plain,
( e4 = op(e4,e0)
| ~ spl154_98 ),
inference(avatar_component_clause,[],[f1447]) ).
fof(f1452,definition,
( spl154_99
<=> e0 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl154_99])],[avatar_definition]) ).
fof(f1454,plain,
( e0 = op(e4,e4)
| ~ spl154_99 ),
inference(avatar_component_clause,[],[f1452]) ).
fof(f1461,definition,
( spl154_101
<=> e4 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl154_101])],[avatar_definition]) ).
fof(f1462,plain,
( e4 = op(e3,e4)
| ~ spl154_101 ),
inference(avatar_component_clause,[],[f1461]) ).
fof(f1466,definition,
( spl154_102
<=> sP30 ),
introduced(definition,[new_symbols(definition,[spl154_102])],[avatar_definition]) ).
fof(f1470,definition,
( spl154_103
<=> e4 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl154_103])],[avatar_definition]) ).
fof(f1471,plain,
( e4 = op(e3,e3)
| ~ spl154_103 ),
inference(avatar_component_clause,[],[f1470]) ).
fof(f1473,plain,
( ~ spl154_102
| ~ spl154_86
| ~ spl154_103 ),
inference(avatar_split_clause,[],[f880,f1470,f1392,f1466]) ).
fof(f1475,definition,
( spl154_104
<=> e3 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl154_104])],[avatar_definition]) ).
fof(f1477,plain,
( e3 = op(e3,e4)
| ~ spl154_104 ),
inference(avatar_component_clause,[],[f1475]) ).
fof(f1478,plain,
( ~ spl154_102
| spl154_104
| ~ spl154_103 ),
inference(avatar_split_clause,[],[f881,f1470,f1475,f1466]) ).
fof(f1484,definition,
( spl154_106
<=> e4 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl154_106])],[avatar_definition]) ).
fof(f1489,definition,
( spl154_107
<=> e2 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl154_107])],[avatar_definition]) ).
fof(f1491,plain,
( e2 = op(e3,e4)
| ~ spl154_107 ),
inference(avatar_component_clause,[],[f1489]) ).
fof(f1498,definition,
( spl154_109
<=> e4 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl154_109])],[avatar_definition]) ).
fof(f1500,plain,
( e4 != op(e3,e1)
| spl154_109 ),
inference(avatar_component_clause,[],[f1498]) ).
fof(f1503,definition,
( spl154_110
<=> e1 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl154_110])],[avatar_definition]) ).
fof(f1505,plain,
( e1 = op(e3,e4)
| ~ spl154_110 ),
inference(avatar_component_clause,[],[f1503]) ).
fof(f1517,definition,
( spl154_113
<=> e0 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl154_113])],[avatar_definition]) ).
fof(f1519,plain,
( e0 = op(e3,e4)
| ~ spl154_113 ),
inference(avatar_component_clause,[],[f1517]) ).
fof(f1526,definition,
( spl154_115
<=> e4 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl154_115])],[avatar_definition]) ).
fof(f1535,definition,
( spl154_117
<=> e4 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl154_117])],[avatar_definition]) ).
fof(f1540,definition,
( spl154_118
<=> e3 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl154_118])],[avatar_definition]) ).
fof(f1542,plain,
( e3 = op(e2,e4)
| ~ spl154_118 ),
inference(avatar_component_clause,[],[f1540]) ).
fof(f1549,definition,
( spl154_120
<=> e4 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl154_120])],[avatar_definition]) ).
fof(f1550,plain,
( e4 = op(e2,e2)
| ~ spl154_120 ),
inference(avatar_component_clause,[],[f1549]) ).
fof(f1554,definition,
( spl154_121
<=> e2 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl154_121])],[avatar_definition]) ).
fof(f1556,plain,
( e2 = op(e2,e4)
| ~ spl154_121 ),
inference(avatar_component_clause,[],[f1554]) ).
fof(f1563,definition,
( spl154_123
<=> e4 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl154_123])],[avatar_definition]) ).
fof(f1568,definition,
( spl154_124
<=> e1 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl154_124])],[avatar_definition]) ).
fof(f1570,plain,
( e1 = op(e2,e4)
| ~ spl154_124 ),
inference(avatar_component_clause,[],[f1568]) ).
fof(f1577,definition,
( spl154_126
<=> e4 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl154_126])],[avatar_definition]) ).
fof(f1582,definition,
( spl154_127
<=> e0 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl154_127])],[avatar_definition]) ).
fof(f1584,plain,
( e0 = op(e2,e4)
| ~ spl154_127 ),
inference(avatar_component_clause,[],[f1582]) ).
fof(f1591,definition,
( spl154_129
<=> e4 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl154_129])],[avatar_definition]) ).
fof(f1592,plain,
( e4 = op(e1,e4)
| ~ spl154_129 ),
inference(avatar_component_clause,[],[f1591]) ).
fof(f1600,definition,
( spl154_131
<=> e4 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl154_131])],[avatar_definition]) ).
fof(f1602,plain,
( e4 != op(e1,e3)
| spl154_131 ),
inference(avatar_component_clause,[],[f1600]) ).
fof(f1605,definition,
( spl154_132
<=> e3 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl154_132])],[avatar_definition]) ).
fof(f1607,plain,
( e3 = op(e1,e4)
| ~ spl154_132 ),
inference(avatar_component_clause,[],[f1605]) ).
fof(f1614,definition,
( spl154_134
<=> e4 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl154_134])],[avatar_definition]) ).
fof(f1615,plain,
( e4 = op(e1,e2)
| ~ spl154_134 ),
inference(avatar_component_clause,[],[f1614]) ).
fof(f1628,definition,
( spl154_137
<=> e4 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl154_137])],[avatar_definition]) ).
fof(f1629,plain,
( e4 = op(e1,e1)
| ~ spl154_137 ),
inference(avatar_component_clause,[],[f1628]) ).
fof(f1633,definition,
( spl154_138
<=> e1 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl154_138])],[avatar_definition]) ).
fof(f1635,plain,
( e1 = op(e1,e4)
| ~ spl154_138 ),
inference(avatar_component_clause,[],[f1633]) ).
fof(f1642,definition,
( spl154_140
<=> e4 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl154_140])],[avatar_definition]) ).
fof(f1656,definition,
( spl154_143
<=> e4 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl154_143])],[avatar_definition]) ).
fof(f1657,plain,
( e4 = op(e0,e4)
| ~ spl154_143 ),
inference(avatar_component_clause,[],[f1656]) ).
fof(f1670,definition,
( spl154_146
<=> e3 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl154_146])],[avatar_definition]) ).
fof(f1672,plain,
( e3 = op(e0,e4)
| ~ spl154_146 ),
inference(avatar_component_clause,[],[f1670]) ).
fof(f1679,definition,
( spl154_148
<=> e4 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl154_148])],[avatar_definition]) ).
fof(f1681,plain,
( e4 != op(e0,e2)
| spl154_148 ),
inference(avatar_component_clause,[],[f1679]) ).
fof(f1693,definition,
( spl154_151
<=> e4 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl154_151])],[avatar_definition]) ).
fof(f1694,plain,
( e4 = op(e0,e1)
| ~ spl154_151 ),
inference(avatar_component_clause,[],[f1693]) ).
fof(f1698,definition,
( spl154_152
<=> e1 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl154_152])],[avatar_definition]) ).
fof(f1721,definition,
( spl154_157
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl154_157])],[avatar_definition]) ).
fof(f1722,plain,
( e3 = unit
| ~ spl154_157 ),
inference(avatar_component_clause,[],[f1721]) ).
fof(f1731,definition,
( spl154_159
<=> e3 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl154_159])],[avatar_definition]) ).
fof(f1732,plain,
( e3 = op(e4,e3)
| ~ spl154_159 ),
inference(avatar_component_clause,[],[f1731]) ).
fof(f1740,definition,
( spl154_161
<=> e3 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl154_161])],[avatar_definition]) ).
fof(f1741,plain,
( e3 = op(e4,e2)
| ~ spl154_161 ),
inference(avatar_component_clause,[],[f1740]) ).
fof(f1745,definition,
( spl154_162
<=> e2 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl154_162])],[avatar_definition]) ).
fof(f1747,plain,
( e2 = op(e4,e3)
| ~ spl154_162 ),
inference(avatar_component_clause,[],[f1745]) ).
fof(f1754,definition,
( spl154_164
<=> e3 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl154_164])],[avatar_definition]) ).
fof(f1755,plain,
( e3 = op(e4,e1)
| ~ spl154_164 ),
inference(avatar_component_clause,[],[f1754]) ).
fof(f1759,definition,
( spl154_165
<=> e1 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl154_165])],[avatar_definition]) ).
fof(f1761,plain,
( e1 = op(e4,e3)
| ~ spl154_165 ),
inference(avatar_component_clause,[],[f1759]) ).
fof(f1773,definition,
( spl154_168
<=> e0 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl154_168])],[avatar_definition]) ).
fof(f1775,plain,
( e0 = op(e4,e3)
| ~ spl154_168 ),
inference(avatar_component_clause,[],[f1773]) ).
fof(f1797,definition,
( spl154_173
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl154_173])],[avatar_definition]) ).
fof(f1798,plain,
( e3 = op(e3,e2)
| ~ spl154_173 ),
inference(avatar_component_clause,[],[f1797]) ).
fof(f1802,definition,
( spl154_174
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl154_174])],[avatar_definition]) ).
fof(f1816,definition,
( spl154_177
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl154_177])],[avatar_definition]) ).
fof(f1818,plain,
( e1 = op(e3,e3)
| ~ spl154_177 ),
inference(avatar_component_clause,[],[f1816]) ).
fof(f1825,definition,
( spl154_179
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl154_179])],[avatar_definition]) ).
fof(f1826,plain,
( e3 = op(e3,e0)
| ~ spl154_179 ),
inference(avatar_component_clause,[],[f1825]) ).
fof(f1845,definition,
( spl154_183
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl154_183])],[avatar_definition]) ).
fof(f1850,definition,
( spl154_184
<=> sP61 ),
introduced(definition,[new_symbols(definition,[spl154_184])],[avatar_definition]) ).
fof(f1854,definition,
( spl154_185
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl154_185])],[avatar_definition]) ).
fof(f1855,plain,
( e3 = op(e2,e2)
| ~ spl154_185 ),
inference(avatar_component_clause,[],[f1854]) ).
fof(f1859,definition,
( spl154_186
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl154_186])],[avatar_definition]) ).
fof(f1861,plain,
( e2 = op(e2,e3)
| ~ spl154_186 ),
inference(avatar_component_clause,[],[f1859]) ).
fof(f1862,plain,
( ~ spl154_184
| spl154_186
| ~ spl154_185 ),
inference(avatar_split_clause,[],[f819,f1854,f1859,f1850]) ).
fof(f1873,definition,
( spl154_189
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl154_189])],[avatar_definition]) ).
fof(f1887,definition,
( spl154_192
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl154_192])],[avatar_definition]) ).
fof(f1889,plain,
( e0 = op(e2,e3)
| ~ spl154_192 ),
inference(avatar_component_clause,[],[f1887]) ).
fof(f1902,definition,
( spl154_195
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl154_195])],[avatar_definition]) ).
fof(f1911,definition,
( spl154_197
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl154_197])],[avatar_definition]) ).
fof(f1916,definition,
( spl154_198
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl154_198])],[avatar_definition]) ).
fof(f1918,plain,
( e2 = op(e1,e3)
| ~ spl154_198 ),
inference(avatar_component_clause,[],[f1916]) ).
fof(f1925,definition,
( spl154_200
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl154_200])],[avatar_definition]) ).
fof(f1926,plain,
( e3 = op(e1,e1)
| ~ spl154_200 ),
inference(avatar_component_clause,[],[f1925]) ).
fof(f1930,definition,
( spl154_201
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl154_201])],[avatar_definition]) ).
fof(f1944,definition,
( spl154_204
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl154_204])],[avatar_definition]) ).
fof(f1946,plain,
( e0 = op(e1,e3)
| ~ spl154_204 ),
inference(avatar_component_clause,[],[f1944]) ).
fof(f1959,definition,
( spl154_207
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl154_207])],[avatar_definition]) ).
fof(f1960,plain,
( e3 = op(e0,e3)
| ~ spl154_207 ),
inference(avatar_component_clause,[],[f1959]) ).
fof(f1968,definition,
( spl154_209
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl154_209])],[avatar_definition]) ).
fof(f1973,definition,
( spl154_210
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl154_210])],[avatar_definition]) ).
fof(f1982,definition,
( spl154_212
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl154_212])],[avatar_definition]) ).
fof(f1987,definition,
( spl154_213
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl154_213])],[avatar_definition]) ).
fof(f2010,definition,
( spl154_218
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl154_218])],[avatar_definition]) ).
fof(f2011,plain,
( e2 = unit
| ~ spl154_218 ),
inference(avatar_component_clause,[],[f2010]) ).
fof(f2016,definition,
( spl154_219
<=> sP75 ),
introduced(definition,[new_symbols(definition,[spl154_219])],[avatar_definition]) ).
fof(f2020,plain,
( ~ spl154_219
| spl154_161
| ~ spl154_162 ),
inference(avatar_split_clause,[],[f791,f1745,f1740,f2016]) ).
fof(f2026,definition,
( spl154_221
<=> e2 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl154_221])],[avatar_definition]) ).
fof(f2031,definition,
( spl154_222
<=> sP77 ),
introduced(definition,[new_symbols(definition,[spl154_222])],[avatar_definition]) ).
fof(f2035,definition,
( spl154_223
<=> e2 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl154_223])],[avatar_definition]) ).
fof(f2040,definition,
( spl154_224
<=> e1 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl154_224])],[avatar_definition]) ).
fof(f2043,plain,
( ~ spl154_222
| spl154_224
| ~ spl154_223 ),
inference(avatar_split_clause,[],[f787,f2035,f2040,f2031]) ).
fof(f2054,definition,
( spl154_227
<=> e0 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl154_227])],[avatar_definition]) ).
fof(f2056,plain,
( e0 = op(e4,e2)
| ~ spl154_227 ),
inference(avatar_component_clause,[],[f2054]) ).
fof(f2059,definition,
( spl154_228
<=> sP79 ),
introduced(definition,[new_symbols(definition,[spl154_228])],[avatar_definition]) ).
fof(f2063,plain,
( ~ spl154_228
| spl154_106
| ~ spl154_107 ),
inference(avatar_split_clause,[],[f783,f1489,f1484,f2059]) ).
fof(f2065,definition,
( spl154_229
<=> sP80 ),
introduced(definition,[new_symbols(definition,[spl154_229])],[avatar_definition]) ).
fof(f2069,plain,
( ~ spl154_229
| spl154_173
| ~ spl154_174 ),
inference(avatar_split_clause,[],[f781,f1802,f1797,f2065]) ).
fof(f2075,definition,
( spl154_231
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl154_231])],[avatar_definition]) ).
fof(f2076,plain,
( e2 = op(e3,e2)
| ~ spl154_231 ),
inference(avatar_component_clause,[],[f2075]) ).
fof(f2084,definition,
( spl154_233
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl154_233])],[avatar_definition]) ).
fof(f2085,plain,
( e2 = op(e3,e1)
| ~ spl154_233 ),
inference(avatar_component_clause,[],[f2084]) ).
fof(f2089,definition,
( spl154_234
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl154_234])],[avatar_definition]) ).
fof(f2091,plain,
( e1 = op(e3,e2)
| ~ spl154_234 ),
inference(avatar_component_clause,[],[f2089]) ).
fof(f2094,definition,
( spl154_235
<=> sP83 ),
introduced(definition,[new_symbols(definition,[spl154_235])],[avatar_definition]) ).
fof(f2098,definition,
( spl154_236
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl154_236])],[avatar_definition]) ).
fof(f2103,definition,
( spl154_237
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl154_237])],[avatar_definition]) ).
fof(f2106,plain,
( ~ spl154_235
| spl154_237
| ~ spl154_236 ),
inference(avatar_split_clause,[],[f775,f2098,f2103,f2094]) ).
fof(f2108,definition,
( spl154_238
<=> sP84 ),
introduced(definition,[new_symbols(definition,[spl154_238])],[avatar_definition]) ).
fof(f2112,plain,
( ~ spl154_238
| spl154_120
| ~ spl154_121 ),
inference(avatar_split_clause,[],[f773,f1554,f1549,f2108]) ).
fof(f2143,definition,
( spl154_245
<=> sP88 ),
introduced(definition,[new_symbols(definition,[spl154_245])],[avatar_definition]) ).
fof(f2147,definition,
( spl154_246
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl154_246])],[avatar_definition]) ).
fof(f2152,definition,
( spl154_247
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl154_247])],[avatar_definition]) ).
fof(f2155,plain,
( ~ spl154_245
| spl154_247
| ~ spl154_246 ),
inference(avatar_split_clause,[],[f765,f2147,f2152,f2143]) ).
fof(f2212,definition,
( spl154_259
<=> sP95 ),
introduced(definition,[new_symbols(definition,[spl154_259])],[avatar_definition]) ).
fof(f2216,plain,
( ~ spl154_259
| spl154_209
| ~ spl154_210 ),
inference(avatar_split_clause,[],[f751,f1973,f1968,f2212]) ).
fof(f2222,definition,
( spl154_261
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl154_261])],[avatar_definition]) ).
fof(f2223,plain,
( e2 = op(e0,e2)
| ~ spl154_261 ),
inference(avatar_component_clause,[],[f2222]) ).
fof(f2255,definition,
( spl154_268
<=> sP99 ),
introduced(definition,[new_symbols(definition,[spl154_268])],[avatar_definition]) ).
fof(f2259,definition,
( spl154_269
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl154_269])],[avatar_definition]) ).
fof(f2260,plain,
( e1 = unit
| ~ spl154_269 ),
inference(avatar_component_clause,[],[f2259]) ).
fof(f2263,plain,
( ~ spl154_268
| spl154_95
| ~ spl154_96 ),
inference(avatar_split_clause,[],[f743,f1438,f1433,f2255]) ).
fof(f2265,definition,
( spl154_270
<=> sP100 ),
introduced(definition,[new_symbols(definition,[spl154_270])],[avatar_definition]) ).
fof(f2269,plain,
( ~ spl154_270
| spl154_164
| ~ spl154_165 ),
inference(avatar_split_clause,[],[f741,f1759,f1754,f2265]) ).
fof(f2281,definition,
( spl154_273
<=> e1 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl154_273])],[avatar_definition]) ).
fof(f2295,definition,
( spl154_276
<=> e0 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl154_276])],[avatar_definition]) ).
fof(f2297,plain,
( e0 = op(e4,e1)
| ~ spl154_276 ),
inference(avatar_component_clause,[],[f2295]) ).
fof(f2312,definition,
( spl154_279
<=> sP106 ),
introduced(definition,[new_symbols(definition,[spl154_279])],[avatar_definition]) ).
fof(f2316,plain,
( ~ spl154_279
| spl154_233
| ~ spl154_234 ),
inference(avatar_split_clause,[],[f729,f2089,f2084,f2312]) ).
fof(f2382,definition,
( spl154_293
<=> sP114 ),
introduced(definition,[new_symbols(definition,[spl154_293])],[avatar_definition]) ).
fof(f2386,plain,
( ~ spl154_293
| spl154_137
| ~ spl154_138 ),
inference(avatar_split_clause,[],[f713,f1633,f1628,f2382]) ).
fof(f2388,definition,
( spl154_294
<=> sP115 ),
introduced(definition,[new_symbols(definition,[spl154_294])],[avatar_definition]) ).
fof(f2392,plain,
( ~ spl154_294
| spl154_200
| ~ spl154_201 ),
inference(avatar_split_clause,[],[f711,f1930,f1925,f2388]) ).
fof(f2413,definition,
( spl154_299
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl154_299])],[avatar_definition]) ).
fof(f2414,plain,
( e1 = op(e1,e0)
| ~ spl154_299 ),
inference(avatar_component_clause,[],[f2413]) ).
fof(f2418,definition,
( spl154_300
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl154_300])],[avatar_definition]) ).
fof(f2420,plain,
( e0 = op(e1,e1)
| ~ spl154_300 ),
inference(avatar_component_clause,[],[f2418]) ).
fof(f2423,definition,
( spl154_301
<=> sP119 ),
introduced(definition,[new_symbols(definition,[spl154_301])],[avatar_definition]) ).
fof(f2427,plain,
( ~ spl154_301
| spl154_151
| ~ spl154_152 ),
inference(avatar_split_clause,[],[f703,f1698,f1693,f2423]) ).
fof(f2429,definition,
( spl154_302
<=> sP120 ),
introduced(definition,[new_symbols(definition,[spl154_302])],[avatar_definition]) ).
fof(f2433,plain,
( ~ spl154_302
| spl154_212
| ~ spl154_213 ),
inference(avatar_split_clause,[],[f701,f1987,f1982,f2429]) ).
fof(f2445,definition,
( spl154_305
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl154_305])],[avatar_definition]) ).
fof(f2446,plain,
( e1 = op(e0,e1)
| ~ spl154_305 ),
inference(avatar_component_clause,[],[f2445]) ).
fof(f2468,definition,
( spl154_310
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl154_310])],[avatar_definition]) ).
fof(f2469,plain,
( e0 = unit
| ~ spl154_310 ),
inference(avatar_component_clause,[],[f2468]) ).
fof(f2585,definition,
( spl154_331
<=> sP142 ),
introduced(definition,[new_symbols(definition,[spl154_331])],[avatar_definition]) ).
fof(f2588,plain,
( ~ spl154_331
| ~ spl154_310
| ~ spl154_300 ),
inference(avatar_split_clause,[],[f656,f2418,f2468,f2585]) ).
fof(f2589,plain,
( ~ spl154_331
| spl154_299
| ~ spl154_300 ),
inference(avatar_split_clause,[],[f657,f2418,f2413,f2585]) ).
fof(f2595,definition,
( spl154_333
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl154_333])],[avatar_definition]) ).
fof(f2638,plain,
( ~ spl154_26
| spl154_102 ),
inference(avatar_split_clause,[],[f625,f1466,f1079]) ).
fof(f2669,plain,
( ~ spl154_27
| spl154_184 ),
inference(avatar_split_clause,[],[f606,f1850,f1083]) ).
fof(f2683,plain,
( ~ spl154_28
| spl154_219 ),
inference(avatar_split_clause,[],[f570,f2016,f1087]) ).
fof(f2685,plain,
( ~ spl154_28
| spl154_222 ),
inference(avatar_split_clause,[],[f572,f2031,f1087]) ).
fof(f2687,plain,
( ~ spl154_28
| spl154_228 ),
inference(avatar_split_clause,[],[f574,f2059,f1087]) ).
fof(f2688,plain,
( ~ spl154_28
| spl154_229 ),
inference(avatar_split_clause,[],[f575,f2065,f1087]) ).
fof(f2691,plain,
( ~ spl154_28
| spl154_235 ),
inference(avatar_split_clause,[],[f578,f2094,f1087]) ).
fof(f2692,plain,
( ~ spl154_28
| spl154_238 ),
inference(avatar_split_clause,[],[f579,f2108,f1087]) ).
fof(f2696,plain,
( ~ spl154_28
| spl154_245 ),
inference(avatar_split_clause,[],[f583,f2143,f1087]) ).
fof(f2703,plain,
( ~ spl154_28
| spl154_259 ),
inference(avatar_split_clause,[],[f590,f2212,f1087]) ).
fof(f2707,plain,
( ~ spl154_29
| spl154_268 ),
inference(avatar_split_clause,[],[f544,f2255,f1091]) ).
fof(f2708,plain,
( ~ spl154_29
| spl154_270 ),
inference(avatar_split_clause,[],[f545,f2265,f1091]) ).
fof(f2714,plain,
( ~ spl154_29
| spl154_279 ),
inference(avatar_split_clause,[],[f551,f2312,f1091]) ).
fof(f2722,plain,
( ~ spl154_29
| spl154_293 ),
inference(avatar_split_clause,[],[f559,f2382,f1091]) ).
fof(f2723,plain,
( ~ spl154_29
| spl154_294 ),
inference(avatar_split_clause,[],[f560,f2388,f1091]) ).
fof(f2727,plain,
( ~ spl154_29
| spl154_301 ),
inference(avatar_split_clause,[],[f564,f2423,f1091]) ).
fof(f2728,plain,
( ~ spl154_29
| spl154_302 ),
inference(avatar_split_clause,[],[f565,f2429,f1091]) ).
fof(f2750,plain,
( ~ spl154_30
| spl154_331 ),
inference(avatar_split_clause,[],[f537,f2585,f1095]) ).
fof(f2757,plain,
spl154_185,
inference(avatar_split_clause,[],[f516,f1854]) ).
fof(f2760,plain,
( spl154_90
| spl154_104
| spl154_118
| spl154_132
| spl154_146 ),
inference(avatar_split_clause,[],[f357,f1670,f1605,f1540,f1475,f1410]) ).
fof(f2764,plain,
( spl154_96
| spl154_110
| spl154_124
| spl154_138
| spl154_152 ),
inference(avatar_split_clause,[],[f361,f1698,f1633,f1568,f1503,f1438]) ).
fof(f2772,plain,
( spl154_162
| spl154_174
| spl154_186
| spl154_198
| spl154_210 ),
inference(avatar_split_clause,[],[f369,f1973,f1916,f1859,f1802,f1745]) ).
fof(f2773,plain,
( spl154_107
| spl154_174
| spl154_231
| spl154_233
| spl154_236 ),
inference(avatar_split_clause,[],[f370,f2098,f2084,f2075,f1802,f1489]) ).
fof(f2774,plain,
( spl154_165
| spl154_177
| spl154_189
| spl154_201
| spl154_213 ),
inference(avatar_split_clause,[],[f371,f1987,f1930,f1873,f1816,f1759]) ).
fof(f2779,plain,
( spl154_115
| spl154_117
| spl154_120
| spl154_123
| spl154_126 ),
inference(avatar_split_clause,[],[f376,f1577,f1563,f1549,f1535,f1526]) ).
fof(f2789,plain,
( spl154_129
| spl154_131
| spl154_134
| spl154_137
| spl154_140 ),
inference(avatar_split_clause,[],[f386,f1642,f1628,f1614,f1600,f1591]) ).
fof(f2808,plain,
( spl154_86
| spl154_157
| spl154_218
| spl154_269
| spl154_310 ),
inference(avatar_split_clause,[],[f344,f2468,f2259,f2010,f1721,f1392]) ).
fof(f2809,plain,
( spl154_87
| spl154_90
| spl154_93
| spl154_96
| spl154_99 ),
inference(avatar_split_clause,[],[f319,f1452,f1438,f1424,f1410,f1396]) ).
fof(f2810,plain,
( spl154_89
| spl154_159
| spl154_162
| spl154_165
| spl154_168 ),
inference(avatar_split_clause,[],[f320,f1773,f1759,f1745,f1731,f1405]) ).
fof(f2811,plain,
( spl154_92
| spl154_161
| spl154_221
| spl154_224
| spl154_227 ),
inference(avatar_split_clause,[],[f321,f2054,f2040,f2026,f1740,f1419]) ).
fof(f2812,plain,
( spl154_95
| spl154_164
| spl154_223
| spl154_273
| spl154_276 ),
inference(avatar_split_clause,[],[f322,f2295,f2281,f2035,f1754,f1433]) ).
fof(f2814,plain,
( spl154_101
| spl154_104
| spl154_107
| spl154_110
| spl154_113 ),
inference(avatar_split_clause,[],[f324,f1517,f1503,f1489,f1475,f1461]) ).
fof(f2819,plain,
( spl154_115
| spl154_118
| spl154_121
| spl154_124
| spl154_127 ),
inference(avatar_split_clause,[],[f329,f1582,f1568,f1554,f1540,f1526]) ).
fof(f2820,plain,
( spl154_117
| spl154_183
| spl154_186
| spl154_189
| spl154_192 ),
inference(avatar_split_clause,[],[f330,f1887,f1873,f1859,f1845,f1535]) ).
fof(f2825,plain,
( spl154_131
| spl154_195
| spl154_198
| spl154_201
| spl154_204 ),
inference(avatar_split_clause,[],[f335,f1944,f1930,f1916,f1902,f1600]) ).
fof(f2834,plain,
( e4 = op(e4,e3)
| ~ spl154_157 ),
inference(superposition,[],[f345,f1722]) ).
fof(f2853,plain,
( spl154_89
| ~ spl154_157 ),
inference(avatar_split_clause,[],[f2834,f1721,f1405]) ).
fof(f2858,plain,
( e2 = op(e2,e4)
| ~ spl154_86 ),
inference(superposition,[],[f349,f1393]) ).
fof(f2860,plain,
( e1 = op(e1,e4)
| ~ spl154_86 ),
inference(superposition,[],[f351,f1393]) ).
fof(f2867,plain,
( spl154_138
| ~ spl154_86 ),
inference(avatar_split_clause,[],[f2860,f1392,f1633]) ).
fof(f2869,plain,
( spl154_121
| ~ spl154_86 ),
inference(avatar_split_clause,[],[f2858,f1392,f1554]) ).
fof(f2880,plain,
( e4 != op(e4,e0)
| ~ spl154_87 ),
inference(superposition,[],[f411,f1397]) ).
fof(f2889,plain,
( ~ spl154_98
| ~ spl154_87 ),
inference(avatar_split_clause,[],[f2880,f1396,f1447]) ).
fof(f2895,plain,
( e2 != op(e4,e3)
| ~ spl154_93 ),
inference(superposition,[],[f405,f1426]) ).
fof(f2896,plain,
( e2 != op(e4,e2)
| ~ spl154_93 ),
inference(superposition,[],[f406,f1426]) ).
fof(f2912,plain,
( ~ spl154_221
| ~ spl154_93 ),
inference(avatar_split_clause,[],[f2896,f1424,f2026]) ).
fof(f2913,plain,
( ~ spl154_162
| ~ spl154_93 ),
inference(avatar_split_clause,[],[f2895,f1424,f1745]) ).
fof(f2917,plain,
e0 = op(e1,e1),
inference(forward_demodulation,[],[f518,f517]) ).
fof(f2918,plain,
spl154_300,
inference(avatar_split_clause,[],[f2917,f2418]) ).
fof(f2919,plain,
( e4 != op(e3,e2)
| ~ spl154_103 ),
inference(superposition,[],[f417,f1471]) ).
fof(f2920,plain,
( e4 != op(e3,e1)
| ~ spl154_103 ),
inference(superposition,[],[f419,f1471]) ).
fof(f2922,plain,
( e4 != op(e2,e3)
| ~ spl154_103 ),
inference(superposition,[],[f467,f1471]) ).
fof(f2923,plain,
( e4 != op(e1,e3)
| ~ spl154_103 ),
inference(superposition,[],[f469,f1471]) ).
fof(f2926,plain,
( ~ spl154_131
| ~ spl154_103 ),
inference(avatar_split_clause,[],[f2923,f1470,f1600]) ).
fof(f2927,plain,
( ~ spl154_117
| ~ spl154_103 ),
inference(avatar_split_clause,[],[f2922,f1470,f1535]) ).
fof(f2929,plain,
( ~ spl154_109
| ~ spl154_103 ),
inference(avatar_split_clause,[],[f2920,f1470,f1498]) ).
fof(f2930,plain,
( ~ spl154_106
| ~ spl154_103 ),
inference(avatar_split_clause,[],[f2919,f1470,f1484]) ).
fof(f2934,plain,
( e3 != op(e3,e0)
| ~ spl154_104 ),
inference(superposition,[],[f421,f1477]) ).
fof(f2942,plain,
( ~ spl154_179
| ~ spl154_104 ),
inference(avatar_split_clause,[],[f2934,f1475,f1825]) ).
fof(f2953,plain,
( e3 = op(e3,e2)
| ~ spl154_218 ),
inference(superposition,[],[f347,f2011]) ).
fof(f2969,plain,
( spl154_173
| ~ spl154_218 ),
inference(avatar_split_clause,[],[f2953,f2010,f1797]) ).
fof(f2982,plain,
( e0 = op(e1,e0)
| ~ spl154_269 ),
inference(superposition,[],[f354,f2260]) ).
fof(f2986,plain,
( spl154_333
| ~ spl154_269 ),
inference(avatar_split_clause,[],[f2982,f2259,f2595]) ).
fof(f2997,plain,
( e4 = op(e0,e4)
| ~ spl154_310 ),
inference(superposition,[],[f346,f2469]) ).
fof(f2998,plain,
( e3 = op(e3,e0)
| ~ spl154_310 ),
inference(superposition,[],[f347,f2469]) ).
fof(f2999,plain,
( e3 = op(e0,e3)
| ~ spl154_310 ),
inference(superposition,[],[f348,f2469]) ).
fof(f3000,plain,
( e2 = op(e2,e0)
| ~ spl154_310 ),
inference(superposition,[],[f349,f2469]) ).
fof(f3001,plain,
( e2 = op(e0,e2)
| ~ spl154_310 ),
inference(superposition,[],[f350,f2469]) ).
fof(f3002,plain,
( e1 = op(e1,e0)
| ~ spl154_310 ),
inference(superposition,[],[f351,f2469]) ).
fof(f3003,plain,
( e1 = op(e0,e1)
| ~ spl154_310 ),
inference(superposition,[],[f352,f2469]) ).
fof(f3011,plain,
( spl154_305
| ~ spl154_310 ),
inference(avatar_split_clause,[],[f3003,f2468,f2445]) ).
fof(f3012,plain,
( spl154_299
| ~ spl154_310 ),
inference(avatar_split_clause,[],[f3002,f2468,f2413]) ).
fof(f3013,plain,
( spl154_261
| ~ spl154_310 ),
inference(avatar_split_clause,[],[f3001,f2468,f2222]) ).
fof(f3014,plain,
( spl154_246
| ~ spl154_310 ),
inference(avatar_split_clause,[],[f3000,f2468,f2147]) ).
fof(f3015,plain,
( spl154_207
| ~ spl154_310 ),
inference(avatar_split_clause,[],[f2999,f2468,f1959]) ).
fof(f3016,plain,
( spl154_179
| ~ spl154_310 ),
inference(avatar_split_clause,[],[f2998,f2468,f1825]) ).
fof(f3017,plain,
( spl154_143
| ~ spl154_310 ),
inference(avatar_split_clause,[],[f2997,f2468,f1656]) ).
fof(f3038,plain,
( e4 != op(e3,e3)
| ~ spl154_89 ),
inference(superposition,[],[f465,f1406]) ).
fof(f3045,plain,
( ~ spl154_103
| ~ spl154_89 ),
inference(avatar_split_clause,[],[f3038,f1405,f1470]) ).
fof(f3049,plain,
( e3 != op(e4,e1)
| ~ spl154_90 ),
inference(superposition,[],[f408,f1412]) ).
fof(f3061,plain,
( ~ spl154_164
| ~ spl154_90 ),
inference(avatar_split_clause,[],[f3049,f1410,f1754]) ).
fof(f3065,plain,
( e4 != op(e4,e0)
| ~ spl154_95 ),
inference(superposition,[],[f414,f1434]) ).
fof(f3079,plain,
( e1 != op(e2,e4)
| ~ spl154_96 ),
inference(superposition,[],[f456,f1440]) ).
fof(f3087,plain,
( ~ spl154_124
| ~ spl154_96 ),
inference(avatar_split_clause,[],[f3079,f1438,f1568]) ).
fof(f3102,plain,
( e2 != op(e3,e1)
| ~ spl154_107 ),
inference(superposition,[],[f418,f1491]) ).
fof(f3113,plain,
( ~ spl154_233
| ~ spl154_107 ),
inference(avatar_split_clause,[],[f3102,f1489,f2084]) ).
fof(f3131,plain,
( e0 != op(e3,e2)
| ~ spl154_113 ),
inference(superposition,[],[f416,f1519]) ).
fof(f3134,plain,
( e0 != op(e2,e4)
| ~ spl154_113 ),
inference(superposition,[],[f457,f1519]) ).
fof(f3143,plain,
( ~ spl154_127
| ~ spl154_113 ),
inference(avatar_split_clause,[],[f3134,f1517,f1582]) ).
fof(f3146,plain,
( ~ spl154_237
| ~ spl154_113 ),
inference(avatar_split_clause,[],[f3131,f1517,f2103]) ).
fof(f3165,plain,
( e3 != op(e2,e2)
| ~ spl154_118 ),
inference(superposition,[],[f426,f1542]) ).
fof(f3168,plain,
( ~ spl154_185
| ~ spl154_118 ),
inference(avatar_split_clause,[],[f3165,f1540,f1854]) ).
fof(f3184,plain,
( e4 != op(e0,e4)
| ~ spl154_129 ),
inference(superposition,[],[f464,f1592]) ).
fof(f3185,plain,
( ~ spl154_143
| ~ spl154_129 ),
inference(avatar_split_clause,[],[f3184,f1591,f1656]) ).
fof(f3200,plain,
( e4 != op(e0,e4)
| ~ spl154_101 ),
inference(superposition,[],[f462,f1462]) ).
fof(f3204,plain,
( ~ spl154_143
| ~ spl154_101 ),
inference(avatar_split_clause,[],[f3200,f1461,f1656]) ).
fof(f3214,plain,
( e0 != op(e3,e4)
| ~ spl154_99 ),
inference(superposition,[],[f455,f1454]) ).
fof(f3225,plain,
( ~ spl154_113
| ~ spl154_99 ),
inference(avatar_split_clause,[],[f3214,f1452,f1517]) ).
fof(f3247,plain,
( e1 != op(e3,e2)
| ~ spl154_110 ),
inference(superposition,[],[f416,f1505]) ).
fof(f3261,plain,
( ~ spl154_234
| ~ spl154_110 ),
inference(avatar_split_clause,[],[f3247,f1503,f2089]) ).
fof(f3272,plain,
( e0 != op(e2,e2)
| ~ spl154_127 ),
inference(superposition,[],[f426,f1584]) ).
fof(f3281,plain,
( ~ spl154_247
| ~ spl154_127 ),
inference(avatar_split_clause,[],[f3272,f1582,f2152]) ).
fof(f3304,plain,
( e0 != op(e2,e3)
| ~ spl154_168 ),
inference(superposition,[],[f466,f1775]) ).
fof(f3318,plain,
( e1 != op(e4,e2)
| ~ spl154_165 ),
inference(superposition,[],[f407,f1761]) ).
fof(f3319,plain,
( e1 != op(e4,e1)
| ~ spl154_165 ),
inference(superposition,[],[f409,f1761]) ).
fof(f3323,plain,
( e1 != op(e1,e3)
| ~ spl154_165 ),
inference(superposition,[],[f468,f1761]) ).
fof(f3329,plain,
( ~ spl154_201
| ~ spl154_165 ),
inference(avatar_split_clause,[],[f3323,f1759,f1930]) ).
fof(f3334,plain,
( ~ spl154_224
| ~ spl154_165 ),
inference(avatar_split_clause,[],[f3318,f1759,f2040]) ).
fof(f3400,plain,
( e1 != op(e2,e3)
| ~ spl154_124 ),
inference(superposition,[],[f425,f1570]) ).
fof(f3419,plain,
( e2 != op(e0,e3)
| ~ spl154_162 ),
inference(superposition,[],[f471,f1747]) ).
fof(f3422,plain,
( ~ spl154_210
| ~ spl154_162 ),
inference(avatar_split_clause,[],[f3419,f1745,f1973]) ).
fof(f3430,plain,
( e1 != op(e3,e2)
| ~ spl154_177 ),
inference(superposition,[],[f417,f1818]) ).
fof(f3444,plain,
( ~ spl154_234
| ~ spl154_177 ),
inference(avatar_split_clause,[],[f3430,f1816,f2089]) ).
fof(f3447,plain,
( e4 = op(e3,e3)
| ~ spl154_185 ),
inference(superposition,[],[f515,f1855]) ).
fof(f3448,plain,
( e1 = op(e3,e2)
| ~ spl154_185 ),
inference(superposition,[],[f517,f1855]) ).
fof(f3449,plain,
( spl154_234
| ~ spl154_185 ),
inference(avatar_split_clause,[],[f3448,f1854,f2089]) ).
fof(f3453,plain,
( ~ spl154_189
| ~ spl154_124 ),
inference(avatar_split_clause,[],[f3400,f1568,f1873]) ).
fof(f3455,plain,
( spl154_103
| ~ spl154_185 ),
inference(avatar_split_clause,[],[f3447,f1854,f1470]) ).
fof(f3456,plain,
( e4 = op(e4,e0)
| ~ spl154_310 ),
inference(superposition,[],[f345,f2469]) ).
fof(f3470,plain,
( spl154_98
| ~ spl154_310 ),
inference(avatar_split_clause,[],[f3456,f2468,f1447]) ).
fof(f3482,plain,
( e4 != op(e4,e2)
| ~ spl154_98 ),
inference(superposition,[],[f413,f1448]) ).
fof(f3484,plain,
( e4 != op(e2,e0)
| ~ spl154_98 ),
inference(superposition,[],[f496,f1448]) ).
fof(f3485,plain,
( e4 != op(e1,e0)
| ~ spl154_98 ),
inference(superposition,[],[f498,f1448]) ).
fof(f3488,plain,
( ~ spl154_126
| ~ spl154_98 ),
inference(avatar_split_clause,[],[f3484,f1447,f1577]) ).
fof(f3502,plain,
( e3 != op(e1,e3)
| ~ spl154_132 ),
inference(superposition,[],[f435,f1607]) ).
fof(f3503,plain,
( e3 != op(e1,e2)
| ~ spl154_132 ),
inference(superposition,[],[f436,f1607]) ).
fof(f3511,plain,
( ~ spl154_197
| ~ spl154_132 ),
inference(avatar_split_clause,[],[f3503,f1605,f1911]) ).
fof(f3512,plain,
( ~ spl154_195
| ~ spl154_132 ),
inference(avatar_split_clause,[],[f3502,f1605,f1902]) ).
fof(f3520,plain,
( ~ spl154_140
| ~ spl154_98 ),
inference(avatar_split_clause,[],[f3485,f1447,f1642]) ).
fof(f3529,plain,
( e4 != op(e0,e2)
| ~ spl154_143 ),
inference(superposition,[],[f446,f1657]) ).
fof(f3532,plain,
( e4 != op(e2,e4)
| ~ spl154_143 ),
inference(superposition,[],[f463,f1657]) ).
fof(f3534,plain,
( ~ spl154_148
| ~ spl154_143 ),
inference(avatar_split_clause,[],[f3529,f1656,f1679]) ).
fof(f3544,plain,
( e3 != op(e0,e3)
| ~ spl154_159 ),
inference(superposition,[],[f471,f1732]) ).
fof(f3546,plain,
( ~ spl154_207
| ~ spl154_159 ),
inference(avatar_split_clause,[],[f3544,f1731,f1959]) ).
fof(f3551,plain,
( ~ spl154_273
| ~ spl154_165 ),
inference(avatar_split_clause,[],[f3319,f1759,f2281]) ).
fof(f3559,plain,
( e3 != op(e2,e2)
| ~ spl154_161 ),
inference(superposition,[],[f476,f1741]) ).
fof(f3561,plain,
( $false
| ~ spl154_161
| ~ spl154_185 ),
inference(forward_subsumption_resolution,[],[f3559,f1855]) ).
fof(f3562,plain,
( ~ spl154_161
| ~ spl154_185 ),
inference(avatar_contradiction_clause,[],[f3561]) ).
fof(f3601,plain,
( e2 != op(e2,e0)
| ~ spl154_186 ),
inference(superposition,[],[f432,f1861]) ).
fof(f3606,plain,
( ~ spl154_246
| ~ spl154_186 ),
inference(avatar_split_clause,[],[f3601,f1859,f2147]) ).
fof(f3619,plain,
( e0 != op(e1,e1)
| ~ spl154_204 ),
inference(superposition,[],[f439,f1946]) ).
fof(f3631,plain,
( ~ spl154_300
| ~ spl154_204 ),
inference(avatar_split_clause,[],[f3619,f1944,f2418]) ).
fof(f3637,plain,
( e2 != op(e0,e3)
| ~ spl154_198 ),
inference(superposition,[],[f474,f1918]) ).
fof(f3641,plain,
( ~ spl154_210
| ~ spl154_198 ),
inference(avatar_split_clause,[],[f3637,f1916,f1973]) ).
fof(f3647,plain,
( e3 != op(e2,e3)
| ~ spl154_207 ),
inference(superposition,[],[f473,f1960]) ).
fof(f3649,plain,
( e3 != op(e0,e1)
| ~ spl154_207 ),
inference(superposition,[],[f449,f1960]) ).
fof(f3650,plain,
( e3 != op(e0,e2)
| ~ spl154_207 ),
inference(superposition,[],[f447,f1960]) ).
fof(f3651,plain,
( ~ spl154_209
| ~ spl154_207 ),
inference(avatar_split_clause,[],[f3650,f1959,f1968]) ).
fof(f3652,plain,
( ~ spl154_212
| ~ spl154_207 ),
inference(avatar_split_clause,[],[f3649,f1959,f1982]) ).
fof(f3674,plain,
( e2 != op(e0,e2)
| ~ spl154_231 ),
inference(superposition,[],[f482,f2076]) ).
fof(f3679,plain,
( ~ spl154_261
| ~ spl154_231 ),
inference(avatar_split_clause,[],[f3674,f2075,f2222]) ).
fof(f3755,plain,
( e0 != op(e1,e1)
| ~ spl154_276 ),
inference(superposition,[],[f488,f2297]) ).
fof(f3762,plain,
( ~ spl154_300
| ~ spl154_276 ),
inference(avatar_split_clause,[],[f3755,f2295,f2418]) ).
fof(f3798,plain,
( e0 != op(e1,e0)
| ~ spl154_300 ),
inference(superposition,[],[f444,f2420]) ).
fof(f3848,plain,
( e4 = op(e0,e2)
| ~ spl154_36
| ~ spl154_227 ),
inference(forward_demodulation,[],[f1129,f2056]) ).
fof(f3849,plain,
( $false
| ~ spl154_36
| spl154_148
| ~ spl154_227 ),
inference(forward_subsumption_resolution,[],[f3848,f1681]) ).
fof(f3850,plain,
( ~ spl154_36
| spl154_148
| ~ spl154_227 ),
inference(avatar_contradiction_clause,[],[f3849]) ).
fof(f3862,plain,
( e1 != op(e0,e1)
| spl154_76
| ~ spl154_299 ),
inference(forward_demodulation,[],[f1341,f2414]) ).
fof(f3869,plain,
( e4 != op(e1,e2)
| spl154_56
| ~ spl154_124 ),
inference(forward_demodulation,[],[f1232,f1570]) ).
fof(f3873,plain,
( $false
| spl154_56
| ~ spl154_124
| ~ spl154_134 ),
inference(forward_subsumption_resolution,[],[f3869,f1615]) ).
fof(f3874,plain,
( spl154_56
| ~ spl154_124
| ~ spl154_134 ),
inference(avatar_contradiction_clause,[],[f3873]) ).
fof(f3877,plain,
( e4 = op(e1,e3)
| ~ spl154_33
| ~ spl154_165 ),
inference(forward_demodulation,[],[f1114,f1761]) ).
fof(f3883,plain,
( $false
| ~ spl154_33
| spl154_131
| ~ spl154_165 ),
inference(forward_subsumption_resolution,[],[f3877,f1602]) ).
fof(f3884,plain,
( ~ spl154_33
| spl154_131
| ~ spl154_165 ),
inference(avatar_contradiction_clause,[],[f3883]) ).
fof(f3894,plain,
( e4 != op(e0,e4)
| spl154_43
| ~ spl154_98 ),
inference(forward_demodulation,[],[f1164,f1448]) ).
fof(f3898,plain,
( $false
| spl154_43
| ~ spl154_98
| ~ spl154_143 ),
inference(forward_subsumption_resolution,[],[f3894,f1657]) ).
fof(f3899,plain,
( spl154_43
| ~ spl154_98
| ~ spl154_143 ),
inference(avatar_contradiction_clause,[],[f3898]) ).
fof(f3908,plain,
( e3 != op(e0,e3)
| spl154_55
| ~ spl154_179 ),
inference(forward_demodulation,[],[f1227,f1826]) ).
fof(f3912,plain,
( $false
| spl154_55
| ~ spl154_179
| ~ spl154_207 ),
inference(forward_subsumption_resolution,[],[f3908,f1960]) ).
fof(f3913,plain,
( spl154_55
| ~ spl154_179
| ~ spl154_207 ),
inference(avatar_contradiction_clause,[],[f3912]) ).
fof(f3916,plain,
( e4 = op(e3,e1)
| ~ spl154_39
| ~ spl154_164 ),
inference(forward_demodulation,[],[f1144,f1755]) ).
fof(f3917,plain,
( e3 != op(e1,e4)
| spl154_40
| ~ spl154_164 ),
inference(forward_demodulation,[],[f1149,f1755]) ).
fof(f3919,plain,
( $false
| ~ spl154_39
| spl154_109
| ~ spl154_164 ),
inference(forward_subsumption_resolution,[],[f3916,f1500]) ).
fof(f3920,plain,
( ~ spl154_39
| spl154_109
| ~ spl154_164 ),
inference(avatar_contradiction_clause,[],[f3919]) ).
fof(f3921,plain,
( $false
| spl154_40
| ~ spl154_132
| ~ spl154_164 ),
inference(forward_subsumption_resolution,[],[f3917,f1607]) ).
fof(f3922,plain,
( spl154_40
| ~ spl154_132
| ~ spl154_164 ),
inference(avatar_contradiction_clause,[],[f3921]) ).
fof(f3926,plain,
( e3 = op(e0,e4)
| ~ spl154_45
| ~ spl154_113 ),
inference(forward_demodulation,[],[f1174,f1519]) ).
fof(f3931,plain,
( e3 = op(e1,e2)
| ~ spl154_48
| ~ spl154_234 ),
inference(forward_demodulation,[],[f1192,f2091]) ).
fof(f3932,plain,
( e1 != op(e2,e3)
| spl154_49
| ~ spl154_234 ),
inference(forward_demodulation,[],[f1197,f2091]) ).
fof(f3935,plain,
( spl154_197
| ~ spl154_48
| ~ spl154_234 ),
inference(avatar_split_clause,[],[f3931,f2089,f1190,f1911]) ).
fof(f3940,plain,
( e2 != op(e1,e3)
| spl154_52
| ~ spl154_233 ),
inference(forward_demodulation,[],[f1212,f2085]) ).
fof(f3948,plain,
( e2 = op(e0,e3)
| ~ spl154_59
| ~ spl154_192 ),
inference(forward_demodulation,[],[f1248,f1889]) ).
fof(f3950,plain,
( spl154_210
| ~ spl154_59
| ~ spl154_192 ),
inference(avatar_split_clause,[],[f3948,f1887,f1246,f1973]) ).
fof(f3952,plain,
( ~ spl154_183
| ~ spl154_207 ),
inference(avatar_split_clause,[],[f3647,f1959,f1845]) ).
fof(f3960,plain,
( ~ spl154_92
| ~ spl154_98 ),
inference(avatar_split_clause,[],[f3482,f1447,f1419]) ).
fof(f3969,plain,
( e0 = e3
| ~ spl154_200
| ~ spl154_300 ),
inference(forward_demodulation,[],[f1926,f2420]) ).
fof(f3981,plain,
( $false
| ~ spl154_200
| ~ spl154_300 ),
inference(forward_subsumption_resolution,[],[f3969,f512]) ).
fof(f3982,plain,
( ~ spl154_200
| ~ spl154_300 ),
inference(avatar_contradiction_clause,[],[f3981]) ).
fof(f3986,plain,
( ~ spl154_198
| spl154_52
| ~ spl154_233 ),
inference(avatar_split_clause,[],[f3940,f2084,f1210,f1916]) ).
fof(f3991,plain,
( ~ spl154_192
| ~ spl154_168 ),
inference(avatar_split_clause,[],[f3304,f1773,f1887]) ).
fof(f3993,plain,
( e1 = e3
| ~ spl154_173
| ~ spl154_234 ),
inference(forward_demodulation,[],[f1798,f2091]) ).
fof(f3999,plain,
( $false
| ~ spl154_173
| ~ spl154_234 ),
inference(forward_subsumption_resolution,[],[f3993,f509]) ).
fof(f4000,plain,
( ~ spl154_173
| ~ spl154_234 ),
inference(avatar_contradiction_clause,[],[f3999]) ).
fof(f4002,plain,
( e1 = e4
| ~ spl154_151
| ~ spl154_305 ),
inference(forward_demodulation,[],[f1694,f2446]) ).
fof(f4014,plain,
( ~ spl154_189
| spl154_49
| ~ spl154_234 ),
inference(avatar_split_clause,[],[f3932,f2089,f1195,f1873]) ).
fof(f4017,plain,
( $false
| ~ spl154_151
| ~ spl154_305 ),
inference(forward_subsumption_resolution,[],[f4002,f508]) ).
fof(f4018,plain,
( ~ spl154_151
| ~ spl154_305 ),
inference(avatar_contradiction_clause,[],[f4017]) ).
fof(f4021,plain,
( e4 != op(e2,e1)
| spl154_63
| ~ spl154_134 ),
inference(forward_demodulation,[],[f1271,f1615]) ).
fof(f4022,plain,
( e3 = e4
| ~ spl154_120
| ~ spl154_185 ),
inference(forward_demodulation,[],[f1550,f1855]) ).
fof(f4023,plain,
( e0 = e4
| ~ spl154_137
| ~ spl154_300 ),
inference(forward_demodulation,[],[f1629,f2420]) ).
fof(f4038,plain,
( ~ spl154_123
| spl154_63
| ~ spl154_134 ),
inference(avatar_split_clause,[],[f4021,f1614,f1269,f1563]) ).
fof(f4039,plain,
( $false
| ~ spl154_120
| ~ spl154_185 ),
inference(forward_subsumption_resolution,[],[f4022,f505]) ).
fof(f4040,plain,
( ~ spl154_120
| ~ spl154_185 ),
inference(avatar_contradiction_clause,[],[f4039]) ).
fof(f4041,plain,
( $false
| ~ spl154_137
| ~ spl154_300 ),
inference(forward_subsumption_resolution,[],[f4023,f511]) ).
fof(f4042,plain,
( ~ spl154_137
| ~ spl154_300 ),
inference(avatar_contradiction_clause,[],[f4041]) ).
fof(f4045,plain,
( $false
| ~ spl154_95
| ~ spl154_98 ),
inference(forward_subsumption_resolution,[],[f3065,f1448]) ).
fof(f4046,plain,
( ~ spl154_95
| ~ spl154_98 ),
inference(avatar_contradiction_clause,[],[f4045]) ).
fof(f4056,plain,
( ~ spl154_115
| ~ spl154_143 ),
inference(avatar_split_clause,[],[f3532,f1656,f1526]) ).
fof(f4058,plain,
( spl154_146
| ~ spl154_45
| ~ spl154_113 ),
inference(avatar_split_clause,[],[f3926,f1517,f1172,f1670]) ).
fof(f4134,plain,
( e3 = e4
| ~ spl154_143
| ~ spl154_146 ),
inference(superposition,[],[f1672,f1657]) ).
fof(f4145,plain,
( $false
| ~ spl154_143
| ~ spl154_146 ),
inference(forward_subsumption_resolution,[],[f4134,f505]) ).
fof(f4146,plain,
( ~ spl154_143
| ~ spl154_146 ),
inference(avatar_contradiction_clause,[],[f4145]) ).
fof(f4175,plain,
( ~ spl154_305
| spl154_76
| ~ spl154_299 ),
inference(avatar_split_clause,[],[f3862,f2413,f1339,f2445]) ).
fof(f4179,plain,
( e2 != op(e2,e0)
| spl154_66
| ~ spl154_261 ),
inference(forward_demodulation,[],[f1286,f2223]) ).
fof(f4180,plain,
( ~ spl154_246
| spl154_66
| ~ spl154_261 ),
inference(avatar_split_clause,[],[f4179,f2222,f1284,f2147]) ).
fof(f4219,plain,
( e2 != op(e2,e3)
| ~ spl154_121 ),
inference(superposition,[],[f425,f1556]) ).
fof(f4222,plain,
( e2 != op(e2,e0)
| ~ spl154_121 ),
inference(superposition,[],[f431,f1556]) ).
fof(f4225,plain,
( ~ spl154_246
| ~ spl154_121 ),
inference(avatar_split_clause,[],[f4222,f1554,f2147]) ).
fof(f4234,plain,
( e1 != op(e1,e0)
| ~ spl154_138 ),
inference(superposition,[],[f441,f1635]) ).
fof(f4252,plain,
( ~ spl154_333
| ~ spl154_300 ),
inference(avatar_split_clause,[],[f3798,f2418,f2595]) ).
fof(f4253,plain,
( ~ spl154_299
| ~ spl154_138 ),
inference(avatar_split_clause,[],[f4234,f1633,f2413]) ).
fof(f4255,plain,
( ~ spl154_186
| ~ spl154_121 ),
inference(avatar_split_clause,[],[f4219,f1554,f1859]) ).
cnf(s3,plain,
( spl154_1
| spl154_2
| spl154_3
| spl154_4
| spl154_5
| spl154_6
| spl154_7
| spl154_8
| spl154_9
| spl154_10
| spl154_11
| spl154_12
| spl154_13
| spl154_14
| spl154_15
| spl154_16
| spl154_17
| spl154_18
| spl154_19
| spl154_20
| spl154_21
| spl154_22
| spl154_23
| spl154_24 ),
inference(sat_conversion,[],[f1077]) ).
cnf(s4,plain,
( spl154_26
| spl154_27
| spl154_28
| spl154_29
| spl154_30 ),
inference(sat_conversion,[],[f1098]) ).
cnf(s7,plain,
~ spl154_1,
inference(sat_conversion,[],[f1105]) ).
cnf(s9,plain,
( ~ spl154_2
| spl154_33 ),
inference(sat_conversion,[],[f1115]) ).
cnf(s12,plain,
( ~ spl154_3
| spl154_36 ),
inference(sat_conversion,[],[f1130]) ).
cnf(s15,plain,
( ~ spl154_4
| spl154_39 ),
inference(sat_conversion,[],[f1145]) ).
cnf(s19,plain,
( ~ spl154_5
| ~ spl154_43 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s21,plain,
( ~ spl154_6
| spl154_45 ),
inference(sat_conversion,[],[f1175]) ).
cnf(s25,plain,
~ spl154_7,
inference(sat_conversion,[],[f1183]) ).
cnf(s27,plain,
( ~ spl154_8
| spl154_48 ),
inference(sat_conversion,[],[f1193]) ).
cnf(s31,plain,
( ~ spl154_9
| ~ spl154_52 ),
inference(sat_conversion,[],[f1213]) ).
cnf(s34,plain,
( ~ spl154_10
| ~ spl154_55 ),
inference(sat_conversion,[],[f1228]) ).
cnf(s35,plain,
( ~ spl154_11
| ~ spl154_56 ),
inference(sat_conversion,[],[f1233]) ).
cnf(s39,plain,
( ~ spl154_12
| spl154_59 ),
inference(sat_conversion,[],[f1249]) ).
cnf(s40,plain,
( ~ spl154_12
| ~ spl154_49 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s43,plain,
~ spl154_13,
inference(sat_conversion,[],[f1257]) ).
cnf(s46,plain,
( ~ spl154_14
| ~ spl154_63 ),
inference(sat_conversion,[],[f1272]) ).
cnf(s49,plain,
( ~ spl154_15
| ~ spl154_66 ),
inference(sat_conversion,[],[f1287]) ).
cnf(s52,plain,
( ~ spl154_16
| ~ spl154_40 ),
inference(sat_conversion,[],[f1298]) ).
cnf(s55,plain,
( ~ spl154_17
| ~ spl154_52 ),
inference(sat_conversion,[],[f1309]) ).
cnf(s58,plain,
( ~ spl154_18
| ~ spl154_63 ),
inference(sat_conversion,[],[f1320]) ).
cnf(s61,plain,
~ spl154_19,
inference(sat_conversion,[],[f1327]) ).
cnf(s64,plain,
( ~ spl154_20
| ~ spl154_76 ),
inference(sat_conversion,[],[f1342]) ).
cnf(s67,plain,
( ~ spl154_21
| ~ spl154_43 ),
inference(sat_conversion,[],[f1353]) ).
cnf(s70,plain,
( ~ spl154_22
| ~ spl154_55 ),
inference(sat_conversion,[],[f1364]) ).
cnf(s73,plain,
( ~ spl154_23
| ~ spl154_66 ),
inference(sat_conversion,[],[f1375]) ).
cnf(s76,plain,
( ~ spl154_24
| ~ spl154_76 ),
inference(sat_conversion,[],[f1386]) ).
cnf(s87,plain,
( ~ spl154_86
| ~ spl154_102
| ~ spl154_103 ),
inference(sat_conversion,[],[f1473]) ).
cnf(s88,plain,
( ~ spl154_102
| ~ spl154_103
| spl154_104 ),
inference(sat_conversion,[],[f1478]) ).
cnf(s144,plain,
( ~ spl154_184
| ~ spl154_185
| spl154_186 ),
inference(sat_conversion,[],[f1862]) ).
cnf(s170,plain,
( spl154_161
| ~ spl154_162
| ~ spl154_219 ),
inference(sat_conversion,[],[f2020]) ).
cnf(s173,plain,
( ~ spl154_222
| ~ spl154_223
| spl154_224 ),
inference(sat_conversion,[],[f2043]) ).
cnf(s177,plain,
( spl154_106
| ~ spl154_107
| ~ spl154_228 ),
inference(sat_conversion,[],[f2063]) ).
cnf(s179,plain,
( spl154_173
| ~ spl154_174
| ~ spl154_229 ),
inference(sat_conversion,[],[f2069]) ).
cnf(s184,plain,
( ~ spl154_235
| ~ spl154_236
| spl154_237 ),
inference(sat_conversion,[],[f2106]) ).
cnf(s186,plain,
( spl154_120
| ~ spl154_121
| ~ spl154_238 ),
inference(sat_conversion,[],[f2112]) ).
cnf(s193,plain,
( ~ spl154_245
| ~ spl154_246
| spl154_247 ),
inference(sat_conversion,[],[f2155]) ).
cnf(s206,plain,
( spl154_209
| ~ spl154_210
| ~ spl154_259 ),
inference(sat_conversion,[],[f2216]) ).
cnf(s213,plain,
( spl154_95
| ~ spl154_96
| ~ spl154_268 ),
inference(sat_conversion,[],[f2263]) ).
cnf(s215,plain,
( spl154_164
| ~ spl154_165
| ~ spl154_270 ),
inference(sat_conversion,[],[f2269]) ).
cnf(s226,plain,
( spl154_233
| ~ spl154_234
| ~ spl154_279 ),
inference(sat_conversion,[],[f2316]) ).
cnf(s240,plain,
( spl154_137
| ~ spl154_138
| ~ spl154_293 ),
inference(sat_conversion,[],[f2386]) ).
cnf(s242,plain,
( spl154_200
| ~ spl154_201
| ~ spl154_294 ),
inference(sat_conversion,[],[f2392]) ).
cnf(s249,plain,
( spl154_151
| ~ spl154_152
| ~ spl154_301 ),
inference(sat_conversion,[],[f2427]) ).
cnf(s251,plain,
( spl154_212
| ~ spl154_213
| ~ spl154_302 ),
inference(sat_conversion,[],[f2433]) ).
cnf(s290,plain,
( ~ spl154_300
| ~ spl154_310
| ~ spl154_331 ),
inference(sat_conversion,[],[f2588]) ).
cnf(s291,plain,
( spl154_299
| ~ spl154_300
| ~ spl154_331 ),
inference(sat_conversion,[],[f2589]) ).
cnf(s308,plain,
( ~ spl154_26
| spl154_102 ),
inference(sat_conversion,[],[f2638]) ).
cnf(s339,plain,
( ~ spl154_27
| spl154_184 ),
inference(sat_conversion,[],[f2669]) ).
cnf(s353,plain,
( ~ spl154_28
| spl154_219 ),
inference(sat_conversion,[],[f2683]) ).
cnf(s355,plain,
( ~ spl154_28
| spl154_222 ),
inference(sat_conversion,[],[f2685]) ).
cnf(s357,plain,
( ~ spl154_28
| spl154_228 ),
inference(sat_conversion,[],[f2687]) ).
cnf(s358,plain,
( ~ spl154_28
| spl154_229 ),
inference(sat_conversion,[],[f2688]) ).
cnf(s361,plain,
( ~ spl154_28
| spl154_235 ),
inference(sat_conversion,[],[f2691]) ).
cnf(s362,plain,
( ~ spl154_28
| spl154_238 ),
inference(sat_conversion,[],[f2692]) ).
cnf(s366,plain,
( ~ spl154_28
| spl154_245 ),
inference(sat_conversion,[],[f2696]) ).
cnf(s373,plain,
( ~ spl154_28
| spl154_259 ),
inference(sat_conversion,[],[f2703]) ).
cnf(s377,plain,
( ~ spl154_29
| spl154_268 ),
inference(sat_conversion,[],[f2707]) ).
cnf(s378,plain,
( ~ spl154_29
| spl154_270 ),
inference(sat_conversion,[],[f2708]) ).
cnf(s384,plain,
( ~ spl154_29
| spl154_279 ),
inference(sat_conversion,[],[f2714]) ).
cnf(s392,plain,
( ~ spl154_29
| spl154_293 ),
inference(sat_conversion,[],[f2722]) ).
cnf(s393,plain,
( ~ spl154_29
| spl154_294 ),
inference(sat_conversion,[],[f2723]) ).
cnf(s397,plain,
( ~ spl154_29
| spl154_301 ),
inference(sat_conversion,[],[f2727]) ).
cnf(s398,plain,
( ~ spl154_29
| spl154_302 ),
inference(sat_conversion,[],[f2728]) ).
cnf(s420,plain,
( ~ spl154_30
| spl154_331 ),
inference(sat_conversion,[],[f2750]) ).
cnf(s427,plain,
spl154_185,
inference(sat_conversion,[],[f2757]) ).
cnf(s430,plain,
( spl154_90
| spl154_104
| spl154_118
| spl154_132
| spl154_146 ),
inference(sat_conversion,[],[f2760]) ).
cnf(s434,plain,
( spl154_96
| spl154_110
| spl154_124
| spl154_138
| spl154_152 ),
inference(sat_conversion,[],[f2764]) ).
cnf(s442,plain,
( spl154_162
| spl154_174
| spl154_186
| spl154_198
| spl154_210 ),
inference(sat_conversion,[],[f2772]) ).
cnf(s443,plain,
( spl154_107
| spl154_174
| spl154_231
| spl154_233
| spl154_236 ),
inference(sat_conversion,[],[f2773]) ).
cnf(s444,plain,
( spl154_165
| spl154_177
| spl154_189
| spl154_201
| spl154_213 ),
inference(sat_conversion,[],[f2774]) ).
cnf(s449,plain,
( spl154_115
| spl154_117
| spl154_120
| spl154_123
| spl154_126 ),
inference(sat_conversion,[],[f2779]) ).
cnf(s459,plain,
( spl154_129
| spl154_131
| spl154_134
| spl154_137
| spl154_140 ),
inference(sat_conversion,[],[f2789]) ).
cnf(s478,plain,
( spl154_86
| spl154_157
| spl154_218
| spl154_269
| spl154_310 ),
inference(sat_conversion,[],[f2808]) ).
cnf(s479,plain,
( spl154_87
| spl154_90
| spl154_93
| spl154_96
| spl154_99 ),
inference(sat_conversion,[],[f2809]) ).
cnf(s480,plain,
( spl154_89
| spl154_159
| spl154_162
| spl154_165
| spl154_168 ),
inference(sat_conversion,[],[f2810]) ).
cnf(s481,plain,
( spl154_92
| spl154_161
| spl154_221
| spl154_224
| spl154_227 ),
inference(sat_conversion,[],[f2811]) ).
cnf(s482,plain,
( spl154_95
| spl154_164
| spl154_223
| spl154_273
| spl154_276 ),
inference(sat_conversion,[],[f2812]) ).
cnf(s484,plain,
( spl154_101
| spl154_104
| spl154_107
| spl154_110
| spl154_113 ),
inference(sat_conversion,[],[f2814]) ).
cnf(s489,plain,
( spl154_115
| spl154_118
| spl154_121
| spl154_124
| spl154_127 ),
inference(sat_conversion,[],[f2819]) ).
cnf(s490,plain,
( spl154_117
| spl154_183
| spl154_186
| spl154_189
| spl154_192 ),
inference(sat_conversion,[],[f2820]) ).
cnf(s495,plain,
( spl154_131
| spl154_195
| spl154_198
| spl154_201
| spl154_204 ),
inference(sat_conversion,[],[f2825]) ).
cnf(s513,plain,
( spl154_89
| ~ spl154_157 ),
inference(sat_conversion,[],[f2853]) ).
cnf(s517,plain,
( ~ spl154_86
| spl154_138 ),
inference(sat_conversion,[],[f2867]) ).
cnf(s519,plain,
( ~ spl154_86
| spl154_121 ),
inference(sat_conversion,[],[f2869]) ).
cnf(s528,plain,
( ~ spl154_87
| ~ spl154_98 ),
inference(sat_conversion,[],[f2889]) ).
cnf(s539,plain,
( ~ spl154_93
| ~ spl154_221 ),
inference(sat_conversion,[],[f2912]) ).
cnf(s540,plain,
( ~ spl154_93
| ~ spl154_162 ),
inference(sat_conversion,[],[f2913]) ).
cnf(s542,plain,
spl154_300,
inference(sat_conversion,[],[f2918]) ).
cnf(s544,plain,
( ~ spl154_103
| ~ spl154_131 ),
inference(sat_conversion,[],[f2926]) ).
cnf(s545,plain,
( ~ spl154_103
| ~ spl154_117 ),
inference(sat_conversion,[],[f2927]) ).
cnf(s547,plain,
( ~ spl154_103
| ~ spl154_109 ),
inference(sat_conversion,[],[f2929]) ).
cnf(s548,plain,
( ~ spl154_103
| ~ spl154_106 ),
inference(sat_conversion,[],[f2930]) ).
cnf(s552,plain,
( ~ spl154_104
| ~ spl154_179 ),
inference(sat_conversion,[],[f2942]) ).
cnf(s564,plain,
( spl154_173
| ~ spl154_218 ),
inference(sat_conversion,[],[f2969]) ).
cnf(s567,plain,
( ~ spl154_269
| spl154_333 ),
inference(sat_conversion,[],[f2986]) ).
cnf(s579,plain,
( spl154_305
| ~ spl154_310 ),
inference(sat_conversion,[],[f3011]) ).
cnf(s580,plain,
( spl154_299
| ~ spl154_310 ),
inference(sat_conversion,[],[f3012]) ).
cnf(s581,plain,
( spl154_261
| ~ spl154_310 ),
inference(sat_conversion,[],[f3013]) ).
cnf(s582,plain,
( spl154_246
| ~ spl154_310 ),
inference(sat_conversion,[],[f3014]) ).
cnf(s583,plain,
( spl154_207
| ~ spl154_310 ),
inference(sat_conversion,[],[f3015]) ).
cnf(s584,plain,
( spl154_179
| ~ spl154_310 ),
inference(sat_conversion,[],[f3016]) ).
cnf(s585,plain,
( spl154_143
| ~ spl154_310 ),
inference(sat_conversion,[],[f3017]) ).
cnf(s600,plain,
( ~ spl154_89
| ~ spl154_103 ),
inference(sat_conversion,[],[f3045]) ).
cnf(s607,plain,
( ~ spl154_90
| ~ spl154_164 ),
inference(sat_conversion,[],[f3061]) ).
cnf(s616,plain,
( ~ spl154_96
| ~ spl154_124 ),
inference(sat_conversion,[],[f3087]) ).
cnf(s628,plain,
( ~ spl154_107
| ~ spl154_233 ),
inference(sat_conversion,[],[f3113]) ).
cnf(s644,plain,
( ~ spl154_113
| ~ spl154_127 ),
inference(sat_conversion,[],[f3143]) ).
cnf(s646,plain,
( ~ spl154_113
| ~ spl154_237 ),
inference(sat_conversion,[],[f3146]) ).
cnf(s655,plain,
( ~ spl154_118
| ~ spl154_185 ),
inference(sat_conversion,[],[f3168]) ).
cnf(s666,plain,
( ~ spl154_129
| ~ spl154_143 ),
inference(sat_conversion,[],[f3185]) ).
cnf(s673,plain,
( ~ spl154_101
| ~ spl154_143 ),
inference(sat_conversion,[],[f3204]) ).
cnf(s683,plain,
( ~ spl154_99
| ~ spl154_113 ),
inference(sat_conversion,[],[f3225]) ).
cnf(s701,plain,
( ~ spl154_110
| ~ spl154_234 ),
inference(sat_conversion,[],[f3261]) ).
cnf(s709,plain,
( ~ spl154_127
| ~ spl154_247 ),
inference(sat_conversion,[],[f3281]) ).
cnf(s719,plain,
( ~ spl154_165
| ~ spl154_201 ),
inference(sat_conversion,[],[f3329]) ).
cnf(s722,plain,
( ~ spl154_165
| ~ spl154_224 ),
inference(sat_conversion,[],[f3334]) ).
cnf(s746,plain,
( ~ spl154_162
| ~ spl154_210 ),
inference(sat_conversion,[],[f3422]) ).
cnf(s752,plain,
( ~ spl154_177
| ~ spl154_234 ),
inference(sat_conversion,[],[f3444]) ).
cnf(s753,plain,
( ~ spl154_185
| spl154_234 ),
inference(sat_conversion,[],[f3449]) ).
cnf(s769,plain,
( ~ spl154_124
| ~ spl154_189 ),
inference(sat_conversion,[],[f3453]) ).
cnf(s772,plain,
( spl154_103
| ~ spl154_185 ),
inference(sat_conversion,[],[f3455]) ).
cnf(s782,plain,
( spl154_98
| ~ spl154_310 ),
inference(sat_conversion,[],[f3470]) ).
cnf(s789,plain,
( ~ spl154_98
| ~ spl154_126 ),
inference(sat_conversion,[],[f3488]) ).
cnf(s796,plain,
( ~ spl154_132
| ~ spl154_197 ),
inference(sat_conversion,[],[f3511]) ).
cnf(s797,plain,
( ~ spl154_132
| ~ spl154_195 ),
inference(sat_conversion,[],[f3512]) ).
cnf(s799,plain,
( ~ spl154_98
| ~ spl154_140 ),
inference(sat_conversion,[],[f3520]) ).
cnf(s802,plain,
( ~ spl154_143
| ~ spl154_148 ),
inference(sat_conversion,[],[f3534]) ).
cnf(s803,plain,
( ~ spl154_159
| ~ spl154_207 ),
inference(sat_conversion,[],[f3546]) ).
cnf(s809,plain,
( ~ spl154_165
| ~ spl154_273 ),
inference(sat_conversion,[],[f3551]) ).
cnf(s813,plain,
( ~ spl154_161
| ~ spl154_185 ),
inference(sat_conversion,[],[f3562]) ).
cnf(s825,plain,
( ~ spl154_186
| ~ spl154_246 ),
inference(sat_conversion,[],[f3606]) ).
cnf(s830,plain,
( ~ spl154_204
| ~ spl154_300 ),
inference(sat_conversion,[],[f3631]) ).
cnf(s831,plain,
( ~ spl154_198
| ~ spl154_210 ),
inference(sat_conversion,[],[f3641]) ).
cnf(s834,plain,
( ~ spl154_207
| ~ spl154_209 ),
inference(sat_conversion,[],[f3651]) ).
cnf(s835,plain,
( ~ spl154_207
| ~ spl154_212 ),
inference(sat_conversion,[],[f3652]) ).
cnf(s839,plain,
( ~ spl154_231
| ~ spl154_261 ),
inference(sat_conversion,[],[f3679]) ).
cnf(s854,plain,
( ~ spl154_276
| ~ spl154_300 ),
inference(sat_conversion,[],[f3762]) ).
cnf(s865,plain,
( ~ spl154_36
| spl154_148
| ~ spl154_227 ),
inference(sat_conversion,[],[f3850]) ).
cnf(s870,plain,
( spl154_56
| ~ spl154_124
| ~ spl154_134 ),
inference(sat_conversion,[],[f3874]) ).
cnf(s873,plain,
( ~ spl154_33
| spl154_131
| ~ spl154_165 ),
inference(sat_conversion,[],[f3884]) ).
cnf(s875,plain,
( spl154_43
| ~ spl154_98
| ~ spl154_143 ),
inference(sat_conversion,[],[f3899]) ).
cnf(s878,plain,
( spl154_55
| ~ spl154_179
| ~ spl154_207 ),
inference(sat_conversion,[],[f3913]) ).
cnf(s879,plain,
( ~ spl154_39
| spl154_109
| ~ spl154_164 ),
inference(sat_conversion,[],[f3920]) ).
cnf(s880,plain,
( spl154_40
| ~ spl154_132
| ~ spl154_164 ),
inference(sat_conversion,[],[f3922]) ).
cnf(s883,plain,
( ~ spl154_48
| spl154_197
| ~ spl154_234 ),
inference(sat_conversion,[],[f3935]) ).
cnf(s886,plain,
( ~ spl154_59
| ~ spl154_192
| spl154_210 ),
inference(sat_conversion,[],[f3950]) ).
cnf(s887,plain,
( ~ spl154_183
| ~ spl154_207 ),
inference(sat_conversion,[],[f3952]) ).
cnf(s889,plain,
( ~ spl154_92
| ~ spl154_98 ),
inference(sat_conversion,[],[f3960]) ).
cnf(s905,plain,
( ~ spl154_200
| ~ spl154_300 ),
inference(sat_conversion,[],[f3982]) ).
cnf(s907,plain,
( spl154_52
| ~ spl154_198
| ~ spl154_233 ),
inference(sat_conversion,[],[f3986]) ).
cnf(s911,plain,
( ~ spl154_168
| ~ spl154_192 ),
inference(sat_conversion,[],[f3991]) ).
cnf(s916,plain,
( ~ spl154_173
| ~ spl154_234 ),
inference(sat_conversion,[],[f4000]) ).
cnf(s921,plain,
( spl154_49
| ~ spl154_189
| ~ spl154_234 ),
inference(sat_conversion,[],[f4014]) ).
cnf(s924,plain,
( ~ spl154_151
| ~ spl154_305 ),
inference(sat_conversion,[],[f4018]) ).
cnf(s934,plain,
( spl154_63
| ~ spl154_123
| ~ spl154_134 ),
inference(sat_conversion,[],[f4038]) ).
cnf(s935,plain,
( ~ spl154_120
| ~ spl154_185 ),
inference(sat_conversion,[],[f4040]) ).
cnf(s936,plain,
( ~ spl154_137
| ~ spl154_300 ),
inference(sat_conversion,[],[f4042]) ).
cnf(s939,plain,
( ~ spl154_95
| ~ spl154_98 ),
inference(sat_conversion,[],[f4046]) ).
cnf(s947,plain,
( ~ spl154_115
| ~ spl154_143 ),
inference(sat_conversion,[],[f4056]) ).
cnf(s949,plain,
( ~ spl154_45
| ~ spl154_113
| spl154_146 ),
inference(sat_conversion,[],[f4058]) ).
cnf(s994,plain,
( ~ spl154_143
| ~ spl154_146 ),
inference(sat_conversion,[],[f4146]) ).
cnf(s1021,plain,
( spl154_76
| ~ spl154_299
| ~ spl154_305 ),
inference(sat_conversion,[],[f4175]) ).
cnf(s1027,plain,
( spl154_66
| ~ spl154_246
| ~ spl154_261 ),
inference(sat_conversion,[],[f4180]) ).
cnf(s1043,plain,
( ~ spl154_121
| ~ spl154_246 ),
inference(sat_conversion,[],[f4225]) ).
cnf(s1052,plain,
( ~ spl154_300
| ~ spl154_333 ),
inference(sat_conversion,[],[f4252]) ).
cnf(s1053,plain,
( ~ spl154_138
| ~ spl154_299 ),
inference(sat_conversion,[],[f4253]) ).
cnf(s1055,plain,
( ~ spl154_121
| ~ spl154_186 ),
inference(sat_conversion,[],[f4255]) ).
cnf(s1058,plain,
~ spl154_333,
inference(rat,[],[s1052,s542]) ).
cnf(s1059,plain,
~ spl154_137,
inference(rat,[],[s936,s542]) ).
cnf(s1061,plain,
~ spl154_200,
inference(rat,[],[s905,s542]) ).
cnf(s1063,plain,
~ spl154_276,
inference(rat,[],[s854,s542]) ).
cnf(s1064,plain,
~ spl154_204,
inference(rat,[],[s830,s542]) ).
cnf(s1065,plain,
~ spl154_269,
inference(rat,[],[s567,s1058]) ).
cnf(s1068,plain,
( spl154_131
| spl154_195
| spl154_198
| spl154_201 ),
inference(rat,[],[s495,s1064]) ).
cnf(s1070,plain,
( spl154_95
| spl154_164
| spl154_223
| spl154_273 ),
inference(rat,[],[s482,s1063]) ).
cnf(s1071,plain,
( spl154_86
| spl154_157
| spl154_218
| spl154_310 ),
inference(rat,[],[s478,s1065]) ).
cnf(s1076,plain,
( spl154_129
| spl154_131
| spl154_134
| spl154_140 ),
inference(rat,[],[s459,s1059]) ).
cnf(s1081,plain,
~ spl154_120,
inference(rat,[],[s935,s427]) ).
cnf(s1082,plain,
~ spl154_161,
inference(rat,[],[s813,s427]) ).
cnf(s1083,plain,
spl154_103,
inference(rat,[],[s772,s427]) ).
cnf(s1084,plain,
spl154_234,
inference(rat,[],[s753,s427]) ).
cnf(s1085,plain,
~ spl154_118,
inference(rat,[],[s655,s427]) ).
cnf(s1086,plain,
~ spl154_89,
inference(rat,[],[s600,s1083]) ).
cnf(s1087,plain,
~ spl154_106,
inference(rat,[],[s548,s1083]) ).
cnf(s1088,plain,
~ spl154_109,
inference(rat,[],[s547,s1083]) ).
cnf(s1090,plain,
~ spl154_117,
inference(rat,[],[s545,s1083]) ).
cnf(s1091,plain,
~ spl154_131,
inference(rat,[],[s544,s1083]) ).
cnf(s1093,plain,
~ spl154_173,
inference(rat,[],[s916,s1084]) ).
cnf(s1095,plain,
~ spl154_177,
inference(rat,[],[s752,s1084]) ).
cnf(s1096,plain,
~ spl154_110,
inference(rat,[],[s701,s1084]) ).
cnf(s1097,plain,
~ spl154_157,
inference(rat,[],[s513,s1086]) ).
cnf(s1098,plain,
~ spl154_218,
inference(rat,[],[s564,s1093]) ).
cnf(s1099,plain,
( spl154_299
| ~ spl154_331 ),
inference(rat,[],[s291,s542]) ).
cnf(s1100,plain,
( ~ spl154_310
| ~ spl154_331 ),
inference(rat,[],[s290,s542]) ).
cnf(s1103,plain,
( ~ spl154_201
| ~ spl154_294 ),
inference(rat,[],[s242,s1061]) ).
cnf(s1104,plain,
( ~ spl154_138
| ~ spl154_293 ),
inference(rat,[],[s240,s1059]) ).
cnf(s1106,plain,
( spl154_233
| ~ spl154_279 ),
inference(rat,[],[s226,s1084]) ).
cnf(s1109,plain,
( ~ spl154_121
| ~ spl154_238 ),
inference(rat,[],[s186,s1081]) ).
cnf(s1110,plain,
( ~ spl154_174
| ~ spl154_229 ),
inference(rat,[],[s179,s1093]) ).
cnf(s1111,plain,
( ~ spl154_107
| ~ spl154_228 ),
inference(rat,[],[s177,s1087]) ).
cnf(s1112,plain,
( ~ spl154_162
| ~ spl154_219 ),
inference(rat,[],[s170,s1082]) ).
cnf(s1116,plain,
( ~ spl154_184
| spl154_186 ),
inference(rat,[],[s144,s427]) ).
cnf(s1119,plain,
( ~ spl154_102
| spl154_104 ),
inference(rat,[],[s88,s1083]) ).
cnf(s1120,plain,
( ~ spl154_86
| ~ spl154_102 ),
inference(rat,[],[s87,s1083]) ).
cnf(s1121,plain,
( spl154_2
| spl154_3
| spl154_4
| spl154_5
| spl154_6
| spl154_8
| spl154_9
| spl154_10
| spl154_11
| spl154_12
| spl154_14
| spl154_15
| spl154_16
| spl154_17
| spl154_18
| spl154_20
| spl154_21
| spl154_22
| spl154_23
| spl154_24 ),
inference(rat,[],[s3,s61,s43,s25,s7]) ).
cnf(s1124,plain,
~ spl154_331,
inference(rat,[],[s517,s1071,s1053,s1100,s1099,s1098,s1097]) ).
cnf(s1125,plain,
~ spl154_30,
inference(rat,[],[s420,s1124]) ).
cnf(s1126,plain,
( ~ spl154_310
| spl154_76 ),
inference(rat,[],[s1021,s579,s580]) ).
cnf(s1127,plain,
~ spl154_86,
inference(rat,[],[s4,s308,s339,s392,s362,s1116,s1104,s1109,s1055,s1120,s517,s519,s1125]) ).
cnf(s1128,plain,
spl154_310,
inference(rat,[],[s1071,s1097,s1098,s1127]) ).
cnf(s1129,plain,
spl154_98,
inference(rat,[],[s782,s1128]) ).
cnf(s1130,plain,
spl154_143,
inference(rat,[],[s585,s1128]) ).
cnf(s1131,plain,
spl154_179,
inference(rat,[],[s584,s1128]) ).
cnf(s1132,plain,
spl154_207,
inference(rat,[],[s583,s1128]) ).
cnf(s1133,plain,
spl154_246,
inference(rat,[],[s582,s1128]) ).
cnf(s1134,plain,
spl154_261,
inference(rat,[],[s581,s1128]) ).
cnf(s1135,plain,
spl154_299,
inference(rat,[],[s580,s1128]) ).
cnf(s1136,plain,
spl154_305,
inference(rat,[],[s579,s1128]) ).
cnf(s1138,plain,
spl154_76,
inference(rat,[],[s1126,s1128]) ).
cnf(s1139,plain,
~ spl154_95,
inference(rat,[],[s939,s1129]) ).
cnf(s1140,plain,
~ spl154_92,
inference(rat,[],[s889,s1129]) ).
cnf(s1141,plain,
~ spl154_140,
inference(rat,[],[s799,s1129]) ).
cnf(s1142,plain,
~ spl154_126,
inference(rat,[],[s789,s1129]) ).
cnf(s1143,plain,
~ spl154_87,
inference(rat,[],[s528,s1129]) ).
cnf(s1144,plain,
~ spl154_146,
inference(rat,[],[s994,s1130]) ).
cnf(s1145,plain,
~ spl154_115,
inference(rat,[],[s947,s1130]) ).
cnf(s1146,plain,
~ spl154_148,
inference(rat,[],[s802,s1130]) ).
cnf(s1147,plain,
~ spl154_101,
inference(rat,[],[s673,s1130]) ).
cnf(s1148,plain,
~ spl154_129,
inference(rat,[],[s666,s1130]) ).
cnf(s1149,plain,
spl154_43,
inference(rat,[],[s875,s1129,s1130]) ).
cnf(s1154,plain,
~ spl154_104,
inference(rat,[],[s552,s1131]) ).
cnf(s1155,plain,
~ spl154_183,
inference(rat,[],[s887,s1132]) ).
cnf(s1156,plain,
~ spl154_212,
inference(rat,[],[s835,s1132]) ).
cnf(s1157,plain,
~ spl154_209,
inference(rat,[],[s834,s1132]) ).
cnf(s1158,plain,
~ spl154_159,
inference(rat,[],[s803,s1132]) ).
cnf(s1160,plain,
spl154_55,
inference(rat,[],[s878,s1131,s1132]) ).
cnf(s1161,plain,
~ spl154_121,
inference(rat,[],[s1043,s1133]) ).
cnf(s1165,plain,
~ spl154_186,
inference(rat,[],[s825,s1133]) ).
cnf(s1168,plain,
~ spl154_231,
inference(rat,[],[s839,s1134]) ).
cnf(s1169,plain,
spl154_66,
inference(rat,[],[s1027,s1133,s1134]) ).
cnf(s1170,plain,
~ spl154_138,
inference(rat,[],[s1053,s1135]) ).
cnf(s1174,plain,
~ spl154_151,
inference(rat,[],[s924,s1136]) ).
cnf(s1178,plain,
~ spl154_24,
inference(rat,[],[s76,s1138]) ).
cnf(s1179,plain,
~ spl154_20,
inference(rat,[],[s64,s1138]) ).
cnf(s1180,plain,
spl154_134,
inference(rat,[],[s1076,s1148,s1091,s1141]) ).
cnf(s1181,plain,
spl154_123,
inference(rat,[],[s449,s1145,s1090,s1081,s1142]) ).
cnf(s1182,plain,
~ spl154_21,
inference(rat,[],[s67,s1149]) ).
cnf(s1183,plain,
~ spl154_5,
inference(rat,[],[s19,s1149]) ).
cnf(s1184,plain,
~ spl154_102,
inference(rat,[],[s1119,s1154]) ).
cnf(s1185,plain,
~ spl154_22,
inference(rat,[],[s70,s1160]) ).
cnf(s1186,plain,
~ spl154_10,
inference(rat,[],[s34,s1160]) ).
cnf(s1187,plain,
~ spl154_184,
inference(rat,[],[s1116,s1165]) ).
cnf(s1188,plain,
~ spl154_23,
inference(rat,[],[s73,s1169]) ).
cnf(s1189,plain,
~ spl154_15,
inference(rat,[],[s49,s1169]) ).
cnf(s1191,plain,
spl154_63,
inference(rat,[],[s934,s1180,s1181]) ).
cnf(s1192,plain,
~ spl154_26,
inference(rat,[],[s308,s1184]) ).
cnf(s1193,plain,
~ spl154_27,
inference(rat,[],[s339,s1187]) ).
cnf(s1194,plain,
~ spl154_18,
inference(rat,[],[s58,s1191]) ).
cnf(s1195,plain,
~ spl154_14,
inference(rat,[],[s46,s1191]) ).
cnf(s1196,plain,
( ~ spl154_29
| spl154_52 ),
inference(rat,[],[s607,s215,s430,s444,s797,s769,s1068,s434,s907,s213,s1106,s1103,s249,s251,s377,s378,s384,s393,s397,s398,s1085,s1154,s1144,s1095,s1091,s1096,s1170,s1139,s1174,s1156]) ).
cnf(s1197,plain,
spl154_52,
inference(rat,[],[s443,s184,s907,s646,s442,s484,s1112,s1111,s1110,s206,s353,s357,s358,s361,s373,s4,s1196,s1168,s1165,s1147,s1096,s1154,s1157,s1192,s1193,s1125]) ).
cnf(s1198,plain,
~ spl154_17,
inference(rat,[],[s55,s1197]) ).
cnf(s1199,plain,
~ spl154_9,
inference(rat,[],[s31,s1197]) ).
cnf(s1200,plain,
( ~ spl154_164
| spl154_40 ),
inference(rat,[],[s430,s880,s607,s1085,s1154,s1144]) ).
cnf(s1201,plain,
( ~ spl154_29
| spl154_164 ),
inference(rat,[],[s769,s434,s444,s213,s215,s1103,s249,s251,s377,s378,s393,s397,s398,s1096,s1170,s1095,s1139,s1174,s1156]) ).
cnf(s1202,plain,
spl154_164,
inference(rat,[],[s173,s1070,s722,s809,s480,s911,s490,s769,s489,s709,s1112,s193,s353,s355,s366,s4,s1201,s1139,s1086,s1158,s1090,s1155,s1165,s1085,s1161,s1145,s1133,s1192,s1193,s1125]) ).
cnf(s1205,plain,
~ spl154_90,
inference(rat,[],[s607,s1202]) ).
cnf(s1206,plain,
~ spl154_39,
inference(rat,[],[s879,s1088,s1202]) ).
cnf(s1207,plain,
spl154_40,
inference(rat,[],[s1200,s1202]) ).
cnf(s1208,plain,
spl154_132,
inference(rat,[],[s430,s1144,s1154,s1085,s1205]) ).
cnf(s1209,plain,
~ spl154_16,
inference(rat,[],[s52,s1207]) ).
cnf(s1210,plain,
~ spl154_195,
inference(rat,[],[s797,s1208]) ).
cnf(s1211,plain,
~ spl154_197,
inference(rat,[],[s796,s1208]) ).
cnf(s1213,plain,
~ spl154_48,
inference(rat,[],[s883,s1084,s1211]) ).
cnf(s1214,plain,
~ spl154_12,
inference(rat,[],[s719,s480,s1068,s746,s831,s886,s911,s490,s921,s39,s40,s1086,s1158,s1091,s1210,s1090,s1155,s1165,s1084]) ).
cnf(s1215,plain,
~ spl154_127,
inference(rat,[],[s384,s1106,s4,s628,s366,s484,s193,s644,s709,s1192,s1193,s1125,s1147,s1096,s1154,s1133]) ).
cnf(s1216,plain,
~ spl154_8,
inference(rat,[],[s27,s1213]) ).
cnf(s1217,plain,
spl154_124,
inference(rat,[],[s489,s1145,s1161,s1085,s1215]) ).
cnf(s1218,plain,
spl154_56,
inference(rat,[],[s870,s1180,s1217]) ).
cnf(s1219,plain,
~ spl154_189,
inference(rat,[],[s769,s1217]) ).
cnf(s1221,plain,
~ spl154_96,
inference(rat,[],[s616,s1217]) ).
cnf(s1222,plain,
~ spl154_11,
inference(rat,[],[s35,s1218]) ).
cnf(s1224,plain,
spl154_192,
inference(rat,[],[s490,s1165,s1155,s1090,s1219]) ).
cnf(s1225,plain,
~ spl154_168,
inference(rat,[],[s911,s1224]) ).
cnf(s1227,plain,
~ spl154_107,
inference(rat,[],[s4,s384,s357,s1106,s1111,s628,s1192,s1193,s1125]) ).
cnf(s1228,plain,
~ spl154_4,
inference(rat,[],[s15,s1206]) ).
cnf(s1229,plain,
spl154_113,
inference(rat,[],[s484,s1154,s1096,s1147,s1227]) ).
cnf(s1230,plain,
~ spl154_45,
inference(rat,[],[s949,s1144,s1229]) ).
cnf(s1232,plain,
~ spl154_99,
inference(rat,[],[s683,s1229]) ).
cnf(s1240,plain,
~ spl154_6,
inference(rat,[],[s21,s1230]) ).
cnf(s1242,plain,
spl154_93,
inference(rat,[],[s479,s1221,s1205,s1143,s1232]) ).
cnf(s1245,plain,
~ spl154_162,
inference(rat,[],[s540,s1242]) ).
cnf(s1246,plain,
~ spl154_221,
inference(rat,[],[s539,s1242]) ).
cnf(s1252,plain,
spl154_165,
inference(rat,[],[s480,s1225,s1158,s1086,s1245]) ).
cnf(s1258,plain,
~ spl154_224,
inference(rat,[],[s722,s1252]) ).
cnf(s1262,plain,
~ spl154_33,
inference(rat,[],[s873,s1091,s1252]) ).
cnf(s1265,plain,
spl154_227,
inference(rat,[],[s481,s1246,s1140,s1082,s1258]) ).
cnf(s1268,plain,
~ spl154_2,
inference(rat,[],[s9,s1262]) ).
cnf(s1295,plain,
~ spl154_36,
inference(rat,[],[s865,s1146,s1265]) ).
cnf(s1301,plain,
spl154_3,
inference(rat,[],[s1121,s1182,s1179,s1194,s1198,s1209,s1189,s1195,s1199,s1216,s1186,s1214,s1228,s1222,s1183,s1188,s1178,s1240,s1185,s1268]) ).
cnf(s1306,plain,
$false,
inference(rat,[],[s12,s1295,s1301]) ).
fof(f4256,plain,
$false,
inference(avatar_sat_refutation,[],[s1306]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG059+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.19 % Computer : n020.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:23:34 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 Running first-order theorem proving
% 0.10/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.20/1.20 % (448303)Detected formulas, will run a generic FOF schedule.
% 2.20/1.20 % (448309)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1347449370:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.20/1.20 % (448311)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3006763737:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.20/1.20 % (448310)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1900967282:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.20/1.20 % (448312)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3469411937:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.20/1.20 % (448314)dis-21_1_sil=8000:lcm=predicate:random_seed=3502999814:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.20/1.20 % (448308)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1181487804:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.20/1.20 % (448313)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1118190870:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.20/1.20 % (448314)Refutation not found, incomplete strategy
% 2.20/1.20 % (448314)------------------------------
% 2.20/1.20 % (448314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.20/1.20 % (448314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.20/1.20 % (448314)CaDiCaL version: 2.1.3
% 2.20/1.20 % (448314)Termination reason: Refutation not found, incomplete strategy
% 2.20/1.20 % (448314)Time elapsed: 0.020 s
% 2.20/1.20 % (448314)Peak memory usage: 90 MB
% 2.20/1.20 % (448314)Instructions burned: 37 (million)
% 2.20/1.20 % (448311)Refutation not found, incomplete strategy
% 2.20/1.20 % (448311)------------------------------
% 2.20/1.20 % (448311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.20/1.20 % (448311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.20/1.20 % (448311)CaDiCaL version: 2.1.3
% 2.20/1.20 % (448311)Termination reason: Refutation not found, incomplete strategy
% 2.20/1.20 % (448311)Time elapsed: 0.023 s
% 2.20/1.20 % (448311)Peak memory usage: 90 MB
% 2.20/1.20 % (448311)Instructions burned: 47 (million)
% 2.20/1.20 % (448312)Instruction limit reached!
% 2.20/1.20 % (448312)------------------------------
% 2.20/1.20 % (448312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.20/1.20 % (448312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.20/1.20 % (448312)CaDiCaL version: 2.1.3
% 2.20/1.20 % (448312)Termination reason: Instruction limit
% 2.20/1.20 % (448312)Termination phase: Saturation
% 2.20/1.20 % (448312)Time elapsed: 0.053 s
% 2.20/1.20 % (448312)Peak memory usage: 88 MB
% 2.20/1.20 % (448312)Instructions burned: 120 (million)
% 2.20/1.20 % (448313)First to succeed.
% 2.20/1.20 % (448313)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-448303"
% 2.20/1.20 [W928 19:23:35.163123026 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.20/1.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.20/1.20 [W928 19:23:35.163155566 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.20/1.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.20/1.20 [W928 19:23:35.163176606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.20/1.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.20/1.20 [W928 19:23:35.163182768 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.20/1.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.20/1.20 [W928 19:23:35.163195571 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.20/1.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.20/1.20 [W928 19:23:35.163201258 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.20/1.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.20/1.20 % (448322)lrs+10_1_sil=8000:sp=occurrence:random_seed=3442255218:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 2.20/1.20 % (448314)------------------------------
% 2.20/1.20 % (448314)------------------------------
% 2.20/1.20 % (448311)------------------------------
% 2.20/1.20 % (448311)------------------------------
% 2.20/1.20 % (448313)Refutation found. Thanks to Tanya!
% 2.20/1.20 % SZS status Theorem for theBenchmark
% 2.20/1.20 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/1.40 % (448313)------------------------------
% 0.20/1.40 % (448313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/1.40 % (448313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/1.40 % (448313)CaDiCaL version: 2.1.3
% 0.20/1.40 % (448313)Termination reason: Refutation
% 0.20/1.40 % (448313)Time elapsed: 0.073 s
% 0.20/1.40 % (448313)Peak memory usage: 92 MB
% 0.20/1.40 % (448313)Instructions burned: 140 (million)
% 0.20/1.40 % (448313)------------------------------
% 0.20/1.40 % (448313)------------------------------
% 0.20/1.40 % (448303)Success in time 0.533 s
% 0.20/1.40 % Vampire exiting
%------------------------------------------------------------------------------