%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG186+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:18:08 AM UTC 2026
% Result : Theorem 2.23s 0.74s
% Output : Refutation 2.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 208
% Syntax : Number of formulae : 890 ( 187 unt; 205 def)
% Number of atoms : 4141 (2405 equ)
% Maximal formula atoms : 425 ( 4 avg)
% Number of connectives : 5643 (2392 ~;1940 |;1181 &)
% ( 130 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 111 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 207 ( 205 usr; 206 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e0 != e4
& e1 != e2
& e1 != e3
& e1 != e4
& e2 != e3
& e2 != e4
& e3 != e4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( op(e0,e0) = e3
& op(e0,e1) = e2
& op(e0,e2) = e0
& op(e0,e3) = e1
& op(e0,e4) = e4
& op(e1,e0) = e0
& op(e1,e1) = e4
& op(e1,e2) = e1
& op(e1,e3) = e2
& op(e1,e4) = e3
& op(e2,e0) = e1
& op(e2,e1) = e3
& op(e2,e2) = e2
& op(e2,e3) = e4
& op(e2,e4) = e0
& op(e3,e0) = e4
& op(e3,e1) = e1
& op(e3,e2) = e3
& op(e3,e3) = e0
& op(e3,e4) = e2
& op(e4,e0) = e2
& op(e4,e1) = e0
& op(e4,e2) = e4
& op(e4,e3) = e3
& op(e4,e4) = e1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,conjecture,
( ( ( op(e0,e0) != e0
& op(e1,e0) != e1
& op(e2,e0) != e2
& op(e3,e0) != e3
& op(e4,e0) != e4 )
| ( op(e0,e1) != e0
& op(e1,e1) != e1
& op(e2,e1) != e2
& op(e3,e1) != e3
& op(e4,e1) != e4 )
| ( op(e0,e2) != e0
& op(e1,e2) != e1
& op(e2,e2) != e2
& op(e3,e2) != e3
& op(e4,e2) != e4 )
| ( op(e0,e3) != e0
& op(e1,e3) != e1
& op(e2,e3) != e2
& op(e3,e3) != e3
& op(e4,e3) != e4 )
| ( op(e0,e4) != e0
& op(e1,e4) != e1
& op(e2,e4) != e2
& op(e3,e4) != e3
& op(e4,e4) != e4 ) )
& ( 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 )
& ( 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 )
& op(op(e0,e0),op(e0,e0)) = e0
& op(op(e1,e0),op(e0,e1)) = e0
& op(op(e2,e0),op(e0,e2)) = e0
& op(op(e3,e0),op(e0,e3)) = e0
& op(op(e4,e0),op(e0,e4)) = e0
& op(op(e0,e1),op(e1,e0)) = e1
& op(op(e1,e1),op(e1,e1)) = e1
& op(op(e2,e1),op(e1,e2)) = e1
& op(op(e3,e1),op(e1,e3)) = e1
& op(op(e4,e1),op(e1,e4)) = e1
& op(op(e0,e2),op(e2,e0)) = e2
& op(op(e1,e2),op(e2,e1)) = e2
& op(op(e2,e2),op(e2,e2)) = e2
& op(op(e3,e2),op(e2,e3)) = e2
& op(op(e4,e2),op(e2,e4)) = e2
& op(op(e0,e3),op(e3,e0)) = e3
& op(op(e1,e3),op(e3,e1)) = e3
& op(op(e2,e3),op(e3,e2)) = e3
& op(op(e3,e3),op(e3,e3)) = e3
& op(op(e4,e3),op(e3,e4)) = e3
& op(op(e0,e4),op(e4,e0)) = e4
& op(op(e1,e4),op(e4,e1)) = e4
& op(op(e2,e4),op(e4,e2)) = e4
& op(op(e3,e4),op(e4,e3)) = e4
& op(op(e4,e4),op(e4,e4)) = e4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f4,negated_conjecture,
~ ( ( ( op(e0,e0) != e0
& op(e1,e0) != e1
& op(e2,e0) != e2
& op(e3,e0) != e3
& op(e4,e0) != e4 )
| ( op(e0,e1) != e0
& op(e1,e1) != e1
& op(e2,e1) != e2
& op(e3,e1) != e3
& op(e4,e1) != e4 )
| ( op(e0,e2) != e0
& op(e1,e2) != e1
& op(e2,e2) != e2
& op(e3,e2) != e3
& op(e4,e2) != e4 )
| ( op(e0,e3) != e0
& op(e1,e3) != e1
& op(e2,e3) != e2
& op(e3,e3) != e3
& op(e4,e3) != e4 )
| ( op(e0,e4) != e0
& op(e1,e4) != e1
& op(e2,e4) != e2
& op(e3,e4) != e3
& op(e4,e4) != e4 ) )
& ( 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 )
& ( 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 )
& op(op(e0,e0),op(e0,e0)) = e0
& op(op(e1,e0),op(e0,e1)) = e0
& op(op(e2,e0),op(e0,e2)) = e0
& op(op(e3,e0),op(e0,e3)) = e0
& op(op(e4,e0),op(e0,e4)) = e0
& op(op(e0,e1),op(e1,e0)) = e1
& op(op(e1,e1),op(e1,e1)) = e1
& op(op(e2,e1),op(e1,e2)) = e1
& op(op(e3,e1),op(e1,e3)) = e1
& op(op(e4,e1),op(e1,e4)) = e1
& op(op(e0,e2),op(e2,e0)) = e2
& op(op(e1,e2),op(e2,e1)) = e2
& op(op(e2,e2),op(e2,e2)) = e2
& op(op(e3,e2),op(e2,e3)) = e2
& op(op(e4,e2),op(e2,e4)) = e2
& op(op(e0,e3),op(e3,e0)) = e3
& op(op(e1,e3),op(e3,e1)) = e3
& op(op(e2,e3),op(e3,e2)) = e3
& op(op(e3,e3),op(e3,e3)) = e3
& op(op(e4,e3),op(e3,e4)) = e3
& op(op(e0,e4),op(e4,e0)) = e4
& op(op(e1,e4),op(e4,e1)) = e4
& op(op(e2,e4),op(e4,e2)) = e4
& op(op(e3,e4),op(e4,e3)) = e4
& op(op(e4,e4),op(e4,e4)) = e4 ),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f5,plain,
( ( ( e0 = op(e0,e0)
| e1 = op(e1,e0)
| e2 = op(e2,e0)
| e3 = op(e3,e0)
| e4 = op(e4,e0) )
& ( e0 = op(e0,e1)
| e1 = op(e1,e1)
| e2 = op(e2,e1)
| e3 = op(e3,e1)
| e4 = op(e4,e1) )
& ( e0 = op(e0,e2)
| e1 = op(e1,e2)
| e2 = op(e2,e2)
| e3 = op(e3,e2)
| e4 = op(e4,e2) )
& ( e0 = op(e0,e3)
| e1 = op(e1,e3)
| e2 = op(e2,e3)
| e3 = op(e3,e3)
| e4 = op(e4,e3) )
& ( e0 = op(e0,e4)
| e1 = op(e1,e4)
| e2 = op(e2,e4)
| e3 = op(e3,e4)
| e4 = op(e4,e4) ) )
| ( e0 != op(e0,e0)
& e1 != op(e0,e0)
& e2 != op(e0,e0)
& e3 != op(e0,e0)
& e4 != op(e0,e0) )
| ( e0 != op(e0,e1)
& e1 != op(e0,e1)
& e2 != op(e0,e1)
& e3 != op(e0,e1)
& e4 != op(e0,e1) )
| ( e0 != op(e0,e2)
& e1 != op(e0,e2)
& e2 != op(e0,e2)
& e3 != op(e0,e2)
& e4 != op(e0,e2) )
| ( e0 != op(e0,e3)
& e1 != op(e0,e3)
& e2 != op(e0,e3)
& e3 != op(e0,e3)
& e4 != op(e0,e3) )
| ( e0 != op(e0,e4)
& e1 != op(e0,e4)
& e2 != op(e0,e4)
& e3 != op(e0,e4)
& e4 != op(e0,e4) )
| ( e0 != op(e1,e0)
& e1 != op(e1,e0)
& e2 != op(e1,e0)
& e3 != op(e1,e0)
& e4 != op(e1,e0) )
| ( e0 != op(e1,e1)
& e1 != op(e1,e1)
& e2 != op(e1,e1)
& e3 != op(e1,e1)
& e4 != op(e1,e1) )
| ( e0 != op(e1,e2)
& e1 != op(e1,e2)
& e2 != op(e1,e2)
& e3 != op(e1,e2)
& e4 != op(e1,e2) )
| ( e0 != op(e1,e3)
& e1 != op(e1,e3)
& e2 != op(e1,e3)
& e3 != op(e1,e3)
& e4 != op(e1,e3) )
| ( e0 != op(e1,e4)
& e1 != op(e1,e4)
& e2 != op(e1,e4)
& e3 != op(e1,e4)
& e4 != op(e1,e4) )
| ( e0 != op(e2,e0)
& e1 != op(e2,e0)
& e2 != op(e2,e0)
& e3 != op(e2,e0)
& e4 != op(e2,e0) )
| ( e0 != op(e2,e1)
& e1 != op(e2,e1)
& e2 != op(e2,e1)
& e3 != op(e2,e1)
& e4 != op(e2,e1) )
| ( e0 != op(e2,e2)
& e1 != op(e2,e2)
& e2 != op(e2,e2)
& e3 != op(e2,e2)
& e4 != op(e2,e2) )
| ( e0 != op(e2,e3)
& e1 != op(e2,e3)
& e2 != op(e2,e3)
& e3 != op(e2,e3)
& e4 != op(e2,e3) )
| ( e0 != op(e2,e4)
& e1 != op(e2,e4)
& e2 != op(e2,e4)
& e3 != op(e2,e4)
& e4 != op(e2,e4) )
| ( e0 != op(e3,e0)
& e1 != op(e3,e0)
& e2 != op(e3,e0)
& e3 != op(e3,e0)
& e4 != op(e3,e0) )
| ( e0 != op(e3,e1)
& e1 != op(e3,e1)
& e2 != op(e3,e1)
& e3 != op(e3,e1)
& e4 != op(e3,e1) )
| ( e0 != op(e3,e2)
& e1 != op(e3,e2)
& e2 != op(e3,e2)
& e3 != op(e3,e2)
& e4 != op(e3,e2) )
| ( e0 != op(e3,e3)
& e1 != op(e3,e3)
& e2 != op(e3,e3)
& e3 != op(e3,e3)
& e4 != op(e3,e3) )
| ( e0 != op(e3,e4)
& e1 != op(e3,e4)
& e2 != op(e3,e4)
& e3 != op(e3,e4)
& e4 != op(e3,e4) )
| ( e0 != op(e4,e0)
& e1 != op(e4,e0)
& e2 != op(e4,e0)
& e3 != op(e4,e0)
& e4 != op(e4,e0) )
| ( e0 != op(e4,e1)
& e1 != op(e4,e1)
& e2 != op(e4,e1)
& e3 != op(e4,e1)
& e4 != op(e4,e1) )
| ( e0 != op(e4,e2)
& e1 != op(e4,e2)
& e2 != op(e4,e2)
& e3 != op(e4,e2)
& e4 != op(e4,e2) )
| ( e0 != op(e4,e3)
& e1 != op(e4,e3)
& e2 != op(e4,e3)
& e3 != op(e4,e3)
& e4 != op(e4,e3) )
| ( e0 != op(e4,e4)
& e1 != op(e4,e4)
& e2 != op(e4,e4)
& e3 != op(e4,e4)
& e4 != op(e4,e4) )
| ( e0 != 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) )
| ( e1 != 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) )
| ( e2 != 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) )
| ( e3 != 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) )
| ( e4 != 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) )
| ( e0 != 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) )
| ( e1 != 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) )
| ( e2 != 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) )
| ( e3 != 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) )
| ( e4 != 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) )
| ( e0 != 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) )
| ( e1 != 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) )
| ( e2 != 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) )
| ( e3 != 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) )
| ( e4 != 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) )
| ( e0 != 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) )
| ( e1 != 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) )
| ( e2 != 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) )
| ( e3 != 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) )
| ( e4 != 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) )
| ( e0 != 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) )
| ( e1 != 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) )
| ( e2 != 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) )
| ( e3 != 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) )
| ( e4 != 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) )
| e0 != op(op(e0,e0),op(e0,e0))
| e0 != op(op(e1,e0),op(e0,e1))
| e0 != op(op(e2,e0),op(e0,e2))
| e0 != op(op(e3,e0),op(e0,e3))
| e0 != op(op(e4,e0),op(e0,e4))
| e1 != op(op(e0,e1),op(e1,e0))
| e1 != op(op(e1,e1),op(e1,e1))
| e1 != op(op(e2,e1),op(e1,e2))
| e1 != op(op(e3,e1),op(e1,e3))
| e1 != op(op(e4,e1),op(e1,e4))
| e2 != op(op(e0,e2),op(e2,e0))
| e2 != op(op(e1,e2),op(e2,e1))
| e2 != op(op(e2,e2),op(e2,e2))
| e2 != op(op(e3,e2),op(e2,e3))
| e2 != op(op(e4,e2),op(e2,e4))
| e3 != op(op(e0,e3),op(e3,e0))
| e3 != op(op(e1,e3),op(e3,e1))
| e3 != op(op(e2,e3),op(e3,e2))
| e3 != op(op(e3,e3),op(e3,e3))
| e3 != op(op(e4,e3),op(e3,e4))
| e4 != op(op(e0,e4),op(e4,e0))
| e4 != op(op(e1,e4),op(e4,e1))
| e4 != op(op(e2,e4),op(e4,e2))
| e4 != op(op(e3,e4),op(e4,e3))
| e4 != op(op(e4,e4),op(e4,e4)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f6,definition,
( ( e4 != op(e0,e4)
& e4 != op(e1,e4)
& e4 != op(e2,e4)
& e4 != op(e3,e4)
& e4 != op(e4,e4) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f7,definition,
( ( e4 != op(e4,e0)
& e4 != op(e4,e1)
& e4 != op(e4,e2)
& e4 != op(e4,e3)
& e4 != op(e4,e4) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f8,definition,
( ( e3 != op(e0,e4)
& e3 != op(e1,e4)
& e3 != op(e2,e4)
& e3 != op(e3,e4)
& e3 != op(e4,e4) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f9,definition,
( ( e3 != op(e4,e0)
& e3 != op(e4,e1)
& e3 != op(e4,e2)
& e3 != op(e4,e3)
& e3 != op(e4,e4) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f10,definition,
( ( e2 != op(e0,e4)
& e2 != op(e1,e4)
& e2 != op(e2,e4)
& e2 != op(e3,e4)
& e2 != op(e4,e4) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f11,definition,
( ( e2 != op(e4,e0)
& e2 != op(e4,e1)
& e2 != op(e4,e2)
& e2 != op(e4,e3)
& e2 != op(e4,e4) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f12,definition,
( ( e1 != op(e0,e4)
& e1 != op(e1,e4)
& e1 != op(e2,e4)
& e1 != op(e3,e4)
& e1 != op(e4,e4) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f13,definition,
( ( e1 != op(e4,e0)
& e1 != op(e4,e1)
& e1 != op(e4,e2)
& e1 != op(e4,e3)
& e1 != op(e4,e4) )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ( e0 != op(e0,e4)
& e0 != op(e1,e4)
& e0 != op(e2,e4)
& e0 != op(e3,e4)
& e0 != op(e4,e4) )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ( e0 != op(e4,e0)
& e0 != op(e4,e1)
& e0 != op(e4,e2)
& e0 != op(e4,e3)
& e0 != op(e4,e4) )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ( e4 != op(e0,e3)
& e4 != op(e1,e3)
& e4 != op(e2,e3)
& e4 != op(e3,e3)
& e4 != op(e4,e3) )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f17,definition,
( ( e4 != op(e3,e0)
& e4 != op(e3,e1)
& e4 != op(e3,e2)
& e4 != op(e3,e3)
& e4 != op(e3,e4) )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f18,definition,
( ( e3 != op(e0,e3)
& e3 != op(e1,e3)
& e3 != op(e2,e3)
& e3 != op(e3,e3)
& e3 != op(e4,e3) )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f19,definition,
( ( e3 != op(e3,e0)
& e3 != op(e3,e1)
& e3 != op(e3,e2)
& e3 != op(e3,e3)
& e3 != op(e3,e4) )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f20,definition,
( ( e2 != op(e0,e3)
& e2 != op(e1,e3)
& e2 != op(e2,e3)
& e2 != op(e3,e3)
& e2 != op(e4,e3) )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f21,definition,
( ( e2 != op(e3,e0)
& e2 != op(e3,e1)
& e2 != op(e3,e2)
& e2 != op(e3,e3)
& e2 != op(e3,e4) )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f22,definition,
( ( e1 != op(e0,e3)
& e1 != op(e1,e3)
& e1 != op(e2,e3)
& e1 != op(e3,e3)
& e1 != op(e4,e3) )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( e1 != op(e3,e0)
& e1 != op(e3,e1)
& e1 != op(e3,e2)
& e1 != op(e3,e3)
& e1 != op(e3,e4) )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( e0 != op(e0,e3)
& e0 != op(e1,e3)
& e0 != op(e2,e3)
& e0 != op(e3,e3)
& e0 != op(e4,e3) )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f25,definition,
( ( e0 != op(e3,e0)
& e0 != op(e3,e1)
& e0 != op(e3,e2)
& e0 != op(e3,e3)
& e0 != op(e3,e4) )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f26,definition,
( ( e4 != op(e0,e2)
& e4 != op(e1,e2)
& e4 != op(e2,e2)
& e4 != op(e3,e2)
& e4 != op(e4,e2) )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f27,definition,
( ( e4 != op(e2,e0)
& e4 != op(e2,e1)
& e4 != op(e2,e2)
& e4 != op(e2,e3)
& e4 != op(e2,e4) )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( e3 != op(e0,e2)
& e3 != op(e1,e2)
& e3 != op(e2,e2)
& e3 != op(e3,e2)
& e3 != op(e4,e2) )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f29,definition,
( ( e3 != op(e2,e0)
& e3 != op(e2,e1)
& e3 != op(e2,e2)
& e3 != op(e2,e3)
& e3 != op(e2,e4) )
| ~ sP23 ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f30,definition,
( ( e2 != op(e0,e2)
& e2 != op(e1,e2)
& e2 != op(e2,e2)
& e2 != op(e3,e2)
& e2 != op(e4,e2) )
| ~ sP24 ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f31,definition,
( ( e2 != op(e2,e0)
& e2 != op(e2,e1)
& e2 != op(e2,e2)
& e2 != op(e2,e3)
& e2 != op(e2,e4) )
| ~ sP25 ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f32,definition,
( ( e1 != op(e0,e2)
& e1 != op(e1,e2)
& e1 != op(e2,e2)
& e1 != op(e3,e2)
& e1 != op(e4,e2) )
| ~ sP26 ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f33,definition,
( ( e1 != op(e2,e0)
& e1 != op(e2,e1)
& e1 != op(e2,e2)
& e1 != op(e2,e3)
& e1 != op(e2,e4) )
| ~ sP27 ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f34,definition,
( ( e0 != op(e0,e2)
& e0 != op(e1,e2)
& e0 != op(e2,e2)
& e0 != op(e3,e2)
& e0 != op(e4,e2) )
| ~ sP28 ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f35,definition,
( ( e0 != op(e2,e0)
& e0 != op(e2,e1)
& e0 != op(e2,e2)
& e0 != op(e2,e3)
& e0 != op(e2,e4) )
| ~ sP29 ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f36,definition,
( ( e4 != op(e0,e1)
& e4 != op(e1,e1)
& e4 != op(e2,e1)
& e4 != op(e3,e1)
& e4 != op(e4,e1) )
| ~ sP30 ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f37,definition,
( ( e4 != op(e1,e0)
& e4 != op(e1,e1)
& e4 != op(e1,e2)
& e4 != op(e1,e3)
& e4 != op(e1,e4) )
| ~ sP31 ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f38,definition,
( ( e3 != op(e0,e1)
& e3 != op(e1,e1)
& e3 != op(e2,e1)
& e3 != op(e3,e1)
& e3 != op(e4,e1) )
| ~ sP32 ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f39,definition,
( ( e3 != op(e1,e0)
& e3 != op(e1,e1)
& e3 != op(e1,e2)
& e3 != op(e1,e3)
& e3 != op(e1,e4) )
| ~ sP33 ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f40,definition,
( ( e2 != op(e0,e1)
& e2 != op(e1,e1)
& e2 != op(e2,e1)
& e2 != op(e3,e1)
& e2 != op(e4,e1) )
| ~ sP34 ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f41,definition,
( ( e2 != op(e1,e0)
& e2 != op(e1,e1)
& e2 != op(e1,e2)
& e2 != op(e1,e3)
& e2 != op(e1,e4) )
| ~ sP35 ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f42,definition,
( ( e1 != op(e0,e1)
& e1 != op(e1,e1)
& e1 != op(e2,e1)
& e1 != op(e3,e1)
& e1 != op(e4,e1) )
| ~ sP36 ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f43,definition,
( ( e1 != op(e1,e0)
& e1 != op(e1,e1)
& e1 != op(e1,e2)
& e1 != op(e1,e3)
& e1 != op(e1,e4) )
| ~ sP37 ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f44,definition,
( ( e0 != op(e0,e1)
& e0 != op(e1,e1)
& e0 != op(e2,e1)
& e0 != op(e3,e1)
& e0 != op(e4,e1) )
| ~ sP38 ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f45,definition,
( ( e0 != op(e1,e0)
& e0 != op(e1,e1)
& e0 != op(e1,e2)
& e0 != op(e1,e3)
& e0 != op(e1,e4) )
| ~ sP39 ),
introduced(definition,[new_symbols(definition,[sP39])],[predicate_definition_introduction]) ).
fof(f46,definition,
( ( e4 != op(e0,e0)
& e4 != op(e1,e0)
& e4 != op(e2,e0)
& e4 != op(e3,e0)
& e4 != op(e4,e0) )
| ~ sP40 ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f47,definition,
( ( e4 != op(e0,e0)
& e4 != op(e0,e1)
& e4 != op(e0,e2)
& e4 != op(e0,e3)
& e4 != op(e0,e4) )
| ~ sP41 ),
introduced(definition,[new_symbols(definition,[sP41])],[predicate_definition_introduction]) ).
fof(f48,definition,
( ( e3 != op(e0,e0)
& e3 != op(e1,e0)
& e3 != op(e2,e0)
& e3 != op(e3,e0)
& e3 != op(e4,e0) )
| ~ sP42 ),
introduced(definition,[new_symbols(definition,[sP42])],[predicate_definition_introduction]) ).
fof(f49,definition,
( ( e3 != op(e0,e0)
& e3 != op(e0,e1)
& e3 != op(e0,e2)
& e3 != op(e0,e3)
& e3 != op(e0,e4) )
| ~ sP43 ),
introduced(definition,[new_symbols(definition,[sP43])],[predicate_definition_introduction]) ).
fof(f50,definition,
( ( e2 != op(e0,e0)
& e2 != op(e1,e0)
& e2 != op(e2,e0)
& e2 != op(e3,e0)
& e2 != op(e4,e0) )
| ~ sP44 ),
introduced(definition,[new_symbols(definition,[sP44])],[predicate_definition_introduction]) ).
fof(f51,definition,
( ( e2 != op(e0,e0)
& e2 != op(e0,e1)
& e2 != op(e0,e2)
& e2 != op(e0,e3)
& e2 != op(e0,e4) )
| ~ sP45 ),
introduced(definition,[new_symbols(definition,[sP45])],[predicate_definition_introduction]) ).
fof(f52,definition,
( ( e1 != op(e0,e0)
& e1 != op(e1,e0)
& e1 != op(e2,e0)
& e1 != op(e3,e0)
& e1 != op(e4,e0) )
| ~ sP46 ),
introduced(definition,[new_symbols(definition,[sP46])],[predicate_definition_introduction]) ).
fof(f53,definition,
( ( e1 != op(e0,e0)
& e1 != op(e0,e1)
& e1 != op(e0,e2)
& e1 != op(e0,e3)
& e1 != op(e0,e4) )
| ~ sP47 ),
introduced(definition,[new_symbols(definition,[sP47])],[predicate_definition_introduction]) ).
fof(f54,definition,
( ( e0 != op(e0,e0)
& e0 != op(e1,e0)
& e0 != op(e2,e0)
& e0 != op(e3,e0)
& e0 != op(e4,e0) )
| ~ sP48 ),
introduced(definition,[new_symbols(definition,[sP48])],[predicate_definition_introduction]) ).
fof(f55,definition,
( ( e0 != op(e0,e0)
& e0 != op(e0,e1)
& e0 != op(e0,e2)
& e0 != op(e0,e3)
& e0 != op(e0,e4) )
| ~ sP49 ),
introduced(definition,[new_symbols(definition,[sP49])],[predicate_definition_introduction]) ).
fof(f56,definition,
( ( e0 != op(e4,e4)
& e1 != op(e4,e4)
& e2 != op(e4,e4)
& e3 != op(e4,e4)
& e4 != op(e4,e4) )
| ~ sP50 ),
introduced(definition,[new_symbols(definition,[sP50])],[predicate_definition_introduction]) ).
fof(f57,definition,
( ( e0 != op(e4,e3)
& e1 != op(e4,e3)
& e2 != op(e4,e3)
& e3 != op(e4,e3)
& e4 != op(e4,e3) )
| ~ sP51 ),
introduced(definition,[new_symbols(definition,[sP51])],[predicate_definition_introduction]) ).
fof(f58,definition,
( ( e0 != op(e4,e2)
& e1 != op(e4,e2)
& e2 != op(e4,e2)
& e3 != op(e4,e2)
& e4 != op(e4,e2) )
| ~ sP52 ),
introduced(definition,[new_symbols(definition,[sP52])],[predicate_definition_introduction]) ).
fof(f59,definition,
( ( e0 != op(e4,e1)
& e1 != op(e4,e1)
& e2 != op(e4,e1)
& e3 != op(e4,e1)
& e4 != op(e4,e1) )
| ~ sP53 ),
introduced(definition,[new_symbols(definition,[sP53])],[predicate_definition_introduction]) ).
fof(f60,definition,
( ( e0 != op(e4,e0)
& e1 != op(e4,e0)
& e2 != op(e4,e0)
& e3 != op(e4,e0)
& e4 != op(e4,e0) )
| ~ sP54 ),
introduced(definition,[new_symbols(definition,[sP54])],[predicate_definition_introduction]) ).
fof(f61,definition,
( ( e0 != op(e3,e4)
& e1 != op(e3,e4)
& e2 != op(e3,e4)
& e3 != op(e3,e4)
& e4 != op(e3,e4) )
| ~ sP55 ),
introduced(definition,[new_symbols(definition,[sP55])],[predicate_definition_introduction]) ).
fof(f62,definition,
( ( e0 != op(e3,e3)
& e1 != op(e3,e3)
& e2 != op(e3,e3)
& e3 != op(e3,e3)
& e4 != op(e3,e3) )
| ~ sP56 ),
introduced(definition,[new_symbols(definition,[sP56])],[predicate_definition_introduction]) ).
fof(f63,definition,
( ( e0 != op(e3,e2)
& e1 != op(e3,e2)
& e2 != op(e3,e2)
& e3 != op(e3,e2)
& e4 != op(e3,e2) )
| ~ sP57 ),
introduced(definition,[new_symbols(definition,[sP57])],[predicate_definition_introduction]) ).
fof(f64,definition,
( ( e0 != op(e3,e1)
& e1 != op(e3,e1)
& e2 != op(e3,e1)
& e3 != op(e3,e1)
& e4 != op(e3,e1) )
| ~ sP58 ),
introduced(definition,[new_symbols(definition,[sP58])],[predicate_definition_introduction]) ).
fof(f65,definition,
( ( e0 != op(e3,e0)
& e1 != op(e3,e0)
& e2 != op(e3,e0)
& e3 != op(e3,e0)
& e4 != op(e3,e0) )
| ~ sP59 ),
introduced(definition,[new_symbols(definition,[sP59])],[predicate_definition_introduction]) ).
fof(f66,definition,
( ( e0 != op(e2,e4)
& e1 != op(e2,e4)
& e2 != op(e2,e4)
& e3 != op(e2,e4)
& e4 != op(e2,e4) )
| ~ sP60 ),
introduced(definition,[new_symbols(definition,[sP60])],[predicate_definition_introduction]) ).
fof(f67,definition,
( ( e0 != op(e2,e3)
& e1 != op(e2,e3)
& e2 != op(e2,e3)
& e3 != op(e2,e3)
& e4 != op(e2,e3) )
| ~ sP61 ),
introduced(definition,[new_symbols(definition,[sP61])],[predicate_definition_introduction]) ).
fof(f68,definition,
( ( e0 != op(e2,e2)
& e1 != op(e2,e2)
& e2 != op(e2,e2)
& e3 != op(e2,e2)
& e4 != op(e2,e2) )
| ~ sP62 ),
introduced(definition,[new_symbols(definition,[sP62])],[predicate_definition_introduction]) ).
fof(f69,definition,
( ( e0 != op(e2,e1)
& e1 != op(e2,e1)
& e2 != op(e2,e1)
& e3 != op(e2,e1)
& e4 != op(e2,e1) )
| ~ sP63 ),
introduced(definition,[new_symbols(definition,[sP63])],[predicate_definition_introduction]) ).
fof(f70,definition,
( ( e0 != op(e2,e0)
& e1 != op(e2,e0)
& e2 != op(e2,e0)
& e3 != op(e2,e0)
& e4 != op(e2,e0) )
| ~ sP64 ),
introduced(definition,[new_symbols(definition,[sP64])],[predicate_definition_introduction]) ).
fof(f71,definition,
( ( e0 != op(e1,e4)
& e1 != op(e1,e4)
& e2 != op(e1,e4)
& e3 != op(e1,e4)
& e4 != op(e1,e4) )
| ~ sP65 ),
introduced(definition,[new_symbols(definition,[sP65])],[predicate_definition_introduction]) ).
fof(f72,definition,
( ( e0 != op(e1,e3)
& e1 != op(e1,e3)
& e2 != op(e1,e3)
& e3 != op(e1,e3)
& e4 != op(e1,e3) )
| ~ sP66 ),
introduced(definition,[new_symbols(definition,[sP66])],[predicate_definition_introduction]) ).
fof(f73,definition,
( ( e0 != op(e1,e2)
& e1 != op(e1,e2)
& e2 != op(e1,e2)
& e3 != op(e1,e2)
& e4 != op(e1,e2) )
| ~ sP67 ),
introduced(definition,[new_symbols(definition,[sP67])],[predicate_definition_introduction]) ).
fof(f74,definition,
( ( e0 != op(e1,e1)
& e1 != op(e1,e1)
& e2 != op(e1,e1)
& e3 != op(e1,e1)
& e4 != op(e1,e1) )
| ~ sP68 ),
introduced(definition,[new_symbols(definition,[sP68])],[predicate_definition_introduction]) ).
fof(f75,definition,
( ( e0 != op(e1,e0)
& e1 != op(e1,e0)
& e2 != op(e1,e0)
& e3 != op(e1,e0)
& e4 != op(e1,e0) )
| ~ sP69 ),
introduced(definition,[new_symbols(definition,[sP69])],[predicate_definition_introduction]) ).
fof(f76,definition,
( ( e0 != op(e0,e4)
& e1 != op(e0,e4)
& e2 != op(e0,e4)
& e3 != op(e0,e4)
& e4 != op(e0,e4) )
| ~ sP70 ),
introduced(definition,[new_symbols(definition,[sP70])],[predicate_definition_introduction]) ).
fof(f77,definition,
( ( e0 != op(e0,e3)
& e1 != op(e0,e3)
& e2 != op(e0,e3)
& e3 != op(e0,e3)
& e4 != op(e0,e3) )
| ~ sP71 ),
introduced(definition,[new_symbols(definition,[sP71])],[predicate_definition_introduction]) ).
fof(f78,definition,
( ( e0 != op(e0,e2)
& e1 != op(e0,e2)
& e2 != op(e0,e2)
& e3 != op(e0,e2)
& e4 != op(e0,e2) )
| ~ sP72 ),
introduced(definition,[new_symbols(definition,[sP72])],[predicate_definition_introduction]) ).
fof(f79,definition,
( ( e0 != op(e0,e1)
& e1 != op(e0,e1)
& e2 != op(e0,e1)
& e3 != op(e0,e1)
& e4 != op(e0,e1) )
| ~ sP73 ),
introduced(definition,[new_symbols(definition,[sP73])],[predicate_definition_introduction]) ).
fof(f80,definition,
( ( e0 != op(e0,e0)
& e1 != op(e0,e0)
& e2 != op(e0,e0)
& e3 != op(e0,e0)
& e4 != op(e0,e0) )
| ~ sP74 ),
introduced(definition,[new_symbols(definition,[sP74])],[predicate_definition_introduction]) ).
fof(f81,plain,
( ( ( e0 = op(e0,e0)
| e1 = op(e1,e0)
| e2 = op(e2,e0)
| e3 = op(e3,e0)
| e4 = op(e4,e0) )
& ( e0 = op(e0,e1)
| e1 = op(e1,e1)
| e2 = op(e2,e1)
| e3 = op(e3,e1)
| e4 = op(e4,e1) )
& ( e0 = op(e0,e2)
| e1 = op(e1,e2)
| e2 = op(e2,e2)
| e3 = op(e3,e2)
| e4 = op(e4,e2) )
& ( e0 = op(e0,e3)
| e1 = op(e1,e3)
| e2 = op(e2,e3)
| e3 = op(e3,e3)
| e4 = op(e4,e3) )
& ( e0 = op(e0,e4)
| e1 = op(e1,e4)
| e2 = op(e2,e4)
| e3 = op(e3,e4)
| e4 = op(e4,e4) ) )
| 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
| 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
| 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
| e0 != op(op(e0,e0),op(e0,e0))
| e0 != op(op(e1,e0),op(e0,e1))
| e0 != op(op(e2,e0),op(e0,e2))
| e0 != op(op(e3,e0),op(e0,e3))
| e0 != op(op(e4,e0),op(e0,e4))
| e1 != op(op(e0,e1),op(e1,e0))
| e1 != op(op(e1,e1),op(e1,e1))
| e1 != op(op(e2,e1),op(e1,e2))
| e1 != op(op(e3,e1),op(e1,e3))
| e1 != op(op(e4,e1),op(e1,e4))
| e2 != op(op(e0,e2),op(e2,e0))
| e2 != op(op(e1,e2),op(e2,e1))
| e2 != op(op(e2,e2),op(e2,e2))
| e2 != op(op(e3,e2),op(e2,e3))
| e2 != op(op(e4,e2),op(e2,e4))
| e3 != op(op(e0,e3),op(e3,e0))
| e3 != op(op(e1,e3),op(e3,e1))
| e3 != op(op(e2,e3),op(e3,e2))
| e3 != op(op(e3,e3),op(e3,e3))
| e3 != op(op(e4,e3),op(e3,e4))
| e4 != op(op(e0,e4),op(e4,e0))
| e4 != op(op(e1,e4),op(e4,e1))
| e4 != op(op(e2,e4),op(e4,e2))
| e4 != op(op(e3,e4),op(e4,e3))
| e4 != op(op(e4,e4),op(e4,e4)) ),
inference(definition_folding,[],[f5,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,f9,f8,f7,f6]) ).
fof(f82,plain,
( ( e0 != op(e0,e0)
& e1 != op(e0,e0)
& e2 != op(e0,e0)
& e3 != op(e0,e0)
& e4 != op(e0,e0) )
| ~ sP74 ),
inference(nnf_transformation,[],[f80]) ).
fof(f83,plain,
( ( e0 != op(e0,e1)
& e1 != op(e0,e1)
& e2 != op(e0,e1)
& e3 != op(e0,e1)
& e4 != op(e0,e1) )
| ~ sP73 ),
inference(nnf_transformation,[],[f79]) ).
fof(f84,plain,
( ( e0 != op(e0,e2)
& e1 != op(e0,e2)
& e2 != op(e0,e2)
& e3 != op(e0,e2)
& e4 != op(e0,e2) )
| ~ sP72 ),
inference(nnf_transformation,[],[f78]) ).
fof(f85,plain,
( ( e0 != op(e0,e3)
& e1 != op(e0,e3)
& e2 != op(e0,e3)
& e3 != op(e0,e3)
& e4 != op(e0,e3) )
| ~ sP71 ),
inference(nnf_transformation,[],[f77]) ).
fof(f86,plain,
( ( e0 != op(e0,e4)
& e1 != op(e0,e4)
& e2 != op(e0,e4)
& e3 != op(e0,e4)
& e4 != op(e0,e4) )
| ~ sP70 ),
inference(nnf_transformation,[],[f76]) ).
fof(f87,plain,
( ( e0 != op(e1,e0)
& e1 != op(e1,e0)
& e2 != op(e1,e0)
& e3 != op(e1,e0)
& e4 != op(e1,e0) )
| ~ sP69 ),
inference(nnf_transformation,[],[f75]) ).
fof(f88,plain,
( ( e0 != op(e1,e1)
& e1 != op(e1,e1)
& e2 != op(e1,e1)
& e3 != op(e1,e1)
& e4 != op(e1,e1) )
| ~ sP68 ),
inference(nnf_transformation,[],[f74]) ).
fof(f89,plain,
( ( e0 != op(e1,e2)
& e1 != op(e1,e2)
& e2 != op(e1,e2)
& e3 != op(e1,e2)
& e4 != op(e1,e2) )
| ~ sP67 ),
inference(nnf_transformation,[],[f73]) ).
fof(f90,plain,
( ( e0 != op(e1,e3)
& e1 != op(e1,e3)
& e2 != op(e1,e3)
& e3 != op(e1,e3)
& e4 != op(e1,e3) )
| ~ sP66 ),
inference(nnf_transformation,[],[f72]) ).
fof(f91,plain,
( ( e0 != op(e1,e4)
& e1 != op(e1,e4)
& e2 != op(e1,e4)
& e3 != op(e1,e4)
& e4 != op(e1,e4) )
| ~ sP65 ),
inference(nnf_transformation,[],[f71]) ).
fof(f92,plain,
( ( e0 != op(e2,e0)
& e1 != op(e2,e0)
& e2 != op(e2,e0)
& e3 != op(e2,e0)
& e4 != op(e2,e0) )
| ~ sP64 ),
inference(nnf_transformation,[],[f70]) ).
fof(f93,plain,
( ( e0 != op(e2,e1)
& e1 != op(e2,e1)
& e2 != op(e2,e1)
& e3 != op(e2,e1)
& e4 != op(e2,e1) )
| ~ sP63 ),
inference(nnf_transformation,[],[f69]) ).
fof(f94,plain,
( ( e0 != op(e2,e2)
& e1 != op(e2,e2)
& e2 != op(e2,e2)
& e3 != op(e2,e2)
& e4 != op(e2,e2) )
| ~ sP62 ),
inference(nnf_transformation,[],[f68]) ).
fof(f95,plain,
( ( e0 != op(e2,e3)
& e1 != op(e2,e3)
& e2 != op(e2,e3)
& e3 != op(e2,e3)
& e4 != op(e2,e3) )
| ~ sP61 ),
inference(nnf_transformation,[],[f67]) ).
fof(f96,plain,
( ( e0 != op(e2,e4)
& e1 != op(e2,e4)
& e2 != op(e2,e4)
& e3 != op(e2,e4)
& e4 != op(e2,e4) )
| ~ sP60 ),
inference(nnf_transformation,[],[f66]) ).
fof(f97,plain,
( ( e0 != op(e3,e0)
& e1 != op(e3,e0)
& e2 != op(e3,e0)
& e3 != op(e3,e0)
& e4 != op(e3,e0) )
| ~ sP59 ),
inference(nnf_transformation,[],[f65]) ).
fof(f98,plain,
( ( e0 != op(e3,e1)
& e1 != op(e3,e1)
& e2 != op(e3,e1)
& e3 != op(e3,e1)
& e4 != op(e3,e1) )
| ~ sP58 ),
inference(nnf_transformation,[],[f64]) ).
fof(f99,plain,
( ( e0 != op(e3,e2)
& e1 != op(e3,e2)
& e2 != op(e3,e2)
& e3 != op(e3,e2)
& e4 != op(e3,e2) )
| ~ sP57 ),
inference(nnf_transformation,[],[f63]) ).
fof(f100,plain,
( ( e0 != op(e3,e3)
& e1 != op(e3,e3)
& e2 != op(e3,e3)
& e3 != op(e3,e3)
& e4 != op(e3,e3) )
| ~ sP56 ),
inference(nnf_transformation,[],[f62]) ).
fof(f101,plain,
( ( e0 != op(e3,e4)
& e1 != op(e3,e4)
& e2 != op(e3,e4)
& e3 != op(e3,e4)
& e4 != op(e3,e4) )
| ~ sP55 ),
inference(nnf_transformation,[],[f61]) ).
fof(f102,plain,
( ( e0 != op(e4,e0)
& e1 != op(e4,e0)
& e2 != op(e4,e0)
& e3 != op(e4,e0)
& e4 != op(e4,e0) )
| ~ sP54 ),
inference(nnf_transformation,[],[f60]) ).
fof(f103,plain,
( ( e0 != op(e4,e1)
& e1 != op(e4,e1)
& e2 != op(e4,e1)
& e3 != op(e4,e1)
& e4 != op(e4,e1) )
| ~ sP53 ),
inference(nnf_transformation,[],[f59]) ).
fof(f104,plain,
( ( e0 != op(e4,e2)
& e1 != op(e4,e2)
& e2 != op(e4,e2)
& e3 != op(e4,e2)
& e4 != op(e4,e2) )
| ~ sP52 ),
inference(nnf_transformation,[],[f58]) ).
fof(f105,plain,
( ( e0 != op(e4,e3)
& e1 != op(e4,e3)
& e2 != op(e4,e3)
& e3 != op(e4,e3)
& e4 != op(e4,e3) )
| ~ sP51 ),
inference(nnf_transformation,[],[f57]) ).
fof(f106,plain,
( ( e0 != op(e4,e4)
& e1 != op(e4,e4)
& e2 != op(e4,e4)
& e3 != op(e4,e4)
& e4 != op(e4,e4) )
| ~ sP50 ),
inference(nnf_transformation,[],[f56]) ).
fof(f107,plain,
( ( e0 != op(e0,e0)
& e0 != op(e0,e1)
& e0 != op(e0,e2)
& e0 != op(e0,e3)
& e0 != op(e0,e4) )
| ~ sP49 ),
inference(nnf_transformation,[],[f55]) ).
fof(f108,plain,
( ( e0 != op(e0,e0)
& e0 != op(e1,e0)
& e0 != op(e2,e0)
& e0 != op(e3,e0)
& e0 != op(e4,e0) )
| ~ sP48 ),
inference(nnf_transformation,[],[f54]) ).
fof(f109,plain,
( ( e1 != op(e0,e0)
& e1 != op(e0,e1)
& e1 != op(e0,e2)
& e1 != op(e0,e3)
& e1 != op(e0,e4) )
| ~ sP47 ),
inference(nnf_transformation,[],[f53]) ).
fof(f110,plain,
( ( e1 != op(e0,e0)
& e1 != op(e1,e0)
& e1 != op(e2,e0)
& e1 != op(e3,e0)
& e1 != op(e4,e0) )
| ~ sP46 ),
inference(nnf_transformation,[],[f52]) ).
fof(f111,plain,
( ( e2 != op(e0,e0)
& e2 != op(e0,e1)
& e2 != op(e0,e2)
& e2 != op(e0,e3)
& e2 != op(e0,e4) )
| ~ sP45 ),
inference(nnf_transformation,[],[f51]) ).
fof(f112,plain,
( ( e2 != op(e0,e0)
& e2 != op(e1,e0)
& e2 != op(e2,e0)
& e2 != op(e3,e0)
& e2 != op(e4,e0) )
| ~ sP44 ),
inference(nnf_transformation,[],[f50]) ).
fof(f113,plain,
( ( e3 != op(e0,e0)
& e3 != op(e0,e1)
& e3 != op(e0,e2)
& e3 != op(e0,e3)
& e3 != op(e0,e4) )
| ~ sP43 ),
inference(nnf_transformation,[],[f49]) ).
fof(f114,plain,
( ( e3 != op(e0,e0)
& e3 != op(e1,e0)
& e3 != op(e2,e0)
& e3 != op(e3,e0)
& e3 != op(e4,e0) )
| ~ sP42 ),
inference(nnf_transformation,[],[f48]) ).
fof(f115,plain,
( ( e4 != op(e0,e0)
& e4 != op(e0,e1)
& e4 != op(e0,e2)
& e4 != op(e0,e3)
& e4 != op(e0,e4) )
| ~ sP41 ),
inference(nnf_transformation,[],[f47]) ).
fof(f116,plain,
( ( e4 != op(e0,e0)
& e4 != op(e1,e0)
& e4 != op(e2,e0)
& e4 != op(e3,e0)
& e4 != op(e4,e0) )
| ~ sP40 ),
inference(nnf_transformation,[],[f46]) ).
fof(f117,plain,
( ( e0 != op(e1,e0)
& e0 != op(e1,e1)
& e0 != op(e1,e2)
& e0 != op(e1,e3)
& e0 != op(e1,e4) )
| ~ sP39 ),
inference(nnf_transformation,[],[f45]) ).
fof(f118,plain,
( ( e0 != op(e0,e1)
& e0 != op(e1,e1)
& e0 != op(e2,e1)
& e0 != op(e3,e1)
& e0 != op(e4,e1) )
| ~ sP38 ),
inference(nnf_transformation,[],[f44]) ).
fof(f119,plain,
( ( e1 != op(e1,e0)
& e1 != op(e1,e1)
& e1 != op(e1,e2)
& e1 != op(e1,e3)
& e1 != op(e1,e4) )
| ~ sP37 ),
inference(nnf_transformation,[],[f43]) ).
fof(f120,plain,
( ( e1 != op(e0,e1)
& e1 != op(e1,e1)
& e1 != op(e2,e1)
& e1 != op(e3,e1)
& e1 != op(e4,e1) )
| ~ sP36 ),
inference(nnf_transformation,[],[f42]) ).
fof(f121,plain,
( ( e2 != op(e1,e0)
& e2 != op(e1,e1)
& e2 != op(e1,e2)
& e2 != op(e1,e3)
& e2 != op(e1,e4) )
| ~ sP35 ),
inference(nnf_transformation,[],[f41]) ).
fof(f122,plain,
( ( e2 != op(e0,e1)
& e2 != op(e1,e1)
& e2 != op(e2,e1)
& e2 != op(e3,e1)
& e2 != op(e4,e1) )
| ~ sP34 ),
inference(nnf_transformation,[],[f40]) ).
fof(f123,plain,
( ( e3 != op(e1,e0)
& e3 != op(e1,e1)
& e3 != op(e1,e2)
& e3 != op(e1,e3)
& e3 != op(e1,e4) )
| ~ sP33 ),
inference(nnf_transformation,[],[f39]) ).
fof(f124,plain,
( ( e3 != op(e0,e1)
& e3 != op(e1,e1)
& e3 != op(e2,e1)
& e3 != op(e3,e1)
& e3 != op(e4,e1) )
| ~ sP32 ),
inference(nnf_transformation,[],[f38]) ).
fof(f125,plain,
( ( e4 != op(e1,e0)
& e4 != op(e1,e1)
& e4 != op(e1,e2)
& e4 != op(e1,e3)
& e4 != op(e1,e4) )
| ~ sP31 ),
inference(nnf_transformation,[],[f37]) ).
fof(f126,plain,
( ( e4 != op(e0,e1)
& e4 != op(e1,e1)
& e4 != op(e2,e1)
& e4 != op(e3,e1)
& e4 != op(e4,e1) )
| ~ sP30 ),
inference(nnf_transformation,[],[f36]) ).
fof(f127,plain,
( ( e0 != op(e2,e0)
& e0 != op(e2,e1)
& e0 != op(e2,e2)
& e0 != op(e2,e3)
& e0 != op(e2,e4) )
| ~ sP29 ),
inference(nnf_transformation,[],[f35]) ).
fof(f128,plain,
( ( e0 != op(e0,e2)
& e0 != op(e1,e2)
& e0 != op(e2,e2)
& e0 != op(e3,e2)
& e0 != op(e4,e2) )
| ~ sP28 ),
inference(nnf_transformation,[],[f34]) ).
fof(f129,plain,
( ( e1 != op(e2,e0)
& e1 != op(e2,e1)
& e1 != op(e2,e2)
& e1 != op(e2,e3)
& e1 != op(e2,e4) )
| ~ sP27 ),
inference(nnf_transformation,[],[f33]) ).
fof(f130,plain,
( ( e1 != op(e0,e2)
& e1 != op(e1,e2)
& e1 != op(e2,e2)
& e1 != op(e3,e2)
& e1 != op(e4,e2) )
| ~ sP26 ),
inference(nnf_transformation,[],[f32]) ).
fof(f131,plain,
( ( e2 != op(e2,e0)
& e2 != op(e2,e1)
& e2 != op(e2,e2)
& e2 != op(e2,e3)
& e2 != op(e2,e4) )
| ~ sP25 ),
inference(nnf_transformation,[],[f31]) ).
fof(f132,plain,
( ( e2 != op(e0,e2)
& e2 != op(e1,e2)
& e2 != op(e2,e2)
& e2 != op(e3,e2)
& e2 != op(e4,e2) )
| ~ sP24 ),
inference(nnf_transformation,[],[f30]) ).
fof(f133,plain,
( ( e3 != op(e2,e0)
& e3 != op(e2,e1)
& e3 != op(e2,e2)
& e3 != op(e2,e3)
& e3 != op(e2,e4) )
| ~ sP23 ),
inference(nnf_transformation,[],[f29]) ).
fof(f134,plain,
( ( e3 != op(e0,e2)
& e3 != op(e1,e2)
& e3 != op(e2,e2)
& e3 != op(e3,e2)
& e3 != op(e4,e2) )
| ~ sP22 ),
inference(nnf_transformation,[],[f28]) ).
fof(f135,plain,
( ( e4 != op(e2,e0)
& e4 != op(e2,e1)
& e4 != op(e2,e2)
& e4 != op(e2,e3)
& e4 != op(e2,e4) )
| ~ sP21 ),
inference(nnf_transformation,[],[f27]) ).
fof(f136,plain,
( ( e4 != op(e0,e2)
& e4 != op(e1,e2)
& e4 != op(e2,e2)
& e4 != op(e3,e2)
& e4 != op(e4,e2) )
| ~ sP20 ),
inference(nnf_transformation,[],[f26]) ).
fof(f137,plain,
( ( e0 != op(e3,e0)
& e0 != op(e3,e1)
& e0 != op(e3,e2)
& e0 != op(e3,e3)
& e0 != op(e3,e4) )
| ~ sP19 ),
inference(nnf_transformation,[],[f25]) ).
fof(f138,plain,
( ( e0 != op(e0,e3)
& e0 != op(e1,e3)
& e0 != op(e2,e3)
& e0 != op(e3,e3)
& e0 != op(e4,e3) )
| ~ sP18 ),
inference(nnf_transformation,[],[f24]) ).
fof(f139,plain,
( ( e1 != op(e3,e0)
& e1 != op(e3,e1)
& e1 != op(e3,e2)
& e1 != op(e3,e3)
& e1 != op(e3,e4) )
| ~ sP17 ),
inference(nnf_transformation,[],[f23]) ).
fof(f140,plain,
( ( e1 != op(e0,e3)
& e1 != op(e1,e3)
& e1 != op(e2,e3)
& e1 != op(e3,e3)
& e1 != op(e4,e3) )
| ~ sP16 ),
inference(nnf_transformation,[],[f22]) ).
fof(f141,plain,
( ( e2 != op(e3,e0)
& e2 != op(e3,e1)
& e2 != op(e3,e2)
& e2 != op(e3,e3)
& e2 != op(e3,e4) )
| ~ sP15 ),
inference(nnf_transformation,[],[f21]) ).
fof(f142,plain,
( ( e2 != op(e0,e3)
& e2 != op(e1,e3)
& e2 != op(e2,e3)
& e2 != op(e3,e3)
& e2 != op(e4,e3) )
| ~ sP14 ),
inference(nnf_transformation,[],[f20]) ).
fof(f143,plain,
( ( e3 != op(e3,e0)
& e3 != op(e3,e1)
& e3 != op(e3,e2)
& e3 != op(e3,e3)
& e3 != op(e3,e4) )
| ~ sP13 ),
inference(nnf_transformation,[],[f19]) ).
fof(f144,plain,
( ( e3 != op(e0,e3)
& e3 != op(e1,e3)
& e3 != op(e2,e3)
& e3 != op(e3,e3)
& e3 != op(e4,e3) )
| ~ sP12 ),
inference(nnf_transformation,[],[f18]) ).
fof(f145,plain,
( ( e4 != op(e3,e0)
& e4 != op(e3,e1)
& e4 != op(e3,e2)
& e4 != op(e3,e3)
& e4 != op(e3,e4) )
| ~ sP11 ),
inference(nnf_transformation,[],[f17]) ).
fof(f146,plain,
( ( e4 != op(e0,e3)
& e4 != op(e1,e3)
& e4 != op(e2,e3)
& e4 != op(e3,e3)
& e4 != op(e4,e3) )
| ~ sP10 ),
inference(nnf_transformation,[],[f16]) ).
fof(f147,plain,
( ( e0 != op(e4,e0)
& e0 != op(e4,e1)
& e0 != op(e4,e2)
& e0 != op(e4,e3)
& e0 != op(e4,e4) )
| ~ sP9 ),
inference(nnf_transformation,[],[f15]) ).
fof(f148,plain,
( ( e0 != op(e0,e4)
& e0 != op(e1,e4)
& e0 != op(e2,e4)
& e0 != op(e3,e4)
& e0 != op(e4,e4) )
| ~ sP8 ),
inference(nnf_transformation,[],[f14]) ).
fof(f149,plain,
( ( e1 != op(e4,e0)
& e1 != op(e4,e1)
& e1 != op(e4,e2)
& e1 != op(e4,e3)
& e1 != op(e4,e4) )
| ~ sP7 ),
inference(nnf_transformation,[],[f13]) ).
fof(f150,plain,
( ( e1 != op(e0,e4)
& e1 != op(e1,e4)
& e1 != op(e2,e4)
& e1 != op(e3,e4)
& e1 != op(e4,e4) )
| ~ sP6 ),
inference(nnf_transformation,[],[f12]) ).
fof(f151,plain,
( ( e2 != op(e4,e0)
& e2 != op(e4,e1)
& e2 != op(e4,e2)
& e2 != op(e4,e3)
& e2 != op(e4,e4) )
| ~ sP5 ),
inference(nnf_transformation,[],[f11]) ).
fof(f152,plain,
( ( e2 != op(e0,e4)
& e2 != op(e1,e4)
& e2 != op(e2,e4)
& e2 != op(e3,e4)
& e2 != op(e4,e4) )
| ~ sP4 ),
inference(nnf_transformation,[],[f10]) ).
fof(f153,plain,
( ( e3 != op(e4,e0)
& e3 != op(e4,e1)
& e3 != op(e4,e2)
& e3 != op(e4,e3)
& e3 != op(e4,e4) )
| ~ sP3 ),
inference(nnf_transformation,[],[f9]) ).
fof(f154,plain,
( ( e3 != op(e0,e4)
& e3 != op(e1,e4)
& e3 != op(e2,e4)
& e3 != op(e3,e4)
& e3 != op(e4,e4) )
| ~ sP2 ),
inference(nnf_transformation,[],[f8]) ).
fof(f155,plain,
( ( e4 != op(e4,e0)
& e4 != op(e4,e1)
& e4 != op(e4,e2)
& e4 != op(e4,e3)
& e4 != op(e4,e4) )
| ~ sP1 ),
inference(nnf_transformation,[],[f7]) ).
fof(f156,plain,
( ( e4 != op(e0,e4)
& e4 != op(e1,e4)
& e4 != op(e2,e4)
& e4 != op(e3,e4)
& e4 != op(e4,e4) )
| ~ sP0 ),
inference(nnf_transformation,[],[f6]) ).
fof(f159,plain,
e2 != e3,
inference(cnf_transformation,[],[f1]) ).
fof(f160,plain,
e1 != e4,
inference(cnf_transformation,[],[f1]) ).
fof(f161,plain,
e1 != e3,
inference(cnf_transformation,[],[f1]) ).
fof(f163,plain,
e0 != e4,
inference(cnf_transformation,[],[f1]) ).
fof(f165,plain,
e0 != e2,
inference(cnf_transformation,[],[f1]) ).
fof(f167,plain,
e1 = op(e4,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f168,plain,
e3 = op(e4,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f169,plain,
e4 = op(e4,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f170,plain,
e0 = op(e4,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f171,plain,
e2 = op(e4,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f172,plain,
e2 = op(e3,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f173,plain,
e0 = op(e3,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f174,plain,
e3 = op(e3,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f175,plain,
e1 = op(e3,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f176,plain,
e4 = op(e3,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f177,plain,
e0 = op(e2,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f178,plain,
e4 = op(e2,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f179,plain,
e2 = op(e2,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f180,plain,
e3 = op(e2,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f181,plain,
e1 = op(e2,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f182,plain,
e3 = op(e1,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f183,plain,
e2 = op(e1,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f184,plain,
e1 = op(e1,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f185,plain,
e4 = op(e1,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f186,plain,
e0 = op(e1,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f187,plain,
e4 = op(e0,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f188,plain,
e1 = op(e0,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f189,plain,
e0 = op(e0,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f190,plain,
e2 = op(e0,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f191,plain,
e3 = op(e0,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f193,plain,
( e3 != op(e0,e0)
| ~ sP74 ),
inference(cnf_transformation,[],[f82]) ).
fof(f199,plain,
( e2 != op(e0,e1)
| ~ sP73 ),
inference(cnf_transformation,[],[f83]) ).
fof(f206,plain,
( e0 != op(e0,e2)
| ~ sP72 ),
inference(cnf_transformation,[],[f84]) ).
fof(f210,plain,
( e1 != op(e0,e3)
| ~ sP71 ),
inference(cnf_transformation,[],[f85]) ).
fof(f212,plain,
( e4 != op(e0,e4)
| ~ sP70 ),
inference(cnf_transformation,[],[f86]) ).
fof(f221,plain,
( e0 != op(e1,e0)
| ~ sP69 ),
inference(cnf_transformation,[],[f87]) ).
fof(f222,plain,
( e4 != op(e1,e1)
| ~ sP68 ),
inference(cnf_transformation,[],[f88]) ).
fof(f230,plain,
( e1 != op(e1,e2)
| ~ sP67 ),
inference(cnf_transformation,[],[f89]) ).
fof(f234,plain,
( e2 != op(e1,e3)
| ~ sP66 ),
inference(cnf_transformation,[],[f90]) ).
fof(f238,plain,
( e3 != op(e1,e4)
| ~ sP65 ),
inference(cnf_transformation,[],[f91]) ).
fof(f245,plain,
( e1 != op(e2,e0)
| ~ sP64 ),
inference(cnf_transformation,[],[f92]) ).
fof(f248,plain,
( e3 != op(e2,e1)
| ~ sP63 ),
inference(cnf_transformation,[],[f93]) ).
fof(f254,plain,
( e2 != op(e2,e2)
| ~ sP62 ),
inference(cnf_transformation,[],[f94]) ).
fof(f257,plain,
( e4 != op(e2,e3)
| ~ sP61 ),
inference(cnf_transformation,[],[f95]) ).
fof(f266,plain,
( e0 != op(e2,e4)
| ~ sP60 ),
inference(cnf_transformation,[],[f96]) ).
fof(f267,plain,
( e4 != op(e3,e0)
| ~ sP59 ),
inference(cnf_transformation,[],[f97]) ).
fof(f275,plain,
( e1 != op(e3,e1)
| ~ sP58 ),
inference(cnf_transformation,[],[f98]) ).
fof(f278,plain,
( e3 != op(e3,e2)
| ~ sP57 ),
inference(cnf_transformation,[],[f99]) ).
fof(f286,plain,
( e0 != op(e3,e3)
| ~ sP56 ),
inference(cnf_transformation,[],[f100]) ).
fof(f289,plain,
( e2 != op(e3,e4)
| ~ sP55 ),
inference(cnf_transformation,[],[f101]) ).
fof(f294,plain,
( e2 != op(e4,e0)
| ~ sP54 ),
inference(cnf_transformation,[],[f102]) ).
fof(f301,plain,
( e0 != op(e4,e1)
| ~ sP53 ),
inference(cnf_transformation,[],[f103]) ).
fof(f302,plain,
( e4 != op(e4,e2)
| ~ sP52 ),
inference(cnf_transformation,[],[f104]) ).
fof(f308,plain,
( e3 != op(e4,e3)
| ~ sP51 ),
inference(cnf_transformation,[],[f105]) ).
fof(f315,plain,
( e1 != op(e4,e4)
| ~ sP50 ),
inference(cnf_transformation,[],[f106]) ).
fof(f319,plain,
( e0 != op(e0,e2)
| ~ sP49 ),
inference(cnf_transformation,[],[f107]) ).
fof(f325,plain,
( e0 != op(e1,e0)
| ~ sP48 ),
inference(cnf_transformation,[],[f108]) ).
fof(f328,plain,
( e1 != op(e0,e3)
| ~ sP47 ),
inference(cnf_transformation,[],[f109]) ).
fof(f334,plain,
( e1 != op(e2,e0)
| ~ sP46 ),
inference(cnf_transformation,[],[f110]) ).
fof(f340,plain,
( e2 != op(e0,e1)
| ~ sP45 ),
inference(cnf_transformation,[],[f111]) ).
fof(f342,plain,
( e2 != op(e4,e0)
| ~ sP44 ),
inference(cnf_transformation,[],[f112]) ).
fof(f351,plain,
( e3 != op(e0,e0)
| ~ sP43 ),
inference(cnf_transformation,[],[f113]) ).
fof(f356,plain,
( e3 != op(e0,e0)
| ~ sP42 ),
inference(cnf_transformation,[],[f114]) ).
fof(f357,plain,
( e4 != op(e0,e4)
| ~ sP41 ),
inference(cnf_transformation,[],[f115]) ).
fof(f363,plain,
( e4 != op(e3,e0)
| ~ sP40 ),
inference(cnf_transformation,[],[f116]) ).
fof(f371,plain,
( e0 != op(e1,e0)
| ~ sP39 ),
inference(cnf_transformation,[],[f117]) ).
fof(f372,plain,
( e0 != op(e4,e1)
| ~ sP38 ),
inference(cnf_transformation,[],[f118]) ).
fof(f379,plain,
( e1 != op(e1,e2)
| ~ sP37 ),
inference(cnf_transformation,[],[f119]) ).
fof(f383,plain,
( e1 != op(e3,e1)
| ~ sP36 ),
inference(cnf_transformation,[],[f120]) ).
fof(f388,plain,
( e2 != op(e1,e3)
| ~ sP35 ),
inference(cnf_transformation,[],[f121]) ).
fof(f396,plain,
( e2 != op(e0,e1)
| ~ sP34 ),
inference(cnf_transformation,[],[f122]) ).
fof(f397,plain,
( e3 != op(e1,e4)
| ~ sP33 ),
inference(cnf_transformation,[],[f123]) ).
fof(f404,plain,
( e3 != op(e2,e1)
| ~ sP32 ),
inference(cnf_transformation,[],[f124]) ).
fof(f410,plain,
( e4 != op(e1,e1)
| ~ sP31 ),
inference(cnf_transformation,[],[f125]) ).
fof(f415,plain,
( e4 != op(e1,e1)
| ~ sP30 ),
inference(cnf_transformation,[],[f126]) ).
fof(f417,plain,
( e0 != op(e2,e4)
| ~ sP29 ),
inference(cnf_transformation,[],[f127]) ).
fof(f426,plain,
( e0 != op(e0,e2)
| ~ sP28 ),
inference(cnf_transformation,[],[f128]) ).
fof(f431,plain,
( e1 != op(e2,e0)
| ~ sP27 ),
inference(cnf_transformation,[],[f129]) ).
fof(f435,plain,
( e1 != op(e1,e2)
| ~ sP26 ),
inference(cnf_transformation,[],[f130]) ).
fof(f439,plain,
( e2 != op(e2,e2)
| ~ sP25 ),
inference(cnf_transformation,[],[f131]) ).
fof(f444,plain,
( e2 != op(e2,e2)
| ~ sP24 ),
inference(cnf_transformation,[],[f132]) ).
fof(f450,plain,
( e3 != op(e2,e1)
| ~ sP23 ),
inference(cnf_transformation,[],[f133]) ).
fof(f453,plain,
( e3 != op(e3,e2)
| ~ sP22 ),
inference(cnf_transformation,[],[f134]) ).
fof(f458,plain,
( e4 != op(e2,e3)
| ~ sP21 ),
inference(cnf_transformation,[],[f135]) ).
fof(f462,plain,
( e4 != op(e4,e2)
| ~ sP20 ),
inference(cnf_transformation,[],[f136]) ).
fof(f468,plain,
( e0 != op(e3,e3)
| ~ sP19 ),
inference(cnf_transformation,[],[f137]) ).
fof(f473,plain,
( e0 != op(e3,e3)
| ~ sP18 ),
inference(cnf_transformation,[],[f138]) ).
fof(f480,plain,
( e1 != op(e3,e1)
| ~ sP17 ),
inference(cnf_transformation,[],[f139]) ).
fof(f486,plain,
( e1 != op(e0,e3)
| ~ sP16 ),
inference(cnf_transformation,[],[f140]) ).
fof(f487,plain,
( e2 != op(e3,e4)
| ~ sP15 ),
inference(cnf_transformation,[],[f141]) ).
fof(f495,plain,
( e2 != op(e1,e3)
| ~ sP14 ),
inference(cnf_transformation,[],[f142]) ).
fof(f499,plain,
( e3 != op(e3,e2)
| ~ sP13 ),
inference(cnf_transformation,[],[f143]) ).
fof(f502,plain,
( e3 != op(e4,e3)
| ~ sP12 ),
inference(cnf_transformation,[],[f144]) ).
fof(f511,plain,
( e4 != op(e3,e0)
| ~ sP11 ),
inference(cnf_transformation,[],[f145]) ).
fof(f514,plain,
( e4 != op(e2,e3)
| ~ sP10 ),
inference(cnf_transformation,[],[f146]) ).
fof(f520,plain,
( e0 != op(e4,e1)
| ~ sP9 ),
inference(cnf_transformation,[],[f147]) ).
fof(f524,plain,
( e0 != op(e2,e4)
| ~ sP8 ),
inference(cnf_transformation,[],[f148]) ).
fof(f527,plain,
( e1 != op(e4,e4)
| ~ sP7 ),
inference(cnf_transformation,[],[f149]) ).
fof(f532,plain,
( e1 != op(e4,e4)
| ~ sP6 ),
inference(cnf_transformation,[],[f150]) ).
fof(f541,plain,
( e2 != op(e4,e0)
| ~ sP5 ),
inference(cnf_transformation,[],[f151]) ).
fof(f543,plain,
( e2 != op(e3,e4)
| ~ sP4 ),
inference(cnf_transformation,[],[f152]) ).
fof(f548,plain,
( e3 != op(e4,e3)
| ~ sP3 ),
inference(cnf_transformation,[],[f153]) ).
fof(f555,plain,
( e3 != op(e1,e4)
| ~ sP2 ),
inference(cnf_transformation,[],[f154]) ).
fof(f559,plain,
( e4 != op(e4,e2)
| ~ sP1 ),
inference(cnf_transformation,[],[f155]) ).
fof(f566,plain,
( e4 != op(e0,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f156]) ).
fof(f567,plain,
( e0 = op(e0,e4)
| e1 = op(e1,e4)
| e2 = op(e2,e4)
| e3 = op(e3,e4)
| e4 = op(e4,e4)
| 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
| 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
| 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
| e0 != op(op(e0,e0),op(e0,e0))
| e0 != op(op(e1,e0),op(e0,e1))
| e0 != op(op(e2,e0),op(e0,e2))
| e0 != op(op(e3,e0),op(e0,e3))
| e0 != op(op(e4,e0),op(e0,e4))
| e1 != op(op(e0,e1),op(e1,e0))
| e1 != op(op(e1,e1),op(e1,e1))
| e1 != op(op(e2,e1),op(e1,e2))
| e1 != op(op(e3,e1),op(e1,e3))
| e1 != op(op(e4,e1),op(e1,e4))
| e2 != op(op(e0,e2),op(e2,e0))
| e2 != op(op(e1,e2),op(e2,e1))
| e2 != op(op(e2,e2),op(e2,e2))
| e2 != op(op(e3,e2),op(e2,e3))
| e2 != op(op(e4,e2),op(e2,e4))
| e3 != op(op(e0,e3),op(e3,e0))
| e3 != op(op(e1,e3),op(e3,e1))
| e3 != op(op(e2,e3),op(e3,e2))
| e3 != op(op(e3,e3),op(e3,e3))
| e3 != op(op(e4,e3),op(e3,e4))
| e4 != op(op(e0,e4),op(e4,e0))
| e4 != op(op(e1,e4),op(e4,e1))
| e4 != op(op(e2,e4),op(e4,e2))
| e4 != op(op(e3,e4),op(e4,e3))
| e4 != op(op(e4,e4),op(e4,e4)) ),
inference(cnf_transformation,[],[f81]) ).
fof(f573,definition,
( spl75_1
<=> e4 = op(op(e4,e4),op(e4,e4)) ),
introduced(definition,[new_symbols(definition,[spl75_1])],[avatar_definition]) ).
fof(f575,plain,
( e4 != op(op(e4,e4),op(e4,e4))
| spl75_1 ),
inference(avatar_component_clause,[],[f573]) ).
fof(f577,definition,
( spl75_2
<=> e4 = op(op(e3,e4),op(e4,e3)) ),
introduced(definition,[new_symbols(definition,[spl75_2])],[avatar_definition]) ).
fof(f579,plain,
( e4 != op(op(e3,e4),op(e4,e3))
| spl75_2 ),
inference(avatar_component_clause,[],[f577]) ).
fof(f581,definition,
( spl75_3
<=> e4 = op(op(e2,e4),op(e4,e2)) ),
introduced(definition,[new_symbols(definition,[spl75_3])],[avatar_definition]) ).
fof(f583,plain,
( e4 != op(op(e2,e4),op(e4,e2))
| spl75_3 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f585,definition,
( spl75_4
<=> e4 = op(op(e1,e4),op(e4,e1)) ),
introduced(definition,[new_symbols(definition,[spl75_4])],[avatar_definition]) ).
fof(f587,plain,
( e4 != op(op(e1,e4),op(e4,e1))
| spl75_4 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f589,definition,
( spl75_5
<=> e4 = op(op(e0,e4),op(e4,e0)) ),
introduced(definition,[new_symbols(definition,[spl75_5])],[avatar_definition]) ).
fof(f591,plain,
( e4 != op(op(e0,e4),op(e4,e0))
| spl75_5 ),
inference(avatar_component_clause,[],[f589]) ).
fof(f593,definition,
( spl75_6
<=> e3 = op(op(e4,e3),op(e3,e4)) ),
introduced(definition,[new_symbols(definition,[spl75_6])],[avatar_definition]) ).
fof(f595,plain,
( e3 != op(op(e4,e3),op(e3,e4))
| spl75_6 ),
inference(avatar_component_clause,[],[f593]) ).
fof(f597,definition,
( spl75_7
<=> e3 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl75_7])],[avatar_definition]) ).
fof(f599,plain,
( e3 != op(op(e3,e3),op(e3,e3))
| spl75_7 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f601,definition,
( spl75_8
<=> e3 = op(op(e2,e3),op(e3,e2)) ),
introduced(definition,[new_symbols(definition,[spl75_8])],[avatar_definition]) ).
fof(f603,plain,
( e3 != op(op(e2,e3),op(e3,e2))
| spl75_8 ),
inference(avatar_component_clause,[],[f601]) ).
fof(f605,definition,
( spl75_9
<=> e3 = op(op(e1,e3),op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl75_9])],[avatar_definition]) ).
fof(f607,plain,
( e3 != op(op(e1,e3),op(e3,e1))
| spl75_9 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f609,definition,
( spl75_10
<=> e3 = op(op(e0,e3),op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl75_10])],[avatar_definition]) ).
fof(f611,plain,
( e3 != op(op(e0,e3),op(e3,e0))
| spl75_10 ),
inference(avatar_component_clause,[],[f609]) ).
fof(f613,definition,
( spl75_11
<=> e2 = op(op(e4,e2),op(e2,e4)) ),
introduced(definition,[new_symbols(definition,[spl75_11])],[avatar_definition]) ).
fof(f615,plain,
( e2 != op(op(e4,e2),op(e2,e4))
| spl75_11 ),
inference(avatar_component_clause,[],[f613]) ).
fof(f617,definition,
( spl75_12
<=> e2 = op(op(e3,e2),op(e2,e3)) ),
introduced(definition,[new_symbols(definition,[spl75_12])],[avatar_definition]) ).
fof(f619,plain,
( e2 != op(op(e3,e2),op(e2,e3))
| spl75_12 ),
inference(avatar_component_clause,[],[f617]) ).
fof(f621,definition,
( spl75_13
<=> e2 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl75_13])],[avatar_definition]) ).
fof(f623,plain,
( e2 != op(op(e2,e2),op(e2,e2))
| spl75_13 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f625,definition,
( spl75_14
<=> e2 = op(op(e1,e2),op(e2,e1)) ),
introduced(definition,[new_symbols(definition,[spl75_14])],[avatar_definition]) ).
fof(f627,plain,
( e2 != op(op(e1,e2),op(e2,e1))
| spl75_14 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f629,definition,
( spl75_15
<=> e2 = op(op(e0,e2),op(e2,e0)) ),
introduced(definition,[new_symbols(definition,[spl75_15])],[avatar_definition]) ).
fof(f631,plain,
( e2 != op(op(e0,e2),op(e2,e0))
| spl75_15 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f633,definition,
( spl75_16
<=> e1 = op(op(e4,e1),op(e1,e4)) ),
introduced(definition,[new_symbols(definition,[spl75_16])],[avatar_definition]) ).
fof(f635,plain,
( e1 != op(op(e4,e1),op(e1,e4))
| spl75_16 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f637,definition,
( spl75_17
<=> e1 = op(op(e3,e1),op(e1,e3)) ),
introduced(definition,[new_symbols(definition,[spl75_17])],[avatar_definition]) ).
fof(f639,plain,
( e1 != op(op(e3,e1),op(e1,e3))
| spl75_17 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f641,definition,
( spl75_18
<=> e1 = op(op(e2,e1),op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl75_18])],[avatar_definition]) ).
fof(f643,plain,
( e1 != op(op(e2,e1),op(e1,e2))
| spl75_18 ),
inference(avatar_component_clause,[],[f641]) ).
fof(f645,definition,
( spl75_19
<=> e1 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl75_19])],[avatar_definition]) ).
fof(f647,plain,
( e1 != op(op(e1,e1),op(e1,e1))
| spl75_19 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f649,definition,
( spl75_20
<=> e1 = op(op(e0,e1),op(e1,e0)) ),
introduced(definition,[new_symbols(definition,[spl75_20])],[avatar_definition]) ).
fof(f651,plain,
( e1 != op(op(e0,e1),op(e1,e0))
| spl75_20 ),
inference(avatar_component_clause,[],[f649]) ).
fof(f653,definition,
( spl75_21
<=> e0 = op(op(e4,e0),op(e0,e4)) ),
introduced(definition,[new_symbols(definition,[spl75_21])],[avatar_definition]) ).
fof(f655,plain,
( e0 != op(op(e4,e0),op(e0,e4))
| spl75_21 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f657,definition,
( spl75_22
<=> e0 = op(op(e3,e0),op(e0,e3)) ),
introduced(definition,[new_symbols(definition,[spl75_22])],[avatar_definition]) ).
fof(f659,plain,
( e0 != op(op(e3,e0),op(e0,e3))
| spl75_22 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f661,definition,
( spl75_23
<=> e0 = op(op(e2,e0),op(e0,e2)) ),
introduced(definition,[new_symbols(definition,[spl75_23])],[avatar_definition]) ).
fof(f663,plain,
( e0 != op(op(e2,e0),op(e0,e2))
| spl75_23 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f665,definition,
( spl75_24
<=> e0 = op(op(e1,e0),op(e0,e1)) ),
introduced(definition,[new_symbols(definition,[spl75_24])],[avatar_definition]) ).
fof(f667,plain,
( e0 != op(op(e1,e0),op(e0,e1))
| spl75_24 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f669,definition,
( spl75_25
<=> e0 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl75_25])],[avatar_definition]) ).
fof(f671,plain,
( e0 != op(op(e0,e0),op(e0,e0))
| spl75_25 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f673,definition,
( spl75_26
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl75_26])],[avatar_definition]) ).
fof(f677,definition,
( spl75_27
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl75_27])],[avatar_definition]) ).
fof(f681,definition,
( spl75_28
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl75_28])],[avatar_definition]) ).
fof(f685,definition,
( spl75_29
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl75_29])],[avatar_definition]) ).
fof(f689,definition,
( spl75_30
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl75_30])],[avatar_definition]) ).
fof(f693,definition,
( spl75_31
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl75_31])],[avatar_definition]) ).
fof(f697,definition,
( spl75_32
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl75_32])],[avatar_definition]) ).
fof(f701,definition,
( spl75_33
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl75_33])],[avatar_definition]) ).
fof(f705,definition,
( spl75_34
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl75_34])],[avatar_definition]) ).
fof(f709,definition,
( spl75_35
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl75_35])],[avatar_definition]) ).
fof(f713,definition,
( spl75_36
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl75_36])],[avatar_definition]) ).
fof(f717,definition,
( spl75_37
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl75_37])],[avatar_definition]) ).
fof(f721,definition,
( spl75_38
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl75_38])],[avatar_definition]) ).
fof(f725,definition,
( spl75_39
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl75_39])],[avatar_definition]) ).
fof(f729,definition,
( spl75_40
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl75_40])],[avatar_definition]) ).
fof(f733,definition,
( spl75_41
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl75_41])],[avatar_definition]) ).
fof(f737,definition,
( spl75_42
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl75_42])],[avatar_definition]) ).
fof(f741,definition,
( spl75_43
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl75_43])],[avatar_definition]) ).
fof(f745,definition,
( spl75_44
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl75_44])],[avatar_definition]) ).
fof(f749,definition,
( spl75_45
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl75_45])],[avatar_definition]) ).
fof(f753,definition,
( spl75_46
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl75_46])],[avatar_definition]) ).
fof(f757,definition,
( spl75_47
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl75_47])],[avatar_definition]) ).
fof(f761,definition,
( spl75_48
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl75_48])],[avatar_definition]) ).
fof(f765,definition,
( spl75_49
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl75_49])],[avatar_definition]) ).
fof(f769,definition,
( spl75_50
<=> sP24 ),
introduced(definition,[new_symbols(definition,[spl75_50])],[avatar_definition]) ).
fof(f773,definition,
( spl75_51
<=> sP25 ),
introduced(definition,[new_symbols(definition,[spl75_51])],[avatar_definition]) ).
fof(f777,definition,
( spl75_52
<=> sP26 ),
introduced(definition,[new_symbols(definition,[spl75_52])],[avatar_definition]) ).
fof(f781,definition,
( spl75_53
<=> sP27 ),
introduced(definition,[new_symbols(definition,[spl75_53])],[avatar_definition]) ).
fof(f785,definition,
( spl75_54
<=> sP28 ),
introduced(definition,[new_symbols(definition,[spl75_54])],[avatar_definition]) ).
fof(f789,definition,
( spl75_55
<=> sP29 ),
introduced(definition,[new_symbols(definition,[spl75_55])],[avatar_definition]) ).
fof(f793,definition,
( spl75_56
<=> sP30 ),
introduced(definition,[new_symbols(definition,[spl75_56])],[avatar_definition]) ).
fof(f797,definition,
( spl75_57
<=> sP31 ),
introduced(definition,[new_symbols(definition,[spl75_57])],[avatar_definition]) ).
fof(f801,definition,
( spl75_58
<=> sP32 ),
introduced(definition,[new_symbols(definition,[spl75_58])],[avatar_definition]) ).
fof(f805,definition,
( spl75_59
<=> sP33 ),
introduced(definition,[new_symbols(definition,[spl75_59])],[avatar_definition]) ).
fof(f809,definition,
( spl75_60
<=> sP34 ),
introduced(definition,[new_symbols(definition,[spl75_60])],[avatar_definition]) ).
fof(f813,definition,
( spl75_61
<=> sP35 ),
introduced(definition,[new_symbols(definition,[spl75_61])],[avatar_definition]) ).
fof(f817,definition,
( spl75_62
<=> sP36 ),
introduced(definition,[new_symbols(definition,[spl75_62])],[avatar_definition]) ).
fof(f821,definition,
( spl75_63
<=> sP37 ),
introduced(definition,[new_symbols(definition,[spl75_63])],[avatar_definition]) ).
fof(f825,definition,
( spl75_64
<=> sP38 ),
introduced(definition,[new_symbols(definition,[spl75_64])],[avatar_definition]) ).
fof(f829,definition,
( spl75_65
<=> sP39 ),
introduced(definition,[new_symbols(definition,[spl75_65])],[avatar_definition]) ).
fof(f833,definition,
( spl75_66
<=> sP40 ),
introduced(definition,[new_symbols(definition,[spl75_66])],[avatar_definition]) ).
fof(f837,definition,
( spl75_67
<=> sP41 ),
introduced(definition,[new_symbols(definition,[spl75_67])],[avatar_definition]) ).
fof(f841,definition,
( spl75_68
<=> sP42 ),
introduced(definition,[new_symbols(definition,[spl75_68])],[avatar_definition]) ).
fof(f845,definition,
( spl75_69
<=> sP43 ),
introduced(definition,[new_symbols(definition,[spl75_69])],[avatar_definition]) ).
fof(f849,definition,
( spl75_70
<=> sP44 ),
introduced(definition,[new_symbols(definition,[spl75_70])],[avatar_definition]) ).
fof(f853,definition,
( spl75_71
<=> sP45 ),
introduced(definition,[new_symbols(definition,[spl75_71])],[avatar_definition]) ).
fof(f857,definition,
( spl75_72
<=> sP46 ),
introduced(definition,[new_symbols(definition,[spl75_72])],[avatar_definition]) ).
fof(f861,definition,
( spl75_73
<=> sP47 ),
introduced(definition,[new_symbols(definition,[spl75_73])],[avatar_definition]) ).
fof(f865,definition,
( spl75_74
<=> sP48 ),
introduced(definition,[new_symbols(definition,[spl75_74])],[avatar_definition]) ).
fof(f869,definition,
( spl75_75
<=> sP49 ),
introduced(definition,[new_symbols(definition,[spl75_75])],[avatar_definition]) ).
fof(f873,definition,
( spl75_76
<=> sP50 ),
introduced(definition,[new_symbols(definition,[spl75_76])],[avatar_definition]) ).
fof(f877,definition,
( spl75_77
<=> sP51 ),
introduced(definition,[new_symbols(definition,[spl75_77])],[avatar_definition]) ).
fof(f881,definition,
( spl75_78
<=> sP52 ),
introduced(definition,[new_symbols(definition,[spl75_78])],[avatar_definition]) ).
fof(f885,definition,
( spl75_79
<=> sP53 ),
introduced(definition,[new_symbols(definition,[spl75_79])],[avatar_definition]) ).
fof(f889,definition,
( spl75_80
<=> sP54 ),
introduced(definition,[new_symbols(definition,[spl75_80])],[avatar_definition]) ).
fof(f893,definition,
( spl75_81
<=> sP55 ),
introduced(definition,[new_symbols(definition,[spl75_81])],[avatar_definition]) ).
fof(f897,definition,
( spl75_82
<=> sP56 ),
introduced(definition,[new_symbols(definition,[spl75_82])],[avatar_definition]) ).
fof(f901,definition,
( spl75_83
<=> sP57 ),
introduced(definition,[new_symbols(definition,[spl75_83])],[avatar_definition]) ).
fof(f905,definition,
( spl75_84
<=> sP58 ),
introduced(definition,[new_symbols(definition,[spl75_84])],[avatar_definition]) ).
fof(f909,definition,
( spl75_85
<=> sP59 ),
introduced(definition,[new_symbols(definition,[spl75_85])],[avatar_definition]) ).
fof(f913,definition,
( spl75_86
<=> sP60 ),
introduced(definition,[new_symbols(definition,[spl75_86])],[avatar_definition]) ).
fof(f917,definition,
( spl75_87
<=> sP61 ),
introduced(definition,[new_symbols(definition,[spl75_87])],[avatar_definition]) ).
fof(f921,definition,
( spl75_88
<=> sP62 ),
introduced(definition,[new_symbols(definition,[spl75_88])],[avatar_definition]) ).
fof(f925,definition,
( spl75_89
<=> sP63 ),
introduced(definition,[new_symbols(definition,[spl75_89])],[avatar_definition]) ).
fof(f929,definition,
( spl75_90
<=> sP64 ),
introduced(definition,[new_symbols(definition,[spl75_90])],[avatar_definition]) ).
fof(f933,definition,
( spl75_91
<=> sP65 ),
introduced(definition,[new_symbols(definition,[spl75_91])],[avatar_definition]) ).
fof(f937,definition,
( spl75_92
<=> sP66 ),
introduced(definition,[new_symbols(definition,[spl75_92])],[avatar_definition]) ).
fof(f941,definition,
( spl75_93
<=> sP67 ),
introduced(definition,[new_symbols(definition,[spl75_93])],[avatar_definition]) ).
fof(f945,definition,
( spl75_94
<=> sP68 ),
introduced(definition,[new_symbols(definition,[spl75_94])],[avatar_definition]) ).
fof(f949,definition,
( spl75_95
<=> sP69 ),
introduced(definition,[new_symbols(definition,[spl75_95])],[avatar_definition]) ).
fof(f953,definition,
( spl75_96
<=> sP70 ),
introduced(definition,[new_symbols(definition,[spl75_96])],[avatar_definition]) ).
fof(f957,definition,
( spl75_97
<=> sP71 ),
introduced(definition,[new_symbols(definition,[spl75_97])],[avatar_definition]) ).
fof(f961,definition,
( spl75_98
<=> sP72 ),
introduced(definition,[new_symbols(definition,[spl75_98])],[avatar_definition]) ).
fof(f965,definition,
( spl75_99
<=> sP73 ),
introduced(definition,[new_symbols(definition,[spl75_99])],[avatar_definition]) ).
fof(f969,definition,
( spl75_100
<=> sP74 ),
introduced(definition,[new_symbols(definition,[spl75_100])],[avatar_definition]) ).
fof(f973,definition,
( spl75_101
<=> e4 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl75_101])],[avatar_definition]) ).
fof(f975,plain,
( e4 = op(e4,e4)
| ~ spl75_101 ),
inference(avatar_component_clause,[],[f973]) ).
fof(f977,definition,
( spl75_102
<=> e3 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl75_102])],[avatar_definition]) ).
fof(f979,plain,
( e3 = op(e3,e4)
| ~ spl75_102 ),
inference(avatar_component_clause,[],[f977]) ).
fof(f981,definition,
( spl75_103
<=> e2 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl75_103])],[avatar_definition]) ).
fof(f983,plain,
( e2 = op(e2,e4)
| ~ spl75_103 ),
inference(avatar_component_clause,[],[f981]) ).
fof(f985,definition,
( spl75_104
<=> e1 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl75_104])],[avatar_definition]) ).
fof(f987,plain,
( e1 = op(e1,e4)
| ~ spl75_104 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f989,definition,
( spl75_105
<=> e0 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl75_105])],[avatar_definition]) ).
fof(f991,plain,
( e0 = op(e0,e4)
| ~ spl75_105 ),
inference(avatar_component_clause,[],[f989]) ).
fof(f992,plain,
( ~ spl75_1
| ~ spl75_2
| ~ spl75_3
| ~ spl75_4
| ~ spl75_5
| ~ spl75_6
| ~ spl75_7
| ~ spl75_8
| ~ spl75_9
| ~ spl75_10
| ~ spl75_11
| ~ spl75_12
| ~ spl75_13
| ~ spl75_14
| ~ spl75_15
| ~ spl75_16
| ~ spl75_17
| ~ spl75_18
| ~ spl75_19
| ~ spl75_20
| ~ spl75_21
| ~ spl75_22
| ~ spl75_23
| ~ spl75_24
| ~ spl75_25
| spl75_26
| spl75_27
| spl75_28
| spl75_29
| spl75_30
| spl75_31
| spl75_32
| spl75_33
| spl75_34
| spl75_35
| spl75_36
| spl75_37
| spl75_38
| spl75_39
| spl75_40
| spl75_41
| spl75_42
| spl75_43
| spl75_44
| spl75_45
| spl75_46
| spl75_47
| spl75_48
| spl75_49
| spl75_50
| spl75_51
| spl75_52
| spl75_53
| spl75_54
| spl75_55
| spl75_56
| spl75_57
| spl75_58
| spl75_59
| spl75_60
| spl75_61
| spl75_62
| spl75_63
| spl75_64
| spl75_65
| spl75_66
| spl75_67
| spl75_68
| spl75_69
| spl75_70
| spl75_71
| spl75_72
| spl75_73
| spl75_74
| spl75_75
| spl75_76
| spl75_77
| spl75_78
| spl75_79
| spl75_80
| spl75_81
| spl75_82
| spl75_83
| spl75_84
| spl75_85
| spl75_86
| spl75_87
| spl75_88
| spl75_89
| spl75_90
| spl75_91
| spl75_92
| spl75_93
| spl75_94
| spl75_95
| spl75_96
| spl75_97
| spl75_98
| spl75_99
| spl75_100
| spl75_101
| spl75_102
| spl75_103
| spl75_104
| spl75_105 ),
inference(avatar_split_clause,[],[f567,f989,f985,f981,f977,f973,f969,f965,f961,f957,f953,f949,f945,f941,f937,f933,f929,f925,f921,f917,f913,f909,f905,f901,f897,f893,f889,f885,f881,f877,f873,f869,f865,f861,f857,f853,f849,f845,f841,f837,f833,f829,f825,f821,f817,f813,f809,f805,f801,f797,f793,f789,f785,f781,f777,f773,f769,f765,f761,f757,f753,f749,f745,f741,f737,f733,f729,f725,f721,f717,f713,f709,f705,f701,f697,f693,f689,f685,f681,f677,f673,f669,f665,f661,f657,f653,f649,f645,f641,f637,f633,f629,f625,f621,f617,f613,f609,f605,f601,f597,f593,f589,f585,f581,f577,f573]) ).
fof(f1015,definition,
( spl75_111
<=> e4 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl75_111])],[avatar_definition]) ).
fof(f1017,plain,
( e4 = op(e4,e2)
| ~ spl75_111 ),
inference(avatar_component_clause,[],[f1015]) ).
fof(f1019,definition,
( spl75_112
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl75_112])],[avatar_definition]) ).
fof(f1021,plain,
( e3 = op(e3,e2)
| ~ spl75_112 ),
inference(avatar_component_clause,[],[f1019]) ).
fof(f1023,definition,
( spl75_113
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl75_113])],[avatar_definition]) ).
fof(f1025,plain,
( e2 = op(e2,e2)
| ~ spl75_113 ),
inference(avatar_component_clause,[],[f1023]) ).
fof(f1027,definition,
( spl75_114
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl75_114])],[avatar_definition]) ).
fof(f1029,plain,
( e1 = op(e1,e2)
| ~ spl75_114 ),
inference(avatar_component_clause,[],[f1027]) ).
fof(f1031,definition,
( spl75_115
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl75_115])],[avatar_definition]) ).
fof(f1033,plain,
( e0 = op(e0,e2)
| ~ spl75_115 ),
inference(avatar_component_clause,[],[f1031]) ).
fof(f1094,definition,
( spl75_129
<=> e4 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl75_129])],[avatar_definition]) ).
fof(f1095,plain,
( e4 = op(e0,e4)
| ~ spl75_129 ),
inference(avatar_component_clause,[],[f1094]) ).
fof(f1097,plain,
( ~ spl75_26
| ~ spl75_129 ),
inference(avatar_split_clause,[],[f566,f1094,f673]) ).
fof(f1100,plain,
( ~ spl75_27
| ~ spl75_111 ),
inference(avatar_split_clause,[],[f559,f1015,f677]) ).
fof(f1115,definition,
( spl75_132
<=> e3 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl75_132])],[avatar_definition]) ).
fof(f1116,plain,
( e3 = op(e1,e4)
| ~ spl75_132 ),
inference(avatar_component_clause,[],[f1115]) ).
fof(f1118,plain,
( ~ spl75_28
| ~ spl75_132 ),
inference(avatar_split_clause,[],[f555,f1115,f681]) ).
fof(f1126,definition,
( spl75_134
<=> e3 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl75_134])],[avatar_definition]) ).
fof(f1127,plain,
( e3 = op(e4,e3)
| ~ spl75_134 ),
inference(avatar_component_clause,[],[f1126]) ).
fof(f1129,plain,
( ~ spl75_29
| ~ spl75_134 ),
inference(avatar_split_clause,[],[f548,f1126,f685]) ).
fof(f1151,definition,
( spl75_139
<=> e2 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl75_139])],[avatar_definition]) ).
fof(f1152,plain,
( e2 = op(e3,e4)
| ~ spl75_139 ),
inference(avatar_component_clause,[],[f1151]) ).
fof(f1154,plain,
( ~ spl75_30
| ~ spl75_139 ),
inference(avatar_split_clause,[],[f543,f1151,f689]) ).
fof(f1183,definition,
( spl75_145
<=> e2 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl75_145])],[avatar_definition]) ).
fof(f1184,plain,
( e2 = op(e4,e0)
| ~ spl75_145 ),
inference(avatar_component_clause,[],[f1183]) ).
fof(f1186,plain,
( ~ spl75_31
| ~ spl75_145 ),
inference(avatar_split_clause,[],[f541,f1183,f693]) ).
fof(f1188,definition,
( spl75_146
<=> e1 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl75_146])],[avatar_definition]) ).
fof(f1189,plain,
( e1 = op(e4,e4)
| ~ spl75_146 ),
inference(avatar_component_clause,[],[f1188]) ).
fof(f1191,plain,
( ~ spl75_32
| ~ spl75_146 ),
inference(avatar_split_clause,[],[f532,f1188,f697]) ).
fof(f1208,plain,
( ~ spl75_33
| ~ spl75_146 ),
inference(avatar_split_clause,[],[f527,f1188,f701]) ).
fof(f1240,definition,
( spl75_156
<=> e0 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl75_156])],[avatar_definition]) ).
fof(f1241,plain,
( e0 = op(e2,e4)
| ~ spl75_156 ),
inference(avatar_component_clause,[],[f1240]) ).
fof(f1243,plain,
( ~ spl75_34
| ~ spl75_156 ),
inference(avatar_split_clause,[],[f524,f1240,f705]) ).
fof(f1262,definition,
( spl75_160
<=> e0 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl75_160])],[avatar_definition]) ).
fof(f1263,plain,
( e0 = op(e4,e1)
| ~ spl75_160 ),
inference(avatar_component_clause,[],[f1262]) ).
fof(f1265,plain,
( ~ spl75_35
| ~ spl75_160 ),
inference(avatar_split_clause,[],[f520,f1262,f709]) ).
fof(f1278,definition,
( spl75_163
<=> e4 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl75_163])],[avatar_definition]) ).
fof(f1279,plain,
( e4 = op(e2,e3)
| ~ spl75_163 ),
inference(avatar_component_clause,[],[f1278]) ).
fof(f1281,plain,
( ~ spl75_36
| ~ spl75_163 ),
inference(avatar_split_clause,[],[f514,f1278,f713]) ).
fof(f1305,definition,
( spl75_168
<=> e4 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl75_168])],[avatar_definition]) ).
fof(f1306,plain,
( e4 = op(e3,e0)
| ~ spl75_168 ),
inference(avatar_component_clause,[],[f1305]) ).
fof(f1308,plain,
( ~ spl75_37
| ~ spl75_168 ),
inference(avatar_split_clause,[],[f511,f1305,f717]) ).
fof(f1309,plain,
( ~ spl75_38
| ~ spl75_134 ),
inference(avatar_split_clause,[],[f502,f1126,f721]) ).
fof(f1328,plain,
( ~ spl75_39
| ~ spl75_112 ),
inference(avatar_split_clause,[],[f499,f1019,f725]) ).
fof(f1339,definition,
( spl75_173
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl75_173])],[avatar_definition]) ).
fof(f1340,plain,
( e2 = op(e1,e3)
| ~ spl75_173 ),
inference(avatar_component_clause,[],[f1339]) ).
fof(f1342,plain,
( ~ spl75_40
| ~ spl75_173 ),
inference(avatar_split_clause,[],[f495,f1339,f729]) ).
fof(f1348,plain,
( ~ spl75_41
| ~ spl75_139 ),
inference(avatar_split_clause,[],[f487,f1151,f733]) ).
fof(f1378,definition,
( spl75_180
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl75_180])],[avatar_definition]) ).
fof(f1379,plain,
( e1 = op(e0,e3)
| ~ spl75_180 ),
inference(avatar_component_clause,[],[f1378]) ).
fof(f1381,plain,
( ~ spl75_42
| ~ spl75_180 ),
inference(avatar_split_clause,[],[f486,f1378,f737]) ).
fof(f1390,definition,
( spl75_182
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl75_182])],[avatar_definition]) ).
fof(f1391,plain,
( e1 = op(e3,e1)
| ~ spl75_182 ),
inference(avatar_component_clause,[],[f1390]) ).
fof(f1393,plain,
( ~ spl75_43
| ~ spl75_182 ),
inference(avatar_split_clause,[],[f480,f1390,f741]) ).
fof(f1401,definition,
( spl75_184
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl75_184])],[avatar_definition]) ).
fof(f1402,plain,
( e0 = op(e3,e3)
| ~ spl75_184 ),
inference(avatar_component_clause,[],[f1401]) ).
fof(f1404,plain,
( ~ spl75_44
| ~ spl75_184 ),
inference(avatar_split_clause,[],[f473,f1401,f745]) ).
fof(f1417,plain,
( ~ spl75_45
| ~ spl75_184 ),
inference(avatar_split_clause,[],[f468,f1401,f749]) ).
fof(f1433,plain,
( ~ spl75_46
| ~ spl75_111 ),
inference(avatar_split_clause,[],[f462,f1015,f753]) ).
fof(f1451,plain,
( ~ spl75_47
| ~ spl75_163 ),
inference(avatar_split_clause,[],[f458,f1278,f757]) ).
fof(f1464,plain,
( ~ spl75_48
| ~ spl75_112 ),
inference(avatar_split_clause,[],[f453,f1019,f761]) ).
fof(f1484,definition,
( spl75_198
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl75_198])],[avatar_definition]) ).
fof(f1485,plain,
( e3 = op(e2,e1)
| ~ spl75_198 ),
inference(avatar_component_clause,[],[f1484]) ).
fof(f1487,plain,
( ~ spl75_49
| ~ spl75_198 ),
inference(avatar_split_clause,[],[f450,f1484,f765]) ).
fof(f1495,plain,
( ~ spl75_50
| ~ spl75_113 ),
inference(avatar_split_clause,[],[f444,f1023,f769]) ).
fof(f1508,plain,
( ~ spl75_51
| ~ spl75_113 ),
inference(avatar_split_clause,[],[f439,f1023,f773]) ).
fof(f1518,plain,
( ~ spl75_52
| ~ spl75_114 ),
inference(avatar_split_clause,[],[f435,f1027,f777]) ).
fof(f1533,definition,
( spl75_205
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl75_205])],[avatar_definition]) ).
fof(f1534,plain,
( e1 = op(e2,e0)
| ~ spl75_205 ),
inference(avatar_component_clause,[],[f1533]) ).
fof(f1536,plain,
( ~ spl75_53
| ~ spl75_205 ),
inference(avatar_split_clause,[],[f431,f1533,f781]) ).
fof(f1549,plain,
( ~ spl75_54
| ~ spl75_115 ),
inference(avatar_split_clause,[],[f426,f1031,f785]) ).
fof(f1550,plain,
( ~ spl75_55
| ~ spl75_156 ),
inference(avatar_split_clause,[],[f417,f1240,f789]) ).
fof(f1567,definition,
( spl75_210
<=> e4 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl75_210])],[avatar_definition]) ).
fof(f1568,plain,
( e4 = op(e1,e1)
| ~ spl75_210 ),
inference(avatar_component_clause,[],[f1567]) ).
fof(f1570,plain,
( ~ spl75_56
| ~ spl75_210 ),
inference(avatar_split_clause,[],[f415,f1567,f793]) ).
fof(f1579,plain,
( ~ spl75_57
| ~ spl75_210 ),
inference(avatar_split_clause,[],[f410,f1567,f797]) ).
fof(f1587,plain,
( ~ spl75_58
| ~ spl75_198 ),
inference(avatar_split_clause,[],[f404,f1484,f801]) ).
fof(f1598,plain,
( ~ spl75_59
| ~ spl75_132 ),
inference(avatar_split_clause,[],[f397,f1115,f805]) ).
fof(f1616,definition,
( spl75_217
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl75_217])],[avatar_definition]) ).
fof(f1617,plain,
( e2 = op(e0,e1)
| ~ spl75_217 ),
inference(avatar_component_clause,[],[f1616]) ).
fof(f1619,plain,
( ~ spl75_60
| ~ spl75_217 ),
inference(avatar_split_clause,[],[f396,f1616,f809]) ).
fof(f1621,plain,
( ~ spl75_61
| ~ spl75_173 ),
inference(avatar_split_clause,[],[f388,f1339,f813]) ).
fof(f1630,plain,
( ~ spl75_62
| ~ spl75_182 ),
inference(avatar_split_clause,[],[f383,f1390,f817]) ).
fof(f1640,plain,
( ~ spl75_63
| ~ spl75_114 ),
inference(avatar_split_clause,[],[f379,f1027,f821]) ).
fof(f1643,plain,
( ~ spl75_64
| ~ spl75_160 ),
inference(avatar_split_clause,[],[f372,f1262,f825]) ).
fof(f1657,definition,
( spl75_221
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl75_221])],[avatar_definition]) ).
fof(f1658,plain,
( e0 = op(e1,e0)
| ~ spl75_221 ),
inference(avatar_component_clause,[],[f1657]) ).
fof(f1660,plain,
( ~ spl75_65
| ~ spl75_221 ),
inference(avatar_split_clause,[],[f371,f1657,f829]) ).
fof(f1662,plain,
( ~ spl75_66
| ~ spl75_168 ),
inference(avatar_split_clause,[],[f363,f1305,f833]) ).
fof(f1670,plain,
( ~ spl75_67
| ~ spl75_129 ),
inference(avatar_split_clause,[],[f357,f1094,f837]) ).
fof(f1680,definition,
( spl75_223
<=> e3 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl75_223])],[avatar_definition]) ).
fof(f1681,plain,
( e3 = op(e0,e0)
| ~ spl75_223 ),
inference(avatar_component_clause,[],[f1680]) ).
fof(f1683,plain,
( ~ spl75_68
| ~ spl75_223 ),
inference(avatar_split_clause,[],[f356,f1680,f841]) ).
fof(f1688,plain,
( ~ spl75_69
| ~ spl75_223 ),
inference(avatar_split_clause,[],[f351,f1680,f845]) ).
fof(f1689,plain,
( ~ spl75_70
| ~ spl75_145 ),
inference(avatar_split_clause,[],[f342,f1183,f849]) ).
fof(f1701,plain,
( ~ spl75_71
| ~ spl75_217 ),
inference(avatar_split_clause,[],[f340,f1616,f853]) ).
fof(f1705,plain,
( ~ spl75_72
| ~ spl75_205 ),
inference(avatar_split_clause,[],[f334,f1533,f857]) ).
fof(f1713,plain,
( ~ spl75_73
| ~ spl75_180 ),
inference(avatar_split_clause,[],[f328,f1378,f861]) ).
fof(f1720,plain,
( ~ spl75_74
| ~ spl75_221 ),
inference(avatar_split_clause,[],[f325,f1657,f865]) ).
fof(f1724,plain,
( ~ spl75_75
| ~ spl75_115 ),
inference(avatar_split_clause,[],[f319,f1031,f869]) ).
fof(f1730,plain,
( ~ spl75_76
| ~ spl75_146 ),
inference(avatar_split_clause,[],[f315,f1188,f873]) ).
fof(f1733,plain,
( ~ spl75_77
| ~ spl75_134 ),
inference(avatar_split_clause,[],[f308,f1126,f877]) ).
fof(f1737,plain,
( ~ spl75_78
| ~ spl75_111 ),
inference(avatar_split_clause,[],[f302,f1015,f881]) ).
fof(f1746,plain,
( ~ spl75_79
| ~ spl75_160 ),
inference(avatar_split_clause,[],[f301,f1262,f885]) ).
fof(f1749,plain,
( ~ spl75_80
| ~ spl75_145 ),
inference(avatar_split_clause,[],[f294,f1183,f889]) ).
fof(f1754,plain,
( ~ spl75_81
| ~ spl75_139 ),
inference(avatar_split_clause,[],[f289,f1151,f893]) ).
fof(f1761,plain,
( ~ spl75_82
| ~ spl75_184 ),
inference(avatar_split_clause,[],[f286,f1401,f897]) ).
fof(f1763,plain,
( ~ spl75_83
| ~ spl75_112 ),
inference(avatar_split_clause,[],[f278,f1019,f901]) ).
fof(f1770,plain,
( ~ spl75_84
| ~ spl75_182 ),
inference(avatar_split_clause,[],[f275,f1390,f905]) ).
fof(f1772,plain,
( ~ spl75_85
| ~ spl75_168 ),
inference(avatar_split_clause,[],[f267,f1305,f909]) ).
fof(f1781,plain,
( ~ spl75_86
| ~ spl75_156 ),
inference(avatar_split_clause,[],[f266,f1240,f913]) ).
fof(f1782,plain,
( ~ spl75_87
| ~ spl75_163 ),
inference(avatar_split_clause,[],[f257,f1278,f917]) ).
fof(f1789,plain,
( ~ spl75_88
| ~ spl75_113 ),
inference(avatar_split_clause,[],[f254,f1023,f921]) ).
fof(f1793,plain,
( ~ spl75_89
| ~ spl75_198 ),
inference(avatar_split_clause,[],[f248,f1484,f925]) ).
fof(f1800,plain,
( ~ spl75_90
| ~ spl75_205 ),
inference(avatar_split_clause,[],[f245,f1533,f929]) ).
fof(f1803,plain,
( ~ spl75_91
| ~ spl75_132 ),
inference(avatar_split_clause,[],[f238,f1115,f933]) ).
fof(f1809,plain,
( ~ spl75_92
| ~ spl75_173 ),
inference(avatar_split_clause,[],[f234,f1339,f937]) ).
fof(f1815,plain,
( ~ spl75_93
| ~ spl75_114 ),
inference(avatar_split_clause,[],[f230,f1027,f941]) ).
fof(f1817,plain,
( ~ spl75_94
| ~ spl75_210 ),
inference(avatar_split_clause,[],[f222,f1567,f945]) ).
fof(f1826,plain,
( ~ spl75_95
| ~ spl75_221 ),
inference(avatar_split_clause,[],[f221,f1657,f949]) ).
fof(f1827,plain,
( ~ spl75_96
| ~ spl75_129 ),
inference(avatar_split_clause,[],[f212,f1094,f953]) ).
fof(f1835,plain,
( ~ spl75_97
| ~ spl75_180 ),
inference(avatar_split_clause,[],[f210,f1378,f957]) ).
fof(f1841,plain,
( ~ spl75_98
| ~ spl75_115 ),
inference(avatar_split_clause,[],[f206,f1031,f961]) ).
fof(f1844,plain,
( ~ spl75_99
| ~ spl75_217 ),
inference(avatar_split_clause,[],[f199,f1616,f965]) ).
fof(f1848,plain,
( ~ spl75_100
| ~ spl75_223 ),
inference(avatar_split_clause,[],[f193,f1680,f969]) ).
fof(f1852,plain,
spl75_146,
inference(avatar_split_clause,[],[f167,f1188]) ).
fof(f1853,plain,
spl75_134,
inference(avatar_split_clause,[],[f168,f1126]) ).
fof(f1854,plain,
spl75_111,
inference(avatar_split_clause,[],[f169,f1015]) ).
fof(f1855,plain,
spl75_160,
inference(avatar_split_clause,[],[f170,f1262]) ).
fof(f1856,plain,
spl75_145,
inference(avatar_split_clause,[],[f171,f1183]) ).
fof(f1857,plain,
spl75_139,
inference(avatar_split_clause,[],[f172,f1151]) ).
fof(f1858,plain,
spl75_184,
inference(avatar_split_clause,[],[f173,f1401]) ).
fof(f1859,plain,
spl75_112,
inference(avatar_split_clause,[],[f174,f1019]) ).
fof(f1860,plain,
spl75_182,
inference(avatar_split_clause,[],[f175,f1390]) ).
fof(f1861,plain,
spl75_168,
inference(avatar_split_clause,[],[f176,f1305]) ).
fof(f1862,plain,
spl75_156,
inference(avatar_split_clause,[],[f177,f1240]) ).
fof(f1863,plain,
spl75_163,
inference(avatar_split_clause,[],[f178,f1278]) ).
fof(f1864,plain,
spl75_113,
inference(avatar_split_clause,[],[f179,f1023]) ).
fof(f1865,plain,
spl75_198,
inference(avatar_split_clause,[],[f180,f1484]) ).
fof(f1866,plain,
spl75_205,
inference(avatar_split_clause,[],[f181,f1533]) ).
fof(f1867,plain,
spl75_132,
inference(avatar_split_clause,[],[f182,f1115]) ).
fof(f1868,plain,
spl75_173,
inference(avatar_split_clause,[],[f183,f1339]) ).
fof(f1869,plain,
spl75_114,
inference(avatar_split_clause,[],[f184,f1027]) ).
fof(f1870,plain,
spl75_210,
inference(avatar_split_clause,[],[f185,f1567]) ).
fof(f1871,plain,
spl75_221,
inference(avatar_split_clause,[],[f186,f1657]) ).
fof(f1872,plain,
spl75_129,
inference(avatar_split_clause,[],[f187,f1094]) ).
fof(f1873,plain,
spl75_180,
inference(avatar_split_clause,[],[f188,f1378]) ).
fof(f1874,plain,
spl75_115,
inference(avatar_split_clause,[],[f189,f1031]) ).
fof(f1875,plain,
spl75_217,
inference(avatar_split_clause,[],[f190,f1616]) ).
fof(f1876,plain,
spl75_223,
inference(avatar_split_clause,[],[f191,f1680]) ).
fof(f1877,plain,
( e4 != op(e1,e1)
| spl75_1
| ~ spl75_146 ),
inference(superposition,[],[f575,f1189]) ).
fof(f1878,plain,
( ~ spl75_210
| spl75_1
| ~ spl75_146 ),
inference(avatar_split_clause,[],[f1877,f1188,f573,f1567]) ).
fof(f1880,plain,
( e4 != op(op(e3,e4),e3)
| spl75_2
| ~ spl75_134 ),
inference(forward_demodulation,[],[f579,f1127]) ).
fof(f1882,plain,
( e4 != op(e2,e3)
| spl75_2
| ~ spl75_134
| ~ spl75_139 ),
inference(forward_demodulation,[],[f1880,f1152]) ).
fof(f1883,plain,
( ~ spl75_163
| spl75_2
| ~ spl75_134
| ~ spl75_139 ),
inference(avatar_split_clause,[],[f1882,f1151,f1126,f577,f1278]) ).
fof(f1885,plain,
( e4 != op(op(e2,e4),e4)
| spl75_3
| ~ spl75_111 ),
inference(forward_demodulation,[],[f583,f1017]) ).
fof(f1888,plain,
( e4 != op(e0,e4)
| spl75_3
| ~ spl75_111
| ~ spl75_156 ),
inference(superposition,[],[f1885,f1241]) ).
fof(f1889,plain,
( $false
| spl75_3
| ~ spl75_111
| ~ spl75_129
| ~ spl75_156 ),
inference(forward_subsumption_resolution,[],[f1888,f1095]) ).
fof(f1890,plain,
( spl75_3
| ~ spl75_111
| ~ spl75_129
| ~ spl75_156 ),
inference(avatar_contradiction_clause,[],[f1889]) ).
fof(f1892,plain,
( e4 != op(e3,op(e4,e1))
| spl75_4
| ~ spl75_132 ),
inference(forward_demodulation,[],[f587,f1116]) ).
fof(f1894,plain,
( e4 != op(e3,e0)
| spl75_4
| ~ spl75_132
| ~ spl75_160 ),
inference(superposition,[],[f1892,f1263]) ).
fof(f1895,plain,
( ~ spl75_168
| spl75_4
| ~ spl75_132
| ~ spl75_160 ),
inference(avatar_split_clause,[],[f1894,f1262,f1115,f585,f1305]) ).
fof(f1897,plain,
( e4 != op(op(e0,e4),e2)
| spl75_5
| ~ spl75_145 ),
inference(forward_demodulation,[],[f591,f1184]) ).
fof(f1899,plain,
( e4 != op(e4,e2)
| spl75_5
| ~ spl75_129
| ~ spl75_145 ),
inference(forward_demodulation,[],[f1897,f1095]) ).
fof(f1901,plain,
( $false
| spl75_5
| ~ spl75_111
| ~ spl75_129
| ~ spl75_145 ),
inference(forward_subsumption_resolution,[],[f1899,f1017]) ).
fof(f1902,plain,
( spl75_5
| ~ spl75_111
| ~ spl75_129
| ~ spl75_145 ),
inference(avatar_contradiction_clause,[],[f1901]) ).
fof(f1904,plain,
( e3 != op(op(e4,e3),e2)
| spl75_6
| ~ spl75_139 ),
inference(forward_demodulation,[],[f595,f1152]) ).
fof(f1906,plain,
( e3 != op(e3,e2)
| spl75_6
| ~ spl75_134
| ~ spl75_139 ),
inference(forward_demodulation,[],[f1904,f1127]) ).
fof(f1907,plain,
( $false
| spl75_6
| ~ spl75_112
| ~ spl75_134
| ~ spl75_139 ),
inference(forward_subsumption_resolution,[],[f1906,f1021]) ).
fof(f1908,plain,
( spl75_6
| ~ spl75_112
| ~ spl75_134
| ~ spl75_139 ),
inference(avatar_contradiction_clause,[],[f1907]) ).
fof(f1911,plain,
( e3 != op(e0,e0)
| spl75_7
| ~ spl75_184 ),
inference(superposition,[],[f599,f1402]) ).
fof(f1912,plain,
( ~ spl75_223
| spl75_7
| ~ spl75_184 ),
inference(avatar_split_clause,[],[f1911,f1401,f597,f1680]) ).
fof(f1914,plain,
( e3 != op(op(e2,e3),e3)
| spl75_8
| ~ spl75_112 ),
inference(forward_demodulation,[],[f603,f1021]) ).
fof(f1916,plain,
( e3 != op(e4,e3)
| spl75_8
| ~ spl75_112
| ~ spl75_163 ),
inference(forward_demodulation,[],[f1914,f1279]) ).
fof(f1917,plain,
( $false
| spl75_8
| ~ spl75_112
| ~ spl75_134
| ~ spl75_163 ),
inference(forward_subsumption_resolution,[],[f1916,f1127]) ).
fof(f1918,plain,
( spl75_8
| ~ spl75_112
| ~ spl75_134
| ~ spl75_163 ),
inference(avatar_contradiction_clause,[],[f1917]) ).
fof(f1920,plain,
( e3 != op(op(e1,e3),e1)
| spl75_9
| ~ spl75_182 ),
inference(forward_demodulation,[],[f607,f1391]) ).
fof(f1922,plain,
( e3 != op(e2,e1)
| spl75_9
| ~ spl75_173
| ~ spl75_182 ),
inference(forward_demodulation,[],[f1920,f1340]) ).
fof(f1923,plain,
( ~ spl75_198
| spl75_9
| ~ spl75_173
| ~ spl75_182 ),
inference(avatar_split_clause,[],[f1922,f1390,f1339,f605,f1484]) ).
fof(f1925,plain,
( e3 != op(op(e0,e3),e4)
| spl75_10
| ~ spl75_168 ),
inference(forward_demodulation,[],[f611,f1306]) ).
fof(f1927,plain,
( e3 != op(e1,e4)
| spl75_10
| ~ spl75_168
| ~ spl75_180 ),
inference(forward_demodulation,[],[f1925,f1379]) ).
fof(f1929,plain,
( $false
| spl75_10
| ~ spl75_132
| ~ spl75_168
| ~ spl75_180 ),
inference(forward_subsumption_resolution,[],[f1927,f1116]) ).
fof(f1930,plain,
( spl75_10
| ~ spl75_132
| ~ spl75_168
| ~ spl75_180 ),
inference(avatar_contradiction_clause,[],[f1929]) ).
fof(f1932,plain,
( e2 != op(op(e4,e2),e0)
| spl75_11
| ~ spl75_156 ),
inference(forward_demodulation,[],[f615,f1241]) ).
fof(f1934,plain,
( e2 != op(e4,e0)
| spl75_11
| ~ spl75_111
| ~ spl75_156 ),
inference(forward_demodulation,[],[f1932,f1017]) ).
fof(f1935,plain,
( $false
| spl75_11
| ~ spl75_111
| ~ spl75_145
| ~ spl75_156 ),
inference(forward_subsumption_resolution,[],[f1934,f1184]) ).
fof(f1936,plain,
( spl75_11
| ~ spl75_111
| ~ spl75_145
| ~ spl75_156 ),
inference(avatar_contradiction_clause,[],[f1935]) ).
fof(f1938,plain,
( e2 != op(op(e3,e2),e4)
| spl75_12
| ~ spl75_163 ),
inference(forward_demodulation,[],[f619,f1279]) ).
fof(f1940,plain,
( e2 != op(e3,e4)
| spl75_12
| ~ spl75_112
| ~ spl75_163 ),
inference(forward_demodulation,[],[f1938,f1021]) ).
fof(f1941,plain,
( $false
| spl75_12
| ~ spl75_112
| ~ spl75_139
| ~ spl75_163 ),
inference(forward_subsumption_resolution,[],[f1940,f1152]) ).
fof(f1942,plain,
( spl75_12
| ~ spl75_112
| ~ spl75_139
| ~ spl75_163 ),
inference(avatar_contradiction_clause,[],[f1941]) ).
fof(f1944,plain,
( e2 != op(e2,e2)
| spl75_13
| ~ spl75_113 ),
inference(forward_demodulation,[],[f623,f1025]) ).
fof(f1946,plain,
( $false
| spl75_13
| ~ spl75_113 ),
inference(forward_subsumption_resolution,[],[f1944,f1025]) ).
fof(f1947,plain,
( spl75_13
| ~ spl75_113 ),
inference(avatar_contradiction_clause,[],[f1946]) ).
fof(f1949,plain,
( e2 != op(e1,op(e2,e1))
| spl75_14
| ~ spl75_114 ),
inference(forward_demodulation,[],[f627,f1029]) ).
fof(f1950,plain,
( e2 != op(e1,e3)
| spl75_14
| ~ spl75_114
| ~ spl75_198 ),
inference(superposition,[],[f1949,f1485]) ).
fof(f1951,plain,
( $false
| spl75_14
| ~ spl75_114
| ~ spl75_173
| ~ spl75_198 ),
inference(forward_subsumption_resolution,[],[f1950,f1340]) ).
fof(f1952,plain,
( spl75_14
| ~ spl75_114
| ~ spl75_173
| ~ spl75_198 ),
inference(avatar_contradiction_clause,[],[f1951]) ).
fof(f1954,plain,
( e2 != op(e0,op(e2,e0))
| spl75_15
| ~ spl75_115 ),
inference(forward_demodulation,[],[f631,f1033]) ).
fof(f1956,plain,
( e2 != op(e0,e1)
| spl75_15
| ~ spl75_115
| ~ spl75_205 ),
inference(superposition,[],[f1954,f1534]) ).
fof(f1957,plain,
( ~ spl75_217
| spl75_15
| ~ spl75_115
| ~ spl75_205 ),
inference(avatar_split_clause,[],[f1956,f1533,f1031,f629,f1616]) ).
fof(f1959,plain,
( e1 != op(op(e4,e1),e3)
| spl75_16
| ~ spl75_132 ),
inference(forward_demodulation,[],[f635,f1116]) ).
fof(f1961,plain,
( e1 != op(e0,e3)
| spl75_16
| ~ spl75_132
| ~ spl75_160 ),
inference(forward_demodulation,[],[f1959,f1263]) ).
fof(f1963,plain,
( $false
| spl75_16
| ~ spl75_132
| ~ spl75_160
| ~ spl75_180 ),
inference(forward_subsumption_resolution,[],[f1961,f1379]) ).
fof(f1964,plain,
( spl75_16
| ~ spl75_132
| ~ spl75_160
| ~ spl75_180 ),
inference(avatar_contradiction_clause,[],[f1963]) ).
fof(f1966,plain,
( e1 != op(op(e3,e1),e2)
| spl75_17
| ~ spl75_173 ),
inference(forward_demodulation,[],[f639,f1340]) ).
fof(f1968,plain,
( e1 != op(e1,e2)
| spl75_17
| ~ spl75_173
| ~ spl75_182 ),
inference(forward_demodulation,[],[f1966,f1391]) ).
fof(f1969,plain,
( $false
| spl75_17
| ~ spl75_114
| ~ spl75_173
| ~ spl75_182 ),
inference(forward_subsumption_resolution,[],[f1968,f1029]) ).
fof(f1970,plain,
( spl75_17
| ~ spl75_114
| ~ spl75_173
| ~ spl75_182 ),
inference(avatar_contradiction_clause,[],[f1969]) ).
fof(f1972,plain,
( e1 != op(op(e2,e1),e1)
| spl75_18
| ~ spl75_114 ),
inference(forward_demodulation,[],[f643,f1029]) ).
fof(f1974,plain,
( e1 != op(e3,e1)
| spl75_18
| ~ spl75_114
| ~ spl75_198 ),
inference(forward_demodulation,[],[f1972,f1485]) ).
fof(f1975,plain,
( $false
| spl75_18
| ~ spl75_114
| ~ spl75_182
| ~ spl75_198 ),
inference(forward_subsumption_resolution,[],[f1974,f1391]) ).
fof(f1976,plain,
( spl75_18
| ~ spl75_114
| ~ spl75_182
| ~ spl75_198 ),
inference(avatar_contradiction_clause,[],[f1975]) ).
fof(f1979,plain,
( e1 != op(e4,e4)
| spl75_19
| ~ spl75_210 ),
inference(superposition,[],[f647,f1568]) ).
fof(f1980,plain,
( $false
| spl75_19
| ~ spl75_146
| ~ spl75_210 ),
inference(forward_subsumption_resolution,[],[f1979,f1189]) ).
fof(f1981,plain,
( spl75_19
| ~ spl75_146
| ~ spl75_210 ),
inference(avatar_contradiction_clause,[],[f1980]) ).
fof(f1985,plain,
( e1 != op(op(e0,e1),e0)
| spl75_20
| ~ spl75_221 ),
inference(superposition,[],[f651,f1658]) ).
fof(f1986,plain,
( e1 != op(e2,e0)
| spl75_20
| ~ spl75_217
| ~ spl75_221 ),
inference(forward_demodulation,[],[f1985,f1617]) ).
fof(f1989,plain,
( $false
| spl75_20
| ~ spl75_205
| ~ spl75_217
| ~ spl75_221 ),
inference(forward_subsumption_resolution,[],[f1986,f1534]) ).
fof(f1990,plain,
( spl75_20
| ~ spl75_205
| ~ spl75_217
| ~ spl75_221 ),
inference(avatar_contradiction_clause,[],[f1989]) ).
fof(f1992,plain,
( e0 != op(op(e4,e0),e4)
| spl75_21
| ~ spl75_129 ),
inference(forward_demodulation,[],[f655,f1095]) ).
fof(f1994,plain,
( e0 != op(e2,e4)
| spl75_21
| ~ spl75_129
| ~ spl75_145 ),
inference(forward_demodulation,[],[f1992,f1184]) ).
fof(f1995,plain,
( $false
| spl75_21
| ~ spl75_129
| ~ spl75_145
| ~ spl75_156 ),
inference(forward_subsumption_resolution,[],[f1994,f1241]) ).
fof(f1996,plain,
( spl75_21
| ~ spl75_129
| ~ spl75_145
| ~ spl75_156 ),
inference(avatar_contradiction_clause,[],[f1995]) ).
fof(f1998,plain,
( e0 != op(op(e3,e0),e1)
| spl75_22
| ~ spl75_180 ),
inference(forward_demodulation,[],[f659,f1379]) ).
fof(f2000,plain,
( e0 != op(e4,e1)
| spl75_22
| ~ spl75_168
| ~ spl75_180 ),
inference(forward_demodulation,[],[f1998,f1306]) ).
fof(f2001,plain,
( $false
| spl75_22
| ~ spl75_160
| ~ spl75_168
| ~ spl75_180 ),
inference(forward_subsumption_resolution,[],[f2000,f1263]) ).
fof(f2002,plain,
( spl75_22
| ~ spl75_160
| ~ spl75_168
| ~ spl75_180 ),
inference(avatar_contradiction_clause,[],[f2001]) ).
fof(f2004,plain,
( e0 != op(op(e2,e0),e0)
| spl75_23
| ~ spl75_115 ),
inference(forward_demodulation,[],[f663,f1033]) ).
fof(f2006,plain,
( e0 != op(e1,e0)
| spl75_23
| ~ spl75_115
| ~ spl75_205 ),
inference(forward_demodulation,[],[f2004,f1534]) ).
fof(f2007,plain,
( $false
| spl75_23
| ~ spl75_115
| ~ spl75_205
| ~ spl75_221 ),
inference(forward_subsumption_resolution,[],[f2006,f1658]) ).
fof(f2008,plain,
( spl75_23
| ~ spl75_115
| ~ spl75_205
| ~ spl75_221 ),
inference(avatar_contradiction_clause,[],[f2007]) ).
fof(f2010,plain,
( e0 != op(op(e1,e0),e2)
| spl75_24
| ~ spl75_217 ),
inference(forward_demodulation,[],[f667,f1617]) ).
fof(f2012,plain,
( e0 != op(e0,e2)
| spl75_24
| ~ spl75_217
| ~ spl75_221 ),
inference(forward_demodulation,[],[f2010,f1658]) ).
fof(f2013,plain,
( $false
| spl75_24
| ~ spl75_115
| ~ spl75_217
| ~ spl75_221 ),
inference(forward_subsumption_resolution,[],[f2012,f1033]) ).
fof(f2014,plain,
( spl75_24
| ~ spl75_115
| ~ spl75_217
| ~ spl75_221 ),
inference(avatar_contradiction_clause,[],[f2013]) ).
fof(f2017,plain,
( e0 != op(e3,e3)
| spl75_25
| ~ spl75_223 ),
inference(superposition,[],[f671,f1681]) ).
fof(f2018,plain,
( $false
| spl75_25
| ~ spl75_184
| ~ spl75_223 ),
inference(forward_subsumption_resolution,[],[f2017,f1402]) ).
fof(f2019,plain,
( spl75_25
| ~ spl75_184
| ~ spl75_223 ),
inference(avatar_contradiction_clause,[],[f2018]) ).
fof(f2021,plain,
( e2 = e3
| ~ spl75_102
| ~ spl75_139 ),
inference(forward_demodulation,[],[f979,f1152]) ).
fof(f2025,plain,
( $false
| ~ spl75_102
| ~ spl75_139 ),
inference(forward_subsumption_resolution,[],[f2021,f159]) ).
fof(f2026,plain,
( ~ spl75_102
| ~ spl75_139 ),
inference(avatar_contradiction_clause,[],[f2025]) ).
fof(f2034,plain,
( e0 = e2
| ~ spl75_103
| ~ spl75_156 ),
inference(forward_demodulation,[],[f983,f1241]) ).
fof(f2040,plain,
( $false
| ~ spl75_103
| ~ spl75_156 ),
inference(forward_subsumption_resolution,[],[f2034,f165]) ).
fof(f2041,plain,
( ~ spl75_103
| ~ spl75_156 ),
inference(avatar_contradiction_clause,[],[f2040]) ).
fof(f2049,plain,
( e1 = e3
| ~ spl75_104
| ~ spl75_132 ),
inference(superposition,[],[f987,f1116]) ).
fof(f2053,plain,
( $false
| ~ spl75_104
| ~ spl75_132 ),
inference(forward_subsumption_resolution,[],[f2049,f161]) ).
fof(f2054,plain,
( ~ spl75_104
| ~ spl75_132 ),
inference(avatar_contradiction_clause,[],[f2053]) ).
fof(f2056,plain,
( e0 = e4
| ~ spl75_105
| ~ spl75_129 ),
inference(superposition,[],[f991,f1095]) ).
fof(f2060,plain,
( $false
| ~ spl75_105
| ~ spl75_129 ),
inference(forward_subsumption_resolution,[],[f2056,f163]) ).
fof(f2061,plain,
( ~ spl75_105
| ~ spl75_129 ),
inference(avatar_contradiction_clause,[],[f2060]) ).
fof(f2062,plain,
( e1 = e4
| ~ spl75_101
| ~ spl75_146 ),
inference(forward_demodulation,[],[f975,f1189]) ).
fof(f2064,plain,
( $false
| ~ spl75_101
| ~ spl75_146 ),
inference(forward_subsumption_resolution,[],[f2062,f160]) ).
fof(f2065,plain,
( ~ spl75_101
| ~ spl75_146 ),
inference(avatar_contradiction_clause,[],[f2064]) ).
cnf(s1,plain,
( ~ spl75_1
| ~ spl75_2
| ~ spl75_3
| ~ spl75_4
| ~ spl75_5
| ~ spl75_6
| ~ spl75_7
| ~ spl75_8
| ~ spl75_9
| ~ spl75_10
| ~ spl75_11
| ~ spl75_12
| ~ spl75_13
| ~ spl75_14
| ~ spl75_15
| ~ spl75_16
| ~ spl75_17
| ~ spl75_18
| ~ spl75_19
| ~ spl75_20
| ~ spl75_21
| ~ spl75_22
| ~ spl75_23
| ~ spl75_24
| ~ spl75_25
| spl75_26
| spl75_27
| spl75_28
| spl75_29
| spl75_30
| spl75_31
| spl75_32
| spl75_33
| spl75_34
| spl75_35
| spl75_36
| spl75_37
| spl75_38
| spl75_39
| spl75_40
| spl75_41
| spl75_42
| spl75_43
| spl75_44
| spl75_45
| spl75_46
| spl75_47
| spl75_48
| spl75_49
| spl75_50
| spl75_51
| spl75_52
| spl75_53
| spl75_54
| spl75_55
| spl75_56
| spl75_57
| spl75_58
| spl75_59
| spl75_60
| spl75_61
| spl75_62
| spl75_63
| spl75_64
| spl75_65
| spl75_66
| spl75_67
| spl75_68
| spl75_69
| spl75_70
| spl75_71
| spl75_72
| spl75_73
| spl75_74
| spl75_75
| spl75_76
| spl75_77
| spl75_78
| spl75_79
| spl75_80
| spl75_81
| spl75_82
| spl75_83
| spl75_84
| spl75_85
| spl75_86
| spl75_87
| spl75_88
| spl75_89
| spl75_90
| spl75_91
| spl75_92
| spl75_93
| spl75_94
| spl75_95
| spl75_96
| spl75_97
| spl75_98
| spl75_99
| spl75_100
| spl75_101
| spl75_102
| spl75_103
| spl75_104
| spl75_105 ),
inference(sat_conversion,[],[f992]) ).
cnf(s10,plain,
( ~ spl75_26
| ~ spl75_129 ),
inference(sat_conversion,[],[f1097]) ).
cnf(s13,plain,
( ~ spl75_27
| ~ spl75_111 ),
inference(sat_conversion,[],[f1100]) ).
cnf(s19,plain,
( ~ spl75_28
| ~ spl75_132 ),
inference(sat_conversion,[],[f1118]) ).
cnf(s22,plain,
( ~ spl75_29
| ~ spl75_134 ),
inference(sat_conversion,[],[f1129]) ).
cnf(s27,plain,
( ~ spl75_30
| ~ spl75_139 ),
inference(sat_conversion,[],[f1154]) ).
cnf(s35,plain,
( ~ spl75_31
| ~ spl75_145 ),
inference(sat_conversion,[],[f1186]) ).
cnf(s36,plain,
( ~ spl75_32
| ~ spl75_146 ),
inference(sat_conversion,[],[f1191]) ).
cnf(s41,plain,
( ~ spl75_33
| ~ spl75_146 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s48,plain,
( ~ spl75_34
| ~ spl75_156 ),
inference(sat_conversion,[],[f1243]) ).
cnf(s54,plain,
( ~ spl75_35
| ~ spl75_160 ),
inference(sat_conversion,[],[f1265]) ).
cnf(s58,plain,
( ~ spl75_36
| ~ spl75_163 ),
inference(sat_conversion,[],[f1281]) ).
cnf(s65,plain,
( ~ spl75_37
| ~ spl75_168 ),
inference(sat_conversion,[],[f1308]) ).
cnf(s66,plain,
( ~ spl75_38
| ~ spl75_134 ),
inference(sat_conversion,[],[f1309]) ).
cnf(s73,plain,
( ~ spl75_39
| ~ spl75_112 ),
inference(sat_conversion,[],[f1328]) ).
cnf(s79,plain,
( ~ spl75_40
| ~ spl75_173 ),
inference(sat_conversion,[],[f1342]) ).
cnf(s81,plain,
( ~ spl75_41
| ~ spl75_139 ),
inference(sat_conversion,[],[f1348]) ).
cnf(s90,plain,
( ~ spl75_42
| ~ spl75_180 ),
inference(sat_conversion,[],[f1381]) ).
cnf(s94,plain,
( ~ spl75_43
| ~ spl75_182 ),
inference(sat_conversion,[],[f1393]) ).
cnf(s97,plain,
( ~ spl75_44
| ~ spl75_184 ),
inference(sat_conversion,[],[f1404]) ).
cnf(s102,plain,
( ~ spl75_45
| ~ spl75_184 ),
inference(sat_conversion,[],[f1417]) ).
cnf(s106,plain,
( ~ spl75_46
| ~ spl75_111 ),
inference(sat_conversion,[],[f1433]) ).
cnf(s112,plain,
( ~ spl75_47
| ~ spl75_163 ),
inference(sat_conversion,[],[f1451]) ).
cnf(s117,plain,
( ~ spl75_48
| ~ spl75_112 ),
inference(sat_conversion,[],[f1464]) ).
cnf(s124,plain,
( ~ spl75_49
| ~ spl75_198 ),
inference(sat_conversion,[],[f1487]) ).
cnf(s128,plain,
( ~ spl75_50
| ~ spl75_113 ),
inference(sat_conversion,[],[f1495]) ).
cnf(s133,plain,
( ~ spl75_51
| ~ spl75_113 ),
inference(sat_conversion,[],[f1508]) ).
cnf(s139,plain,
( ~ spl75_52
| ~ spl75_114 ),
inference(sat_conversion,[],[f1518]) ).
cnf(s145,plain,
( ~ spl75_53
| ~ spl75_205 ),
inference(sat_conversion,[],[f1536]) ).
cnf(s150,plain,
( ~ spl75_54
| ~ spl75_115 ),
inference(sat_conversion,[],[f1549]) ).
cnf(s151,plain,
( ~ spl75_55
| ~ spl75_156 ),
inference(sat_conversion,[],[f1550]) ).
cnf(s159,plain,
( ~ spl75_56
| ~ spl75_210 ),
inference(sat_conversion,[],[f1570]) ).
cnf(s164,plain,
( ~ spl75_57
| ~ spl75_210 ),
inference(sat_conversion,[],[f1579]) ).
cnf(s168,plain,
( ~ spl75_58
| ~ spl75_198 ),
inference(sat_conversion,[],[f1587]) ).
cnf(s171,plain,
( ~ spl75_59
| ~ spl75_132 ),
inference(sat_conversion,[],[f1598]) ).
cnf(s180,plain,
( ~ spl75_60
| ~ spl75_217 ),
inference(sat_conversion,[],[f1619]) ).
cnf(s182,plain,
( ~ spl75_61
| ~ spl75_173 ),
inference(sat_conversion,[],[f1621]) ).
cnf(s187,plain,
( ~ spl75_62
| ~ spl75_182 ),
inference(sat_conversion,[],[f1630]) ).
cnf(s193,plain,
( ~ spl75_63
| ~ spl75_114 ),
inference(sat_conversion,[],[f1640]) ).
cnf(s196,plain,
( ~ spl75_64
| ~ spl75_160 ),
inference(sat_conversion,[],[f1643]) ).
cnf(s205,plain,
( ~ spl75_65
| ~ spl75_221 ),
inference(sat_conversion,[],[f1660]) ).
cnf(s207,plain,
( ~ spl75_66
| ~ spl75_168 ),
inference(sat_conversion,[],[f1662]) ).
cnf(s211,plain,
( ~ spl75_67
| ~ spl75_129 ),
inference(sat_conversion,[],[f1670]) ).
cnf(s220,plain,
( ~ spl75_68
| ~ spl75_223 ),
inference(sat_conversion,[],[f1683]) ).
cnf(s225,plain,
( ~ spl75_69
| ~ spl75_223 ),
inference(sat_conversion,[],[f1688]) ).
cnf(s226,plain,
( ~ spl75_70
| ~ spl75_145 ),
inference(sat_conversion,[],[f1689]) ).
cnf(s234,plain,
( ~ spl75_71
| ~ spl75_217 ),
inference(sat_conversion,[],[f1701]) ).
cnf(s238,plain,
( ~ spl75_72
| ~ spl75_205 ),
inference(sat_conversion,[],[f1705]) ).
cnf(s242,plain,
( ~ spl75_73
| ~ spl75_180 ),
inference(sat_conversion,[],[f1713]) ).
cnf(s249,plain,
( ~ spl75_74
| ~ spl75_221 ),
inference(sat_conversion,[],[f1720]) ).
cnf(s253,plain,
( ~ spl75_75
| ~ spl75_115 ),
inference(sat_conversion,[],[f1724]) ).
cnf(s259,plain,
( ~ spl75_76
| ~ spl75_146 ),
inference(sat_conversion,[],[f1730]) ).
cnf(s262,plain,
( ~ spl75_77
| ~ spl75_134 ),
inference(sat_conversion,[],[f1733]) ).
cnf(s266,plain,
( ~ spl75_78
| ~ spl75_111 ),
inference(sat_conversion,[],[f1737]) ).
cnf(s275,plain,
( ~ spl75_79
| ~ spl75_160 ),
inference(sat_conversion,[],[f1746]) ).
cnf(s278,plain,
( ~ spl75_80
| ~ spl75_145 ),
inference(sat_conversion,[],[f1749]) ).
cnf(s283,plain,
( ~ spl75_81
| ~ spl75_139 ),
inference(sat_conversion,[],[f1754]) ).
cnf(s290,plain,
( ~ spl75_82
| ~ spl75_184 ),
inference(sat_conversion,[],[f1761]) ).
cnf(s292,plain,
( ~ spl75_83
| ~ spl75_112 ),
inference(sat_conversion,[],[f1763]) ).
cnf(s299,plain,
( ~ spl75_84
| ~ spl75_182 ),
inference(sat_conversion,[],[f1770]) ).
cnf(s301,plain,
( ~ spl75_85
| ~ spl75_168 ),
inference(sat_conversion,[],[f1772]) ).
cnf(s310,plain,
( ~ spl75_86
| ~ spl75_156 ),
inference(sat_conversion,[],[f1781]) ).
cnf(s311,plain,
( ~ spl75_87
| ~ spl75_163 ),
inference(sat_conversion,[],[f1782]) ).
cnf(s318,plain,
( ~ spl75_88
| ~ spl75_113 ),
inference(sat_conversion,[],[f1789]) ).
cnf(s322,plain,
( ~ spl75_89
| ~ spl75_198 ),
inference(sat_conversion,[],[f1793]) ).
cnf(s329,plain,
( ~ spl75_90
| ~ spl75_205 ),
inference(sat_conversion,[],[f1800]) ).
cnf(s332,plain,
( ~ spl75_91
| ~ spl75_132 ),
inference(sat_conversion,[],[f1803]) ).
cnf(s338,plain,
( ~ spl75_92
| ~ spl75_173 ),
inference(sat_conversion,[],[f1809]) ).
cnf(s344,plain,
( ~ spl75_93
| ~ spl75_114 ),
inference(sat_conversion,[],[f1815]) ).
cnf(s346,plain,
( ~ spl75_94
| ~ spl75_210 ),
inference(sat_conversion,[],[f1817]) ).
cnf(s355,plain,
( ~ spl75_95
| ~ spl75_221 ),
inference(sat_conversion,[],[f1826]) ).
cnf(s356,plain,
( ~ spl75_96
| ~ spl75_129 ),
inference(sat_conversion,[],[f1827]) ).
cnf(s364,plain,
( ~ spl75_97
| ~ spl75_180 ),
inference(sat_conversion,[],[f1835]) ).
cnf(s370,plain,
( ~ spl75_98
| ~ spl75_115 ),
inference(sat_conversion,[],[f1841]) ).
cnf(s373,plain,
( ~ spl75_99
| ~ spl75_217 ),
inference(sat_conversion,[],[f1844]) ).
cnf(s377,plain,
( ~ spl75_100
| ~ spl75_223 ),
inference(sat_conversion,[],[f1848]) ).
cnf(s381,plain,
spl75_146,
inference(sat_conversion,[],[f1852]) ).
cnf(s382,plain,
spl75_134,
inference(sat_conversion,[],[f1853]) ).
cnf(s383,plain,
spl75_111,
inference(sat_conversion,[],[f1854]) ).
cnf(s384,plain,
spl75_160,
inference(sat_conversion,[],[f1855]) ).
cnf(s385,plain,
spl75_145,
inference(sat_conversion,[],[f1856]) ).
cnf(s386,plain,
spl75_139,
inference(sat_conversion,[],[f1857]) ).
cnf(s387,plain,
spl75_184,
inference(sat_conversion,[],[f1858]) ).
cnf(s388,plain,
spl75_112,
inference(sat_conversion,[],[f1859]) ).
cnf(s389,plain,
spl75_182,
inference(sat_conversion,[],[f1860]) ).
cnf(s390,plain,
spl75_168,
inference(sat_conversion,[],[f1861]) ).
cnf(s391,plain,
spl75_156,
inference(sat_conversion,[],[f1862]) ).
cnf(s392,plain,
spl75_163,
inference(sat_conversion,[],[f1863]) ).
cnf(s393,plain,
spl75_113,
inference(sat_conversion,[],[f1864]) ).
cnf(s394,plain,
spl75_198,
inference(sat_conversion,[],[f1865]) ).
cnf(s395,plain,
spl75_205,
inference(sat_conversion,[],[f1866]) ).
cnf(s396,plain,
spl75_132,
inference(sat_conversion,[],[f1867]) ).
cnf(s397,plain,
spl75_173,
inference(sat_conversion,[],[f1868]) ).
cnf(s398,plain,
spl75_114,
inference(sat_conversion,[],[f1869]) ).
cnf(s399,plain,
spl75_210,
inference(sat_conversion,[],[f1870]) ).
cnf(s400,plain,
spl75_221,
inference(sat_conversion,[],[f1871]) ).
cnf(s401,plain,
spl75_129,
inference(sat_conversion,[],[f1872]) ).
cnf(s402,plain,
spl75_180,
inference(sat_conversion,[],[f1873]) ).
cnf(s403,plain,
spl75_115,
inference(sat_conversion,[],[f1874]) ).
cnf(s404,plain,
spl75_217,
inference(sat_conversion,[],[f1875]) ).
cnf(s405,plain,
spl75_223,
inference(sat_conversion,[],[f1876]) ).
cnf(s406,plain,
( spl75_1
| ~ spl75_146
| ~ spl75_210 ),
inference(sat_conversion,[],[f1878]) ).
cnf(s408,plain,
( spl75_2
| ~ spl75_134
| ~ spl75_139
| ~ spl75_163 ),
inference(sat_conversion,[],[f1883]) ).
cnf(s410,plain,
( spl75_3
| ~ spl75_111
| ~ spl75_129
| ~ spl75_156 ),
inference(sat_conversion,[],[f1890]) ).
cnf(s411,plain,
( spl75_4
| ~ spl75_132
| ~ spl75_160
| ~ spl75_168 ),
inference(sat_conversion,[],[f1895]) ).
cnf(s413,plain,
( spl75_5
| ~ spl75_111
| ~ spl75_129
| ~ spl75_145 ),
inference(sat_conversion,[],[f1902]) ).
cnf(s414,plain,
( spl75_6
| ~ spl75_112
| ~ spl75_134
| ~ spl75_139 ),
inference(sat_conversion,[],[f1908]) ).
cnf(s415,plain,
( spl75_7
| ~ spl75_184
| ~ spl75_223 ),
inference(sat_conversion,[],[f1912]) ).
cnf(s417,plain,
( spl75_8
| ~ spl75_112
| ~ spl75_134
| ~ spl75_163 ),
inference(sat_conversion,[],[f1918]) ).
cnf(s418,plain,
( spl75_9
| ~ spl75_173
| ~ spl75_182
| ~ spl75_198 ),
inference(sat_conversion,[],[f1923]) ).
cnf(s420,plain,
( spl75_10
| ~ spl75_132
| ~ spl75_168
| ~ spl75_180 ),
inference(sat_conversion,[],[f1930]) ).
cnf(s421,plain,
( spl75_11
| ~ spl75_111
| ~ spl75_145
| ~ spl75_156 ),
inference(sat_conversion,[],[f1936]) ).
cnf(s422,plain,
( spl75_12
| ~ spl75_112
| ~ spl75_139
| ~ spl75_163 ),
inference(sat_conversion,[],[f1942]) ).
cnf(s423,plain,
( spl75_13
| ~ spl75_113 ),
inference(sat_conversion,[],[f1947]) ).
cnf(s424,plain,
( spl75_14
| ~ spl75_114
| ~ spl75_173
| ~ spl75_198 ),
inference(sat_conversion,[],[f1952]) ).
cnf(s425,plain,
( spl75_15
| ~ spl75_115
| ~ spl75_205
| ~ spl75_217 ),
inference(sat_conversion,[],[f1957]) ).
cnf(s427,plain,
( spl75_16
| ~ spl75_132
| ~ spl75_160
| ~ spl75_180 ),
inference(sat_conversion,[],[f1964]) ).
cnf(s428,plain,
( spl75_17
| ~ spl75_114
| ~ spl75_173
| ~ spl75_182 ),
inference(sat_conversion,[],[f1970]) ).
cnf(s429,plain,
( spl75_18
| ~ spl75_114
| ~ spl75_182
| ~ spl75_198 ),
inference(sat_conversion,[],[f1976]) ).
cnf(s430,plain,
( spl75_19
| ~ spl75_146
| ~ spl75_210 ),
inference(sat_conversion,[],[f1981]) ).
cnf(s432,plain,
( spl75_20
| ~ spl75_205
| ~ spl75_217
| ~ spl75_221 ),
inference(sat_conversion,[],[f1990]) ).
cnf(s433,plain,
( spl75_21
| ~ spl75_129
| ~ spl75_145
| ~ spl75_156 ),
inference(sat_conversion,[],[f1996]) ).
cnf(s434,plain,
( spl75_22
| ~ spl75_160
| ~ spl75_168
| ~ spl75_180 ),
inference(sat_conversion,[],[f2002]) ).
cnf(s435,plain,
( spl75_23
| ~ spl75_115
| ~ spl75_205
| ~ spl75_221 ),
inference(sat_conversion,[],[f2008]) ).
cnf(s436,plain,
( spl75_24
| ~ spl75_115
| ~ spl75_217
| ~ spl75_221 ),
inference(sat_conversion,[],[f2014]) ).
cnf(s437,plain,
( spl75_25
| ~ spl75_184
| ~ spl75_223 ),
inference(sat_conversion,[],[f2019]) ).
cnf(s438,plain,
( ~ spl75_102
| ~ spl75_139 ),
inference(sat_conversion,[],[f2026]) ).
cnf(s442,plain,
( ~ spl75_103
| ~ spl75_156 ),
inference(sat_conversion,[],[f2041]) ).
cnf(s446,plain,
( ~ spl75_104
| ~ spl75_132 ),
inference(sat_conversion,[],[f2054]) ).
cnf(s448,plain,
( ~ spl75_105
| ~ spl75_129 ),
inference(sat_conversion,[],[f2061]) ).
cnf(s449,plain,
( ~ spl75_101
| ~ spl75_146 ),
inference(sat_conversion,[],[f2065]) ).
cnf(s450,plain,
~ spl75_105,
inference(rat,[],[s448,s401]) ).
cnf(s451,plain,
spl75_24,
inference(rat,[],[s436,s403,s404,s400]) ).
cnf(s452,plain,
~ spl75_104,
inference(rat,[],[s446,s396]) ).
cnf(s453,plain,
spl75_20,
inference(rat,[],[s432,s400,s404,s395]) ).
cnf(s454,plain,
spl75_23,
inference(rat,[],[s435,s400,s403,s395]) ).
cnf(s455,plain,
spl75_15,
inference(rat,[],[s425,s404,s403,s395]) ).
cnf(s456,plain,
spl75_14,
inference(rat,[],[s424,s397,s398,s394]) ).
cnf(s457,plain,
spl75_13,
inference(rat,[],[s423,s393]) ).
cnf(s458,plain,
~ spl75_103,
inference(rat,[],[s442,s391]) ).
cnf(s459,plain,
spl75_10,
inference(rat,[],[s420,s402,s396,s390]) ).
cnf(s461,plain,
spl75_18,
inference(rat,[],[s429,s394,s398,s389]) ).
cnf(s462,plain,
spl75_9,
inference(rat,[],[s418,s394,s397,s389]) ).
cnf(s463,plain,
spl75_17,
inference(rat,[],[s428,s397,s398,s389]) ).
cnf(s465,plain,
spl75_25,
inference(rat,[],[s437,s405,s387]) ).
cnf(s466,plain,
spl75_7,
inference(rat,[],[s415,s405,s387]) ).
cnf(s467,plain,
~ spl75_102,
inference(rat,[],[s438,s386]) ).
cnf(s468,plain,
spl75_12,
inference(rat,[],[s422,s392,s388,s386]) ).
cnf(s470,plain,
spl75_21,
inference(rat,[],[s433,s391,s401,s385]) ).
cnf(s472,plain,
spl75_22,
inference(rat,[],[s434,s402,s390,s384]) ).
cnf(s473,plain,
spl75_16,
inference(rat,[],[s427,s402,s396,s384]) ).
cnf(s474,plain,
spl75_4,
inference(rat,[],[s411,s390,s396,s384]) ).
cnf(s475,plain,
spl75_11,
inference(rat,[],[s421,s391,s385,s383]) ).
cnf(s476,plain,
spl75_5,
inference(rat,[],[s413,s385,s401,s383]) ).
cnf(s477,plain,
spl75_3,
inference(rat,[],[s410,s391,s401,s383]) ).
cnf(s479,plain,
spl75_2,
inference(rat,[],[s408,s392,s386,s382]) ).
cnf(s480,plain,
spl75_8,
inference(rat,[],[s417,s392,s388,s382]) ).
cnf(s481,plain,
spl75_6,
inference(rat,[],[s414,s386,s388,s382]) ).
cnf(s482,plain,
~ spl75_101,
inference(rat,[],[s449,s381]) ).
cnf(s483,plain,
spl75_19,
inference(rat,[],[s430,s399,s381]) ).
cnf(s484,plain,
spl75_1,
inference(rat,[],[s406,s399,s381]) ).
cnf(s485,plain,
~ spl75_100,
inference(rat,[],[s377,s405]) ).
cnf(s486,plain,
~ spl75_99,
inference(rat,[],[s373,s404]) ).
cnf(s487,plain,
~ spl75_98,
inference(rat,[],[s370,s403]) ).
cnf(s488,plain,
~ spl75_97,
inference(rat,[],[s364,s402]) ).
cnf(s489,plain,
~ spl75_96,
inference(rat,[],[s356,s401]) ).
cnf(s490,plain,
~ spl75_95,
inference(rat,[],[s355,s400]) ).
cnf(s491,plain,
~ spl75_94,
inference(rat,[],[s346,s399]) ).
cnf(s492,plain,
~ spl75_93,
inference(rat,[],[s344,s398]) ).
cnf(s493,plain,
~ spl75_92,
inference(rat,[],[s338,s397]) ).
cnf(s494,plain,
~ spl75_91,
inference(rat,[],[s332,s396]) ).
cnf(s495,plain,
~ spl75_90,
inference(rat,[],[s329,s395]) ).
cnf(s496,plain,
~ spl75_89,
inference(rat,[],[s322,s394]) ).
cnf(s497,plain,
~ spl75_88,
inference(rat,[],[s318,s393]) ).
cnf(s498,plain,
~ spl75_87,
inference(rat,[],[s311,s392]) ).
cnf(s499,plain,
~ spl75_86,
inference(rat,[],[s310,s391]) ).
cnf(s500,plain,
~ spl75_85,
inference(rat,[],[s301,s390]) ).
cnf(s501,plain,
~ spl75_84,
inference(rat,[],[s299,s389]) ).
cnf(s502,plain,
~ spl75_83,
inference(rat,[],[s292,s388]) ).
cnf(s503,plain,
~ spl75_82,
inference(rat,[],[s290,s387]) ).
cnf(s504,plain,
~ spl75_81,
inference(rat,[],[s283,s386]) ).
cnf(s505,plain,
~ spl75_80,
inference(rat,[],[s278,s385]) ).
cnf(s506,plain,
~ spl75_79,
inference(rat,[],[s275,s384]) ).
cnf(s507,plain,
~ spl75_78,
inference(rat,[],[s266,s383]) ).
cnf(s508,plain,
~ spl75_77,
inference(rat,[],[s262,s382]) ).
cnf(s509,plain,
~ spl75_76,
inference(rat,[],[s259,s381]) ).
cnf(s510,plain,
~ spl75_75,
inference(rat,[],[s253,s403]) ).
cnf(s511,plain,
~ spl75_74,
inference(rat,[],[s249,s400]) ).
cnf(s512,plain,
~ spl75_73,
inference(rat,[],[s242,s402]) ).
cnf(s513,plain,
~ spl75_72,
inference(rat,[],[s238,s395]) ).
cnf(s514,plain,
~ spl75_71,
inference(rat,[],[s234,s404]) ).
cnf(s515,plain,
~ spl75_70,
inference(rat,[],[s226,s385]) ).
cnf(s516,plain,
~ spl75_69,
inference(rat,[],[s225,s405]) ).
cnf(s517,plain,
~ spl75_68,
inference(rat,[],[s220,s405]) ).
cnf(s518,plain,
~ spl75_67,
inference(rat,[],[s211,s401]) ).
cnf(s519,plain,
~ spl75_66,
inference(rat,[],[s207,s390]) ).
cnf(s520,plain,
~ spl75_65,
inference(rat,[],[s205,s400]) ).
cnf(s521,plain,
~ spl75_64,
inference(rat,[],[s196,s384]) ).
cnf(s522,plain,
~ spl75_63,
inference(rat,[],[s193,s398]) ).
cnf(s523,plain,
~ spl75_62,
inference(rat,[],[s187,s389]) ).
cnf(s524,plain,
~ spl75_61,
inference(rat,[],[s182,s397]) ).
cnf(s525,plain,
~ spl75_60,
inference(rat,[],[s180,s404]) ).
cnf(s526,plain,
~ spl75_59,
inference(rat,[],[s171,s396]) ).
cnf(s527,plain,
~ spl75_58,
inference(rat,[],[s168,s394]) ).
cnf(s528,plain,
~ spl75_57,
inference(rat,[],[s164,s399]) ).
cnf(s529,plain,
~ spl75_56,
inference(rat,[],[s159,s399]) ).
cnf(s530,plain,
~ spl75_55,
inference(rat,[],[s151,s391]) ).
cnf(s531,plain,
~ spl75_54,
inference(rat,[],[s150,s403]) ).
cnf(s532,plain,
~ spl75_53,
inference(rat,[],[s145,s395]) ).
cnf(s533,plain,
~ spl75_52,
inference(rat,[],[s139,s398]) ).
cnf(s534,plain,
~ spl75_51,
inference(rat,[],[s133,s393]) ).
cnf(s535,plain,
~ spl75_50,
inference(rat,[],[s128,s393]) ).
cnf(s536,plain,
~ spl75_49,
inference(rat,[],[s124,s394]) ).
cnf(s537,plain,
~ spl75_48,
inference(rat,[],[s117,s388]) ).
cnf(s538,plain,
~ spl75_47,
inference(rat,[],[s112,s392]) ).
cnf(s539,plain,
~ spl75_46,
inference(rat,[],[s106,s383]) ).
cnf(s540,plain,
~ spl75_45,
inference(rat,[],[s102,s387]) ).
cnf(s541,plain,
~ spl75_44,
inference(rat,[],[s97,s387]) ).
cnf(s542,plain,
~ spl75_43,
inference(rat,[],[s94,s389]) ).
cnf(s543,plain,
~ spl75_42,
inference(rat,[],[s90,s402]) ).
cnf(s544,plain,
~ spl75_41,
inference(rat,[],[s81,s386]) ).
cnf(s545,plain,
~ spl75_40,
inference(rat,[],[s79,s397]) ).
cnf(s546,plain,
~ spl75_39,
inference(rat,[],[s73,s388]) ).
cnf(s547,plain,
~ spl75_38,
inference(rat,[],[s66,s382]) ).
cnf(s548,plain,
~ spl75_37,
inference(rat,[],[s65,s390]) ).
cnf(s549,plain,
~ spl75_36,
inference(rat,[],[s58,s392]) ).
cnf(s550,plain,
~ spl75_35,
inference(rat,[],[s54,s384]) ).
cnf(s551,plain,
~ spl75_34,
inference(rat,[],[s48,s391]) ).
cnf(s552,plain,
~ spl75_33,
inference(rat,[],[s41,s381]) ).
cnf(s553,plain,
~ spl75_32,
inference(rat,[],[s36,s381]) ).
cnf(s554,plain,
~ spl75_31,
inference(rat,[],[s35,s385]) ).
cnf(s555,plain,
~ spl75_30,
inference(rat,[],[s27,s386]) ).
cnf(s556,plain,
~ spl75_29,
inference(rat,[],[s22,s382]) ).
cnf(s557,plain,
~ spl75_28,
inference(rat,[],[s19,s396]) ).
cnf(s558,plain,
~ spl75_27,
inference(rat,[],[s13,s383]) ).
cnf(s559,plain,
~ spl75_26,
inference(rat,[],[s10,s401]) ).
cnf(s563,plain,
$false,
inference(rat,[],[s1,s450,s452,s458,s467,s482,s485,s486,s487,s488,s489,s490,s491,s492,s493,s494,s495,s496,s497,s498,s499,s500,s501,s502,s503,s504,s505,s506,s507,s508,s509,s510,s511,s512,s513,s514,s515,s516,s517,s518,s519,s520,s521,s522,s523,s524,s525,s526,s527,s528,s529,s530,s531,s532,s533,s534,s535,s536,s537,s538,s539,s540,s541,s542,s543,s544,s545,s546,s547,s548,s549,s550,s551,s552,s553,s554,s555,s556,s557,s558,s559,s465,s451,s454,s472,s470,s453,s483,s461,s463,s473,s455,s456,s457,s468,s475,s459,s462,s480,s466,s481,s476,s474,s477,s479,s484]) ).
fof(f2066,plain,
$false,
inference(avatar_sat_refutation,[],[s563]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG186+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n005.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 19:40:16 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.23/0.74 % (1078149)Detected formulas, will run a generic FOF schedule.
% 2.23/0.74 % (1078159)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=998026685:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.23/0.74 % (1078159)First to succeed.
% 2.23/0.74 % (1078159)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1078149"
% 2.23/0.74 % (1078157)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=550095457:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.23/0.74 % (1078155)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=778282104:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.23/0.74 % (1078154)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=1536131273:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.23/0.74 % (1078160)dis-21_1_sil=8000:lcm=predicate:random_seed=1337959257:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.23/0.74 % (1078156)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=2454119980:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.23/0.74 % (1078158)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2847976597:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.23/0.74 % (1078160)Refutation not found, incomplete strategy
% 2.23/0.74 % (1078160)------------------------------
% 2.23/0.74 % (1078160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.23/0.74 % (1078160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.23/0.74 % (1078160)CaDiCaL version: 2.1.3
% 2.23/0.74 % (1078160)Termination reason: Refutation not found, incomplete strategy
% 2.23/0.74 % (1078160)Time elapsed: 0.011 s
% 2.23/0.74 % (1078160)Peak memory usage: 89 MB
% 2.23/0.74 % (1078160)Instructions burned: 20 (million)
% 2.23/0.74 % (1078158)Also succeeded, but the first one will report.
% 2.23/0.74 % (1078157)Instruction limit reached!
% 2.23/0.74 % (1078157)------------------------------
% 2.23/0.74 % (1078157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.23/0.74 % (1078157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.23/0.74 % (1078157)CaDiCaL version: 2.1.3
% 2.23/0.74 % (1078157)Termination reason: Instruction limit
% 2.23/0.74 % (1078157)Termination phase: Saturation
% 2.23/0.74 % (1078157)Time elapsed: 0.048 s
% 2.23/0.74 % (1078157)Peak memory usage: 89 MB
% 2.23/0.74 % (1078157)Instructions burned: 109 (million)
% 2.23/0.74 % (1078159)Refutation found. Thanks to Tanya!
% 2.23/0.74 % SZS status Theorem for theBenchmark
% 2.23/0.74 % SZS output start Proof for theBenchmark
% See solution above
% 2.64/0.84 % (1078159)------------------------------
% 2.64/0.84 % (1078159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.64/0.84 % (1078159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.84 % (1078159)CaDiCaL version: 2.1.3
% 2.64/0.84 % (1078159)Termination reason: Refutation
% 2.64/0.84 % (1078159)Time elapsed: 0.017 s
% 2.64/0.84 % (1078159)Peak memory usage: 90 MB
% 2.64/0.84 % (1078159)Instructions burned: 62 (million)
% 2.64/0.84 % (1078159)------------------------------
% 2.64/0.84 % (1078159)------------------------------
% 2.64/0.84 % (1078149)Success in time 0.33 s
% 2.64/0.84 % Vampire exiting
%------------------------------------------------------------------------------