%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG063+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:09:25 AM UTC 2026
% Result : Theorem 4.00s 1.31s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 164
% Syntax : Number of formulae : 1298 ( 82 unt; 158 def)
% Number of atoms : 4293 (1482 equ)
% Maximal formula atoms : 250 ( 3 avg)
% Number of connectives : 4770 (1775 ~;2498 |; 363 &)
% ( 134 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 54 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 160 ( 158 usr; 159 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e4 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e4 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3
| op(e0,e2) = e4 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3
| op(e0,e3) = e4 )
& ( op(e0,e4) = e0
| op(e0,e4) = e1
| op(e0,e4) = e2
| op(e0,e4) = e3
| op(e0,e4) = e4 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3
| op(e1,e0) = e4 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3
| op(e1,e1) = e4 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3
| op(e1,e2) = e4 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3
| op(e1,e3) = e4 )
& ( op(e1,e4) = e0
| op(e1,e4) = e1
| op(e1,e4) = e2
| op(e1,e4) = e3
| op(e1,e4) = e4 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3
| op(e2,e0) = e4 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3
| op(e2,e1) = e4 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3
| op(e2,e2) = e4 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3
| op(e2,e3) = e4 )
& ( op(e2,e4) = e0
| op(e2,e4) = e1
| op(e2,e4) = e2
| op(e2,e4) = e3
| op(e2,e4) = e4 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3
| op(e3,e0) = e4 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3
| op(e3,e1) = e4 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3
| op(e3,e2) = e4 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3
| op(e3,e3) = e4 )
& ( op(e3,e4) = e0
| op(e3,e4) = e1
| op(e3,e4) = e2
| op(e3,e4) = e3
| op(e3,e4) = e4 )
& ( op(e4,e0) = e0
| op(e4,e0) = e1
| op(e4,e0) = e2
| op(e4,e0) = e3
| op(e4,e0) = e4 )
& ( op(e4,e1) = e0
| op(e4,e1) = e1
| op(e4,e1) = e2
| op(e4,e1) = e3
| op(e4,e1) = e4 )
& ( op(e4,e2) = e0
| op(e4,e2) = e1
| op(e4,e2) = e2
| op(e4,e2) = e3
| op(e4,e2) = e4 )
& ( op(e4,e3) = e0
| op(e4,e3) = e1
| op(e4,e3) = e2
| op(e4,e3) = e3
| op(e4,e3) = e4 )
& ( op(e4,e4) = e0
| op(e4,e4) = e1
| op(e4,e4) = e2
| op(e4,e4) = e3
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& op(unit,e4) = e4
& op(e4,unit) = e4
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3
| unit = e4 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0
| op(e0,e4) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0
| op(e4,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| op(e0,e4) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e4,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| op(e0,e4) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2
| op(e4,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3
| op(e0,e4) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3
| op(e4,e0) = e3 )
& ( op(e0,e0) = e4
| op(e0,e1) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e4) = e4 )
& ( op(e0,e0) = e4
| op(e1,e0) = e4
| op(e2,e0) = e4
| op(e3,e0) = e4
| op(e4,e0) = e4 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0
| op(e1,e4) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0
| op(e4,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1
| op(e1,e4) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1
| op(e4,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2
| op(e1,e4) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| op(e4,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3
| op(e1,e4) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3
| op(e4,e1) = e3 )
& ( op(e1,e0) = e4
| op(e1,e1) = e4
| op(e1,e2) = e4
| op(e1,e3) = e4
| op(e1,e4) = e4 )
& ( op(e0,e1) = e4
| op(e1,e1) = e4
| op(e2,e1) = e4
| op(e3,e1) = e4
| op(e4,e1) = e4 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0
| op(e2,e4) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0
| op(e4,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1
| op(e2,e4) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1
| op(e4,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2
| op(e2,e4) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2
| op(e4,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| op(e2,e4) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3
| op(e4,e2) = e3 )
& ( op(e2,e0) = e4
| op(e2,e1) = e4
| op(e2,e2) = e4
| op(e2,e3) = e4
| op(e2,e4) = e4 )
& ( op(e0,e2) = e4
| op(e1,e2) = e4
| op(e2,e2) = e4
| op(e3,e2) = e4
| op(e4,e2) = e4 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0
| op(e3,e4) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0
| op(e4,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1
| op(e3,e4) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1
| op(e4,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| op(e3,e4) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2
| op(e4,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3
| op(e3,e4) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3
| op(e4,e3) = e3 )
& ( op(e3,e0) = e4
| op(e3,e1) = e4
| op(e3,e2) = e4
| op(e3,e3) = e4
| op(e3,e4) = e4 )
& ( op(e0,e3) = e4
| op(e1,e3) = e4
| op(e2,e3) = e4
| op(e3,e3) = e4
| op(e4,e3) = e4 )
& ( op(e4,e0) = e0
| op(e4,e1) = e0
| op(e4,e2) = e0
| op(e4,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e4) = e0
| op(e1,e4) = e0
| op(e2,e4) = e0
| op(e3,e4) = e0
| op(e4,e4) = e0 )
& ( op(e4,e0) = e1
| op(e4,e1) = e1
| op(e4,e2) = e1
| op(e4,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e4) = e1
| op(e1,e4) = e1
| op(e2,e4) = e1
| op(e3,e4) = e1
| op(e4,e4) = e1 )
& ( op(e4,e0) = e2
| op(e4,e1) = e2
| op(e4,e2) = e2
| op(e4,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e4) = e2
| op(e1,e4) = e2
| op(e2,e4) = e2
| op(e3,e4) = e2
| op(e4,e4) = e2 )
& ( op(e4,e0) = e3
| op(e4,e1) = e3
| op(e4,e2) = e3
| op(e4,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e4) = e3
| op(e1,e4) = e3
| op(e2,e4) = e3
| op(e3,e4) = e3
| op(e4,e4) = e3 )
& ( op(e4,e0) = e4
| op(e4,e1) = e4
| op(e4,e2) = e4
| op(e4,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e4) = e4
| op(e1,e4) = e4
| op(e2,e4) = e4
| op(e3,e4) = e4
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f5,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e0 != e4
& e1 != e2
& e1 != e3
& e1 != e4
& e2 != e3
& e2 != e4
& e3 != e4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( e0 = op(e1,op(op(e1,e1),op(e1,e1)))
& e2 = op(op(e1,e1),op(e1,e1))
& e3 = op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1)))
& e4 = op(e1,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f7,conjecture,
~ ( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f8,negated_conjecture,
~ ~ ( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 ) ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f9,plain,
( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 ) ) ),
inference(flattening,[],[f8]) ).
fof(f10,definition,
( ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11,definition,
( ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f12,definition,
( ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f13,definition,
( ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f17,definition,
( ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f18,definition,
( ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f19,definition,
( ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f20,definition,
( ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f21,definition,
( ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f22,definition,
( ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f25,definition,
( ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f26,definition,
( ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f27,definition,
( ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f29,definition,
( ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f30,definition,
( ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f31,definition,
( ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f32,definition,
( ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f33,definition,
( ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ~ sP23 ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f34,plain,
( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ) ),
inference(definition_folding,[],[f9,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10]) ).
fof(f35,plain,
( ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ~ sP23 ),
inference(nnf_transformation,[],[f33]) ).
fof(f36,plain,
( ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ~ sP22 ),
inference(nnf_transformation,[],[f32]) ).
fof(f37,plain,
( ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ~ sP21 ),
inference(nnf_transformation,[],[f31]) ).
fof(f38,plain,
( ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ~ sP20 ),
inference(nnf_transformation,[],[f30]) ).
fof(f39,plain,
( ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ~ sP19 ),
inference(nnf_transformation,[],[f29]) ).
fof(f40,plain,
( ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ~ sP18 ),
inference(nnf_transformation,[],[f28]) ).
fof(f41,plain,
( ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ~ sP17 ),
inference(nnf_transformation,[],[f27]) ).
fof(f42,plain,
( ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ~ sP16 ),
inference(nnf_transformation,[],[f26]) ).
fof(f43,plain,
( ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ~ sP15 ),
inference(nnf_transformation,[],[f25]) ).
fof(f44,plain,
( ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ~ sP14 ),
inference(nnf_transformation,[],[f24]) ).
fof(f45,plain,
( ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ~ sP13 ),
inference(nnf_transformation,[],[f23]) ).
fof(f46,plain,
( ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ~ sP12 ),
inference(nnf_transformation,[],[f22]) ).
fof(f47,plain,
( ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ~ sP11 ),
inference(nnf_transformation,[],[f21]) ).
fof(f48,plain,
( ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ~ sP10 ),
inference(nnf_transformation,[],[f20]) ).
fof(f49,plain,
( ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ~ sP9 ),
inference(nnf_transformation,[],[f19]) ).
fof(f50,plain,
( ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ~ sP8 ),
inference(nnf_transformation,[],[f18]) ).
fof(f51,plain,
( ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ~ sP7 ),
inference(nnf_transformation,[],[f17]) ).
fof(f52,plain,
( ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ~ sP6 ),
inference(nnf_transformation,[],[f16]) ).
fof(f53,plain,
( ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ~ sP5 ),
inference(nnf_transformation,[],[f15]) ).
fof(f54,plain,
( ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ~ sP4 ),
inference(nnf_transformation,[],[f14]) ).
fof(f55,plain,
( ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ~ sP3 ),
inference(nnf_transformation,[],[f13]) ).
fof(f56,plain,
( ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ~ sP2 ),
inference(nnf_transformation,[],[f12]) ).
fof(f57,plain,
( ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ~ sP1 ),
inference(nnf_transformation,[],[f11]) ).
fof(f58,plain,
( ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 )
| ~ sP0 ),
inference(nnf_transformation,[],[f10]) ).
fof(f60,plain,
( e0 = op(e1,e1)
| ~ sP23 ),
inference(cnf_transformation,[],[f35]) ).
fof(f63,plain,
( e0 = op(e2,e2)
| ~ sP22 ),
inference(cnf_transformation,[],[f36]) ).
fof(f64,plain,
( op(e0,e0) = e2
| ~ sP22 ),
inference(cnf_transformation,[],[f36]) ).
fof(f65,plain,
( e0 != op(e0,e3)
| ~ sP21 ),
inference(cnf_transformation,[],[f37]) ).
fof(f67,plain,
( op(e0,e0) = e3
| ~ sP21 ),
inference(cnf_transformation,[],[f37]) ).
fof(f69,plain,
( e0 = op(e4,e4)
| ~ sP20 ),
inference(cnf_transformation,[],[f38]) ).
fof(f70,plain,
( op(e0,e0) = e4
| ~ sP20 ),
inference(cnf_transformation,[],[f38]) ).
fof(f73,plain,
( e0 = op(e1,e1)
| ~ sP19 ),
inference(cnf_transformation,[],[f39]) ).
fof(f76,plain,
( e1 = op(e1,e1)
| ~ sP18 ),
inference(cnf_transformation,[],[f40]) ).
fof(f79,plain,
( e2 = op(e1,e1)
| ~ sP17 ),
inference(cnf_transformation,[],[f41]) ).
fof(f82,plain,
( e3 = op(e1,e1)
| ~ sP16 ),
inference(cnf_transformation,[],[f42]) ).
fof(f84,plain,
( e1 = op(e4,e4)
| ~ sP15 ),
inference(cnf_transformation,[],[f43]) ).
fof(f86,plain,
( e2 != op(e2,e0)
| ~ sP14 ),
inference(cnf_transformation,[],[f44]) ).
fof(f87,plain,
( op(e0,e0) = e2
| ~ sP14 ),
inference(cnf_transformation,[],[f44]) ).
fof(f88,plain,
( e0 = op(e2,e2)
| ~ sP14 ),
inference(cnf_transformation,[],[f44]) ).
fof(f90,plain,
( e2 = op(e1,e1)
| ~ sP13 ),
inference(cnf_transformation,[],[f45]) ).
fof(f92,plain,
( e2 != op(e2,e2)
| ~ sP12 ),
inference(cnf_transformation,[],[f46]) ).
fof(f94,plain,
( e2 = op(e2,e2)
| ~ sP12 ),
inference(cnf_transformation,[],[f46]) ).
fof(f95,plain,
( e2 != op(e2,e3)
| ~ sP11 ),
inference(cnf_transformation,[],[f47]) ).
fof(f96,plain,
( e2 = op(e3,e3)
| ~ sP11 ),
inference(cnf_transformation,[],[f47]) ).
fof(f97,plain,
( e3 = op(e2,e2)
| ~ sP11 ),
inference(cnf_transformation,[],[f47]) ).
fof(f99,plain,
( e2 = op(e4,e4)
| ~ sP10 ),
inference(cnf_transformation,[],[f48]) ).
fof(f100,plain,
( e4 = op(e2,e2)
| ~ sP10 ),
inference(cnf_transformation,[],[f48]) ).
fof(f102,plain,
( op(e0,e0) = e3
| ~ sP9 ),
inference(cnf_transformation,[],[f49]) ).
fof(f103,plain,
( e0 = op(e3,e3)
| ~ sP9 ),
inference(cnf_transformation,[],[f49]) ).
fof(f105,plain,
( e3 = op(e1,e1)
| ~ sP8 ),
inference(cnf_transformation,[],[f50]) ).
fof(f108,plain,
( e3 = op(e2,e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f51]) ).
fof(f109,plain,
( e2 = op(e3,e3)
| ~ sP7 ),
inference(cnf_transformation,[],[f51]) ).
fof(f110,plain,
( e3 != op(e3,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f52]) ).
fof(f112,plain,
( e3 = op(e3,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f52]) ).
fof(f114,plain,
( e3 = op(e4,e4)
| ~ sP5 ),
inference(cnf_transformation,[],[f53]) ).
fof(f115,plain,
( e4 = op(e3,e3)
| ~ sP5 ),
inference(cnf_transformation,[],[f53]) ).
fof(f117,plain,
( op(e0,e0) = e4
| ~ sP4 ),
inference(cnf_transformation,[],[f54]) ).
fof(f118,plain,
( e0 = op(e4,e4)
| ~ sP4 ),
inference(cnf_transformation,[],[f54]) ).
fof(f121,plain,
( e1 = op(e4,e4)
| ~ sP3 ),
inference(cnf_transformation,[],[f55]) ).
fof(f123,plain,
( e4 = op(e2,e2)
| ~ sP2 ),
inference(cnf_transformation,[],[f56]) ).
fof(f124,plain,
( e2 = op(e4,e4)
| ~ sP2 ),
inference(cnf_transformation,[],[f56]) ).
fof(f125,plain,
( e4 != op(e4,e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f57]) ).
fof(f126,plain,
( e4 = op(e3,e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f57]) ).
fof(f127,plain,
( e3 = op(e4,e4)
| ~ sP1 ),
inference(cnf_transformation,[],[f57]) ).
fof(f128,plain,
( e4 != op(e4,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f58]) ).
fof(f130,plain,
( e4 = op(e4,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f58]) ).
fof(f131,plain,
( e0 != op(e0,e0)
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f34]) ).
fof(f133,plain,
( e0 = op(e0,e0)
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f34]) ).
fof(f135,plain,
( op(e0,e0) = e3
| e3 = op(e1,e1)
| e3 = op(e2,e2)
| e3 = op(e3,e3)
| e3 = op(e4,e4) ),
inference(cnf_transformation,[],[f34]) ).
fof(f136,plain,
( op(e0,e0) = e2
| e2 = op(e1,e1)
| e2 = op(e2,e2)
| e2 = op(e3,e3)
| e2 = op(e4,e4) ),
inference(cnf_transformation,[],[f34]) ).
fof(f137,plain,
( op(e0,e0) = e1
| e1 = op(e1,e1)
| e1 = op(e2,e2)
| e1 = op(e3,e3)
| e1 = op(e4,e4) ),
inference(cnf_transformation,[],[f34]) ).
fof(f138,plain,
( e0 = op(e0,e0)
| e0 = op(e1,e1)
| e0 = op(e2,e2)
| e0 = op(e3,e3)
| e0 = op(e4,e4) ),
inference(cnf_transformation,[],[f34]) ).
fof(f139,plain,
e4 = op(e1,e1),
inference(cnf_transformation,[],[f6]) ).
fof(f141,plain,
e2 = op(op(e1,e1),op(e1,e1)),
inference(cnf_transformation,[],[f6]) ).
fof(f142,plain,
e0 = op(e1,op(op(e1,e1),op(e1,e1))),
inference(cnf_transformation,[],[f6]) ).
fof(f143,plain,
e3 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f144,plain,
e2 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f145,plain,
e2 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f146,plain,
e1 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f147,plain,
e1 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f148,plain,
e1 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f149,plain,
e0 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f150,plain,
e0 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f151,plain,
e0 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f152,plain,
e0 != e1,
inference(cnf_transformation,[],[f5]) ).
fof(f255,plain,
( e3 = op(e0,e4)
| e3 = op(e1,e4)
| e3 = op(e2,e4)
| e3 = op(e3,e4)
| e3 = op(e4,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f256,plain,
( e3 = op(e4,e0)
| e3 = op(e4,e1)
| e3 = op(e4,e2)
| e3 = op(e4,e3)
| e3 = op(e4,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f257,plain,
( e2 = op(e0,e4)
| e2 = op(e1,e4)
| e2 = op(e2,e4)
| e2 = op(e3,e4)
| e2 = op(e4,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f258,plain,
( e2 = op(e4,e0)
| e2 = op(e4,e1)
| e2 = op(e4,e2)
| e2 = op(e4,e3)
| e2 = op(e4,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f261,plain,
( e0 = op(e0,e4)
| e0 = op(e1,e4)
| e0 = op(e2,e4)
| e0 = op(e3,e4)
| e0 = op(e4,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f262,plain,
( e0 = op(e4,e0)
| e0 = op(e4,e1)
| e0 = op(e4,e2)
| e0 = op(e4,e3)
| e0 = op(e4,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f263,plain,
( e4 = op(e0,e3)
| e4 = op(e1,e3)
| e4 = op(e2,e3)
| e4 = op(e3,e3)
| e4 = op(e4,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f264,plain,
( e4 = op(e3,e0)
| e4 = op(e3,e1)
| e4 = op(e3,e2)
| e4 = op(e3,e3)
| e4 = op(e3,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f271,plain,
( e0 = op(e0,e3)
| e0 = op(e1,e3)
| e0 = op(e2,e3)
| e0 = op(e3,e3)
| e0 = op(e4,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f272,plain,
( e0 = op(e3,e0)
| e0 = op(e3,e1)
| e0 = op(e3,e2)
| e0 = op(e3,e3)
| e0 = op(e3,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f273,plain,
( e4 = op(e0,e2)
| e4 = op(e1,e2)
| e4 = op(e2,e2)
| e4 = op(e3,e2)
| e4 = op(e4,e2) ),
inference(cnf_transformation,[],[f3]) ).
fof(f274,plain,
( e4 = op(e2,e0)
| e4 = op(e2,e1)
| e4 = op(e2,e2)
| e4 = op(e2,e3)
| e4 = op(e2,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f275,plain,
( e3 = op(e0,e2)
| e3 = op(e1,e2)
| e3 = op(e2,e2)
| e3 = op(e3,e2)
| e3 = op(e4,e2) ),
inference(cnf_transformation,[],[f3]) ).
fof(f276,plain,
( e3 = op(e2,e0)
| e3 = op(e2,e1)
| e3 = op(e2,e2)
| e3 = op(e2,e3)
| e3 = op(e2,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f279,plain,
( e1 = op(e0,e2)
| e1 = op(e1,e2)
| e1 = op(e2,e2)
| e1 = op(e3,e2)
| e1 = op(e4,e2) ),
inference(cnf_transformation,[],[f3]) ).
fof(f280,plain,
( e1 = op(e2,e0)
| e1 = op(e2,e1)
| e1 = op(e2,e2)
| e1 = op(e2,e3)
| e1 = op(e2,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f282,plain,
( e0 = op(e2,e0)
| e0 = op(e2,e1)
| e0 = op(e2,e2)
| e0 = op(e2,e3)
| e0 = op(e2,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f285,plain,
( e3 = op(e0,e1)
| e3 = op(e1,e1)
| e3 = op(e2,e1)
| e3 = op(e3,e1)
| e3 = op(e4,e1) ),
inference(cnf_transformation,[],[f3]) ).
fof(f286,plain,
( e3 = op(e1,e0)
| e3 = op(e1,e1)
| e3 = op(e1,e2)
| e3 = op(e1,e3)
| e3 = op(e1,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f287,plain,
( e2 = op(e0,e1)
| e2 = op(e1,e1)
| e2 = op(e2,e1)
| e2 = op(e3,e1)
| e2 = op(e4,e1) ),
inference(cnf_transformation,[],[f3]) ).
fof(f288,plain,
( e2 = op(e1,e0)
| e2 = op(e1,e1)
| e2 = op(e1,e2)
| e2 = op(e1,e3)
| e2 = op(e1,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f291,plain,
( e0 = op(e0,e1)
| e0 = op(e1,e1)
| e0 = op(e2,e1)
| e0 = op(e3,e1)
| e0 = op(e4,e1) ),
inference(cnf_transformation,[],[f3]) ).
fof(f295,plain,
( op(e0,e0) = e3
| e3 = op(e1,e0)
| e3 = op(e2,e0)
| e3 = op(e3,e0)
| e3 = op(e4,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f296,plain,
( op(e0,e0) = e3
| e3 = op(e0,e1)
| e3 = op(e0,e2)
| e3 = op(e0,e3)
| e3 = op(e0,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f303,plain,
( e0 = unit
| e1 = unit
| e2 = unit
| e3 = unit
| e4 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f304,plain,
e4 = op(e4,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f305,plain,
e4 = op(unit,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f306,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f307,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f308,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f309,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f310,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f311,plain,
e1 = op(unit,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f312,plain,
e0 = op(e0,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f314,plain,
( e0 = op(e4,e4)
| e1 = op(e4,e4)
| e2 = op(e4,e4)
| e3 = op(e4,e4)
| e4 = op(e4,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f340,definition,
( spl24_1
<=> e4 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl24_1])],[avatar_definition]) ).
fof(f342,plain,
( e4 = op(e4,e4)
| ~ spl24_1 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f344,definition,
( spl24_2
<=> e3 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl24_2])],[avatar_definition]) ).
fof(f346,plain,
( e3 = op(e4,e4)
| ~ spl24_2 ),
inference(avatar_component_clause,[],[f344]) ).
fof(f348,definition,
( spl24_3
<=> e2 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl24_3])],[avatar_definition]) ).
fof(f350,plain,
( e2 = op(e4,e4)
| ~ spl24_3 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f352,definition,
( spl24_4
<=> e1 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl24_4])],[avatar_definition]) ).
fof(f354,plain,
( e1 = op(e4,e4)
| ~ spl24_4 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f356,definition,
( spl24_5
<=> e0 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl24_5])],[avatar_definition]) ).
fof(f358,plain,
( e0 = op(e4,e4)
| ~ spl24_5 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f359,plain,
( spl24_1
| spl24_2
| spl24_3
| spl24_4
| spl24_5 ),
inference(avatar_split_clause,[],[f314,f356,f352,f348,f344,f340]) ).
fof(f361,definition,
( spl24_6
<=> e4 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl24_6])],[avatar_definition]) ).
fof(f362,plain,
( e4 != op(e4,e3)
| spl24_6 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f363,plain,
( e4 = op(e4,e3)
| ~ spl24_6 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f365,definition,
( spl24_7
<=> e3 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl24_7])],[avatar_definition]) ).
fof(f367,plain,
( e3 = op(e4,e3)
| ~ spl24_7 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f369,definition,
( spl24_8
<=> e2 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl24_8])],[avatar_definition]) ).
fof(f371,plain,
( e2 = op(e4,e3)
| ~ spl24_8 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f377,definition,
( spl24_10
<=> e0 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl24_10])],[avatar_definition]) ).
fof(f379,plain,
( e0 = op(e4,e3)
| ~ spl24_10 ),
inference(avatar_component_clause,[],[f377]) ).
fof(f382,definition,
( spl24_11
<=> e4 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl24_11])],[avatar_definition]) ).
fof(f384,plain,
( e4 = op(e4,e2)
| ~ spl24_11 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f386,definition,
( spl24_12
<=> e3 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl24_12])],[avatar_definition]) ).
fof(f388,plain,
( e3 = op(e4,e2)
| ~ spl24_12 ),
inference(avatar_component_clause,[],[f386]) ).
fof(f390,definition,
( spl24_13
<=> e2 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl24_13])],[avatar_definition]) ).
fof(f391,plain,
( e2 != op(e4,e2)
| spl24_13 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f392,plain,
( e2 = op(e4,e2)
| ~ spl24_13 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f394,definition,
( spl24_14
<=> e1 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl24_14])],[avatar_definition]) ).
fof(f396,plain,
( e1 = op(e4,e2)
| ~ spl24_14 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f398,definition,
( spl24_15
<=> e0 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl24_15])],[avatar_definition]) ).
fof(f400,plain,
( e0 = op(e4,e2)
| ~ spl24_15 ),
inference(avatar_component_clause,[],[f398]) ).
fof(f407,definition,
( spl24_17
<=> e3 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl24_17])],[avatar_definition]) ).
fof(f409,plain,
( e3 = op(e4,e1)
| ~ spl24_17 ),
inference(avatar_component_clause,[],[f407]) ).
fof(f411,definition,
( spl24_18
<=> e2 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl24_18])],[avatar_definition]) ).
fof(f413,plain,
( e2 = op(e4,e1)
| ~ spl24_18 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f419,definition,
( spl24_20
<=> e0 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl24_20])],[avatar_definition]) ).
fof(f421,plain,
( e0 = op(e4,e1)
| ~ spl24_20 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f428,definition,
( spl24_22
<=> e3 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl24_22])],[avatar_definition]) ).
fof(f430,plain,
( e3 = op(e4,e0)
| ~ spl24_22 ),
inference(avatar_component_clause,[],[f428]) ).
fof(f432,definition,
( spl24_23
<=> e2 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl24_23])],[avatar_definition]) ).
fof(f434,plain,
( e2 = op(e4,e0)
| ~ spl24_23 ),
inference(avatar_component_clause,[],[f432]) ).
fof(f440,definition,
( spl24_25
<=> e0 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl24_25])],[avatar_definition]) ).
fof(f442,plain,
( e0 = op(e4,e0)
| ~ spl24_25 ),
inference(avatar_component_clause,[],[f440]) ).
fof(f445,definition,
( spl24_26
<=> e4 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl24_26])],[avatar_definition]) ).
fof(f447,plain,
( e4 = op(e3,e4)
| ~ spl24_26 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f449,definition,
( spl24_27
<=> e3 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl24_27])],[avatar_definition]) ).
fof(f451,plain,
( e3 = op(e3,e4)
| ~ spl24_27 ),
inference(avatar_component_clause,[],[f449]) ).
fof(f453,definition,
( spl24_28
<=> e2 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl24_28])],[avatar_definition]) ).
fof(f455,plain,
( e2 = op(e3,e4)
| ~ spl24_28 ),
inference(avatar_component_clause,[],[f453]) ).
fof(f461,definition,
( spl24_30
<=> e0 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl24_30])],[avatar_definition]) ).
fof(f463,plain,
( e0 = op(e3,e4)
| ~ spl24_30 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f466,definition,
( spl24_31
<=> e4 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl24_31])],[avatar_definition]) ).
fof(f468,plain,
( e4 = op(e3,e3)
| ~ spl24_31 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f470,definition,
( spl24_32
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl24_32])],[avatar_definition]) ).
fof(f472,plain,
( e3 = op(e3,e3)
| ~ spl24_32 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f474,definition,
( spl24_33
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl24_33])],[avatar_definition]) ).
fof(f476,plain,
( e2 = op(e3,e3)
| ~ spl24_33 ),
inference(avatar_component_clause,[],[f474]) ).
fof(f478,definition,
( spl24_34
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl24_34])],[avatar_definition]) ).
fof(f480,plain,
( e1 = op(e3,e3)
| ~ spl24_34 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f482,definition,
( spl24_35
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl24_35])],[avatar_definition]) ).
fof(f484,plain,
( e0 = op(e3,e3)
| ~ spl24_35 ),
inference(avatar_component_clause,[],[f482]) ).
fof(f487,definition,
( spl24_36
<=> e4 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl24_36])],[avatar_definition]) ).
fof(f489,plain,
( e4 = op(e3,e2)
| ~ spl24_36 ),
inference(avatar_component_clause,[],[f487]) ).
fof(f491,definition,
( spl24_37
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl24_37])],[avatar_definition]) ).
fof(f493,plain,
( e3 = op(e3,e2)
| ~ spl24_37 ),
inference(avatar_component_clause,[],[f491]) ).
fof(f495,definition,
( spl24_38
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl24_38])],[avatar_definition]) ).
fof(f497,plain,
( e2 = op(e3,e2)
| ~ spl24_38 ),
inference(avatar_component_clause,[],[f495]) ).
fof(f499,definition,
( spl24_39
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl24_39])],[avatar_definition]) ).
fof(f501,plain,
( e1 = op(e3,e2)
| ~ spl24_39 ),
inference(avatar_component_clause,[],[f499]) ).
fof(f503,definition,
( spl24_40
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl24_40])],[avatar_definition]) ).
fof(f505,plain,
( e0 = op(e3,e2)
| ~ spl24_40 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f508,definition,
( spl24_41
<=> e4 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl24_41])],[avatar_definition]) ).
fof(f510,plain,
( e4 = op(e3,e1)
| ~ spl24_41 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f512,definition,
( spl24_42
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl24_42])],[avatar_definition]) ).
fof(f514,plain,
( e3 = op(e3,e1)
| ~ spl24_42 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f516,definition,
( spl24_43
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl24_43])],[avatar_definition]) ).
fof(f518,plain,
( e2 = op(e3,e1)
| ~ spl24_43 ),
inference(avatar_component_clause,[],[f516]) ).
fof(f524,definition,
( spl24_45
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl24_45])],[avatar_definition]) ).
fof(f526,plain,
( e0 = op(e3,e1)
| ~ spl24_45 ),
inference(avatar_component_clause,[],[f524]) ).
fof(f529,definition,
( spl24_46
<=> e4 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl24_46])],[avatar_definition]) ).
fof(f531,plain,
( e4 = op(e3,e0)
| ~ spl24_46 ),
inference(avatar_component_clause,[],[f529]) ).
fof(f533,definition,
( spl24_47
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl24_47])],[avatar_definition]) ).
fof(f535,plain,
( e3 = op(e3,e0)
| ~ spl24_47 ),
inference(avatar_component_clause,[],[f533]) ).
fof(f545,definition,
( spl24_50
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl24_50])],[avatar_definition]) ).
fof(f547,plain,
( e0 = op(e3,e0)
| ~ spl24_50 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f550,definition,
( spl24_51
<=> e4 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl24_51])],[avatar_definition]) ).
fof(f552,plain,
( e4 = op(e2,e4)
| ~ spl24_51 ),
inference(avatar_component_clause,[],[f550]) ).
fof(f554,definition,
( spl24_52
<=> e3 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl24_52])],[avatar_definition]) ).
fof(f556,plain,
( e3 = op(e2,e4)
| ~ spl24_52 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f558,definition,
( spl24_53
<=> e2 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl24_53])],[avatar_definition]) ).
fof(f560,plain,
( e2 = op(e2,e4)
| ~ spl24_53 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f562,definition,
( spl24_54
<=> e1 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl24_54])],[avatar_definition]) ).
fof(f564,plain,
( e1 = op(e2,e4)
| ~ spl24_54 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f566,definition,
( spl24_55
<=> e0 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl24_55])],[avatar_definition]) ).
fof(f568,plain,
( e0 = op(e2,e4)
| ~ spl24_55 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f571,definition,
( spl24_56
<=> e4 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl24_56])],[avatar_definition]) ).
fof(f573,plain,
( e4 = op(e2,e3)
| ~ spl24_56 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f575,definition,
( spl24_57
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl24_57])],[avatar_definition]) ).
fof(f577,plain,
( e3 = op(e2,e3)
| ~ spl24_57 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f579,definition,
( spl24_58
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl24_58])],[avatar_definition]) ).
fof(f581,plain,
( e2 = op(e2,e3)
| ~ spl24_58 ),
inference(avatar_component_clause,[],[f579]) ).
fof(f583,definition,
( spl24_59
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl24_59])],[avatar_definition]) ).
fof(f585,plain,
( e1 = op(e2,e3)
| ~ spl24_59 ),
inference(avatar_component_clause,[],[f583]) ).
fof(f587,definition,
( spl24_60
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl24_60])],[avatar_definition]) ).
fof(f589,plain,
( e0 = op(e2,e3)
| ~ spl24_60 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f592,definition,
( spl24_61
<=> e4 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl24_61])],[avatar_definition]) ).
fof(f594,plain,
( e4 = op(e2,e2)
| ~ spl24_61 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f596,definition,
( spl24_62
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl24_62])],[avatar_definition]) ).
fof(f598,plain,
( e3 = op(e2,e2)
| ~ spl24_62 ),
inference(avatar_component_clause,[],[f596]) ).
fof(f600,definition,
( spl24_63
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl24_63])],[avatar_definition]) ).
fof(f602,plain,
( e2 = op(e2,e2)
| ~ spl24_63 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f604,definition,
( spl24_64
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl24_64])],[avatar_definition]) ).
fof(f606,plain,
( e1 = op(e2,e2)
| ~ spl24_64 ),
inference(avatar_component_clause,[],[f604]) ).
fof(f608,definition,
( spl24_65
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl24_65])],[avatar_definition]) ).
fof(f610,plain,
( e0 = op(e2,e2)
| ~ spl24_65 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f613,definition,
( spl24_66
<=> e4 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl24_66])],[avatar_definition]) ).
fof(f615,plain,
( e4 = op(e2,e1)
| ~ spl24_66 ),
inference(avatar_component_clause,[],[f613]) ).
fof(f617,definition,
( spl24_67
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl24_67])],[avatar_definition]) ).
fof(f619,plain,
( e3 = op(e2,e1)
| ~ spl24_67 ),
inference(avatar_component_clause,[],[f617]) ).
fof(f621,definition,
( spl24_68
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl24_68])],[avatar_definition]) ).
fof(f623,plain,
( e2 = op(e2,e1)
| ~ spl24_68 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f625,definition,
( spl24_69
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl24_69])],[avatar_definition]) ).
fof(f627,plain,
( e1 = op(e2,e1)
| ~ spl24_69 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f629,definition,
( spl24_70
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl24_70])],[avatar_definition]) ).
fof(f631,plain,
( e0 = op(e2,e1)
| ~ spl24_70 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f634,definition,
( spl24_71
<=> e4 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl24_71])],[avatar_definition]) ).
fof(f636,plain,
( e4 = op(e2,e0)
| ~ spl24_71 ),
inference(avatar_component_clause,[],[f634]) ).
fof(f638,definition,
( spl24_72
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl24_72])],[avatar_definition]) ).
fof(f640,plain,
( e3 = op(e2,e0)
| ~ spl24_72 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f642,definition,
( spl24_73
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl24_73])],[avatar_definition]) ).
fof(f644,plain,
( e2 = op(e2,e0)
| ~ spl24_73 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f646,definition,
( spl24_74
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl24_74])],[avatar_definition]) ).
fof(f648,plain,
( e1 = op(e2,e0)
| ~ spl24_74 ),
inference(avatar_component_clause,[],[f646]) ).
fof(f650,definition,
( spl24_75
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl24_75])],[avatar_definition]) ).
fof(f652,plain,
( e0 = op(e2,e0)
| ~ spl24_75 ),
inference(avatar_component_clause,[],[f650]) ).
fof(f659,definition,
( spl24_77
<=> e3 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl24_77])],[avatar_definition]) ).
fof(f661,plain,
( e3 = op(e1,e4)
| ~ spl24_77 ),
inference(avatar_component_clause,[],[f659]) ).
fof(f663,definition,
( spl24_78
<=> e2 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl24_78])],[avatar_definition]) ).
fof(f665,plain,
( e2 = op(e1,e4)
| ~ spl24_78 ),
inference(avatar_component_clause,[],[f663]) ).
fof(f671,definition,
( spl24_80
<=> e0 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl24_80])],[avatar_definition]) ).
fof(f673,plain,
( e0 = op(e1,e4)
| ~ spl24_80 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f676,definition,
( spl24_81
<=> e4 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl24_81])],[avatar_definition]) ).
fof(f678,plain,
( e4 = op(e1,e3)
| ~ spl24_81 ),
inference(avatar_component_clause,[],[f676]) ).
fof(f680,definition,
( spl24_82
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl24_82])],[avatar_definition]) ).
fof(f682,plain,
( e3 = op(e1,e3)
| ~ spl24_82 ),
inference(avatar_component_clause,[],[f680]) ).
fof(f684,definition,
( spl24_83
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl24_83])],[avatar_definition]) ).
fof(f686,plain,
( e2 = op(e1,e3)
| ~ spl24_83 ),
inference(avatar_component_clause,[],[f684]) ).
fof(f692,definition,
( spl24_85
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl24_85])],[avatar_definition]) ).
fof(f694,plain,
( e0 = op(e1,e3)
| ~ spl24_85 ),
inference(avatar_component_clause,[],[f692]) ).
fof(f697,definition,
( spl24_86
<=> e4 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl24_86])],[avatar_definition]) ).
fof(f699,plain,
( e4 = op(e1,e2)
| ~ spl24_86 ),
inference(avatar_component_clause,[],[f697]) ).
fof(f701,definition,
( spl24_87
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl24_87])],[avatar_definition]) ).
fof(f703,plain,
( e3 = op(e1,e2)
| ~ spl24_87 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f705,definition,
( spl24_88
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl24_88])],[avatar_definition]) ).
fof(f707,plain,
( e2 = op(e1,e2)
| ~ spl24_88 ),
inference(avatar_component_clause,[],[f705]) ).
fof(f709,definition,
( spl24_89
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl24_89])],[avatar_definition]) ).
fof(f711,plain,
( e1 = op(e1,e2)
| ~ spl24_89 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f713,definition,
( spl24_90
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl24_90])],[avatar_definition]) ).
fof(f715,plain,
( e0 = op(e1,e2)
| ~ spl24_90 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f718,definition,
( spl24_91
<=> e4 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl24_91])],[avatar_definition]) ).
fof(f720,plain,
( e4 = op(e1,e1)
| ~ spl24_91 ),
inference(avatar_component_clause,[],[f718]) ).
fof(f722,definition,
( spl24_92
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl24_92])],[avatar_definition]) ).
fof(f724,plain,
( e3 = op(e1,e1)
| ~ spl24_92 ),
inference(avatar_component_clause,[],[f722]) ).
fof(f726,definition,
( spl24_93
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl24_93])],[avatar_definition]) ).
fof(f728,plain,
( e2 = op(e1,e1)
| ~ spl24_93 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f730,definition,
( spl24_94
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl24_94])],[avatar_definition]) ).
fof(f732,plain,
( e1 = op(e1,e1)
| ~ spl24_94 ),
inference(avatar_component_clause,[],[f730]) ).
fof(f734,definition,
( spl24_95
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl24_95])],[avatar_definition]) ).
fof(f736,plain,
( e0 = op(e1,e1)
| ~ spl24_95 ),
inference(avatar_component_clause,[],[f734]) ).
fof(f743,definition,
( spl24_97
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl24_97])],[avatar_definition]) ).
fof(f745,plain,
( e3 = op(e1,e0)
| ~ spl24_97 ),
inference(avatar_component_clause,[],[f743]) ).
fof(f747,definition,
( spl24_98
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl24_98])],[avatar_definition]) ).
fof(f749,plain,
( e2 = op(e1,e0)
| ~ spl24_98 ),
inference(avatar_component_clause,[],[f747]) ).
fof(f751,definition,
( spl24_99
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl24_99])],[avatar_definition]) ).
fof(f753,plain,
( e1 = op(e1,e0)
| ~ spl24_99 ),
inference(avatar_component_clause,[],[f751]) ).
fof(f764,definition,
( spl24_102
<=> e3 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl24_102])],[avatar_definition]) ).
fof(f766,plain,
( e3 = op(e0,e4)
| ~ spl24_102 ),
inference(avatar_component_clause,[],[f764]) ).
fof(f768,definition,
( spl24_103
<=> e2 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl24_103])],[avatar_definition]) ).
fof(f770,plain,
( e2 = op(e0,e4)
| ~ spl24_103 ),
inference(avatar_component_clause,[],[f768]) ).
fof(f776,definition,
( spl24_105
<=> e0 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl24_105])],[avatar_definition]) ).
fof(f778,plain,
( e0 = op(e0,e4)
| ~ spl24_105 ),
inference(avatar_component_clause,[],[f776]) ).
fof(f781,definition,
( spl24_106
<=> e4 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl24_106])],[avatar_definition]) ).
fof(f783,plain,
( e4 = op(e0,e3)
| ~ spl24_106 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f785,definition,
( spl24_107
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl24_107])],[avatar_definition]) ).
fof(f787,plain,
( e3 = op(e0,e3)
| ~ spl24_107 ),
inference(avatar_component_clause,[],[f785]) ).
fof(f797,definition,
( spl24_110
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl24_110])],[avatar_definition]) ).
fof(f799,plain,
( e0 = op(e0,e3)
| ~ spl24_110 ),
inference(avatar_component_clause,[],[f797]) ).
fof(f802,definition,
( spl24_111
<=> e4 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl24_111])],[avatar_definition]) ).
fof(f804,plain,
( e4 = op(e0,e2)
| ~ spl24_111 ),
inference(avatar_component_clause,[],[f802]) ).
fof(f806,definition,
( spl24_112
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl24_112])],[avatar_definition]) ).
fof(f808,plain,
( e3 = op(e0,e2)
| ~ spl24_112 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f810,definition,
( spl24_113
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl24_113])],[avatar_definition]) ).
fof(f812,plain,
( e2 = op(e0,e2)
| ~ spl24_113 ),
inference(avatar_component_clause,[],[f810]) ).
fof(f814,definition,
( spl24_114
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl24_114])],[avatar_definition]) ).
fof(f816,plain,
( e1 = op(e0,e2)
| ~ spl24_114 ),
inference(avatar_component_clause,[],[f814]) ).
fof(f827,definition,
( spl24_117
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl24_117])],[avatar_definition]) ).
fof(f829,plain,
( e3 = op(e0,e1)
| ~ spl24_117 ),
inference(avatar_component_clause,[],[f827]) ).
fof(f831,definition,
( spl24_118
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl24_118])],[avatar_definition]) ).
fof(f833,plain,
( e2 = op(e0,e1)
| ~ spl24_118 ),
inference(avatar_component_clause,[],[f831]) ).
fof(f835,definition,
( spl24_119
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl24_119])],[avatar_definition]) ).
fof(f837,plain,
( e1 = op(e0,e1)
| ~ spl24_119 ),
inference(avatar_component_clause,[],[f835]) ).
fof(f839,definition,
( spl24_120
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl24_120])],[avatar_definition]) ).
fof(f841,plain,
( e0 = op(e0,e1)
| ~ spl24_120 ),
inference(avatar_component_clause,[],[f839]) ).
fof(f844,definition,
( spl24_121
<=> op(e0,e0) = e4 ),
introduced(definition,[new_symbols(definition,[spl24_121])],[avatar_definition]) ).
fof(f846,plain,
( op(e0,e0) = e4
| ~ spl24_121 ),
inference(avatar_component_clause,[],[f844]) ).
fof(f848,definition,
( spl24_122
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl24_122])],[avatar_definition]) ).
fof(f850,plain,
( op(e0,e0) = e3
| ~ spl24_122 ),
inference(avatar_component_clause,[],[f848]) ).
fof(f852,definition,
( spl24_123
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl24_123])],[avatar_definition]) ).
fof(f854,plain,
( op(e0,e0) = e2
| ~ spl24_123 ),
inference(avatar_component_clause,[],[f852]) ).
fof(f856,definition,
( spl24_124
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl24_124])],[avatar_definition]) ).
fof(f858,plain,
( op(e0,e0) = e1
| ~ spl24_124 ),
inference(avatar_component_clause,[],[f856]) ).
fof(f860,definition,
( spl24_125
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl24_125])],[avatar_definition]) ).
fof(f862,plain,
( e0 = op(e0,e0)
| ~ spl24_125 ),
inference(avatar_component_clause,[],[f860]) ).
fof(f865,definition,
( spl24_126
<=> e4 = unit ),
introduced(definition,[new_symbols(definition,[spl24_126])],[avatar_definition]) ).
fof(f867,plain,
( e4 = unit
| ~ spl24_126 ),
inference(avatar_component_clause,[],[f865]) ).
fof(f869,definition,
( spl24_127
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl24_127])],[avatar_definition]) ).
fof(f871,plain,
( e3 = unit
| ~ spl24_127 ),
inference(avatar_component_clause,[],[f869]) ).
fof(f873,definition,
( spl24_128
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl24_128])],[avatar_definition]) ).
fof(f875,plain,
( e2 = unit
| ~ spl24_128 ),
inference(avatar_component_clause,[],[f873]) ).
fof(f877,definition,
( spl24_129
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl24_129])],[avatar_definition]) ).
fof(f879,plain,
( e1 = unit
| ~ spl24_129 ),
inference(avatar_component_clause,[],[f877]) ).
fof(f881,definition,
( spl24_130
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl24_130])],[avatar_definition]) ).
fof(f883,plain,
( e0 = unit
| ~ spl24_130 ),
inference(avatar_component_clause,[],[f881]) ).
fof(f884,plain,
( spl24_126
| spl24_127
| spl24_128
| spl24_129
| spl24_130 ),
inference(avatar_split_clause,[],[f303,f881,f877,f873,f869,f865]) ).
fof(f887,plain,
( spl24_2
| spl24_27
| spl24_52
| spl24_77
| spl24_102 ),
inference(avatar_split_clause,[],[f255,f764,f659,f554,f449,f344]) ).
fof(f888,plain,
( spl24_2
| spl24_7
| spl24_12
| spl24_17
| spl24_22 ),
inference(avatar_split_clause,[],[f256,f428,f407,f386,f365,f344]) ).
fof(f889,plain,
( spl24_3
| spl24_28
| spl24_53
| spl24_78
| spl24_103 ),
inference(avatar_split_clause,[],[f257,f768,f663,f558,f453,f348]) ).
fof(f890,plain,
( spl24_3
| spl24_8
| spl24_13
| spl24_18
| spl24_23 ),
inference(avatar_split_clause,[],[f258,f432,f411,f390,f369,f348]) ).
fof(f893,plain,
( spl24_5
| spl24_30
| spl24_55
| spl24_80
| spl24_105 ),
inference(avatar_split_clause,[],[f261,f776,f671,f566,f461,f356]) ).
fof(f894,plain,
( spl24_5
| spl24_10
| spl24_15
| spl24_20
| spl24_25 ),
inference(avatar_split_clause,[],[f262,f440,f419,f398,f377,f356]) ).
fof(f895,plain,
( spl24_6
| spl24_31
| spl24_56
| spl24_81
| spl24_106 ),
inference(avatar_split_clause,[],[f263,f781,f676,f571,f466,f361]) ).
fof(f896,plain,
( spl24_26
| spl24_31
| spl24_36
| spl24_41
| spl24_46 ),
inference(avatar_split_clause,[],[f264,f529,f508,f487,f466,f445]) ).
fof(f903,plain,
( spl24_10
| spl24_35
| spl24_60
| spl24_85
| spl24_110 ),
inference(avatar_split_clause,[],[f271,f797,f692,f587,f482,f377]) ).
fof(f904,plain,
( spl24_30
| spl24_35
| spl24_40
| spl24_45
| spl24_50 ),
inference(avatar_split_clause,[],[f272,f545,f524,f503,f482,f461]) ).
fof(f905,plain,
( spl24_11
| spl24_36
| spl24_61
| spl24_86
| spl24_111 ),
inference(avatar_split_clause,[],[f273,f802,f697,f592,f487,f382]) ).
fof(f906,plain,
( spl24_51
| spl24_56
| spl24_61
| spl24_66
| spl24_71 ),
inference(avatar_split_clause,[],[f274,f634,f613,f592,f571,f550]) ).
fof(f907,plain,
( spl24_12
| spl24_37
| spl24_62
| spl24_87
| spl24_112 ),
inference(avatar_split_clause,[],[f275,f806,f701,f596,f491,f386]) ).
fof(f908,plain,
( spl24_52
| spl24_57
| spl24_62
| spl24_67
| spl24_72 ),
inference(avatar_split_clause,[],[f276,f638,f617,f596,f575,f554]) ).
fof(f911,plain,
( spl24_14
| spl24_39
| spl24_64
| spl24_89
| spl24_114 ),
inference(avatar_split_clause,[],[f279,f814,f709,f604,f499,f394]) ).
fof(f912,plain,
( spl24_54
| spl24_59
| spl24_64
| spl24_69
| spl24_74 ),
inference(avatar_split_clause,[],[f280,f646,f625,f604,f583,f562]) ).
fof(f914,plain,
( spl24_55
| spl24_60
| spl24_65
| spl24_70
| spl24_75 ),
inference(avatar_split_clause,[],[f282,f650,f629,f608,f587,f566]) ).
fof(f917,plain,
( spl24_17
| spl24_42
| spl24_67
| spl24_92
| spl24_117 ),
inference(avatar_split_clause,[],[f285,f827,f722,f617,f512,f407]) ).
fof(f918,plain,
( spl24_77
| spl24_82
| spl24_87
| spl24_92
| spl24_97 ),
inference(avatar_split_clause,[],[f286,f743,f722,f701,f680,f659]) ).
fof(f919,plain,
( spl24_18
| spl24_43
| spl24_68
| spl24_93
| spl24_118 ),
inference(avatar_split_clause,[],[f287,f831,f726,f621,f516,f411]) ).
fof(f920,plain,
( spl24_78
| spl24_83
| spl24_88
| spl24_93
| spl24_98 ),
inference(avatar_split_clause,[],[f288,f747,f726,f705,f684,f663]) ).
fof(f923,plain,
( spl24_20
| spl24_45
| spl24_70
| spl24_95
| spl24_120 ),
inference(avatar_split_clause,[],[f291,f839,f734,f629,f524,f419]) ).
fof(f927,plain,
( spl24_22
| spl24_47
| spl24_72
| spl24_97
| spl24_122 ),
inference(avatar_split_clause,[],[f295,f848,f743,f638,f533,f428]) ).
fof(f928,plain,
( spl24_102
| spl24_107
| spl24_112
| spl24_117
| spl24_122 ),
inference(avatar_split_clause,[],[f296,f848,f827,f806,f785,f764]) ).
fof(f935,plain,
spl24_91,
inference(avatar_split_clause,[],[f139,f718]) ).
fof(f936,plain,
e0 = op(e1,e2),
inference(forward_demodulation,[],[f142,f141]) ).
fof(f938,definition,
( spl24_131
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl24_131])],[avatar_definition]) ).
fof(f942,definition,
( spl24_132
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl24_132])],[avatar_definition]) ).
fof(f946,definition,
( spl24_133
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl24_133])],[avatar_definition]) ).
fof(f950,definition,
( spl24_134
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl24_134])],[avatar_definition]) ).
fof(f954,definition,
( spl24_135
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl24_135])],[avatar_definition]) ).
fof(f958,definition,
( spl24_136
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl24_136])],[avatar_definition]) ).
fof(f962,definition,
( spl24_137
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl24_137])],[avatar_definition]) ).
fof(f966,definition,
( spl24_138
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl24_138])],[avatar_definition]) ).
fof(f970,definition,
( spl24_139
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl24_139])],[avatar_definition]) ).
fof(f974,definition,
( spl24_140
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl24_140])],[avatar_definition]) ).
fof(f978,definition,
( spl24_141
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl24_141])],[avatar_definition]) ).
fof(f982,definition,
( spl24_142
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl24_142])],[avatar_definition]) ).
fof(f986,definition,
( spl24_143
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl24_143])],[avatar_definition]) ).
fof(f990,definition,
( spl24_144
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl24_144])],[avatar_definition]) ).
fof(f994,definition,
( spl24_145
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl24_145])],[avatar_definition]) ).
fof(f998,definition,
( spl24_146
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl24_146])],[avatar_definition]) ).
fof(f1002,definition,
( spl24_147
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl24_147])],[avatar_definition]) ).
fof(f1006,definition,
( spl24_148
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl24_148])],[avatar_definition]) ).
fof(f1010,definition,
( spl24_149
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl24_149])],[avatar_definition]) ).
fof(f1014,definition,
( spl24_150
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl24_150])],[avatar_definition]) ).
fof(f1018,definition,
( spl24_151
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl24_151])],[avatar_definition]) ).
fof(f1022,definition,
( spl24_152
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl24_152])],[avatar_definition]) ).
fof(f1026,definition,
( spl24_153
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl24_153])],[avatar_definition]) ).
fof(f1030,definition,
( spl24_154
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl24_154])],[avatar_definition]) ).
fof(f1033,plain,
( spl24_131
| spl24_132
| spl24_133
| spl24_134
| spl24_135
| spl24_136
| spl24_137
| spl24_138
| spl24_139
| spl24_140
| spl24_141
| spl24_142
| spl24_143
| spl24_144
| spl24_145
| spl24_146
| spl24_147
| spl24_148
| spl24_149
| spl24_150
| spl24_151
| spl24_152
| spl24_153
| spl24_154
| ~ spl24_125 ),
inference(avatar_split_clause,[],[f131,f860,f1030,f1026,f1022,f1018,f1014,f1010,f1006,f1002,f998,f994,f990,f986,f982,f978,f974,f970,f966,f962,f958,f954,f950,f946,f942,f938]) ).
fof(f1035,plain,
( spl24_131
| spl24_132
| spl24_133
| spl24_134
| spl24_135
| spl24_136
| spl24_137
| spl24_138
| spl24_139
| spl24_140
| spl24_141
| spl24_142
| spl24_143
| spl24_144
| spl24_145
| spl24_146
| spl24_147
| spl24_148
| spl24_149
| spl24_150
| spl24_151
| spl24_152
| spl24_153
| spl24_154
| spl24_125 ),
inference(avatar_split_clause,[],[f133,f860,f1030,f1026,f1022,f1018,f1014,f1010,f1006,f1002,f998,f994,f990,f986,f982,f978,f974,f970,f966,f962,f958,f954,f950,f946,f942,f938]) ).
fof(f1037,plain,
( spl24_2
| spl24_32
| spl24_62
| spl24_92
| spl24_122 ),
inference(avatar_split_clause,[],[f135,f848,f722,f596,f470,f344]) ).
fof(f1038,plain,
( spl24_3
| spl24_33
| spl24_63
| spl24_93
| spl24_123 ),
inference(avatar_split_clause,[],[f136,f852,f726,f600,f474,f348]) ).
fof(f1039,plain,
( spl24_4
| spl24_34
| spl24_64
| spl24_94
| spl24_124 ),
inference(avatar_split_clause,[],[f137,f856,f730,f604,f478,f352]) ).
fof(f1040,plain,
( spl24_5
| spl24_35
| spl24_65
| spl24_95
| spl24_125 ),
inference(avatar_split_clause,[],[f138,f860,f734,f608,f482,f356]) ).
fof(f1041,plain,
( ~ spl24_131
| ~ spl24_1 ),
inference(avatar_split_clause,[],[f128,f340,f938]) ).
fof(f1043,plain,
( ~ spl24_131
| spl24_1 ),
inference(avatar_split_clause,[],[f130,f340,f938]) ).
fof(f1044,plain,
( ~ spl24_132
| ~ spl24_6 ),
inference(avatar_split_clause,[],[f125,f361,f942]) ).
fof(f1045,plain,
( ~ spl24_132
| spl24_31 ),
inference(avatar_split_clause,[],[f126,f466,f942]) ).
fof(f1046,plain,
( ~ spl24_132
| spl24_2 ),
inference(avatar_split_clause,[],[f127,f344,f942]) ).
fof(f1048,plain,
( ~ spl24_133
| spl24_61 ),
inference(avatar_split_clause,[],[f123,f592,f946]) ).
fof(f1049,plain,
( ~ spl24_133
| spl24_3 ),
inference(avatar_split_clause,[],[f124,f348,f946]) ).
fof(f1052,plain,
( ~ spl24_134
| spl24_4 ),
inference(avatar_split_clause,[],[f121,f352,f950]) ).
fof(f1054,plain,
( ~ spl24_135
| spl24_121 ),
inference(avatar_split_clause,[],[f117,f844,f954]) ).
fof(f1055,plain,
( ~ spl24_135
| spl24_5 ),
inference(avatar_split_clause,[],[f118,f356,f954]) ).
fof(f1057,plain,
( ~ spl24_136
| spl24_2 ),
inference(avatar_split_clause,[],[f114,f344,f958]) ).
fof(f1058,plain,
( ~ spl24_136
| spl24_31 ),
inference(avatar_split_clause,[],[f115,f466,f958]) ).
fof(f1059,plain,
( ~ spl24_137
| ~ spl24_32 ),
inference(avatar_split_clause,[],[f110,f470,f962]) ).
fof(f1061,plain,
( ~ spl24_137
| spl24_32 ),
inference(avatar_split_clause,[],[f112,f470,f962]) ).
fof(f1063,plain,
( ~ spl24_138
| spl24_62 ),
inference(avatar_split_clause,[],[f108,f596,f966]) ).
fof(f1064,plain,
( ~ spl24_138
| spl24_33 ),
inference(avatar_split_clause,[],[f109,f474,f966]) ).
fof(f1066,plain,
( ~ spl24_139
| spl24_92 ),
inference(avatar_split_clause,[],[f105,f722,f970]) ).
fof(f1069,plain,
( ~ spl24_140
| spl24_122 ),
inference(avatar_split_clause,[],[f102,f848,f974]) ).
fof(f1070,plain,
( ~ spl24_140
| spl24_35 ),
inference(avatar_split_clause,[],[f103,f482,f974]) ).
fof(f1072,plain,
( ~ spl24_141
| spl24_3 ),
inference(avatar_split_clause,[],[f99,f348,f978]) ).
fof(f1073,plain,
( ~ spl24_141
| spl24_61 ),
inference(avatar_split_clause,[],[f100,f592,f978]) ).
fof(f1074,plain,
( ~ spl24_142
| ~ spl24_58 ),
inference(avatar_split_clause,[],[f95,f579,f982]) ).
fof(f1075,plain,
( ~ spl24_142
| spl24_33 ),
inference(avatar_split_clause,[],[f96,f474,f982]) ).
fof(f1076,plain,
( ~ spl24_142
| spl24_62 ),
inference(avatar_split_clause,[],[f97,f596,f982]) ).
fof(f1077,plain,
( ~ spl24_143
| ~ spl24_63 ),
inference(avatar_split_clause,[],[f92,f600,f986]) ).
fof(f1079,plain,
( ~ spl24_143
| spl24_63 ),
inference(avatar_split_clause,[],[f94,f600,f986]) ).
fof(f1081,plain,
( ~ spl24_144
| spl24_93 ),
inference(avatar_split_clause,[],[f90,f726,f990]) ).
fof(f1083,plain,
( ~ spl24_145
| ~ spl24_73 ),
inference(avatar_split_clause,[],[f86,f642,f994]) ).
fof(f1084,plain,
( ~ spl24_145
| spl24_123 ),
inference(avatar_split_clause,[],[f87,f852,f994]) ).
fof(f1085,plain,
( ~ spl24_145
| spl24_65 ),
inference(avatar_split_clause,[],[f88,f608,f994]) ).
fof(f1087,plain,
( ~ spl24_146
| spl24_4 ),
inference(avatar_split_clause,[],[f84,f352,f998]) ).
fof(f1091,plain,
( ~ spl24_147
| spl24_92 ),
inference(avatar_split_clause,[],[f82,f722,f1002]) ).
fof(f1094,plain,
( ~ spl24_148
| spl24_93 ),
inference(avatar_split_clause,[],[f79,f726,f1006]) ).
fof(f1097,plain,
( ~ spl24_149
| spl24_94 ),
inference(avatar_split_clause,[],[f76,f730,f1010]) ).
fof(f1100,plain,
( ~ spl24_150
| spl24_95 ),
inference(avatar_split_clause,[],[f73,f734,f1014]) ).
fof(f1102,plain,
( ~ spl24_151
| spl24_5 ),
inference(avatar_split_clause,[],[f69,f356,f1018]) ).
fof(f1103,plain,
( ~ spl24_151
| spl24_121 ),
inference(avatar_split_clause,[],[f70,f844,f1018]) ).
fof(f1104,plain,
( ~ spl24_152
| ~ spl24_110 ),
inference(avatar_split_clause,[],[f65,f797,f1022]) ).
fof(f1106,plain,
( ~ spl24_152
| spl24_122 ),
inference(avatar_split_clause,[],[f67,f848,f1022]) ).
fof(f1108,plain,
( ~ spl24_153
| spl24_65 ),
inference(avatar_split_clause,[],[f63,f608,f1026]) ).
fof(f1109,plain,
( ~ spl24_153
| spl24_123 ),
inference(avatar_split_clause,[],[f64,f852,f1026]) ).
fof(f1111,plain,
( ~ spl24_154
| spl24_95 ),
inference(avatar_split_clause,[],[f60,f734,f1030]) ).
fof(f1113,plain,
spl24_90,
inference(avatar_split_clause,[],[f936,f713]) ).
fof(f1114,plain,
( e4 = op(e4,e0)
| ~ spl24_130 ),
inference(superposition,[],[f304,f883]) ).
fof(f1115,plain,
( e3 = e4
| ~ spl24_22
| ~ spl24_130 ),
inference(forward_demodulation,[],[f1114,f430]) ).
fof(f1116,plain,
( $false
| ~ spl24_22
| ~ spl24_130 ),
inference(forward_subsumption_resolution,[],[f1115,f143]) ).
fof(f1117,plain,
( ~ spl24_22
| ~ spl24_130 ),
inference(avatar_contradiction_clause,[],[f1116]) ).
fof(f1119,plain,
( e2 = e4
| ~ spl24_23
| ~ spl24_130 ),
inference(forward_demodulation,[],[f1114,f434]) ).
fof(f1120,plain,
( $false
| ~ spl24_23
| ~ spl24_130 ),
inference(forward_subsumption_resolution,[],[f1119,f144]) ).
fof(f1121,plain,
( ~ spl24_23
| ~ spl24_130 ),
inference(avatar_contradiction_clause,[],[f1120]) ).
fof(f1123,plain,
( e4 = op(e4,e4)
| ~ spl24_126 ),
inference(superposition,[],[f304,f867]) ).
fof(f1124,plain,
( e3 = e4
| ~ spl24_2
| ~ spl24_126 ),
inference(forward_demodulation,[],[f1123,f346]) ).
fof(f1125,plain,
( $false
| ~ spl24_2
| ~ spl24_126 ),
inference(forward_subsumption_resolution,[],[f1124,f143]) ).
fof(f1126,plain,
( ~ spl24_2
| ~ spl24_126 ),
inference(avatar_contradiction_clause,[],[f1125]) ).
fof(f1129,plain,
( e4 = op(e4,e3)
| ~ spl24_127 ),
inference(superposition,[],[f304,f871]) ).
fof(f1130,plain,
( $false
| spl24_6
| ~ spl24_127 ),
inference(forward_subsumption_resolution,[],[f1129,f362]) ).
fof(f1131,plain,
( spl24_6
| ~ spl24_127 ),
inference(avatar_contradiction_clause,[],[f1130]) ).
fof(f1158,plain,
( e4 = op(e4,e0)
| ~ spl24_130 ),
inference(superposition,[],[f304,f883]) ).
fof(f1159,plain,
( e4 = op(e0,e4)
| ~ spl24_130 ),
inference(superposition,[],[f305,f883]) ).
fof(f1164,plain,
( e3 = e4
| ~ spl24_102
| ~ spl24_130 ),
inference(forward_demodulation,[],[f1159,f766]) ).
fof(f1166,plain,
( $false
| ~ spl24_102
| ~ spl24_130 ),
inference(forward_subsumption_resolution,[],[f1164,f143]) ).
fof(f1167,plain,
( ~ spl24_102
| ~ spl24_130 ),
inference(avatar_contradiction_clause,[],[f1166]) ).
fof(f1172,plain,
( e2 = e4
| ~ spl24_103
| ~ spl24_130 ),
inference(forward_demodulation,[],[f1159,f770]) ).
fof(f1175,plain,
( e0 = e4
| ~ spl24_25
| ~ spl24_130 ),
inference(forward_demodulation,[],[f1158,f442]) ).
fof(f1176,plain,
( $false
| ~ spl24_103
| ~ spl24_130 ),
inference(forward_subsumption_resolution,[],[f1172,f144]) ).
fof(f1177,plain,
( ~ spl24_103
| ~ spl24_130 ),
inference(avatar_contradiction_clause,[],[f1176]) ).
fof(f1178,plain,
( $false
| ~ spl24_25
| ~ spl24_130 ),
inference(forward_subsumption_resolution,[],[f1175,f149]) ).
fof(f1179,plain,
( ~ spl24_25
| ~ spl24_130 ),
inference(avatar_contradiction_clause,[],[f1178]) ).
fof(f1181,plain,
( e1 = e2
| ~ spl24_63
| ~ spl24_64 ),
inference(forward_demodulation,[],[f602,f606]) ).
fof(f1184,plain,
( $false
| ~ spl24_63
| ~ spl24_64 ),
inference(forward_subsumption_resolution,[],[f1181,f148]) ).
fof(f1185,plain,
( ~ spl24_63
| ~ spl24_64 ),
inference(avatar_contradiction_clause,[],[f1184]) ).
fof(f1202,plain,
( e4 = op(e0,e4)
| ~ spl24_130 ),
inference(superposition,[],[f305,f883]) ).
fof(f1213,plain,
( e0 = e4
| ~ spl24_105
| ~ spl24_130 ),
inference(forward_demodulation,[],[f1202,f778]) ).
fof(f1214,plain,
( $false
| ~ spl24_105
| ~ spl24_130 ),
inference(forward_subsumption_resolution,[],[f1213,f149]) ).
fof(f1215,plain,
( ~ spl24_105
| ~ spl24_130 ),
inference(avatar_contradiction_clause,[],[f1214]) ).
fof(f1222,plain,
( e2 = op(e2,e0)
| ~ spl24_130 ),
inference(superposition,[],[f308,f883]) ).
fof(f1223,plain,
( e1 = e2
| ~ spl24_74
| ~ spl24_130 ),
inference(forward_demodulation,[],[f1222,f648]) ).
fof(f1224,plain,
( $false
| ~ spl24_74
| ~ spl24_130 ),
inference(forward_subsumption_resolution,[],[f1223,f148]) ).
fof(f1225,plain,
( ~ spl24_74
| ~ spl24_130 ),
inference(avatar_contradiction_clause,[],[f1224]) ).
fof(f1228,plain,
( spl24_73
| ~ spl24_130 ),
inference(avatar_split_clause,[],[f1222,f881,f642]) ).
fof(f1233,plain,
( e1 = op(e1,e0)
| ~ spl24_130 ),
inference(superposition,[],[f310,f883]) ).
fof(f1238,plain,
( spl24_99
| ~ spl24_130 ),
inference(avatar_split_clause,[],[f1233,f881,f751]) ).
fof(f1239,plain,
( e1 = op(e0,e1)
| ~ spl24_130 ),
inference(superposition,[],[f311,f883]) ).
fof(f1240,plain,
( spl24_119
| ~ spl24_130 ),
inference(avatar_split_clause,[],[f1239,f881,f835]) ).
fof(f1241,plain,
( e0 = op(e0,e0)
| ~ spl24_130 ),
inference(superposition,[],[f312,f883]) ).
fof(f1242,plain,
( spl24_125
| ~ spl24_130 ),
inference(avatar_split_clause,[],[f1241,f881,f860]) ).
fof(f1253,plain,
( e1 = op(e1,e2)
| ~ spl24_128 ),
inference(superposition,[],[f310,f875]) ).
fof(f1261,plain,
( e0 = e1
| ~ spl24_90
| ~ spl24_128 ),
inference(forward_demodulation,[],[f1253,f715]) ).
fof(f1265,plain,
( $false
| ~ spl24_90
| ~ spl24_128 ),
inference(forward_subsumption_resolution,[],[f1261,f152]) ).
fof(f1266,plain,
( ~ spl24_90
| ~ spl24_128 ),
inference(avatar_contradiction_clause,[],[f1265]) ).
fof(f1279,plain,
( e2 = op(e1,e2)
| ~ spl24_129 ),
inference(superposition,[],[f309,f879]) ).
fof(f1288,plain,
( e0 = e2
| ~ spl24_90
| ~ spl24_129 ),
inference(forward_demodulation,[],[f1279,f715]) ).
fof(f1291,plain,
( $false
| ~ spl24_90
| ~ spl24_129 ),
inference(forward_subsumption_resolution,[],[f1288,f151]) ).
fof(f1292,plain,
( ~ spl24_90
| ~ spl24_129 ),
inference(avatar_contradiction_clause,[],[f1291]) ).
fof(f1297,plain,
( e3 = e4
| ~ spl24_6
| ~ spl24_7 ),
inference(forward_demodulation,[],[f363,f367]) ).
fof(f1301,plain,
( $false
| ~ spl24_6
| ~ spl24_7 ),
inference(forward_subsumption_resolution,[],[f1297,f143]) ).
fof(f1302,plain,
( ~ spl24_6
| ~ spl24_7 ),
inference(avatar_contradiction_clause,[],[f1301]) ).
fof(f1304,plain,
( e2 = e4
| ~ spl24_6
| ~ spl24_8 ),
inference(forward_demodulation,[],[f363,f371]) ).
fof(f1305,plain,
( $false
| ~ spl24_6
| ~ spl24_8 ),
inference(forward_subsumption_resolution,[],[f1304,f144]) ).
fof(f1306,plain,
( ~ spl24_6
| ~ spl24_8 ),
inference(avatar_contradiction_clause,[],[f1305]) ).
fof(f1308,plain,
( e0 = e2
| ~ spl24_33
| ~ spl24_35 ),
inference(forward_demodulation,[],[f476,f484]) ).
fof(f1311,plain,
( $false
| ~ spl24_33
| ~ spl24_35 ),
inference(forward_subsumption_resolution,[],[f1308,f151]) ).
fof(f1312,plain,
( ~ spl24_33
| ~ spl24_35 ),
inference(avatar_contradiction_clause,[],[f1311]) ).
fof(f1316,plain,
( e0 = e2
| ~ spl24_58
| ~ spl24_60 ),
inference(forward_demodulation,[],[f581,f589]) ).
fof(f1317,plain,
( e0 = e1
| ~ spl24_59
| ~ spl24_60 ),
inference(forward_demodulation,[],[f585,f589]) ).
fof(f1318,plain,
( $false
| ~ spl24_58
| ~ spl24_60 ),
inference(forward_subsumption_resolution,[],[f1316,f151]) ).
fof(f1319,plain,
( ~ spl24_58
| ~ spl24_60 ),
inference(avatar_contradiction_clause,[],[f1318]) ).
fof(f1320,plain,
( $false
| ~ spl24_59
| ~ spl24_60 ),
inference(forward_subsumption_resolution,[],[f1317,f152]) ).
fof(f1321,plain,
( ~ spl24_59
| ~ spl24_60 ),
inference(avatar_contradiction_clause,[],[f1320]) ).
fof(f1325,plain,
( e3 = op(e3,e3)
| ~ spl24_127 ),
inference(superposition,[],[f306,f871]) ).
fof(f1326,plain,
( e3 = op(e3,e3)
| ~ spl24_127 ),
inference(superposition,[],[f307,f871]) ).
fof(f1327,plain,
( e2 = op(e2,e3)
| ~ spl24_127 ),
inference(superposition,[],[f308,f871]) ).
fof(f1328,plain,
( e2 = op(e3,e2)
| ~ spl24_127 ),
inference(superposition,[],[f309,f871]) ).
fof(f1336,plain,
( spl24_38
| ~ spl24_127 ),
inference(avatar_split_clause,[],[f1328,f869,f495]) ).
fof(f1338,plain,
( e0 = e3
| ~ spl24_35
| ~ spl24_127 ),
inference(forward_demodulation,[],[f1325,f484]) ).
fof(f1341,plain,
( $false
| ~ spl24_35
| ~ spl24_127 ),
inference(forward_subsumption_resolution,[],[f1338,f150]) ).
fof(f1342,plain,
( ~ spl24_35
| ~ spl24_127 ),
inference(avatar_contradiction_clause,[],[f1341]) ).
fof(f1344,plain,
( spl24_32
| ~ spl24_127 ),
inference(avatar_split_clause,[],[f1326,f869,f470]) ).
fof(f1346,plain,
( e2 = e3
| ~ spl24_2
| ~ spl24_3 ),
inference(superposition,[],[f350,f346]) ).
fof(f1350,plain,
( $false
| ~ spl24_2
| ~ spl24_3 ),
inference(forward_subsumption_resolution,[],[f1346,f145]) ).
fof(f1351,plain,
( ~ spl24_2
| ~ spl24_3 ),
inference(avatar_contradiction_clause,[],[f1350]) ).
fof(f1353,plain,
( e0 = e3
| ~ spl24_2
| ~ spl24_5 ),
inference(superposition,[],[f358,f346]) ).
fof(f1357,plain,
( $false
| ~ spl24_2
| ~ spl24_5 ),
inference(forward_subsumption_resolution,[],[f1353,f150]) ).
fof(f1358,plain,
( ~ spl24_2
| ~ spl24_5 ),
inference(avatar_contradiction_clause,[],[f1357]) ).
fof(f1363,plain,
( e3 = e4
| ~ spl24_11
| ~ spl24_12 ),
inference(superposition,[],[f388,f384]) ).
fof(f1367,plain,
( $false
| ~ spl24_11
| ~ spl24_12 ),
inference(forward_subsumption_resolution,[],[f1363,f143]) ).
fof(f1368,plain,
( ~ spl24_11
| ~ spl24_12 ),
inference(avatar_contradiction_clause,[],[f1367]) ).
fof(f1370,plain,
( e2 = e3
| ~ spl24_37
| ~ spl24_38 ),
inference(forward_demodulation,[],[f493,f497]) ).
fof(f1371,plain,
( $false
| ~ spl24_37
| ~ spl24_38 ),
inference(forward_subsumption_resolution,[],[f1370,f145]) ).
fof(f1372,plain,
( ~ spl24_37
| ~ spl24_38 ),
inference(avatar_contradiction_clause,[],[f1371]) ).
fof(f1374,plain,
( e2 = e3
| ~ spl24_12
| ~ spl24_13 ),
inference(forward_demodulation,[],[f388,f392]) ).
fof(f1376,plain,
( $false
| ~ spl24_12
| ~ spl24_13 ),
inference(forward_subsumption_resolution,[],[f1374,f145]) ).
fof(f1377,plain,
( ~ spl24_12
| ~ spl24_13 ),
inference(avatar_contradiction_clause,[],[f1376]) ).
fof(f1387,plain,
( e1 = e3
| ~ spl24_62
| ~ spl24_64 ),
inference(forward_demodulation,[],[f598,f606]) ).
fof(f1389,plain,
( $false
| ~ spl24_62
| ~ spl24_64 ),
inference(forward_subsumption_resolution,[],[f1387,f147]) ).
fof(f1390,plain,
( ~ spl24_62
| ~ spl24_64 ),
inference(avatar_contradiction_clause,[],[f1389]) ).
fof(f1392,plain,
( e2 = e3
| ~ spl24_112
| ~ spl24_113 ),
inference(forward_demodulation,[],[f808,f812]) ).
fof(f1393,plain,
( $false
| ~ spl24_112
| ~ spl24_113 ),
inference(forward_subsumption_resolution,[],[f1392,f145]) ).
fof(f1394,plain,
( ~ spl24_112
| ~ spl24_113 ),
inference(avatar_contradiction_clause,[],[f1393]) ).
fof(f1395,plain,
( e0 = e3
| ~ spl24_87
| ~ spl24_90 ),
inference(forward_demodulation,[],[f703,f715]) ).
fof(f1397,plain,
( $false
| ~ spl24_87
| ~ spl24_90 ),
inference(forward_subsumption_resolution,[],[f1395,f150]) ).
fof(f1398,plain,
( ~ spl24_87
| ~ spl24_90 ),
inference(avatar_contradiction_clause,[],[f1397]) ).
fof(f1427,plain,
( e1 = e3
| ~ spl24_12
| ~ spl24_14 ),
inference(superposition,[],[f396,f388]) ).
fof(f1432,plain,
( $false
| ~ spl24_12
| ~ spl24_14 ),
inference(forward_subsumption_resolution,[],[f1427,f147]) ).
fof(f1433,plain,
( ~ spl24_12
| ~ spl24_14 ),
inference(avatar_contradiction_clause,[],[f1432]) ).
fof(f1438,plain,
( e0 = e3
| ~ spl24_12
| ~ spl24_15 ),
inference(superposition,[],[f400,f388]) ).
fof(f1443,plain,
( $false
| ~ spl24_12
| ~ spl24_15 ),
inference(forward_subsumption_resolution,[],[f1438,f150]) ).
fof(f1444,plain,
( ~ spl24_12
| ~ spl24_15 ),
inference(avatar_contradiction_clause,[],[f1443]) ).
fof(f1446,plain,
( e1 = e3
| ~ spl24_112
| ~ spl24_114 ),
inference(forward_demodulation,[],[f808,f816]) ).
fof(f1448,plain,
( e1 = e2
| ~ spl24_123
| ~ spl24_124 ),
inference(forward_demodulation,[],[f854,f858]) ).
fof(f1451,plain,
( $false
| ~ spl24_112
| ~ spl24_114 ),
inference(forward_subsumption_resolution,[],[f1446,f147]) ).
fof(f1452,plain,
( ~ spl24_112
| ~ spl24_114 ),
inference(avatar_contradiction_clause,[],[f1451]) ).
fof(f1453,plain,
( $false
| ~ spl24_123
| ~ spl24_124 ),
inference(forward_subsumption_resolution,[],[f1448,f148]) ).
fof(f1454,plain,
( ~ spl24_123
| ~ spl24_124 ),
inference(avatar_contradiction_clause,[],[f1453]) ).
fof(f1457,plain,
( e3 = e4
| ~ spl24_26
| ~ spl24_27 ),
inference(superposition,[],[f451,f447]) ).
fof(f1461,plain,
( $false
| ~ spl24_26
| ~ spl24_27 ),
inference(forward_subsumption_resolution,[],[f1457,f143]) ).
fof(f1462,plain,
( ~ spl24_26
| ~ spl24_27 ),
inference(avatar_contradiction_clause,[],[f1461]) ).
fof(f1464,plain,
( e2 = e4
| ~ spl24_26
| ~ spl24_28 ),
inference(superposition,[],[f455,f447]) ).
fof(f1468,plain,
( $false
| ~ spl24_26
| ~ spl24_28 ),
inference(forward_subsumption_resolution,[],[f1464,f144]) ).
fof(f1469,plain,
( ~ spl24_26
| ~ spl24_28 ),
inference(avatar_contradiction_clause,[],[f1468]) ).
fof(f1497,plain,
( e3 = e4
| ~ spl24_31
| ~ spl24_32 ),
inference(superposition,[],[f472,f468]) ).
fof(f1501,plain,
( $false
| ~ spl24_31
| ~ spl24_32 ),
inference(forward_subsumption_resolution,[],[f1497,f143]) ).
fof(f1502,plain,
( ~ spl24_31
| ~ spl24_32 ),
inference(avatar_contradiction_clause,[],[f1501]) ).
fof(f1506,plain,
( e2 = e4
| ~ spl24_36
| ~ spl24_38 ),
inference(superposition,[],[f497,f489]) ).
fof(f1510,plain,
( $false
| ~ spl24_36
| ~ spl24_38 ),
inference(forward_subsumption_resolution,[],[f1506,f144]) ).
fof(f1511,plain,
( ~ spl24_36
| ~ spl24_38 ),
inference(avatar_contradiction_clause,[],[f1510]) ).
fof(f1524,plain,
( e0 = e2
| ~ spl24_13
| ~ spl24_15 ),
inference(forward_demodulation,[],[f392,f400]) ).
fof(f1528,plain,
( $false
| ~ spl24_13
| ~ spl24_15 ),
inference(forward_subsumption_resolution,[],[f1524,f151]) ).
fof(f1529,plain,
( ~ spl24_13
| ~ spl24_15 ),
inference(avatar_contradiction_clause,[],[f1528]) ).
fof(f1530,plain,
( e0 = e4
| ~ spl24_6
| ~ spl24_10 ),
inference(superposition,[],[f379,f363]) ).
fof(f1537,plain,
( $false
| ~ spl24_6
| ~ spl24_10 ),
inference(forward_subsumption_resolution,[],[f1530,f149]) ).
fof(f1538,plain,
( ~ spl24_6
| ~ spl24_10 ),
inference(avatar_contradiction_clause,[],[f1537]) ).
fof(f1544,plain,
( e2 = e3
| ~ spl24_17
| ~ spl24_18 ),
inference(superposition,[],[f413,f409]) ).
fof(f1548,plain,
( $false
| ~ spl24_17
| ~ spl24_18 ),
inference(forward_subsumption_resolution,[],[f1544,f145]) ).
fof(f1549,plain,
( ~ spl24_17
| ~ spl24_18 ),
inference(avatar_contradiction_clause,[],[f1548]) ).
fof(f1570,plain,
( e3 = e4
| ~ spl24_46
| ~ spl24_47 ),
inference(superposition,[],[f535,f531]) ).
fof(f1574,plain,
( $false
| ~ spl24_46
| ~ spl24_47 ),
inference(forward_subsumption_resolution,[],[f1570,f143]) ).
fof(f1575,plain,
( ~ spl24_46
| ~ spl24_47 ),
inference(avatar_contradiction_clause,[],[f1574]) ).
fof(f1589,plain,
( e2 = e3
| ~ spl24_122
| ~ spl24_123 ),
inference(forward_demodulation,[],[f850,f854]) ).
fof(f1590,plain,
( $false
| ~ spl24_122
| ~ spl24_123 ),
inference(forward_subsumption_resolution,[],[f1589,f145]) ).
fof(f1591,plain,
( ~ spl24_122
| ~ spl24_123 ),
inference(avatar_contradiction_clause,[],[f1590]) ).
fof(f1592,plain,
( e2 = e3
| ~ spl24_72
| ~ spl24_73 ),
inference(forward_demodulation,[],[f640,f644]) ).
fof(f1594,plain,
( $false
| ~ spl24_72
| ~ spl24_73 ),
inference(forward_subsumption_resolution,[],[f1592,f145]) ).
fof(f1595,plain,
( ~ spl24_72
| ~ spl24_73 ),
inference(avatar_contradiction_clause,[],[f1594]) ).
fof(f1596,plain,
( e0 = e3
| ~ spl24_47
| ~ spl24_50 ),
inference(forward_demodulation,[],[f535,f547]) ).
fof(f1600,plain,
( $false
| ~ spl24_47
| ~ spl24_50 ),
inference(forward_subsumption_resolution,[],[f1596,f150]) ).
fof(f1601,plain,
( ~ spl24_47
| ~ spl24_50 ),
inference(avatar_contradiction_clause,[],[f1600]) ).
fof(f1606,plain,
( e0 = e1
| ~ spl24_14
| ~ spl24_15 ),
inference(forward_demodulation,[],[f396,f400]) ).
fof(f1612,plain,
( $false
| ~ spl24_14
| ~ spl24_15 ),
inference(forward_subsumption_resolution,[],[f1606,f152]) ).
fof(f1613,plain,
( ~ spl24_14
| ~ spl24_15 ),
inference(avatar_contradiction_clause,[],[f1612]) ).
fof(f1618,plain,
( e0 = e2
| ~ spl24_18
| ~ spl24_20 ),
inference(superposition,[],[f421,f413]) ).
fof(f1620,plain,
( e0 = e2
| ~ spl24_18
| ~ spl24_20 ),
inference(superposition,[],[f413,f421]) ).
fof(f1621,plain,
( $false
| ~ spl24_18
| ~ spl24_20 ),
inference(forward_subsumption_resolution,[],[f1620,f151]) ).
fof(f1622,plain,
( ~ spl24_18
| ~ spl24_20 ),
inference(avatar_contradiction_clause,[],[f1621]) ).
fof(f1623,plain,
( $false
| ~ spl24_18
| ~ spl24_20 ),
inference(forward_subsumption_resolution,[],[f1618,f151]) ).
fof(f1624,plain,
( ~ spl24_18
| ~ spl24_20 ),
inference(avatar_contradiction_clause,[],[f1623]) ).
fof(f1626,plain,
( e1 = e3
| ~ spl24_2
| ~ spl24_4 ),
inference(superposition,[],[f354,f346]) ).
fof(f1630,plain,
( $false
| ~ spl24_2
| ~ spl24_4 ),
inference(forward_subsumption_resolution,[],[f1626,f147]) ).
fof(f1631,plain,
( ~ spl24_2
| ~ spl24_4 ),
inference(avatar_contradiction_clause,[],[f1630]) ).
fof(f1638,plain,
( e0 = e3
| ~ spl24_22
| ~ spl24_25 ),
inference(superposition,[],[f442,f430]) ).
fof(f1643,plain,
( $false
| ~ spl24_22
| ~ spl24_25 ),
inference(forward_subsumption_resolution,[],[f1638,f150]) ).
fof(f1644,plain,
( ~ spl24_22
| ~ spl24_25 ),
inference(avatar_contradiction_clause,[],[f1643]) ).
fof(f1649,plain,
( e2 = e3
| ~ spl24_22
| ~ spl24_23 ),
inference(superposition,[],[f434,f430]) ).
fof(f1653,plain,
( $false
| ~ spl24_22
| ~ spl24_23 ),
inference(forward_subsumption_resolution,[],[f1649,f145]) ).
fof(f1654,plain,
( ~ spl24_22
| ~ spl24_23 ),
inference(avatar_contradiction_clause,[],[f1653]) ).
fof(f1655,plain,
( e1 = e2
| ~ spl24_13
| ~ spl24_14 ),
inference(forward_demodulation,[],[f392,f396]) ).
fof(f1657,plain,
( $false
| ~ spl24_13
| ~ spl24_14 ),
inference(forward_subsumption_resolution,[],[f1655,f148]) ).
fof(f1658,plain,
( ~ spl24_13
| ~ spl24_14 ),
inference(avatar_contradiction_clause,[],[f1657]) ).
fof(f1659,plain,
( e0 = e3
| ~ spl24_72
| ~ spl24_75 ),
inference(forward_demodulation,[],[f640,f652]) ).
fof(f1664,plain,
( $false
| ~ spl24_72
| ~ spl24_75 ),
inference(forward_subsumption_resolution,[],[f1659,f150]) ).
fof(f1665,plain,
( ~ spl24_72
| ~ spl24_75 ),
inference(avatar_contradiction_clause,[],[f1664]) ).
fof(f1680,plain,
( e0 = e4
| ~ spl24_51
| ~ spl24_55 ),
inference(superposition,[],[f568,f552]) ).
fof(f1684,plain,
( $false
| ~ spl24_51
| ~ spl24_55 ),
inference(forward_subsumption_resolution,[],[f1680,f149]) ).
fof(f1685,plain,
( ~ spl24_51
| ~ spl24_55 ),
inference(avatar_contradiction_clause,[],[f1684]) ).
fof(f1687,plain,
( e3 = e4
| ~ spl24_56
| ~ spl24_57 ),
inference(superposition,[],[f577,f573]) ).
fof(f1691,plain,
( $false
| ~ spl24_56
| ~ spl24_57 ),
inference(forward_subsumption_resolution,[],[f1687,f143]) ).
fof(f1692,plain,
( ~ spl24_56
| ~ spl24_57 ),
inference(avatar_contradiction_clause,[],[f1691]) ).
fof(f1695,plain,
( e2 = e3
| ~ spl24_57
| ~ spl24_58 ),
inference(superposition,[],[f581,f577]) ).
fof(f1699,plain,
( $false
| ~ spl24_57
| ~ spl24_58 ),
inference(forward_subsumption_resolution,[],[f1695,f145]) ).
fof(f1700,plain,
( ~ spl24_57
| ~ spl24_58 ),
inference(avatar_contradiction_clause,[],[f1699]) ).
fof(f1704,plain,
( e1 = e2
| ~ spl24_59
| ~ spl24_127 ),
inference(forward_demodulation,[],[f1327,f585]) ).
fof(f1707,plain,
( $false
| ~ spl24_59
| ~ spl24_127 ),
inference(forward_subsumption_resolution,[],[f1704,f148]) ).
fof(f1708,plain,
( ~ spl24_59
| ~ spl24_127 ),
inference(avatar_contradiction_clause,[],[f1707]) ).
fof(f1709,plain,
( e0 = e3
| ~ spl24_17
| ~ spl24_20 ),
inference(forward_demodulation,[],[f409,f421]) ).
fof(f1712,plain,
( spl24_58
| ~ spl24_127 ),
inference(avatar_split_clause,[],[f1327,f869,f579]) ).
fof(f1713,plain,
( $false
| ~ spl24_17
| ~ spl24_20 ),
inference(forward_subsumption_resolution,[],[f1709,f150]) ).
fof(f1714,plain,
( ~ spl24_17
| ~ spl24_20 ),
inference(avatar_contradiction_clause,[],[f1713]) ).
fof(f1729,plain,
( e1 = e3
| ~ spl24_117
| ~ spl24_119 ),
inference(forward_demodulation,[],[f829,f837]) ).
fof(f1730,plain,
( $false
| ~ spl24_117
| ~ spl24_119 ),
inference(forward_subsumption_resolution,[],[f1729,f147]) ).
fof(f1731,plain,
( ~ spl24_117
| ~ spl24_119 ),
inference(avatar_contradiction_clause,[],[f1730]) ).
fof(f1737,plain,
( e2 = e3
| ~ spl24_32
| ~ spl24_33 ),
inference(superposition,[],[f476,f472]) ).
fof(f1738,plain,
( e2 = e3
| ~ spl24_32
| ~ spl24_33 ),
inference(superposition,[],[f472,f476]) ).
fof(f1739,plain,
( $false
| ~ spl24_32
| ~ spl24_33 ),
inference(forward_subsumption_resolution,[],[f1738,f145]) ).
fof(f1740,plain,
( ~ spl24_32
| ~ spl24_33 ),
inference(avatar_contradiction_clause,[],[f1739]) ).
fof(f1741,plain,
( $false
| ~ spl24_32
| ~ spl24_33 ),
inference(forward_subsumption_resolution,[],[f1737,f145]) ).
fof(f1742,plain,
( ~ spl24_32
| ~ spl24_33 ),
inference(avatar_contradiction_clause,[],[f1741]) ).
fof(f1745,plain,
( e0 = e1
| ~ spl24_64
| ~ spl24_65 ),
inference(superposition,[],[f610,f606]) ).
fof(f1749,plain,
( $false
| ~ spl24_64
| ~ spl24_65 ),
inference(forward_subsumption_resolution,[],[f1745,f152]) ).
fof(f1750,plain,
( ~ spl24_64
| ~ spl24_65 ),
inference(avatar_contradiction_clause,[],[f1749]) ).
fof(f1753,plain,
( e1 = e3
| ~ spl24_97
| ~ spl24_99 ),
inference(forward_demodulation,[],[f745,f753]) ).
fof(f1754,plain,
( $false
| ~ spl24_97
| ~ spl24_99 ),
inference(forward_subsumption_resolution,[],[f1753,f147]) ).
fof(f1755,plain,
( ~ spl24_97
| ~ spl24_99 ),
inference(avatar_contradiction_clause,[],[f1754]) ).
fof(f1761,plain,
( e3 = e4
| ~ spl24_66
| ~ spl24_67 ),
inference(superposition,[],[f619,f615]) ).
fof(f1765,plain,
( $false
| ~ spl24_66
| ~ spl24_67 ),
inference(forward_subsumption_resolution,[],[f1761,f143]) ).
fof(f1766,plain,
( ~ spl24_66
| ~ spl24_67 ),
inference(avatar_contradiction_clause,[],[f1765]) ).
fof(f1769,plain,
( e3 = e4
| ~ spl24_71
| ~ spl24_72 ),
inference(superposition,[],[f640,f636]) ).
fof(f1773,plain,
( $false
| ~ spl24_71
| ~ spl24_72 ),
inference(forward_subsumption_resolution,[],[f1769,f143]) ).
fof(f1774,plain,
( ~ spl24_71
| ~ spl24_72 ),
inference(avatar_contradiction_clause,[],[f1773]) ).
fof(f1775,plain,
( e1 = e4
| ~ spl24_61
| ~ spl24_64 ),
inference(forward_demodulation,[],[f594,f606]) ).
fof(f1780,plain,
( $false
| ~ spl24_61
| ~ spl24_64 ),
inference(forward_subsumption_resolution,[],[f1775,f146]) ).
fof(f1781,plain,
( ~ spl24_61
| ~ spl24_64 ),
inference(avatar_contradiction_clause,[],[f1780]) ).
fof(f1782,plain,
( e2 = e4
| ~ spl24_56
| ~ spl24_58 ),
inference(forward_demodulation,[],[f573,f581]) ).
fof(f1784,plain,
( $false
| ~ spl24_56
| ~ spl24_58 ),
inference(forward_subsumption_resolution,[],[f1782,f144]) ).
fof(f1785,plain,
( ~ spl24_56
| ~ spl24_58 ),
inference(avatar_contradiction_clause,[],[f1784]) ).
fof(f1790,plain,
( e0 = e3
| ~ spl24_67
| ~ spl24_70 ),
inference(superposition,[],[f631,f619]) ).
fof(f1791,plain,
( e0 = e3
| ~ spl24_67
| ~ spl24_70 ),
inference(superposition,[],[f619,f631]) ).
fof(f1792,plain,
( $false
| ~ spl24_67
| ~ spl24_70 ),
inference(forward_subsumption_resolution,[],[f1791,f150]) ).
fof(f1793,plain,
( ~ spl24_67
| ~ spl24_70 ),
inference(avatar_contradiction_clause,[],[f1792]) ).
fof(f1794,plain,
( $false
| ~ spl24_67
| ~ spl24_70 ),
inference(forward_subsumption_resolution,[],[f1790,f150]) ).
fof(f1795,plain,
( ~ spl24_67
| ~ spl24_70 ),
inference(avatar_contradiction_clause,[],[f1794]) ).
fof(f1803,plain,
( e1 = e2
| ~ spl24_98
| ~ spl24_99 ),
inference(forward_demodulation,[],[f749,f753]) ).
fof(f1807,plain,
( $false
| ~ spl24_98
| ~ spl24_99 ),
inference(forward_subsumption_resolution,[],[f1803,f148]) ).
fof(f1808,plain,
( ~ spl24_98
| ~ spl24_99 ),
inference(avatar_contradiction_clause,[],[f1807]) ).
fof(f1846,plain,
( e0 = e4
| ~ spl24_71
| ~ spl24_75 ),
inference(superposition,[],[f652,f636]) ).
fof(f1850,plain,
( $false
| ~ spl24_71
| ~ spl24_75 ),
inference(forward_subsumption_resolution,[],[f1846,f149]) ).
fof(f1851,plain,
( ~ spl24_71
| ~ spl24_75 ),
inference(avatar_contradiction_clause,[],[f1850]) ).
fof(f1854,plain,
( e0 = e2
| ~ spl24_78
| ~ spl24_80 ),
inference(forward_demodulation,[],[f665,f673]) ).
fof(f1862,plain,
( $false
| ~ spl24_78
| ~ spl24_80 ),
inference(forward_subsumption_resolution,[],[f1854,f151]) ).
fof(f1863,plain,
( ~ spl24_78
| ~ spl24_80 ),
inference(avatar_contradiction_clause,[],[f1862]) ).
fof(f1873,plain,
( e3 = e4
| ~ spl24_81
| ~ spl24_82 ),
inference(superposition,[],[f682,f678]) ).
fof(f1877,plain,
( $false
| ~ spl24_81
| ~ spl24_82 ),
inference(forward_subsumption_resolution,[],[f1873,f143]) ).
fof(f1878,plain,
( ~ spl24_81
| ~ spl24_82 ),
inference(avatar_contradiction_clause,[],[f1877]) ).
fof(f1888,plain,
( e2 = e4
| ~ spl24_91
| ~ spl24_93 ),
inference(superposition,[],[f728,f720]) ).
fof(f1892,plain,
( $false
| ~ spl24_91
| ~ spl24_93 ),
inference(forward_subsumption_resolution,[],[f1888,f144]) ).
fof(f1893,plain,
( ~ spl24_91
| ~ spl24_93 ),
inference(avatar_contradiction_clause,[],[f1892]) ).
fof(f1910,plain,
( e1 = e3
| ~ spl24_32
| ~ spl24_34 ),
inference(superposition,[],[f480,f472]) ).
fof(f1914,plain,
( $false
| ~ spl24_32
| ~ spl24_34 ),
inference(forward_subsumption_resolution,[],[f1910,f147]) ).
fof(f1915,plain,
( ~ spl24_32
| ~ spl24_34 ),
inference(avatar_contradiction_clause,[],[f1914]) ).
fof(f1936,plain,
( e1 = e3
| ~ spl24_52
| ~ spl24_54 ),
inference(forward_demodulation,[],[f556,f564]) ).
fof(f1938,plain,
( e1 = e2
| ~ spl24_118
| ~ spl24_119 ),
inference(forward_demodulation,[],[f833,f837]) ).
fof(f1939,plain,
( $false
| ~ spl24_52
| ~ spl24_54 ),
inference(forward_subsumption_resolution,[],[f1936,f147]) ).
fof(f1940,plain,
( ~ spl24_52
| ~ spl24_54 ),
inference(avatar_contradiction_clause,[],[f1939]) ).
fof(f1941,plain,
( $false
| ~ spl24_118
| ~ spl24_119 ),
inference(forward_subsumption_resolution,[],[f1938,f148]) ).
fof(f1942,plain,
( ~ spl24_118
| ~ spl24_119 ),
inference(avatar_contradiction_clause,[],[f1941]) ).
fof(f1944,plain,
( e2 = e3
| ~ spl24_77
| ~ spl24_78 ),
inference(forward_demodulation,[],[f661,f665]) ).
fof(f1946,plain,
( $false
| ~ spl24_77
| ~ spl24_78 ),
inference(forward_subsumption_resolution,[],[f1944,f145]) ).
fof(f1947,plain,
( ~ spl24_77
| ~ spl24_78 ),
inference(avatar_contradiction_clause,[],[f1946]) ).
fof(f1964,plain,
( e0 = e2
| ~ spl24_23
| ~ spl24_25 ),
inference(superposition,[],[f434,f442]) ).
fof(f1966,plain,
( $false
| ~ spl24_23
| ~ spl24_25 ),
inference(forward_subsumption_resolution,[],[f1964,f151]) ).
fof(f1967,plain,
( ~ spl24_23
| ~ spl24_25 ),
inference(avatar_contradiction_clause,[],[f1966]) ).
fof(f1973,plain,
( e1 = e2
| ~ spl24_38
| ~ spl24_39 ),
inference(superposition,[],[f501,f497]) ).
fof(f1977,plain,
( $false
| ~ spl24_38
| ~ spl24_39 ),
inference(forward_subsumption_resolution,[],[f1973,f148]) ).
fof(f1978,plain,
( ~ spl24_38
| ~ spl24_39 ),
inference(avatar_contradiction_clause,[],[f1977]) ).
fof(f1987,plain,
( e3 = e4
| ~ spl24_51
| ~ spl24_52 ),
inference(superposition,[],[f556,f552]) ).
fof(f1991,plain,
( $false
| ~ spl24_51
| ~ spl24_52 ),
inference(forward_subsumption_resolution,[],[f1987,f143]) ).
fof(f1992,plain,
( ~ spl24_51
| ~ spl24_52 ),
inference(avatar_contradiction_clause,[],[f1991]) ).
fof(f2000,plain,
( e0 = e3
| ~ spl24_52
| ~ spl24_55 ),
inference(superposition,[],[f568,f556]) ).
fof(f2001,plain,
( e0 = e3
| ~ spl24_52
| ~ spl24_55 ),
inference(superposition,[],[f556,f568]) ).
fof(f2002,plain,
( $false
| ~ spl24_52
| ~ spl24_55 ),
inference(forward_subsumption_resolution,[],[f2001,f150]) ).
fof(f2003,plain,
( ~ spl24_52
| ~ spl24_55 ),
inference(avatar_contradiction_clause,[],[f2002]) ).
fof(f2004,plain,
( $false
| ~ spl24_52
| ~ spl24_55 ),
inference(forward_subsumption_resolution,[],[f2000,f150]) ).
fof(f2005,plain,
( ~ spl24_52
| ~ spl24_55 ),
inference(avatar_contradiction_clause,[],[f2004]) ).
fof(f2027,plain,
( e0 = e4
| ~ spl24_91
| ~ spl24_95 ),
inference(superposition,[],[f736,f720]) ).
fof(f2031,plain,
( $false
| ~ spl24_91
| ~ spl24_95 ),
inference(forward_subsumption_resolution,[],[f2027,f149]) ).
fof(f2032,plain,
( ~ spl24_91
| ~ spl24_95 ),
inference(avatar_contradiction_clause,[],[f2031]) ).
fof(f2034,plain,
( e0 = e2
| ~ spl24_3
| ~ spl24_5 ),
inference(superposition,[],[f358,f350]) ).
fof(f2039,plain,
( $false
| ~ spl24_3
| ~ spl24_5 ),
inference(forward_subsumption_resolution,[],[f2034,f151]) ).
fof(f2040,plain,
( ~ spl24_3
| ~ spl24_5 ),
inference(avatar_contradiction_clause,[],[f2039]) ).
fof(f2047,plain,
( e0 = e1
| ~ spl24_119
| ~ spl24_120 ),
inference(forward_demodulation,[],[f837,f841]) ).
fof(f2048,plain,
( e1 = e3
| ~ spl24_122
| ~ spl24_124 ),
inference(forward_demodulation,[],[f850,f858]) ).
fof(f2066,plain,
( $false
| ~ spl24_119
| ~ spl24_120 ),
inference(forward_subsumption_resolution,[],[f2047,f152]) ).
fof(f2067,plain,
( ~ spl24_119
| ~ spl24_120 ),
inference(avatar_contradiction_clause,[],[f2066]) ).
fof(f2068,plain,
( $false
| ~ spl24_122
| ~ spl24_124 ),
inference(forward_subsumption_resolution,[],[f2048,f147]) ).
fof(f2069,plain,
( ~ spl24_122
| ~ spl24_124 ),
inference(avatar_contradiction_clause,[],[f2068]) ).
fof(f2078,plain,
( e4 = op(e4,e4)
| ~ spl24_126 ),
inference(superposition,[],[f304,f867]) ).
fof(f2083,plain,
( e2 = op(e4,e2)
| ~ spl24_126 ),
inference(superposition,[],[f309,f867]) ).
fof(f2092,plain,
( $false
| spl24_13
| ~ spl24_126 ),
inference(forward_subsumption_resolution,[],[f2083,f391]) ).
fof(f2093,plain,
( spl24_13
| ~ spl24_126 ),
inference(avatar_contradiction_clause,[],[f2092]) ).
fof(f2099,plain,
( e0 = e4
| ~ spl24_5
| ~ spl24_126 ),
inference(forward_demodulation,[],[f2078,f358]) ).
fof(f2104,plain,
( $false
| ~ spl24_5
| ~ spl24_126 ),
inference(forward_subsumption_resolution,[],[f2099,f149]) ).
fof(f2105,plain,
( ~ spl24_5
| ~ spl24_126 ),
inference(avatar_contradiction_clause,[],[f2104]) ).
fof(f2109,plain,
( e0 = e2
| ~ spl24_123
| ~ spl24_125 ),
inference(forward_demodulation,[],[f854,f862]) ).
fof(f2118,plain,
( $false
| ~ spl24_123
| ~ spl24_125 ),
inference(forward_subsumption_resolution,[],[f2109,f151]) ).
fof(f2119,plain,
( ~ spl24_123
| ~ spl24_125 ),
inference(avatar_contradiction_clause,[],[f2118]) ).
fof(f2129,plain,
( e0 = op(e0,e3)
| ~ spl24_127 ),
inference(superposition,[],[f312,f871]) ).
fof(f2133,plain,
( spl24_110
| ~ spl24_127 ),
inference(avatar_split_clause,[],[f2129,f869,f797]) ).
fof(f2150,plain,
( e3 = e4
| ~ spl24_91
| ~ spl24_92 ),
inference(superposition,[],[f724,f720]) ).
fof(f2154,plain,
( $false
| ~ spl24_91
| ~ spl24_92 ),
inference(forward_subsumption_resolution,[],[f2150,f143]) ).
fof(f2155,plain,
( ~ spl24_91
| ~ spl24_92 ),
inference(avatar_contradiction_clause,[],[f2154]) ).
fof(f2161,plain,
( e0 = e4
| ~ spl24_66
| ~ spl24_70 ),
inference(superposition,[],[f631,f615]) ).
fof(f2165,plain,
( $false
| ~ spl24_66
| ~ spl24_70 ),
inference(forward_subsumption_resolution,[],[f2161,f149]) ).
fof(f2166,plain,
( ~ spl24_66
| ~ spl24_70 ),
inference(avatar_contradiction_clause,[],[f2165]) ).
fof(f2212,plain,
( e1 = e4
| ~ spl24_51
| ~ spl24_54 ),
inference(superposition,[],[f564,f552]) ).
fof(f2216,plain,
( $false
| ~ spl24_51
| ~ spl24_54 ),
inference(forward_subsumption_resolution,[],[f2212,f146]) ).
fof(f2217,plain,
( ~ spl24_51
| ~ spl24_54 ),
inference(avatar_contradiction_clause,[],[f2216]) ).
fof(f2227,plain,
( e0 = e2
| ~ spl24_88
| ~ spl24_90 ),
inference(forward_demodulation,[],[f707,f715]) ).
fof(f2228,plain,
( $false
| ~ spl24_88
| ~ spl24_90 ),
inference(forward_subsumption_resolution,[],[f2227,f151]) ).
fof(f2229,plain,
( ~ spl24_88
| ~ spl24_90 ),
inference(avatar_contradiction_clause,[],[f2228]) ).
fof(f2239,plain,
( e1 = e3
| ~ spl24_67
| ~ spl24_69 ),
inference(superposition,[],[f627,f619]) ).
fof(f2240,plain,
( e1 = e3
| ~ spl24_67
| ~ spl24_69 ),
inference(superposition,[],[f619,f627]) ).
fof(f2242,plain,
( $false
| ~ spl24_67
| ~ spl24_69 ),
inference(forward_subsumption_resolution,[],[f2240,f147]) ).
fof(f2243,plain,
( ~ spl24_67
| ~ spl24_69 ),
inference(avatar_contradiction_clause,[],[f2242]) ).
fof(f2244,plain,
( $false
| ~ spl24_67
| ~ spl24_69 ),
inference(forward_subsumption_resolution,[],[f2239,f147]) ).
fof(f2245,plain,
( ~ spl24_67
| ~ spl24_69 ),
inference(avatar_contradiction_clause,[],[f2244]) ).
fof(f2247,plain,
( e0 = e1
| ~ spl24_74
| ~ spl24_75 ),
inference(forward_demodulation,[],[f648,f652]) ).
fof(f2248,plain,
( $false
| ~ spl24_74
| ~ spl24_75 ),
inference(forward_subsumption_resolution,[],[f2247,f152]) ).
fof(f2249,plain,
( ~ spl24_74
| ~ spl24_75 ),
inference(avatar_contradiction_clause,[],[f2248]) ).
fof(f2253,plain,
( e0 = e2
| ~ spl24_73
| ~ spl24_75 ),
inference(forward_demodulation,[],[f644,f652]) ).
fof(f2281,plain,
( $false
| ~ spl24_73
| ~ spl24_75 ),
inference(forward_subsumption_resolution,[],[f2253,f151]) ).
fof(f2282,plain,
( ~ spl24_73
| ~ spl24_75 ),
inference(avatar_contradiction_clause,[],[f2281]) ).
fof(f2288,plain,
( e0 = e3
| ~ spl24_42
| ~ spl24_45 ),
inference(forward_demodulation,[],[f514,f526]) ).
fof(f2289,plain,
( e0 = e2
| ~ spl24_43
| ~ spl24_45 ),
inference(forward_demodulation,[],[f518,f526]) ).
fof(f2294,plain,
( e0 = e1
| ~ spl24_89
| ~ spl24_90 ),
inference(forward_demodulation,[],[f711,f715]) ).
fof(f2328,plain,
( $false
| ~ spl24_42
| ~ spl24_45 ),
inference(forward_subsumption_resolution,[],[f2288,f150]) ).
fof(f2329,plain,
( ~ spl24_42
| ~ spl24_45 ),
inference(avatar_contradiction_clause,[],[f2328]) ).
fof(f2330,plain,
( $false
| ~ spl24_43
| ~ spl24_45 ),
inference(forward_subsumption_resolution,[],[f2289,f151]) ).
fof(f2331,plain,
( ~ spl24_43
| ~ spl24_45 ),
inference(avatar_contradiction_clause,[],[f2330]) ).
fof(f2332,plain,
( $false
| ~ spl24_89
| ~ spl24_90 ),
inference(forward_subsumption_resolution,[],[f2294,f152]) ).
fof(f2333,plain,
( ~ spl24_89
| ~ spl24_90 ),
inference(avatar_contradiction_clause,[],[f2332]) ).
fof(f2337,plain,
( e1 = e2
| ~ spl24_68
| ~ spl24_69 ),
inference(forward_demodulation,[],[f623,f627]) ).
fof(f2345,plain,
( $false
| ~ spl24_68
| ~ spl24_69 ),
inference(forward_subsumption_resolution,[],[f2337,f148]) ).
fof(f2346,plain,
( ~ spl24_68
| ~ spl24_69 ),
inference(avatar_contradiction_clause,[],[f2345]) ).
fof(f2347,plain,
( e4 = op(e4,e4)
| ~ spl24_126 ),
inference(superposition,[],[f304,f867]) ).
fof(f2359,plain,
( e3 = e4
| ~ spl24_36
| ~ spl24_37 ),
inference(forward_demodulation,[],[f489,f493]) ).
fof(f2362,plain,
( $false
| ~ spl24_36
| ~ spl24_37 ),
inference(forward_subsumption_resolution,[],[f2359,f143]) ).
fof(f2363,plain,
( ~ spl24_36
| ~ spl24_37 ),
inference(avatar_contradiction_clause,[],[f2362]) ).
fof(f2372,plain,
( e2 = e4
| ~ spl24_31
| ~ spl24_33 ),
inference(forward_demodulation,[],[f468,f476]) ).
fof(f2374,plain,
( $false
| ~ spl24_31
| ~ spl24_33 ),
inference(forward_subsumption_resolution,[],[f2372,f144]) ).
fof(f2375,plain,
( ~ spl24_31
| ~ spl24_33 ),
inference(avatar_contradiction_clause,[],[f2374]) ).
fof(f2385,plain,
( e0 = e3
| ~ spl24_7
| ~ spl24_10 ),
inference(superposition,[],[f379,f367]) ).
fof(f2391,plain,
( $false
| ~ spl24_7
| ~ spl24_10 ),
inference(forward_subsumption_resolution,[],[f2385,f150]) ).
fof(f2392,plain,
( ~ spl24_7
| ~ spl24_10 ),
inference(avatar_contradiction_clause,[],[f2391]) ).
fof(f2421,plain,
( e0 = e4
| ~ spl24_36
| ~ spl24_40 ),
inference(superposition,[],[f489,f505]) ).
fof(f2422,plain,
( $false
| ~ spl24_36
| ~ spl24_40 ),
inference(forward_subsumption_resolution,[],[f2421,f149]) ).
fof(f2423,plain,
( ~ spl24_36
| ~ spl24_40 ),
inference(avatar_contradiction_clause,[],[f2422]) ).
fof(f2438,plain,
( e1 = e4
| ~ spl24_56
| ~ spl24_59 ),
inference(superposition,[],[f585,f573]) ).
fof(f2443,plain,
( $false
| ~ spl24_56
| ~ spl24_59 ),
inference(forward_subsumption_resolution,[],[f2438,f146]) ).
fof(f2444,plain,
( ~ spl24_56
| ~ spl24_59 ),
inference(avatar_contradiction_clause,[],[f2443]) ).
fof(f2446,plain,
( e3 = e4
| ~ spl24_61
| ~ spl24_62 ),
inference(forward_demodulation,[],[f594,f598]) ).
fof(f2449,plain,
( $false
| ~ spl24_61
| ~ spl24_62 ),
inference(forward_subsumption_resolution,[],[f2446,f143]) ).
fof(f2450,plain,
( ~ spl24_61
| ~ spl24_62 ),
inference(avatar_contradiction_clause,[],[f2449]) ).
fof(f2458,plain,
( e0 = e4
| ~ spl24_56
| ~ spl24_60 ),
inference(superposition,[],[f589,f573]) ).
fof(f2463,plain,
( $false
| ~ spl24_56
| ~ spl24_60 ),
inference(forward_subsumption_resolution,[],[f2458,f149]) ).
fof(f2464,plain,
( ~ spl24_56
| ~ spl24_60 ),
inference(avatar_contradiction_clause,[],[f2463]) ).
fof(f2466,plain,
( e0 = e2
| ~ spl24_53
| ~ spl24_55 ),
inference(superposition,[],[f568,f560]) ).
fof(f2471,plain,
( $false
| ~ spl24_53
| ~ spl24_55 ),
inference(forward_subsumption_resolution,[],[f2466,f151]) ).
fof(f2472,plain,
( ~ spl24_53
| ~ spl24_55 ),
inference(avatar_contradiction_clause,[],[f2471]) ).
fof(f2475,plain,
( e0 = e3
| ~ spl24_62
| ~ spl24_65 ),
inference(superposition,[],[f610,f598]) ).
fof(f2480,plain,
( $false
| ~ spl24_62
| ~ spl24_65 ),
inference(forward_subsumption_resolution,[],[f2475,f150]) ).
fof(f2481,plain,
( ~ spl24_62
| ~ spl24_65 ),
inference(avatar_contradiction_clause,[],[f2480]) ).
fof(f2482,plain,
( e0 = e1
| ~ spl24_39
| ~ spl24_40 ),
inference(forward_demodulation,[],[f501,f505]) ).
fof(f2490,plain,
( $false
| ~ spl24_39
| ~ spl24_40 ),
inference(forward_subsumption_resolution,[],[f2482,f152]) ).
fof(f2491,plain,
( ~ spl24_39
| ~ spl24_40 ),
inference(avatar_contradiction_clause,[],[f2490]) ).
fof(f2493,plain,
( e1 = e2
| ~ spl24_33
| ~ spl24_34 ),
inference(superposition,[],[f480,f476]) ).
fof(f2494,plain,
( e1 = e2
| ~ spl24_33
| ~ spl24_34 ),
inference(superposition,[],[f476,f480]) ).
fof(f2495,plain,
( $false
| ~ spl24_33
| ~ spl24_34 ),
inference(forward_subsumption_resolution,[],[f2494,f148]) ).
fof(f2496,plain,
( ~ spl24_33
| ~ spl24_34 ),
inference(avatar_contradiction_clause,[],[f2495]) ).
fof(f2497,plain,
( $false
| ~ spl24_33
| ~ spl24_34 ),
inference(forward_subsumption_resolution,[],[f2493,f148]) ).
fof(f2498,plain,
( ~ spl24_33
| ~ spl24_34 ),
inference(avatar_contradiction_clause,[],[f2497]) ).
fof(f2508,plain,
( e0 = e2
| ~ spl24_68
| ~ spl24_70 ),
inference(forward_demodulation,[],[f623,f631]) ).
fof(f2509,plain,
( e1 = e4
| ~ spl24_71
| ~ spl24_74 ),
inference(forward_demodulation,[],[f636,f648]) ).
fof(f2517,plain,
( $false
| ~ spl24_68
| ~ spl24_70 ),
inference(forward_subsumption_resolution,[],[f2508,f151]) ).
fof(f2518,plain,
( ~ spl24_68
| ~ spl24_70 ),
inference(avatar_contradiction_clause,[],[f2517]) ).
fof(f2519,plain,
( $false
| ~ spl24_71
| ~ spl24_74 ),
inference(forward_subsumption_resolution,[],[f2509,f146]) ).
fof(f2520,plain,
( ~ spl24_71
| ~ spl24_74 ),
inference(avatar_contradiction_clause,[],[f2519]) ).
fof(f2523,plain,
( e0 = e1
| ~ spl24_69
| ~ spl24_70 ),
inference(forward_demodulation,[],[f627,f631]) ).
fof(f2527,plain,
( $false
| ~ spl24_69
| ~ spl24_70 ),
inference(forward_subsumption_resolution,[],[f2523,f152]) ).
fof(f2528,plain,
( ~ spl24_69
| ~ spl24_70 ),
inference(avatar_contradiction_clause,[],[f2527]) ).
fof(f2535,plain,
( e2 = e4
| ~ spl24_41
| ~ spl24_43 ),
inference(superposition,[],[f518,f510]) ).
fof(f2540,plain,
( $false
| ~ spl24_41
| ~ spl24_43 ),
inference(forward_subsumption_resolution,[],[f2535,f144]) ).
fof(f2541,plain,
( ~ spl24_41
| ~ spl24_43 ),
inference(avatar_contradiction_clause,[],[f2540]) ).
fof(f2545,plain,
( e0 = e2
| ~ spl24_83
| ~ spl24_85 ),
inference(forward_demodulation,[],[f686,f694]) ).
fof(f2554,plain,
( $false
| ~ spl24_83
| ~ spl24_85 ),
inference(forward_subsumption_resolution,[],[f2545,f151]) ).
fof(f2555,plain,
( ~ spl24_83
| ~ spl24_85 ),
inference(avatar_contradiction_clause,[],[f2554]) ).
fof(f2564,plain,
( e0 = e1
| ~ spl24_124
| ~ spl24_125 ),
inference(forward_demodulation,[],[f858,f862]) ).
fof(f2567,plain,
( $false
| ~ spl24_124
| ~ spl24_125 ),
inference(forward_subsumption_resolution,[],[f2564,f152]) ).
fof(f2568,plain,
( ~ spl24_124
| ~ spl24_125 ),
inference(avatar_contradiction_clause,[],[f2567]) ).
fof(f2572,plain,
( e0 = e3
| ~ spl24_122
| ~ spl24_125 ),
inference(forward_demodulation,[],[f850,f862]) ).
fof(f2577,plain,
( $false
| ~ spl24_122
| ~ spl24_125 ),
inference(forward_subsumption_resolution,[],[f2572,f150]) ).
fof(f2578,plain,
( ~ spl24_122
| ~ spl24_125 ),
inference(avatar_contradiction_clause,[],[f2577]) ).
fof(f2581,plain,
( e1 = e3
| ~ spl24_37
| ~ spl24_39 ),
inference(forward_demodulation,[],[f493,f501]) ).
fof(f2595,plain,
( $false
| ~ spl24_37
| ~ spl24_39 ),
inference(forward_subsumption_resolution,[],[f2581,f147]) ).
fof(f2596,plain,
( ~ spl24_37
| ~ spl24_39 ),
inference(avatar_contradiction_clause,[],[f2595]) ).
fof(f2608,plain,
( e1 = e4
| ~ spl24_1
| ~ spl24_4 ),
inference(superposition,[],[f354,f342]) ).
fof(f2613,plain,
( $false
| ~ spl24_1
| ~ spl24_4 ),
inference(forward_subsumption_resolution,[],[f2608,f146]) ).
fof(f2614,plain,
( ~ spl24_1
| ~ spl24_4 ),
inference(avatar_contradiction_clause,[],[f2613]) ).
fof(f2616,plain,
( e2 = e4
| ~ spl24_11
| ~ spl24_13 ),
inference(forward_demodulation,[],[f384,f392]) ).
fof(f2620,plain,
( e1 = e4
| ~ spl24_4
| ~ spl24_126 ),
inference(forward_demodulation,[],[f2347,f354]) ).
fof(f2621,plain,
( $false
| ~ spl24_11
| ~ spl24_13 ),
inference(forward_subsumption_resolution,[],[f2616,f144]) ).
fof(f2622,plain,
( ~ spl24_11
| ~ spl24_13 ),
inference(avatar_contradiction_clause,[],[f2621]) ).
fof(f2625,plain,
( $false
| ~ spl24_4
| ~ spl24_126 ),
inference(forward_subsumption_resolution,[],[f2620,f146]) ).
fof(f2626,plain,
( ~ spl24_4
| ~ spl24_126 ),
inference(avatar_contradiction_clause,[],[f2625]) ).
fof(f2630,plain,
( e2 = e4
| ~ spl24_61
| ~ spl24_63 ),
inference(forward_demodulation,[],[f594,f602]) ).
fof(f2634,plain,
( e2 = e4
| ~ spl24_3
| ~ spl24_126 ),
inference(forward_demodulation,[],[f2347,f350]) ).
fof(f2637,plain,
( $false
| ~ spl24_61
| ~ spl24_63 ),
inference(forward_subsumption_resolution,[],[f2630,f144]) ).
fof(f2638,plain,
( ~ spl24_61
| ~ spl24_63 ),
inference(avatar_contradiction_clause,[],[f2637]) ).
fof(f2641,plain,
( $false
| ~ spl24_3
| ~ spl24_126 ),
inference(forward_subsumption_resolution,[],[f2634,f144]) ).
fof(f2642,plain,
( ~ spl24_3
| ~ spl24_126 ),
inference(avatar_contradiction_clause,[],[f2641]) ).
fof(f2646,plain,
( e2 = e3
| ~ spl24_62
| ~ spl24_63 ),
inference(forward_demodulation,[],[f598,f602]) ).
fof(f2660,plain,
( $false
| ~ spl24_62
| ~ spl24_63 ),
inference(forward_subsumption_resolution,[],[f2646,f145]) ).
fof(f2661,plain,
( ~ spl24_62
| ~ spl24_63 ),
inference(avatar_contradiction_clause,[],[f2660]) ).
fof(f2685,plain,
( e1 = e4
| ~ spl24_36
| ~ spl24_39 ),
inference(forward_demodulation,[],[f489,f501]) ).
fof(f2689,plain,
( $false
| ~ spl24_36
| ~ spl24_39 ),
inference(forward_subsumption_resolution,[],[f2685,f146]) ).
fof(f2690,plain,
( ~ spl24_36
| ~ spl24_39 ),
inference(avatar_contradiction_clause,[],[f2689]) ).
fof(f2699,plain,
( e1 = e2
| ~ spl24_53
| ~ spl24_54 ),
inference(superposition,[],[f564,f560]) ).
fof(f2704,plain,
( $false
| ~ spl24_53
| ~ spl24_54 ),
inference(forward_subsumption_resolution,[],[f2699,f148]) ).
fof(f2705,plain,
( ~ spl24_53
| ~ spl24_54 ),
inference(avatar_contradiction_clause,[],[f2704]) ).
fof(f2755,plain,
( e2 = op(e0,e2)
| ~ spl24_130 ),
inference(superposition,[],[f309,f883]) ).
fof(f2763,plain,
( e1 = e2
| ~ spl24_114
| ~ spl24_130 ),
inference(forward_demodulation,[],[f2755,f816]) ).
fof(f2764,plain,
( $false
| ~ spl24_114
| ~ spl24_130 ),
inference(forward_subsumption_resolution,[],[f2763,f148]) ).
fof(f2765,plain,
( ~ spl24_114
| ~ spl24_130 ),
inference(avatar_contradiction_clause,[],[f2764]) ).
fof(f2767,plain,
( spl24_113
| ~ spl24_130 ),
inference(avatar_split_clause,[],[f2755,f881,f810]) ).
fof(f2770,plain,
( e1 = e2
| ~ spl24_3
| ~ spl24_4 ),
inference(superposition,[],[f354,f350]) ).
fof(f2776,plain,
( $false
| ~ spl24_3
| ~ spl24_4 ),
inference(forward_subsumption_resolution,[],[f2770,f148]) ).
fof(f2777,plain,
( ~ spl24_3
| ~ spl24_4 ),
inference(avatar_contradiction_clause,[],[f2776]) ).
fof(f2796,plain,
( e2 = e4
| ~ spl24_71
| ~ spl24_73 ),
inference(superposition,[],[f644,f636]) ).
fof(f2800,plain,
( $false
| ~ spl24_71
| ~ spl24_73 ),
inference(forward_subsumption_resolution,[],[f2796,f144]) ).
fof(f2801,plain,
( ~ spl24_71
| ~ spl24_73 ),
inference(avatar_contradiction_clause,[],[f2800]) ).
fof(f2802,plain,
( e0 = e1
| ~ spl24_54
| ~ spl24_55 ),
inference(forward_demodulation,[],[f564,f568]) ).
fof(f2811,plain,
( $false
| ~ spl24_54
| ~ spl24_55 ),
inference(forward_subsumption_resolution,[],[f2802,f152]) ).
fof(f2812,plain,
( ~ spl24_54
| ~ spl24_55 ),
inference(avatar_contradiction_clause,[],[f2811]) ).
fof(f2869,plain,
( e0 = e1
| ~ spl24_4
| ~ spl24_5 ),
inference(superposition,[],[f358,f354]) ).
fof(f2876,plain,
( $false
| ~ spl24_4
| ~ spl24_5 ),
inference(forward_subsumption_resolution,[],[f2869,f152]) ).
fof(f2877,plain,
( ~ spl24_4
| ~ spl24_5 ),
inference(avatar_contradiction_clause,[],[f2876]) ).
fof(f2917,plain,
( e1 = e3
| ~ spl24_72
| ~ spl24_74 ),
inference(superposition,[],[f640,f648]) ).
fof(f2919,plain,
( $false
| ~ spl24_72
| ~ spl24_74 ),
inference(forward_subsumption_resolution,[],[f2917,f147]) ).
fof(f2920,plain,
( ~ spl24_72
| ~ spl24_74 ),
inference(avatar_contradiction_clause,[],[f2919]) ).
fof(f2954,plain,
( e1 = e4
| ~ spl24_91
| ~ spl24_94 ),
inference(superposition,[],[f732,f720]) ).
fof(f2958,plain,
( $false
| ~ spl24_91
| ~ spl24_94 ),
inference(forward_subsumption_resolution,[],[f2954,f146]) ).
fof(f2959,plain,
( ~ spl24_91
| ~ spl24_94 ),
inference(avatar_contradiction_clause,[],[f2958]) ).
fof(f2971,plain,
( e1 = e4
| ~ spl24_66
| ~ spl24_69 ),
inference(superposition,[],[f627,f615]) ).
fof(f2977,plain,
( $false
| ~ spl24_66
| ~ spl24_69 ),
inference(forward_subsumption_resolution,[],[f2971,f146]) ).
fof(f2978,plain,
( ~ spl24_66
| ~ spl24_69 ),
inference(avatar_contradiction_clause,[],[f2977]) ).
fof(f3043,plain,
( e1 = e4
| ~ spl24_31
| ~ spl24_34 ),
inference(superposition,[],[f480,f468]) ).
fof(f3047,plain,
( $false
| ~ spl24_31
| ~ spl24_34 ),
inference(forward_subsumption_resolution,[],[f3043,f146]) ).
fof(f3048,plain,
( ~ spl24_31
| ~ spl24_34 ),
inference(avatar_contradiction_clause,[],[f3047]) ).
fof(f3099,plain,
( e0 = e4
| ~ spl24_1
| ~ spl24_5 ),
inference(superposition,[],[f358,f342]) ).
fof(f3105,plain,
( $false
| ~ spl24_1
| ~ spl24_5 ),
inference(forward_subsumption_resolution,[],[f3099,f149]) ).
fof(f3106,plain,
( ~ spl24_1
| ~ spl24_5 ),
inference(avatar_contradiction_clause,[],[f3105]) ).
fof(f3138,plain,
( e3 = e4
| ~ spl24_106
| ~ spl24_107 ),
inference(superposition,[],[f787,f783]) ).
fof(f3142,plain,
( $false
| ~ spl24_106
| ~ spl24_107 ),
inference(forward_subsumption_resolution,[],[f3138,f143]) ).
fof(f3143,plain,
( ~ spl24_106
| ~ spl24_107 ),
inference(avatar_contradiction_clause,[],[f3142]) ).
fof(f3155,plain,
( e3 = e4
| ~ spl24_111
| ~ spl24_112 ),
inference(superposition,[],[f808,f804]) ).
fof(f3159,plain,
( $false
| ~ spl24_111
| ~ spl24_112 ),
inference(forward_subsumption_resolution,[],[f3155,f143]) ).
fof(f3160,plain,
( ~ spl24_111
| ~ spl24_112 ),
inference(avatar_contradiction_clause,[],[f3159]) ).
fof(f3161,plain,
( e0 = e4
| ~ spl24_86
| ~ spl24_90 ),
inference(forward_demodulation,[],[f699,f715]) ).
fof(f3165,plain,
( $false
| ~ spl24_86
| ~ spl24_90 ),
inference(forward_subsumption_resolution,[],[f3161,f149]) ).
fof(f3166,plain,
( ~ spl24_86
| ~ spl24_90 ),
inference(avatar_contradiction_clause,[],[f3165]) ).
fof(f3220,plain,
( e1 = e4
| ~ spl24_111
| ~ spl24_114 ),
inference(superposition,[],[f816,f804]) ).
fof(f3221,plain,
( e1 = e4
| ~ spl24_111
| ~ spl24_114 ),
inference(superposition,[],[f804,f816]) ).
fof(f3222,plain,
( $false
| ~ spl24_111
| ~ spl24_114 ),
inference(forward_subsumption_resolution,[],[f3221,f146]) ).
fof(f3223,plain,
( ~ spl24_111
| ~ spl24_114 ),
inference(avatar_contradiction_clause,[],[f3222]) ).
fof(f3224,plain,
( $false
| ~ spl24_111
| ~ spl24_114 ),
inference(forward_subsumption_resolution,[],[f3220,f146]) ).
fof(f3225,plain,
( ~ spl24_111
| ~ spl24_114 ),
inference(avatar_contradiction_clause,[],[f3224]) ).
fof(f3237,plain,
( e2 = e4
| ~ spl24_121
| ~ spl24_123 ),
inference(superposition,[],[f854,f846]) ).
fof(f3241,plain,
( $false
| ~ spl24_121
| ~ spl24_123 ),
inference(forward_subsumption_resolution,[],[f3237,f144]) ).
fof(f3242,plain,
( ~ spl24_121
| ~ spl24_123 ),
inference(avatar_contradiction_clause,[],[f3241]) ).
fof(f3280,plain,
( e0 = e4
| ~ spl24_61
| ~ spl24_65 ),
inference(superposition,[],[f610,f594]) ).
fof(f3285,plain,
( $false
| ~ spl24_61
| ~ spl24_65 ),
inference(forward_subsumption_resolution,[],[f3280,f149]) ).
fof(f3286,plain,
( ~ spl24_61
| ~ spl24_65 ),
inference(avatar_contradiction_clause,[],[f3285]) ).
fof(f3294,plain,
( e0 = e2
| ~ spl24_63
| ~ spl24_65 ),
inference(forward_demodulation,[],[f602,f610]) ).
fof(f3299,plain,
( e0 = e3
| ~ spl24_107
| ~ spl24_110 ),
inference(forward_demodulation,[],[f787,f799]) ).
fof(f3334,plain,
( $false
| ~ spl24_63
| ~ spl24_65 ),
inference(forward_subsumption_resolution,[],[f3294,f151]) ).
fof(f3335,plain,
( ~ spl24_63
| ~ spl24_65 ),
inference(avatar_contradiction_clause,[],[f3334]) ).
fof(f3336,plain,
( $false
| ~ spl24_107
| ~ spl24_110 ),
inference(forward_subsumption_resolution,[],[f3299,f150]) ).
fof(f3337,plain,
( ~ spl24_107
| ~ spl24_110 ),
inference(avatar_contradiction_clause,[],[f3336]) ).
fof(f3341,plain,
( e0 = e2
| ~ spl24_28
| ~ spl24_30 ),
inference(forward_demodulation,[],[f455,f463]) ).
fof(f3347,plain,
( e2 = e4
| ~ spl24_81
| ~ spl24_83 ),
inference(forward_demodulation,[],[f678,f686]) ).
fof(f3374,plain,
( $false
| ~ spl24_28
| ~ spl24_30 ),
inference(forward_subsumption_resolution,[],[f3341,f151]) ).
fof(f3375,plain,
( ~ spl24_28
| ~ spl24_30 ),
inference(avatar_contradiction_clause,[],[f3374]) ).
fof(f3376,plain,
( $false
| ~ spl24_81
| ~ spl24_83 ),
inference(forward_subsumption_resolution,[],[f3347,f144]) ).
fof(f3377,plain,
( ~ spl24_81
| ~ spl24_83 ),
inference(avatar_contradiction_clause,[],[f3376]) ).
fof(f3378,plain,
( e0 = e3
| ~ spl24_27
| ~ spl24_30 ),
inference(forward_demodulation,[],[f451,f463]) ).
fof(f3391,plain,
( $false
| ~ spl24_27
| ~ spl24_30 ),
inference(forward_subsumption_resolution,[],[f3378,f150]) ).
fof(f3392,plain,
( ~ spl24_27
| ~ spl24_30 ),
inference(avatar_contradiction_clause,[],[f3391]) ).
cnf(s1,plain,
( spl24_1
| spl24_2
| spl24_3
| spl24_4
| spl24_5 ),
inference(sat_conversion,[],[f359]) ).
cnf(s26,plain,
( spl24_126
| spl24_127
| spl24_128
| spl24_129
| spl24_130 ),
inference(sat_conversion,[],[f884]) ).
cnf(s29,plain,
( spl24_2
| spl24_27
| spl24_52
| spl24_77
| spl24_102 ),
inference(sat_conversion,[],[f887]) ).
cnf(s30,plain,
( spl24_2
| spl24_7
| spl24_12
| spl24_17
| spl24_22 ),
inference(sat_conversion,[],[f888]) ).
cnf(s31,plain,
( spl24_3
| spl24_28
| spl24_53
| spl24_78
| spl24_103 ),
inference(sat_conversion,[],[f889]) ).
cnf(s32,plain,
( spl24_3
| spl24_8
| spl24_13
| spl24_18
| spl24_23 ),
inference(sat_conversion,[],[f890]) ).
cnf(s35,plain,
( spl24_5
| spl24_30
| spl24_55
| spl24_80
| spl24_105 ),
inference(sat_conversion,[],[f893]) ).
cnf(s36,plain,
( spl24_5
| spl24_10
| spl24_15
| spl24_20
| spl24_25 ),
inference(sat_conversion,[],[f894]) ).
cnf(s37,plain,
( spl24_6
| spl24_31
| spl24_56
| spl24_81
| spl24_106 ),
inference(sat_conversion,[],[f895]) ).
cnf(s38,plain,
( spl24_26
| spl24_31
| spl24_36
| spl24_41
| spl24_46 ),
inference(sat_conversion,[],[f896]) ).
cnf(s45,plain,
( spl24_10
| spl24_35
| spl24_60
| spl24_85
| spl24_110 ),
inference(sat_conversion,[],[f903]) ).
cnf(s46,plain,
( spl24_30
| spl24_35
| spl24_40
| spl24_45
| spl24_50 ),
inference(sat_conversion,[],[f904]) ).
cnf(s47,plain,
( spl24_11
| spl24_36
| spl24_61
| spl24_86
| spl24_111 ),
inference(sat_conversion,[],[f905]) ).
cnf(s48,plain,
( spl24_51
| spl24_56
| spl24_61
| spl24_66
| spl24_71 ),
inference(sat_conversion,[],[f906]) ).
cnf(s49,plain,
( spl24_12
| spl24_37
| spl24_62
| spl24_87
| spl24_112 ),
inference(sat_conversion,[],[f907]) ).
cnf(s50,plain,
( spl24_52
| spl24_57
| spl24_62
| spl24_67
| spl24_72 ),
inference(sat_conversion,[],[f908]) ).
cnf(s53,plain,
( spl24_14
| spl24_39
| spl24_64
| spl24_89
| spl24_114 ),
inference(sat_conversion,[],[f911]) ).
cnf(s54,plain,
( spl24_54
| spl24_59
| spl24_64
| spl24_69
| spl24_74 ),
inference(sat_conversion,[],[f912]) ).
cnf(s56,plain,
( spl24_55
| spl24_60
| spl24_65
| spl24_70
| spl24_75 ),
inference(sat_conversion,[],[f914]) ).
cnf(s59,plain,
( spl24_17
| spl24_42
| spl24_67
| spl24_92
| spl24_117 ),
inference(sat_conversion,[],[f917]) ).
cnf(s60,plain,
( spl24_77
| spl24_82
| spl24_87
| spl24_92
| spl24_97 ),
inference(sat_conversion,[],[f918]) ).
cnf(s61,plain,
( spl24_18
| spl24_43
| spl24_68
| spl24_93
| spl24_118 ),
inference(sat_conversion,[],[f919]) ).
cnf(s62,plain,
( spl24_78
| spl24_83
| spl24_88
| spl24_93
| spl24_98 ),
inference(sat_conversion,[],[f920]) ).
cnf(s65,plain,
( spl24_20
| spl24_45
| spl24_70
| spl24_95
| spl24_120 ),
inference(sat_conversion,[],[f923]) ).
cnf(s69,plain,
( spl24_22
| spl24_47
| spl24_72
| spl24_97
| spl24_122 ),
inference(sat_conversion,[],[f927]) ).
cnf(s70,plain,
( spl24_102
| spl24_107
| spl24_112
| spl24_117
| spl24_122 ),
inference(sat_conversion,[],[f928]) ).
cnf(s77,plain,
spl24_91,
inference(sat_conversion,[],[f935]) ).
cnf(s78,plain,
( ~ spl24_125
| spl24_131
| spl24_132
| spl24_133
| spl24_134
| spl24_135
| spl24_136
| spl24_137
| spl24_138
| spl24_139
| spl24_140
| spl24_141
| spl24_142
| spl24_143
| spl24_144
| spl24_145
| spl24_146
| spl24_147
| spl24_148
| spl24_149
| spl24_150
| spl24_151
| spl24_152
| spl24_153
| spl24_154 ),
inference(sat_conversion,[],[f1033]) ).
cnf(s80,plain,
( spl24_125
| spl24_131
| spl24_132
| spl24_133
| spl24_134
| spl24_135
| spl24_136
| spl24_137
| spl24_138
| spl24_139
| spl24_140
| spl24_141
| spl24_142
| spl24_143
| spl24_144
| spl24_145
| spl24_146
| spl24_147
| spl24_148
| spl24_149
| spl24_150
| spl24_151
| spl24_152
| spl24_153
| spl24_154 ),
inference(sat_conversion,[],[f1035]) ).
cnf(s82,plain,
( spl24_2
| spl24_32
| spl24_62
| spl24_92
| spl24_122 ),
inference(sat_conversion,[],[f1037]) ).
cnf(s83,plain,
( spl24_3
| spl24_33
| spl24_63
| spl24_93
| spl24_123 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s84,plain,
( spl24_4
| spl24_34
| spl24_64
| spl24_94
| spl24_124 ),
inference(sat_conversion,[],[f1039]) ).
cnf(s85,plain,
( spl24_5
| spl24_35
| spl24_65
| spl24_95
| spl24_125 ),
inference(sat_conversion,[],[f1040]) ).
cnf(s86,plain,
( ~ spl24_1
| ~ spl24_131 ),
inference(sat_conversion,[],[f1041]) ).
cnf(s88,plain,
( spl24_1
| ~ spl24_131 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s89,plain,
( ~ spl24_6
| ~ spl24_132 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s90,plain,
( spl24_31
| ~ spl24_132 ),
inference(sat_conversion,[],[f1045]) ).
cnf(s91,plain,
( spl24_2
| ~ spl24_132 ),
inference(sat_conversion,[],[f1046]) ).
cnf(s93,plain,
( spl24_61
| ~ spl24_133 ),
inference(sat_conversion,[],[f1048]) ).
cnf(s94,plain,
( spl24_3
| ~ spl24_133 ),
inference(sat_conversion,[],[f1049]) ).
cnf(s97,plain,
( spl24_4
| ~ spl24_134 ),
inference(sat_conversion,[],[f1052]) ).
cnf(s99,plain,
( spl24_121
| ~ spl24_135 ),
inference(sat_conversion,[],[f1054]) ).
cnf(s100,plain,
( spl24_5
| ~ spl24_135 ),
inference(sat_conversion,[],[f1055]) ).
cnf(s102,plain,
( spl24_2
| ~ spl24_136 ),
inference(sat_conversion,[],[f1057]) ).
cnf(s103,plain,
( spl24_31
| ~ spl24_136 ),
inference(sat_conversion,[],[f1058]) ).
cnf(s104,plain,
( ~ spl24_32
| ~ spl24_137 ),
inference(sat_conversion,[],[f1059]) ).
cnf(s106,plain,
( spl24_32
| ~ spl24_137 ),
inference(sat_conversion,[],[f1061]) ).
cnf(s108,plain,
( spl24_62
| ~ spl24_138 ),
inference(sat_conversion,[],[f1063]) ).
cnf(s109,plain,
( spl24_33
| ~ spl24_138 ),
inference(sat_conversion,[],[f1064]) ).
cnf(s111,plain,
( spl24_92
| ~ spl24_139 ),
inference(sat_conversion,[],[f1066]) ).
cnf(s114,plain,
( spl24_122
| ~ spl24_140 ),
inference(sat_conversion,[],[f1069]) ).
cnf(s115,plain,
( spl24_35
| ~ spl24_140 ),
inference(sat_conversion,[],[f1070]) ).
cnf(s117,plain,
( spl24_3
| ~ spl24_141 ),
inference(sat_conversion,[],[f1072]) ).
cnf(s118,plain,
( spl24_61
| ~ spl24_141 ),
inference(sat_conversion,[],[f1073]) ).
cnf(s119,plain,
( ~ spl24_58
| ~ spl24_142 ),
inference(sat_conversion,[],[f1074]) ).
cnf(s120,plain,
( spl24_33
| ~ spl24_142 ),
inference(sat_conversion,[],[f1075]) ).
cnf(s121,plain,
( spl24_62
| ~ spl24_142 ),
inference(sat_conversion,[],[f1076]) ).
cnf(s122,plain,
( ~ spl24_63
| ~ spl24_143 ),
inference(sat_conversion,[],[f1077]) ).
cnf(s124,plain,
( spl24_63
| ~ spl24_143 ),
inference(sat_conversion,[],[f1079]) ).
cnf(s126,plain,
( spl24_93
| ~ spl24_144 ),
inference(sat_conversion,[],[f1081]) ).
cnf(s128,plain,
( ~ spl24_73
| ~ spl24_145 ),
inference(sat_conversion,[],[f1083]) ).
cnf(s129,plain,
( spl24_123
| ~ spl24_145 ),
inference(sat_conversion,[],[f1084]) ).
cnf(s130,plain,
( spl24_65
| ~ spl24_145 ),
inference(sat_conversion,[],[f1085]) ).
cnf(s132,plain,
( spl24_4
| ~ spl24_146 ),
inference(sat_conversion,[],[f1087]) ).
cnf(s136,plain,
( spl24_92
| ~ spl24_147 ),
inference(sat_conversion,[],[f1091]) ).
cnf(s139,plain,
( spl24_93
| ~ spl24_148 ),
inference(sat_conversion,[],[f1094]) ).
cnf(s142,plain,
( spl24_94
| ~ spl24_149 ),
inference(sat_conversion,[],[f1097]) ).
cnf(s145,plain,
( spl24_95
| ~ spl24_150 ),
inference(sat_conversion,[],[f1100]) ).
cnf(s147,plain,
( spl24_5
| ~ spl24_151 ),
inference(sat_conversion,[],[f1102]) ).
cnf(s148,plain,
( spl24_121
| ~ spl24_151 ),
inference(sat_conversion,[],[f1103]) ).
cnf(s149,plain,
( ~ spl24_110
| ~ spl24_152 ),
inference(sat_conversion,[],[f1104]) ).
cnf(s151,plain,
( spl24_122
| ~ spl24_152 ),
inference(sat_conversion,[],[f1106]) ).
cnf(s153,plain,
( spl24_65
| ~ spl24_153 ),
inference(sat_conversion,[],[f1108]) ).
cnf(s154,plain,
( spl24_123
| ~ spl24_153 ),
inference(sat_conversion,[],[f1109]) ).
cnf(s156,plain,
( spl24_95
| ~ spl24_154 ),
inference(sat_conversion,[],[f1111]) ).
cnf(s158,plain,
spl24_90,
inference(sat_conversion,[],[f1113]) ).
cnf(s159,plain,
( ~ spl24_22
| ~ spl24_130 ),
inference(sat_conversion,[],[f1117]) ).
cnf(s160,plain,
( ~ spl24_23
| ~ spl24_130 ),
inference(sat_conversion,[],[f1121]) ).
cnf(s161,plain,
( ~ spl24_2
| ~ spl24_126 ),
inference(sat_conversion,[],[f1126]) ).
cnf(s162,plain,
( spl24_6
| ~ spl24_127 ),
inference(sat_conversion,[],[f1131]) ).
cnf(s167,plain,
( ~ spl24_102
| ~ spl24_130 ),
inference(sat_conversion,[],[f1167]) ).
cnf(s169,plain,
( ~ spl24_103
| ~ spl24_130 ),
inference(sat_conversion,[],[f1177]) ).
cnf(s170,plain,
( ~ spl24_25
| ~ spl24_130 ),
inference(sat_conversion,[],[f1179]) ).
cnf(s171,plain,
( ~ spl24_63
| ~ spl24_64 ),
inference(sat_conversion,[],[f1185]) ).
cnf(s174,plain,
( ~ spl24_105
| ~ spl24_130 ),
inference(sat_conversion,[],[f1215]) ).
cnf(s175,plain,
( ~ spl24_74
| ~ spl24_130 ),
inference(sat_conversion,[],[f1225]) ).
cnf(s176,plain,
( spl24_73
| ~ spl24_130 ),
inference(sat_conversion,[],[f1228]) ).
cnf(s179,plain,
( spl24_99
| ~ spl24_130 ),
inference(sat_conversion,[],[f1238]) ).
cnf(s180,plain,
( spl24_119
| ~ spl24_130 ),
inference(sat_conversion,[],[f1240]) ).
cnf(s181,plain,
( spl24_125
| ~ spl24_130 ),
inference(sat_conversion,[],[f1242]) ).
cnf(s185,plain,
( ~ spl24_90
| ~ spl24_128 ),
inference(sat_conversion,[],[f1266]) ).
cnf(s191,plain,
( ~ spl24_90
| ~ spl24_129 ),
inference(sat_conversion,[],[f1292]) ).
cnf(s194,plain,
( ~ spl24_6
| ~ spl24_7 ),
inference(sat_conversion,[],[f1302]) ).
cnf(s195,plain,
( ~ spl24_6
| ~ spl24_8 ),
inference(sat_conversion,[],[f1306]) ).
cnf(s196,plain,
( ~ spl24_33
| ~ spl24_35 ),
inference(sat_conversion,[],[f1312]) ).
cnf(s198,plain,
( ~ spl24_58
| ~ spl24_60 ),
inference(sat_conversion,[],[f1319]) ).
cnf(s199,plain,
( ~ spl24_59
| ~ spl24_60 ),
inference(sat_conversion,[],[f1321]) ).
cnf(s202,plain,
( spl24_38
| ~ spl24_127 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s204,plain,
( ~ spl24_35
| ~ spl24_127 ),
inference(sat_conversion,[],[f1342]) ).
cnf(s205,plain,
( spl24_32
| ~ spl24_127 ),
inference(sat_conversion,[],[f1344]) ).
cnf(s208,plain,
( ~ spl24_2
| ~ spl24_3 ),
inference(sat_conversion,[],[f1351]) ).
cnf(s210,plain,
( ~ spl24_2
| ~ spl24_5 ),
inference(sat_conversion,[],[f1358]) ).
cnf(s212,plain,
( ~ spl24_11
| ~ spl24_12 ),
inference(sat_conversion,[],[f1368]) ).
cnf(s213,plain,
( ~ spl24_37
| ~ spl24_38 ),
inference(sat_conversion,[],[f1372]) ).
cnf(s214,plain,
( ~ spl24_12
| ~ spl24_13 ),
inference(sat_conversion,[],[f1377]) ).
cnf(s217,plain,
( ~ spl24_62
| ~ spl24_64 ),
inference(sat_conversion,[],[f1390]) ).
cnf(s218,plain,
( ~ spl24_112
| ~ spl24_113 ),
inference(sat_conversion,[],[f1394]) ).
cnf(s219,plain,
( ~ spl24_87
| ~ spl24_90 ),
inference(sat_conversion,[],[f1398]) ).
cnf(s227,plain,
( ~ spl24_12
| ~ spl24_14 ),
inference(sat_conversion,[],[f1433]) ).
cnf(s229,plain,
( ~ spl24_12
| ~ spl24_15 ),
inference(sat_conversion,[],[f1444]) ).
cnf(s230,plain,
( ~ spl24_112
| ~ spl24_114 ),
inference(sat_conversion,[],[f1452]) ).
cnf(s231,plain,
( ~ spl24_123
| ~ spl24_124 ),
inference(sat_conversion,[],[f1454]) ).
cnf(s233,plain,
( ~ spl24_26
| ~ spl24_27 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s235,plain,
( ~ spl24_26
| ~ spl24_28 ),
inference(sat_conversion,[],[f1469]) ).
cnf(s241,plain,
( ~ spl24_31
| ~ spl24_32 ),
inference(sat_conversion,[],[f1502]) ).
cnf(s243,plain,
( ~ spl24_36
| ~ spl24_38 ),
inference(sat_conversion,[],[f1511]) ).
cnf(s247,plain,
( ~ spl24_13
| ~ spl24_15 ),
inference(sat_conversion,[],[f1529]) ).
cnf(s249,plain,
( ~ spl24_6
| ~ spl24_10 ),
inference(sat_conversion,[],[f1538]) ).
cnf(s251,plain,
( ~ spl24_17
| ~ spl24_18 ),
inference(sat_conversion,[],[f1549]) ).
cnf(s257,plain,
( ~ spl24_46
| ~ spl24_47 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s261,plain,
( ~ spl24_122
| ~ spl24_123 ),
inference(sat_conversion,[],[f1591]) ).
cnf(s262,plain,
( ~ spl24_72
| ~ spl24_73 ),
inference(sat_conversion,[],[f1595]) ).
cnf(s263,plain,
( ~ spl24_47
| ~ spl24_50 ),
inference(sat_conversion,[],[f1601]) ).
cnf(s265,plain,
( ~ spl24_14
| ~ spl24_15 ),
inference(sat_conversion,[],[f1613]) ).
cnf(s266,plain,
( ~ spl24_18
| ~ spl24_20 ),
inference(sat_conversion,[],[f1622]) ).
cnf(s267,plain,
( ~ spl24_18
| ~ spl24_20 ),
inference(sat_conversion,[],[f1624]) ).
cnf(s269,plain,
( ~ spl24_2
| ~ spl24_4 ),
inference(sat_conversion,[],[f1631]) ).
cnf(s271,plain,
( ~ spl24_22
| ~ spl24_25 ),
inference(sat_conversion,[],[f1644]) ).
cnf(s273,plain,
( ~ spl24_22
| ~ spl24_23 ),
inference(sat_conversion,[],[f1654]) ).
cnf(s274,plain,
( ~ spl24_13
| ~ spl24_14 ),
inference(sat_conversion,[],[f1658]) ).
cnf(s275,plain,
( ~ spl24_72
| ~ spl24_75 ),
inference(sat_conversion,[],[f1665]) ).
cnf(s279,plain,
( ~ spl24_51
| ~ spl24_55 ),
inference(sat_conversion,[],[f1685]) ).
cnf(s281,plain,
( ~ spl24_56
| ~ spl24_57 ),
inference(sat_conversion,[],[f1692]) ).
cnf(s283,plain,
( ~ spl24_57
| ~ spl24_58 ),
inference(sat_conversion,[],[f1700]) ).
cnf(s285,plain,
( ~ spl24_59
| ~ spl24_127 ),
inference(sat_conversion,[],[f1708]) ).
cnf(s286,plain,
( spl24_58
| ~ spl24_127 ),
inference(sat_conversion,[],[f1712]) ).
cnf(s287,plain,
( ~ spl24_17
| ~ spl24_20 ),
inference(sat_conversion,[],[f1714]) ).
cnf(s290,plain,
( ~ spl24_117
| ~ spl24_119 ),
inference(sat_conversion,[],[f1731]) ).
cnf(s291,plain,
( ~ spl24_32
| ~ spl24_33 ),
inference(sat_conversion,[],[f1740]) ).
cnf(s292,plain,
( ~ spl24_32
| ~ spl24_33 ),
inference(sat_conversion,[],[f1742]) ).
cnf(s294,plain,
( ~ spl24_64
| ~ spl24_65 ),
inference(sat_conversion,[],[f1750]) ).
cnf(s295,plain,
( ~ spl24_97
| ~ spl24_99 ),
inference(sat_conversion,[],[f1755]) ).
cnf(s297,plain,
( ~ spl24_66
| ~ spl24_67 ),
inference(sat_conversion,[],[f1766]) ).
cnf(s299,plain,
( ~ spl24_71
| ~ spl24_72 ),
inference(sat_conversion,[],[f1774]) ).
cnf(s300,plain,
( ~ spl24_61
| ~ spl24_64 ),
inference(sat_conversion,[],[f1781]) ).
cnf(s301,plain,
( ~ spl24_56
| ~ spl24_58 ),
inference(sat_conversion,[],[f1785]) ).
cnf(s302,plain,
( ~ spl24_67
| ~ spl24_70 ),
inference(sat_conversion,[],[f1793]) ).
cnf(s303,plain,
( ~ spl24_67
| ~ spl24_70 ),
inference(sat_conversion,[],[f1795]) ).
cnf(s305,plain,
( ~ spl24_98
| ~ spl24_99 ),
inference(sat_conversion,[],[f1808]) ).
cnf(s314,plain,
( ~ spl24_71
| ~ spl24_75 ),
inference(sat_conversion,[],[f1851]) ).
cnf(s315,plain,
( ~ spl24_78
| ~ spl24_80 ),
inference(sat_conversion,[],[f1863]) ).
cnf(s318,plain,
( ~ spl24_81
| ~ spl24_82 ),
inference(sat_conversion,[],[f1878]) ).
cnf(s322,plain,
( ~ spl24_91
| ~ spl24_93 ),
inference(sat_conversion,[],[f1893]) ).
cnf(s325,plain,
( ~ spl24_32
| ~ spl24_34 ),
inference(sat_conversion,[],[f1915]) ).
cnf(s328,plain,
( ~ spl24_52
| ~ spl24_54 ),
inference(sat_conversion,[],[f1940]) ).
cnf(s329,plain,
( ~ spl24_118
| ~ spl24_119 ),
inference(sat_conversion,[],[f1942]) ).
cnf(s330,plain,
( ~ spl24_77
| ~ spl24_78 ),
inference(sat_conversion,[],[f1947]) ).
cnf(s332,plain,
( ~ spl24_23
| ~ spl24_25 ),
inference(sat_conversion,[],[f1967]) ).
cnf(s335,plain,
( ~ spl24_38
| ~ spl24_39 ),
inference(sat_conversion,[],[f1978]) ).
cnf(s339,plain,
( ~ spl24_51
| ~ spl24_52 ),
inference(sat_conversion,[],[f1992]) ).
cnf(s340,plain,
( ~ spl24_52
| ~ spl24_55 ),
inference(sat_conversion,[],[f2003]) ).
cnf(s341,plain,
( ~ spl24_52
| ~ spl24_55 ),
inference(sat_conversion,[],[f2005]) ).
cnf(s344,plain,
( ~ spl24_91
| ~ spl24_95 ),
inference(sat_conversion,[],[f2032]) ).
cnf(s346,plain,
( ~ spl24_3
| ~ spl24_5 ),
inference(sat_conversion,[],[f2040]) ).
cnf(s348,plain,
( ~ spl24_119
| ~ spl24_120 ),
inference(sat_conversion,[],[f2067]) ).
cnf(s349,plain,
( ~ spl24_122
| ~ spl24_124 ),
inference(sat_conversion,[],[f2069]) ).
cnf(s353,plain,
( spl24_13
| ~ spl24_126 ),
inference(sat_conversion,[],[f2093]) ).
cnf(s358,plain,
( ~ spl24_5
| ~ spl24_126 ),
inference(sat_conversion,[],[f2105]) ).
cnf(s359,plain,
( ~ spl24_123
| ~ spl24_125 ),
inference(sat_conversion,[],[f2119]) ).
cnf(s360,plain,
( spl24_110
| ~ spl24_127 ),
inference(sat_conversion,[],[f2133]) ).
cnf(s364,plain,
( ~ spl24_91
| ~ spl24_92 ),
inference(sat_conversion,[],[f2155]) ).
cnf(s367,plain,
( ~ spl24_66
| ~ spl24_70 ),
inference(sat_conversion,[],[f2166]) ).
cnf(s377,plain,
( ~ spl24_51
| ~ spl24_54 ),
inference(sat_conversion,[],[f2217]) ).
cnf(s379,plain,
( ~ spl24_88
| ~ spl24_90 ),
inference(sat_conversion,[],[f2229]) ).
cnf(s380,plain,
( ~ spl24_67
| ~ spl24_69 ),
inference(sat_conversion,[],[f2243]) ).
cnf(s381,plain,
( ~ spl24_67
| ~ spl24_69 ),
inference(sat_conversion,[],[f2245]) ).
cnf(s382,plain,
( ~ spl24_74
| ~ spl24_75 ),
inference(sat_conversion,[],[f2249]) ).
cnf(s383,plain,
( ~ spl24_73
| ~ spl24_75 ),
inference(sat_conversion,[],[f2282]) ).
cnf(s385,plain,
( ~ spl24_42
| ~ spl24_45 ),
inference(sat_conversion,[],[f2329]) ).
cnf(s386,plain,
( ~ spl24_43
| ~ spl24_45 ),
inference(sat_conversion,[],[f2331]) ).
cnf(s387,plain,
( ~ spl24_89
| ~ spl24_90 ),
inference(sat_conversion,[],[f2333]) ).
cnf(s388,plain,
( ~ spl24_68
| ~ spl24_69 ),
inference(sat_conversion,[],[f2346]) ).
cnf(s390,plain,
( ~ spl24_36
| ~ spl24_37 ),
inference(sat_conversion,[],[f2363]) ).
cnf(s393,plain,
( ~ spl24_31
| ~ spl24_33 ),
inference(sat_conversion,[],[f2375]) ).
cnf(s395,plain,
( ~ spl24_7
| ~ spl24_10 ),
inference(sat_conversion,[],[f2392]) ).
cnf(s399,plain,
( ~ spl24_36
| ~ spl24_40 ),
inference(sat_conversion,[],[f2423]) ).
cnf(s402,plain,
( ~ spl24_56
| ~ spl24_59 ),
inference(sat_conversion,[],[f2444]) ).
cnf(s403,plain,
( ~ spl24_61
| ~ spl24_62 ),
inference(sat_conversion,[],[f2450]) ).
cnf(s405,plain,
( ~ spl24_56
| ~ spl24_60 ),
inference(sat_conversion,[],[f2464]) ).
cnf(s407,plain,
( ~ spl24_53
| ~ spl24_55 ),
inference(sat_conversion,[],[f2472]) ).
cnf(s409,plain,
( ~ spl24_62
| ~ spl24_65 ),
inference(sat_conversion,[],[f2481]) ).
cnf(s410,plain,
( ~ spl24_39
| ~ spl24_40 ),
inference(sat_conversion,[],[f2491]) ).
cnf(s411,plain,
( ~ spl24_33
| ~ spl24_34 ),
inference(sat_conversion,[],[f2496]) ).
cnf(s412,plain,
( ~ spl24_33
| ~ spl24_34 ),
inference(sat_conversion,[],[f2498]) ).
cnf(s415,plain,
( ~ spl24_68
| ~ spl24_70 ),
inference(sat_conversion,[],[f2518]) ).
cnf(s416,plain,
( ~ spl24_71
| ~ spl24_74 ),
inference(sat_conversion,[],[f2520]) ).
cnf(s417,plain,
( ~ spl24_69
| ~ spl24_70 ),
inference(sat_conversion,[],[f2528]) ).
cnf(s419,plain,
( ~ spl24_41
| ~ spl24_43 ),
inference(sat_conversion,[],[f2541]) ).
cnf(s420,plain,
( ~ spl24_83
| ~ spl24_85 ),
inference(sat_conversion,[],[f2555]) ).
cnf(s422,plain,
( ~ spl24_124
| ~ spl24_125 ),
inference(sat_conversion,[],[f2568]) ).
cnf(s424,plain,
( ~ spl24_122
| ~ spl24_125 ),
inference(sat_conversion,[],[f2578]) ).
cnf(s425,plain,
( ~ spl24_37
| ~ spl24_39 ),
inference(sat_conversion,[],[f2596]) ).
cnf(s428,plain,
( ~ spl24_1
| ~ spl24_4 ),
inference(sat_conversion,[],[f2614]) ).
cnf(s429,plain,
( ~ spl24_11
| ~ spl24_13 ),
inference(sat_conversion,[],[f2622]) ).
cnf(s431,plain,
( ~ spl24_4
| ~ spl24_126 ),
inference(sat_conversion,[],[f2626]) ).
cnf(s433,plain,
( ~ spl24_61
| ~ spl24_63 ),
inference(sat_conversion,[],[f2638]) ).
cnf(s435,plain,
( ~ spl24_3
| ~ spl24_126 ),
inference(sat_conversion,[],[f2642]) ).
cnf(s436,plain,
( ~ spl24_62
| ~ spl24_63 ),
inference(sat_conversion,[],[f2661]) ).
cnf(s441,plain,
( ~ spl24_36
| ~ spl24_39 ),
inference(sat_conversion,[],[f2690]) ).
cnf(s443,plain,
( ~ spl24_53
| ~ spl24_54 ),
inference(sat_conversion,[],[f2705]) ).
cnf(s446,plain,
( ~ spl24_114
| ~ spl24_130 ),
inference(sat_conversion,[],[f2765]) ).
cnf(s447,plain,
( spl24_113
| ~ spl24_130 ),
inference(sat_conversion,[],[f2767]) ).
cnf(s449,plain,
( ~ spl24_3
| ~ spl24_4 ),
inference(sat_conversion,[],[f2777]) ).
cnf(s452,plain,
( ~ spl24_71
| ~ spl24_73 ),
inference(sat_conversion,[],[f2801]) ).
cnf(s453,plain,
( ~ spl24_54
| ~ spl24_55 ),
inference(sat_conversion,[],[f2812]) ).
cnf(s455,plain,
( ~ spl24_4
| ~ spl24_5 ),
inference(sat_conversion,[],[f2877]) ).
cnf(s456,plain,
( ~ spl24_72
| ~ spl24_74 ),
inference(sat_conversion,[],[f2920]) ).
cnf(s459,plain,
( ~ spl24_91
| ~ spl24_94 ),
inference(sat_conversion,[],[f2959]) ).
cnf(s461,plain,
( ~ spl24_66
| ~ spl24_69 ),
inference(sat_conversion,[],[f2978]) ).
cnf(s464,plain,
( ~ spl24_31
| ~ spl24_34 ),
inference(sat_conversion,[],[f3048]) ).
cnf(s466,plain,
( ~ spl24_1
| ~ spl24_5 ),
inference(sat_conversion,[],[f3106]) ).
cnf(s468,plain,
( ~ spl24_106
| ~ spl24_107 ),
inference(sat_conversion,[],[f3143]) ).
cnf(s472,plain,
( ~ spl24_111
| ~ spl24_112 ),
inference(sat_conversion,[],[f3160]) ).
cnf(s473,plain,
( ~ spl24_86
| ~ spl24_90 ),
inference(sat_conversion,[],[f3166]) ).
cnf(s476,plain,
( ~ spl24_111
| ~ spl24_114 ),
inference(sat_conversion,[],[f3223]) ).
cnf(s477,plain,
( ~ spl24_111
| ~ spl24_114 ),
inference(sat_conversion,[],[f3225]) ).
cnf(s481,plain,
( ~ spl24_121
| ~ spl24_123 ),
inference(sat_conversion,[],[f3242]) ).
cnf(s483,plain,
( ~ spl24_61
| ~ spl24_65 ),
inference(sat_conversion,[],[f3286]) ).
cnf(s484,plain,
( ~ spl24_63
| ~ spl24_65 ),
inference(sat_conversion,[],[f3335]) ).
cnf(s485,plain,
( ~ spl24_107
| ~ spl24_110 ),
inference(sat_conversion,[],[f3337]) ).
cnf(s486,plain,
( ~ spl24_28
| ~ spl24_30 ),
inference(sat_conversion,[],[f3375]) ).
cnf(s487,plain,
( ~ spl24_81
| ~ spl24_83 ),
inference(sat_conversion,[],[f3377]) ).
cnf(s488,plain,
( ~ spl24_27
| ~ spl24_30 ),
inference(sat_conversion,[],[f3392]) ).
cnf(s490,plain,
~ spl24_86,
inference(rat,[],[s473,s158]) ).
cnf(s491,plain,
~ spl24_89,
inference(rat,[],[s387,s158]) ).
cnf(s492,plain,
~ spl24_88,
inference(rat,[],[s379,s158]) ).
cnf(s493,plain,
~ spl24_87,
inference(rat,[],[s219,s158]) ).
cnf(s494,plain,
~ spl24_129,
inference(rat,[],[s191,s158]) ).
cnf(s495,plain,
~ spl24_128,
inference(rat,[],[s185,s158]) ).
cnf(s496,plain,
~ spl24_94,
inference(rat,[],[s459,s77]) ).
cnf(s497,plain,
~ spl24_92,
inference(rat,[],[s364,s77]) ).
cnf(s498,plain,
~ spl24_95,
inference(rat,[],[s344,s77]) ).
cnf(s499,plain,
~ spl24_93,
inference(rat,[],[s322,s77]) ).
cnf(s500,plain,
~ spl24_149,
inference(rat,[],[s142,s496]) ).
cnf(s501,plain,
~ spl24_147,
inference(rat,[],[s136,s497]) ).
cnf(s502,plain,
~ spl24_139,
inference(rat,[],[s111,s497]) ).
cnf(s503,plain,
~ spl24_154,
inference(rat,[],[s156,s498]) ).
cnf(s504,plain,
~ spl24_150,
inference(rat,[],[s145,s498]) ).
cnf(s505,plain,
~ spl24_148,
inference(rat,[],[s139,s499]) ).
cnf(s506,plain,
~ spl24_144,
inference(rat,[],[s126,s499]) ).
cnf(s507,plain,
( spl24_20
| spl24_45
| spl24_70
| spl24_120 ),
inference(rat,[],[s65,s498]) ).
cnf(s510,plain,
( spl24_78
| spl24_83
| spl24_98 ),
inference(rat,[],[s62,s499,s492]) ).
cnf(s511,plain,
( spl24_18
| spl24_43
| spl24_68
| spl24_118 ),
inference(rat,[],[s61,s499]) ).
cnf(s512,plain,
( spl24_77
| spl24_82
| spl24_97 ),
inference(rat,[],[s60,s497,s493]) ).
cnf(s513,plain,
( spl24_17
| spl24_42
| spl24_67
| spl24_117 ),
inference(rat,[],[s59,s497]) ).
cnf(s514,plain,
( spl24_14
| spl24_39
| spl24_64
| spl24_114 ),
inference(rat,[],[s53,s491]) ).
cnf(s516,plain,
( spl24_12
| spl24_37
| spl24_62
| spl24_112 ),
inference(rat,[],[s49,s493]) ).
cnf(s517,plain,
( spl24_11
| spl24_36
| spl24_61
| spl24_111 ),
inference(rat,[],[s47,s490]) ).
cnf(s518,plain,
( spl24_126
| spl24_127
| spl24_130 ),
inference(rat,[],[s26,s494,s495]) ).
cnf(s521,plain,
( ~ spl24_62
| ~ spl24_125
| spl24_4
| spl24_3 ),
inference(rat,[],[s411,s84,s83,s217,s436,s422,s359,s496,s499]) ).
cnf(s522,plain,
( ~ spl24_125
| spl24_4
| spl24_3
| spl24_2 ),
inference(rat,[],[s171,s83,s84,s292,s325,s82,s521,s359,s422,s424,s499,s496,s497]) ).
cnf(s523,plain,
( ~ spl24_62
| spl24_33
| spl24_34
| spl24_4
| spl24_3 ),
inference(rat,[],[s231,s84,s83,s217,s436,s496,s499]) ).
cnf(s524,plain,
( spl24_63
| spl24_140
| spl24_137
| spl24_33
| spl24_34
| spl24_142
| spl24_152
| spl24_4
| spl24_3
| spl24_2
| spl24_131 ),
inference(rat,[],[s80,s130,s153,s294,s84,s99,s148,s231,s481,s83,s124,s102,s91,s117,s94,s132,s97,s522,s109,s502,s506,s501,s505,s500,s504,s503,s496,s499]) ).
cnf(s525,plain,
( spl24_121
| spl24_145
| spl24_153
| spl24_143
| spl24_138
| spl24_140
| spl24_137
| spl24_142
| spl24_152
| spl24_125
| spl24_134
| spl24_146
| spl24_3
| spl24_2
| spl24_131 ),
inference(rat,[],[s80,s99,s148,s102,s91,s117,s94,s502,s506,s501,s505,s500,s504,s503]) ).
cnf(s526,plain,
( ~ spl24_71
| spl24_54
| spl24_52
| spl24_64
| spl24_62
| spl24_57
| spl24_59 ),
inference(rat,[],[s380,s50,s54,s299,s416]) ).
cnf(s527,plain,
( spl24_54
| spl24_52
| spl24_51
| spl24_64
| spl24_61
| spl24_62
| spl24_57
| spl24_56
| spl24_59 ),
inference(rat,[],[s456,s50,s54,s297,s461,s48,s526]) ).
cnf(s528,plain,
( ~ spl24_71
| spl24_55
| spl24_52
| spl24_65
| spl24_62
| spl24_60
| spl24_57 ),
inference(rat,[],[s302,s50,s56,s299,s314]) ).
cnf(s529,plain,
( spl24_52
| spl24_51
| spl24_64
| spl24_61
| spl24_65
| spl24_62
| spl24_60
| spl24_57
| spl24_56
| spl24_59 ),
inference(rat,[],[s275,s50,s56,s297,s367,s48,s528,s453,s527]) ).
cnf(s530,plain,
( ~ spl24_71
| ~ spl24_52
| spl24_64
| spl24_65
| spl24_60
| spl24_59 ),
inference(rat,[],[s417,s56,s54,s314,s416,s341,s328]) ).
cnf(s531,plain,
( spl24_51
| spl24_59
| spl24_64
| spl24_61
| spl24_65
| spl24_62
| spl24_60
| spl24_57
| spl24_56 ),
inference(rat,[],[s382,s56,s54,s367,s461,s48,s530,s328,s341,s529]) ).
cnf(s532,plain,
( ~ spl24_75
| spl24_52
| spl24_54
| spl24_64
| spl24_62
| spl24_57
| spl24_59 ),
inference(rat,[],[s380,s50,s54,s275,s382]) ).
cnf(s533,plain,
( spl24_59
| spl24_56
| spl24_64
| spl24_61
| spl24_65
| spl24_62
| spl24_60
| spl24_57 ),
inference(rat,[],[s456,s50,s54,s303,s417,s56,s532,s279,s339,s377,s531]) ).
cnf(s534,plain,
( spl24_4
| spl24_3
| spl24_2
| spl24_1 ),
inference(rat,[],[s533,s171,s433,s484,s524,s523,s115,s104,s292,s325,s119,s198,s283,s301,s149,s204,s205,s285,s286,s360,s518,s181,s522,s358,s1,s88]) ).
cnf(s535,plain,
( ~ spl24_63
| ~ spl24_127
| spl24_64 ),
inference(rat,[],[s533,s433,s436,s484,s285,s301,s283,s198,s286]) ).
cnf(s536,plain,
( ~ spl24_17
| spl24_15
| spl24_13
| ~ spl24_6
| spl24_5
| spl24_3 ),
inference(rat,[],[s332,s32,s36,s251,s287,s249,s195]) ).
cnf(s537,plain,
( spl24_12
| ~ spl24_127
| spl24_64
| spl24_5
| spl24_3
| spl24_2 ),
inference(rat,[],[s266,s36,s32,s271,s273,s30,s536,s265,s429,s514,s517,s230,s472,s516,s335,s243,s213,s202,s249,s195,s194,s162,s483,s409,s85,s359,s83,s535,s292,s205,s204,s498,s499]) ).
cnf(s538,plain,
( ~ spl24_127
| spl24_64
| spl24_5
| spl24_3
| spl24_2 ),
inference(rat,[],[s476,s517,s514,s212,s227,s537,s483,s85,s359,s83,s535,s243,s335,s292,s202,s204,s205,s498,s499]) ).
cnf(s540,plain,
( ~ spl24_51
| spl24_59
| spl24_57
| spl24_62
| spl24_72
| spl24_74
| spl24_64 ),
inference(rat,[],[s380,s50,s54,s339,s377]) ).
cnf(s541,plain,
( ~ spl24_66
| spl24_59
| spl24_57
| spl24_62
| spl24_72
| spl24_74
| spl24_64 ),
inference(rat,[],[s328,s50,s54,s297,s461]) ).
cnf(s542,plain,
( ~ spl24_67
| spl24_60
| spl24_59
| spl24_65
| spl24_75
| spl24_74
| spl24_64 ),
inference(rat,[],[s453,s56,s54,s303,s381]) ).
cnf(s543,plain,
( spl24_59
| spl24_57
| ~ spl24_63
| spl24_72
| spl24_75
| spl24_71
| spl24_74
| spl24_64 ),
inference(rat,[],[s417,s54,s56,s328,s341,s50,s542,s405,s48,s541,s540,s484,s436,s433]) ).
cnf(s544,plain,
( ~ spl24_51
| spl24_60
| spl24_57
| ~ spl24_63
| ~ spl24_73 ),
inference(rat,[],[s302,s56,s50,s279,s339,s383,s262,s484,s436]) ).
cnf(s545,plain,
( spl24_57
| ~ spl24_63
| spl24_74
| ~ spl24_73
| spl24_64 ),
inference(rat,[],[s340,s50,s56,s297,s367,s48,s544,s199,s402,s543,s452,s383,s262,s484,s436,s433]) ).
cnf(s546,plain,
( ~ spl24_6
| ~ spl24_14
| spl24_22
| spl24_5
| spl24_3
| spl24_2 ),
inference(rat,[],[s30,s536,s194,s274,s265,s227]) ).
cnf(s547,plain,
( ~ spl24_81
| ~ spl24_99 ),
inference(rat,[],[s330,s512,s510,s318,s487,s305,s295]) ).
cnf(s548,plain,
( ~ spl24_63
| spl24_81
| spl24_106
| spl24_122
| spl24_112
| spl24_22
| spl24_23
| spl24_25
| spl24_74
| ~ spl24_73
| spl24_114
| spl24_64
| spl24_5
| spl24_3
| spl24_2 ),
inference(rat,[],[s266,s32,s36,s214,s229,s516,s425,s514,s546,s195,s249,s37,s281,s545,s241,s82,s436,s497]) ).
cnf(s549,plain,
( ~ spl24_17
| ~ spl24_6
| ~ spl24_130
| spl24_5
| spl24_3 ),
inference(rat,[],[s247,s32,s36,s251,s287,s170,s160,s249,s195]) ).
cnf(s550,plain,
( ~ spl24_6
| ~ spl24_130
| spl24_5
| spl24_3
| spl24_2 ),
inference(rat,[],[s266,s32,s36,s214,s229,s30,s549,s194,s195,s249,s170,s160,s159]) ).
cnf(s553,plain,
( ~ spl24_43
| spl24_12
| spl24_70
| spl24_52
| spl24_60
| spl24_35
| spl24_31
| spl24_46
| spl24_50
| spl24_110
| spl24_98
| spl24_120
| spl24_22
| spl24_102
| spl24_2 ),
inference(rat,[],[s399,s38,s46,s233,s488,s29,s330,s510,s420,s45,s395,s30,s287,s507,s386,s419]) ).
cnf(s554,plain,
( ~ spl24_18
| spl24_70
| spl24_67
| spl24_117
| spl24_120 ),
inference(rat,[],[s385,s513,s507,s251,s267]) ).
cnf(s555,plain,
( ~ spl24_69
| spl24_52
| spl24_67
| spl24_60
| spl24_65
| spl24_35
| spl24_31
| spl24_46
| spl24_50
| spl24_110
| spl24_75
| spl24_98
| spl24_117
| spl24_118
| spl24_120
| spl24_22
| spl24_102
| spl24_103
| spl24_114
| spl24_64
| spl24_3
| spl24_2 ),
inference(rat,[],[s330,s29,s31,s233,s235,s38,s441,s514,s227,s553,s419,s511,s554,s407,s56,s388,s417]) ).
cnf(s556,plain,
( ~ spl24_26
| spl24_53
| spl24_52
| ~ spl24_130
| spl24_3
| spl24_2 ),
inference(rat,[],[s330,s29,s31,s233,s235,s169,s167]) ).
cnf(s557,plain,
( ~ spl24_30
| spl24_53
| spl24_52
| ~ spl24_130
| spl24_3
| spl24_2 ),
inference(rat,[],[s330,s31,s29,s486,s488,s169,s167]) ).
cnf(s558,plain,
( ~ spl24_43
| spl24_30
| spl24_26
| spl24_35
| spl24_31
| spl24_46
| spl24_50 ),
inference(rat,[],[s399,s46,s38,s386,s419]) ).
cnf(s559,plain,
( spl24_52
| ~ spl24_130
| spl24_64
| spl24_5
| spl24_3
| spl24_2 ),
inference(rat,[],[s410,s46,s514,s385,s227,s513,s30,s251,s511,s558,s395,s45,s420,s510,s315,s35,s557,s556,s415,s56,s443,s453,s54,s555,s174,s169,s348,s329,s305,s485,s263,s257,s69,s262,s295,s196,s542,s405,s402,s37,s550,s393,s409,s82,s292,s83,s548,s547,s179,s468,s70,s290,s180,s167,s218,s447,s159,s160,s170,s446,s359,s424,s181,s383,s176,s175,s497,s499]) ).
cnf(s560,plain,
( spl24_64
| spl24_126
| spl24_5
| spl24_3
| spl24_2 ),
inference(rat,[],[s417,s54,s56,s328,s341,s559,s402,s405,s37,s550,s409,s82,s292,s393,s83,s548,s547,s468,s70,s383,s290,s359,s424,s218,s159,s160,s167,s170,s175,s176,s179,s180,s181,s446,s447,s518,s538,s497,s499]) ).
cnf(s561,plain,
( ~ spl24_127
| spl24_63
| spl24_65
| spl24_5
| spl24_3 ),
inference(rat,[],[s359,s83,s85,s292,s204,s205,s499,s498]) ).
cnf(s562,plain,
( spl24_126
| spl24_5
| spl24_2
| spl24_3 ),
inference(rat,[],[s291,s83,s82,s359,s424,s181,s518,s561,s171,s217,s294,s560,s497,s499]) ).
cnf(s563,plain,
( spl24_3
| spl24_2
| spl24_1 ),
inference(rat,[],[s562,s431,s455,s534]) ).
cnf(s564,plain,
( ~ spl24_127
| spl24_64
| spl24_5
| spl24_4
| spl24_132
| spl24_136
| spl24_131 ),
inference(rat,[],[s80,s93,s118,s483,s129,s154,s85,s231,s422,s109,s84,s124,s115,s104,s292,s325,s119,s149,s535,s204,s205,s286,s360,s132,s97,s147,s100,s502,s506,s501,s505,s500,s504,s503,s498,s496]) ).
cnf(s565,plain,
( spl24_64
| spl24_5
| spl24_126
| spl24_4
| spl24_2
| spl24_131 ),
inference(rat,[],[s78,s93,s118,s124,s403,s436,s82,s106,s109,s120,s325,s412,s154,s84,s114,s151,s128,s359,s422,s424,s176,s181,s518,s564,s102,s91,s132,s97,s147,s100,s502,s506,s501,s505,s500,s504,s503,s497,s496]) ).
cnf(s566,plain,
( ~ spl24_127
| spl24_143
| spl24_138
| spl24_142
| spl24_133
| spl24_141
| spl24_65
| spl24_134
| spl24_146
| spl24_5
| spl24_132
| spl24_136
| spl24_131 ),
inference(rat,[],[s78,s85,s115,s104,s149,s204,s205,s360,s147,s100,s153,s130,s502,s506,s501,s505,s500,s504,s503,s498]) ).
cnf(s567,plain,
( spl24_2
| spl24_1 ),
inference(rat,[],[s104,s78,s82,s114,s151,s424,s181,s518,s566,s124,s108,s121,s130,s153,s93,s118,s171,s217,s294,s300,s565,s100,s147,s97,s132,s346,s435,s449,s563,s91,s102,s88,s502,s506,s501,s505,s500,s504,s503,s497]) ).
cnf(s568,plain,
( ~ spl24_127
| spl24_64
| spl24_1 ),
inference(rat,[],[s564,s103,s89,s241,s162,s205,s88,s269,s210,s567]) ).
cnf(s569,plain,
( spl24_64
| spl24_1 ),
inference(rat,[],[s78,s122,s106,s83,s90,s103,s325,s412,s464,s108,s121,s154,s84,s114,s151,s128,s521,s359,s422,s424,s176,s181,s518,s568,s88,s161,s132,s97,s269,s147,s100,s210,s117,s94,s208,s567,s502,s506,s501,s505,s500,s504,s503,s499,s496]) ).
cnf(s570,plain,
spl24_1,
inference(rat,[],[s78,s106,s90,s103,s292,s393,s83,s114,s151,s359,s424,s181,s518,s561,s124,s108,s121,s130,s153,s171,s217,s294,s569,s94,s117,s100,s147,s97,s132,s161,s208,s210,s269,s567,s88,s502,s506,s501,s505,s500,s504,s503,s499]) ).
cnf(s571,plain,
~ spl24_5,
inference(rat,[],[s466,s570]) ).
cnf(s572,plain,
~ spl24_4,
inference(rat,[],[s428,s570]) ).
cnf(s573,plain,
~ spl24_131,
inference(rat,[],[s86,s570]) ).
cnf(s574,plain,
~ spl24_151,
inference(rat,[],[s147,s571]) ).
cnf(s575,plain,
~ spl24_135,
inference(rat,[],[s100,s571]) ).
cnf(s576,plain,
~ spl24_146,
inference(rat,[],[s132,s572]) ).
cnf(s577,plain,
~ spl24_134,
inference(rat,[],[s97,s572]) ).
cnf(s581,plain,
( ~ spl24_36
| spl24_62
| ~ spl24_13
| spl24_64 ),
inference(rat,[],[s230,s516,s514,s390,s441,s274,s214]) ).
cnf(s583,plain,
( ~ spl24_63
| ~ spl24_13
| spl24_64 ),
inference(rat,[],[s425,s516,s514,s472,s477,s517,s581,s433,s436,s429,s274,s214]) ).
cnf(s584,plain,
( ~ spl24_32
| ~ spl24_126
| spl24_64 ),
inference(rat,[],[s231,s83,s84,s292,s325,s435,s583,s353,s499,s496,s572]) ).
cnf(s585,plain,
( ~ spl24_122
| ~ spl24_126
| spl24_64 ),
inference(rat,[],[s411,s83,s84,s261,s349,s435,s583,s353,s499,s496,s572]) ).
cnf(s586,plain,
( spl24_2
| spl24_64 ),
inference(rat,[],[s80,s109,s120,s196,s85,s130,s153,s409,s82,s114,s151,s585,s106,s584,s124,s583,s522,s94,s117,s353,s435,s565,s91,s102,s576,s573,s577,s502,s506,s501,s505,s500,s504,s574,s575,s503,s571,s498,s497,s572]) ).
cnf(s587,plain,
( ~ spl24_127
| spl24_64 ),
inference(rat,[],[s564,s103,s89,s241,s162,s205,s571,s572,s573]) ).
cnf(s588,plain,
spl24_64,
inference(rat,[],[s78,s122,s106,s83,s90,s103,s325,s412,s464,s108,s121,s154,s84,s114,s151,s128,s521,s359,s422,s424,s176,s181,s518,s587,s94,s117,s161,s208,s586,s573,s575,s502,s506,s576,s501,s505,s500,s504,s574,s577,s503,s499,s496,s572]) ).
cnf(s589,plain,
~ spl24_61,
inference(rat,[],[s300,s588]) ).
cnf(s590,plain,
~ spl24_65,
inference(rat,[],[s294,s588]) ).
cnf(s591,plain,
~ spl24_62,
inference(rat,[],[s217,s588]) ).
cnf(s592,plain,
~ spl24_63,
inference(rat,[],[s171,s588]) ).
cnf(s593,plain,
~ spl24_141,
inference(rat,[],[s118,s589]) ).
cnf(s594,plain,
~ spl24_133,
inference(rat,[],[s93,s589]) ).
cnf(s595,plain,
~ spl24_153,
inference(rat,[],[s153,s590]) ).
cnf(s596,plain,
~ spl24_145,
inference(rat,[],[s130,s590]) ).
cnf(s597,plain,
~ spl24_142,
inference(rat,[],[s121,s591]) ).
cnf(s598,plain,
~ spl24_138,
inference(rat,[],[s108,s591]) ).
cnf(s599,plain,
~ spl24_143,
inference(rat,[],[s124,s592]) ).
cnf(s600,plain,
( ~ spl24_125
| spl24_2 ),
inference(rat,[],[s104,s78,s82,s114,s151,s424,s102,s91,s599,s573,s575,s596,s595,s502,s593,s597,s506,s598,s576,s501,s505,s500,s504,s574,s577,s594,s503,s591,s497]) ).
cnf(s601,plain,
spl24_2,
inference(rat,[],[s104,s525,s82,s114,s151,s261,s481,s83,s435,s196,s518,s85,s181,s600,s566,s91,s102,s576,s599,s596,s595,s598,s597,s577,s573,s591,s497,s592,s499,s571,s498,s590,s594,s593]) ).
cnf(s602,plain,
~ spl24_3,
inference(rat,[],[s208,s601]) ).
cnf(s603,plain,
~ spl24_126,
inference(rat,[],[s161,s601]) ).
cnf(s604,plain,
~ spl24_127,
inference(rat,[],[s561,s592,s571,s590,s602]) ).
cnf(s605,plain,
spl24_130,
inference(rat,[],[s518,s604,s603]) ).
cnf(s608,plain,
spl24_125,
inference(rat,[],[s181,s605]) ).
cnf(s623,plain,
~ spl24_122,
inference(rat,[],[s424,s608]) ).
cnf(s625,plain,
~ spl24_123,
inference(rat,[],[s359,s608]) ).
cnf(s638,plain,
~ spl24_152,
inference(rat,[],[s151,s623]) ).
cnf(s639,plain,
~ spl24_140,
inference(rat,[],[s114,s623]) ).
cnf(s640,plain,
spl24_33,
inference(rat,[],[s83,s602,s499,s592,s625]) ).
cnf(s645,plain,
~ spl24_31,
inference(rat,[],[s393,s640]) ).
cnf(s646,plain,
~ spl24_32,
inference(rat,[],[s292,s640]) ).
cnf(s651,plain,
~ spl24_136,
inference(rat,[],[s103,s645]) ).
cnf(s652,plain,
~ spl24_132,
inference(rat,[],[s90,s645]) ).
cnf(s653,plain,
~ spl24_137,
inference(rat,[],[s106,s646]) ).
cnf(s654,plain,
$false,
inference(rat,[],[s78,s503,s594,s577,s574,s504,s500,s505,s501,s576,s598,s506,s638,s597,s593,s639,s502,s595,s596,s608,s575,s573,s651,s599,s652,s653]) ).
fof(f3395,plain,
$false,
inference(avatar_sat_refutation,[],[s654]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG063+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n004.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 19:22:37 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.00/1.31 % (670093)Detected formulas, will run a generic FOF schedule.
% 4.00/1.31 % (670100)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=1135268099:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.00/1.31 % (670103)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1831255068:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.00/1.31 % (670102)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2284692633:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.00/1.31 % (670101)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4028574145:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.00/1.31 % (670098)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=4018850372:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.00/1.31 % (670099)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=3001098449:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.00/1.31 % (670101)Refutation not found, incomplete strategy
% 4.00/1.31 % (670101)------------------------------
% 4.00/1.31 % (670101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.00/1.31 % (670101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/1.31 % (670101)CaDiCaL version: 2.1.3
% 4.00/1.31 % (670101)Termination reason: Refutation not found, incomplete strategy
% 4.00/1.31 % (670101)Time elapsed: 0.011 s
% 4.00/1.31 % (670101)Peak memory usage: 88 MB
% 4.00/1.31 % (670101)Instructions burned: 22 (million)
% 4.00/1.31 % (670104)dis-21_1_sil=8000:lcm=predicate:random_seed=3709073295: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)
% 4.00/1.31 % (670104)Refutation not found, incomplete strategy
% 4.00/1.31 % (670104)------------------------------
% 4.00/1.31 % (670104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.00/1.31 % (670104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/1.31 % (670104)CaDiCaL version: 2.1.3
% 4.00/1.31 % (670104)Termination reason: Refutation not found, incomplete strategy
% 4.00/1.31 % (670104)Time elapsed: 0.011 s
% 4.00/1.31 % (670104)Peak memory usage: 89 MB
% 4.00/1.31 % (670104)Instructions burned: 21 (million)
% 4.00/1.31 % (670102)Instruction limit reached!
% 4.00/1.31 % (670102)------------------------------
% 4.00/1.31 % (670102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.00/1.31 % (670102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/1.31 % (670102)CaDiCaL version: 2.1.3
% 4.00/1.31 % (670102)Termination reason: Instruction limit
% 4.00/1.31 % (670102)Termination phase: Saturation
% 4.00/1.31 % (670102)Time elapsed: 0.054 s
% 4.00/1.31 % (670102)Peak memory usage: 88 MB
% 4.00/1.31 % (670102)Instructions burned: 121 (million)
% 4.00/1.31 % (670103)Instruction limit reached!
% 4.00/1.31 % (670103)------------------------------
% 4.00/1.31 % (670103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.00/1.31 % (670103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/1.31 % (670103)CaDiCaL version: 2.1.3
% 4.00/1.31 % (670103)Termination reason: Instruction limit
% 4.00/1.31 % (670103)Termination phase: Saturation
% 4.00/1.31 % (670103)Time elapsed: 0.075 s
% 4.00/1.31 % (670103)Peak memory usage: 89 MB
% 4.00/1.31 % (670103)Instructions burned: 139 (million)
% 4.00/1.31 % (670112)lrs+10_1_sil=8000:sp=occurrence:random_seed=1992971692:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 4.00/1.31 [W928 19:22:38.091894663 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.091958354 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.091983344 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.091989420 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.092010448 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.092016606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 % (670113)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1254695591:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.00/1.31 % (670112)First to succeed.
% 4.00/1.31 % (670112)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-670093"
% 4.00/1.31 % (670101)------------------------------
% 4.00/1.31 % (670101)------------------------------
% 4.00/1.31 % (670104)------------------------------
% 4.00/1.31 % (670104)------------------------------
% 4.00/1.31 % (670113)Also succeeded, but the first one will report.
% 4.00/1.31 [W928 19:22:38.293644047 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.293680387 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.293716261 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.293727621 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.293753204 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.293765968 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.293849745 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.293876442 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.293926002 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.293937702 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.293967363 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 [W928 19:22:38.293977899 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.00/1.31 % (670116)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3634982429:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 4.00/1.31 % (670117)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1845584675:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 4.00/1.31 % (670116)Also succeeded, but the first one will report.
% 4.00/1.31 % (670112)Refutation found. Thanks to Tanya!
% 4.00/1.31 % SZS status Theorem for theBenchmark
% 4.00/1.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/1.51 % (670112)------------------------------
% 0.20/1.51 % (670112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/1.51 % (670112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/1.51 % (670112)CaDiCaL version: 2.1.3
% 0.20/1.51 % (670112)Termination reason: Refutation
% 0.20/1.51 % (670112)Time elapsed: 0.070 s
% 0.20/1.51 % (670112)Peak memory usage: 90 MB
% 0.20/1.51 % (670112)Instructions burned: 130 (million)
% 0.20/1.51 % (670112)------------------------------
% 0.20/1.51 % (670112)------------------------------
% 0.20/1.51 % (670093)Success in time 0.645 s
% 0.20/1.51 % Vampire exiting
%------------------------------------------------------------------------------