%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG068+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n013.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:29 AM UTC 2026
% Result : Theorem 2.56s 0.98s
% Output : Refutation 4.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 147
% Syntax : Number of formulae : 812 ( 152 unt; 140 def)
% Number of atoms : 2888 (1459 equ)
% Maximal formula atoms : 250 ( 3 avg)
% Number of connectives : 3384 (1308 ~;1419 |; 541 &)
% ( 116 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 142 ( 140 usr; 141 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e4 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e4 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3
| op(e0,e2) = e4 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3
| op(e0,e3) = e4 )
& ( op(e0,e4) = e0
| op(e0,e4) = e1
| op(e0,e4) = e2
| op(e0,e4) = e3
| op(e0,e4) = e4 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3
| op(e1,e0) = e4 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3
| op(e1,e1) = e4 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3
| op(e1,e2) = e4 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3
| op(e1,e3) = e4 )
& ( op(e1,e4) = e0
| op(e1,e4) = e1
| op(e1,e4) = e2
| op(e1,e4) = e3
| op(e1,e4) = e4 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3
| op(e2,e0) = e4 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3
| op(e2,e1) = e4 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3
| op(e2,e2) = e4 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3
| op(e2,e3) = e4 )
& ( op(e2,e4) = e0
| op(e2,e4) = e1
| op(e2,e4) = e2
| op(e2,e4) = e3
| op(e2,e4) = e4 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3
| op(e3,e0) = e4 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3
| op(e3,e1) = e4 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3
| op(e3,e2) = e4 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3
| op(e3,e3) = e4 )
& ( op(e3,e4) = e0
| op(e3,e4) = e1
| op(e3,e4) = e2
| op(e3,e4) = e3
| op(e3,e4) = e4 )
& ( op(e4,e0) = e0
| op(e4,e0) = e1
| op(e4,e0) = e2
| op(e4,e0) = e3
| op(e4,e0) = e4 )
& ( op(e4,e1) = e0
| op(e4,e1) = e1
| op(e4,e1) = e2
| op(e4,e1) = e3
| op(e4,e1) = e4 )
& ( op(e4,e2) = e0
| op(e4,e2) = e1
| op(e4,e2) = e2
| op(e4,e2) = e3
| op(e4,e2) = e4 )
& ( op(e4,e3) = e0
| op(e4,e3) = e1
| op(e4,e3) = e2
| op(e4,e3) = e3
| op(e4,e3) = e4 )
& ( op(e4,e4) = e0
| op(e4,e4) = e1
| op(e4,e4) = e2
| op(e4,e4) = e3
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& op(unit,e4) = e4
& op(e4,unit) = e4
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3
| unit = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0
| op(e0,e4) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0
| op(e4,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| op(e0,e4) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e4,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| op(e0,e4) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2
| op(e4,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3
| op(e0,e4) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3
| op(e4,e0) = e3 )
& ( op(e0,e0) = e4
| op(e0,e1) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e4) = e4 )
& ( op(e0,e0) = e4
| op(e1,e0) = e4
| op(e2,e0) = e4
| op(e3,e0) = e4
| op(e4,e0) = e4 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0
| op(e1,e4) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0
| op(e4,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1
| op(e1,e4) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1
| op(e4,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2
| op(e1,e4) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| op(e4,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3
| op(e1,e4) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3
| op(e4,e1) = e3 )
& ( op(e1,e0) = e4
| op(e1,e1) = e4
| op(e1,e2) = e4
| op(e1,e3) = e4
| op(e1,e4) = e4 )
& ( op(e0,e1) = e4
| op(e1,e1) = e4
| op(e2,e1) = e4
| op(e3,e1) = e4
| op(e4,e1) = e4 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0
| op(e2,e4) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0
| op(e4,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1
| op(e2,e4) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1
| op(e4,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2
| op(e2,e4) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2
| op(e4,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| op(e2,e4) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3
| op(e4,e2) = e3 )
& ( op(e2,e0) = e4
| op(e2,e1) = e4
| op(e2,e2) = e4
| op(e2,e3) = e4
| op(e2,e4) = e4 )
& ( op(e0,e2) = e4
| op(e1,e2) = e4
| op(e2,e2) = e4
| op(e3,e2) = e4
| op(e4,e2) = e4 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0
| op(e3,e4) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0
| op(e4,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1
| op(e3,e4) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1
| op(e4,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| op(e3,e4) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2
| op(e4,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3
| op(e3,e4) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3
| op(e4,e3) = e3 )
& ( op(e3,e0) = e4
| op(e3,e1) = e4
| op(e3,e2) = e4
| op(e3,e3) = e4
| op(e3,e4) = e4 )
& ( op(e0,e3) = e4
| op(e1,e3) = e4
| op(e2,e3) = e4
| op(e3,e3) = e4
| op(e4,e3) = e4 )
& ( op(e4,e0) = e0
| op(e4,e1) = e0
| op(e4,e2) = e0
| op(e4,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e4) = e0
| op(e1,e4) = e0
| op(e2,e4) = e0
| op(e3,e4) = e0
| op(e4,e4) = e0 )
& ( op(e4,e0) = e1
| op(e4,e1) = e1
| op(e4,e2) = e1
| op(e4,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e4) = e1
| op(e1,e4) = e1
| op(e2,e4) = e1
| op(e3,e4) = e1
| op(e4,e4) = e1 )
& ( op(e4,e0) = e2
| op(e4,e1) = e2
| op(e4,e2) = e2
| op(e4,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e4) = e2
| op(e1,e4) = e2
| op(e2,e4) = e2
| op(e3,e4) = e2
| op(e4,e4) = e2 )
& ( op(e4,e0) = e3
| op(e4,e1) = e3
| op(e4,e2) = e3
| op(e4,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e4) = e3
| op(e1,e4) = e3
| op(e2,e4) = e3
| op(e3,e4) = e3
| op(e4,e4) = e3 )
& ( op(e4,e0) = e4
| op(e4,e1) = e4
| op(e4,e2) = e4
| op(e4,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e4) = e4
| op(e1,e4) = e4
| op(e2,e4) = e4
| op(e3,e4) = e4
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e4,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e4,e0)
& op(e2,e0) != op(e3,e0)
& op(e2,e0) != op(e4,e0)
& op(e3,e0) != op(e4,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e4,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e4,e1)
& op(e2,e1) != op(e3,e1)
& op(e2,e1) != op(e4,e1)
& op(e3,e1) != op(e4,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e4,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e4,e2)
& op(e2,e2) != op(e3,e2)
& op(e2,e2) != op(e4,e2)
& op(e3,e2) != op(e4,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e4,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e4,e3)
& op(e2,e3) != op(e3,e3)
& op(e2,e3) != op(e4,e3)
& op(e3,e3) != op(e4,e3)
& op(e0,e4) != op(e1,e4)
& op(e0,e4) != op(e2,e4)
& op(e0,e4) != op(e3,e4)
& op(e0,e4) != op(e4,e4)
& op(e1,e4) != op(e2,e4)
& op(e1,e4) != op(e3,e4)
& op(e1,e4) != op(e4,e4)
& op(e2,e4) != op(e3,e4)
& op(e2,e4) != op(e4,e4)
& op(e3,e4) != op(e4,e4)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e4)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e4)
& op(e0,e2) != op(e0,e3)
& op(e0,e2) != op(e0,e4)
& op(e0,e3) != op(e0,e4)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e4)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e4)
& op(e1,e2) != op(e1,e3)
& op(e1,e2) != op(e1,e4)
& op(e1,e3) != op(e1,e4)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e4)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e4)
& op(e2,e2) != op(e2,e3)
& op(e2,e2) != op(e2,e4)
& op(e2,e3) != op(e2,e4)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e4)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e4)
& op(e3,e2) != op(e3,e3)
& op(e3,e2) != op(e3,e4)
& op(e3,e3) != op(e3,e4)
& op(e4,e0) != op(e4,e1)
& op(e4,e0) != op(e4,e2)
& op(e4,e0) != op(e4,e3)
& op(e4,e0) != op(e4,e4)
& op(e4,e1) != op(e4,e2)
& op(e4,e1) != op(e4,e3)
& op(e4,e1) != op(e4,e4)
& op(e4,e2) != op(e4,e3)
& op(e4,e2) != op(e4,e4)
& op(e4,e3) != op(e4,e4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e0 != e4
& e1 != e2
& e1 != e3
& e1 != e4
& e2 != e3
& e2 != e4
& e3 != e4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( e0 = op(op(e4,e2),op(e4,e2))
& e1 = op(e4,e2)
& e3 = op(e2,e4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,conjecture,
~ ( ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e0,e0) != e4
| op(e0,e4) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e1,e1) != e4
| op(e1,e4) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e2,e4) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( op(e3,e3) != e4
| op(e3,e4) = e3 )
& ( op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e4,e4) != e1
| op(e4,e1) = e4 )
& ( op(e4,e4) != e2
| op(e4,e2) = e4 )
& ( op(e4,e4) != e3
| op(e4,e3) = e4 )
& ( op(e4,e4) != e4
| op(e4,e4) = e4 )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f8,negated_conjecture,
~ ~ ( ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e0,e0) != e4
| op(e0,e4) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e1,e1) != e4
| op(e1,e4) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e2,e4) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( op(e3,e3) != e4
| op(e3,e4) = e3 )
& ( op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e4,e4) != e1
| op(e4,e1) = e4 )
& ( op(e4,e4) != e2
| op(e4,e2) = e4 )
& ( op(e4,e4) != e3
| op(e4,e3) = e4 )
& ( op(e4,e4) != e4
| op(e4,e4) = e4 )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 ) ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f9,plain,
( ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e0,e0) != e4
| op(e0,e4) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e1,e1) != e4
| op(e1,e4) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e2,e4) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( op(e3,e3) != e4
| op(e3,e4) = e3 )
& ( op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e4,e4) != e1
| op(e4,e1) = e4 )
& ( op(e4,e4) != e2
| op(e4,e2) = e4 )
& ( op(e4,e4) != e3
| op(e4,e3) = e4 )
& ( op(e4,e4) != e4
| op(e4,e4) = e4 )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 ) ) ),
inference(flattening,[],[f8]) ).
fof(f10,definition,
( ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11,definition,
( ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f12,definition,
( ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f13,definition,
( ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f17,definition,
( ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f18,definition,
( ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f19,definition,
( ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f20,definition,
( ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f21,definition,
( ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f22,definition,
( ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f25,definition,
( ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f26,definition,
( ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f27,definition,
( ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f29,definition,
( ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f30,definition,
( ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f31,definition,
( ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f32,definition,
( ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f33,definition,
( ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ~ sP23 ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f34,plain,
( ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e0,e0) != e4
| op(e0,e4) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e1,e1) != e4
| op(e1,e4) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e2,e4) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( op(e3,e3) != e4
| op(e3,e4) = e3 )
& ( op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e4,e4) != e1
| op(e4,e1) = e4 )
& ( op(e4,e4) != e2
| op(e4,e2) = e4 )
& ( op(e4,e4) != e3
| op(e4,e3) = e4 )
& ( op(e4,e4) != e4
| op(e4,e4) = e4 )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ) ),
inference(definition_folding,[],[f9,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(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ~ sP23 ),
inference(nnf_transformation,[],[f33]) ).
fof(f36,plain,
( ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ~ sP22 ),
inference(nnf_transformation,[],[f32]) ).
fof(f37,plain,
( ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ~ sP21 ),
inference(nnf_transformation,[],[f31]) ).
fof(f38,plain,
( ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ~ sP20 ),
inference(nnf_transformation,[],[f30]) ).
fof(f39,plain,
( ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ~ sP19 ),
inference(nnf_transformation,[],[f29]) ).
fof(f40,plain,
( ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ~ sP18 ),
inference(nnf_transformation,[],[f28]) ).
fof(f41,plain,
( ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ~ sP17 ),
inference(nnf_transformation,[],[f27]) ).
fof(f42,plain,
( ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ~ sP16 ),
inference(nnf_transformation,[],[f26]) ).
fof(f43,plain,
( ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ~ sP15 ),
inference(nnf_transformation,[],[f25]) ).
fof(f44,plain,
( ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ~ sP14 ),
inference(nnf_transformation,[],[f24]) ).
fof(f45,plain,
( ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ~ sP13 ),
inference(nnf_transformation,[],[f23]) ).
fof(f46,plain,
( ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ~ sP12 ),
inference(nnf_transformation,[],[f22]) ).
fof(f47,plain,
( ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ~ sP11 ),
inference(nnf_transformation,[],[f21]) ).
fof(f48,plain,
( ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ~ sP10 ),
inference(nnf_transformation,[],[f20]) ).
fof(f49,plain,
( ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ~ sP9 ),
inference(nnf_transformation,[],[f19]) ).
fof(f50,plain,
( ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ~ sP8 ),
inference(nnf_transformation,[],[f18]) ).
fof(f51,plain,
( ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ~ sP7 ),
inference(nnf_transformation,[],[f17]) ).
fof(f52,plain,
( ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ~ sP6 ),
inference(nnf_transformation,[],[f16]) ).
fof(f53,plain,
( ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ~ sP5 ),
inference(nnf_transformation,[],[f15]) ).
fof(f54,plain,
( ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ~ sP4 ),
inference(nnf_transformation,[],[f14]) ).
fof(f55,plain,
( ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ~ sP3 ),
inference(nnf_transformation,[],[f13]) ).
fof(f56,plain,
( ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ~ sP2 ),
inference(nnf_transformation,[],[f12]) ).
fof(f57,plain,
( ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ~ sP1 ),
inference(nnf_transformation,[],[f11]) ).
fof(f58,plain,
( ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 )
| ~ sP0 ),
inference(nnf_transformation,[],[f10]) ).
fof(f59,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(f84,plain,
( e0 = unit
| e1 = unit
| e2 = unit
| e3 = unit
| e4 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f85,plain,
e4 = op(e4,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f86,plain,
e4 = op(unit,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f87,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f88,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f90,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f92,plain,
e1 = op(unit,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
e0 = op(unit,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f98,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(f99,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(f100,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(f101,plain,
( e1 = op(e0,e4)
| e1 = op(e1,e4)
| e1 = op(e2,e4)
| e1 = op(e3,e4)
| e1 = op(e4,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f105,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(f109,plain,
( e2 = op(e0,e3)
| e2 = op(e1,e3)
| e2 = op(e2,e3)
| e2 = op(e3,e3)
| e2 = op(e4,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f110,plain,
( e2 = op(e3,e0)
| e2 = op(e3,e1)
| e2 = op(e3,e2)
| e2 = op(e3,e3)
| e2 = op(e3,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f115,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(f116,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(f117,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(f122,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(f139,plain,
( op(e0,e0) = e2
| e2 = op(e1,e0)
| e2 = op(e2,e0)
| e2 = op(e3,e0)
| e2 = op(e4,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f145,plain,
op(e4,e3) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f149,plain,
op(e4,e1) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f152,plain,
op(e4,e0) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f177,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f181,plain,
op(e1,e0) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f184,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f187,plain,
op(e0,e2) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f193,plain,
op(e0,e0) != op(e0,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f196,plain,
op(e2,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f216,plain,
op(e2,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f233,plain,
op(e0,e1) != op(e2,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f240,plain,
op(e1,e0) != op(e2,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f245,plain,
e3 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f246,plain,
e2 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f247,plain,
e2 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f248,plain,
e1 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f249,plain,
e1 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f250,plain,
e1 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f255,plain,
e3 = op(e2,e4),
inference(cnf_transformation,[],[f6]) ).
fof(f256,plain,
e1 = op(e4,e2),
inference(cnf_transformation,[],[f6]) ).
fof(f257,plain,
e0 = op(op(e4,e2),op(e4,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f260,plain,
( op(e0,e1) != op(e1,e0)
| ~ sP23 ),
inference(cnf_transformation,[],[f35]) ).
fof(f263,plain,
( op(e0,e2) != op(e2,e0)
| ~ sP22 ),
inference(cnf_transformation,[],[f36]) ).
fof(f266,plain,
( op(e0,e3) != op(e3,e0)
| ~ sP21 ),
inference(cnf_transformation,[],[f37]) ).
fof(f269,plain,
( op(e0,e4) != op(e4,e0)
| ~ sP20 ),
inference(cnf_transformation,[],[f38]) ).
fof(f270,plain,
( e0 != op(op(e1,e0),e1)
| ~ sP19 ),
inference(cnf_transformation,[],[f39]) ).
fof(f275,plain,
( op(e1,e1) != op(e1,e1)
| ~ sP18 ),
inference(cnf_transformation,[],[f40]) ).
fof(f276,plain,
( e2 != op(op(e1,e2),e1)
| ~ sP17 ),
inference(cnf_transformation,[],[f41]) ).
fof(f280,plain,
( e1 = op(op(e1,e3),e3)
| ~ sP16 ),
inference(cnf_transformation,[],[f42]) ).
fof(f282,plain,
( e4 != op(op(e1,e4),e1)
| ~ sP15 ),
inference(cnf_transformation,[],[f43]) ).
fof(f287,plain,
( op(e0,e2) != op(e2,e0)
| ~ sP14 ),
inference(cnf_transformation,[],[f44]) ).
fof(f288,plain,
( e1 != op(op(e2,e1),e2)
| ~ sP13 ),
inference(cnf_transformation,[],[f45]) ).
fof(f293,plain,
( op(e2,e2) != op(e2,e2)
| ~ sP12 ),
inference(cnf_transformation,[],[f46]) ).
fof(f295,plain,
( e2 = op(op(e2,e3),e3)
| ~ sP11 ),
inference(cnf_transformation,[],[f47]) ).
fof(f298,plain,
( e2 = op(op(e2,e4),e4)
| ~ sP10 ),
inference(cnf_transformation,[],[f48]) ).
fof(f302,plain,
( op(e0,e3) != op(e3,e0)
| ~ sP9 ),
inference(cnf_transformation,[],[f49]) ).
fof(f304,plain,
( e3 = op(op(e3,e1),e1)
| ~ sP8 ),
inference(cnf_transformation,[],[f50]) ).
fof(f307,plain,
( e3 = op(op(e3,e2),e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f51]) ).
fof(f311,plain,
( op(e3,e3) != op(e3,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f52]) ).
fof(f312,plain,
( e4 != op(op(e3,e4),e3)
| ~ sP5 ),
inference(cnf_transformation,[],[f53]) ).
fof(f317,plain,
( op(e0,e4) != op(e4,e0)
| ~ sP4 ),
inference(cnf_transformation,[],[f54]) ).
fof(f319,plain,
( e4 = op(op(e4,e1),e1)
| ~ sP3 ),
inference(cnf_transformation,[],[f55]) ).
fof(f321,plain,
( e2 != op(op(e4,e2),e4)
| ~ sP2 ),
inference(cnf_transformation,[],[f56]) ).
fof(f325,plain,
( e4 = op(op(e4,e3),e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f57]) ).
fof(f329,plain,
( op(e4,e4) != op(e4,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f58]) ).
fof(f332,plain,
( op(e0,e0) != op(e0,e0)
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f34]) ).
fof(f335,plain,
( e2 != op(e4,e4)
| e4 = op(e4,e2) ),
inference(cnf_transformation,[],[f34]) ).
fof(f336,plain,
( e1 != op(e4,e4)
| e4 = op(e4,e1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f337,plain,
( e0 != op(e4,e4)
| e4 = op(e4,e0) ),
inference(cnf_transformation,[],[f34]) ).
fof(f338,plain,
( e4 != op(e3,e3)
| e3 = op(e3,e4) ),
inference(cnf_transformation,[],[f34]) ).
fof(f340,plain,
( e2 != op(e3,e3)
| e3 = op(e3,e2) ),
inference(cnf_transformation,[],[f34]) ).
fof(f343,plain,
( e4 != op(e2,e2)
| e2 = op(e2,e4) ),
inference(cnf_transformation,[],[f34]) ).
fof(f344,plain,
( e3 != op(e2,e2)
| e2 = op(e2,e3) ),
inference(cnf_transformation,[],[f34]) ).
fof(f352,plain,
( e0 != op(e1,e1)
| e1 = op(e1,e0) ),
inference(cnf_transformation,[],[f34]) ).
fof(f355,plain,
( op(e0,e0) != e2
| e0 = op(e0,e2) ),
inference(cnf_transformation,[],[f34]) ).
fof(f358,plain,
( sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(trivial_inequality_removal,[],[f332]) ).
fof(f359,plain,
~ sP0,
inference(trivial_inequality_removal,[],[f329]) ).
fof(f360,plain,
~ sP6,
inference(trivial_inequality_removal,[],[f311]) ).
fof(f361,plain,
~ sP12,
inference(trivial_inequality_removal,[],[f293]) ).
fof(f362,plain,
~ sP18,
inference(trivial_inequality_removal,[],[f275]) ).
fof(f364,definition,
( spl24_1
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl24_1])],[avatar_definition]) ).
fof(f368,definition,
( spl24_2
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl24_2])],[avatar_definition]) ).
fof(f372,definition,
( spl24_3
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl24_3])],[avatar_definition]) ).
fof(f376,definition,
( spl24_4
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl24_4])],[avatar_definition]) ).
fof(f380,definition,
( spl24_5
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl24_5])],[avatar_definition]) ).
fof(f384,definition,
( spl24_6
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl24_6])],[avatar_definition]) ).
fof(f388,definition,
( spl24_7
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl24_7])],[avatar_definition]) ).
fof(f392,definition,
( spl24_8
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl24_8])],[avatar_definition]) ).
fof(f396,definition,
( spl24_9
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl24_9])],[avatar_definition]) ).
fof(f400,definition,
( spl24_10
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl24_10])],[avatar_definition]) ).
fof(f404,definition,
( spl24_11
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl24_11])],[avatar_definition]) ).
fof(f408,definition,
( spl24_12
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl24_12])],[avatar_definition]) ).
fof(f412,definition,
( spl24_13
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl24_13])],[avatar_definition]) ).
fof(f416,definition,
( spl24_14
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl24_14])],[avatar_definition]) ).
fof(f420,definition,
( spl24_15
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl24_15])],[avatar_definition]) ).
fof(f424,definition,
( spl24_16
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl24_16])],[avatar_definition]) ).
fof(f428,definition,
( spl24_17
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl24_17])],[avatar_definition]) ).
fof(f432,definition,
( spl24_18
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl24_18])],[avatar_definition]) ).
fof(f436,definition,
( spl24_19
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl24_19])],[avatar_definition]) ).
fof(f440,definition,
( spl24_20
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl24_20])],[avatar_definition]) ).
fof(f444,definition,
( spl24_21
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl24_21])],[avatar_definition]) ).
fof(f448,definition,
( spl24_22
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl24_22])],[avatar_definition]) ).
fof(f452,definition,
( spl24_23
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl24_23])],[avatar_definition]) ).
fof(f456,definition,
( spl24_24
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl24_24])],[avatar_definition]) ).
fof(f465,plain,
( spl24_1
| spl24_2
| spl24_3
| spl24_4
| spl24_5
| spl24_6
| spl24_7
| spl24_8
| spl24_9
| spl24_10
| spl24_11
| spl24_12
| spl24_13
| spl24_14
| spl24_15
| spl24_16
| spl24_17
| spl24_18
| spl24_19
| spl24_20
| spl24_21
| spl24_22
| spl24_23
| spl24_24 ),
inference(avatar_split_clause,[],[f358,f456,f452,f448,f444,f440,f436,f432,f428,f424,f420,f416,f412,f408,f404,f400,f396,f392,f388,f384,f380,f376,f372,f368,f364]) ).
fof(f467,definition,
( spl24_26
<=> e4 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl24_26])],[avatar_definition]) ).
fof(f469,plain,
( e4 = op(e4,e3)
| ~ spl24_26 ),
inference(avatar_component_clause,[],[f467]) ).
fof(f471,definition,
( spl24_27
<=> e3 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl24_27])],[avatar_definition]) ).
fof(f472,plain,
( e3 = op(e4,e4)
| ~ spl24_27 ),
inference(avatar_component_clause,[],[f471]) ).
fof(f476,definition,
( spl24_28
<=> e4 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl24_28])],[avatar_definition]) ).
fof(f477,plain,
( e4 != op(e4,e2)
| spl24_28 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f478,plain,
( e4 = op(e4,e2)
| ~ spl24_28 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f480,definition,
( spl24_29
<=> e2 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl24_29])],[avatar_definition]) ).
fof(f483,plain,
( spl24_28
| ~ spl24_29 ),
inference(avatar_split_clause,[],[f335,f480,f476]) ).
fof(f485,definition,
( spl24_30
<=> e4 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl24_30])],[avatar_definition]) ).
fof(f487,plain,
( e4 = op(e4,e1)
| ~ spl24_30 ),
inference(avatar_component_clause,[],[f485]) ).
fof(f489,definition,
( spl24_31
<=> e1 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl24_31])],[avatar_definition]) ).
fof(f492,plain,
( spl24_30
| ~ spl24_31 ),
inference(avatar_split_clause,[],[f336,f489,f485]) ).
fof(f494,definition,
( spl24_32
<=> e4 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl24_32])],[avatar_definition]) ).
fof(f496,plain,
( e4 = op(e4,e0)
| ~ spl24_32 ),
inference(avatar_component_clause,[],[f494]) ).
fof(f498,definition,
( spl24_33
<=> e0 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl24_33])],[avatar_definition]) ).
fof(f501,plain,
( spl24_32
| ~ spl24_33 ),
inference(avatar_split_clause,[],[f337,f498,f494]) ).
fof(f503,definition,
( spl24_34
<=> e3 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl24_34])],[avatar_definition]) ).
fof(f505,plain,
( e3 = op(e3,e4)
| ~ spl24_34 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f507,definition,
( spl24_35
<=> e4 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl24_35])],[avatar_definition]) ).
fof(f510,plain,
( spl24_34
| ~ spl24_35 ),
inference(avatar_split_clause,[],[f338,f507,f503]) ).
fof(f512,definition,
( spl24_36
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl24_36])],[avatar_definition]) ).
fof(f514,plain,
( e3 = op(e3,e2)
| ~ spl24_36 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f516,definition,
( spl24_37
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl24_37])],[avatar_definition]) ).
fof(f519,plain,
( spl24_36
| ~ spl24_37 ),
inference(avatar_split_clause,[],[f340,f516,f512]) ).
fof(f530,definition,
( spl24_40
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl24_40])],[avatar_definition]) ).
fof(f532,plain,
( e3 = op(e3,e0)
| ~ spl24_40 ),
inference(avatar_component_clause,[],[f530]) ).
fof(f539,definition,
( spl24_42
<=> e2 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl24_42])],[avatar_definition]) ).
fof(f541,plain,
( e2 = op(e2,e4)
| ~ spl24_42 ),
inference(avatar_component_clause,[],[f539]) ).
fof(f543,definition,
( spl24_43
<=> e4 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl24_43])],[avatar_definition]) ).
fof(f546,plain,
( spl24_42
| ~ spl24_43 ),
inference(avatar_split_clause,[],[f343,f543,f539]) ).
fof(f548,definition,
( spl24_44
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl24_44])],[avatar_definition]) ).
fof(f550,plain,
( e2 = op(e2,e3)
| ~ spl24_44 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f552,definition,
( spl24_45
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl24_45])],[avatar_definition]) ).
fof(f555,plain,
( spl24_44
| ~ spl24_45 ),
inference(avatar_split_clause,[],[f344,f552,f548]) ).
fof(f561,definition,
( spl24_47
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl24_47])],[avatar_definition]) ).
fof(f566,definition,
( spl24_48
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl24_48])],[avatar_definition]) ).
fof(f568,plain,
( e2 = op(e2,e0)
| ~ spl24_48 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f575,definition,
( spl24_50
<=> e1 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl24_50])],[avatar_definition]) ).
fof(f602,definition,
( spl24_56
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl24_56])],[avatar_definition]) ).
fof(f604,plain,
( e1 = op(e1,e0)
| ~ spl24_56 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f606,definition,
( spl24_57
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl24_57])],[avatar_definition]) ).
fof(f607,plain,
( e0 = op(e1,e1)
| ~ spl24_57 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f609,plain,
( spl24_56
| ~ spl24_57 ),
inference(avatar_split_clause,[],[f352,f606,f602]) ).
fof(f629,definition,
( spl24_62
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl24_62])],[avatar_definition]) ).
fof(f633,definition,
( spl24_63
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl24_63])],[avatar_definition]) ).
fof(f636,plain,
( spl24_62
| ~ spl24_63 ),
inference(avatar_split_clause,[],[f355,f633,f629]) ).
fof(f652,plain,
~ spl24_1,
inference(avatar_split_clause,[],[f359,f364]) ).
fof(f659,definition,
( spl24_68
<=> e4 = op(op(e4,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl24_68])],[avatar_definition]) ).
fof(f661,plain,
( e4 = op(op(e4,e3),e3)
| ~ spl24_68 ),
inference(avatar_component_clause,[],[f659]) ).
fof(f662,plain,
( ~ spl24_2
| spl24_68 ),
inference(avatar_split_clause,[],[f325,f659,f368]) ).
fof(f669,definition,
( spl24_70
<=> e2 = op(op(e4,e2),e4) ),
introduced(definition,[new_symbols(definition,[spl24_70])],[avatar_definition]) ).
fof(f671,plain,
( e2 != op(op(e4,e2),e4)
| spl24_70 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f672,plain,
( ~ spl24_3
| ~ spl24_70 ),
inference(avatar_split_clause,[],[f321,f669,f372]) ).
fof(f689,definition,
( spl24_74
<=> e4 = op(op(e4,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl24_74])],[avatar_definition]) ).
fof(f691,plain,
( e4 = op(op(e4,e1),e1)
| ~ spl24_74 ),
inference(avatar_component_clause,[],[f689]) ).
fof(f692,plain,
( ~ spl24_4
| spl24_74 ),
inference(avatar_split_clause,[],[f319,f689,f376]) ).
fof(f709,definition,
( spl24_78
<=> op(e0,e4) = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl24_78])],[avatar_definition]) ).
fof(f711,plain,
( op(e0,e4) != op(e4,e0)
| spl24_78 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f712,plain,
( ~ spl24_5
| ~ spl24_78 ),
inference(avatar_split_clause,[],[f317,f709,f380]) ).
fof(f714,definition,
( spl24_79
<=> e4 = op(op(e3,e4),e3) ),
introduced(definition,[new_symbols(definition,[spl24_79])],[avatar_definition]) ).
fof(f716,plain,
( e4 != op(op(e3,e4),e3)
| spl24_79 ),
inference(avatar_component_clause,[],[f714]) ).
fof(f717,plain,
( ~ spl24_6
| ~ spl24_79 ),
inference(avatar_split_clause,[],[f312,f714,f384]) ).
fof(f730,plain,
~ spl24_7,
inference(avatar_split_clause,[],[f360,f388]) ).
fof(f737,definition,
( spl24_83
<=> e3 = op(op(e3,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl24_83])],[avatar_definition]) ).
fof(f739,plain,
( e3 = op(op(e3,e2),e2)
| ~ spl24_83 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f740,plain,
( ~ spl24_8
| spl24_83 ),
inference(avatar_split_clause,[],[f307,f737,f392]) ).
fof(f752,definition,
( spl24_86
<=> e3 = op(op(e3,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl24_86])],[avatar_definition]) ).
fof(f754,plain,
( e3 = op(op(e3,e1),e1)
| ~ spl24_86 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f755,plain,
( ~ spl24_9
| spl24_86 ),
inference(avatar_split_clause,[],[f304,f752,f396]) ).
fof(f772,definition,
( spl24_90
<=> op(e0,e3) = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl24_90])],[avatar_definition]) ).
fof(f774,plain,
( op(e0,e3) != op(e3,e0)
| spl24_90 ),
inference(avatar_component_clause,[],[f772]) ).
fof(f775,plain,
( ~ spl24_10
| ~ spl24_90 ),
inference(avatar_split_clause,[],[f302,f772,f400]) ).
fof(f782,definition,
( spl24_92
<=> e2 = op(op(e2,e4),e4) ),
introduced(definition,[new_symbols(definition,[spl24_92])],[avatar_definition]) ).
fof(f784,plain,
( e2 = op(op(e2,e4),e4)
| ~ spl24_92 ),
inference(avatar_component_clause,[],[f782]) ).
fof(f785,plain,
( ~ spl24_11
| spl24_92 ),
inference(avatar_split_clause,[],[f298,f782,f404]) ).
fof(f793,definition,
( spl24_94
<=> e2 = op(op(e2,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl24_94])],[avatar_definition]) ).
fof(f795,plain,
( e2 = op(op(e2,e3),e3)
| ~ spl24_94 ),
inference(avatar_component_clause,[],[f793]) ).
fof(f796,plain,
( ~ spl24_12
| spl24_94 ),
inference(avatar_split_clause,[],[f295,f793,f408]) ).
fof(f804,plain,
~ spl24_13,
inference(avatar_split_clause,[],[f361,f412]) ).
fof(f806,definition,
( spl24_96
<=> e1 = op(op(e2,e1),e2) ),
introduced(definition,[new_symbols(definition,[spl24_96])],[avatar_definition]) ).
fof(f808,plain,
( e1 != op(op(e2,e1),e2)
| spl24_96 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f809,plain,
( ~ spl24_14
| ~ spl24_96 ),
inference(avatar_split_clause,[],[f288,f806,f416]) ).
fof(f831,definition,
( spl24_101
<=> op(e0,e2) = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl24_101])],[avatar_definition]) ).
fof(f833,plain,
( op(e0,e2) != op(e2,e0)
| spl24_101 ),
inference(avatar_component_clause,[],[f831]) ).
fof(f834,plain,
( ~ spl24_15
| ~ spl24_101 ),
inference(avatar_split_clause,[],[f287,f831,f420]) ).
fof(f836,definition,
( spl24_102
<=> e4 = op(op(e1,e4),e1) ),
introduced(definition,[new_symbols(definition,[spl24_102])],[avatar_definition]) ).
fof(f838,plain,
( e4 != op(op(e1,e4),e1)
| spl24_102 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f839,plain,
( ~ spl24_16
| ~ spl24_102 ),
inference(avatar_split_clause,[],[f282,f836,f424]) ).
fof(f852,definition,
( spl24_105
<=> e1 = op(op(e1,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl24_105])],[avatar_definition]) ).
fof(f854,plain,
( e1 = op(op(e1,e3),e3)
| ~ spl24_105 ),
inference(avatar_component_clause,[],[f852]) ).
fof(f855,plain,
( ~ spl24_17
| spl24_105 ),
inference(avatar_split_clause,[],[f280,f852,f428]) ).
fof(f858,definition,
( spl24_106
<=> e2 = op(op(e1,e2),e1) ),
introduced(definition,[new_symbols(definition,[spl24_106])],[avatar_definition]) ).
fof(f860,plain,
( e2 != op(op(e1,e2),e1)
| spl24_106 ),
inference(avatar_component_clause,[],[f858]) ).
fof(f861,plain,
( ~ spl24_18
| ~ spl24_106 ),
inference(avatar_split_clause,[],[f276,f858,f432]) ).
fof(f874,plain,
~ spl24_19,
inference(avatar_split_clause,[],[f362,f436]) ).
fof(f876,definition,
( spl24_109
<=> e0 = op(op(e1,e0),e1) ),
introduced(definition,[new_symbols(definition,[spl24_109])],[avatar_definition]) ).
fof(f878,plain,
( e0 != op(op(e1,e0),e1)
| spl24_109 ),
inference(avatar_component_clause,[],[f876]) ).
fof(f879,plain,
( ~ spl24_20
| ~ spl24_109 ),
inference(avatar_split_clause,[],[f270,f876,f440]) ).
fof(f886,definition,
( spl24_111
<=> op(e0,e1) = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl24_111])],[avatar_definition]) ).
fof(f888,plain,
( op(e0,e1) != op(e1,e0)
| spl24_111 ),
inference(avatar_component_clause,[],[f886]) ).
fof(f900,plain,
( ~ spl24_21
| ~ spl24_78 ),
inference(avatar_split_clause,[],[f269,f709,f444]) ).
fof(f911,plain,
( ~ spl24_22
| ~ spl24_90 ),
inference(avatar_split_clause,[],[f266,f772,f448]) ).
fof(f922,plain,
( ~ spl24_23
| ~ spl24_101 ),
inference(avatar_split_clause,[],[f263,f831,f452]) ).
fof(f933,plain,
( ~ spl24_24
| ~ spl24_111 ),
inference(avatar_split_clause,[],[f260,f886,f456]) ).
fof(f935,definition,
( spl24_120
<=> e4 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl24_120])],[avatar_definition]) ).
fof(f943,definition,
( spl24_122
<=> e4 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl24_122])],[avatar_definition]) ).
fof(f945,plain,
( e4 = op(e2,e4)
| ~ spl24_122 ),
inference(avatar_component_clause,[],[f943]) ).
fof(f951,definition,
( spl24_124
<=> e4 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl24_124])],[avatar_definition]) ).
fof(f953,plain,
( e4 = op(e0,e4)
| ~ spl24_124 ),
inference(avatar_component_clause,[],[f951]) ).
fof(f957,definition,
( spl24_125
<=> e3 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl24_125])],[avatar_definition]) ).
fof(f959,plain,
( e3 = op(e2,e4)
| ~ spl24_125 ),
inference(avatar_component_clause,[],[f957]) ).
fof(f970,definition,
( spl24_128
<=> e3 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl24_128])],[avatar_definition]) ).
fof(f972,plain,
( e3 = op(e4,e3)
| ~ spl24_128 ),
inference(avatar_component_clause,[],[f970]) ).
fof(f974,definition,
( spl24_129
<=> e3 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl24_129])],[avatar_definition]) ).
fof(f975,plain,
( e3 != op(e4,e2)
| spl24_129 ),
inference(avatar_component_clause,[],[f974]) ).
fof(f976,plain,
( e3 = op(e4,e2)
| ~ spl24_129 ),
inference(avatar_component_clause,[],[f974]) ).
fof(f978,definition,
( spl24_130
<=> e3 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl24_130])],[avatar_definition]) ).
fof(f980,plain,
( e3 = op(e4,e1)
| ~ spl24_130 ),
inference(avatar_component_clause,[],[f978]) ).
fof(f982,definition,
( spl24_131
<=> e3 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl24_131])],[avatar_definition]) ).
fof(f984,plain,
( e3 = op(e4,e0)
| ~ spl24_131 ),
inference(avatar_component_clause,[],[f982]) ).
fof(f985,plain,
( spl24_27
| spl24_128
| spl24_129
| spl24_130
| spl24_131 ),
inference(avatar_split_clause,[],[f98,f982,f978,f974,f970,f471]) ).
fof(f987,definition,
( spl24_132
<=> e2 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl24_132])],[avatar_definition]) ).
fof(f988,plain,
( e2 != op(e3,e4)
| spl24_132 ),
inference(avatar_component_clause,[],[f987]) ).
fof(f989,plain,
( e2 = op(e3,e4)
| ~ spl24_132 ),
inference(avatar_component_clause,[],[f987]) ).
fof(f991,definition,
( spl24_133
<=> e2 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl24_133])],[avatar_definition]) ).
fof(f993,plain,
( e2 = op(e1,e4)
| ~ spl24_133 ),
inference(avatar_component_clause,[],[f991]) ).
fof(f995,definition,
( spl24_134
<=> e2 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl24_134])],[avatar_definition]) ).
fof(f997,plain,
( e2 = op(e0,e4)
| ~ spl24_134 ),
inference(avatar_component_clause,[],[f995]) ).
fof(f998,plain,
( spl24_29
| spl24_132
| spl24_42
| spl24_133
| spl24_134 ),
inference(avatar_split_clause,[],[f99,f995,f991,f539,f987,f480]) ).
fof(f1000,definition,
( spl24_135
<=> e2 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl24_135])],[avatar_definition]) ).
fof(f1002,plain,
( e2 = op(e4,e3)
| ~ spl24_135 ),
inference(avatar_component_clause,[],[f1000]) ).
fof(f1004,definition,
( spl24_136
<=> e2 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl24_136])],[avatar_definition]) ).
fof(f1006,plain,
( e2 = op(e4,e2)
| ~ spl24_136 ),
inference(avatar_component_clause,[],[f1004]) ).
fof(f1008,definition,
( spl24_137
<=> e2 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl24_137])],[avatar_definition]) ).
fof(f1010,plain,
( e2 = op(e4,e1)
| ~ spl24_137 ),
inference(avatar_component_clause,[],[f1008]) ).
fof(f1012,definition,
( spl24_138
<=> e2 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl24_138])],[avatar_definition]) ).
fof(f1014,plain,
( e2 = op(e4,e0)
| ~ spl24_138 ),
inference(avatar_component_clause,[],[f1012]) ).
fof(f1015,plain,
( spl24_29
| spl24_135
| spl24_136
| spl24_137
| spl24_138 ),
inference(avatar_split_clause,[],[f100,f1012,f1008,f1004,f1000,f480]) ).
fof(f1017,definition,
( spl24_139
<=> e1 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl24_139])],[avatar_definition]) ).
fof(f1019,plain,
( e1 = op(e3,e4)
| ~ spl24_139 ),
inference(avatar_component_clause,[],[f1017]) ).
fof(f1021,definition,
( spl24_140
<=> e1 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl24_140])],[avatar_definition]) ).
fof(f1023,plain,
( e1 = op(e2,e4)
| ~ spl24_140 ),
inference(avatar_component_clause,[],[f1021]) ).
fof(f1025,definition,
( spl24_141
<=> e1 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl24_141])],[avatar_definition]) ).
fof(f1027,plain,
( e1 = op(e0,e4)
| ~ spl24_141 ),
inference(avatar_component_clause,[],[f1025]) ).
fof(f1028,plain,
( spl24_31
| spl24_139
| spl24_140
| spl24_50
| spl24_141 ),
inference(avatar_split_clause,[],[f101,f1025,f575,f1021,f1017,f489]) ).
fof(f1030,definition,
( spl24_142
<=> e1 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl24_142])],[avatar_definition]) ).
fof(f1031,plain,
( e1 != op(e4,e3)
| spl24_142 ),
inference(avatar_component_clause,[],[f1030]) ).
fof(f1032,plain,
( e1 = op(e4,e3)
| ~ spl24_142 ),
inference(avatar_component_clause,[],[f1030]) ).
fof(f1034,definition,
( spl24_143
<=> e1 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl24_143])],[avatar_definition]) ).
fof(f1036,plain,
( e1 = op(e4,e2)
| ~ spl24_143 ),
inference(avatar_component_clause,[],[f1034]) ).
fof(f1077,definition,
( spl24_153
<=> e4 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl24_153])],[avatar_definition]) ).
fof(f1079,plain,
( e4 = op(e2,e3)
| ~ spl24_153 ),
inference(avatar_component_clause,[],[f1077]) ).
fof(f1081,definition,
( spl24_154
<=> e4 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl24_154])],[avatar_definition]) ).
fof(f1083,plain,
( e4 = op(e1,e3)
| ~ spl24_154 ),
inference(avatar_component_clause,[],[f1081]) ).
fof(f1085,definition,
( spl24_155
<=> e4 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl24_155])],[avatar_definition]) ).
fof(f1087,plain,
( e4 = op(e0,e3)
| ~ spl24_155 ),
inference(avatar_component_clause,[],[f1085]) ).
fof(f1088,plain,
( spl24_26
| spl24_35
| spl24_153
| spl24_154
| spl24_155 ),
inference(avatar_split_clause,[],[f105,f1085,f1081,f1077,f507,f467]) ).
fof(f1090,definition,
( spl24_156
<=> e4 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl24_156])],[avatar_definition]) ).
fof(f1092,plain,
( e4 = op(e3,e2)
| ~ spl24_156 ),
inference(avatar_component_clause,[],[f1090]) ).
fof(f1094,definition,
( spl24_157
<=> e4 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl24_157])],[avatar_definition]) ).
fof(f1095,plain,
( e4 != op(e3,e1)
| spl24_157 ),
inference(avatar_component_clause,[],[f1094]) ).
fof(f1096,plain,
( e4 = op(e3,e1)
| ~ spl24_157 ),
inference(avatar_component_clause,[],[f1094]) ).
fof(f1115,definition,
( spl24_162
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl24_162])],[avatar_definition]) ).
fof(f1117,plain,
( e3 = op(e0,e3)
| ~ spl24_162 ),
inference(avatar_component_clause,[],[f1115]) ).
fof(f1121,definition,
( spl24_163
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl24_163])],[avatar_definition]) ).
fof(f1123,plain,
( e2 = op(e1,e3)
| ~ spl24_163 ),
inference(avatar_component_clause,[],[f1121]) ).
fof(f1125,definition,
( spl24_164
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl24_164])],[avatar_definition]) ).
fof(f1127,plain,
( e2 = op(e0,e3)
| ~ spl24_164 ),
inference(avatar_component_clause,[],[f1125]) ).
fof(f1128,plain,
( spl24_135
| spl24_37
| spl24_44
| spl24_163
| spl24_164 ),
inference(avatar_split_clause,[],[f109,f1125,f1121,f548,f516,f1000]) ).
fof(f1130,definition,
( spl24_165
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl24_165])],[avatar_definition]) ).
fof(f1132,plain,
( e2 = op(e3,e2)
| ~ spl24_165 ),
inference(avatar_component_clause,[],[f1130]) ).
fof(f1134,definition,
( spl24_166
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl24_166])],[avatar_definition]) ).
fof(f1136,plain,
( e2 = op(e3,e1)
| ~ spl24_166 ),
inference(avatar_component_clause,[],[f1134]) ).
fof(f1138,definition,
( spl24_167
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl24_167])],[avatar_definition]) ).
fof(f1140,plain,
( e2 = op(e3,e0)
| ~ spl24_167 ),
inference(avatar_component_clause,[],[f1138]) ).
fof(f1141,plain,
( spl24_132
| spl24_37
| spl24_165
| spl24_166
| spl24_167 ),
inference(avatar_split_clause,[],[f110,f1138,f1134,f1130,f516,f987]) ).
fof(f1143,definition,
( spl24_168
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl24_168])],[avatar_definition]) ).
fof(f1145,plain,
( e1 = op(e2,e3)
| ~ spl24_168 ),
inference(avatar_component_clause,[],[f1143]) ).
fof(f1187,definition,
( spl24_178
<=> e4 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl24_178])],[avatar_definition]) ).
fof(f1191,definition,
( spl24_179
<=> e4 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl24_179])],[avatar_definition]) ).
fof(f1193,plain,
( e4 = op(e0,e2)
| ~ spl24_179 ),
inference(avatar_component_clause,[],[f1191]) ).
fof(f1194,plain,
( spl24_28
| spl24_156
| spl24_43
| spl24_178
| spl24_179 ),
inference(avatar_split_clause,[],[f115,f1191,f1187,f543,f1090,f476]) ).
fof(f1196,definition,
( spl24_180
<=> e4 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl24_180])],[avatar_definition]) ).
fof(f1198,plain,
( e4 = op(e2,e1)
| ~ spl24_180 ),
inference(avatar_component_clause,[],[f1196]) ).
fof(f1200,definition,
( spl24_181
<=> e4 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl24_181])],[avatar_definition]) ).
fof(f1202,plain,
( e4 = op(e2,e0)
| ~ spl24_181 ),
inference(avatar_component_clause,[],[f1200]) ).
fof(f1203,plain,
( spl24_122
| spl24_153
| spl24_43
| spl24_180
| spl24_181 ),
inference(avatar_split_clause,[],[f116,f1200,f1196,f543,f1077,f943]) ).
fof(f1205,definition,
( spl24_182
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl24_182])],[avatar_definition]) ).
fof(f1207,plain,
( e3 = op(e1,e2)
| ~ spl24_182 ),
inference(avatar_component_clause,[],[f1205]) ).
fof(f1209,definition,
( spl24_183
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl24_183])],[avatar_definition]) ).
fof(f1212,plain,
( spl24_129
| spl24_36
| spl24_45
| spl24_182
| spl24_183 ),
inference(avatar_split_clause,[],[f117,f1209,f1205,f552,f512,f974]) ).
fof(f1214,definition,
( spl24_184
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl24_184])],[avatar_definition]) ).
fof(f1216,plain,
( e3 = op(e2,e1)
| ~ spl24_184 ),
inference(avatar_component_clause,[],[f1214]) ).
fof(f1231,definition,
( spl24_188
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl24_188])],[avatar_definition]) ).
fof(f1233,plain,
( e2 = op(e0,e2)
| ~ spl24_188 ),
inference(avatar_component_clause,[],[f1231]) ).
fof(f1242,definition,
( spl24_190
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl24_190])],[avatar_definition]) ).
fof(f1246,definition,
( spl24_191
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl24_191])],[avatar_definition]) ).
fof(f1249,plain,
( spl24_140
| spl24_168
| spl24_47
| spl24_190
| spl24_191 ),
inference(avatar_split_clause,[],[f122,f1246,f1242,f561,f1143,f1021]) ).
fof(f1290,definition,
( spl24_200
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl24_200])],[avatar_definition]) ).
fof(f1292,plain,
( e2 = op(e1,e0)
| ~ spl24_200 ),
inference(avatar_component_clause,[],[f1290]) ).
fof(f1299,definition,
( spl24_202
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl24_202])],[avatar_definition]) ).
fof(f1301,plain,
( e1 = op(e0,e1)
| ~ spl24_202 ),
inference(avatar_component_clause,[],[f1299]) ).
fof(f1306,definition,
( spl24_203
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl24_203])],[avatar_definition]) ).
fof(f1314,plain,
( spl24_138
| spl24_167
| spl24_48
| spl24_200
| spl24_63 ),
inference(avatar_split_clause,[],[f139,f633,f1290,f566,f1138,f1012]) ).
fof(f1319,definition,
( spl24_204
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl24_204])],[avatar_definition]) ).
fof(f1321,plain,
( e0 = op(e0,e0)
| ~ spl24_204 ),
inference(avatar_component_clause,[],[f1319]) ).
fof(f1325,definition,
( spl24_205
<=> e4 = unit ),
introduced(definition,[new_symbols(definition,[spl24_205])],[avatar_definition]) ).
fof(f1327,plain,
( e4 = unit
| ~ spl24_205 ),
inference(avatar_component_clause,[],[f1325]) ).
fof(f1329,definition,
( spl24_206
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl24_206])],[avatar_definition]) ).
fof(f1331,plain,
( e3 = unit
| ~ spl24_206 ),
inference(avatar_component_clause,[],[f1329]) ).
fof(f1333,definition,
( spl24_207
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl24_207])],[avatar_definition]) ).
fof(f1335,plain,
( e2 = unit
| ~ spl24_207 ),
inference(avatar_component_clause,[],[f1333]) ).
fof(f1337,definition,
( spl24_208
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl24_208])],[avatar_definition]) ).
fof(f1339,plain,
( e1 = unit
| ~ spl24_208 ),
inference(avatar_component_clause,[],[f1337]) ).
fof(f1341,definition,
( spl24_209
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl24_209])],[avatar_definition]) ).
fof(f1343,plain,
( e0 = unit
| ~ spl24_209 ),
inference(avatar_component_clause,[],[f1341]) ).
fof(f1344,plain,
( spl24_205
| spl24_206
| spl24_207
| spl24_208
| spl24_209 ),
inference(avatar_split_clause,[],[f84,f1341,f1337,f1333,f1329,f1325]) ).
fof(f1345,plain,
( spl24_120
| spl24_27
| spl24_29
| spl24_31
| spl24_33 ),
inference(avatar_split_clause,[],[f59,f498,f489,f480,f471,f935]) ).
fof(f1737,plain,
( e2 = op(e4,e2)
| ~ spl24_205 ),
inference(superposition,[],[f90,f1327]) ).
fof(f1738,plain,
( spl24_136
| ~ spl24_205 ),
inference(avatar_split_clause,[],[f1737,f1325,f1004]) ).
fof(f1745,plain,
spl24_125,
inference(avatar_split_clause,[],[f255,f957]) ).
fof(f1746,plain,
spl24_143,
inference(avatar_split_clause,[],[f256,f1034]) ).
fof(f1844,plain,
( e0 = op(e1,e0)
| ~ spl24_208 ),
inference(superposition,[],[f94,f1339]) ).
fof(f1846,plain,
( spl24_203
| ~ spl24_208 ),
inference(avatar_split_clause,[],[f1844,f1337,f1306]) ).
fof(f1855,plain,
( e4 = op(e0,e4)
| ~ spl24_209 ),
inference(superposition,[],[f86,f1343]) ).
fof(f1857,plain,
( e3 = op(e0,e3)
| ~ spl24_209 ),
inference(superposition,[],[f88,f1343]) ).
fof(f1859,plain,
( e2 = op(e0,e2)
| ~ spl24_209 ),
inference(superposition,[],[f90,f1343]) ).
fof(f1861,plain,
( e1 = op(e0,e1)
| ~ spl24_209 ),
inference(superposition,[],[f92,f1343]) ).
fof(f1863,plain,
( e0 = op(e0,e0)
| ~ spl24_209 ),
inference(superposition,[],[f94,f1343]) ).
fof(f1866,plain,
( spl24_204
| ~ spl24_209 ),
inference(avatar_split_clause,[],[f1863,f1341,f1319]) ).
fof(f1867,plain,
( spl24_202
| ~ spl24_209 ),
inference(avatar_split_clause,[],[f1861,f1341,f1299]) ).
fof(f1868,plain,
( spl24_188
| ~ spl24_209 ),
inference(avatar_split_clause,[],[f1859,f1341,f1231]) ).
fof(f1869,plain,
( spl24_162
| ~ spl24_209 ),
inference(avatar_split_clause,[],[f1857,f1341,f1115]) ).
fof(f1870,plain,
( spl24_124
| ~ spl24_209 ),
inference(avatar_split_clause,[],[f1855,f1341,f951]) ).
fof(f1887,plain,
( e4 = op(e4,e2)
| ~ spl24_207 ),
inference(superposition,[],[f85,f1335]) ).
fof(f1907,plain,
( $false
| spl24_28
| ~ spl24_207 ),
inference(forward_subsumption_resolution,[],[f1887,f477]) ).
fof(f1908,plain,
( spl24_28
| ~ spl24_207 ),
inference(avatar_contradiction_clause,[],[f1907]) ).
fof(f1909,plain,
( e4 = op(e4,e3)
| ~ spl24_206 ),
inference(superposition,[],[f85,f1331]) ).
fof(f1971,plain,
( e3 = e4
| ~ spl24_122
| ~ spl24_125 ),
inference(superposition,[],[f959,f945]) ).
fof(f1976,plain,
( $false
| ~ spl24_122
| ~ spl24_125 ),
inference(forward_subsumption_resolution,[],[f1971,f245]) ).
fof(f1977,plain,
( ~ spl24_122
| ~ spl24_125 ),
inference(avatar_contradiction_clause,[],[f1976]) ).
fof(f2001,plain,
( spl24_26
| ~ spl24_206 ),
inference(avatar_split_clause,[],[f1909,f1329,f467]) ).
fof(f2046,plain,
( e2 = e4
| ~ spl24_32
| ~ spl24_138 ),
inference(superposition,[],[f1014,f496]) ).
fof(f2050,plain,
( $false
| ~ spl24_32
| ~ spl24_138 ),
inference(forward_subsumption_resolution,[],[f2046,f246]) ).
fof(f2051,plain,
( ~ spl24_32
| ~ spl24_138 ),
inference(avatar_contradiction_clause,[],[f2050]) ).
fof(f2052,plain,
( e2 = e4
| ~ spl24_30
| ~ spl24_137 ),
inference(superposition,[],[f1010,f487]) ).
fof(f2056,plain,
( $false
| ~ spl24_30
| ~ spl24_137 ),
inference(forward_subsumption_resolution,[],[f2052,f246]) ).
fof(f2057,plain,
( ~ spl24_30
| ~ spl24_137 ),
inference(avatar_contradiction_clause,[],[f2056]) ).
fof(f2069,plain,
( e1 = e3
| ~ spl24_125
| ~ spl24_140 ),
inference(superposition,[],[f1023,f959]) ).
fof(f2075,plain,
( $false
| ~ spl24_125
| ~ spl24_140 ),
inference(forward_subsumption_resolution,[],[f2069,f249]) ).
fof(f2076,plain,
( ~ spl24_125
| ~ spl24_140 ),
inference(avatar_contradiction_clause,[],[f2075]) ).
fof(f2128,plain,
( e2 = e3
| ~ spl24_42
| ~ spl24_125 ),
inference(superposition,[],[f541,f959]) ).
fof(f2133,plain,
( $false
| ~ spl24_42
| ~ spl24_125 ),
inference(forward_subsumption_resolution,[],[f2128,f247]) ).
fof(f2134,plain,
( ~ spl24_42
| ~ spl24_125 ),
inference(avatar_contradiction_clause,[],[f2133]) ).
fof(f2189,plain,
( e1 = e2
| ~ spl24_136
| ~ spl24_143 ),
inference(superposition,[],[f1036,f1006]) ).
fof(f2195,plain,
( $false
| ~ spl24_136
| ~ spl24_143 ),
inference(forward_subsumption_resolution,[],[f2189,f250]) ).
fof(f2196,plain,
( ~ spl24_136
| ~ spl24_143 ),
inference(avatar_contradiction_clause,[],[f2195]) ).
fof(f2231,plain,
( e1 = e3
| ~ spl24_129
| ~ spl24_143 ),
inference(superposition,[],[f976,f1036]) ).
fof(f2237,plain,
( $false
| ~ spl24_129
| ~ spl24_143 ),
inference(forward_subsumption_resolution,[],[f2231,f249]) ).
fof(f2238,plain,
( ~ spl24_129
| ~ spl24_143 ),
inference(avatar_contradiction_clause,[],[f2237]) ).
fof(f2268,plain,
( e3 = e4
| ~ spl24_32
| ~ spl24_131 ),
inference(superposition,[],[f984,f496]) ).
fof(f2273,plain,
( $false
| ~ spl24_32
| ~ spl24_131 ),
inference(forward_subsumption_resolution,[],[f2268,f245]) ).
fof(f2274,plain,
( ~ spl24_32
| ~ spl24_131 ),
inference(avatar_contradiction_clause,[],[f2273]) ).
fof(f2368,plain,
( e3 = e4
| ~ spl24_30
| ~ spl24_130 ),
inference(superposition,[],[f980,f487]) ).
fof(f2373,plain,
( $false
| ~ spl24_30
| ~ spl24_130 ),
inference(forward_subsumption_resolution,[],[f2368,f245]) ).
fof(f2374,plain,
( ~ spl24_30
| ~ spl24_130 ),
inference(avatar_contradiction_clause,[],[f2373]) ).
fof(f2489,plain,
( e1 = e2
| ~ spl24_132
| ~ spl24_139 ),
inference(superposition,[],[f1019,f989]) ).
fof(f2496,plain,
( $false
| ~ spl24_132
| ~ spl24_139 ),
inference(forward_subsumption_resolution,[],[f2489,f250]) ).
fof(f2497,plain,
( ~ spl24_132
| ~ spl24_139 ),
inference(avatar_contradiction_clause,[],[f2496]) ).
fof(f2500,plain,
( e1 = e4
| ~ spl24_124
| ~ spl24_141 ),
inference(superposition,[],[f1027,f953]) ).
fof(f2507,plain,
( $false
| ~ spl24_124
| ~ spl24_141 ),
inference(forward_subsumption_resolution,[],[f2500,f248]) ).
fof(f2508,plain,
( ~ spl24_124
| ~ spl24_141 ),
inference(avatar_contradiction_clause,[],[f2507]) ).
fof(f2531,plain,
( e2 = e3
| ~ spl24_128
| ~ spl24_135 ),
inference(superposition,[],[f1002,f972]) ).
fof(f2532,plain,
( e2 = e3
| ~ spl24_128
| ~ spl24_135 ),
inference(superposition,[],[f972,f1002]) ).
fof(f2534,plain,
( $false
| ~ spl24_128
| ~ spl24_135 ),
inference(forward_subsumption_resolution,[],[f2532,f247]) ).
fof(f2535,plain,
( ~ spl24_128
| ~ spl24_135 ),
inference(avatar_contradiction_clause,[],[f2534]) ).
fof(f2536,plain,
( $false
| ~ spl24_128
| ~ spl24_135 ),
inference(forward_subsumption_resolution,[],[f2531,f247]) ).
fof(f2537,plain,
( ~ spl24_128
| ~ spl24_135 ),
inference(avatar_contradiction_clause,[],[f2536]) ).
fof(f2543,plain,
( e4 = op(e4,e0)
| ~ spl24_209 ),
inference(superposition,[],[f85,f1343]) ).
fof(f2545,plain,
( e3 = op(e3,e0)
| ~ spl24_209 ),
inference(superposition,[],[f87,f1343]) ).
fof(f2559,plain,
( spl24_40
| ~ spl24_209 ),
inference(avatar_split_clause,[],[f2545,f1341,f530]) ).
fof(f2566,plain,
( e2 = e4
| ~ spl24_124
| ~ spl24_134 ),
inference(superposition,[],[f997,f953]) ).
fof(f2572,plain,
( $false
| ~ spl24_124
| ~ spl24_134 ),
inference(forward_subsumption_resolution,[],[f2566,f246]) ).
fof(f2573,plain,
( ~ spl24_124
| ~ spl24_134 ),
inference(avatar_contradiction_clause,[],[f2572]) ).
fof(f2619,plain,
( e3 = e4
| ~ spl24_36
| ~ spl24_156 ),
inference(superposition,[],[f1092,f514]) ).
fof(f2623,plain,
( $false
| ~ spl24_36
| ~ spl24_156 ),
inference(forward_subsumption_resolution,[],[f2619,f245]) ).
fof(f2624,plain,
( ~ spl24_36
| ~ spl24_156 ),
inference(avatar_contradiction_clause,[],[f2623]) ).
fof(f2663,plain,
( e3 = e4
| ~ spl24_155
| ~ spl24_162 ),
inference(superposition,[],[f1117,f1087]) ).
fof(f2668,plain,
( $false
| ~ spl24_155
| ~ spl24_162 ),
inference(forward_subsumption_resolution,[],[f2663,f245]) ).
fof(f2669,plain,
( ~ spl24_155
| ~ spl24_162 ),
inference(avatar_contradiction_clause,[],[f2668]) ).
fof(f2688,plain,
( e1 = e4
| ~ spl24_153
| ~ spl24_168 ),
inference(superposition,[],[f1145,f1079]) ).
fof(f2693,plain,
( $false
| ~ spl24_153
| ~ spl24_168 ),
inference(forward_subsumption_resolution,[],[f2688,f248]) ).
fof(f2694,plain,
( ~ spl24_153
| ~ spl24_168 ),
inference(avatar_contradiction_clause,[],[f2693]) ).
fof(f2696,plain,
( e2 = e4
| ~ spl24_154
| ~ spl24_163 ),
inference(superposition,[],[f1083,f1123]) ).
fof(f2702,plain,
( $false
| ~ spl24_154
| ~ spl24_163 ),
inference(forward_subsumption_resolution,[],[f2696,f246]) ).
fof(f2703,plain,
( ~ spl24_154
| ~ spl24_163 ),
inference(avatar_contradiction_clause,[],[f2702]) ).
fof(f2791,plain,
( e2 = e3
| ~ spl24_162
| ~ spl24_164 ),
inference(superposition,[],[f1127,f1117]) ).
fof(f2797,plain,
( $false
| ~ spl24_162
| ~ spl24_164 ),
inference(forward_subsumption_resolution,[],[f2791,f247]) ).
fof(f2798,plain,
( ~ spl24_162
| ~ spl24_164 ),
inference(avatar_contradiction_clause,[],[f2797]) ).
fof(f2887,plain,
( spl24_32
| ~ spl24_209 ),
inference(avatar_split_clause,[],[f2543,f1341,f494]) ).
fof(f2971,plain,
( e2 = e3
| ~ spl24_40
| ~ spl24_167 ),
inference(superposition,[],[f1140,f532]) ).
fof(f2977,plain,
( $false
| ~ spl24_40
| ~ spl24_167 ),
inference(forward_subsumption_resolution,[],[f2971,f247]) ).
fof(f2978,plain,
( ~ spl24_40
| ~ spl24_167 ),
inference(avatar_contradiction_clause,[],[f2977]) ).
fof(f2979,plain,
( e2 = e4
| ~ spl24_157
| ~ spl24_166 ),
inference(superposition,[],[f1136,f1096]) ).
fof(f2985,plain,
( $false
| ~ spl24_157
| ~ spl24_166 ),
inference(forward_subsumption_resolution,[],[f2979,f246]) ).
fof(f2986,plain,
( ~ spl24_157
| ~ spl24_166 ),
inference(avatar_contradiction_clause,[],[f2985]) ).
fof(f2992,plain,
( e1 = e2
| ~ spl24_44
| ~ spl24_168 ),
inference(superposition,[],[f1145,f550]) ).
fof(f2998,plain,
( $false
| ~ spl24_44
| ~ spl24_168 ),
inference(forward_subsumption_resolution,[],[f2992,f250]) ).
fof(f2999,plain,
( ~ spl24_44
| ~ spl24_168 ),
inference(avatar_contradiction_clause,[],[f2998]) ).
fof(f3071,plain,
( e1 = e4
| ~ spl24_28
| ~ spl24_143 ),
inference(superposition,[],[f478,f1036]) ).
fof(f3078,plain,
( $false
| ~ spl24_28
| ~ spl24_143 ),
inference(forward_subsumption_resolution,[],[f3071,f248]) ).
fof(f3079,plain,
( ~ spl24_28
| ~ spl24_143 ),
inference(avatar_contradiction_clause,[],[f3078]) ).
fof(f3193,plain,
( e1 = e3
| ~ spl24_34
| ~ spl24_139 ),
inference(superposition,[],[f1019,f505]) ).
fof(f3199,plain,
( $false
| ~ spl24_34
| ~ spl24_139 ),
inference(forward_subsumption_resolution,[],[f3193,f249]) ).
fof(f3200,plain,
( ~ spl24_34
| ~ spl24_139 ),
inference(avatar_contradiction_clause,[],[f3199]) ).
fof(f3203,plain,
( e1 = e2
| ~ spl24_135
| ~ spl24_142 ),
inference(superposition,[],[f1032,f1002]) ).
fof(f3209,plain,
( $false
| ~ spl24_135
| ~ spl24_142 ),
inference(forward_subsumption_resolution,[],[f3203,f250]) ).
fof(f3210,plain,
( ~ spl24_135
| ~ spl24_142 ),
inference(avatar_contradiction_clause,[],[f3209]) ).
fof(f3397,plain,
( e2 = e4
| ~ spl24_156
| ~ spl24_165 ),
inference(superposition,[],[f1132,f1092]) ).
fof(f3403,plain,
( $false
| ~ spl24_156
| ~ spl24_165 ),
inference(forward_subsumption_resolution,[],[f3397,f246]) ).
fof(f3404,plain,
( ~ spl24_156
| ~ spl24_165 ),
inference(avatar_contradiction_clause,[],[f3403]) ).
fof(f3430,plain,
( e2 = e4
| ~ spl24_48
| ~ spl24_181 ),
inference(superposition,[],[f1202,f568]) ).
fof(f3434,plain,
( $false
| ~ spl24_48
| ~ spl24_181 ),
inference(forward_subsumption_resolution,[],[f3430,f246]) ).
fof(f3435,plain,
( ~ spl24_48
| ~ spl24_181 ),
inference(avatar_contradiction_clause,[],[f3434]) ).
fof(f3455,plain,
( e3 = e4
| ~ spl24_180
| ~ spl24_184 ),
inference(superposition,[],[f1216,f1198]) ).
fof(f3460,plain,
( $false
| ~ spl24_180
| ~ spl24_184 ),
inference(forward_subsumption_resolution,[],[f3455,f245]) ).
fof(f3461,plain,
( ~ spl24_180
| ~ spl24_184 ),
inference(avatar_contradiction_clause,[],[f3460]) ).
fof(f3473,plain,
( e2 = e4
| ~ spl24_179
| ~ spl24_188 ),
inference(superposition,[],[f1233,f1193]) ).
fof(f3478,plain,
( $false
| ~ spl24_179
| ~ spl24_188 ),
inference(forward_subsumption_resolution,[],[f3473,f246]) ).
fof(f3479,plain,
( ~ spl24_179
| ~ spl24_188 ),
inference(avatar_contradiction_clause,[],[f3478]) ).
fof(f3532,plain,
( e1 = e2
| ~ spl24_56
| ~ spl24_200 ),
inference(superposition,[],[f1292,f604]) ).
fof(f3537,plain,
( $false
| ~ spl24_56
| ~ spl24_200 ),
inference(forward_subsumption_resolution,[],[f3532,f250]) ).
fof(f3538,plain,
( ~ spl24_56
| ~ spl24_200 ),
inference(avatar_contradiction_clause,[],[f3537]) ).
fof(f3621,plain,
( e4 != op(e1,e2)
| ~ spl24_154 ),
inference(superposition,[],[f177,f1083]) ).
fof(f3627,plain,
( e1 != op(e1,e4)
| ~ spl24_56 ),
inference(superposition,[],[f181,f604]) ).
fof(f3632,plain,
( e0 != op(e1,e0)
| ~ spl24_57 ),
inference(superposition,[],[f184,f607]) ).
fof(f3635,plain,
( e3 != op(e0,e2)
| ~ spl24_162 ),
inference(superposition,[],[f187,f1117]) ).
fof(f3643,plain,
( e0 != op(e0,e2)
| ~ spl24_204 ),
inference(superposition,[],[f193,f1321]) ).
fof(f3644,plain,
( ~ spl24_62
| ~ spl24_204 ),
inference(avatar_split_clause,[],[f3643,f1319,f629]) ).
fof(f3670,plain,
( e1 != op(e2,e2)
| ~ spl24_143 ),
inference(superposition,[],[f216,f1036]) ).
fof(f3687,plain,
( e1 != op(e2,e1)
| ~ spl24_202 ),
inference(superposition,[],[f233,f1301]) ).
fof(f3696,plain,
( e1 != op(e2,e0)
| ~ spl24_56 ),
inference(superposition,[],[f240,f604]) ).
fof(f3703,plain,
( e0 = op(e1,e1)
| ~ spl24_143 ),
inference(superposition,[],[f257,f1036]) ).
fof(f3704,plain,
( e2 != op(e1,e4)
| spl24_70
| ~ spl24_143 ),
inference(superposition,[],[f671,f1036]) ).
fof(f3713,plain,
( e0 != op(e1,e1)
| ~ spl24_56
| spl24_109 ),
inference(superposition,[],[f878,f604]) ).
fof(f3714,plain,
( $false
| ~ spl24_56
| ~ spl24_57
| spl24_109 ),
inference(forward_subsumption_resolution,[],[f3713,f607]) ).
fof(f3715,plain,
( ~ spl24_56
| ~ spl24_57
| spl24_109 ),
inference(avatar_contradiction_clause,[],[f3714]) ).
fof(f3717,plain,
( e4 != op(e1,e3)
| spl24_79
| ~ spl24_139 ),
inference(superposition,[],[f716,f1019]) ).
fof(f3720,plain,
( e4 != op(e4,e0)
| spl24_78
| ~ spl24_124 ),
inference(superposition,[],[f711,f953]) ).
fof(f3721,plain,
( $false
| ~ spl24_32
| spl24_78
| ~ spl24_124 ),
inference(forward_subsumption_resolution,[],[f3720,f496]) ).
fof(f3722,plain,
( ~ spl24_32
| spl24_78
| ~ spl24_124 ),
inference(avatar_contradiction_clause,[],[f3721]) ).
fof(f3745,plain,
( e4 = op(e3,e1)
| ~ spl24_74
| ~ spl24_130 ),
inference(superposition,[],[f691,f980]) ).
fof(f3746,plain,
( $false
| ~ spl24_74
| ~ spl24_130
| spl24_157 ),
inference(forward_subsumption_resolution,[],[f3745,f1095]) ).
fof(f3747,plain,
( ~ spl24_74
| ~ spl24_130
| spl24_157 ),
inference(avatar_contradiction_clause,[],[f3746]) ).
fof(f3755,plain,
( e3 != op(e0,e3)
| ~ spl24_40
| spl24_90 ),
inference(superposition,[],[f774,f532]) ).
fof(f3756,plain,
( $false
| ~ spl24_40
| spl24_90
| ~ spl24_162 ),
inference(forward_subsumption_resolution,[],[f3755,f1117]) ).
fof(f3757,plain,
( ~ spl24_40
| spl24_90
| ~ spl24_162 ),
inference(avatar_contradiction_clause,[],[f3756]) ).
fof(f3775,plain,
( e1 = op(e4,e3)
| ~ spl24_105
| ~ spl24_154 ),
inference(superposition,[],[f854,f1083]) ).
fof(f3776,plain,
( $false
| ~ spl24_105
| spl24_142
| ~ spl24_154 ),
inference(forward_subsumption_resolution,[],[f3775,f1031]) ).
fof(f3777,plain,
( ~ spl24_105
| spl24_142
| ~ spl24_154 ),
inference(avatar_contradiction_clause,[],[f3776]) ).
fof(f3781,plain,
( e1 != op(e0,e1)
| ~ spl24_56
| spl24_111 ),
inference(superposition,[],[f888,f604]) ).
fof(f3782,plain,
( $false
| ~ spl24_56
| spl24_111
| ~ spl24_202 ),
inference(forward_subsumption_resolution,[],[f3781,f1301]) ).
fof(f3783,plain,
( ~ spl24_56
| spl24_111
| ~ spl24_202 ),
inference(avatar_contradiction_clause,[],[f3782]) ).
fof(f3784,plain,
( e2 != op(e2,e0)
| spl24_101
| ~ spl24_188 ),
inference(superposition,[],[f833,f1233]) ).
fof(f3785,plain,
( $false
| ~ spl24_48
| spl24_101
| ~ spl24_188 ),
inference(forward_subsumption_resolution,[],[f3784,f568]) ).
fof(f3786,plain,
( ~ spl24_48
| spl24_101
| ~ spl24_188 ),
inference(avatar_contradiction_clause,[],[f3785]) ).
fof(f3792,plain,
( e2 = op(e3,e4)
| ~ spl24_92
| ~ spl24_125 ),
inference(superposition,[],[f784,f959]) ).
fof(f3793,plain,
( $false
| ~ spl24_92
| ~ spl24_125
| spl24_132 ),
inference(forward_subsumption_resolution,[],[f3792,f988]) ).
fof(f3794,plain,
( ~ spl24_92
| ~ spl24_125
| spl24_132 ),
inference(avatar_contradiction_clause,[],[f3793]) ).
fof(f3803,plain,
( e3 = op(e4,e2)
| ~ spl24_83
| ~ spl24_156 ),
inference(superposition,[],[f739,f1092]) ).
fof(f3804,plain,
( $false
| ~ spl24_83
| spl24_129
| ~ spl24_156 ),
inference(forward_subsumption_resolution,[],[f3803,f975]) ).
fof(f3805,plain,
( ~ spl24_83
| spl24_129
| ~ spl24_156 ),
inference(avatar_contradiction_clause,[],[f3804]) ).
fof(f3808,plain,
( e2 = op(e1,e3)
| ~ spl24_94
| ~ spl24_168 ),
inference(superposition,[],[f795,f1145]) ).
fof(f3821,plain,
( e2 != op(e3,e1)
| spl24_106
| ~ spl24_182 ),
inference(superposition,[],[f860,f1207]) ).
fof(f3822,plain,
( $false
| spl24_106
| ~ spl24_166
| ~ spl24_182 ),
inference(forward_subsumption_resolution,[],[f3821,f1136]) ).
fof(f3823,plain,
( spl24_106
| ~ spl24_166
| ~ spl24_182 ),
inference(avatar_contradiction_clause,[],[f3822]) ).
fof(f3824,plain,
( e4 != op(e2,e1)
| spl24_102
| ~ spl24_133 ),
inference(superposition,[],[f838,f993]) ).
fof(f3825,plain,
( $false
| spl24_102
| ~ spl24_133
| ~ spl24_180 ),
inference(forward_subsumption_resolution,[],[f3824,f1198]) ).
fof(f3826,plain,
( spl24_102
| ~ spl24_133
| ~ spl24_180 ),
inference(avatar_contradiction_clause,[],[f3825]) ).
fof(f3834,plain,
( e4 = op(e2,e3)
| ~ spl24_68
| ~ spl24_135 ),
inference(superposition,[],[f661,f1002]) ).
fof(f3839,plain,
( e3 = op(e2,e1)
| ~ spl24_86
| ~ spl24_166 ),
inference(superposition,[],[f754,f1136]) ).
fof(f3843,plain,
( e1 != op(e4,e2)
| spl24_96
| ~ spl24_180 ),
inference(superposition,[],[f808,f1198]) ).
fof(f3844,plain,
( $false
| spl24_96
| ~ spl24_143
| ~ spl24_180 ),
inference(forward_subsumption_resolution,[],[f3843,f1036]) ).
fof(f3845,plain,
( spl24_96
| ~ spl24_143
| ~ spl24_180 ),
inference(avatar_contradiction_clause,[],[f3844]) ).
fof(f3846,plain,
( ~ spl24_183
| ~ spl24_162 ),
inference(avatar_split_clause,[],[f3635,f1115,f1209]) ).
fof(f3848,plain,
( ~ spl24_178
| ~ spl24_154 ),
inference(avatar_split_clause,[],[f3621,f1081,f1187]) ).
fof(f3852,plain,
( spl24_184
| ~ spl24_86
| ~ spl24_166 ),
inference(avatar_split_clause,[],[f3839,f1134,f752,f1214]) ).
fof(f3855,plain,
( ~ spl24_190
| ~ spl24_202 ),
inference(avatar_split_clause,[],[f3687,f1299,f1242]) ).
fof(f3860,plain,
( spl24_153
| ~ spl24_68
| ~ spl24_135 ),
inference(avatar_split_clause,[],[f3834,f1000,f659,f1077]) ).
fof(f3861,plain,
( ~ spl24_154
| spl24_79
| ~ spl24_139 ),
inference(avatar_split_clause,[],[f3717,f1017,f714,f1081]) ).
fof(f3863,plain,
( ~ spl24_191
| ~ spl24_56 ),
inference(avatar_split_clause,[],[f3696,f602,f1246]) ).
fof(f3873,plain,
( spl24_57
| ~ spl24_143 ),
inference(avatar_split_clause,[],[f3703,f1034,f606]) ).
fof(f3875,plain,
( ~ spl24_47
| ~ spl24_143 ),
inference(avatar_split_clause,[],[f3670,f1034,f561]) ).
fof(f3877,plain,
( ~ spl24_203
| ~ spl24_57 ),
inference(avatar_split_clause,[],[f3632,f606,f1306]) ).
fof(f3889,plain,
( ~ spl24_133
| spl24_70
| ~ spl24_143 ),
inference(avatar_split_clause,[],[f3704,f1034,f669,f991]) ).
fof(f3892,plain,
( ~ spl24_50
| ~ spl24_56 ),
inference(avatar_split_clause,[],[f3627,f602,f575]) ).
fof(f3893,plain,
( spl24_163
| ~ spl24_94
| ~ spl24_168 ),
inference(avatar_split_clause,[],[f3808,f1143,f793,f1121]) ).
fof(f3899,plain,
( e4 != op(e4,e4)
| ~ spl24_26 ),
inference(superposition,[],[f145,f469]) ).
fof(f3901,plain,
( e4 != op(e4,e1)
| ~ spl24_26 ),
inference(superposition,[],[f149,f469]) ).
fof(f3902,plain,
( e4 != op(e4,e0)
| ~ spl24_26 ),
inference(superposition,[],[f152,f469]) ).
fof(f3911,plain,
( ~ spl24_32
| ~ spl24_26 ),
inference(avatar_split_clause,[],[f3902,f467,f494]) ).
fof(f3912,plain,
( ~ spl24_30
| ~ spl24_26 ),
inference(avatar_split_clause,[],[f3901,f467,f485]) ).
fof(f3913,plain,
( ~ spl24_120
| ~ spl24_26 ),
inference(avatar_split_clause,[],[f3899,f467,f935]) ).
fof(f3916,plain,
( e3 != op(e2,e4)
| ~ spl24_27 ),
inference(superposition,[],[f196,f472]) ).
fof(f3919,plain,
( $false
| ~ spl24_27
| ~ spl24_125 ),
inference(forward_subsumption_resolution,[],[f3916,f959]) ).
fof(f3920,plain,
( ~ spl24_27
| ~ spl24_125 ),
inference(avatar_contradiction_clause,[],[f3919]) ).
cnf(s3,plain,
( spl24_1
| spl24_2
| spl24_3
| spl24_4
| spl24_5
| spl24_6
| spl24_7
| spl24_8
| spl24_9
| spl24_10
| spl24_11
| spl24_12
| spl24_13
| spl24_14
| spl24_15
| spl24_16
| spl24_17
| spl24_18
| spl24_19
| spl24_20
| spl24_21
| spl24_22
| spl24_23
| spl24_24 ),
inference(sat_conversion,[],[f465]) ).
cnf(s5,plain,
( spl24_28
| ~ spl24_29 ),
inference(sat_conversion,[],[f483]) ).
cnf(s6,plain,
( spl24_30
| ~ spl24_31 ),
inference(sat_conversion,[],[f492]) ).
cnf(s7,plain,
( spl24_32
| ~ spl24_33 ),
inference(sat_conversion,[],[f501]) ).
cnf(s8,plain,
( spl24_34
| ~ spl24_35 ),
inference(sat_conversion,[],[f510]) ).
cnf(s9,plain,
( spl24_36
| ~ spl24_37 ),
inference(sat_conversion,[],[f519]) ).
cnf(s12,plain,
( spl24_42
| ~ spl24_43 ),
inference(sat_conversion,[],[f546]) ).
cnf(s13,plain,
( spl24_44
| ~ spl24_45 ),
inference(sat_conversion,[],[f555]) ).
cnf(s19,plain,
( spl24_56
| ~ spl24_57 ),
inference(sat_conversion,[],[f609]) ).
cnf(s22,plain,
( spl24_62
| ~ spl24_63 ),
inference(sat_conversion,[],[f636]) ).
cnf(s26,plain,
~ spl24_1,
inference(sat_conversion,[],[f652]) ).
cnf(s28,plain,
( ~ spl24_2
| spl24_68 ),
inference(sat_conversion,[],[f662]) ).
cnf(s30,plain,
( ~ spl24_3
| ~ spl24_70 ),
inference(sat_conversion,[],[f672]) ).
cnf(s34,plain,
( ~ spl24_4
| spl24_74 ),
inference(sat_conversion,[],[f692]) ).
cnf(s38,plain,
( ~ spl24_5
| ~ spl24_78 ),
inference(sat_conversion,[],[f712]) ).
cnf(s39,plain,
( ~ spl24_6
| ~ spl24_79 ),
inference(sat_conversion,[],[f717]) ).
cnf(s44,plain,
~ spl24_7,
inference(sat_conversion,[],[f730]) ).
cnf(s46,plain,
( ~ spl24_8
| spl24_83 ),
inference(sat_conversion,[],[f740]) ).
cnf(s49,plain,
( ~ spl24_9
| spl24_86 ),
inference(sat_conversion,[],[f755]) ).
cnf(s53,plain,
( ~ spl24_10
| ~ spl24_90 ),
inference(sat_conversion,[],[f775]) ).
cnf(s55,plain,
( ~ spl24_11
| spl24_92 ),
inference(sat_conversion,[],[f785]) ).
cnf(s58,plain,
( ~ spl24_12
| spl24_94 ),
inference(sat_conversion,[],[f796]) ).
cnf(s62,plain,
~ spl24_13,
inference(sat_conversion,[],[f804]) ).
cnf(s63,plain,
( ~ spl24_14
| ~ spl24_96 ),
inference(sat_conversion,[],[f809]) ).
cnf(s68,plain,
( ~ spl24_15
| ~ spl24_101 ),
inference(sat_conversion,[],[f834]) ).
cnf(s69,plain,
( ~ spl24_16
| ~ spl24_102 ),
inference(sat_conversion,[],[f839]) ).
cnf(s73,plain,
( ~ spl24_17
| spl24_105 ),
inference(sat_conversion,[],[f855]) ).
cnf(s75,plain,
( ~ spl24_18
| ~ spl24_106 ),
inference(sat_conversion,[],[f861]) ).
cnf(s80,plain,
~ spl24_19,
inference(sat_conversion,[],[f874]) ).
cnf(s81,plain,
( ~ spl24_20
| ~ spl24_109 ),
inference(sat_conversion,[],[f879]) ).
cnf(s86,plain,
( ~ spl24_21
| ~ spl24_78 ),
inference(sat_conversion,[],[f900]) ).
cnf(s89,plain,
( ~ spl24_22
| ~ spl24_90 ),
inference(sat_conversion,[],[f911]) ).
cnf(s92,plain,
( ~ spl24_23
| ~ spl24_101 ),
inference(sat_conversion,[],[f922]) ).
cnf(s95,plain,
( ~ spl24_24
| ~ spl24_111 ),
inference(sat_conversion,[],[f933]) ).
cnf(s99,plain,
( spl24_27
| spl24_128
| spl24_129
| spl24_130
| spl24_131 ),
inference(sat_conversion,[],[f985]) ).
cnf(s100,plain,
( spl24_29
| spl24_42
| spl24_132
| spl24_133
| spl24_134 ),
inference(sat_conversion,[],[f998]) ).
cnf(s101,plain,
( spl24_29
| spl24_135
| spl24_136
| spl24_137
| spl24_138 ),
inference(sat_conversion,[],[f1015]) ).
cnf(s102,plain,
( spl24_31
| spl24_50
| spl24_139
| spl24_140
| spl24_141 ),
inference(sat_conversion,[],[f1028]) ).
cnf(s106,plain,
( spl24_26
| spl24_35
| spl24_153
| spl24_154
| spl24_155 ),
inference(sat_conversion,[],[f1088]) ).
cnf(s110,plain,
( spl24_37
| spl24_44
| spl24_135
| spl24_163
| spl24_164 ),
inference(sat_conversion,[],[f1128]) ).
cnf(s111,plain,
( spl24_37
| spl24_132
| spl24_165
| spl24_166
| spl24_167 ),
inference(sat_conversion,[],[f1141]) ).
cnf(s116,plain,
( spl24_28
| spl24_43
| spl24_156
| spl24_178
| spl24_179 ),
inference(sat_conversion,[],[f1194]) ).
cnf(s117,plain,
( spl24_43
| spl24_122
| spl24_153
| spl24_180
| spl24_181 ),
inference(sat_conversion,[],[f1203]) ).
cnf(s118,plain,
( spl24_36
| spl24_45
| spl24_129
| spl24_182
| spl24_183 ),
inference(sat_conversion,[],[f1212]) ).
cnf(s123,plain,
( spl24_47
| spl24_140
| spl24_168
| spl24_190
| spl24_191 ),
inference(sat_conversion,[],[f1249]) ).
cnf(s140,plain,
( spl24_48
| spl24_63
| spl24_138
| spl24_167
| spl24_200 ),
inference(sat_conversion,[],[f1314]) ).
cnf(s146,plain,
( spl24_205
| spl24_206
| spl24_207
| spl24_208
| spl24_209 ),
inference(sat_conversion,[],[f1344]) ).
cnf(s147,plain,
( spl24_27
| spl24_29
| spl24_31
| spl24_33
| spl24_120 ),
inference(sat_conversion,[],[f1345]) ).
cnf(s268,plain,
( spl24_136
| ~ spl24_205 ),
inference(sat_conversion,[],[f1738]) ).
cnf(s271,plain,
spl24_125,
inference(sat_conversion,[],[f1745]) ).
cnf(s272,plain,
spl24_143,
inference(sat_conversion,[],[f1746]) ).
cnf(s284,plain,
( spl24_203
| ~ spl24_208 ),
inference(sat_conversion,[],[f1846]) ).
cnf(s291,plain,
( spl24_204
| ~ spl24_209 ),
inference(sat_conversion,[],[f1866]) ).
cnf(s293,plain,
( spl24_202
| ~ spl24_209 ),
inference(sat_conversion,[],[f1867]) ).
cnf(s294,plain,
( spl24_188
| ~ spl24_209 ),
inference(sat_conversion,[],[f1868]) ).
cnf(s295,plain,
( spl24_162
| ~ spl24_209 ),
inference(sat_conversion,[],[f1869]) ).
cnf(s296,plain,
( spl24_124
| ~ spl24_209 ),
inference(sat_conversion,[],[f1870]) ).
cnf(s309,plain,
( spl24_28
| ~ spl24_207 ),
inference(sat_conversion,[],[f1908]) ).
cnf(s326,plain,
( ~ spl24_122
| ~ spl24_125 ),
inference(sat_conversion,[],[f1977]) ).
cnf(s333,plain,
( spl24_26
| ~ spl24_206 ),
inference(sat_conversion,[],[f2001]) ).
cnf(s345,plain,
( ~ spl24_32
| ~ spl24_138 ),
inference(sat_conversion,[],[f2051]) ).
cnf(s347,plain,
( ~ spl24_30
| ~ spl24_137 ),
inference(sat_conversion,[],[f2057]) ).
cnf(s351,plain,
( ~ spl24_125
| ~ spl24_140 ),
inference(sat_conversion,[],[f2076]) ).
cnf(s368,plain,
( ~ spl24_42
| ~ spl24_125 ),
inference(sat_conversion,[],[f2134]) ).
cnf(s385,plain,
( ~ spl24_136
| ~ spl24_143 ),
inference(sat_conversion,[],[f2196]) ).
cnf(s396,plain,
( ~ spl24_129
| ~ spl24_143 ),
inference(sat_conversion,[],[f2238]) ).
cnf(s403,plain,
( ~ spl24_32
| ~ spl24_131 ),
inference(sat_conversion,[],[f2274]) ).
cnf(s428,plain,
( ~ spl24_30
| ~ spl24_130 ),
inference(sat_conversion,[],[f2374]) ).
cnf(s457,plain,
( ~ spl24_132
| ~ spl24_139 ),
inference(sat_conversion,[],[f2497]) ).
cnf(s459,plain,
( ~ spl24_124
| ~ spl24_141 ),
inference(sat_conversion,[],[f2508]) ).
cnf(s464,plain,
( ~ spl24_128
| ~ spl24_135 ),
inference(sat_conversion,[],[f2535]) ).
cnf(s465,plain,
( ~ spl24_128
| ~ spl24_135 ),
inference(sat_conversion,[],[f2537]) ).
cnf(s475,plain,
( spl24_40
| ~ spl24_209 ),
inference(sat_conversion,[],[f2559]) ).
cnf(s477,plain,
( ~ spl24_124
| ~ spl24_134 ),
inference(sat_conversion,[],[f2573]) ).
cnf(s485,plain,
( ~ spl24_36
| ~ spl24_156 ),
inference(sat_conversion,[],[f2624]) ).
cnf(s495,plain,
( ~ spl24_155
| ~ spl24_162 ),
inference(sat_conversion,[],[f2669]) ).
cnf(s501,plain,
( ~ spl24_153
| ~ spl24_168 ),
inference(sat_conversion,[],[f2694]) ).
cnf(s503,plain,
( ~ spl24_154
| ~ spl24_163 ),
inference(sat_conversion,[],[f2703]) ).
cnf(s519,plain,
( ~ spl24_162
| ~ spl24_164 ),
inference(sat_conversion,[],[f2798]) ).
cnf(s532,plain,
( spl24_32
| ~ spl24_209 ),
inference(sat_conversion,[],[f2887]) ).
cnf(s542,plain,
( ~ spl24_40
| ~ spl24_167 ),
inference(sat_conversion,[],[f2978]) ).
cnf(s544,plain,
( ~ spl24_157
| ~ spl24_166 ),
inference(sat_conversion,[],[f2986]) ).
cnf(s546,plain,
( ~ spl24_44
| ~ spl24_168 ),
inference(sat_conversion,[],[f2999]) ).
cnf(s568,plain,
( ~ spl24_28
| ~ spl24_143 ),
inference(sat_conversion,[],[f3079]) ).
cnf(s595,plain,
( ~ spl24_34
| ~ spl24_139 ),
inference(sat_conversion,[],[f3200]) ).
cnf(s597,plain,
( ~ spl24_135
| ~ spl24_142 ),
inference(sat_conversion,[],[f3210]) ).
cnf(s629,plain,
( ~ spl24_156
| ~ spl24_165 ),
inference(sat_conversion,[],[f3404]) ).
cnf(s635,plain,
( ~ spl24_48
| ~ spl24_181 ),
inference(sat_conversion,[],[f3435]) ).
cnf(s641,plain,
( ~ spl24_180
| ~ spl24_184 ),
inference(sat_conversion,[],[f3461]) ).
cnf(s645,plain,
( ~ spl24_179
| ~ spl24_188 ),
inference(sat_conversion,[],[f3479]) ).
cnf(s660,plain,
( ~ spl24_56
| ~ spl24_200 ),
inference(sat_conversion,[],[f3538]) ).
cnf(s673,plain,
( ~ spl24_62
| ~ spl24_204 ),
inference(sat_conversion,[],[f3644]) ).
cnf(s679,plain,
( ~ spl24_56
| ~ spl24_57
| spl24_109 ),
inference(sat_conversion,[],[f3715]) ).
cnf(s681,plain,
( ~ spl24_32
| spl24_78
| ~ spl24_124 ),
inference(sat_conversion,[],[f3722]) ).
cnf(s685,plain,
( ~ spl24_74
| ~ spl24_130
| spl24_157 ),
inference(sat_conversion,[],[f3747]) ).
cnf(s687,plain,
( ~ spl24_40
| spl24_90
| ~ spl24_162 ),
inference(sat_conversion,[],[f3757]) ).
cnf(s690,plain,
( ~ spl24_105
| spl24_142
| ~ spl24_154 ),
inference(sat_conversion,[],[f3777]) ).
cnf(s691,plain,
( ~ spl24_56
| spl24_111
| ~ spl24_202 ),
inference(sat_conversion,[],[f3783]) ).
cnf(s692,plain,
( ~ spl24_48
| spl24_101
| ~ spl24_188 ),
inference(sat_conversion,[],[f3786]) ).
cnf(s694,plain,
( ~ spl24_92
| ~ spl24_125
| spl24_132 ),
inference(sat_conversion,[],[f3794]) ).
cnf(s697,plain,
( ~ spl24_83
| spl24_129
| ~ spl24_156 ),
inference(sat_conversion,[],[f3805]) ).
cnf(s699,plain,
( spl24_106
| ~ spl24_166
| ~ spl24_182 ),
inference(sat_conversion,[],[f3823]) ).
cnf(s700,plain,
( spl24_102
| ~ spl24_133
| ~ spl24_180 ),
inference(sat_conversion,[],[f3826]) ).
cnf(s705,plain,
( spl24_96
| ~ spl24_143
| ~ spl24_180 ),
inference(sat_conversion,[],[f3845]) ).
cnf(s706,plain,
( ~ spl24_162
| ~ spl24_183 ),
inference(sat_conversion,[],[f3846]) ).
cnf(s708,plain,
( ~ spl24_154
| ~ spl24_178 ),
inference(sat_conversion,[],[f3848]) ).
cnf(s712,plain,
( ~ spl24_86
| ~ spl24_166
| spl24_184 ),
inference(sat_conversion,[],[f3852]) ).
cnf(s715,plain,
( ~ spl24_190
| ~ spl24_202 ),
inference(sat_conversion,[],[f3855]) ).
cnf(s720,plain,
( ~ spl24_68
| ~ spl24_135
| spl24_153 ),
inference(sat_conversion,[],[f3860]) ).
cnf(s721,plain,
( spl24_79
| ~ spl24_139
| ~ spl24_154 ),
inference(sat_conversion,[],[f3861]) ).
cnf(s723,plain,
( ~ spl24_56
| ~ spl24_191 ),
inference(sat_conversion,[],[f3863]) ).
cnf(s733,plain,
( spl24_57
| ~ spl24_143 ),
inference(sat_conversion,[],[f3873]) ).
cnf(s735,plain,
( ~ spl24_47
| ~ spl24_143 ),
inference(sat_conversion,[],[f3875]) ).
cnf(s738,plain,
( ~ spl24_57
| ~ spl24_203 ),
inference(sat_conversion,[],[f3877]) ).
cnf(s756,plain,
( spl24_70
| ~ spl24_133
| ~ spl24_143 ),
inference(sat_conversion,[],[f3889]) ).
cnf(s763,plain,
( ~ spl24_50
| ~ spl24_56 ),
inference(sat_conversion,[],[f3892]) ).
cnf(s765,plain,
( ~ spl24_94
| spl24_163
| ~ spl24_168 ),
inference(sat_conversion,[],[f3893]) ).
cnf(s773,plain,
( ~ spl24_26
| ~ spl24_32 ),
inference(sat_conversion,[],[f3911]) ).
cnf(s774,plain,
( ~ spl24_26
| ~ spl24_30 ),
inference(sat_conversion,[],[f3912]) ).
cnf(s775,plain,
( ~ spl24_26
| ~ spl24_120 ),
inference(sat_conversion,[],[f3913]) ).
cnf(s777,plain,
( ~ spl24_27
| ~ spl24_125 ),
inference(sat_conversion,[],[f3920]) ).
cnf(s778,plain,
~ spl24_47,
inference(rat,[],[s735,s272]) ).
cnf(s779,plain,
spl24_57,
inference(rat,[],[s733,s272]) ).
cnf(s780,plain,
~ spl24_28,
inference(rat,[],[s568,s272]) ).
cnf(s781,plain,
~ spl24_129,
inference(rat,[],[s396,s272]) ).
cnf(s782,plain,
~ spl24_136,
inference(rat,[],[s385,s272]) ).
cnf(s784,plain,
~ spl24_203,
inference(rat,[],[s738,s779]) ).
cnf(s787,plain,
~ spl24_207,
inference(rat,[],[s309,s780]) ).
cnf(s788,plain,
~ spl24_208,
inference(rat,[],[s284,s784]) ).
cnf(s789,plain,
~ spl24_27,
inference(rat,[],[s777,s271]) ).
cnf(s790,plain,
~ spl24_42,
inference(rat,[],[s368,s271]) ).
cnf(s791,plain,
~ spl24_140,
inference(rat,[],[s351,s271]) ).
cnf(s792,plain,
~ spl24_122,
inference(rat,[],[s326,s271]) ).
cnf(s793,plain,
~ spl24_205,
inference(rat,[],[s268,s782]) ).
cnf(s820,plain,
( spl24_29
| spl24_31
| spl24_33
| spl24_120 ),
inference(rat,[],[s147,s789]) ).
cnf(s821,plain,
( spl24_206
| spl24_209 ),
inference(rat,[],[s146,s788,s787,s793]) ).
cnf(s825,plain,
( spl24_168
| spl24_190
| spl24_191 ),
inference(rat,[],[s123,s791,s778]) ).
cnf(s828,plain,
( spl24_36
| spl24_45
| spl24_182
| spl24_183 ),
inference(rat,[],[s118,s781]) ).
cnf(s829,plain,
( spl24_43
| spl24_153
| spl24_180
| spl24_181 ),
inference(rat,[],[s117,s792]) ).
cnf(s830,plain,
( spl24_43
| spl24_156
| spl24_178
| spl24_179 ),
inference(rat,[],[s116,s780]) ).
cnf(s832,plain,
( spl24_31
| spl24_50
| spl24_139
| spl24_141 ),
inference(rat,[],[s102,s791]) ).
cnf(s833,plain,
( spl24_29
| spl24_135
| spl24_137
| spl24_138 ),
inference(rat,[],[s101,s782]) ).
cnf(s834,plain,
( spl24_29
| spl24_132
| spl24_133
| spl24_134 ),
inference(rat,[],[s100,s790]) ).
cnf(s835,plain,
( spl24_128
| spl24_130
| spl24_131 ),
inference(rat,[],[s99,s781,s789]) ).
cnf(s838,plain,
spl24_56,
inference(rat,[],[s19,s779]) ).
cnf(s839,plain,
~ spl24_50,
inference(rat,[],[s763,s838]) ).
cnf(s840,plain,
~ spl24_191,
inference(rat,[],[s723,s838]) ).
cnf(s841,plain,
spl24_109,
inference(rat,[],[s679,s779,s838]) ).
cnf(s842,plain,
~ spl24_200,
inference(rat,[],[s660,s838]) ).
cnf(s844,plain,
~ spl24_20,
inference(rat,[],[s81,s841]) ).
cnf(s846,plain,
~ spl24_43,
inference(rat,[],[s12,s790]) ).
cnf(s847,plain,
~ spl24_29,
inference(rat,[],[s5,s780]) ).
cnf(s848,plain,
( spl24_2
| spl24_3
| spl24_4
| spl24_5
| spl24_6
| spl24_8
| spl24_9
| spl24_10
| spl24_11
| spl24_12
| spl24_14
| spl24_15
| spl24_16
| spl24_17
| spl24_18
| spl24_21
| spl24_22
| spl24_23
| spl24_24 ),
inference(rat,[],[s3,s844,s80,s62,s44,s26]) ).
cnf(s851,plain,
~ spl24_26,
inference(rat,[],[s820,s7,s6,s773,s774,s775,s847]) ).
cnf(s852,plain,
~ spl24_206,
inference(rat,[],[s333,s851]) ).
cnf(s853,plain,
spl24_209,
inference(rat,[],[s821,s852]) ).
cnf(s854,plain,
spl24_32,
inference(rat,[],[s532,s853]) ).
cnf(s855,plain,
spl24_40,
inference(rat,[],[s475,s853]) ).
cnf(s856,plain,
spl24_124,
inference(rat,[],[s296,s853]) ).
cnf(s857,plain,
spl24_162,
inference(rat,[],[s295,s853]) ).
cnf(s858,plain,
spl24_188,
inference(rat,[],[s294,s853]) ).
cnf(s859,plain,
spl24_202,
inference(rat,[],[s293,s853]) ).
cnf(s860,plain,
spl24_204,
inference(rat,[],[s291,s853]) ).
cnf(s863,plain,
~ spl24_131,
inference(rat,[],[s403,s854]) ).
cnf(s864,plain,
~ spl24_138,
inference(rat,[],[s345,s854]) ).
cnf(s867,plain,
~ spl24_167,
inference(rat,[],[s542,s855]) ).
cnf(s870,plain,
~ spl24_134,
inference(rat,[],[s477,s856]) ).
cnf(s871,plain,
~ spl24_141,
inference(rat,[],[s459,s856]) ).
cnf(s874,plain,
spl24_78,
inference(rat,[],[s681,s854,s856]) ).
cnf(s876,plain,
~ spl24_183,
inference(rat,[],[s706,s857]) ).
cnf(s879,plain,
~ spl24_164,
inference(rat,[],[s519,s857]) ).
cnf(s880,plain,
~ spl24_155,
inference(rat,[],[s495,s857]) ).
cnf(s881,plain,
spl24_90,
inference(rat,[],[s687,s855,s857]) ).
cnf(s882,plain,
~ spl24_179,
inference(rat,[],[s645,s858]) ).
cnf(s883,plain,
~ spl24_190,
inference(rat,[],[s715,s859]) ).
cnf(s885,plain,
spl24_111,
inference(rat,[],[s691,s838,s859]) ).
cnf(s888,plain,
~ spl24_62,
inference(rat,[],[s673,s860]) ).
cnf(s890,plain,
~ spl24_21,
inference(rat,[],[s86,s874]) ).
cnf(s891,plain,
~ spl24_5,
inference(rat,[],[s38,s874]) ).
cnf(s892,plain,
~ spl24_22,
inference(rat,[],[s89,s881]) ).
cnf(s893,plain,
~ spl24_10,
inference(rat,[],[s53,s881]) ).
cnf(s894,plain,
spl24_168,
inference(rat,[],[s825,s840,s883]) ).
cnf(s895,plain,
~ spl24_24,
inference(rat,[],[s95,s885]) ).
cnf(s896,plain,
~ spl24_63,
inference(rat,[],[s22,s888]) ).
cnf(s897,plain,
~ spl24_44,
inference(rat,[],[s546,s894]) ).
cnf(s898,plain,
~ spl24_153,
inference(rat,[],[s501,s894]) ).
cnf(s899,plain,
spl24_48,
inference(rat,[],[s140,s842,s867,s864,s896]) ).
cnf(s900,plain,
~ spl24_45,
inference(rat,[],[s13,s897]) ).
cnf(s902,plain,
spl24_101,
inference(rat,[],[s692,s858,s899]) ).
cnf(s903,plain,
~ spl24_181,
inference(rat,[],[s635,s899]) ).
cnf(s905,plain,
~ spl24_23,
inference(rat,[],[s92,s902]) ).
cnf(s906,plain,
~ spl24_15,
inference(rat,[],[s68,s902]) ).
cnf(s907,plain,
spl24_180,
inference(rat,[],[s829,s898,s846,s903]) ).
cnf(s916,plain,
~ spl24_184,
inference(rat,[],[s641,s907]) ).
cnf(s918,plain,
spl24_96,
inference(rat,[],[s705,s272,s907]) ).
cnf(s921,plain,
~ spl24_14,
inference(rat,[],[s63,s918]) ).
cnf(s922,plain,
( ~ spl24_139
| spl24_106 ),
inference(rat,[],[s699,s111,s828,s9,s485,s629,s830,s708,s106,s8,s457,s595,s867,s900,s876,s846,s882,s851,s898,s880]) ).
cnf(s923,plain,
~ spl24_30,
inference(rat,[],[s464,s833,s835,s347,s428,s847,s864,s863]) ).
cnf(s924,plain,
~ spl24_31,
inference(rat,[],[s6,s923]) ).
cnf(s926,plain,
spl24_139,
inference(rat,[],[s832,s871,s839,s924]) ).
cnf(s927,plain,
~ spl24_34,
inference(rat,[],[s595,s926]) ).
cnf(s928,plain,
~ spl24_132,
inference(rat,[],[s457,s926]) ).
cnf(s931,plain,
spl24_106,
inference(rat,[],[s922,s926]) ).
cnf(s932,plain,
~ spl24_35,
inference(rat,[],[s8,s927]) ).
cnf(s933,plain,
~ spl24_92,
inference(rat,[],[s694,s271,s928]) ).
cnf(s934,plain,
spl24_133,
inference(rat,[],[s834,s870,s847,s928]) ).
cnf(s935,plain,
~ spl24_18,
inference(rat,[],[s75,s931]) ).
cnf(s936,plain,
spl24_154,
inference(rat,[],[s106,s880,s898,s851,s932]) ).
cnf(s937,plain,
~ spl24_11,
inference(rat,[],[s55,s933]) ).
cnf(s939,plain,
spl24_70,
inference(rat,[],[s756,s272,s934]) ).
cnf(s940,plain,
spl24_102,
inference(rat,[],[s700,s907,s934]) ).
cnf(s943,plain,
~ spl24_178,
inference(rat,[],[s708,s936]) ).
cnf(s945,plain,
~ spl24_163,
inference(rat,[],[s503,s936]) ).
cnf(s948,plain,
spl24_79,
inference(rat,[],[s721,s926,s936]) ).
cnf(s949,plain,
~ spl24_3,
inference(rat,[],[s30,s939]) ).
cnf(s950,plain,
~ spl24_16,
inference(rat,[],[s69,s940]) ).
cnf(s953,plain,
spl24_156,
inference(rat,[],[s830,s882,s846,s943]) ).
cnf(s954,plain,
~ spl24_94,
inference(rat,[],[s765,s894,s945]) ).
cnf(s955,plain,
~ spl24_6,
inference(rat,[],[s39,s948]) ).
cnf(s956,plain,
~ spl24_165,
inference(rat,[],[s629,s953]) ).
cnf(s958,plain,
~ spl24_36,
inference(rat,[],[s485,s953]) ).
cnf(s959,plain,
~ spl24_83,
inference(rat,[],[s697,s781,s953]) ).
cnf(s962,plain,
~ spl24_12,
inference(rat,[],[s58,s954]) ).
cnf(s963,plain,
~ spl24_37,
inference(rat,[],[s9,s958]) ).
cnf(s965,plain,
~ spl24_8,
inference(rat,[],[s46,s959]) ).
cnf(s966,plain,
spl24_135,
inference(rat,[],[s110,s879,s897,s945,s963]) ).
cnf(s967,plain,
spl24_166,
inference(rat,[],[s111,s867,s928,s956,s963]) ).
cnf(s970,plain,
~ spl24_68,
inference(rat,[],[s720,s898,s966]) ).
cnf(s973,plain,
~ spl24_142,
inference(rat,[],[s597,s966]) ).
cnf(s974,plain,
~ spl24_128,
inference(rat,[],[s465,s966]) ).
cnf(s976,plain,
~ spl24_86,
inference(rat,[],[s712,s916,s967]) ).
cnf(s979,plain,
~ spl24_157,
inference(rat,[],[s544,s967]) ).
cnf(s981,plain,
~ spl24_105,
inference(rat,[],[s690,s936,s973]) ).
cnf(s982,plain,
spl24_130,
inference(rat,[],[s835,s863,s974]) ).
cnf(s983,plain,
~ spl24_9,
inference(rat,[],[s49,s976]) ).
cnf(s986,plain,
~ spl24_17,
inference(rat,[],[s73,s981]) ).
cnf(s987,plain,
~ spl24_74,
inference(rat,[],[s685,s979,s982]) ).
cnf(s992,plain,
~ spl24_4,
inference(rat,[],[s34,s987]) ).
cnf(s993,plain,
~ spl24_2,
inference(rat,[],[s28,s970]) ).
cnf(s994,plain,
$false,
inference(rat,[],[s848,s935,s962,s937,s906,s921,s983,s965,s893,s955,s950,s949,s891,s905,s895,s993,s892,s890,s992,s986]) ).
fof(f3921,plain,
$false,
inference(avatar_sat_refutation,[],[s994]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG068+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.20 % Computer : n013.cluster.edu
% 0.11/0.20 % Model : x86_64 x86_64
% 0.11/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.20 % Memory : 8046.5625MB
% 0.11/0.20 % OS : Linux 6.8.0-71-generic
% 0.11/0.20 % CPULimit : 300
% 0.11/0.20 % WCLimit : 300
% 0.11/0.20 % DateTime : Mon Sep 28 19:23:52 UTC 2026
% 0.11/0.20 % CPUTime :
% 0.11/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.23 Running first-order theorem proving
% 0.11/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.56/0.98 % (1474109)Detected formulas, will run a generic FOF schedule.
% 2.56/0.98 % (1474120)dis-21_1_sil=8000:lcm=predicate:random_seed=3271204574:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.56/0.98 % (1474120)Refutation not found, incomplete strategy
% 2.56/0.98 % (1474120)------------------------------
% 2.56/0.98 % (1474120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.56/0.98 % (1474120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.98 % (1474120)CaDiCaL version: 2.1.3
% 2.56/0.98 % (1474120)Termination reason: Refutation not found, incomplete strategy
% 2.56/0.98 % (1474120)Time elapsed: 0.007 s
% 2.56/0.98 % (1474120)Peak memory usage: 89 MB
% 2.56/0.98 % (1474120)Instructions burned: 23 (million)
% 2.56/0.98 % (1474115)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=3449870552:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.56/0.98 % (1474117)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=891415627:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.56/0.98 % (1474118)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2778762508:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.56/0.98 % (1474116)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=1705994200:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.56/0.98 % (1474114)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=1548953607:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.56/0.98 % (1474119)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1373868904:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.56/0.98 % (1474117)Instruction limit reached!
% 2.56/0.98 % (1474117)------------------------------
% 2.56/0.98 % (1474117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.56/0.98 % (1474117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.98 % (1474117)CaDiCaL version: 2.1.3
% 2.56/0.98 % (1474117)Termination reason: Instruction limit
% 2.56/0.98 % (1474117)Termination phase: Saturation
% 2.56/0.98 % (1474117)Time elapsed: 0.053 s
% 2.56/0.98 % (1474117)Peak memory usage: 89 MB
% 2.56/0.98 % (1474117)Instructions burned: 109 (million)
% 2.56/0.98 % (1474118)Instruction limit reached!
% 2.56/0.98 % (1474118)------------------------------
% 2.56/0.98 % (1474118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.56/0.98 % (1474118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.98 % (1474118)CaDiCaL version: 2.1.3
% 2.56/0.98 % (1474118)Termination reason: Instruction limit
% 2.56/0.98 % (1474118)Termination phase: Saturation
% 2.56/0.98 % (1474118)Time elapsed: 0.055 s
% 2.56/0.98 % (1474118)Peak memory usage: 87 MB
% 2.56/0.98 % (1474118)Instructions burned: 121 (million)
% 2.56/0.98 % (1474119)Instruction limit reached!
% 2.56/0.98 % (1474119)------------------------------
% 2.56/0.98 % (1474119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.56/0.98 % (1474119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.98 % (1474119)CaDiCaL version: 2.1.3
% 2.56/0.98 % (1474119)Termination reason: Instruction limit
% 2.56/0.98 % (1474119)Termination phase: Saturation
% 2.56/0.98 % (1474119)Time elapsed: 0.077 s
% 2.56/0.98 % (1474119)Peak memory usage: 89 MB
% 2.56/0.98 % (1474119)Instructions burned: 140 (million)
% 2.56/0.98 % (1474120)------------------------------
% 2.56/0.98 % (1474120)------------------------------
% 2.56/0.98 % (1474129)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1111929516:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 2.56/0.98 % (1474128)lrs+10_1_sil=8000:sp=occurrence:random_seed=83780562:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 2.56/0.98 % (1474131)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=174278875:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 2.56/0.98 % (1474130)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1613410043:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 2.56/0.98 % (1474131)First to succeed.
% 2.56/0.98 % (1474131)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1474109"
% 2.56/0.98 % (1474129)Also succeeded, but the first one will report.
% 2.56/0.98 % (1474128)Also succeeded, but the first one will report.
% 2.56/0.98 % (1474130)Also succeeded, but the first one will report.
% 2.56/0.98 [W928 19:23:52.864333312 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864343262 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864365606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864366756 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864401322 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864401419 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864412876 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864413996 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864438119 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864440862 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864451106 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864452112 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864904667 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864938793 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864973467 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.864996343 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.865033847 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 [W928 19:23:52.865043993 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 2.56/0.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 2.56/0.98 % (1474131)Refutation found. Thanks to Tanya!
% 2.56/0.98 % SZS status Theorem for theBenchmark
% 2.56/0.98 % SZS output start Proof for theBenchmark
% See solution above
% 4.30/1.18 % (1474131)------------------------------
% 4.30/1.18 % (1474131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.30/1.18 % (1474131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.30/1.18 % (1474131)CaDiCaL version: 2.1.3
% 4.30/1.18 % (1474131)Termination reason: Refutation
% 4.30/1.18 % (1474131)Time elapsed: 0.050 s
% 4.30/1.18 % (1474131)Peak memory usage: 91 MB
% 4.30/1.18 % (1474131)Instructions burned: 165 (million)
% 4.30/1.18 % (1474131)------------------------------
% 4.30/1.18 % (1474131)------------------------------
% 4.30/1.18 % (1474109)Success in time 0.554 s
% 4.30/1.18 % Vampire exiting
%------------------------------------------------------------------------------