%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG055+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 : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:08:58 AM UTC 2026
% Result : Theorem 3.25s 1.17s
% Output : Refutation 4.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 220
% Syntax : Number of formulae : 630 ( 87 unt; 213 def)
% Number of atoms : 3655 (2485 equ)
% Maximal formula atoms : 425 ( 5 avg)
% Number of connectives : 4917 (1892 ~;1527 |;1425 &)
% ( 73 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 215 ( 213 usr; 214 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(e2,e2),op(e2,e2))
& e1 = op(op(e2,op(e2,e2)),op(e2,e2))
& e3 = op(e2,op(e2,e2))
& e4 = op(e2,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,conjecture,
~ ( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 ) )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 ) )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 ) )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 ) )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 ) )
& ( ( ( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit ) )
& ( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit ) )
& ( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit ) )
& ( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit ) )
& ( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit ) )
& ( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit ) )
& ( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit ) )
& ( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit ) )
& ( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit ) )
& ( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit ) )
& ( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit ) )
& ( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit ) )
& ( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit ) )
& ( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit ) )
& ( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit ) )
& ( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit ) )
& ( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit ) )
& ( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit ) )
& ( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit ) )
& ( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit ) )
& ( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit ) )
& ( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit ) )
& ( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit ) )
& ( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit ) )
& ( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit ) ) )
| ( ( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit ) )
& ( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit ) )
& ( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit ) )
& ( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit ) )
& ( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit ) )
& ( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit ) )
& ( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit ) )
& ( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit ) )
& ( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit ) )
& ( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit ) )
& ( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit ) )
& ( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit ) )
& ( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit ) )
& ( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit ) )
& ( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit ) )
& ( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit ) )
& ( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit ) )
& ( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit ) )
& ( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit ) )
& ( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit ) )
& ( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit ) )
& ( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit ) )
& ( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit ) )
& ( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit ) )
& ( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit ) ) )
| ( ( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit ) )
& ( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit ) )
& ( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit ) )
& ( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit ) )
& ( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit ) )
& ( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit ) )
& ( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit ) )
& ( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit ) )
& ( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit ) )
& ( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit ) )
& ( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit ) )
& ( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit ) )
& ( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit ) )
& ( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit ) )
& ( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit ) )
& ( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit ) )
& ( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit ) )
& ( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit ) )
& ( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit ) )
& ( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit ) )
& ( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit ) )
& ( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit ) )
& ( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit ) )
& ( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit ) )
& ( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit ) ) )
| ( ( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit ) )
& ( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit ) )
& ( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit ) )
& ( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit ) )
& ( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit ) )
& ( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit ) )
& ( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit ) )
& ( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit ) )
& ( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit ) )
& ( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit ) )
& ( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit ) )
& ( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit ) )
& ( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit ) )
& ( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit ) )
& ( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit ) )
& ( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit ) )
& ( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit ) )
& ( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit ) )
& ( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit ) )
& ( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit ) )
& ( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit ) )
& ( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit ) )
& ( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit ) )
& ( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit ) )
& ( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit ) ) )
| ( ( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit ) )
& ( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit ) )
& ( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit ) )
& ( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit ) )
& ( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit ) )
& ( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit ) )
& ( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit ) )
& ( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit ) )
& ( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit ) )
& ( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit ) )
& ( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit ) )
& ( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit ) )
& ( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit ) )
& ( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit ) )
& ( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit ) )
& ( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit ) )
& ( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit ) )
& ( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit ) )
& ( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit ) )
& ( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit ) )
& ( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit ) )
& ( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit ) )
& ( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit ) )
& ( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit ) )
& ( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f8,negated_conjecture,
~ ~ ( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 ) )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 ) )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 ) )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 ) )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 ) )
& ( ( ( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit ) )
& ( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit ) )
& ( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit ) )
& ( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit ) )
& ( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit ) )
& ( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit ) )
& ( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit ) )
& ( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit ) )
& ( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit ) )
& ( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit ) )
& ( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit ) )
& ( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit ) )
& ( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit ) )
& ( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit ) )
& ( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit ) )
& ( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit ) )
& ( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit ) )
& ( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit ) )
& ( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit ) )
& ( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit ) )
& ( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit ) )
& ( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit ) )
& ( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit ) )
& ( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit ) )
& ( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit ) ) )
| ( ( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit ) )
& ( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit ) )
& ( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit ) )
& ( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit ) )
& ( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit ) )
& ( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit ) )
& ( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit ) )
& ( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit ) )
& ( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit ) )
& ( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit ) )
& ( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit ) )
& ( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit ) )
& ( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit ) )
& ( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit ) )
& ( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit ) )
& ( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit ) )
& ( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit ) )
& ( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit ) )
& ( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit ) )
& ( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit ) )
& ( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit ) )
& ( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit ) )
& ( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit ) )
& ( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit ) )
& ( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit ) ) )
| ( ( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit ) )
& ( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit ) )
& ( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit ) )
& ( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit ) )
& ( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit ) )
& ( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit ) )
& ( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit ) )
& ( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit ) )
& ( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit ) )
& ( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit ) )
& ( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit ) )
& ( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit ) )
& ( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit ) )
& ( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit ) )
& ( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit ) )
& ( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit ) )
& ( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit ) )
& ( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit ) )
& ( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit ) )
& ( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit ) )
& ( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit ) )
& ( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit ) )
& ( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit ) )
& ( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit ) )
& ( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit ) ) )
| ( ( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit ) )
& ( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit ) )
& ( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit ) )
& ( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit ) )
& ( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit ) )
& ( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit ) )
& ( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit ) )
& ( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit ) )
& ( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit ) )
& ( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit ) )
& ( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit ) )
& ( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit ) )
& ( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit ) )
& ( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit ) )
& ( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit ) )
& ( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit ) )
& ( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit ) )
& ( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit ) )
& ( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit ) )
& ( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit ) )
& ( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit ) )
& ( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit ) )
& ( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit ) )
& ( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit ) )
& ( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit ) ) )
| ( ( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit ) )
& ( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit ) )
& ( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit ) )
& ( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit ) )
& ( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit ) )
& ( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit ) )
& ( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit ) )
& ( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit ) )
& ( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit ) )
& ( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit ) )
& ( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit ) )
& ( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit ) )
& ( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit ) )
& ( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit ) )
& ( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit ) )
& ( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit ) )
& ( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit ) )
& ( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit ) )
& ( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit ) )
& ( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit ) )
& ( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit ) )
& ( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit ) )
& ( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit ) )
& ( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit ) )
& ( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f9,plain,
( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 ) )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 ) )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 ) )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 ) )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 ) )
& ( ( ( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit ) )
& ( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit ) )
& ( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit ) )
& ( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit ) )
& ( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit ) )
& ( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit ) )
& ( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit ) )
& ( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit ) )
& ( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit ) )
& ( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit ) )
& ( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit ) )
& ( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit ) )
& ( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit ) )
& ( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit ) )
& ( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit ) )
& ( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit ) )
& ( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit ) )
& ( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit ) )
& ( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit ) )
& ( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit ) )
& ( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit ) )
& ( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit ) )
& ( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit ) )
& ( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit ) )
& ( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit ) ) )
| ( ( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit ) )
& ( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit ) )
& ( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit ) )
& ( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit ) )
& ( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit ) )
& ( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit ) )
& ( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit ) )
& ( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit ) )
& ( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit ) )
& ( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit ) )
& ( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit ) )
& ( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit ) )
& ( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit ) )
& ( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit ) )
& ( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit ) )
& ( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit ) )
& ( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit ) )
& ( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit ) )
& ( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit ) )
& ( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit ) )
& ( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit ) )
& ( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit ) )
& ( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit ) )
& ( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit ) )
& ( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit ) ) )
| ( ( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit ) )
& ( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit ) )
& ( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit ) )
& ( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit ) )
& ( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit ) )
& ( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit ) )
& ( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit ) )
& ( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit ) )
& ( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit ) )
& ( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit ) )
& ( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit ) )
& ( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit ) )
& ( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit ) )
& ( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit ) )
& ( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit ) )
& ( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit ) )
& ( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit ) )
& ( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit ) )
& ( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit ) )
& ( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit ) )
& ( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit ) )
& ( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit ) )
& ( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit ) )
& ( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit ) )
& ( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit ) ) )
| ( ( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit ) )
& ( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit ) )
& ( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit ) )
& ( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit ) )
& ( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit ) )
& ( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit ) )
& ( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit ) )
& ( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit ) )
& ( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit ) )
& ( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit ) )
& ( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit ) )
& ( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit ) )
& ( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit ) )
& ( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit ) )
& ( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit ) )
& ( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit ) )
& ( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit ) )
& ( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit ) )
& ( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit ) )
& ( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit ) )
& ( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit ) )
& ( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit ) )
& ( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit ) )
& ( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit ) )
& ( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit ) ) )
| ( ( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit ) )
& ( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit ) )
& ( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit ) )
& ( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit ) )
& ( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit ) )
& ( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit ) )
& ( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit ) )
& ( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit ) )
& ( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit ) )
& ( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit ) )
& ( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit ) )
& ( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit ) )
& ( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit ) )
& ( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit ) )
& ( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit ) )
& ( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit ) )
& ( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit ) )
& ( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit ) )
& ( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit ) )
& ( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit ) )
& ( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit ) )
& ( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit ) )
& ( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit ) )
& ( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit ) )
& ( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit ) ) ) ) ),
inference(flattening,[],[f8]) ).
fof(f10,definition,
( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11,definition,
( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f12,definition,
( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f13,definition,
( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f14,definition,
( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f15,definition,
( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f16,definition,
( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f17,definition,
( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f18,definition,
( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f19,definition,
( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f20,definition,
( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f21,definition,
( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f22,definition,
( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f23,definition,
( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f24,definition,
( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f25,definition,
( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f26,definition,
( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f27,definition,
( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f28,definition,
( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f29,definition,
( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f30,definition,
( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f31,definition,
( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f32,definition,
( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f33,definition,
( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit )
| ~ sP23 ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f34,definition,
( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit )
| ~ sP24 ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f35,definition,
( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit )
| ~ sP25 ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f36,definition,
( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit )
| ~ sP26 ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f37,definition,
( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit )
| ~ sP27 ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f38,definition,
( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit )
| ~ sP28 ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f39,definition,
( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit )
| ~ sP29 ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f40,definition,
( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit )
| ~ sP30 ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f41,definition,
( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit )
| ~ sP31 ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f42,definition,
( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit )
| ~ sP32 ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f43,definition,
( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit )
| ~ sP33 ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f44,definition,
( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit )
| ~ sP34 ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f45,definition,
( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit )
| ~ sP35 ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f46,definition,
( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit )
| ~ sP36 ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f47,definition,
( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit )
| ~ sP37 ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f48,definition,
( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit )
| ~ sP38 ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f49,definition,
( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit )
| ~ sP39 ),
introduced(definition,[new_symbols(definition,[sP39])],[predicate_definition_introduction]) ).
fof(f50,definition,
( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit )
| ~ sP40 ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f51,definition,
( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit )
| ~ sP41 ),
introduced(definition,[new_symbols(definition,[sP41])],[predicate_definition_introduction]) ).
fof(f52,definition,
( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit )
| ~ sP42 ),
introduced(definition,[new_symbols(definition,[sP42])],[predicate_definition_introduction]) ).
fof(f53,definition,
( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit )
| ~ sP43 ),
introduced(definition,[new_symbols(definition,[sP43])],[predicate_definition_introduction]) ).
fof(f54,definition,
( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit )
| ~ sP44 ),
introduced(definition,[new_symbols(definition,[sP44])],[predicate_definition_introduction]) ).
fof(f55,definition,
( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit )
| ~ sP45 ),
introduced(definition,[new_symbols(definition,[sP45])],[predicate_definition_introduction]) ).
fof(f56,definition,
( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit )
| ~ sP46 ),
introduced(definition,[new_symbols(definition,[sP46])],[predicate_definition_introduction]) ).
fof(f57,definition,
( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit )
| ~ sP47 ),
introduced(definition,[new_symbols(definition,[sP47])],[predicate_definition_introduction]) ).
fof(f58,definition,
( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit )
| ~ sP48 ),
introduced(definition,[new_symbols(definition,[sP48])],[predicate_definition_introduction]) ).
fof(f59,definition,
( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit )
| ~ sP49 ),
introduced(definition,[new_symbols(definition,[sP49])],[predicate_definition_introduction]) ).
fof(f60,definition,
( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit )
| ~ sP50 ),
introduced(definition,[new_symbols(definition,[sP50])],[predicate_definition_introduction]) ).
fof(f61,definition,
( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit )
| ~ sP51 ),
introduced(definition,[new_symbols(definition,[sP51])],[predicate_definition_introduction]) ).
fof(f62,definition,
( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit )
| ~ sP52 ),
introduced(definition,[new_symbols(definition,[sP52])],[predicate_definition_introduction]) ).
fof(f63,definition,
( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit )
| ~ sP53 ),
introduced(definition,[new_symbols(definition,[sP53])],[predicate_definition_introduction]) ).
fof(f64,definition,
( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit )
| ~ sP54 ),
introduced(definition,[new_symbols(definition,[sP54])],[predicate_definition_introduction]) ).
fof(f65,definition,
( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit )
| ~ sP55 ),
introduced(definition,[new_symbols(definition,[sP55])],[predicate_definition_introduction]) ).
fof(f66,definition,
( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit )
| ~ sP56 ),
introduced(definition,[new_symbols(definition,[sP56])],[predicate_definition_introduction]) ).
fof(f67,definition,
( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit )
| ~ sP57 ),
introduced(definition,[new_symbols(definition,[sP57])],[predicate_definition_introduction]) ).
fof(f68,definition,
( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit )
| ~ sP58 ),
introduced(definition,[new_symbols(definition,[sP58])],[predicate_definition_introduction]) ).
fof(f69,definition,
( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit )
| ~ sP59 ),
introduced(definition,[new_symbols(definition,[sP59])],[predicate_definition_introduction]) ).
fof(f70,definition,
( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit )
| ~ sP60 ),
introduced(definition,[new_symbols(definition,[sP60])],[predicate_definition_introduction]) ).
fof(f71,definition,
( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit )
| ~ sP61 ),
introduced(definition,[new_symbols(definition,[sP61])],[predicate_definition_introduction]) ).
fof(f72,definition,
( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit )
| ~ sP62 ),
introduced(definition,[new_symbols(definition,[sP62])],[predicate_definition_introduction]) ).
fof(f73,definition,
( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit )
| ~ sP63 ),
introduced(definition,[new_symbols(definition,[sP63])],[predicate_definition_introduction]) ).
fof(f74,definition,
( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit )
| ~ sP64 ),
introduced(definition,[new_symbols(definition,[sP64])],[predicate_definition_introduction]) ).
fof(f75,definition,
( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit )
| ~ sP65 ),
introduced(definition,[new_symbols(definition,[sP65])],[predicate_definition_introduction]) ).
fof(f76,definition,
( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit )
| ~ sP66 ),
introduced(definition,[new_symbols(definition,[sP66])],[predicate_definition_introduction]) ).
fof(f77,definition,
( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit )
| ~ sP67 ),
introduced(definition,[new_symbols(definition,[sP67])],[predicate_definition_introduction]) ).
fof(f78,definition,
( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit )
| ~ sP68 ),
introduced(definition,[new_symbols(definition,[sP68])],[predicate_definition_introduction]) ).
fof(f79,definition,
( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit )
| ~ sP69 ),
introduced(definition,[new_symbols(definition,[sP69])],[predicate_definition_introduction]) ).
fof(f80,definition,
( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit )
| ~ sP70 ),
introduced(definition,[new_symbols(definition,[sP70])],[predicate_definition_introduction]) ).
fof(f81,definition,
( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit )
| ~ sP71 ),
introduced(definition,[new_symbols(definition,[sP71])],[predicate_definition_introduction]) ).
fof(f82,definition,
( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit )
| ~ sP72 ),
introduced(definition,[new_symbols(definition,[sP72])],[predicate_definition_introduction]) ).
fof(f83,definition,
( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit )
| ~ sP73 ),
introduced(definition,[new_symbols(definition,[sP73])],[predicate_definition_introduction]) ).
fof(f84,definition,
( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit )
| ~ sP74 ),
introduced(definition,[new_symbols(definition,[sP74])],[predicate_definition_introduction]) ).
fof(f85,definition,
( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit )
| ~ sP75 ),
introduced(definition,[new_symbols(definition,[sP75])],[predicate_definition_introduction]) ).
fof(f86,definition,
( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit )
| ~ sP76 ),
introduced(definition,[new_symbols(definition,[sP76])],[predicate_definition_introduction]) ).
fof(f87,definition,
( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit )
| ~ sP77 ),
introduced(definition,[new_symbols(definition,[sP77])],[predicate_definition_introduction]) ).
fof(f88,definition,
( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit )
| ~ sP78 ),
introduced(definition,[new_symbols(definition,[sP78])],[predicate_definition_introduction]) ).
fof(f89,definition,
( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit )
| ~ sP79 ),
introduced(definition,[new_symbols(definition,[sP79])],[predicate_definition_introduction]) ).
fof(f90,definition,
( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit )
| ~ sP80 ),
introduced(definition,[new_symbols(definition,[sP80])],[predicate_definition_introduction]) ).
fof(f91,definition,
( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit )
| ~ sP81 ),
introduced(definition,[new_symbols(definition,[sP81])],[predicate_definition_introduction]) ).
fof(f92,definition,
( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit )
| ~ sP82 ),
introduced(definition,[new_symbols(definition,[sP82])],[predicate_definition_introduction]) ).
fof(f93,definition,
( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit )
| ~ sP83 ),
introduced(definition,[new_symbols(definition,[sP83])],[predicate_definition_introduction]) ).
fof(f94,definition,
( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit )
| ~ sP84 ),
introduced(definition,[new_symbols(definition,[sP84])],[predicate_definition_introduction]) ).
fof(f95,definition,
( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit )
| ~ sP85 ),
introduced(definition,[new_symbols(definition,[sP85])],[predicate_definition_introduction]) ).
fof(f96,definition,
( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit )
| ~ sP86 ),
introduced(definition,[new_symbols(definition,[sP86])],[predicate_definition_introduction]) ).
fof(f97,definition,
( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit )
| ~ sP87 ),
introduced(definition,[new_symbols(definition,[sP87])],[predicate_definition_introduction]) ).
fof(f98,definition,
( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit )
| ~ sP88 ),
introduced(definition,[new_symbols(definition,[sP88])],[predicate_definition_introduction]) ).
fof(f99,definition,
( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit )
| ~ sP89 ),
introduced(definition,[new_symbols(definition,[sP89])],[predicate_definition_introduction]) ).
fof(f100,definition,
( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit )
| ~ sP90 ),
introduced(definition,[new_symbols(definition,[sP90])],[predicate_definition_introduction]) ).
fof(f101,definition,
( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit )
| ~ sP91 ),
introduced(definition,[new_symbols(definition,[sP91])],[predicate_definition_introduction]) ).
fof(f102,definition,
( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit )
| ~ sP92 ),
introduced(definition,[new_symbols(definition,[sP92])],[predicate_definition_introduction]) ).
fof(f103,definition,
( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit )
| ~ sP93 ),
introduced(definition,[new_symbols(definition,[sP93])],[predicate_definition_introduction]) ).
fof(f104,definition,
( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit )
| ~ sP94 ),
introduced(definition,[new_symbols(definition,[sP94])],[predicate_definition_introduction]) ).
fof(f105,definition,
( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit )
| ~ sP95 ),
introduced(definition,[new_symbols(definition,[sP95])],[predicate_definition_introduction]) ).
fof(f106,definition,
( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit )
| ~ sP96 ),
introduced(definition,[new_symbols(definition,[sP96])],[predicate_definition_introduction]) ).
fof(f107,definition,
( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit )
| ~ sP97 ),
introduced(definition,[new_symbols(definition,[sP97])],[predicate_definition_introduction]) ).
fof(f108,definition,
( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit )
| ~ sP98 ),
introduced(definition,[new_symbols(definition,[sP98])],[predicate_definition_introduction]) ).
fof(f109,definition,
( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit )
| ~ sP99 ),
introduced(definition,[new_symbols(definition,[sP99])],[predicate_definition_introduction]) ).
fof(f110,definition,
( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit )
| ~ sP100 ),
introduced(definition,[new_symbols(definition,[sP100])],[predicate_definition_introduction]) ).
fof(f111,definition,
( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit )
| ~ sP101 ),
introduced(definition,[new_symbols(definition,[sP101])],[predicate_definition_introduction]) ).
fof(f112,definition,
( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit )
| ~ sP102 ),
introduced(definition,[new_symbols(definition,[sP102])],[predicate_definition_introduction]) ).
fof(f113,definition,
( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit )
| ~ sP103 ),
introduced(definition,[new_symbols(definition,[sP103])],[predicate_definition_introduction]) ).
fof(f114,definition,
( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit )
| ~ sP104 ),
introduced(definition,[new_symbols(definition,[sP104])],[predicate_definition_introduction]) ).
fof(f115,definition,
( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit )
| ~ sP105 ),
introduced(definition,[new_symbols(definition,[sP105])],[predicate_definition_introduction]) ).
fof(f116,definition,
( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit )
| ~ sP106 ),
introduced(definition,[new_symbols(definition,[sP106])],[predicate_definition_introduction]) ).
fof(f117,definition,
( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit )
| ~ sP107 ),
introduced(definition,[new_symbols(definition,[sP107])],[predicate_definition_introduction]) ).
fof(f118,definition,
( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit )
| ~ sP108 ),
introduced(definition,[new_symbols(definition,[sP108])],[predicate_definition_introduction]) ).
fof(f119,definition,
( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit )
| ~ sP109 ),
introduced(definition,[new_symbols(definition,[sP109])],[predicate_definition_introduction]) ).
fof(f120,definition,
( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit )
| ~ sP110 ),
introduced(definition,[new_symbols(definition,[sP110])],[predicate_definition_introduction]) ).
fof(f121,definition,
( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit )
| ~ sP111 ),
introduced(definition,[new_symbols(definition,[sP111])],[predicate_definition_introduction]) ).
fof(f122,definition,
( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit )
| ~ sP112 ),
introduced(definition,[new_symbols(definition,[sP112])],[predicate_definition_introduction]) ).
fof(f123,definition,
( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit )
| ~ sP113 ),
introduced(definition,[new_symbols(definition,[sP113])],[predicate_definition_introduction]) ).
fof(f124,definition,
( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit )
| ~ sP114 ),
introduced(definition,[new_symbols(definition,[sP114])],[predicate_definition_introduction]) ).
fof(f125,definition,
( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit )
| ~ sP115 ),
introduced(definition,[new_symbols(definition,[sP115])],[predicate_definition_introduction]) ).
fof(f126,definition,
( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit )
| ~ sP116 ),
introduced(definition,[new_symbols(definition,[sP116])],[predicate_definition_introduction]) ).
fof(f127,definition,
( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit )
| ~ sP117 ),
introduced(definition,[new_symbols(definition,[sP117])],[predicate_definition_introduction]) ).
fof(f128,definition,
( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit )
| ~ sP118 ),
introduced(definition,[new_symbols(definition,[sP118])],[predicate_definition_introduction]) ).
fof(f129,definition,
( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit )
| ~ sP119 ),
introduced(definition,[new_symbols(definition,[sP119])],[predicate_definition_introduction]) ).
fof(f130,definition,
( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit )
| ~ sP120 ),
introduced(definition,[new_symbols(definition,[sP120])],[predicate_definition_introduction]) ).
fof(f131,definition,
( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit )
| ~ sP121 ),
introduced(definition,[new_symbols(definition,[sP121])],[predicate_definition_introduction]) ).
fof(f132,definition,
( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit )
| ~ sP122 ),
introduced(definition,[new_symbols(definition,[sP122])],[predicate_definition_introduction]) ).
fof(f133,definition,
( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit )
| ~ sP123 ),
introduced(definition,[new_symbols(definition,[sP123])],[predicate_definition_introduction]) ).
fof(f134,definition,
( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit )
| ~ sP124 ),
introduced(definition,[new_symbols(definition,[sP124])],[predicate_definition_introduction]) ).
fof(f135,definition,
( ( sP24
& sP23
& sP22
& sP21
& sP20
& sP19
& sP18
& sP17
& sP16
& sP15
& sP14
& sP13
& sP12
& sP11
& sP10
& sP9
& sP8
& sP7
& sP6
& sP5
& sP4
& sP3
& sP2
& sP1
& sP0 )
| ~ sP125 ),
introduced(definition,[new_symbols(definition,[sP125])],[predicate_definition_introduction]) ).
fof(f136,definition,
( ( sP49
& sP48
& sP47
& sP46
& sP45
& sP44
& sP43
& sP42
& sP41
& sP40
& sP39
& sP38
& sP37
& sP36
& sP35
& sP34
& sP33
& sP32
& sP31
& sP30
& sP29
& sP28
& sP27
& sP26
& sP25 )
| ~ sP126 ),
introduced(definition,[new_symbols(definition,[sP126])],[predicate_definition_introduction]) ).
fof(f137,definition,
( ( sP74
& sP73
& sP72
& sP71
& sP70
& sP69
& sP68
& sP67
& sP66
& sP65
& sP64
& sP63
& sP62
& sP61
& sP60
& sP59
& sP58
& sP57
& sP56
& sP55
& sP54
& sP53
& sP52
& sP51
& sP50 )
| ~ sP127 ),
introduced(definition,[new_symbols(definition,[sP127])],[predicate_definition_introduction]) ).
fof(f138,definition,
( ( sP99
& sP98
& sP97
& sP96
& sP95
& sP94
& sP93
& sP92
& sP91
& sP90
& sP89
& sP88
& sP87
& sP86
& sP85
& sP84
& sP83
& sP82
& sP81
& sP80
& sP79
& sP78
& sP77
& sP76
& sP75 )
| ~ sP128 ),
introduced(definition,[new_symbols(definition,[sP128])],[predicate_definition_introduction]) ).
fof(f139,definition,
( ( sP124
& sP123
& sP122
& sP121
& sP120
& sP119
& sP118
& sP117
& sP116
& sP115
& sP114
& sP113
& sP112
& sP111
& sP110
& sP109
& sP108
& sP107
& sP106
& sP105
& sP104
& sP103
& sP102
& sP101
& sP100 )
| ~ sP129 ),
introduced(definition,[new_symbols(definition,[sP129])],[predicate_definition_introduction]) ).
fof(f140,definition,
( ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 )
| ~ sP130 ),
introduced(definition,[new_symbols(definition,[sP130])],[predicate_definition_introduction]) ).
fof(f141,definition,
( ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ~ sP131 ),
introduced(definition,[new_symbols(definition,[sP131])],[predicate_definition_introduction]) ).
fof(f142,definition,
( ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 )
| ~ sP132 ),
introduced(definition,[new_symbols(definition,[sP132])],[predicate_definition_introduction]) ).
fof(f143,definition,
( ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ~ sP133 ),
introduced(definition,[new_symbols(definition,[sP133])],[predicate_definition_introduction]) ).
fof(f144,definition,
( ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 )
| ~ sP134 ),
introduced(definition,[new_symbols(definition,[sP134])],[predicate_definition_introduction]) ).
fof(f145,definition,
( ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ~ sP135 ),
introduced(definition,[new_symbols(definition,[sP135])],[predicate_definition_introduction]) ).
fof(f146,definition,
( ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 )
| ~ sP136 ),
introduced(definition,[new_symbols(definition,[sP136])],[predicate_definition_introduction]) ).
fof(f147,definition,
( ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ~ sP137 ),
introduced(definition,[new_symbols(definition,[sP137])],[predicate_definition_introduction]) ).
fof(f148,definition,
( ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 )
| ~ sP138 ),
introduced(definition,[new_symbols(definition,[sP138])],[predicate_definition_introduction]) ).
fof(f149,definition,
( ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ~ sP139 ),
introduced(definition,[new_symbols(definition,[sP139])],[predicate_definition_introduction]) ).
fof(f150,plain,
( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| sP139
| sP138 )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| sP137
| sP136 )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| sP135
| sP134 )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| sP133
| sP132 )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| sP131
| sP130 )
& ( sP129
| sP128
| sP127
| sP126
| sP125 ) ),
inference(definition_folding,[],[f9,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(f159,plain,
( ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ~ sP131 ),
inference(nnf_transformation,[],[f141]) ).
fof(f160,plain,
( ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 )
| ~ sP130 ),
inference(nnf_transformation,[],[f140]) ).
fof(f161,plain,
( ( sP124
& sP123
& sP122
& sP121
& sP120
& sP119
& sP118
& sP117
& sP116
& sP115
& sP114
& sP113
& sP112
& sP111
& sP110
& sP109
& sP108
& sP107
& sP106
& sP105
& sP104
& sP103
& sP102
& sP101
& sP100 )
| ~ sP129 ),
inference(nnf_transformation,[],[f139]) ).
fof(f162,plain,
( ( sP99
& sP98
& sP97
& sP96
& sP95
& sP94
& sP93
& sP92
& sP91
& sP90
& sP89
& sP88
& sP87
& sP86
& sP85
& sP84
& sP83
& sP82
& sP81
& sP80
& sP79
& sP78
& sP77
& sP76
& sP75 )
| ~ sP128 ),
inference(nnf_transformation,[],[f138]) ).
fof(f163,plain,
( ( sP74
& sP73
& sP72
& sP71
& sP70
& sP69
& sP68
& sP67
& sP66
& sP65
& sP64
& sP63
& sP62
& sP61
& sP60
& sP59
& sP58
& sP57
& sP56
& sP55
& sP54
& sP53
& sP52
& sP51
& sP50 )
| ~ sP127 ),
inference(nnf_transformation,[],[f137]) ).
fof(f164,plain,
( ( sP49
& sP48
& sP47
& sP46
& sP45
& sP44
& sP43
& sP42
& sP41
& sP40
& sP39
& sP38
& sP37
& sP36
& sP35
& sP34
& sP33
& sP32
& sP31
& sP30
& sP29
& sP28
& sP27
& sP26
& sP25 )
| ~ sP126 ),
inference(nnf_transformation,[],[f136]) ).
fof(f165,plain,
( ( sP24
& sP23
& sP22
& sP21
& sP20
& sP19
& sP18
& sP17
& sP16
& sP15
& sP14
& sP13
& sP12
& sP11
& sP10
& sP9
& sP8
& sP7
& sP6
& sP5
& sP4
& sP3
& sP2
& sP1
& sP0 )
| ~ sP125 ),
inference(nnf_transformation,[],[f135]) ).
fof(f190,plain,
( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit )
| ~ sP100 ),
inference(nnf_transformation,[],[f110]) ).
fof(f204,plain,
( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit )
| ~ sP86 ),
inference(nnf_transformation,[],[f96]) ).
fof(f210,plain,
( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit )
| ~ sP80 ),
inference(nnf_transformation,[],[f90]) ).
fof(f220,plain,
( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit )
| ~ sP70 ),
inference(nnf_transformation,[],[f80]) ).
fof(f225,plain,
( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit )
| ~ sP65 ),
inference(nnf_transformation,[],[f75]) ).
fof(f235,plain,
( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit )
| ~ sP55 ),
inference(nnf_transformation,[],[f65]) ).
fof(f255,plain,
( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit )
| ~ sP35 ),
inference(nnf_transformation,[],[f45]) ).
fof(f257,plain,
( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit )
| ~ sP33 ),
inference(nnf_transformation,[],[f43]) ).
fof(f278,plain,
( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit )
| ~ sP12 ),
inference(nnf_transformation,[],[f22]) ).
fof(f292,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(f297,plain,
( e0 = op(e3,e3)
| e1 = op(e3,e3)
| e2 = op(e3,e3)
| e3 = op(e3,e3)
| e4 = op(e3,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f302,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(f306,plain,
( e0 = op(e1,e4)
| e1 = op(e1,e4)
| e2 = op(e1,e4)
| e3 = op(e1,e4)
| e4 = op(e1,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f316,plain,
( e0 = unit
| e1 = unit
| e2 = unit
| e3 = unit
| e4 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f317,plain,
e4 = op(e4,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f318,plain,
e4 = op(unit,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f319,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f320,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f321,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f331,plain,
( e2 = op(e0,e4)
| e2 = op(e1,e4)
| e2 = op(e2,e4)
| e2 = op(e3,e4)
| e2 = op(e4,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f338,plain,
( e4 = op(e3,e0)
| e4 = op(e3,e1)
| e4 = op(e3,e2)
| e4 = op(e3,e3)
| e4 = op(e3,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f358,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(f377,plain,
op(e4,e3) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f379,plain,
op(e4,e2) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f384,plain,
op(e4,e0) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f386,plain,
op(e4,e0) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f387,plain,
op(e3,e3) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f391,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f394,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f397,plain,
op(e2,e3) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f398,plain,
op(e2,e2) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f400,plain,
op(e2,e1) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f430,plain,
op(e1,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f431,plain,
op(e1,e4) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f432,plain,
op(e1,e4) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f436,plain,
op(e0,e4) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f437,plain,
op(e3,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f438,plain,
op(e2,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f439,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f442,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f443,plain,
op(e0,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f449,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f452,plain,
op(e1,e2) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f455,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f461,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f467,plain,
op(e3,e0) != op(e4,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f470,plain,
op(e1,e0) != op(e4,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f479,plain,
e2 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f480,plain,
e1 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f485,plain,
e0 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f487,plain,
e4 = op(e2,e2),
inference(cnf_transformation,[],[f6]) ).
fof(f488,plain,
e3 = op(e2,op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f489,plain,
e1 = op(op(e2,op(e2,e2)),op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f490,plain,
e0 = op(op(e2,e2),op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f508,plain,
( e4 != op(e3,op(e3,e4))
| ~ sP131 ),
inference(cnf_transformation,[],[f159]) ).
fof(f509,plain,
( e4 = op(e4,op(e4,e4))
| ~ sP130 ),
inference(cnf_transformation,[],[f160]) ).
fof(f510,plain,
( e4 != op(e4,op(e4,e4))
| ~ sP130 ),
inference(cnf_transformation,[],[f160]) ).
fof(f511,plain,
( sP100
| ~ sP129 ),
inference(cnf_transformation,[],[f161]) ).
fof(f541,plain,
( sP80
| ~ sP128 ),
inference(cnf_transformation,[],[f162]) ).
fof(f547,plain,
( sP86
| ~ sP128 ),
inference(cnf_transformation,[],[f162]) ).
fof(f566,plain,
( sP55
| ~ sP127 ),
inference(cnf_transformation,[],[f163]) ).
fof(f576,plain,
( sP65
| ~ sP127 ),
inference(cnf_transformation,[],[f163]) ).
fof(f581,plain,
( sP70
| ~ sP127 ),
inference(cnf_transformation,[],[f163]) ).
fof(f594,plain,
( sP33
| ~ sP126 ),
inference(cnf_transformation,[],[f164]) ).
fof(f596,plain,
( sP35
| ~ sP126 ),
inference(cnf_transformation,[],[f164]) ).
fof(f623,plain,
( sP12
| ~ sP125 ),
inference(cnf_transformation,[],[f165]) ).
fof(f684,plain,
( e0 != op(e4,e4)
| e0 != unit
| ~ sP100 ),
inference(cnf_transformation,[],[f190]) ).
fof(f685,plain,
( e0 != op(e4,e4)
| e4 = op(e4,e0)
| ~ sP100 ),
inference(cnf_transformation,[],[f190]) ).
fof(f713,plain,
( e1 != op(e2,e3)
| e3 = op(e2,e1)
| ~ sP86 ),
inference(cnf_transformation,[],[f204]) ).
fof(f724,plain,
( e1 != op(e3,e4)
| e1 != unit
| ~ sP80 ),
inference(cnf_transformation,[],[f210]) ).
fof(f725,plain,
( e1 != op(e3,e4)
| e4 = op(e3,e1)
| ~ sP80 ),
inference(cnf_transformation,[],[f210]) ).
fof(f745,plain,
( e2 != op(e0,e4)
| e4 = op(e0,e2)
| ~ sP70 ),
inference(cnf_transformation,[],[f220]) ).
fof(f755,plain,
( e2 != op(e1,e4)
| e4 = op(e1,e2)
| ~ sP65 ),
inference(cnf_transformation,[],[f225]) ).
fof(f775,plain,
( e2 != op(e3,e4)
| e4 = op(e3,e2)
| ~ sP55 ),
inference(cnf_transformation,[],[f235]) ).
fof(f815,plain,
( e3 != op(e2,e4)
| e4 = op(e2,e3)
| ~ sP35 ),
inference(cnf_transformation,[],[f255]) ).
fof(f819,plain,
( e3 != op(e3,e1)
| e1 = op(e3,e3)
| ~ sP33 ),
inference(cnf_transformation,[],[f257]) ).
fof(f861,plain,
( e4 != op(e2,e2)
| e2 = op(e2,e4)
| ~ sP12 ),
inference(cnf_transformation,[],[f278]) ).
fof(f886,plain,
( sP129
| sP128
| sP127
| sP126
| sP125 ),
inference(cnf_transformation,[],[f150]) ).
fof(f891,plain,
( e4 != op(e0,op(e0,e4))
| e1 = op(e4,op(e1,e4))
| e2 = op(e4,op(e2,e4))
| sP131
| sP130 ),
inference(cnf_transformation,[],[f150]) ).
fof(f928,definition,
( spl140_1
<=> sP125 ),
introduced(definition,[new_symbols(definition,[spl140_1])],[avatar_definition]) ).
fof(f932,definition,
( spl140_2
<=> sP126 ),
introduced(definition,[new_symbols(definition,[spl140_2])],[avatar_definition]) ).
fof(f936,definition,
( spl140_3
<=> sP127 ),
introduced(definition,[new_symbols(definition,[spl140_3])],[avatar_definition]) ).
fof(f940,definition,
( spl140_4
<=> sP128 ),
introduced(definition,[new_symbols(definition,[spl140_4])],[avatar_definition]) ).
fof(f944,definition,
( spl140_5
<=> sP129 ),
introduced(definition,[new_symbols(definition,[spl140_5])],[avatar_definition]) ).
fof(f947,plain,
( spl140_1
| spl140_2
| spl140_3
| spl140_4
| spl140_5 ),
inference(avatar_split_clause,[],[f886,f944,f940,f936,f932,f928]) ).
fof(f949,definition,
( spl140_6
<=> sP130 ),
introduced(definition,[new_symbols(definition,[spl140_6])],[avatar_definition]) ).
fof(f953,definition,
( spl140_7
<=> sP131 ),
introduced(definition,[new_symbols(definition,[spl140_7])],[avatar_definition]) ).
fof(f957,definition,
( spl140_8
<=> e2 = op(e4,op(e2,e4)) ),
introduced(definition,[new_symbols(definition,[spl140_8])],[avatar_definition]) ).
fof(f958,plain,
( e2 != op(e4,op(e2,e4))
| spl140_8 ),
inference(avatar_component_clause,[],[f957]) ).
fof(f959,plain,
( e2 = op(e4,op(e2,e4))
| ~ spl140_8 ),
inference(avatar_component_clause,[],[f957]) ).
fof(f961,definition,
( spl140_9
<=> e1 = op(e4,op(e1,e4)) ),
introduced(definition,[new_symbols(definition,[spl140_9])],[avatar_definition]) ).
fof(f963,plain,
( e1 = op(e4,op(e1,e4))
| ~ spl140_9 ),
inference(avatar_component_clause,[],[f961]) ).
fof(f981,definition,
( spl140_13
<=> e4 = op(e0,op(e0,e4)) ),
introduced(definition,[new_symbols(definition,[spl140_13])],[avatar_definition]) ).
fof(f983,plain,
( e4 != op(e0,op(e0,e4))
| spl140_13 ),
inference(avatar_component_clause,[],[f981]) ).
fof(f984,plain,
( spl140_6
| spl140_7
| spl140_8
| spl140_9
| ~ spl140_13 ),
inference(avatar_split_clause,[],[f891,f981,f961,f957,f953,f949]) ).
fof(f1037,definition,
( spl140_24
<=> e2 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl140_24])],[avatar_definition]) ).
fof(f1038,plain,
( e2 != op(e2,op(e2,e2))
| spl140_24 ),
inference(avatar_component_clause,[],[f1037]) ).
fof(f1039,plain,
( e2 = op(e2,op(e2,e2))
| ~ spl140_24 ),
inference(avatar_component_clause,[],[f1037]) ).
fof(f1141,definition,
( spl140_44
<=> e4 = unit ),
introduced(definition,[new_symbols(definition,[spl140_44])],[avatar_definition]) ).
fof(f1142,plain,
( e4 = unit
| ~ spl140_44 ),
inference(avatar_component_clause,[],[f1141]) ).
fof(f1154,definition,
( spl140_47
<=> e4 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl140_47])],[avatar_definition]) ).
fof(f1155,plain,
( e4 = op(e4,e3)
| ~ spl140_47 ),
inference(avatar_component_clause,[],[f1154]) ).
fof(f1173,definition,
( spl140_51
<=> e2 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl140_51])],[avatar_definition]) ).
fof(f1175,plain,
( e2 = op(e4,e4)
| ~ spl140_51 ),
inference(avatar_component_clause,[],[f1173]) ).
fof(f1182,definition,
( spl140_53
<=> e4 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl140_53])],[avatar_definition]) ).
fof(f1183,plain,
( e4 = op(e4,e1)
| ~ spl140_53 ),
inference(avatar_component_clause,[],[f1182]) ).
fof(f1184,plain,
( e4 != op(e4,e1)
| spl140_53 ),
inference(avatar_component_clause,[],[f1182]) ).
fof(f1196,definition,
( spl140_56
<=> e4 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl140_56])],[avatar_definition]) ).
fof(f1197,plain,
( e4 = op(e4,e0)
| ~ spl140_56 ),
inference(avatar_component_clause,[],[f1196]) ).
fof(f1201,definition,
( spl140_57
<=> e0 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl140_57])],[avatar_definition]) ).
fof(f1203,plain,
( e0 = op(e4,e4)
| ~ spl140_57 ),
inference(avatar_component_clause,[],[f1201]) ).
fof(f1210,definition,
( spl140_59
<=> e4 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl140_59])],[avatar_definition]) ).
fof(f1211,plain,
( e4 = op(e3,e4)
| ~ spl140_59 ),
inference(avatar_component_clause,[],[f1210]) ).
fof(f1219,definition,
( spl140_61
<=> e4 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl140_61])],[avatar_definition]) ).
fof(f1220,plain,
( e4 = op(e3,e3)
| ~ spl140_61 ),
inference(avatar_component_clause,[],[f1219]) ).
fof(f1233,definition,
( spl140_64
<=> e4 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl140_64])],[avatar_definition]) ).
fof(f1234,plain,
( e4 = op(e3,e2)
| ~ spl140_64 ),
inference(avatar_component_clause,[],[f1233]) ).
fof(f1238,definition,
( spl140_65
<=> e2 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl140_65])],[avatar_definition]) ).
fof(f1247,definition,
( spl140_67
<=> e4 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl140_67])],[avatar_definition]) ).
fof(f1248,plain,
( e4 = op(e3,e1)
| ~ spl140_67 ),
inference(avatar_component_clause,[],[f1247]) ).
fof(f1252,definition,
( spl140_68
<=> e1 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl140_68])],[avatar_definition]) ).
fof(f1254,plain,
( e1 = op(e3,e4)
| ~ spl140_68 ),
inference(avatar_component_clause,[],[f1252]) ).
fof(f1261,definition,
( spl140_70
<=> e4 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl140_70])],[avatar_definition]) ).
fof(f1275,definition,
( spl140_73
<=> e4 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl140_73])],[avatar_definition]) ).
fof(f1276,plain,
( e4 = op(e2,e4)
| ~ spl140_73 ),
inference(avatar_component_clause,[],[f1275]) ).
fof(f1284,definition,
( spl140_75
<=> e4 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl140_75])],[avatar_definition]) ).
fof(f1289,definition,
( spl140_76
<=> e3 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl140_76])],[avatar_definition]) ).
fof(f1291,plain,
( e3 = op(e2,e4)
| ~ spl140_76 ),
inference(avatar_component_clause,[],[f1289]) ).
fof(f1294,definition,
( spl140_77
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl140_77])],[avatar_definition]) ).
fof(f1298,definition,
( spl140_78
<=> e4 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl140_78])],[avatar_definition]) ).
fof(f1299,plain,
( e4 = op(e2,e2)
| ~ spl140_78 ),
inference(avatar_component_clause,[],[f1298]) ).
fof(f1303,definition,
( spl140_79
<=> e2 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl140_79])],[avatar_definition]) ).
fof(f1306,plain,
( ~ spl140_77
| spl140_79
| ~ spl140_78 ),
inference(avatar_split_clause,[],[f861,f1298,f1303,f1294]) ).
fof(f1340,definition,
( spl140_87
<=> e4 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl140_87])],[avatar_definition]) ).
fof(f1341,plain,
( e4 = op(e1,e4)
| ~ spl140_87 ),
inference(avatar_component_clause,[],[f1340]) ).
fof(f1349,definition,
( spl140_89
<=> e4 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl140_89])],[avatar_definition]) ).
fof(f1350,plain,
( e4 = op(e1,e3)
| ~ spl140_89 ),
inference(avatar_component_clause,[],[f1349]) ).
fof(f1354,definition,
( spl140_90
<=> e3 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl140_90])],[avatar_definition]) ).
fof(f1356,plain,
( e3 = op(e1,e4)
| ~ spl140_90 ),
inference(avatar_component_clause,[],[f1354]) ).
fof(f1363,definition,
( spl140_92
<=> e4 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl140_92])],[avatar_definition]) ).
fof(f1364,plain,
( e4 = op(e1,e2)
| ~ spl140_92 ),
inference(avatar_component_clause,[],[f1363]) ).
fof(f1368,definition,
( spl140_93
<=> e2 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl140_93])],[avatar_definition]) ).
fof(f1370,plain,
( e2 = op(e1,e4)
| ~ spl140_93 ),
inference(avatar_component_clause,[],[f1368]) ).
fof(f1377,definition,
( spl140_95
<=> e4 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl140_95])],[avatar_definition]) ).
fof(f1382,definition,
( spl140_96
<=> e1 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl140_96])],[avatar_definition]) ).
fof(f1391,definition,
( spl140_98
<=> e4 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl140_98])],[avatar_definition]) ).
fof(f1396,definition,
( spl140_99
<=> e0 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl140_99])],[avatar_definition]) ).
fof(f1405,definition,
( spl140_101
<=> e4 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl140_101])],[avatar_definition]) ).
fof(f1406,plain,
( e4 = op(e0,e4)
| ~ spl140_101 ),
inference(avatar_component_clause,[],[f1405]) ).
fof(f1428,definition,
( spl140_106
<=> e4 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl140_106])],[avatar_definition]) ).
fof(f1429,plain,
( e4 = op(e0,e2)
| ~ spl140_106 ),
inference(avatar_component_clause,[],[f1428]) ).
fof(f1433,definition,
( spl140_107
<=> e2 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl140_107])],[avatar_definition]) ).
fof(f1470,definition,
( spl140_115
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl140_115])],[avatar_definition]) ).
fof(f1471,plain,
( e3 = unit
| ~ spl140_115 ),
inference(avatar_component_clause,[],[f1470]) ).
fof(f1480,definition,
( spl140_117
<=> e3 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl140_117])],[avatar_definition]) ).
fof(f1481,plain,
( e3 = op(e4,e3)
| ~ spl140_117 ),
inference(avatar_component_clause,[],[f1480]) ).
fof(f1494,definition,
( spl140_120
<=> e2 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl140_120])],[avatar_definition]) ).
fof(f1496,plain,
( e2 = op(e4,e3)
| ~ spl140_120 ),
inference(avatar_component_clause,[],[f1494]) ).
fof(f1508,definition,
( spl140_123
<=> e1 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl140_123])],[avatar_definition]) ).
fof(f1510,plain,
( e1 = op(e4,e3)
| ~ spl140_123 ),
inference(avatar_component_clause,[],[f1508]) ).
fof(f1522,definition,
( spl140_126
<=> e0 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl140_126])],[avatar_definition]) ).
fof(f1537,definition,
( spl140_129
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl140_129])],[avatar_definition]) ).
fof(f1538,plain,
( e3 = op(e3,e3)
| ~ spl140_129 ),
inference(avatar_component_clause,[],[f1537]) ).
fof(f1551,definition,
( spl140_132
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl140_132])],[avatar_definition]) ).
fof(f1556,definition,
( spl140_133
<=> sP33 ),
introduced(definition,[new_symbols(definition,[spl140_133])],[avatar_definition]) ).
fof(f1560,definition,
( spl140_134
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl140_134])],[avatar_definition]) ).
fof(f1565,definition,
( spl140_135
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl140_135])],[avatar_definition]) ).
fof(f1568,plain,
( ~ spl140_133
| spl140_135
| ~ spl140_134 ),
inference(avatar_split_clause,[],[f819,f1560,f1565,f1556]) ).
fof(f1574,definition,
( spl140_137
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl140_137])],[avatar_definition]) ).
fof(f1575,plain,
( e3 = op(e3,e0)
| ~ spl140_137 ),
inference(avatar_component_clause,[],[f1574]) ).
fof(f1579,definition,
( spl140_138
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl140_138])],[avatar_definition]) ).
fof(f1581,plain,
( e0 = op(e3,e3)
| ~ spl140_138 ),
inference(avatar_component_clause,[],[f1579]) ).
fof(f1584,definition,
( spl140_139
<=> sP35 ),
introduced(definition,[new_symbols(definition,[spl140_139])],[avatar_definition]) ).
fof(f1588,plain,
( ~ spl140_139
| spl140_75
| ~ spl140_76 ),
inference(avatar_split_clause,[],[f815,f1289,f1284,f1584]) ).
fof(f1594,definition,
( spl140_141
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl140_141])],[avatar_definition]) ).
fof(f1608,definition,
( spl140_144
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl140_144])],[avatar_definition]) ).
fof(f1617,definition,
( spl140_146
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl140_146])],[avatar_definition]) ).
fof(f1622,definition,
( spl140_147
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl140_147])],[avatar_definition]) ).
fof(f1636,definition,
( spl140_150
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl140_150])],[avatar_definition]) ).
fof(f1708,definition,
( spl140_165
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl140_165])],[avatar_definition]) ).
fof(f1759,definition,
( spl140_176
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl140_176])],[avatar_definition]) ).
fof(f1760,plain,
( e2 = unit
| ~ spl140_176 ),
inference(avatar_component_clause,[],[f1759]) ).
fof(f1789,definition,
( spl140_182
<=> e1 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl140_182])],[avatar_definition]) ).
fof(f1808,definition,
( spl140_186
<=> sP55 ),
introduced(definition,[new_symbols(definition,[spl140_186])],[avatar_definition]) ).
fof(f1812,plain,
( ~ spl140_186
| spl140_64
| ~ spl140_65 ),
inference(avatar_split_clause,[],[f775,f1238,f1233,f1808]) ).
fof(f1906,definition,
( spl140_206
<=> sP65 ),
introduced(definition,[new_symbols(definition,[spl140_206])],[avatar_definition]) ).
fof(f1910,plain,
( ~ spl140_206
| spl140_92
| ~ spl140_93 ),
inference(avatar_split_clause,[],[f755,f1368,f1363,f1906]) ).
fof(f1955,definition,
( spl140_216
<=> sP70 ),
introduced(definition,[new_symbols(definition,[spl140_216])],[avatar_definition]) ).
fof(f1959,plain,
( ~ spl140_216
| spl140_106
| ~ spl140_107 ),
inference(avatar_split_clause,[],[f745,f1433,f1428,f1955]) ).
fof(f2008,definition,
( spl140_227
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl140_227])],[avatar_definition]) ).
fof(f2009,plain,
( e1 = unit
| ~ spl140_227 ),
inference(avatar_component_clause,[],[f2008]) ).
fof(f2049,definition,
( spl140_235
<=> sP80 ),
introduced(definition,[new_symbols(definition,[spl140_235])],[avatar_definition]) ).
fof(f2052,plain,
( ~ spl140_235
| ~ spl140_227
| ~ spl140_68 ),
inference(avatar_split_clause,[],[f724,f1252,f2008,f2049]) ).
fof(f2053,plain,
( ~ spl140_235
| spl140_67
| ~ spl140_68 ),
inference(avatar_split_clause,[],[f725,f1252,f1247,f2049]) ).
fof(f2096,definition,
( spl140_244
<=> sP86 ),
introduced(definition,[new_symbols(definition,[spl140_244])],[avatar_definition]) ).
fof(f2100,plain,
( ~ spl140_244
| spl140_146
| ~ spl140_147 ),
inference(avatar_split_clause,[],[f713,f1622,f1617,f2096]) ).
fof(f2213,definition,
( spl140_267
<=> sP100 ),
introduced(definition,[new_symbols(definition,[spl140_267])],[avatar_definition]) ).
fof(f2217,definition,
( spl140_268
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl140_268])],[avatar_definition]) ).
fof(f2218,plain,
( e0 = unit
| ~ spl140_268 ),
inference(avatar_component_clause,[],[f2217]) ).
fof(f2220,plain,
( ~ spl140_267
| ~ spl140_268
| ~ spl140_57 ),
inference(avatar_split_clause,[],[f684,f1201,f2217,f2213]) ).
fof(f2221,plain,
( ~ spl140_267
| spl140_56
| ~ spl140_57 ),
inference(avatar_split_clause,[],[f685,f1201,f1196,f2213]) ).
fof(f2393,plain,
( ~ spl140_1
| spl140_77 ),
inference(avatar_split_clause,[],[f623,f1294,f928]) ).
fof(f2414,plain,
( ~ spl140_2
| spl140_133 ),
inference(avatar_split_clause,[],[f594,f1556,f932]) ).
fof(f2416,plain,
( ~ spl140_2
| spl140_139 ),
inference(avatar_split_clause,[],[f596,f1584,f932]) ).
fof(f2436,plain,
( ~ spl140_3
| spl140_186 ),
inference(avatar_split_clause,[],[f566,f1808,f936]) ).
fof(f2446,plain,
( ~ spl140_3
| spl140_206 ),
inference(avatar_split_clause,[],[f576,f1906,f936]) ).
fof(f2451,plain,
( ~ spl140_3
| spl140_216 ),
inference(avatar_split_clause,[],[f581,f1955,f936]) ).
fof(f2461,plain,
( ~ spl140_4
| spl140_235 ),
inference(avatar_split_clause,[],[f541,f2049,f940]) ).
fof(f2467,plain,
( ~ spl140_4
| spl140_244 ),
inference(avatar_split_clause,[],[f547,f2096,f940]) ).
fof(f2481,plain,
( ~ spl140_5
| spl140_267 ),
inference(avatar_split_clause,[],[f511,f2213,f944]) ).
fof(f2507,definition,
( spl140_298
<=> e4 = op(e4,op(e4,e4)) ),
introduced(definition,[new_symbols(definition,[spl140_298])],[avatar_definition]) ).
fof(f2510,plain,
( ~ spl140_6
| spl140_298 ),
inference(avatar_split_clause,[],[f509,f2507,f949]) ).
fof(f2511,plain,
( ~ spl140_6
| ~ spl140_298 ),
inference(avatar_split_clause,[],[f510,f2507,f949]) ).
fof(f2518,definition,
( spl140_300
<=> e4 = op(e3,op(e3,e4)) ),
introduced(definition,[new_symbols(definition,[spl140_300])],[avatar_definition]) ).
fof(f2520,plain,
( e4 != op(e3,op(e3,e4))
| spl140_300 ),
inference(avatar_component_clause,[],[f2518]) ).
fof(f2521,plain,
( ~ spl140_7
| ~ spl140_300 ),
inference(avatar_split_clause,[],[f508,f2518,f953]) ).
fof(f2598,plain,
spl140_78,
inference(avatar_split_clause,[],[f487,f1298]) ).
fof(f2603,plain,
( spl140_51
| spl140_65
| spl140_79
| spl140_93
| spl140_107 ),
inference(avatar_split_clause,[],[f331,f1433,f1368,f1303,f1238,f1173]) ).
fof(f2610,plain,
( spl140_59
| spl140_61
| spl140_64
| spl140_67
| spl140_70 ),
inference(avatar_split_clause,[],[f338,f1261,f1247,f1233,f1219,f1210]) ).
fof(f2630,plain,
( spl140_87
| spl140_89
| spl140_92
| spl140_95
| spl140_98 ),
inference(avatar_split_clause,[],[f358,f1391,f1377,f1363,f1349,f1340]) ).
fof(f2649,plain,
( spl140_44
| spl140_115
| spl140_176
| spl140_227
| spl140_268 ),
inference(avatar_split_clause,[],[f316,f2217,f2008,f1759,f1470,f1141]) ).
fof(f2651,plain,
( spl140_47
| spl140_117
| spl140_120
| spl140_123
| spl140_126 ),
inference(avatar_split_clause,[],[f292,f1522,f1508,f1494,f1480,f1154]) ).
fof(f2656,plain,
( spl140_61
| spl140_129
| spl140_132
| spl140_135
| spl140_138 ),
inference(avatar_split_clause,[],[f297,f1579,f1565,f1551,f1537,f1219]) ).
fof(f2661,plain,
( spl140_75
| spl140_141
| spl140_144
| spl140_147
| spl140_150 ),
inference(avatar_split_clause,[],[f302,f1636,f1622,f1608,f1594,f1284]) ).
fof(f2665,plain,
( spl140_87
| spl140_90
| spl140_93
| spl140_96
| spl140_99 ),
inference(avatar_split_clause,[],[f306,f1396,f1382,f1368,f1354,f1340]) ).
fof(f2679,plain,
( e2 = op(e2,e4)
| ~ spl140_44 ),
inference(superposition,[],[f321,f1142]) ).
fof(f2690,plain,
( spl140_79
| ~ spl140_44 ),
inference(avatar_split_clause,[],[f2679,f1141,f1303]) ).
fof(f2716,plain,
( e4 != op(e3,e1)
| ~ spl140_61 ),
inference(superposition,[],[f391,f1220]) ).
fof(f2719,plain,
( ~ spl140_67
| ~ spl140_61 ),
inference(avatar_split_clause,[],[f2716,f1219,f1247]) ).
fof(f2722,plain,
( e4 = op(e2,e4)
| ~ spl140_176 ),
inference(superposition,[],[f318,f1760]) ).
fof(f2740,plain,
( spl140_73
| ~ spl140_176 ),
inference(avatar_split_clause,[],[f2722,f1759,f1275]) ).
fof(f2760,plain,
( e4 != op(e2,e3)
| ~ spl140_61 ),
inference(superposition,[],[f439,f1220]) ).
fof(f2765,plain,
( ~ spl140_75
| ~ spl140_61 ),
inference(avatar_split_clause,[],[f2760,f1219,f1284]) ).
fof(f2804,plain,
( e1 != op(e3,e3)
| ~ spl140_68 ),
inference(superposition,[],[f387,f1254]) ).
fof(f2809,plain,
( e1 != op(e1,e4)
| ~ spl140_68 ),
inference(superposition,[],[f431,f1254]) ).
fof(f2816,plain,
( ~ spl140_96
| ~ spl140_68 ),
inference(avatar_split_clause,[],[f2809,f1252,f1382]) ).
fof(f2850,plain,
( e2 = e3
| ~ spl140_24 ),
inference(forward_demodulation,[],[f488,f1039]) ).
fof(f2851,plain,
( $false
| ~ spl140_24 ),
inference(forward_subsumption_resolution,[],[f2850,f479]) ).
fof(f2852,plain,
~ spl140_24,
inference(avatar_contradiction_clause,[],[f2851]) ).
fof(f2854,plain,
( e4 = op(e4,e1)
| ~ spl140_227 ),
inference(superposition,[],[f317,f2009]) ).
fof(f2856,plain,
( e3 = op(e3,e1)
| ~ spl140_227 ),
inference(superposition,[],[f319,f2009]) ).
fof(f2873,plain,
( spl140_134
| ~ spl140_227 ),
inference(avatar_split_clause,[],[f2856,f2008,f1560]) ).
fof(f2875,plain,
( $false
| spl140_53
| ~ spl140_227 ),
inference(forward_subsumption_resolution,[],[f2854,f1184]) ).
fof(f2876,plain,
( spl140_53
| ~ spl140_227 ),
inference(avatar_contradiction_clause,[],[f2875]) ).
fof(f2877,plain,
e1 = op(e3,op(e2,e2)),
inference(forward_demodulation,[],[f489,f488]) ).
fof(f2879,plain,
( e4 = op(e0,e4)
| ~ spl140_268 ),
inference(superposition,[],[f318,f2218]) ).
fof(f2880,plain,
( e3 = op(e3,e0)
| ~ spl140_268 ),
inference(superposition,[],[f319,f2218]) ).
fof(f2881,plain,
( e3 = op(e0,e3)
| ~ spl140_268 ),
inference(superposition,[],[f320,f2218]) ).
fof(f2897,plain,
( spl140_165
| ~ spl140_268 ),
inference(avatar_split_clause,[],[f2881,f2217,f1708]) ).
fof(f2898,plain,
( spl140_137
| ~ spl140_268 ),
inference(avatar_split_clause,[],[f2880,f2217,f1574]) ).
fof(f2899,plain,
( spl140_101
| ~ spl140_268 ),
inference(avatar_split_clause,[],[f2879,f2217,f1405]) ).
fof(f2940,plain,
( e4 != op(e4,e0)
| ~ spl140_53 ),
inference(superposition,[],[f386,f1183]) ).
fof(f2993,plain,
( e4 != op(e2,e2)
| ~ spl140_73 ),
inference(superposition,[],[f398,f1276]) ).
fof(f3002,plain,
( ~ spl140_78
| ~ spl140_73 ),
inference(avatar_split_clause,[],[f2993,f1275,f1298]) ).
fof(f3004,plain,
( e1 = op(e3,e4)
| ~ spl140_78 ),
inference(superposition,[],[f2877,f1299]) ).
fof(f3005,plain,
( e0 = op(e4,e4)
| ~ spl140_78 ),
inference(superposition,[],[f490,f1299]) ).
fof(f3006,plain,
( e3 = op(e2,e4)
| ~ spl140_78 ),
inference(superposition,[],[f488,f1299]) ).
fof(f3007,plain,
( e2 != op(e2,e4)
| spl140_24
| ~ spl140_78 ),
inference(superposition,[],[f1038,f1299]) ).
fof(f3008,plain,
( ~ spl140_79
| spl140_24
| ~ spl140_78 ),
inference(avatar_split_clause,[],[f3007,f1298,f1037,f1303]) ).
fof(f3011,plain,
( e0 = e2
| ~ spl140_51
| ~ spl140_78 ),
inference(forward_demodulation,[],[f3005,f1175]) ).
fof(f3013,plain,
( $false
| ~ spl140_51
| ~ spl140_78 ),
inference(forward_subsumption_resolution,[],[f3011,f485]) ).
fof(f3014,plain,
( ~ spl140_51
| ~ spl140_78 ),
inference(avatar_contradiction_clause,[],[f3013]) ).
fof(f3020,plain,
( spl140_76
| ~ spl140_78 ),
inference(avatar_split_clause,[],[f3006,f1298,f1289]) ).
fof(f3021,plain,
( spl140_68
| ~ spl140_78 ),
inference(avatar_split_clause,[],[f3004,f1298,f1252]) ).
fof(f3022,plain,
( ~ spl140_56
| ~ spl140_53 ),
inference(avatar_split_clause,[],[f2940,f1182,f1196]) ).
fof(f3023,plain,
( spl140_57
| ~ spl140_78 ),
inference(avatar_split_clause,[],[f3005,f1298,f1201]) ).
fof(f3024,plain,
( ~ spl140_135
| ~ spl140_68 ),
inference(avatar_split_clause,[],[f2804,f1252,f1565]) ).
fof(f3027,plain,
( e0 != op(e4,e3)
| ~ spl140_57 ),
inference(superposition,[],[f377,f1203]) ).
fof(f3033,plain,
( e0 != op(e1,e4)
| ~ spl140_57 ),
inference(superposition,[],[f430,f1203]) ).
fof(f3040,plain,
( ~ spl140_99
| ~ spl140_57 ),
inference(avatar_split_clause,[],[f3033,f1201,f1396]) ).
fof(f3046,plain,
( ~ spl140_126
| ~ spl140_57 ),
inference(avatar_split_clause,[],[f3027,f1201,f1522]) ).
fof(f3059,plain,
( e3 != op(e2,e3)
| ~ spl140_76 ),
inference(superposition,[],[f397,f1291]) ).
fof(f3061,plain,
( e3 != op(e2,e1)
| ~ spl140_76 ),
inference(superposition,[],[f400,f1291]) ).
fof(f3063,plain,
( e2 = op(e4,e3)
| ~ spl140_8
| ~ spl140_76 ),
inference(superposition,[],[f959,f1291]) ).
fof(f3066,plain,
( spl140_120
| ~ spl140_8
| ~ spl140_76 ),
inference(avatar_split_clause,[],[f3063,f1289,f957,f1494]) ).
fof(f3068,plain,
( ~ spl140_146
| ~ spl140_76 ),
inference(avatar_split_clause,[],[f3061,f1289,f1617]) ).
fof(f3070,plain,
( ~ spl140_141
| ~ spl140_76 ),
inference(avatar_split_clause,[],[f3059,f1289,f1594]) ).
fof(f3071,plain,
( e2 != op(e4,e3)
| spl140_8
| ~ spl140_76 ),
inference(forward_demodulation,[],[f958,f1291]) ).
fof(f3072,plain,
( ~ spl140_120
| spl140_8
| ~ spl140_76 ),
inference(avatar_split_clause,[],[f3071,f1289,f957,f1494]) ).
fof(f3081,plain,
( e4 != op(e0,e4)
| ~ spl140_87 ),
inference(superposition,[],[f436,f1341]) ).
fof(f3088,plain,
( ~ spl140_101
| ~ spl140_87 ),
inference(avatar_split_clause,[],[f3081,f1340,f1405]) ).
fof(f3116,plain,
( e4 != op(e2,e2)
| ~ spl140_64 ),
inference(superposition,[],[f449,f1234]) ).
fof(f3117,plain,
( $false
| ~ spl140_64
| ~ spl140_78 ),
inference(forward_subsumption_resolution,[],[f3116,f1299]) ).
fof(f3118,plain,
( ~ spl140_64
| ~ spl140_78 ),
inference(avatar_contradiction_clause,[],[f3117]) ).
fof(f3123,plain,
( e4 = op(e4,e0)
| ~ spl140_268 ),
inference(superposition,[],[f317,f2218]) ).
fof(f3137,plain,
( spl140_56
| ~ spl140_268 ),
inference(avatar_split_clause,[],[f3123,f2217,f1196]) ).
fof(f3139,plain,
( e4 != op(e1,e0)
| ~ spl140_56 ),
inference(superposition,[],[f470,f1197]) ).
fof(f3141,plain,
( e4 != op(e3,e0)
| ~ spl140_56 ),
inference(superposition,[],[f467,f1197]) ).
fof(f3143,plain,
( ~ spl140_70
| ~ spl140_56 ),
inference(avatar_split_clause,[],[f3141,f1196,f1261]) ).
fof(f3147,plain,
( e4 != op(e1,e1)
| ~ spl140_67 ),
inference(superposition,[],[f461,f1248]) ).
fof(f3154,plain,
( e4 != op(e2,e2)
| ~ spl140_92 ),
inference(superposition,[],[f452,f1364]) ).
fof(f3159,plain,
( $false
| ~ spl140_78
| ~ spl140_92 ),
inference(forward_subsumption_resolution,[],[f3154,f1299]) ).
fof(f3160,plain,
( ~ spl140_78
| ~ spl140_92 ),
inference(avatar_contradiction_clause,[],[f3159]) ).
fof(f3162,plain,
( ~ spl140_98
| ~ spl140_56 ),
inference(avatar_split_clause,[],[f3139,f1196,f1391]) ).
fof(f3163,plain,
( ~ spl140_95
| ~ spl140_67 ),
inference(avatar_split_clause,[],[f3147,f1247,f1377]) ).
fof(f3164,plain,
( e1 = e4
| ~ spl140_59
| ~ spl140_68 ),
inference(forward_demodulation,[],[f1211,f1254]) ).
fof(f3165,plain,
( $false
| ~ spl140_59
| ~ spl140_68 ),
inference(forward_subsumption_resolution,[],[f3164,f480]) ).
fof(f3166,plain,
( ~ spl140_59
| ~ spl140_68 ),
inference(avatar_contradiction_clause,[],[f3165]) ).
fof(f3170,plain,
( e4 != op(e4,e0)
| ~ spl140_47 ),
inference(superposition,[],[f384,f1155]) ).
fof(f3177,plain,
( $false
| ~ spl140_47
| ~ spl140_56 ),
inference(forward_subsumption_resolution,[],[f3170,f1197]) ).
fof(f3178,plain,
( ~ spl140_47
| ~ spl140_56 ),
inference(avatar_contradiction_clause,[],[f3177]) ).
fof(f3189,plain,
( e3 != op(e2,e4)
| ~ spl140_90 ),
inference(superposition,[],[f432,f1356]) ).
fof(f3198,plain,
( $false
| ~ spl140_76
| ~ spl140_90 ),
inference(forward_subsumption_resolution,[],[f3189,f1291]) ).
fof(f3199,plain,
( ~ spl140_76
| ~ spl140_90 ),
inference(avatar_contradiction_clause,[],[f3198]) ).
fof(f3206,plain,
( e4 = op(e3,e4)
| ~ spl140_115 ),
inference(superposition,[],[f318,f1471]) ).
fof(f3225,plain,
( e1 = e4
| ~ spl140_68
| ~ spl140_115 ),
inference(forward_demodulation,[],[f3206,f1254]) ).
fof(f3228,plain,
( $false
| ~ spl140_68
| ~ spl140_115 ),
inference(forward_subsumption_resolution,[],[f3225,f480]) ).
fof(f3229,plain,
( ~ spl140_68
| ~ spl140_115 ),
inference(avatar_contradiction_clause,[],[f3228]) ).
fof(f3262,plain,
( e4 != op(e2,e2)
| ~ spl140_106 ),
inference(superposition,[],[f455,f1429]) ).
fof(f3263,plain,
( $false
| ~ spl140_78
| ~ spl140_106 ),
inference(forward_subsumption_resolution,[],[f3262,f1299]) ).
fof(f3264,plain,
( ~ spl140_78
| ~ spl140_106 ),
inference(avatar_contradiction_clause,[],[f3263]) ).
fof(f3292,plain,
( e4 != op(e2,e3)
| ~ spl140_89 ),
inference(superposition,[],[f442,f1350]) ).
fof(f3315,plain,
( e1 = op(e4,e2)
| ~ spl140_9
| ~ spl140_93 ),
inference(forward_demodulation,[],[f963,f1370]) ).
fof(f3317,plain,
( spl140_182
| ~ spl140_9
| ~ spl140_93 ),
inference(avatar_split_clause,[],[f3315,f1368,f961,f1789]) ).
fof(f3326,plain,
( e4 != op(e0,e4)
| spl140_13
| ~ spl140_101 ),
inference(superposition,[],[f983,f1406]) ).
fof(f3328,plain,
( $false
| spl140_13
| ~ spl140_101 ),
inference(forward_subsumption_resolution,[],[f3326,f1406]) ).
fof(f3329,plain,
( spl140_13
| ~ spl140_101 ),
inference(avatar_contradiction_clause,[],[f3328]) ).
fof(f3343,plain,
( e3 != op(e0,e3)
| ~ spl140_117 ),
inference(superposition,[],[f443,f1481]) ).
fof(f3345,plain,
( ~ spl140_165
| ~ spl140_117 ),
inference(avatar_split_clause,[],[f3343,f1480,f1708]) ).
fof(f3364,plain,
( e1 != op(e4,e2)
| ~ spl140_123 ),
inference(superposition,[],[f379,f1510]) ).
fof(f3380,plain,
( ~ spl140_182
| ~ spl140_123 ),
inference(avatar_split_clause,[],[f3364,f1508,f1789]) ).
fof(f3383,plain,
( e4 != op(e3,e1)
| ~ spl140_68
| spl140_300 ),
inference(forward_demodulation,[],[f2520,f1254]) ).
fof(f3385,plain,
( $false
| ~ spl140_67
| ~ spl140_68
| spl140_300 ),
inference(forward_subsumption_resolution,[],[f3383,f1248]) ).
fof(f3386,plain,
( ~ spl140_67
| ~ spl140_68
| spl140_300 ),
inference(avatar_contradiction_clause,[],[f3385]) ).
fof(f3393,plain,
( e2 != op(e3,e3)
| ~ spl140_120 ),
inference(superposition,[],[f437,f1496]) ).
fof(f3394,plain,
( e2 != op(e2,e3)
| ~ spl140_120 ),
inference(superposition,[],[f438,f1496]) ).
fof(f3404,plain,
( ~ spl140_144
| ~ spl140_120 ),
inference(avatar_split_clause,[],[f3394,f1494,f1608]) ).
fof(f3405,plain,
( ~ spl140_132
| ~ spl140_120 ),
inference(avatar_split_clause,[],[f3393,f1494,f1551]) ).
fof(f3473,plain,
( e0 != op(e2,e3)
| ~ spl140_138 ),
inference(superposition,[],[f439,f1581]) ).
fof(f3482,plain,
( ~ spl140_150
| ~ spl140_138 ),
inference(avatar_split_clause,[],[f3473,f1579,f1636]) ).
fof(f3488,plain,
( e3 != op(e3,e0)
| ~ spl140_129 ),
inference(superposition,[],[f394,f1538]) ).
fof(f3498,plain,
( $false
| ~ spl140_129
| ~ spl140_137 ),
inference(forward_subsumption_resolution,[],[f3488,f1575]) ).
fof(f3499,plain,
( ~ spl140_129
| ~ spl140_137 ),
inference(avatar_contradiction_clause,[],[f3498]) ).
fof(f3505,plain,
( ~ spl140_75
| ~ spl140_89 ),
inference(avatar_split_clause,[],[f3292,f1349,f1284]) ).
cnf(s1,plain,
( spl140_1
| spl140_2
| spl140_3
| spl140_4
| spl140_5 ),
inference(sat_conversion,[],[f947]) ).
cnf(s6,plain,
( spl140_6
| spl140_7
| spl140_8
| spl140_9
| ~ spl140_13 ),
inference(sat_conversion,[],[f984]) ).
cnf(s64,plain,
( ~ spl140_77
| ~ spl140_78
| spl140_79 ),
inference(sat_conversion,[],[f1306]) ).
cnf(s102,plain,
( ~ spl140_133
| ~ spl140_134
| spl140_135 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s106,plain,
( spl140_75
| ~ spl140_76
| ~ spl140_139 ),
inference(sat_conversion,[],[f1588]) ).
cnf(s142,plain,
( spl140_64
| ~ spl140_65
| ~ spl140_186 ),
inference(sat_conversion,[],[f1812]) ).
cnf(s160,plain,
( spl140_92
| ~ spl140_93
| ~ spl140_206 ),
inference(sat_conversion,[],[f1910]) ).
cnf(s169,plain,
( spl140_106
| ~ spl140_107
| ~ spl140_216 ),
inference(sat_conversion,[],[f1959]) ).
cnf(s186,plain,
( ~ spl140_68
| ~ spl140_227
| ~ spl140_235 ),
inference(sat_conversion,[],[f2052]) ).
cnf(s187,plain,
( spl140_67
| ~ spl140_68
| ~ spl140_235 ),
inference(sat_conversion,[],[f2053]) ).
cnf(s198,plain,
( spl140_146
| ~ spl140_147
| ~ spl140_244 ),
inference(sat_conversion,[],[f2100]) ).
cnf(s222,plain,
( ~ spl140_57
| ~ spl140_267
| ~ spl140_268 ),
inference(sat_conversion,[],[f2220]) ).
cnf(s223,plain,
( spl140_56
| ~ spl140_57
| ~ spl140_267 ),
inference(sat_conversion,[],[f2221]) ).
cnf(s279,plain,
( ~ spl140_1
| spl140_77 ),
inference(sat_conversion,[],[f2393]) ).
cnf(s300,plain,
( ~ spl140_2
| spl140_133 ),
inference(sat_conversion,[],[f2414]) ).
cnf(s302,plain,
( ~ spl140_2
| spl140_139 ),
inference(sat_conversion,[],[f2416]) ).
cnf(s322,plain,
( ~ spl140_3
| spl140_186 ),
inference(sat_conversion,[],[f2436]) ).
cnf(s332,plain,
( ~ spl140_3
| spl140_206 ),
inference(sat_conversion,[],[f2446]) ).
cnf(s337,plain,
( ~ spl140_3
| spl140_216 ),
inference(sat_conversion,[],[f2451]) ).
cnf(s347,plain,
( ~ spl140_4
| spl140_235 ),
inference(sat_conversion,[],[f2461]) ).
cnf(s353,plain,
( ~ spl140_4
| spl140_244 ),
inference(sat_conversion,[],[f2467]) ).
cnf(s367,plain,
( ~ spl140_5
| spl140_267 ),
inference(sat_conversion,[],[f2481]) ).
cnf(s392,plain,
( ~ spl140_6
| spl140_298 ),
inference(sat_conversion,[],[f2510]) ).
cnf(s393,plain,
( ~ spl140_6
| ~ spl140_298 ),
inference(sat_conversion,[],[f2511]) ).
cnf(s395,plain,
( ~ spl140_7
| ~ spl140_300 ),
inference(sat_conversion,[],[f2521]) ).
cnf(s412,plain,
spl140_78,
inference(sat_conversion,[],[f2598]) ).
cnf(s417,plain,
( spl140_51
| spl140_65
| spl140_79
| spl140_93
| spl140_107 ),
inference(sat_conversion,[],[f2603]) ).
cnf(s424,plain,
( spl140_59
| spl140_61
| spl140_64
| spl140_67
| spl140_70 ),
inference(sat_conversion,[],[f2610]) ).
cnf(s444,plain,
( spl140_87
| spl140_89
| spl140_92
| spl140_95
| spl140_98 ),
inference(sat_conversion,[],[f2630]) ).
cnf(s463,plain,
( spl140_44
| spl140_115
| spl140_176
| spl140_227
| spl140_268 ),
inference(sat_conversion,[],[f2649]) ).
cnf(s465,plain,
( spl140_47
| spl140_117
| spl140_120
| spl140_123
| spl140_126 ),
inference(sat_conversion,[],[f2651]) ).
cnf(s470,plain,
( spl140_61
| spl140_129
| spl140_132
| spl140_135
| spl140_138 ),
inference(sat_conversion,[],[f2656]) ).
cnf(s475,plain,
( spl140_75
| spl140_141
| spl140_144
| spl140_147
| spl140_150 ),
inference(sat_conversion,[],[f2661]) ).
cnf(s479,plain,
( spl140_87
| spl140_90
| spl140_93
| spl140_96
| spl140_99 ),
inference(sat_conversion,[],[f2665]) ).
cnf(s494,plain,
( ~ spl140_44
| spl140_79 ),
inference(sat_conversion,[],[f2690]) ).
cnf(s508,plain,
( ~ spl140_61
| ~ spl140_67 ),
inference(sat_conversion,[],[f2719]) ).
cnf(s518,plain,
( spl140_73
| ~ spl140_176 ),
inference(sat_conversion,[],[f2740]) ).
cnf(s533,plain,
( ~ spl140_61
| ~ spl140_75 ),
inference(sat_conversion,[],[f2765]) ).
cnf(s553,plain,
( ~ spl140_68
| ~ spl140_96 ),
inference(sat_conversion,[],[f2816]) ).
cnf(s568,plain,
~ spl140_24,
inference(sat_conversion,[],[f2852]) ).
cnf(s576,plain,
( spl140_134
| ~ spl140_227 ),
inference(sat_conversion,[],[f2873]) ).
cnf(s578,plain,
( spl140_53
| ~ spl140_227 ),
inference(sat_conversion,[],[f2876]) ).
cnf(s585,plain,
( spl140_165
| ~ spl140_268 ),
inference(sat_conversion,[],[f2897]) ).
cnf(s586,plain,
( spl140_137
| ~ spl140_268 ),
inference(sat_conversion,[],[f2898]) ).
cnf(s587,plain,
( spl140_101
| ~ spl140_268 ),
inference(sat_conversion,[],[f2899]) ).
cnf(s633,plain,
( ~ spl140_73
| ~ spl140_78 ),
inference(sat_conversion,[],[f3002]) ).
cnf(s635,plain,
( spl140_24
| ~ spl140_78
| ~ spl140_79 ),
inference(sat_conversion,[],[f3008]) ).
cnf(s637,plain,
( ~ spl140_51
| ~ spl140_78 ),
inference(sat_conversion,[],[f3014]) ).
cnf(s645,plain,
( spl140_76
| ~ spl140_78 ),
inference(sat_conversion,[],[f3020]) ).
cnf(s646,plain,
( spl140_68
| ~ spl140_78 ),
inference(sat_conversion,[],[f3021]) ).
cnf(s647,plain,
( ~ spl140_53
| ~ spl140_56 ),
inference(sat_conversion,[],[f3022]) ).
cnf(s648,plain,
( spl140_57
| ~ spl140_78 ),
inference(sat_conversion,[],[f3023]) ).
cnf(s649,plain,
( ~ spl140_68
| ~ spl140_135 ),
inference(sat_conversion,[],[f3024]) ).
cnf(s656,plain,
( ~ spl140_57
| ~ spl140_99 ),
inference(sat_conversion,[],[f3040]) ).
cnf(s661,plain,
( ~ spl140_57
| ~ spl140_126 ),
inference(sat_conversion,[],[f3046]) ).
cnf(s668,plain,
( ~ spl140_8
| ~ spl140_76
| spl140_120 ),
inference(sat_conversion,[],[f3066]) ).
cnf(s670,plain,
( ~ spl140_76
| ~ spl140_146 ),
inference(sat_conversion,[],[f3068]) ).
cnf(s671,plain,
( ~ spl140_76
| ~ spl140_141 ),
inference(sat_conversion,[],[f3070]) ).
cnf(s672,plain,
( spl140_8
| ~ spl140_76
| ~ spl140_120 ),
inference(sat_conversion,[],[f3072]) ).
cnf(s675,plain,
( ~ spl140_87
| ~ spl140_101 ),
inference(sat_conversion,[],[f3088]) ).
cnf(s693,plain,
( ~ spl140_64
| ~ spl140_78 ),
inference(sat_conversion,[],[f3118]) ).
cnf(s705,plain,
( spl140_56
| ~ spl140_268 ),
inference(sat_conversion,[],[f3137]) ).
cnf(s706,plain,
( ~ spl140_56
| ~ spl140_70 ),
inference(sat_conversion,[],[f3143]) ).
cnf(s713,plain,
( ~ spl140_78
| ~ spl140_92 ),
inference(sat_conversion,[],[f3160]) ).
cnf(s715,plain,
( ~ spl140_56
| ~ spl140_98 ),
inference(sat_conversion,[],[f3162]) ).
cnf(s716,plain,
( ~ spl140_67
| ~ spl140_95 ),
inference(sat_conversion,[],[f3163]) ).
cnf(s717,plain,
( ~ spl140_59
| ~ spl140_68 ),
inference(sat_conversion,[],[f3166]) ).
cnf(s723,plain,
( ~ spl140_47
| ~ spl140_56 ),
inference(sat_conversion,[],[f3178]) ).
cnf(s729,plain,
( ~ spl140_76
| ~ spl140_90 ),
inference(sat_conversion,[],[f3199]) ).
cnf(s747,plain,
( ~ spl140_68
| ~ spl140_115 ),
inference(sat_conversion,[],[f3229]) ).
cnf(s770,plain,
( ~ spl140_78
| ~ spl140_106 ),
inference(sat_conversion,[],[f3264]) ).
cnf(s792,plain,
( ~ spl140_9
| ~ spl140_93
| spl140_182 ),
inference(sat_conversion,[],[f3317]) ).
cnf(s793,plain,
( spl140_13
| ~ spl140_101 ),
inference(sat_conversion,[],[f3329]) ).
cnf(s797,plain,
( ~ spl140_117
| ~ spl140_165 ),
inference(sat_conversion,[],[f3345]) ).
cnf(s808,plain,
( ~ spl140_123
| ~ spl140_182 ),
inference(sat_conversion,[],[f3380]) ).
cnf(s812,plain,
( ~ spl140_67
| ~ spl140_68
| spl140_300 ),
inference(sat_conversion,[],[f3386]) ).
cnf(s817,plain,
( ~ spl140_120
| ~ spl140_144 ),
inference(sat_conversion,[],[f3404]) ).
cnf(s818,plain,
( ~ spl140_120
| ~ spl140_132 ),
inference(sat_conversion,[],[f3405]) ).
cnf(s849,plain,
( ~ spl140_138
| ~ spl140_150 ),
inference(sat_conversion,[],[f3482]) ).
cnf(s853,plain,
( ~ spl140_129
| ~ spl140_137 ),
inference(sat_conversion,[],[f3499]) ).
cnf(s858,plain,
( ~ spl140_75
| ~ spl140_89 ),
inference(sat_conversion,[],[f3505]) ).
cnf(s859,plain,
~ spl140_106,
inference(rat,[],[s770,s412]) ).
cnf(s860,plain,
~ spl140_92,
inference(rat,[],[s713,s412]) ).
cnf(s861,plain,
~ spl140_64,
inference(rat,[],[s693,s412]) ).
cnf(s862,plain,
spl140_57,
inference(rat,[],[s648,s412]) ).
cnf(s863,plain,
spl140_68,
inference(rat,[],[s646,s412]) ).
cnf(s864,plain,
spl140_76,
inference(rat,[],[s645,s412]) ).
cnf(s866,plain,
~ spl140_51,
inference(rat,[],[s637,s412]) ).
cnf(s867,plain,
~ spl140_79,
inference(rat,[],[s635,s568,s412]) ).
cnf(s868,plain,
~ spl140_73,
inference(rat,[],[s633,s412]) ).
cnf(s871,plain,
~ spl140_126,
inference(rat,[],[s661,s862]) ).
cnf(s875,plain,
~ spl140_99,
inference(rat,[],[s656,s862]) ).
cnf(s877,plain,
~ spl140_115,
inference(rat,[],[s747,s863]) ).
cnf(s878,plain,
~ spl140_59,
inference(rat,[],[s717,s863]) ).
cnf(s879,plain,
~ spl140_135,
inference(rat,[],[s649,s863]) ).
cnf(s885,plain,
~ spl140_96,
inference(rat,[],[s553,s863]) ).
cnf(s887,plain,
~ spl140_90,
inference(rat,[],[s729,s864]) ).
cnf(s888,plain,
~ spl140_141,
inference(rat,[],[s671,s864]) ).
cnf(s889,plain,
~ spl140_146,
inference(rat,[],[s670,s864]) ).
cnf(s891,plain,
~ spl140_44,
inference(rat,[],[s494,s867]) ).
cnf(s892,plain,
~ spl140_176,
inference(rat,[],[s518,s868]) ).
cnf(s895,plain,
( spl140_56
| ~ spl140_267 ),
inference(rat,[],[s223,s862]) ).
cnf(s896,plain,
( ~ spl140_267
| ~ spl140_268 ),
inference(rat,[],[s222,s862]) ).
cnf(s897,plain,
( ~ spl140_147
| ~ spl140_244 ),
inference(rat,[],[s198,s889]) ).
cnf(s898,plain,
( spl140_67
| ~ spl140_235 ),
inference(rat,[],[s187,s863]) ).
cnf(s899,plain,
( ~ spl140_227
| ~ spl140_235 ),
inference(rat,[],[s186,s863]) ).
cnf(s901,plain,
( ~ spl140_107
| ~ spl140_216 ),
inference(rat,[],[s169,s859]) ).
cnf(s902,plain,
( ~ spl140_93
| ~ spl140_206 ),
inference(rat,[],[s160,s860]) ).
cnf(s904,plain,
( ~ spl140_65
| ~ spl140_186 ),
inference(rat,[],[s142,s861]) ).
cnf(s906,plain,
( spl140_75
| ~ spl140_139 ),
inference(rat,[],[s106,s864]) ).
cnf(s907,plain,
( ~ spl140_133
| ~ spl140_134 ),
inference(rat,[],[s102,s879]) ).
cnf(s916,plain,
~ spl140_77,
inference(rat,[],[s64,s867,s412]) ).
cnf(s917,plain,
~ spl140_1,
inference(rat,[],[s279,s916]) ).
cnf(s924,plain,
( spl140_2
| spl140_3
| spl140_4
| spl140_5 ),
inference(rat,[],[s1,s917]) ).
cnf(s925,plain,
~ spl140_267,
inference(rat,[],[s578,s463,s647,s896,s895,s892,s877,s891]) ).
cnf(s926,plain,
~ spl140_5,
inference(rat,[],[s367,s925]) ).
cnf(s927,plain,
( spl140_8
| spl140_6
| ~ spl140_235 ),
inference(rat,[],[s808,s792,s465,s6,s672,s395,s812,s898,s723,s705,s793,s797,s585,s479,s675,s587,s463,s899,s871,s864,s875,s885,s887,s891,s877,s892,s863]) ).
cnf(s928,plain,
( ~ spl140_120
| ~ spl140_4 ),
inference(rat,[],[s849,s475,s470,s817,s818,s897,s353,s508,s853,s586,s858,s444,s675,s587,s716,s898,s715,s705,s463,s899,s347,s888,s879,s891,s877,s892,s860]) ).
cnf(s929,plain,
~ spl140_6,
inference(rat,[],[s392,s393]) ).
cnf(s930,plain,
~ spl140_4,
inference(rat,[],[s668,s927,s928,s347,s864,s929]) ).
cnf(s931,plain,
~ spl140_3,
inference(rat,[],[s417,s904,s902,s901,s322,s332,s337,s867,s866]) ).
cnf(s932,plain,
spl140_2,
inference(rat,[],[s924,s926,s930,s931]) ).
cnf(s947,plain,
spl140_139,
inference(rat,[],[s302,s932]) ).
cnf(s949,plain,
spl140_133,
inference(rat,[],[s300,s932]) ).
cnf(s958,plain,
spl140_75,
inference(rat,[],[s906,s947]) ).
cnf(s959,plain,
~ spl140_134,
inference(rat,[],[s907,s949]) ).
cnf(s961,plain,
~ spl140_89,
inference(rat,[],[s858,s958]) ).
cnf(s963,plain,
~ spl140_61,
inference(rat,[],[s533,s958]) ).
cnf(s964,plain,
~ spl140_227,
inference(rat,[],[s576,s959]) ).
cnf(s965,plain,
spl140_268,
inference(rat,[],[s463,s891,s877,s892,s964]) ).
cnf(s966,plain,
spl140_56,
inference(rat,[],[s705,s965]) ).
cnf(s967,plain,
spl140_101,
inference(rat,[],[s587,s965]) ).
cnf(s976,plain,
~ spl140_98,
inference(rat,[],[s715,s966]) ).
cnf(s979,plain,
~ spl140_70,
inference(rat,[],[s706,s966]) ).
cnf(s984,plain,
~ spl140_87,
inference(rat,[],[s675,s967]) ).
cnf(s992,plain,
spl140_67,
inference(rat,[],[s424,s963,s878,s861,s979]) ).
cnf(s994,plain,
spl140_95,
inference(rat,[],[s444,s976,s961,s860,s984]) ).
cnf(s1000,plain,
$false,
inference(rat,[],[s716,s994,s992]) ).
fof(f3506,plain,
$false,
inference(avatar_sat_refutation,[],[s1000]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG055+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n001.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 19:27:04 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 3.25/1.17 % (648651)Detected formulas, will run a generic FOF schedule.
% 3.25/1.17 % (648660)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1042993555:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.25/1.17 % (648660)Instruction limit reached!
% 3.25/1.17 % (648660)------------------------------
% 3.25/1.17 % (648660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.25/1.17 % (648660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/1.17 % (648660)CaDiCaL version: 2.1.3
% 3.25/1.17 % (648660)Termination reason: Instruction limit
% 3.25/1.17 % (648660)Termination phase: Saturation
% 3.25/1.17 % (648660)Time elapsed: 0.030 s
% 3.25/1.17 % (648660)Peak memory usage: 88 MB
% 3.25/1.17 % (648660)Instructions burned: 120 (million)
% 3.25/1.17 % (648661)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3429463569:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.25/1.17 % (648659)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1837318812:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.25/1.17 % (648658)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=4049482604:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.25/1.17 % (648657)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=6056460:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.25/1.17 % (648662)dis-21_1_sil=8000:lcm=predicate:random_seed=3339410766: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)
% 3.25/1.17 % (648656)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=3636684417:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.25/1.17 % (648662)Refutation not found, incomplete strategy
% 3.25/1.17 % (648662)------------------------------
% 3.25/1.17 % (648662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.25/1.17 % (648662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/1.17 % (648662)CaDiCaL version: 2.1.3
% 3.25/1.17 % (648662)Termination reason: Refutation not found, incomplete strategy
% 3.25/1.17 % (648662)Time elapsed: 0.021 s
% 3.25/1.17 % (648662)Peak memory usage: 90 MB
% 3.25/1.17 % (648662)Instructions burned: 39 (million)
% 3.25/1.17 % (648659)Refutation not found, incomplete strategy
% 3.25/1.17 % (648659)------------------------------
% 3.25/1.17 % (648659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.25/1.17 % (648659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/1.17 % (648659)CaDiCaL version: 2.1.3
% 3.25/1.17 % (648659)Termination reason: Refutation not found, incomplete strategy
% 3.25/1.17 % (648659)Time elapsed: 0.027 s
% 3.25/1.17 % (648659)Peak memory usage: 90 MB
% 3.25/1.17 % (648659)Instructions burned: 55 (million)
% 3.25/1.17 % (648661)First to succeed.
% 3.25/1.17 % (648661)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-648651"
% 3.25/1.17 % (648664)lrs+10_1_sil=8000:sp=occurrence:random_seed=1590989295:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.25/1.17 % (648664)Also succeeded, but the first one will report.
% 3.25/1.17 % (648662)------------------------------
% 3.25/1.17 % (648662)------------------------------
% 3.25/1.17 % (648659)------------------------------
% 3.25/1.17 % (648659)------------------------------
% 3.25/1.17 % (648661)Refutation found. Thanks to Tanya!
% 3.25/1.17 % SZS status Theorem for theBenchmark
% 3.25/1.17 % SZS output start Proof for theBenchmark
% See solution above
% 4.13/1.37 % (648661)------------------------------
% 4.13/1.37 % (648661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.13/1.37 % (648661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/1.37 % (648661)CaDiCaL version: 2.1.3
% 4.13/1.37 % (648661)Termination reason: Refutation
% 4.13/1.37 % (648661)Time elapsed: 0.055 s
% 4.13/1.37 % (648661)Peak memory usage: 91 MB
% 4.13/1.37 % (648661)Instructions burned: 104 (million)
% 4.13/1.37 % (648661)------------------------------
% 4.13/1.37 % (648661)------------------------------
% 4.13/1.37 % (648651)Success in time 0.499 s
% 4.13/1.37 % Vampire exiting
%------------------------------------------------------------------------------