%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG187+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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.93s 1.12s
% Output : Refutation 3.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 208
% Syntax : Number of formulae : 891 ( 187 unt; 205 def)
% Number of atoms : 4146 (2405 equ)
% Maximal formula atoms : 425 ( 4 avg)
% Number of connectives : 5650 (2395 ~;1944 |;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/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( op(e0,e0) = e4
& op(e0,e1) = e2
& op(e0,e2) = e0
& op(e0,e3) = e1
& op(e0,e4) = e3
& op(e1,e0) = e0
& op(e1,e1) = e1
& op(e1,e2) = e2
& op(e1,e3) = e3
& op(e1,e4) = e4
& op(e2,e0) = e1
& op(e2,e1) = e4
& op(e2,e2) = e3
& op(e2,e3) = e0
& op(e2,e4) = e2
& op(e3,e0) = e3
& op(e3,e1) = e0
& op(e3,e2) = e4
& op(e3,e3) = e2
& op(e3,e4) = e1
& op(e4,e0) = e2
& op(e4,e1) = e3
& op(e4,e2) = e1
& op(e4,e3) = e4
& op(e4,e4) = e0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,conjecture,
( ( ( op(e0,e0) != e0
& op(e0,e1) != e1
& op(e0,e2) != e2
& op(e0,e3) != e3
& op(e0,e4) != e4 )
| ( op(e1,e0) != e0
& op(e1,e1) != e1
& op(e1,e2) != e2
& op(e1,e3) != e3
& op(e1,e4) != e4 )
| ( op(e2,e0) != e0
& op(e2,e1) != e1
& op(e2,e2) != e2
& op(e2,e3) != e3
& op(e2,e4) != e4 )
| ( op(e3,e0) != e0
& op(e3,e1) != e1
& op(e3,e2) != e2
& op(e3,e3) != e3
& op(e3,e4) != e4 )
| ( op(e4,e0) != e0
& op(e4,e1) != e1
& op(e4,e2) != e2
& op(e4,e3) != 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/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f4,negated_conjecture,
~ ( ( ( op(e0,e0) != e0
& op(e0,e1) != e1
& op(e0,e2) != e2
& op(e0,e3) != e3
& op(e0,e4) != e4 )
| ( op(e1,e0) != e0
& op(e1,e1) != e1
& op(e1,e2) != e2
& op(e1,e3) != e3
& op(e1,e4) != e4 )
| ( op(e2,e0) != e0
& op(e2,e1) != e1
& op(e2,e2) != e2
& op(e2,e3) != e3
& op(e2,e4) != e4 )
| ( op(e3,e0) != e0
& op(e3,e1) != e1
& op(e3,e2) != e2
& op(e3,e3) != e3
& op(e3,e4) != e4 )
| ( op(e4,e0) != e0
& op(e4,e1) != e1
& op(e4,e2) != e2
& op(e4,e3) != 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(e0,e1)
| e2 = op(e0,e2)
| e3 = op(e0,e3)
| e4 = op(e0,e4) )
& ( e0 = op(e1,e0)
| e1 = op(e1,e1)
| e2 = op(e1,e2)
| e3 = op(e1,e3)
| e4 = op(e1,e4) )
& ( e0 = op(e2,e0)
| e1 = op(e2,e1)
| e2 = op(e2,e2)
| e3 = op(e2,e3)
| e4 = op(e2,e4) )
& ( e0 = op(e3,e0)
| e1 = op(e3,e1)
| e2 = op(e3,e2)
| e3 = op(e3,e3)
| e4 = op(e3,e4) )
& ( e0 = op(e4,e0)
| e1 = op(e4,e1)
| e2 = op(e4,e2)
| e3 = op(e4,e3)
| 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(e0,e1)
| e2 = op(e0,e2)
| e3 = op(e0,e3)
| e4 = op(e0,e4) )
& ( e0 = op(e1,e0)
| e1 = op(e1,e1)
| e2 = op(e1,e2)
| e3 = op(e1,e3)
| e4 = op(e1,e4) )
& ( e0 = op(e2,e0)
| e1 = op(e2,e1)
| e2 = op(e2,e2)
| e3 = op(e2,e3)
| e4 = op(e2,e4) )
& ( e0 = op(e3,e0)
| e1 = op(e3,e1)
| e2 = op(e3,e2)
| e3 = op(e3,e3)
| e4 = op(e3,e4) )
& ( e0 = op(e4,e0)
| e1 = op(e4,e1)
| e2 = op(e4,e2)
| e3 = op(e4,e3)
| 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(f157,plain,
e3 != e4,
inference(cnf_transformation,[],[f1]) ).
fof(f161,plain,
e1 != e3,
inference(cnf_transformation,[],[f1]) ).
fof(f162,plain,
e1 != e2,
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,
e0 = op(e4,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f168,plain,
e4 = op(e4,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f169,plain,
e1 = op(e4,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f170,plain,
e3 = op(e4,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f171,plain,
e2 = op(e4,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f172,plain,
e1 = op(e3,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f173,plain,
e2 = op(e3,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f174,plain,
e4 = op(e3,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f175,plain,
e0 = op(e3,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f176,plain,
e3 = op(e3,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f177,plain,
e2 = op(e2,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f178,plain,
e0 = op(e2,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f179,plain,
e3 = op(e2,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f180,plain,
e4 = op(e2,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f181,plain,
e1 = op(e2,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f182,plain,
e4 = op(e1,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f183,plain,
e3 = op(e1,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f184,plain,
e2 = op(e1,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f185,plain,
e1 = op(e1,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f186,plain,
e0 = op(e1,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f187,plain,
e3 = 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,
e4 = op(e0,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f192,plain,
( e4 != 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(f213,plain,
( e3 != op(e0,e4)
| ~ sP70 ),
inference(cnf_transformation,[],[f86]) ).
fof(f221,plain,
( e0 != op(e1,e0)
| ~ sP69 ),
inference(cnf_transformation,[],[f87]) ).
fof(f225,plain,
( e1 != op(e1,e1)
| ~ sP68 ),
inference(cnf_transformation,[],[f88]) ).
fof(f229,plain,
( e2 != op(e1,e2)
| ~ sP67 ),
inference(cnf_transformation,[],[f89]) ).
fof(f233,plain,
( e3 != op(e1,e3)
| ~ sP66 ),
inference(cnf_transformation,[],[f90]) ).
fof(f237,plain,
( e4 != op(e1,e4)
| ~ sP65 ),
inference(cnf_transformation,[],[f91]) ).
fof(f245,plain,
( e1 != op(e2,e0)
| ~ sP64 ),
inference(cnf_transformation,[],[f92]) ).
fof(f247,plain,
( e4 != op(e2,e1)
| ~ sP63 ),
inference(cnf_transformation,[],[f93]) ).
fof(f253,plain,
( e3 != op(e2,e2)
| ~ sP62 ),
inference(cnf_transformation,[],[f94]) ).
fof(f261,plain,
( e0 != op(e2,e3)
| ~ sP61 ),
inference(cnf_transformation,[],[f95]) ).
fof(f264,plain,
( e2 != op(e2,e4)
| ~ sP60 ),
inference(cnf_transformation,[],[f96]) ).
fof(f268,plain,
( e3 != op(e3,e0)
| ~ sP59 ),
inference(cnf_transformation,[],[f97]) ).
fof(f276,plain,
( e0 != op(e3,e1)
| ~ sP58 ),
inference(cnf_transformation,[],[f98]) ).
fof(f277,plain,
( e4 != op(e3,e2)
| ~ sP57 ),
inference(cnf_transformation,[],[f99]) ).
fof(f284,plain,
( e2 != op(e3,e3)
| ~ sP56 ),
inference(cnf_transformation,[],[f100]) ).
fof(f290,plain,
( e1 != op(e3,e4)
| ~ sP55 ),
inference(cnf_transformation,[],[f101]) ).
fof(f294,plain,
( e2 != op(e4,e0)
| ~ sP54 ),
inference(cnf_transformation,[],[f102]) ).
fof(f298,plain,
( e3 != op(e4,e1)
| ~ sP53 ),
inference(cnf_transformation,[],[f103]) ).
fof(f305,plain,
( e1 != op(e4,e2)
| ~ sP52 ),
inference(cnf_transformation,[],[f104]) ).
fof(f307,plain,
( e4 != op(e4,e3)
| ~ sP51 ),
inference(cnf_transformation,[],[f105]) ).
fof(f316,plain,
( e0 != 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(f347,plain,
( e3 != op(e0,e4)
| ~ sP43 ),
inference(cnf_transformation,[],[f113]) ).
fof(f353,plain,
( e3 != op(e3,e0)
| ~ sP42 ),
inference(cnf_transformation,[],[f114]) ).
fof(f361,plain,
( e4 != op(e0,e0)
| ~ sP41 ),
inference(cnf_transformation,[],[f115]) ).
fof(f366,plain,
( e4 != op(e0,e0)
| ~ sP40 ),
inference(cnf_transformation,[],[f116]) ).
fof(f371,plain,
( e0 != op(e1,e0)
| ~ sP39 ),
inference(cnf_transformation,[],[f117]) ).
fof(f373,plain,
( e0 != op(e3,e1)
| ~ sP38 ),
inference(cnf_transformation,[],[f118]) ).
fof(f380,plain,
( e1 != op(e1,e1)
| ~ sP37 ),
inference(cnf_transformation,[],[f119]) ).
fof(f385,plain,
( e1 != op(e1,e1)
| ~ sP36 ),
inference(cnf_transformation,[],[f120]) ).
fof(f389,plain,
( e2 != op(e1,e2)
| ~ sP35 ),
inference(cnf_transformation,[],[f121]) ).
fof(f396,plain,
( e2 != op(e0,e1)
| ~ sP34 ),
inference(cnf_transformation,[],[f122]) ).
fof(f398,plain,
( e3 != op(e1,e3)
| ~ sP33 ),
inference(cnf_transformation,[],[f123]) ).
fof(f402,plain,
( e3 != op(e4,e1)
| ~ sP32 ),
inference(cnf_transformation,[],[f124]) ).
fof(f407,plain,
( e4 != op(e1,e4)
| ~ sP31 ),
inference(cnf_transformation,[],[f125]) ).
fof(f414,plain,
( e4 != op(e2,e1)
| ~ sP30 ),
inference(cnf_transformation,[],[f126]) ).
fof(f418,plain,
( e0 != op(e2,e3)
| ~ 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(f432,plain,
( e1 != op(e4,e2)
| ~ sP26 ),
inference(cnf_transformation,[],[f130]) ).
fof(f437,plain,
( e2 != op(e2,e4)
| ~ sP25 ),
inference(cnf_transformation,[],[f131]) ).
fof(f445,plain,
( e2 != op(e1,e2)
| ~ sP24 ),
inference(cnf_transformation,[],[f132]) ).
fof(f449,plain,
( e3 != op(e2,e2)
| ~ sP23 ),
inference(cnf_transformation,[],[f133]) ).
fof(f454,plain,
( e3 != op(e2,e2)
| ~ sP22 ),
inference(cnf_transformation,[],[f134]) ).
fof(f460,plain,
( e4 != op(e2,e1)
| ~ sP21 ),
inference(cnf_transformation,[],[f135]) ).
fof(f463,plain,
( e4 != op(e3,e2)
| ~ sP20 ),
inference(cnf_transformation,[],[f136]) ).
fof(f470,plain,
( e0 != op(e3,e1)
| ~ sP19 ),
inference(cnf_transformation,[],[f137]) ).
fof(f474,plain,
( e0 != op(e2,e3)
| ~ sP18 ),
inference(cnf_transformation,[],[f138]) ).
fof(f477,plain,
( e1 != op(e3,e4)
| ~ sP17 ),
inference(cnf_transformation,[],[f139]) ).
fof(f486,plain,
( e1 != op(e0,e3)
| ~ sP16 ),
inference(cnf_transformation,[],[f140]) ).
fof(f488,plain,
( e2 != op(e3,e3)
| ~ sP15 ),
inference(cnf_transformation,[],[f141]) ).
fof(f493,plain,
( e2 != op(e3,e3)
| ~ sP14 ),
inference(cnf_transformation,[],[f142]) ).
fof(f501,plain,
( e3 != op(e3,e0)
| ~ sP13 ),
inference(cnf_transformation,[],[f143]) ).
fof(f505,plain,
( e3 != op(e1,e3)
| ~ sP12 ),
inference(cnf_transformation,[],[f144]) ).
fof(f509,plain,
( e4 != op(e3,e2)
| ~ sP11 ),
inference(cnf_transformation,[],[f145]) ).
fof(f512,plain,
( e4 != op(e4,e3)
| ~ sP10 ),
inference(cnf_transformation,[],[f146]) ).
fof(f517,plain,
( e0 != op(e4,e4)
| ~ sP9 ),
inference(cnf_transformation,[],[f147]) ).
fof(f522,plain,
( e0 != op(e4,e4)
| ~ sP8 ),
inference(cnf_transformation,[],[f148]) ).
fof(f529,plain,
( e1 != op(e4,e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f149]) ).
fof(f533,plain,
( e1 != op(e3,e4)
| ~ sP6 ),
inference(cnf_transformation,[],[f150]) ).
fof(f541,plain,
( e2 != op(e4,e0)
| ~ sP5 ),
inference(cnf_transformation,[],[f151]) ).
fof(f544,plain,
( e2 != op(e2,e4)
| ~ sP4 ),
inference(cnf_transformation,[],[f152]) ).
fof(f550,plain,
( e3 != op(e4,e1)
| ~ sP3 ),
inference(cnf_transformation,[],[f153]) ).
fof(f556,plain,
( e3 != op(e0,e4)
| ~ sP2 ),
inference(cnf_transformation,[],[f154]) ).
fof(f558,plain,
( e4 != op(e4,e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f155]) ).
fof(f565,plain,
( e4 != op(e1,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f156]) ).
fof(f567,plain,
( e0 = op(e4,e0)
| e1 = op(e4,e1)
| e2 = op(e4,e2)
| e3 = op(e4,e3)
| 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(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl75_102])],[avatar_definition]) ).
fof(f979,plain,
( e3 = op(e4,e3)
| ~ spl75_102 ),
inference(avatar_component_clause,[],[f977]) ).
fof(f981,definition,
( spl75_103
<=> e2 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl75_103])],[avatar_definition]) ).
fof(f983,plain,
( e2 = op(e4,e2)
| ~ spl75_103 ),
inference(avatar_component_clause,[],[f981]) ).
fof(f985,definition,
( spl75_104
<=> e1 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl75_104])],[avatar_definition]) ).
fof(f987,plain,
( e1 = op(e4,e1)
| ~ spl75_104 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f989,definition,
( spl75_105
<=> e0 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl75_105])],[avatar_definition]) ).
fof(f991,plain,
( e0 = op(e4,e0)
| ~ 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(f1036,definition,
( spl75_116
<=> e4 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl75_116])],[avatar_definition]) ).
fof(f1038,plain,
( e4 = op(e1,e4)
| ~ spl75_116 ),
inference(avatar_component_clause,[],[f1036]) ).
fof(f1040,definition,
( spl75_117
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl75_117])],[avatar_definition]) ).
fof(f1042,plain,
( e3 = op(e1,e3)
| ~ spl75_117 ),
inference(avatar_component_clause,[],[f1040]) ).
fof(f1044,definition,
( spl75_118
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl75_118])],[avatar_definition]) ).
fof(f1046,plain,
( e2 = op(e1,e2)
| ~ spl75_118 ),
inference(avatar_component_clause,[],[f1044]) ).
fof(f1048,definition,
( spl75_119
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl75_119])],[avatar_definition]) ).
fof(f1050,plain,
( e1 = op(e1,e1)
| ~ spl75_119 ),
inference(avatar_component_clause,[],[f1048]) ).
fof(f1052,definition,
( spl75_120
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl75_120])],[avatar_definition]) ).
fof(f1054,plain,
( e0 = op(e1,e0)
| ~ spl75_120 ),
inference(avatar_component_clause,[],[f1052]) ).
fof(f1080,plain,
( ~ spl75_26
| ~ spl75_116 ),
inference(avatar_split_clause,[],[f565,f1036,f673]) ).
fof(f1084,definition,
( spl75_126
<=> e4 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl75_126])],[avatar_definition]) ).
fof(f1085,plain,
( e4 = op(e4,e3)
| ~ spl75_126 ),
inference(avatar_component_clause,[],[f1084]) ).
fof(f1087,plain,
( ~ spl75_27
| ~ spl75_126 ),
inference(avatar_split_clause,[],[f558,f1084,f677]) ).
fof(f1124,definition,
( spl75_134
<=> e3 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl75_134])],[avatar_definition]) ).
fof(f1125,plain,
( e3 = op(e0,e4)
| ~ spl75_134 ),
inference(avatar_component_clause,[],[f1124]) ).
fof(f1127,plain,
( ~ spl75_28
| ~ spl75_134 ),
inference(avatar_split_clause,[],[f556,f1124,f681]) ).
fof(f1136,definition,
( spl75_136
<=> e3 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl75_136])],[avatar_definition]) ).
fof(f1137,plain,
( e3 = op(e4,e1)
| ~ spl75_136 ),
inference(avatar_component_clause,[],[f1136]) ).
fof(f1139,plain,
( ~ spl75_29
| ~ spl75_136 ),
inference(avatar_split_clause,[],[f550,f1136,f685]) ).
fof(f1156,definition,
( spl75_140
<=> e2 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl75_140])],[avatar_definition]) ).
fof(f1157,plain,
( e2 = op(e2,e4)
| ~ spl75_140 ),
inference(avatar_component_clause,[],[f1156]) ).
fof(f1159,plain,
( ~ spl75_30
| ~ spl75_140 ),
inference(avatar_split_clause,[],[f544,f1156,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(f1193,definition,
( spl75_147
<=> e1 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl75_147])],[avatar_definition]) ).
fof(f1194,plain,
( e1 = op(e3,e4)
| ~ spl75_147 ),
inference(avatar_component_clause,[],[f1193]) ).
fof(f1196,plain,
( ~ spl75_32
| ~ spl75_147 ),
inference(avatar_split_clause,[],[f533,f1193,f697]) ).
fof(f1219,definition,
( spl75_152
<=> e1 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl75_152])],[avatar_definition]) ).
fof(f1220,plain,
( e1 = op(e4,e2)
| ~ spl75_152 ),
inference(avatar_component_clause,[],[f1219]) ).
fof(f1222,plain,
( ~ spl75_33
| ~ spl75_152 ),
inference(avatar_split_clause,[],[f529,f1219,f701]) ).
fof(f1230,definition,
( spl75_154
<=> e0 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl75_154])],[avatar_definition]) ).
fof(f1231,plain,
( e0 = op(e4,e4)
| ~ spl75_154 ),
inference(avatar_component_clause,[],[f1230]) ).
fof(f1233,plain,
( ~ spl75_34
| ~ spl75_154 ),
inference(avatar_split_clause,[],[f522,f1230,f705]) ).
fof(f1254,plain,
( ~ spl75_35
| ~ spl75_154 ),
inference(avatar_split_clause,[],[f517,f1230,f709]) ).
fof(f1271,plain,
( ~ spl75_36
| ~ spl75_126 ),
inference(avatar_split_clause,[],[f512,f1084,f713]) ).
fof(f1295,definition,
( spl75_166
<=> e4 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl75_166])],[avatar_definition]) ).
fof(f1296,plain,
( e4 = op(e3,e2)
| ~ spl75_166 ),
inference(avatar_component_clause,[],[f1295]) ).
fof(f1298,plain,
( ~ spl75_37
| ~ spl75_166 ),
inference(avatar_split_clause,[],[f509,f1295,f717]) ).
fof(f1312,plain,
( ~ spl75_38
| ~ spl75_117 ),
inference(avatar_split_clause,[],[f505,f1040,f721]) ).
fof(f1327,definition,
( spl75_171
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl75_171])],[avatar_definition]) ).
fof(f1328,plain,
( e3 = op(e3,e0)
| ~ spl75_171 ),
inference(avatar_component_clause,[],[f1327]) ).
fof(f1330,plain,
( ~ spl75_39
| ~ spl75_171 ),
inference(avatar_split_clause,[],[f501,f1327,f725]) ).
fof(f1333,definition,
( spl75_172
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl75_172])],[avatar_definition]) ).
fof(f1334,plain,
( e2 = op(e3,e3)
| ~ spl75_172 ),
inference(avatar_component_clause,[],[f1333]) ).
fof(f1336,plain,
( ~ spl75_40
| ~ spl75_172 ),
inference(avatar_split_clause,[],[f493,f1333,f729]) ).
fof(f1353,plain,
( ~ spl75_41
| ~ spl75_172 ),
inference(avatar_split_clause,[],[f488,f1333,f733]) ).
fof(f1382,definition,
( spl75_181
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl75_181])],[avatar_definition]) ).
fof(f1383,plain,
( e1 = op(e0,e3)
| ~ spl75_181 ),
inference(avatar_component_clause,[],[f1382]) ).
fof(f1385,plain,
( ~ spl75_42
| ~ spl75_181 ),
inference(avatar_split_clause,[],[f486,f1382,f737]) ).
fof(f1386,plain,
( ~ spl75_43
| ~ spl75_147 ),
inference(avatar_split_clause,[],[f477,f1193,f741]) ).
fof(f1406,definition,
( spl75_185
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl75_185])],[avatar_definition]) ).
fof(f1407,plain,
( e0 = op(e2,e3)
| ~ spl75_185 ),
inference(avatar_component_clause,[],[f1406]) ).
fof(f1409,plain,
( ~ spl75_44
| ~ spl75_185 ),
inference(avatar_split_clause,[],[f474,f1406,f745]) ).
fof(f1428,definition,
( spl75_189
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl75_189])],[avatar_definition]) ).
fof(f1429,plain,
( e0 = op(e3,e1)
| ~ spl75_189 ),
inference(avatar_component_clause,[],[f1428]) ).
fof(f1431,plain,
( ~ spl75_45
| ~ spl75_189 ),
inference(avatar_split_clause,[],[f470,f1428,f749]) ).
fof(f1434,plain,
( ~ spl75_46
| ~ spl75_166 ),
inference(avatar_split_clause,[],[f463,f1295,f753]) ).
fof(f1454,definition,
( spl75_193
<=> e4 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl75_193])],[avatar_definition]) ).
fof(f1455,plain,
( e4 = op(e2,e1)
| ~ spl75_193 ),
inference(avatar_component_clause,[],[f1454]) ).
fof(f1457,plain,
( ~ spl75_47
| ~ spl75_193 ),
inference(avatar_split_clause,[],[f460,f1454,f757]) ).
fof(f1466,definition,
( spl75_195
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl75_195])],[avatar_definition]) ).
fof(f1467,plain,
( e3 = op(e2,e2)
| ~ spl75_195 ),
inference(avatar_component_clause,[],[f1466]) ).
fof(f1469,plain,
( ~ spl75_48
| ~ spl75_195 ),
inference(avatar_split_clause,[],[f454,f1466,f761]) ).
fof(f1482,plain,
( ~ spl75_49
| ~ spl75_195 ),
inference(avatar_split_clause,[],[f449,f1466,f765]) ).
fof(f1496,plain,
( ~ spl75_50
| ~ spl75_118 ),
inference(avatar_split_clause,[],[f445,f1044,f769]) ).
fof(f1498,plain,
( ~ spl75_51
| ~ spl75_140 ),
inference(avatar_split_clause,[],[f437,f1156,f773]) ).
fof(f1511,plain,
( ~ spl75_52
| ~ spl75_152 ),
inference(avatar_split_clause,[],[f432,f1219,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(f1550,definition,
( spl75_208
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl75_208])],[avatar_definition]) ).
fof(f1551,plain,
( e0 = op(e0,e2)
| ~ spl75_208 ),
inference(avatar_component_clause,[],[f1550]) ).
fof(f1553,plain,
( ~ spl75_54
| ~ spl75_208 ),
inference(avatar_split_clause,[],[f426,f1550,f785]) ).
fof(f1555,plain,
( ~ spl75_55
| ~ spl75_185 ),
inference(avatar_split_clause,[],[f418,f1406,f789]) ).
fof(f1565,plain,
( ~ spl75_56
| ~ spl75_193 ),
inference(avatar_split_clause,[],[f414,f1454,f793]) ).
fof(f1576,plain,
( ~ spl75_57
| ~ spl75_116 ),
inference(avatar_split_clause,[],[f407,f1036,f797]) ).
fof(f1585,plain,
( ~ spl75_58
| ~ spl75_136 ),
inference(avatar_split_clause,[],[f402,f1136,f801]) ).
fof(f1599,plain,
( ~ spl75_59
| ~ spl75_117 ),
inference(avatar_split_clause,[],[f398,f1040,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(f1622,plain,
( ~ spl75_61
| ~ spl75_118 ),
inference(avatar_split_clause,[],[f389,f1044,f813]) ).
fof(f1632,plain,
( ~ spl75_62
| ~ spl75_119 ),
inference(avatar_split_clause,[],[f385,f1048,f817]) ).
fof(f1637,plain,
( ~ spl75_63
| ~ spl75_119 ),
inference(avatar_split_clause,[],[f380,f1048,f821]) ).
fof(f1644,plain,
( ~ spl75_64
| ~ spl75_189 ),
inference(avatar_split_clause,[],[f373,f1428,f825]) ).
fof(f1660,plain,
( ~ spl75_65
| ~ spl75_120 ),
inference(avatar_split_clause,[],[f371,f1052,f829]) ).
fof(f1666,definition,
( spl75_222
<=> e4 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl75_222])],[avatar_definition]) ).
fof(f1667,plain,
( e4 = op(e0,e0)
| ~ spl75_222 ),
inference(avatar_component_clause,[],[f1666]) ).
fof(f1669,plain,
( ~ spl75_66
| ~ spl75_222 ),
inference(avatar_split_clause,[],[f366,f1666,f833]) ).
fof(f1674,plain,
( ~ spl75_67
| ~ spl75_222 ),
inference(avatar_split_clause,[],[f361,f1666,f837]) ).
fof(f1676,plain,
( ~ spl75_68
| ~ spl75_171 ),
inference(avatar_split_clause,[],[f353,f1327,f841]) ).
fof(f1684,plain,
( ~ spl75_69
| ~ spl75_134 ),
inference(avatar_split_clause,[],[f347,f1124,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_181 ),
inference(avatar_split_clause,[],[f328,f1382,f861]) ).
fof(f1720,plain,
( ~ spl75_74
| ~ spl75_120 ),
inference(avatar_split_clause,[],[f325,f1052,f865]) ).
fof(f1724,plain,
( ~ spl75_75
| ~ spl75_208 ),
inference(avatar_split_clause,[],[f319,f1550,f869]) ).
fof(f1731,plain,
( ~ spl75_76
| ~ spl75_154 ),
inference(avatar_split_clause,[],[f316,f1230,f873]) ).
fof(f1732,plain,
( ~ spl75_77
| ~ spl75_126 ),
inference(avatar_split_clause,[],[f307,f1084,f877]) ).
fof(f1740,plain,
( ~ spl75_78
| ~ spl75_152 ),
inference(avatar_split_clause,[],[f305,f1219,f881]) ).
fof(f1743,plain,
( ~ spl75_79
| ~ spl75_136 ),
inference(avatar_split_clause,[],[f298,f1136,f885]) ).
fof(f1749,plain,
( ~ spl75_80
| ~ spl75_145 ),
inference(avatar_split_clause,[],[f294,f1183,f889]) ).
fof(f1755,plain,
( ~ spl75_81
| ~ spl75_147 ),
inference(avatar_split_clause,[],[f290,f1193,f893]) ).
fof(f1759,plain,
( ~ spl75_82
| ~ spl75_172 ),
inference(avatar_split_clause,[],[f284,f1333,f897]) ).
fof(f1762,plain,
( ~ spl75_83
| ~ spl75_166 ),
inference(avatar_split_clause,[],[f277,f1295,f901]) ).
fof(f1771,plain,
( ~ spl75_84
| ~ spl75_189 ),
inference(avatar_split_clause,[],[f276,f1428,f905]) ).
fof(f1773,plain,
( ~ spl75_85
| ~ spl75_171 ),
inference(avatar_split_clause,[],[f268,f1327,f909]) ).
fof(f1779,plain,
( ~ spl75_86
| ~ spl75_140 ),
inference(avatar_split_clause,[],[f264,f1156,f913]) ).
fof(f1786,plain,
( ~ spl75_87
| ~ spl75_185 ),
inference(avatar_split_clause,[],[f261,f1406,f917]) ).
fof(f1788,plain,
( ~ spl75_88
| ~ spl75_195 ),
inference(avatar_split_clause,[],[f253,f1466,f921]) ).
fof(f1792,plain,
( ~ spl75_89
| ~ spl75_193 ),
inference(avatar_split_clause,[],[f247,f1454,f925]) ).
fof(f1800,plain,
( ~ spl75_90
| ~ spl75_205 ),
inference(avatar_split_clause,[],[f245,f1533,f929]) ).
fof(f1802,plain,
( ~ spl75_91
| ~ spl75_116 ),
inference(avatar_split_clause,[],[f237,f1036,f933]) ).
fof(f1808,plain,
( ~ spl75_92
| ~ spl75_117 ),
inference(avatar_split_clause,[],[f233,f1040,f937]) ).
fof(f1814,plain,
( ~ spl75_93
| ~ spl75_118 ),
inference(avatar_split_clause,[],[f229,f1044,f941]) ).
fof(f1820,plain,
( ~ spl75_94
| ~ spl75_119 ),
inference(avatar_split_clause,[],[f225,f1048,f945]) ).
fof(f1826,plain,
( ~ spl75_95
| ~ spl75_120 ),
inference(avatar_split_clause,[],[f221,f1052,f949]) ).
fof(f1828,plain,
( ~ spl75_96
| ~ spl75_134 ),
inference(avatar_split_clause,[],[f213,f1124,f953]) ).
fof(f1835,plain,
( ~ spl75_97
| ~ spl75_181 ),
inference(avatar_split_clause,[],[f210,f1382,f957]) ).
fof(f1841,plain,
( ~ spl75_98
| ~ spl75_208 ),
inference(avatar_split_clause,[],[f206,f1550,f961]) ).
fof(f1844,plain,
( ~ spl75_99
| ~ spl75_217 ),
inference(avatar_split_clause,[],[f199,f1616,f965]) ).
fof(f1847,plain,
( ~ spl75_100
| ~ spl75_222 ),
inference(avatar_split_clause,[],[f192,f1666,f969]) ).
fof(f1852,plain,
spl75_154,
inference(avatar_split_clause,[],[f167,f1230]) ).
fof(f1853,plain,
spl75_126,
inference(avatar_split_clause,[],[f168,f1084]) ).
fof(f1854,plain,
spl75_152,
inference(avatar_split_clause,[],[f169,f1219]) ).
fof(f1855,plain,
spl75_136,
inference(avatar_split_clause,[],[f170,f1136]) ).
fof(f1856,plain,
spl75_145,
inference(avatar_split_clause,[],[f171,f1183]) ).
fof(f1857,plain,
spl75_147,
inference(avatar_split_clause,[],[f172,f1193]) ).
fof(f1858,plain,
spl75_172,
inference(avatar_split_clause,[],[f173,f1333]) ).
fof(f1859,plain,
spl75_166,
inference(avatar_split_clause,[],[f174,f1295]) ).
fof(f1860,plain,
spl75_189,
inference(avatar_split_clause,[],[f175,f1428]) ).
fof(f1861,plain,
spl75_171,
inference(avatar_split_clause,[],[f176,f1327]) ).
fof(f1862,plain,
spl75_140,
inference(avatar_split_clause,[],[f177,f1156]) ).
fof(f1863,plain,
spl75_185,
inference(avatar_split_clause,[],[f178,f1406]) ).
fof(f1864,plain,
spl75_195,
inference(avatar_split_clause,[],[f179,f1466]) ).
fof(f1865,plain,
spl75_193,
inference(avatar_split_clause,[],[f180,f1454]) ).
fof(f1866,plain,
spl75_205,
inference(avatar_split_clause,[],[f181,f1533]) ).
fof(f1867,plain,
spl75_116,
inference(avatar_split_clause,[],[f182,f1036]) ).
fof(f1868,plain,
spl75_117,
inference(avatar_split_clause,[],[f183,f1040]) ).
fof(f1869,plain,
spl75_118,
inference(avatar_split_clause,[],[f184,f1044]) ).
fof(f1870,plain,
spl75_119,
inference(avatar_split_clause,[],[f185,f1048]) ).
fof(f1871,plain,
spl75_120,
inference(avatar_split_clause,[],[f186,f1052]) ).
fof(f1872,plain,
spl75_134,
inference(avatar_split_clause,[],[f187,f1124]) ).
fof(f1873,plain,
spl75_181,
inference(avatar_split_clause,[],[f188,f1382]) ).
fof(f1874,plain,
spl75_208,
inference(avatar_split_clause,[],[f189,f1550]) ).
fof(f1875,plain,
spl75_217,
inference(avatar_split_clause,[],[f190,f1616]) ).
fof(f1876,plain,
spl75_222,
inference(avatar_split_clause,[],[f191,f1666]) ).
fof(f1877,plain,
( e4 != op(e0,e0)
| spl75_1
| ~ spl75_154 ),
inference(superposition,[],[f575,f1231]) ).
fof(f1878,plain,
( ~ spl75_222
| spl75_1
| ~ spl75_154 ),
inference(avatar_split_clause,[],[f1877,f1230,f573,f1666]) ).
fof(f1880,plain,
( e4 != op(op(e3,e4),e4)
| spl75_2
| ~ spl75_126 ),
inference(forward_demodulation,[],[f579,f1085]) ).
fof(f1882,plain,
( e4 != op(e1,e4)
| spl75_2
| ~ spl75_126
| ~ spl75_147 ),
inference(forward_demodulation,[],[f1880,f1194]) ).
fof(f1883,plain,
( $false
| spl75_2
| ~ spl75_116
| ~ spl75_126
| ~ spl75_147 ),
inference(forward_subsumption_resolution,[],[f1882,f1038]) ).
fof(f1884,plain,
( spl75_2
| ~ spl75_116
| ~ spl75_126
| ~ spl75_147 ),
inference(avatar_contradiction_clause,[],[f1883]) ).
fof(f1886,plain,
( e4 != op(op(e2,e4),e1)
| spl75_3
| ~ spl75_152 ),
inference(forward_demodulation,[],[f583,f1220]) ).
fof(f1888,plain,
( e4 != op(e2,e1)
| spl75_3
| ~ spl75_140
| ~ spl75_152 ),
inference(forward_demodulation,[],[f1886,f1157]) ).
fof(f1889,plain,
( ~ spl75_193
| spl75_3
| ~ spl75_140
| ~ spl75_152 ),
inference(avatar_split_clause,[],[f1888,f1219,f1156,f581,f1454]) ).
fof(f1891,plain,
( e4 != op(op(e1,e4),e3)
| spl75_4
| ~ spl75_136 ),
inference(forward_demodulation,[],[f587,f1137]) ).
fof(f1893,plain,
( e4 != op(e4,e3)
| spl75_4
| ~ spl75_116
| ~ spl75_136 ),
inference(forward_demodulation,[],[f1891,f1038]) ).
fof(f1895,plain,
( $false
| spl75_4
| ~ spl75_116
| ~ spl75_126
| ~ spl75_136 ),
inference(forward_subsumption_resolution,[],[f1893,f1085]) ).
fof(f1896,plain,
( spl75_4
| ~ spl75_116
| ~ spl75_126
| ~ spl75_136 ),
inference(avatar_contradiction_clause,[],[f1895]) ).
fof(f1898,plain,
( e4 != op(op(e0,e4),e2)
| spl75_5
| ~ spl75_145 ),
inference(forward_demodulation,[],[f591,f1184]) ).
fof(f1900,plain,
( e4 != op(e3,e2)
| spl75_5
| ~ spl75_134
| ~ spl75_145 ),
inference(forward_demodulation,[],[f1898,f1125]) ).
fof(f1901,plain,
( ~ spl75_166
| spl75_5
| ~ spl75_134
| ~ spl75_145 ),
inference(avatar_split_clause,[],[f1900,f1183,f1124,f589,f1295]) ).
fof(f1903,plain,
( e3 != op(op(e4,e3),e1)
| spl75_6
| ~ spl75_147 ),
inference(forward_demodulation,[],[f595,f1194]) ).
fof(f1905,plain,
( e3 != op(e4,e1)
| spl75_6
| ~ spl75_126
| ~ spl75_147 ),
inference(forward_demodulation,[],[f1903,f1085]) ).
fof(f1907,plain,
( $false
| spl75_6
| ~ spl75_126
| ~ spl75_136
| ~ spl75_147 ),
inference(forward_subsumption_resolution,[],[f1905,f1137]) ).
fof(f1908,plain,
( spl75_6
| ~ spl75_126
| ~ spl75_136
| ~ spl75_147 ),
inference(avatar_contradiction_clause,[],[f1907]) ).
fof(f1911,plain,
( e3 != op(e2,e2)
| spl75_7
| ~ spl75_172 ),
inference(superposition,[],[f599,f1334]) ).
fof(f1912,plain,
( ~ spl75_195
| spl75_7
| ~ spl75_172 ),
inference(avatar_split_clause,[],[f1911,f1333,f597,f1466]) ).
fof(f1914,plain,
( e3 != op(op(e2,e3),e4)
| spl75_8
| ~ spl75_166 ),
inference(forward_demodulation,[],[f603,f1296]) ).
fof(f1916,plain,
( e3 != op(e0,e4)
| spl75_8
| ~ spl75_166
| ~ spl75_185 ),
inference(superposition,[],[f1914,f1407]) ).
fof(f1917,plain,
( $false
| spl75_8
| ~ spl75_134
| ~ spl75_166
| ~ spl75_185 ),
inference(forward_subsumption_resolution,[],[f1916,f1125]) ).
fof(f1918,plain,
( spl75_8
| ~ spl75_134
| ~ spl75_166
| ~ spl75_185 ),
inference(avatar_contradiction_clause,[],[f1917]) ).
fof(f1920,plain,
( e3 != op(e3,op(e3,e1))
| spl75_9
| ~ spl75_117 ),
inference(forward_demodulation,[],[f607,f1042]) ).
fof(f1922,plain,
( e3 != op(e3,e0)
| spl75_9
| ~ spl75_117
| ~ spl75_189 ),
inference(superposition,[],[f1920,f1429]) ).
fof(f1923,plain,
( $false
| spl75_9
| ~ spl75_117
| ~ spl75_171
| ~ spl75_189 ),
inference(forward_subsumption_resolution,[],[f1922,f1328]) ).
fof(f1924,plain,
( spl75_9
| ~ spl75_117
| ~ spl75_171
| ~ spl75_189 ),
inference(avatar_contradiction_clause,[],[f1923]) ).
fof(f1926,plain,
( e3 != op(op(e0,e3),e3)
| spl75_10
| ~ spl75_171 ),
inference(forward_demodulation,[],[f611,f1328]) ).
fof(f1928,plain,
( e3 != op(e1,e3)
| spl75_10
| ~ spl75_171
| ~ spl75_181 ),
inference(forward_demodulation,[],[f1926,f1383]) ).
fof(f1929,plain,
( $false
| spl75_10
| ~ spl75_117
| ~ spl75_171
| ~ spl75_181 ),
inference(forward_subsumption_resolution,[],[f1928,f1042]) ).
fof(f1930,plain,
( spl75_10
| ~ spl75_117
| ~ spl75_171
| ~ spl75_181 ),
inference(avatar_contradiction_clause,[],[f1929]) ).
fof(f1932,plain,
( e2 != op(op(e4,e2),e2)
| spl75_11
| ~ spl75_140 ),
inference(forward_demodulation,[],[f615,f1157]) ).
fof(f1934,plain,
( e2 != op(e1,e2)
| spl75_11
| ~ spl75_140
| ~ spl75_152 ),
inference(forward_demodulation,[],[f1932,f1220]) ).
fof(f1935,plain,
( $false
| spl75_11
| ~ spl75_118
| ~ spl75_140
| ~ spl75_152 ),
inference(forward_subsumption_resolution,[],[f1934,f1046]) ).
fof(f1936,plain,
( spl75_11
| ~ spl75_118
| ~ spl75_140
| ~ spl75_152 ),
inference(avatar_contradiction_clause,[],[f1935]) ).
fof(f1938,plain,
( e2 != op(op(e3,e2),e0)
| spl75_12
| ~ spl75_185 ),
inference(forward_demodulation,[],[f619,f1407]) ).
fof(f1940,plain,
( e2 != op(e4,e0)
| spl75_12
| ~ spl75_166
| ~ spl75_185 ),
inference(forward_demodulation,[],[f1938,f1296]) ).
fof(f1941,plain,
( $false
| spl75_12
| ~ spl75_145
| ~ spl75_166
| ~ spl75_185 ),
inference(forward_subsumption_resolution,[],[f1940,f1184]) ).
fof(f1942,plain,
( spl75_12
| ~ spl75_145
| ~ spl75_166
| ~ spl75_185 ),
inference(avatar_contradiction_clause,[],[f1941]) ).
fof(f1945,plain,
( e2 != op(e3,e3)
| spl75_13
| ~ spl75_195 ),
inference(superposition,[],[f623,f1467]) ).
fof(f1946,plain,
( $false
| spl75_13
| ~ spl75_172
| ~ spl75_195 ),
inference(forward_subsumption_resolution,[],[f1945,f1334]) ).
fof(f1947,plain,
( spl75_13
| ~ spl75_172
| ~ spl75_195 ),
inference(avatar_contradiction_clause,[],[f1946]) ).
fof(f1949,plain,
( e2 != op(op(e1,e2),e4)
| spl75_14
| ~ spl75_193 ),
inference(forward_demodulation,[],[f627,f1455]) ).
fof(f1950,plain,
( e2 != op(e2,e4)
| spl75_14
| ~ spl75_118
| ~ spl75_193 ),
inference(forward_demodulation,[],[f1949,f1046]) ).
fof(f1951,plain,
( $false
| spl75_14
| ~ spl75_118
| ~ spl75_140
| ~ spl75_193 ),
inference(forward_subsumption_resolution,[],[f1950,f1157]) ).
fof(f1952,plain,
( spl75_14
| ~ spl75_118
| ~ spl75_140
| ~ spl75_193 ),
inference(avatar_contradiction_clause,[],[f1951]) ).
fof(f1956,plain,
( e2 != op(e0,op(e2,e0))
| spl75_15
| ~ spl75_208 ),
inference(superposition,[],[f631,f1551]) ).
fof(f1957,plain,
( e2 != op(e0,e1)
| spl75_15
| ~ spl75_205
| ~ spl75_208 ),
inference(forward_demodulation,[],[f1956,f1534]) ).
fof(f1958,plain,
( ~ spl75_217
| spl75_15
| ~ spl75_205
| ~ spl75_208 ),
inference(avatar_split_clause,[],[f1957,f1550,f1533,f629,f1616]) ).
fof(f1960,plain,
( e1 != op(op(e4,e1),e4)
| spl75_16
| ~ spl75_116 ),
inference(forward_demodulation,[],[f635,f1038]) ).
fof(f1962,plain,
( e1 != op(e3,e4)
| spl75_16
| ~ spl75_116
| ~ spl75_136 ),
inference(forward_demodulation,[],[f1960,f1137]) ).
fof(f1964,plain,
( $false
| spl75_16
| ~ spl75_116
| ~ spl75_136
| ~ spl75_147 ),
inference(forward_subsumption_resolution,[],[f1962,f1194]) ).
fof(f1965,plain,
( spl75_16
| ~ spl75_116
| ~ spl75_136
| ~ spl75_147 ),
inference(avatar_contradiction_clause,[],[f1964]) ).
fof(f1967,plain,
( e1 != op(op(e3,e1),e3)
| spl75_17
| ~ spl75_117 ),
inference(forward_demodulation,[],[f639,f1042]) ).
fof(f1969,plain,
( e1 != op(e0,e3)
| spl75_17
| ~ spl75_117
| ~ spl75_189 ),
inference(forward_demodulation,[],[f1967,f1429]) ).
fof(f1970,plain,
( $false
| spl75_17
| ~ spl75_117
| ~ spl75_181
| ~ spl75_189 ),
inference(forward_subsumption_resolution,[],[f1969,f1383]) ).
fof(f1971,plain,
( spl75_17
| ~ spl75_117
| ~ spl75_181
| ~ spl75_189 ),
inference(avatar_contradiction_clause,[],[f1970]) ).
fof(f1973,plain,
( e1 != op(op(e2,e1),e2)
| spl75_18
| ~ spl75_118 ),
inference(forward_demodulation,[],[f643,f1046]) ).
fof(f1975,plain,
( e1 != op(e4,e2)
| spl75_18
| ~ spl75_118
| ~ spl75_193 ),
inference(forward_demodulation,[],[f1973,f1455]) ).
fof(f1976,plain,
( $false
| spl75_18
| ~ spl75_118
| ~ spl75_152
| ~ spl75_193 ),
inference(forward_subsumption_resolution,[],[f1975,f1220]) ).
fof(f1977,plain,
( spl75_18
| ~ spl75_118
| ~ spl75_152
| ~ spl75_193 ),
inference(avatar_contradiction_clause,[],[f1976]) ).
fof(f1979,plain,
( e1 != op(e1,e1)
| spl75_19
| ~ spl75_119 ),
inference(forward_demodulation,[],[f647,f1050]) ).
fof(f1981,plain,
( $false
| spl75_19
| ~ spl75_119 ),
inference(forward_subsumption_resolution,[],[f1979,f1050]) ).
fof(f1982,plain,
( spl75_19
| ~ spl75_119 ),
inference(avatar_contradiction_clause,[],[f1981]) ).
fof(f1984,plain,
( e1 != op(op(e0,e1),e0)
| spl75_20
| ~ spl75_120 ),
inference(forward_demodulation,[],[f651,f1054]) ).
fof(f1985,plain,
( e1 != op(e2,e0)
| spl75_20
| ~ spl75_120
| ~ spl75_217 ),
inference(superposition,[],[f1984,f1617]) ).
fof(f1986,plain,
( $false
| spl75_20
| ~ spl75_120
| ~ spl75_205
| ~ spl75_217 ),
inference(forward_subsumption_resolution,[],[f1985,f1534]) ).
fof(f1987,plain,
( spl75_20
| ~ spl75_120
| ~ spl75_205
| ~ spl75_217 ),
inference(avatar_contradiction_clause,[],[f1986]) ).
fof(f1989,plain,
( e0 != op(op(e4,e0),e3)
| spl75_21
| ~ spl75_134 ),
inference(forward_demodulation,[],[f655,f1125]) ).
fof(f1991,plain,
( e0 != op(e2,e3)
| spl75_21
| ~ spl75_134
| ~ spl75_145 ),
inference(forward_demodulation,[],[f1989,f1184]) ).
fof(f1992,plain,
( $false
| spl75_21
| ~ spl75_134
| ~ spl75_145
| ~ spl75_185 ),
inference(forward_subsumption_resolution,[],[f1991,f1407]) ).
fof(f1993,plain,
( spl75_21
| ~ spl75_134
| ~ spl75_145
| ~ spl75_185 ),
inference(avatar_contradiction_clause,[],[f1992]) ).
fof(f1995,plain,
( e0 != op(op(e3,e0),e1)
| spl75_22
| ~ spl75_181 ),
inference(forward_demodulation,[],[f659,f1383]) ).
fof(f1997,plain,
( e0 != op(e3,e1)
| spl75_22
| ~ spl75_171
| ~ spl75_181 ),
inference(forward_demodulation,[],[f1995,f1328]) ).
fof(f1998,plain,
( $false
| spl75_22
| ~ spl75_171
| ~ spl75_181
| ~ spl75_189 ),
inference(forward_subsumption_resolution,[],[f1997,f1429]) ).
fof(f1999,plain,
( spl75_22
| ~ spl75_171
| ~ spl75_181
| ~ spl75_189 ),
inference(avatar_contradiction_clause,[],[f1998]) ).
fof(f2001,plain,
( e0 != op(op(e2,e0),e0)
| spl75_23
| ~ spl75_208 ),
inference(forward_demodulation,[],[f663,f1551]) ).
fof(f2003,plain,
( e0 != op(e1,e0)
| spl75_23
| ~ spl75_205
| ~ spl75_208 ),
inference(forward_demodulation,[],[f2001,f1534]) ).
fof(f2004,plain,
( $false
| spl75_23
| ~ spl75_120
| ~ spl75_205
| ~ spl75_208 ),
inference(forward_subsumption_resolution,[],[f2003,f1054]) ).
fof(f2005,plain,
( spl75_23
| ~ spl75_120
| ~ spl75_205
| ~ spl75_208 ),
inference(avatar_contradiction_clause,[],[f2004]) ).
fof(f2007,plain,
( e0 != op(op(e1,e0),e2)
| spl75_24
| ~ spl75_217 ),
inference(forward_demodulation,[],[f667,f1617]) ).
fof(f2009,plain,
( e0 != op(e0,e2)
| spl75_24
| ~ spl75_120
| ~ spl75_217 ),
inference(forward_demodulation,[],[f2007,f1054]) ).
fof(f2010,plain,
( $false
| spl75_24
| ~ spl75_120
| ~ spl75_208
| ~ spl75_217 ),
inference(forward_subsumption_resolution,[],[f2009,f1551]) ).
fof(f2011,plain,
( spl75_24
| ~ spl75_120
| ~ spl75_208
| ~ spl75_217 ),
inference(avatar_contradiction_clause,[],[f2010]) ).
fof(f2014,plain,
( e0 != op(e4,e4)
| spl75_25
| ~ spl75_222 ),
inference(superposition,[],[f671,f1667]) ).
fof(f2015,plain,
( $false
| spl75_25
| ~ spl75_154
| ~ spl75_222 ),
inference(forward_subsumption_resolution,[],[f2014,f1231]) ).
fof(f2016,plain,
( spl75_25
| ~ spl75_154
| ~ spl75_222 ),
inference(avatar_contradiction_clause,[],[f2015]) ).
fof(f2046,plain,
( e3 = e4
| ~ spl75_102
| ~ spl75_126 ),
inference(superposition,[],[f979,f1085]) ).
fof(f2050,plain,
( $false
| ~ spl75_102
| ~ spl75_126 ),
inference(forward_subsumption_resolution,[],[f2046,f157]) ).
fof(f2051,plain,
( ~ spl75_102
| ~ spl75_126 ),
inference(avatar_contradiction_clause,[],[f2050]) ).
fof(f2053,plain,
( e1 = e2
| ~ spl75_103
| ~ spl75_152 ),
inference(forward_demodulation,[],[f983,f1220]) ).
fof(f2054,plain,
( $false
| ~ spl75_103
| ~ spl75_152 ),
inference(forward_subsumption_resolution,[],[f2053,f162]) ).
fof(f2055,plain,
( ~ spl75_103
| ~ spl75_152 ),
inference(avatar_contradiction_clause,[],[f2054]) ).
fof(f2057,plain,
( e1 = e3
| ~ spl75_104
| ~ spl75_136 ),
inference(superposition,[],[f987,f1137]) ).
fof(f2061,plain,
( $false
| ~ spl75_104
| ~ spl75_136 ),
inference(forward_subsumption_resolution,[],[f2057,f161]) ).
fof(f2062,plain,
( ~ spl75_104
| ~ spl75_136 ),
inference(avatar_contradiction_clause,[],[f2061]) ).
fof(f2064,plain,
( e0 = e2
| ~ spl75_105
| ~ spl75_145 ),
inference(superposition,[],[f991,f1184]) ).
fof(f2068,plain,
( $false
| ~ spl75_105
| ~ spl75_145 ),
inference(forward_subsumption_resolution,[],[f2064,f165]) ).
fof(f2069,plain,
( ~ spl75_105
| ~ spl75_145 ),
inference(avatar_contradiction_clause,[],[f2068]) ).
fof(f2070,plain,
( e0 = e4
| ~ spl75_101
| ~ spl75_154 ),
inference(forward_demodulation,[],[f975,f1231]) ).
fof(f2072,plain,
( $false
| ~ spl75_101
| ~ spl75_154 ),
inference(forward_subsumption_resolution,[],[f2070,f163]) ).
fof(f2073,plain,
( ~ spl75_101
| ~ spl75_154 ),
inference(avatar_contradiction_clause,[],[f2072]) ).
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(s9,plain,
( ~ spl75_26
| ~ spl75_116 ),
inference(sat_conversion,[],[f1080]) ).
cnf(s12,plain,
( ~ spl75_27
| ~ spl75_126 ),
inference(sat_conversion,[],[f1087]) ).
cnf(s20,plain,
( ~ spl75_28
| ~ spl75_134 ),
inference(sat_conversion,[],[f1127]) ).
cnf(s24,plain,
( ~ spl75_29
| ~ spl75_136 ),
inference(sat_conversion,[],[f1139]) ).
cnf(s28,plain,
( ~ spl75_30
| ~ spl75_140 ),
inference(sat_conversion,[],[f1159]) ).
cnf(s35,plain,
( ~ spl75_31
| ~ spl75_145 ),
inference(sat_conversion,[],[f1186]) ).
cnf(s37,plain,
( ~ spl75_32
| ~ spl75_147 ),
inference(sat_conversion,[],[f1196]) ).
cnf(s43,plain,
( ~ spl75_33
| ~ spl75_152 ),
inference(sat_conversion,[],[f1222]) ).
cnf(s46,plain,
( ~ spl75_34
| ~ spl75_154 ),
inference(sat_conversion,[],[f1233]) ).
cnf(s51,plain,
( ~ spl75_35
| ~ spl75_154 ),
inference(sat_conversion,[],[f1254]) ).
cnf(s56,plain,
( ~ spl75_36
| ~ spl75_126 ),
inference(sat_conversion,[],[f1271]) ).
cnf(s63,plain,
( ~ spl75_37
| ~ spl75_166 ),
inference(sat_conversion,[],[f1298]) ).
cnf(s69,plain,
( ~ spl75_38
| ~ spl75_117 ),
inference(sat_conversion,[],[f1312]) ).
cnf(s75,plain,
( ~ spl75_39
| ~ spl75_171 ),
inference(sat_conversion,[],[f1330]) ).
cnf(s77,plain,
( ~ spl75_40
| ~ spl75_172 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s82,plain,
( ~ spl75_41
| ~ spl75_172 ),
inference(sat_conversion,[],[f1353]) ).
cnf(s90,plain,
( ~ spl75_42
| ~ spl75_181 ),
inference(sat_conversion,[],[f1385]) ).
cnf(s91,plain,
( ~ spl75_43
| ~ spl75_147 ),
inference(sat_conversion,[],[f1386]) ).
cnf(s98,plain,
( ~ spl75_44
| ~ spl75_185 ),
inference(sat_conversion,[],[f1409]) ).
cnf(s104,plain,
( ~ spl75_45
| ~ spl75_189 ),
inference(sat_conversion,[],[f1431]) ).
cnf(s107,plain,
( ~ spl75_46
| ~ spl75_166 ),
inference(sat_conversion,[],[f1434]) ).
cnf(s114,plain,
( ~ spl75_47
| ~ spl75_193 ),
inference(sat_conversion,[],[f1457]) ).
cnf(s118,plain,
( ~ spl75_48
| ~ spl75_195 ),
inference(sat_conversion,[],[f1469]) ).
cnf(s123,plain,
( ~ spl75_49
| ~ spl75_195 ),
inference(sat_conversion,[],[f1482]) ).
cnf(s129,plain,
( ~ spl75_50
| ~ spl75_118 ),
inference(sat_conversion,[],[f1496]) ).
cnf(s131,plain,
( ~ spl75_51
| ~ spl75_140 ),
inference(sat_conversion,[],[f1498]) ).
cnf(s136,plain,
( ~ spl75_52
| ~ spl75_152 ),
inference(sat_conversion,[],[f1511]) ).
cnf(s145,plain,
( ~ spl75_53
| ~ spl75_205 ),
inference(sat_conversion,[],[f1536]) ).
cnf(s150,plain,
( ~ spl75_54
| ~ spl75_208 ),
inference(sat_conversion,[],[f1553]) ).
cnf(s152,plain,
( ~ spl75_55
| ~ spl75_185 ),
inference(sat_conversion,[],[f1555]) ).
cnf(s158,plain,
( ~ spl75_56
| ~ spl75_193 ),
inference(sat_conversion,[],[f1565]) ).
cnf(s161,plain,
( ~ spl75_57
| ~ spl75_116 ),
inference(sat_conversion,[],[f1576]) ).
cnf(s166,plain,
( ~ spl75_58
| ~ spl75_136 ),
inference(sat_conversion,[],[f1585]) ).
cnf(s172,plain,
( ~ spl75_59
| ~ spl75_117 ),
inference(sat_conversion,[],[f1599]) ).
cnf(s180,plain,
( ~ spl75_60
| ~ spl75_217 ),
inference(sat_conversion,[],[f1619]) ).
cnf(s183,plain,
( ~ spl75_61
| ~ spl75_118 ),
inference(sat_conversion,[],[f1622]) ).
cnf(s189,plain,
( ~ spl75_62
| ~ spl75_119 ),
inference(sat_conversion,[],[f1632]) ).
cnf(s194,plain,
( ~ spl75_63
| ~ spl75_119 ),
inference(sat_conversion,[],[f1637]) ).
cnf(s197,plain,
( ~ spl75_64
| ~ spl75_189 ),
inference(sat_conversion,[],[f1644]) ).
cnf(s205,plain,
( ~ spl75_65
| ~ spl75_120 ),
inference(sat_conversion,[],[f1660]) ).
cnf(s210,plain,
( ~ spl75_66
| ~ spl75_222 ),
inference(sat_conversion,[],[f1669]) ).
cnf(s215,plain,
( ~ spl75_67
| ~ spl75_222 ),
inference(sat_conversion,[],[f1674]) ).
cnf(s217,plain,
( ~ spl75_68
| ~ spl75_171 ),
inference(sat_conversion,[],[f1676]) ).
cnf(s221,plain,
( ~ spl75_69
| ~ spl75_134 ),
inference(sat_conversion,[],[f1684]) ).
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_181 ),
inference(sat_conversion,[],[f1713]) ).
cnf(s249,plain,
( ~ spl75_74
| ~ spl75_120 ),
inference(sat_conversion,[],[f1720]) ).
cnf(s253,plain,
( ~ spl75_75
| ~ spl75_208 ),
inference(sat_conversion,[],[f1724]) ).
cnf(s260,plain,
( ~ spl75_76
| ~ spl75_154 ),
inference(sat_conversion,[],[f1731]) ).
cnf(s261,plain,
( ~ spl75_77
| ~ spl75_126 ),
inference(sat_conversion,[],[f1732]) ).
cnf(s269,plain,
( ~ spl75_78
| ~ spl75_152 ),
inference(sat_conversion,[],[f1740]) ).
cnf(s272,plain,
( ~ spl75_79
| ~ spl75_136 ),
inference(sat_conversion,[],[f1743]) ).
cnf(s278,plain,
( ~ spl75_80
| ~ spl75_145 ),
inference(sat_conversion,[],[f1749]) ).
cnf(s284,plain,
( ~ spl75_81
| ~ spl75_147 ),
inference(sat_conversion,[],[f1755]) ).
cnf(s288,plain,
( ~ spl75_82
| ~ spl75_172 ),
inference(sat_conversion,[],[f1759]) ).
cnf(s291,plain,
( ~ spl75_83
| ~ spl75_166 ),
inference(sat_conversion,[],[f1762]) ).
cnf(s300,plain,
( ~ spl75_84
| ~ spl75_189 ),
inference(sat_conversion,[],[f1771]) ).
cnf(s302,plain,
( ~ spl75_85
| ~ spl75_171 ),
inference(sat_conversion,[],[f1773]) ).
cnf(s308,plain,
( ~ spl75_86
| ~ spl75_140 ),
inference(sat_conversion,[],[f1779]) ).
cnf(s315,plain,
( ~ spl75_87
| ~ spl75_185 ),
inference(sat_conversion,[],[f1786]) ).
cnf(s317,plain,
( ~ spl75_88
| ~ spl75_195 ),
inference(sat_conversion,[],[f1788]) ).
cnf(s321,plain,
( ~ spl75_89
| ~ spl75_193 ),
inference(sat_conversion,[],[f1792]) ).
cnf(s329,plain,
( ~ spl75_90
| ~ spl75_205 ),
inference(sat_conversion,[],[f1800]) ).
cnf(s331,plain,
( ~ spl75_91
| ~ spl75_116 ),
inference(sat_conversion,[],[f1802]) ).
cnf(s337,plain,
( ~ spl75_92
| ~ spl75_117 ),
inference(sat_conversion,[],[f1808]) ).
cnf(s343,plain,
( ~ spl75_93
| ~ spl75_118 ),
inference(sat_conversion,[],[f1814]) ).
cnf(s349,plain,
( ~ spl75_94
| ~ spl75_119 ),
inference(sat_conversion,[],[f1820]) ).
cnf(s355,plain,
( ~ spl75_95
| ~ spl75_120 ),
inference(sat_conversion,[],[f1826]) ).
cnf(s357,plain,
( ~ spl75_96
| ~ spl75_134 ),
inference(sat_conversion,[],[f1828]) ).
cnf(s364,plain,
( ~ spl75_97
| ~ spl75_181 ),
inference(sat_conversion,[],[f1835]) ).
cnf(s370,plain,
( ~ spl75_98
| ~ spl75_208 ),
inference(sat_conversion,[],[f1841]) ).
cnf(s373,plain,
( ~ spl75_99
| ~ spl75_217 ),
inference(sat_conversion,[],[f1844]) ).
cnf(s376,plain,
( ~ spl75_100
| ~ spl75_222 ),
inference(sat_conversion,[],[f1847]) ).
cnf(s381,plain,
spl75_154,
inference(sat_conversion,[],[f1852]) ).
cnf(s382,plain,
spl75_126,
inference(sat_conversion,[],[f1853]) ).
cnf(s383,plain,
spl75_152,
inference(sat_conversion,[],[f1854]) ).
cnf(s384,plain,
spl75_136,
inference(sat_conversion,[],[f1855]) ).
cnf(s385,plain,
spl75_145,
inference(sat_conversion,[],[f1856]) ).
cnf(s386,plain,
spl75_147,
inference(sat_conversion,[],[f1857]) ).
cnf(s387,plain,
spl75_172,
inference(sat_conversion,[],[f1858]) ).
cnf(s388,plain,
spl75_166,
inference(sat_conversion,[],[f1859]) ).
cnf(s389,plain,
spl75_189,
inference(sat_conversion,[],[f1860]) ).
cnf(s390,plain,
spl75_171,
inference(sat_conversion,[],[f1861]) ).
cnf(s391,plain,
spl75_140,
inference(sat_conversion,[],[f1862]) ).
cnf(s392,plain,
spl75_185,
inference(sat_conversion,[],[f1863]) ).
cnf(s393,plain,
spl75_195,
inference(sat_conversion,[],[f1864]) ).
cnf(s394,plain,
spl75_193,
inference(sat_conversion,[],[f1865]) ).
cnf(s395,plain,
spl75_205,
inference(sat_conversion,[],[f1866]) ).
cnf(s396,plain,
spl75_116,
inference(sat_conversion,[],[f1867]) ).
cnf(s397,plain,
spl75_117,
inference(sat_conversion,[],[f1868]) ).
cnf(s398,plain,
spl75_118,
inference(sat_conversion,[],[f1869]) ).
cnf(s399,plain,
spl75_119,
inference(sat_conversion,[],[f1870]) ).
cnf(s400,plain,
spl75_120,
inference(sat_conversion,[],[f1871]) ).
cnf(s401,plain,
spl75_134,
inference(sat_conversion,[],[f1872]) ).
cnf(s402,plain,
spl75_181,
inference(sat_conversion,[],[f1873]) ).
cnf(s403,plain,
spl75_208,
inference(sat_conversion,[],[f1874]) ).
cnf(s404,plain,
spl75_217,
inference(sat_conversion,[],[f1875]) ).
cnf(s405,plain,
spl75_222,
inference(sat_conversion,[],[f1876]) ).
cnf(s406,plain,
( spl75_1
| ~ spl75_154
| ~ spl75_222 ),
inference(sat_conversion,[],[f1878]) ).
cnf(s408,plain,
( spl75_2
| ~ spl75_116
| ~ spl75_126
| ~ spl75_147 ),
inference(sat_conversion,[],[f1884]) ).
cnf(s409,plain,
( spl75_3
| ~ spl75_140
| ~ spl75_152
| ~ spl75_193 ),
inference(sat_conversion,[],[f1889]) ).
cnf(s411,plain,
( spl75_4
| ~ spl75_116
| ~ spl75_126
| ~ spl75_136 ),
inference(sat_conversion,[],[f1896]) ).
cnf(s412,plain,
( spl75_5
| ~ spl75_134
| ~ spl75_145
| ~ spl75_166 ),
inference(sat_conversion,[],[f1901]) ).
cnf(s414,plain,
( spl75_6
| ~ spl75_126
| ~ spl75_136
| ~ spl75_147 ),
inference(sat_conversion,[],[f1908]) ).
cnf(s415,plain,
( spl75_7
| ~ spl75_172
| ~ spl75_195 ),
inference(sat_conversion,[],[f1912]) ).
cnf(s417,plain,
( spl75_8
| ~ spl75_134
| ~ spl75_166
| ~ spl75_185 ),
inference(sat_conversion,[],[f1918]) ).
cnf(s418,plain,
( spl75_9
| ~ spl75_117
| ~ spl75_171
| ~ spl75_189 ),
inference(sat_conversion,[],[f1924]) ).
cnf(s419,plain,
( spl75_10
| ~ spl75_117
| ~ spl75_171
| ~ spl75_181 ),
inference(sat_conversion,[],[f1930]) ).
cnf(s420,plain,
( spl75_11
| ~ spl75_118
| ~ spl75_140
| ~ spl75_152 ),
inference(sat_conversion,[],[f1936]) ).
cnf(s421,plain,
( spl75_12
| ~ spl75_145
| ~ spl75_166
| ~ spl75_185 ),
inference(sat_conversion,[],[f1942]) ).
cnf(s422,plain,
( spl75_13
| ~ spl75_172
| ~ spl75_195 ),
inference(sat_conversion,[],[f1947]) ).
cnf(s423,plain,
( spl75_14
| ~ spl75_118
| ~ spl75_140
| ~ spl75_193 ),
inference(sat_conversion,[],[f1952]) ).
cnf(s424,plain,
( spl75_15
| ~ spl75_205
| ~ spl75_208
| ~ spl75_217 ),
inference(sat_conversion,[],[f1958]) ).
cnf(s426,plain,
( spl75_16
| ~ spl75_116
| ~ spl75_136
| ~ spl75_147 ),
inference(sat_conversion,[],[f1965]) ).
cnf(s427,plain,
( spl75_17
| ~ spl75_117
| ~ spl75_181
| ~ spl75_189 ),
inference(sat_conversion,[],[f1971]) ).
cnf(s428,plain,
( spl75_18
| ~ spl75_118
| ~ spl75_152
| ~ spl75_193 ),
inference(sat_conversion,[],[f1977]) ).
cnf(s429,plain,
( spl75_19
| ~ spl75_119 ),
inference(sat_conversion,[],[f1982]) ).
cnf(s430,plain,
( spl75_20
| ~ spl75_120
| ~ spl75_205
| ~ spl75_217 ),
inference(sat_conversion,[],[f1987]) ).
cnf(s431,plain,
( spl75_21
| ~ spl75_134
| ~ spl75_145
| ~ spl75_185 ),
inference(sat_conversion,[],[f1993]) ).
cnf(s432,plain,
( spl75_22
| ~ spl75_171
| ~ spl75_181
| ~ spl75_189 ),
inference(sat_conversion,[],[f1999]) ).
cnf(s433,plain,
( spl75_23
| ~ spl75_120
| ~ spl75_205
| ~ spl75_208 ),
inference(sat_conversion,[],[f2005]) ).
cnf(s434,plain,
( spl75_24
| ~ spl75_120
| ~ spl75_208
| ~ spl75_217 ),
inference(sat_conversion,[],[f2011]) ).
cnf(s435,plain,
( spl75_25
| ~ spl75_154
| ~ spl75_222 ),
inference(sat_conversion,[],[f2016]) ).
cnf(s444,plain,
( ~ spl75_102
| ~ spl75_126 ),
inference(sat_conversion,[],[f2051]) ).
cnf(s445,plain,
( ~ spl75_103
| ~ spl75_152 ),
inference(sat_conversion,[],[f2055]) ).
cnf(s447,plain,
( ~ spl75_104
| ~ spl75_136 ),
inference(sat_conversion,[],[f2062]) ).
cnf(s449,plain,
( ~ spl75_105
| ~ spl75_145 ),
inference(sat_conversion,[],[f2069]) ).
cnf(s450,plain,
( ~ spl75_101
| ~ spl75_154 ),
inference(sat_conversion,[],[f2073]) ).
cnf(s454,plain,
spl75_24,
inference(rat,[],[s434,s404,s403,s400]) ).
cnf(s455,plain,
spl75_19,
inference(rat,[],[s429,s399]) ).
cnf(s456,plain,
spl75_15,
inference(rat,[],[s424,s404,s403,s395]) ).
cnf(s457,plain,
spl75_23,
inference(rat,[],[s433,s403,s400,s395]) ).
cnf(s458,plain,
spl75_20,
inference(rat,[],[s430,s404,s400,s395]) ).
cnf(s461,plain,
spl75_14,
inference(rat,[],[s423,s394,s398,s391]) ).
cnf(s462,plain,
spl75_10,
inference(rat,[],[s419,s402,s397,s390]) ).
cnf(s463,plain,
spl75_17,
inference(rat,[],[s427,s397,s402,s389]) ).
cnf(s464,plain,
spl75_22,
inference(rat,[],[s432,s390,s402,s389]) ).
cnf(s465,plain,
spl75_9,
inference(rat,[],[s418,s390,s397,s389]) ).
cnf(s466,plain,
spl75_8,
inference(rat,[],[s417,s392,s401,s388]) ).
cnf(s468,plain,
spl75_13,
inference(rat,[],[s422,s393,s387]) ).
cnf(s469,plain,
spl75_7,
inference(rat,[],[s415,s393,s387]) ).
cnf(s471,plain,
~ spl75_105,
inference(rat,[],[s449,s385]) ).
cnf(s472,plain,
spl75_12,
inference(rat,[],[s421,s392,s388,s385]) ).
cnf(s473,plain,
spl75_21,
inference(rat,[],[s431,s392,s401,s385]) ).
cnf(s474,plain,
spl75_5,
inference(rat,[],[s412,s388,s401,s385]) ).
cnf(s475,plain,
~ spl75_104,
inference(rat,[],[s447,s384]) ).
cnf(s476,plain,
spl75_16,
inference(rat,[],[s426,s386,s396,s384]) ).
cnf(s477,plain,
~ spl75_103,
inference(rat,[],[s445,s383]) ).
cnf(s478,plain,
spl75_18,
inference(rat,[],[s428,s394,s398,s383]) ).
cnf(s479,plain,
spl75_3,
inference(rat,[],[s409,s394,s391,s383]) ).
cnf(s480,plain,
spl75_11,
inference(rat,[],[s420,s391,s398,s383]) ).
cnf(s481,plain,
~ spl75_102,
inference(rat,[],[s444,s382]) ).
cnf(s482,plain,
spl75_6,
inference(rat,[],[s414,s386,s384,s382]) ).
cnf(s483,plain,
spl75_4,
inference(rat,[],[s411,s384,s396,s382]) ).
cnf(s484,plain,
spl75_2,
inference(rat,[],[s408,s386,s396,s382]) ).
cnf(s485,plain,
~ spl75_101,
inference(rat,[],[s450,s381]) ).
cnf(s486,plain,
spl75_25,
inference(rat,[],[s435,s405,s381]) ).
cnf(s487,plain,
spl75_1,
inference(rat,[],[s406,s405,s381]) ).
cnf(s488,plain,
~ spl75_100,
inference(rat,[],[s376,s405]) ).
cnf(s489,plain,
~ spl75_99,
inference(rat,[],[s373,s404]) ).
cnf(s490,plain,
~ spl75_98,
inference(rat,[],[s370,s403]) ).
cnf(s491,plain,
~ spl75_97,
inference(rat,[],[s364,s402]) ).
cnf(s492,plain,
~ spl75_96,
inference(rat,[],[s357,s401]) ).
cnf(s493,plain,
~ spl75_95,
inference(rat,[],[s355,s400]) ).
cnf(s494,plain,
~ spl75_94,
inference(rat,[],[s349,s399]) ).
cnf(s495,plain,
~ spl75_93,
inference(rat,[],[s343,s398]) ).
cnf(s496,plain,
~ spl75_92,
inference(rat,[],[s337,s397]) ).
cnf(s497,plain,
~ spl75_91,
inference(rat,[],[s331,s396]) ).
cnf(s498,plain,
~ spl75_90,
inference(rat,[],[s329,s395]) ).
cnf(s499,plain,
~ spl75_89,
inference(rat,[],[s321,s394]) ).
cnf(s500,plain,
~ spl75_88,
inference(rat,[],[s317,s393]) ).
cnf(s501,plain,
~ spl75_87,
inference(rat,[],[s315,s392]) ).
cnf(s502,plain,
~ spl75_86,
inference(rat,[],[s308,s391]) ).
cnf(s503,plain,
~ spl75_85,
inference(rat,[],[s302,s390]) ).
cnf(s504,plain,
~ spl75_84,
inference(rat,[],[s300,s389]) ).
cnf(s505,plain,
~ spl75_83,
inference(rat,[],[s291,s388]) ).
cnf(s506,plain,
~ spl75_82,
inference(rat,[],[s288,s387]) ).
cnf(s507,plain,
~ spl75_81,
inference(rat,[],[s284,s386]) ).
cnf(s508,plain,
~ spl75_80,
inference(rat,[],[s278,s385]) ).
cnf(s509,plain,
~ spl75_79,
inference(rat,[],[s272,s384]) ).
cnf(s510,plain,
~ spl75_78,
inference(rat,[],[s269,s383]) ).
cnf(s511,plain,
~ spl75_77,
inference(rat,[],[s261,s382]) ).
cnf(s512,plain,
~ spl75_76,
inference(rat,[],[s260,s381]) ).
cnf(s513,plain,
~ spl75_75,
inference(rat,[],[s253,s403]) ).
cnf(s514,plain,
~ spl75_74,
inference(rat,[],[s249,s400]) ).
cnf(s515,plain,
~ spl75_73,
inference(rat,[],[s242,s402]) ).
cnf(s516,plain,
~ spl75_72,
inference(rat,[],[s238,s395]) ).
cnf(s517,plain,
~ spl75_71,
inference(rat,[],[s234,s404]) ).
cnf(s518,plain,
~ spl75_70,
inference(rat,[],[s226,s385]) ).
cnf(s519,plain,
~ spl75_69,
inference(rat,[],[s221,s401]) ).
cnf(s520,plain,
~ spl75_68,
inference(rat,[],[s217,s390]) ).
cnf(s521,plain,
~ spl75_67,
inference(rat,[],[s215,s405]) ).
cnf(s522,plain,
~ spl75_66,
inference(rat,[],[s210,s405]) ).
cnf(s523,plain,
~ spl75_65,
inference(rat,[],[s205,s400]) ).
cnf(s524,plain,
~ spl75_64,
inference(rat,[],[s197,s389]) ).
cnf(s525,plain,
~ spl75_63,
inference(rat,[],[s194,s399]) ).
cnf(s526,plain,
~ spl75_62,
inference(rat,[],[s189,s399]) ).
cnf(s527,plain,
~ spl75_61,
inference(rat,[],[s183,s398]) ).
cnf(s528,plain,
~ spl75_60,
inference(rat,[],[s180,s404]) ).
cnf(s529,plain,
~ spl75_59,
inference(rat,[],[s172,s397]) ).
cnf(s530,plain,
~ spl75_58,
inference(rat,[],[s166,s384]) ).
cnf(s531,plain,
~ spl75_57,
inference(rat,[],[s161,s396]) ).
cnf(s532,plain,
~ spl75_56,
inference(rat,[],[s158,s394]) ).
cnf(s533,plain,
~ spl75_55,
inference(rat,[],[s152,s392]) ).
cnf(s534,plain,
~ spl75_54,
inference(rat,[],[s150,s403]) ).
cnf(s535,plain,
~ spl75_53,
inference(rat,[],[s145,s395]) ).
cnf(s536,plain,
~ spl75_52,
inference(rat,[],[s136,s383]) ).
cnf(s537,plain,
~ spl75_51,
inference(rat,[],[s131,s391]) ).
cnf(s538,plain,
~ spl75_50,
inference(rat,[],[s129,s398]) ).
cnf(s539,plain,
~ spl75_49,
inference(rat,[],[s123,s393]) ).
cnf(s540,plain,
~ spl75_48,
inference(rat,[],[s118,s393]) ).
cnf(s541,plain,
~ spl75_47,
inference(rat,[],[s114,s394]) ).
cnf(s542,plain,
~ spl75_46,
inference(rat,[],[s107,s388]) ).
cnf(s543,plain,
~ spl75_45,
inference(rat,[],[s104,s389]) ).
cnf(s544,plain,
~ spl75_44,
inference(rat,[],[s98,s392]) ).
cnf(s545,plain,
~ spl75_43,
inference(rat,[],[s91,s386]) ).
cnf(s546,plain,
~ spl75_42,
inference(rat,[],[s90,s402]) ).
cnf(s547,plain,
~ spl75_41,
inference(rat,[],[s82,s387]) ).
cnf(s548,plain,
~ spl75_40,
inference(rat,[],[s77,s387]) ).
cnf(s549,plain,
~ spl75_39,
inference(rat,[],[s75,s390]) ).
cnf(s550,plain,
~ spl75_38,
inference(rat,[],[s69,s397]) ).
cnf(s551,plain,
~ spl75_37,
inference(rat,[],[s63,s388]) ).
cnf(s552,plain,
~ spl75_36,
inference(rat,[],[s56,s382]) ).
cnf(s553,plain,
~ spl75_35,
inference(rat,[],[s51,s381]) ).
cnf(s554,plain,
~ spl75_34,
inference(rat,[],[s46,s381]) ).
cnf(s555,plain,
~ spl75_33,
inference(rat,[],[s43,s383]) ).
cnf(s556,plain,
~ spl75_32,
inference(rat,[],[s37,s386]) ).
cnf(s557,plain,
~ spl75_31,
inference(rat,[],[s35,s385]) ).
cnf(s558,plain,
~ spl75_30,
inference(rat,[],[s28,s391]) ).
cnf(s559,plain,
~ spl75_29,
inference(rat,[],[s24,s384]) ).
cnf(s560,plain,
~ spl75_28,
inference(rat,[],[s20,s401]) ).
cnf(s561,plain,
~ spl75_27,
inference(rat,[],[s12,s382]) ).
cnf(s562,plain,
~ spl75_26,
inference(rat,[],[s9,s396]) ).
cnf(s566,plain,
$false,
inference(rat,[],[s1,s471,s475,s477,s481,s485,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,s560,s561,s562,s486,s454,s457,s464,s473,s458,s455,s478,s463,s476,s456,s461,s468,s472,s480,s462,s465,s466,s469,s482,s474,s483,s479,s484,s487]) ).
fof(f2074,plain,
$false,
inference(avatar_sat_refutation,[],[s566]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG187+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n008.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 19:41:25 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.93/1.12 % (2554358)Detected formulas, will run a generic FOF schedule.
% 2.93/1.12 % (2554366)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3737095332:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.93/1.12 % (2554366)Instruction limit reached!
% 2.93/1.12 % (2554366)------------------------------
% 2.93/1.12 % (2554366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.93/1.12 % (2554366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/1.12 % (2554366)CaDiCaL version: 2.1.3
% 2.93/1.12 % (2554366)Termination reason: Instruction limit
% 2.93/1.12 % (2554366)Termination phase: Saturation
% 2.93/1.12 % (2554366)Time elapsed: 0.026 s
% 2.93/1.12 % (2554366)Peak memory usage: 89 MB
% 2.93/1.12 % (2554366)Instructions burned: 114 (million)
% 2.93/1.12 % (2554363)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=3720108086:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.93/1.12 % (2554364)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=3511293007:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.93/1.12 % (2554369)dis-21_1_sil=8000:lcm=predicate:random_seed=1455841209: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.93/1.12 % (2554367)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1285775762:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.93/1.12 % (2554368)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3106274806:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.93/1.12 % (2554365)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=2891990597:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.93/1.12 % (2554369)Refutation not found, incomplete strategy
% 2.93/1.12 % (2554369)------------------------------
% 2.93/1.12 % (2554369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.93/1.12 % (2554369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/1.12 % (2554369)CaDiCaL version: 2.1.3
% 2.93/1.12 % (2554369)Termination reason: Refutation not found, incomplete strategy
% 2.93/1.12 % (2554369)Time elapsed: 0.010 s
% 2.93/1.12 % (2554369)Peak memory usage: 89 MB
% 2.93/1.12 % (2554369)Instructions burned: 20 (million)
% 2.93/1.12 % (2554368)First to succeed.
% 2.93/1.12 % (2554367)Also succeeded, but the first one will report.
% 2.93/1.12 % (2554368)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2554358"
% 2.93/1.12 % (2554371)lrs+10_1_sil=8000:sp=occurrence:random_seed=3063230547:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 2.93/1.12 % (2554371)Also succeeded, but the first one will report.
% 2.93/1.12 % (2554369)------------------------------
% 2.93/1.12 % (2554369)------------------------------
% 2.93/1.12 % (2554368)Refutation found. Thanks to Tanya!
% 2.93/1.12 % SZS status Theorem for theBenchmark
% 2.93/1.12 % SZS output start Proof for theBenchmark
% See solution above
% 3.80/1.32 % (2554368)------------------------------
% 3.80/1.32 % (2554368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.80/1.32 % (2554368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.80/1.32 % (2554368)CaDiCaL version: 2.1.3
% 3.80/1.32 % (2554368)Termination reason: Refutation
% 3.80/1.32 % (2554368)Time elapsed: 0.030 s
% 3.80/1.32 % (2554368)Peak memory usage: 90 MB
% 3.80/1.32 % (2554368)Instructions burned: 62 (million)
% 3.80/1.32 % (2554368)------------------------------
% 3.80/1.32 % (2554368)------------------------------
% 3.80/1.32 % (2554358)Success in time 0.446 s
% 3.80/1.32 % Vampire exiting
%------------------------------------------------------------------------------