%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG038+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 : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:08:15 AM UTC 2026
% Result : Theorem 4.70s 1.34s
% Output : Refutation 5.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 156
% Syntax : Number of formulae : 1041 ( 145 unt; 142 def)
% Number of atoms : 3648 (1696 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 4333 (1726 ~;2083 |; 394 &)
% ( 130 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 144 ( 142 usr; 143 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e10) = e11
| op1(e10,e10) = e12
| op1(e10,e10) = e13 )
& ( op1(e10,e11) = e10
| op1(e10,e11) = e11
| op1(e10,e11) = e12
| op1(e10,e11) = e13 )
& ( op1(e10,e12) = e10
| op1(e10,e12) = e11
| op1(e10,e12) = e12
| op1(e10,e12) = e13 )
& ( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e12
| op1(e10,e13) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 )
& ( op1(e11,e11) = e10
| op1(e11,e11) = e11
| op1(e11,e11) = e12
| op1(e11,e11) = e13 )
& ( op1(e11,e12) = e10
| op1(e11,e12) = e11
| op1(e11,e12) = e12
| op1(e11,e12) = e13 )
& ( op1(e11,e13) = e10
| op1(e11,e13) = e11
| op1(e11,e13) = e12
| op1(e11,e13) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e10) = e11
| op1(e12,e10) = e12
| op1(e12,e10) = e13 )
& ( op1(e12,e11) = e10
| op1(e12,e11) = e11
| op1(e12,e11) = e12
| op1(e12,e11) = e13 )
& ( op1(e12,e12) = e10
| op1(e12,e12) = e11
| op1(e12,e12) = e12
| op1(e12,e12) = e13 )
& ( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12
| op1(e12,e13) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e10) = e11
| op1(e13,e10) = e12
| op1(e13,e10) = e13 )
& ( op1(e13,e11) = e10
| op1(e13,e11) = e11
| op1(e13,e11) = e12
| op1(e13,e11) = e13 )
& ( op1(e13,e12) = e10
| op1(e13,e12) = e11
| op1(e13,e12) = e12
| op1(e13,e12) = e13 )
& ( op1(e13,e13) = e10
| op1(e13,e13) = e11
| op1(e13,e13) = e12
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( op1(unit1,e10) = e10
& op1(e10,unit1) = e10
& op1(unit1,e11) = e11
& op1(e11,unit1) = e11
& op1(unit1,e12) = e12
& op1(e12,unit1) = e12
& op1(unit1,e13) = e13
& op1(e13,unit1) = e13
& ( unit1 = e10
| unit1 = e11
| unit1 = e12
| unit1 = e13 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e11) = e10
| op1(e10,e12) = e10
| op1(e10,e13) = e10 )
& ( op1(e10,e10) = e10
| op1(e11,e10) = e10
| op1(e12,e10) = e10
| op1(e13,e10) = e10 )
& ( op1(e10,e10) = e11
| op1(e10,e11) = e11
| op1(e10,e12) = e11
| op1(e10,e13) = e11 )
& ( op1(e10,e10) = e11
| op1(e11,e10) = e11
| op1(e12,e10) = e11
| op1(e13,e10) = e11 )
& ( op1(e10,e10) = e12
| op1(e10,e11) = e12
| op1(e10,e12) = e12
| op1(e10,e13) = e12 )
& ( op1(e10,e10) = e12
| op1(e11,e10) = e12
| op1(e12,e10) = e12
| op1(e13,e10) = e12 )
& ( op1(e10,e10) = e13
| op1(e10,e11) = e13
| op1(e10,e12) = e13
| op1(e10,e13) = e13 )
& ( op1(e10,e10) = e13
| op1(e11,e10) = e13
| op1(e12,e10) = e13
| op1(e13,e10) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e11) = e10
| op1(e11,e12) = e10
| op1(e11,e13) = e10 )
& ( op1(e10,e11) = e10
| op1(e11,e11) = e10
| op1(e12,e11) = e10
| op1(e13,e11) = e10 )
& ( op1(e11,e10) = e11
| op1(e11,e11) = e11
| op1(e11,e12) = e11
| op1(e11,e13) = e11 )
& ( op1(e10,e11) = e11
| op1(e11,e11) = e11
| op1(e12,e11) = e11
| op1(e13,e11) = e11 )
& ( op1(e11,e10) = e12
| op1(e11,e11) = e12
| op1(e11,e12) = e12
| op1(e11,e13) = e12 )
& ( op1(e10,e11) = e12
| op1(e11,e11) = e12
| op1(e12,e11) = e12
| op1(e13,e11) = e12 )
& ( op1(e11,e10) = e13
| op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e11,e13) = e13 )
& ( op1(e10,e11) = e13
| op1(e11,e11) = e13
| op1(e12,e11) = e13
| op1(e13,e11) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e11) = e10
| op1(e12,e12) = e10
| op1(e12,e13) = e10 )
& ( op1(e10,e12) = e10
| op1(e11,e12) = e10
| op1(e12,e12) = e10
| op1(e13,e12) = e10 )
& ( op1(e12,e10) = e11
| op1(e12,e11) = e11
| op1(e12,e12) = e11
| op1(e12,e13) = e11 )
& ( op1(e10,e12) = e11
| op1(e11,e12) = e11
| op1(e12,e12) = e11
| op1(e13,e12) = e11 )
& ( op1(e12,e10) = e12
| op1(e12,e11) = e12
| op1(e12,e12) = e12
| op1(e12,e13) = e12 )
& ( op1(e10,e12) = e12
| op1(e11,e12) = e12
| op1(e12,e12) = e12
| op1(e13,e12) = e12 )
& ( op1(e12,e10) = e13
| op1(e12,e11) = e13
| op1(e12,e12) = e13
| op1(e12,e13) = e13 )
& ( op1(e10,e12) = e13
| op1(e11,e12) = e13
| op1(e12,e12) = e13
| op1(e13,e12) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10 )
& ( op1(e10,e13) = e10
| op1(e11,e13) = e10
| op1(e12,e13) = e10
| op1(e13,e13) = e10 )
& ( op1(e13,e10) = e11
| op1(e13,e11) = e11
| op1(e13,e12) = e11
| op1(e13,e13) = e11 )
& ( op1(e10,e13) = e11
| op1(e11,e13) = e11
| op1(e12,e13) = e11
| op1(e13,e13) = e11 )
& ( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12
| op1(e13,e13) = e12 )
& ( op1(e10,e13) = e12
| op1(e11,e13) = e12
| op1(e12,e13) = e12
| op1(e13,e13) = e12 )
& ( op1(e13,e10) = e13
| op1(e13,e11) = e13
| op1(e13,e12) = e13
| op1(e13,e13) = e13 )
& ( op1(e10,e13) = e13
| op1(e11,e13) = e13
| op1(e12,e13) = e13
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e20) = e21
| op2(e20,e20) = e22
| op2(e20,e20) = e23 )
& ( op2(e20,e21) = e20
| op2(e20,e21) = e21
| op2(e20,e21) = e22
| op2(e20,e21) = e23 )
& ( op2(e20,e22) = e20
| op2(e20,e22) = e21
| op2(e20,e22) = e22
| op2(e20,e22) = e23 )
& ( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22
| op2(e20,e23) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e20) = e21
| op2(e21,e20) = e22
| op2(e21,e20) = e23 )
& ( op2(e21,e21) = e20
| op2(e21,e21) = e21
| op2(e21,e21) = e22
| op2(e21,e21) = e23 )
& ( op2(e21,e22) = e20
| op2(e21,e22) = e21
| op2(e21,e22) = e22
| op2(e21,e22) = e23 )
& ( op2(e21,e23) = e20
| op2(e21,e23) = e21
| op2(e21,e23) = e22
| op2(e21,e23) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e20) = e21
| op2(e22,e20) = e22
| op2(e22,e20) = e23 )
& ( op2(e22,e21) = e20
| op2(e22,e21) = e21
| op2(e22,e21) = e22
| op2(e22,e21) = e23 )
& ( op2(e22,e22) = e20
| op2(e22,e22) = e21
| op2(e22,e22) = e22
| op2(e22,e22) = e23 )
& ( op2(e22,e23) = e20
| op2(e22,e23) = e21
| op2(e22,e23) = e22
| op2(e22,e23) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e20) = e21
| op2(e23,e20) = e22
| op2(e23,e20) = e23 )
& ( op2(e23,e21) = e20
| op2(e23,e21) = e21
| op2(e23,e21) = e22
| op2(e23,e21) = e23 )
& ( op2(e23,e22) = e20
| op2(e23,e22) = e21
| op2(e23,e22) = e22
| op2(e23,e22) = e23 )
& ( op2(e23,e23) = e20
| op2(e23,e23) = e21
| op2(e23,e23) = e22
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op2(unit2,e20) = e20
& op2(e20,unit2) = e20
& op2(unit2,e21) = e21
& op2(e21,unit2) = e21
& op2(unit2,e22) = e22
& op2(e22,unit2) = e22
& op2(unit2,e23) = e23
& op2(e23,unit2) = e23
& ( unit2 = e20
| unit2 = e21
| unit2 = e22
| unit2 = e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e22) = e20
| op2(e20,e23) = e20 )
& ( op2(e20,e20) = e20
| op2(e21,e20) = e20
| op2(e22,e20) = e20
| op2(e23,e20) = e20 )
& ( op2(e20,e20) = e21
| op2(e20,e21) = e21
| op2(e20,e22) = e21
| op2(e20,e23) = e21 )
& ( op2(e20,e20) = e21
| op2(e21,e20) = e21
| op2(e22,e20) = e21
| op2(e23,e20) = e21 )
& ( op2(e20,e20) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 )
& ( op2(e20,e20) = e22
| op2(e21,e20) = e22
| op2(e22,e20) = e22
| op2(e23,e20) = e22 )
& ( op2(e20,e20) = e23
| op2(e20,e21) = e23
| op2(e20,e22) = e23
| op2(e20,e23) = e23 )
& ( op2(e20,e20) = e23
| op2(e21,e20) = e23
| op2(e22,e20) = e23
| op2(e23,e20) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e21) = e20
| op2(e21,e22) = e20
| op2(e21,e23) = e20 )
& ( op2(e20,e21) = e20
| op2(e21,e21) = e20
| op2(e22,e21) = e20
| op2(e23,e21) = e20 )
& ( op2(e21,e20) = e21
| op2(e21,e21) = e21
| op2(e21,e22) = e21
| op2(e21,e23) = e21 )
& ( op2(e20,e21) = e21
| op2(e21,e21) = e21
| op2(e22,e21) = e21
| op2(e23,e21) = e21 )
& ( op2(e21,e20) = e22
| op2(e21,e21) = e22
| op2(e21,e22) = e22
| op2(e21,e23) = e22 )
& ( op2(e20,e21) = e22
| op2(e21,e21) = e22
| op2(e22,e21) = e22
| op2(e23,e21) = e22 )
& ( op2(e21,e20) = e23
| op2(e21,e21) = e23
| op2(e21,e22) = e23
| op2(e21,e23) = e23 )
& ( op2(e20,e21) = e23
| op2(e21,e21) = e23
| op2(e22,e21) = e23
| op2(e23,e21) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e21) = e20
| op2(e22,e22) = e20
| op2(e22,e23) = e20 )
& ( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e22,e22) = e20
| op2(e23,e22) = e20 )
& ( op2(e22,e20) = e21
| op2(e22,e21) = e21
| op2(e22,e22) = e21
| op2(e22,e23) = e21 )
& ( op2(e20,e22) = e21
| op2(e21,e22) = e21
| op2(e22,e22) = e21
| op2(e23,e22) = e21 )
& ( op2(e22,e20) = e22
| op2(e22,e21) = e22
| op2(e22,e22) = e22
| op2(e22,e23) = e22 )
& ( op2(e20,e22) = e22
| op2(e21,e22) = e22
| op2(e22,e22) = e22
| op2(e23,e22) = e22 )
& ( op2(e22,e20) = e23
| op2(e22,e21) = e23
| op2(e22,e22) = e23
| op2(e22,e23) = e23 )
& ( op2(e20,e22) = e23
| op2(e21,e22) = e23
| op2(e22,e22) = e23
| op2(e23,e22) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e23) = e20 )
& ( op2(e20,e23) = e20
| op2(e21,e23) = e20
| op2(e22,e23) = e20
| op2(e23,e23) = e20 )
& ( op2(e23,e20) = e21
| op2(e23,e21) = e21
| op2(e23,e22) = e21
| op2(e23,e23) = e21 )
& ( op2(e20,e23) = e21
| op2(e21,e23) = e21
| op2(e22,e23) = e21
| op2(e23,e23) = e21 )
& ( op2(e23,e20) = e22
| op2(e23,e21) = e22
| op2(e23,e22) = e22
| op2(e23,e23) = e22 )
& ( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22
| op2(e23,e23) = e22 )
& ( op2(e23,e20) = e23
| op2(e23,e21) = e23
| op2(e23,e22) = e23
| op2(e23,e23) = e23 )
& ( op2(e20,e23) = e23
| op2(e21,e23) = e23
| op2(e22,e23) = e23
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f9,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
fof(f10,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
fof(f14,axiom,
( e10 = op1(e11,op1(e11,op1(e11,e11)))
& e12 = op1(e11,op1(e11,e11))
& e13 = op1(e11,e11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
( e20 = op2(e21,op2(e21,op2(e21,e21)))
& e22 = op2(e21,op2(e21,e21))
& e23 = op2(e21,e21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
( h1(e11) = e20
& h1(e10) = op2(e20,op2(e20,op2(e20,e20)))
& h1(e12) = op2(e20,op2(e20,e20))
& h1(e13) = op2(e20,e20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
( h2(e11) = e21
& h2(e10) = op2(e21,op2(e21,op2(e21,e21)))
& h2(e12) = op2(e21,op2(e21,e21))
& h2(e13) = op2(e21,e21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
fof(f19,axiom,
( h4(e11) = e23
& h4(e10) = op2(e23,op2(e23,op2(e23,e23)))
& h4(e12) = op2(e23,op2(e23,e23))
& h4(e13) = op2(e23,e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax19) ).
fof(f20,conjecture,
( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f21,negated_conjecture,
~ ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f20]) ).
fof(f22,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) ) )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) ) )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) ) )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) ) ) ),
inference(ennf_transformation,[],[f21]) ).
fof(f25,definition,
( ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f26,definition,
( ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f27,definition,
( ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f29,definition,
( ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f30,definition,
( ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f31,definition,
( ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f32,definition,
( ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f33,definition,
( ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f34,definition,
( ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f35,definition,
( ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f36,definition,
( ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f37,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| sP11
| sP10
| sP9 )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| sP8
| sP7
| sP6 )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| sP5
| sP4
| sP3 )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| sP2
| sP1
| sP0 ) ),
inference(definition_folding,[],[f22,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25]) ).
fof(f41,plain,
( ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ~ sP8 ),
inference(nnf_transformation,[],[f33]) ).
fof(f42,plain,
( ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ~ sP7 ),
inference(nnf_transformation,[],[f32]) ).
fof(f43,plain,
( ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) )
| ~ sP6 ),
inference(nnf_transformation,[],[f31]) ).
fof(f64,plain,
( e21 != h2(e11)
| ~ sP8 ),
inference(cnf_transformation,[],[f41]) ).
fof(f67,plain,
( e22 != h2(e12)
| ~ sP7 ),
inference(cnf_transformation,[],[f42]) ).
fof(f70,plain,
( e23 != h2(e13)
| ~ sP6 ),
inference(cnf_transformation,[],[f43]) ).
fof(f109,plain,
( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| e20 != h2(e10)
| sP8
| sP7
| sP6 ),
inference(cnf_transformation,[],[f37]) ).
fof(f114,plain,
op2(e23,e23) = h4(e13),
inference(cnf_transformation,[],[f19]) ).
fof(f122,plain,
op2(e21,e21) = h2(e13),
inference(cnf_transformation,[],[f17]) ).
fof(f123,plain,
op2(e21,op2(e21,e21)) = h2(e12),
inference(cnf_transformation,[],[f17]) ).
fof(f124,plain,
op2(e21,op2(e21,op2(e21,e21))) = h2(e10),
inference(cnf_transformation,[],[f17]) ).
fof(f125,plain,
e21 = h2(e11),
inference(cnf_transformation,[],[f17]) ).
fof(f126,plain,
op2(e20,e20) = h1(e13),
inference(cnf_transformation,[],[f16]) ).
fof(f130,plain,
e23 = op2(e21,e21),
inference(cnf_transformation,[],[f15]) ).
fof(f131,plain,
e22 = op2(e21,op2(e21,e21)),
inference(cnf_transformation,[],[f15]) ).
fof(f132,plain,
e20 = op2(e21,op2(e21,op2(e21,e21))),
inference(cnf_transformation,[],[f15]) ).
fof(f133,plain,
e13 = op1(e11,e11),
inference(cnf_transformation,[],[f14]) ).
fof(f134,plain,
e12 = op1(e11,op1(e11,e11)),
inference(cnf_transformation,[],[f14]) ).
fof(f135,plain,
e10 = op1(e11,op1(e11,op1(e11,e11))),
inference(cnf_transformation,[],[f14]) ).
fof(f160,plain,
e22 != e23,
inference(cnf_transformation,[],[f10]) ).
fof(f161,plain,
e21 != e23,
inference(cnf_transformation,[],[f10]) ).
fof(f162,plain,
e21 != e22,
inference(cnf_transformation,[],[f10]) ).
fof(f163,plain,
e20 != e23,
inference(cnf_transformation,[],[f10]) ).
fof(f164,plain,
e20 != e22,
inference(cnf_transformation,[],[f10]) ).
fof(f165,plain,
e20 != e21,
inference(cnf_transformation,[],[f10]) ).
fof(f166,plain,
e12 != e13,
inference(cnf_transformation,[],[f9]) ).
fof(f167,plain,
e11 != e13,
inference(cnf_transformation,[],[f9]) ).
fof(f168,plain,
e11 != e12,
inference(cnf_transformation,[],[f9]) ).
fof(f169,plain,
e10 != e13,
inference(cnf_transformation,[],[f9]) ).
fof(f170,plain,
e10 != e12,
inference(cnf_transformation,[],[f9]) ).
fof(f171,plain,
e10 != e11,
inference(cnf_transformation,[],[f9]) ).
fof(f271,plain,
( e22 = op2(e23,e20)
| e22 = op2(e23,e21)
| e22 = op2(e23,e22)
| e22 = op2(e23,e23) ),
inference(cnf_transformation,[],[f6]) ).
fof(f272,plain,
( e21 = op2(e20,e23)
| e21 = op2(e21,e23)
| e21 = op2(e22,e23)
| e21 = op2(e23,e23) ),
inference(cnf_transformation,[],[f6]) ).
fof(f273,plain,
( e21 = op2(e23,e20)
| e21 = op2(e23,e21)
| e21 = op2(e23,e22)
| e21 = op2(e23,e23) ),
inference(cnf_transformation,[],[f6]) ).
fof(f275,plain,
( e20 = op2(e23,e20)
| e20 = op2(e23,e21)
| e20 = op2(e23,e22)
| e20 = op2(e23,e23) ),
inference(cnf_transformation,[],[f6]) ).
fof(f276,plain,
( e23 = op2(e20,e22)
| e23 = op2(e21,e22)
| e23 = op2(e22,e22)
| e23 = op2(e23,e22) ),
inference(cnf_transformation,[],[f6]) ).
fof(f280,plain,
( e21 = op2(e20,e22)
| e21 = op2(e21,e22)
| e21 = op2(e22,e22)
| e21 = op2(e23,e22) ),
inference(cnf_transformation,[],[f6]) ).
fof(f283,plain,
( e20 = op2(e22,e20)
| e20 = op2(e22,e21)
| e20 = op2(e22,e22)
| e20 = op2(e22,e23) ),
inference(cnf_transformation,[],[f6]) ).
fof(f286,plain,
( e22 = op2(e20,e21)
| e22 = op2(e21,e21)
| e22 = op2(e22,e21)
| e22 = op2(e23,e21) ),
inference(cnf_transformation,[],[f6]) ).
fof(f292,plain,
( op2(e20,e20) = e23
| e23 = op2(e21,e20)
| e23 = op2(e22,e20)
| e23 = op2(e23,e20) ),
inference(cnf_transformation,[],[f6]) ).
fof(f293,plain,
( op2(e20,e20) = e23
| e23 = op2(e20,e21)
| e23 = op2(e20,e22)
| e23 = op2(e20,e23) ),
inference(cnf_transformation,[],[f6]) ).
fof(f300,plain,
( e20 = unit2
| e21 = unit2
| e22 = unit2
| e23 = unit2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f301,plain,
e23 = op2(e23,unit2),
inference(cnf_transformation,[],[f5]) ).
fof(f302,plain,
e23 = op2(unit2,e23),
inference(cnf_transformation,[],[f5]) ).
fof(f303,plain,
e22 = op2(e22,unit2),
inference(cnf_transformation,[],[f5]) ).
fof(f304,plain,
e22 = op2(unit2,e22),
inference(cnf_transformation,[],[f5]) ).
fof(f305,plain,
e21 = op2(e21,unit2),
inference(cnf_transformation,[],[f5]) ).
fof(f306,plain,
e21 = op2(unit2,e21),
inference(cnf_transformation,[],[f5]) ).
fof(f308,plain,
e20 = op2(unit2,e20),
inference(cnf_transformation,[],[f5]) ).
fof(f309,plain,
( e20 = op2(e23,e23)
| e21 = op2(e23,e23)
| e22 = op2(e23,e23)
| e23 = op2(e23,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f328,plain,
( e12 = op1(e13,e10)
| e12 = op1(e13,e11)
| e12 = op1(e13,e12)
| e12 = op1(e13,e13) ),
inference(cnf_transformation,[],[f3]) ).
fof(f329,plain,
( e11 = op1(e10,e13)
| e11 = op1(e11,e13)
| e11 = op1(e12,e13)
| e11 = op1(e13,e13) ),
inference(cnf_transformation,[],[f3]) ).
fof(f330,plain,
( e11 = op1(e13,e10)
| e11 = op1(e13,e11)
| e11 = op1(e13,e12)
| e11 = op1(e13,e13) ),
inference(cnf_transformation,[],[f3]) ).
fof(f331,plain,
( e10 = op1(e10,e13)
| e10 = op1(e11,e13)
| e10 = op1(e12,e13)
| e10 = op1(e13,e13) ),
inference(cnf_transformation,[],[f3]) ).
fof(f332,plain,
( e10 = op1(e13,e10)
| e10 = op1(e13,e11)
| e10 = op1(e13,e12)
| e10 = op1(e13,e13) ),
inference(cnf_transformation,[],[f3]) ).
fof(f333,plain,
( e13 = op1(e10,e12)
| e13 = op1(e11,e12)
| e13 = op1(e12,e12)
| e13 = op1(e13,e12) ),
inference(cnf_transformation,[],[f3]) ).
fof(f334,plain,
( e13 = op1(e12,e10)
| e13 = op1(e12,e11)
| e13 = op1(e12,e12)
| e13 = op1(e12,e13) ),
inference(cnf_transformation,[],[f3]) ).
fof(f337,plain,
( e11 = op1(e10,e12)
| e11 = op1(e11,e12)
| e11 = op1(e12,e12)
| e11 = op1(e13,e12) ),
inference(cnf_transformation,[],[f3]) ).
fof(f338,plain,
( e11 = op1(e12,e10)
| e11 = op1(e12,e11)
| e11 = op1(e12,e12)
| e11 = op1(e12,e13) ),
inference(cnf_transformation,[],[f3]) ).
fof(f340,plain,
( e10 = op1(e12,e10)
| e10 = op1(e12,e11)
| e10 = op1(e12,e12)
| e10 = op1(e12,e13) ),
inference(cnf_transformation,[],[f3]) ).
fof(f343,plain,
( e12 = op1(e10,e11)
| e12 = op1(e11,e11)
| e12 = op1(e12,e11)
| e12 = op1(e13,e11) ),
inference(cnf_transformation,[],[f3]) ).
fof(f346,plain,
( e11 = op1(e11,e10)
| e11 = op1(e11,e11)
| e11 = op1(e11,e12)
| e11 = op1(e11,e13) ),
inference(cnf_transformation,[],[f3]) ).
fof(f347,plain,
( e10 = op1(e10,e11)
| e10 = op1(e11,e11)
| e10 = op1(e12,e11)
| e10 = op1(e13,e11) ),
inference(cnf_transformation,[],[f3]) ).
fof(f349,plain,
( op1(e10,e10) = e13
| e13 = op1(e11,e10)
| e13 = op1(e12,e10)
| e13 = op1(e13,e10) ),
inference(cnf_transformation,[],[f3]) ).
fof(f350,plain,
( op1(e10,e10) = e13
| e13 = op1(e10,e11)
| e13 = op1(e10,e12)
| e13 = op1(e10,e13) ),
inference(cnf_transformation,[],[f3]) ).
fof(f357,plain,
( e10 = unit1
| e11 = unit1
| e12 = unit1
| e13 = unit1 ),
inference(cnf_transformation,[],[f2]) ).
fof(f358,plain,
e13 = op1(e13,unit1),
inference(cnf_transformation,[],[f2]) ).
fof(f359,plain,
e13 = op1(unit1,e13),
inference(cnf_transformation,[],[f2]) ).
fof(f360,plain,
e12 = op1(e12,unit1),
inference(cnf_transformation,[],[f2]) ).
fof(f361,plain,
e12 = op1(unit1,e12),
inference(cnf_transformation,[],[f2]) ).
fof(f362,plain,
e11 = op1(e11,unit1),
inference(cnf_transformation,[],[f2]) ).
fof(f363,plain,
e11 = op1(unit1,e11),
inference(cnf_transformation,[],[f2]) ).
fof(f364,plain,
e10 = op1(e10,unit1),
inference(cnf_transformation,[],[f2]) ).
fof(f366,plain,
( e10 = op1(e13,e13)
| e11 = op1(e13,e13)
| e12 = op1(e13,e13)
| e13 = op1(e13,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f383,definition,
( spl12_1
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition]) ).
fof(f385,plain,
( e13 = op1(e13,e13)
| ~ spl12_1 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f387,definition,
( spl12_2
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition]) ).
fof(f389,plain,
( e12 = op1(e13,e13)
| ~ spl12_2 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f391,definition,
( spl12_3
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_3])],[avatar_definition]) ).
fof(f393,plain,
( e11 = op1(e13,e13)
| ~ spl12_3 ),
inference(avatar_component_clause,[],[f391]) ).
fof(f395,definition,
( spl12_4
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_4])],[avatar_definition]) ).
fof(f397,plain,
( e10 = op1(e13,e13)
| ~ spl12_4 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f398,plain,
( spl12_1
| spl12_2
| spl12_3
| spl12_4 ),
inference(avatar_split_clause,[],[f366,f395,f391,f387,f383]) ).
fof(f400,definition,
( spl12_5
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_5])],[avatar_definition]) ).
fof(f402,plain,
( e13 = op1(e13,e12)
| ~ spl12_5 ),
inference(avatar_component_clause,[],[f400]) ).
fof(f404,definition,
( spl12_6
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_6])],[avatar_definition]) ).
fof(f406,plain,
( e12 = op1(e13,e12)
| ~ spl12_6 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f408,definition,
( spl12_7
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_7])],[avatar_definition]) ).
fof(f410,plain,
( e11 = op1(e13,e12)
| ~ spl12_7 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f412,definition,
( spl12_8
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_8])],[avatar_definition]) ).
fof(f414,plain,
( e10 = op1(e13,e12)
| ~ spl12_8 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f421,definition,
( spl12_10
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_10])],[avatar_definition]) ).
fof(f423,plain,
( e12 = op1(e13,e11)
| ~ spl12_10 ),
inference(avatar_component_clause,[],[f421]) ).
fof(f425,definition,
( spl12_11
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_11])],[avatar_definition]) ).
fof(f427,plain,
( e11 = op1(e13,e11)
| ~ spl12_11 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f429,definition,
( spl12_12
<=> e10 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_12])],[avatar_definition]) ).
fof(f431,plain,
( e10 = op1(e13,e11)
| ~ spl12_12 ),
inference(avatar_component_clause,[],[f429]) ).
fof(f434,definition,
( spl12_13
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_13])],[avatar_definition]) ).
fof(f436,plain,
( e13 = op1(e13,e10)
| ~ spl12_13 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f438,definition,
( spl12_14
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_14])],[avatar_definition]) ).
fof(f440,plain,
( e12 = op1(e13,e10)
| ~ spl12_14 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f442,definition,
( spl12_15
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_15])],[avatar_definition]) ).
fof(f444,plain,
( e11 = op1(e13,e10)
| ~ spl12_15 ),
inference(avatar_component_clause,[],[f442]) ).
fof(f446,definition,
( spl12_16
<=> e10 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_16])],[avatar_definition]) ).
fof(f448,plain,
( e10 = op1(e13,e10)
| ~ spl12_16 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f451,definition,
( spl12_17
<=> e13 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_17])],[avatar_definition]) ).
fof(f453,plain,
( e13 = op1(e12,e13)
| ~ spl12_17 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f459,definition,
( spl12_19
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_19])],[avatar_definition]) ).
fof(f461,plain,
( e11 = op1(e12,e13)
| ~ spl12_19 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f463,definition,
( spl12_20
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_20])],[avatar_definition]) ).
fof(f465,plain,
( e10 = op1(e12,e13)
| ~ spl12_20 ),
inference(avatar_component_clause,[],[f463]) ).
fof(f468,definition,
( spl12_21
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_21])],[avatar_definition]) ).
fof(f470,plain,
( e13 = op1(e12,e12)
| ~ spl12_21 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f476,definition,
( spl12_23
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_23])],[avatar_definition]) ).
fof(f478,plain,
( e11 = op1(e12,e12)
| ~ spl12_23 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f480,definition,
( spl12_24
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_24])],[avatar_definition]) ).
fof(f482,plain,
( e10 = op1(e12,e12)
| ~ spl12_24 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f485,definition,
( spl12_25
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_25])],[avatar_definition]) ).
fof(f487,plain,
( e13 = op1(e12,e11)
| ~ spl12_25 ),
inference(avatar_component_clause,[],[f485]) ).
fof(f489,definition,
( spl12_26
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_26])],[avatar_definition]) ).
fof(f491,plain,
( e12 = op1(e12,e11)
| ~ spl12_26 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f493,definition,
( spl12_27
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_27])],[avatar_definition]) ).
fof(f495,plain,
( e11 = op1(e12,e11)
| ~ spl12_27 ),
inference(avatar_component_clause,[],[f493]) ).
fof(f497,definition,
( spl12_28
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_28])],[avatar_definition]) ).
fof(f499,plain,
( e10 = op1(e12,e11)
| ~ spl12_28 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f502,definition,
( spl12_29
<=> e13 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_29])],[avatar_definition]) ).
fof(f504,plain,
( e13 = op1(e12,e10)
| ~ spl12_29 ),
inference(avatar_component_clause,[],[f502]) ).
fof(f506,definition,
( spl12_30
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_30])],[avatar_definition]) ).
fof(f508,plain,
( e12 = op1(e12,e10)
| ~ spl12_30 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f510,definition,
( spl12_31
<=> e11 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_31])],[avatar_definition]) ).
fof(f512,plain,
( e11 = op1(e12,e10)
| ~ spl12_31 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f514,definition,
( spl12_32
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_32])],[avatar_definition]) ).
fof(f516,plain,
( e10 = op1(e12,e10)
| ~ spl12_32 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f523,definition,
( spl12_34
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_34])],[avatar_definition]) ).
fof(f524,plain,
( e12 != op1(e11,e13)
| spl12_34 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f525,plain,
( e12 = op1(e11,e13)
| ~ spl12_34 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f527,definition,
( spl12_35
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_35])],[avatar_definition]) ).
fof(f529,plain,
( e11 = op1(e11,e13)
| ~ spl12_35 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f531,definition,
( spl12_36
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_36])],[avatar_definition]) ).
fof(f533,plain,
( e10 = op1(e11,e13)
| ~ spl12_36 ),
inference(avatar_component_clause,[],[f531]) ).
fof(f536,definition,
( spl12_37
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_37])],[avatar_definition]) ).
fof(f538,plain,
( e13 = op1(e11,e12)
| ~ spl12_37 ),
inference(avatar_component_clause,[],[f536]) ).
fof(f544,definition,
( spl12_39
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_39])],[avatar_definition]) ).
fof(f546,plain,
( e11 = op1(e11,e12)
| ~ spl12_39 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f548,definition,
( spl12_40
<=> e10 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_40])],[avatar_definition]) ).
fof(f550,plain,
( e10 = op1(e11,e12)
| ~ spl12_40 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f553,definition,
( spl12_41
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_41])],[avatar_definition]) ).
fof(f555,plain,
( e13 = op1(e11,e11)
| ~ spl12_41 ),
inference(avatar_component_clause,[],[f553]) ).
fof(f557,definition,
( spl12_42
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_42])],[avatar_definition]) ).
fof(f559,plain,
( e12 = op1(e11,e11)
| ~ spl12_42 ),
inference(avatar_component_clause,[],[f557]) ).
fof(f561,definition,
( spl12_43
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_43])],[avatar_definition]) ).
fof(f563,plain,
( e11 = op1(e11,e11)
| ~ spl12_43 ),
inference(avatar_component_clause,[],[f561]) ).
fof(f565,definition,
( spl12_44
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_44])],[avatar_definition]) ).
fof(f567,plain,
( e10 = op1(e11,e11)
| ~ spl12_44 ),
inference(avatar_component_clause,[],[f565]) ).
fof(f570,definition,
( spl12_45
<=> e13 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl12_45])],[avatar_definition]) ).
fof(f572,plain,
( e13 = op1(e11,e10)
| ~ spl12_45 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f578,definition,
( spl12_47
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl12_47])],[avatar_definition]) ).
fof(f580,plain,
( e11 = op1(e11,e10)
| ~ spl12_47 ),
inference(avatar_component_clause,[],[f578]) ).
fof(f587,definition,
( spl12_49
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_49])],[avatar_definition]) ).
fof(f589,plain,
( e13 = op1(e10,e13)
| ~ spl12_49 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f595,definition,
( spl12_51
<=> e11 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_51])],[avatar_definition]) ).
fof(f597,plain,
( e11 = op1(e10,e13)
| ~ spl12_51 ),
inference(avatar_component_clause,[],[f595]) ).
fof(f599,definition,
( spl12_52
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_52])],[avatar_definition]) ).
fof(f601,plain,
( e10 = op1(e10,e13)
| ~ spl12_52 ),
inference(avatar_component_clause,[],[f599]) ).
fof(f604,definition,
( spl12_53
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_53])],[avatar_definition]) ).
fof(f606,plain,
( e13 = op1(e10,e12)
| ~ spl12_53 ),
inference(avatar_component_clause,[],[f604]) ).
fof(f608,definition,
( spl12_54
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_54])],[avatar_definition]) ).
fof(f610,plain,
( e12 = op1(e10,e12)
| ~ spl12_54 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f612,definition,
( spl12_55
<=> e11 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_55])],[avatar_definition]) ).
fof(f614,plain,
( e11 = op1(e10,e12)
| ~ spl12_55 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f621,definition,
( spl12_57
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_57])],[avatar_definition]) ).
fof(f623,plain,
( e13 = op1(e10,e11)
| ~ spl12_57 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f625,definition,
( spl12_58
<=> e12 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_58])],[avatar_definition]) ).
fof(f627,plain,
( e12 = op1(e10,e11)
| ~ spl12_58 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f629,definition,
( spl12_59
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_59])],[avatar_definition]) ).
fof(f631,plain,
( e11 = op1(e10,e11)
| ~ spl12_59 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f633,definition,
( spl12_60
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_60])],[avatar_definition]) ).
fof(f635,plain,
( e10 = op1(e10,e11)
| ~ spl12_60 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f638,definition,
( spl12_61
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl12_61])],[avatar_definition]) ).
fof(f640,plain,
( op1(e10,e10) = e13
| ~ spl12_61 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f650,definition,
( spl12_64
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl12_64])],[avatar_definition]) ).
fof(f652,plain,
( e10 = op1(e10,e10)
| ~ spl12_64 ),
inference(avatar_component_clause,[],[f650]) ).
fof(f655,definition,
( spl12_65
<=> e13 = unit1 ),
introduced(definition,[new_symbols(definition,[spl12_65])],[avatar_definition]) ).
fof(f657,plain,
( e13 = unit1
| ~ spl12_65 ),
inference(avatar_component_clause,[],[f655]) ).
fof(f659,definition,
( spl12_66
<=> e12 = unit1 ),
introduced(definition,[new_symbols(definition,[spl12_66])],[avatar_definition]) ).
fof(f661,plain,
( e12 = unit1
| ~ spl12_66 ),
inference(avatar_component_clause,[],[f659]) ).
fof(f663,definition,
( spl12_67
<=> e11 = unit1 ),
introduced(definition,[new_symbols(definition,[spl12_67])],[avatar_definition]) ).
fof(f665,plain,
( e11 = unit1
| ~ spl12_67 ),
inference(avatar_component_clause,[],[f663]) ).
fof(f667,definition,
( spl12_68
<=> e10 = unit1 ),
introduced(definition,[new_symbols(definition,[spl12_68])],[avatar_definition]) ).
fof(f669,plain,
( e10 = unit1
| ~ spl12_68 ),
inference(avatar_component_clause,[],[f667]) ).
fof(f670,plain,
( spl12_65
| spl12_66
| spl12_67
| spl12_68 ),
inference(avatar_split_clause,[],[f357,f667,f663,f659,f655]) ).
fof(f674,plain,
( spl12_2
| spl12_6
| spl12_10
| spl12_14 ),
inference(avatar_split_clause,[],[f328,f438,f421,f404,f387]) ).
fof(f675,plain,
( spl12_3
| spl12_19
| spl12_35
| spl12_51 ),
inference(avatar_split_clause,[],[f329,f595,f527,f459,f391]) ).
fof(f676,plain,
( spl12_3
| spl12_7
| spl12_11
| spl12_15 ),
inference(avatar_split_clause,[],[f330,f442,f425,f408,f391]) ).
fof(f677,plain,
( spl12_4
| spl12_20
| spl12_36
| spl12_52 ),
inference(avatar_split_clause,[],[f331,f599,f531,f463,f395]) ).
fof(f678,plain,
( spl12_4
| spl12_8
| spl12_12
| spl12_16 ),
inference(avatar_split_clause,[],[f332,f446,f429,f412,f395]) ).
fof(f679,plain,
( spl12_5
| spl12_21
| spl12_37
| spl12_53 ),
inference(avatar_split_clause,[],[f333,f604,f536,f468,f400]) ).
fof(f680,plain,
( spl12_17
| spl12_21
| spl12_25
| spl12_29 ),
inference(avatar_split_clause,[],[f334,f502,f485,f468,f451]) ).
fof(f683,plain,
( spl12_7
| spl12_23
| spl12_39
| spl12_55 ),
inference(avatar_split_clause,[],[f337,f612,f544,f476,f408]) ).
fof(f684,plain,
( spl12_19
| spl12_23
| spl12_27
| spl12_31 ),
inference(avatar_split_clause,[],[f338,f510,f493,f476,f459]) ).
fof(f686,plain,
( spl12_20
| spl12_24
| spl12_28
| spl12_32 ),
inference(avatar_split_clause,[],[f340,f514,f497,f480,f463]) ).
fof(f689,plain,
( spl12_10
| spl12_26
| spl12_42
| spl12_58 ),
inference(avatar_split_clause,[],[f343,f625,f557,f489,f421]) ).
fof(f692,plain,
( spl12_35
| spl12_39
| spl12_43
| spl12_47 ),
inference(avatar_split_clause,[],[f346,f578,f561,f544,f527]) ).
fof(f693,plain,
( spl12_12
| spl12_28
| spl12_44
| spl12_60 ),
inference(avatar_split_clause,[],[f347,f633,f565,f497,f429]) ).
fof(f695,plain,
( spl12_13
| spl12_29
| spl12_45
| spl12_61 ),
inference(avatar_split_clause,[],[f349,f638,f570,f502,f434]) ).
fof(f696,plain,
( spl12_49
| spl12_53
| spl12_57
| spl12_61 ),
inference(avatar_split_clause,[],[f350,f638,f621,f604,f587]) ).
fof(f704,definition,
( spl12_69
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_69])],[avatar_definition]) ).
fof(f706,plain,
( e23 = op2(e23,e23)
| ~ spl12_69 ),
inference(avatar_component_clause,[],[f704]) ).
fof(f708,definition,
( spl12_70
<=> e22 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_70])],[avatar_definition]) ).
fof(f710,plain,
( e22 = op2(e23,e23)
| ~ spl12_70 ),
inference(avatar_component_clause,[],[f708]) ).
fof(f712,definition,
( spl12_71
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_71])],[avatar_definition]) ).
fof(f714,plain,
( e21 = op2(e23,e23)
| ~ spl12_71 ),
inference(avatar_component_clause,[],[f712]) ).
fof(f716,definition,
( spl12_72
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_72])],[avatar_definition]) ).
fof(f718,plain,
( e20 = op2(e23,e23)
| ~ spl12_72 ),
inference(avatar_component_clause,[],[f716]) ).
fof(f719,plain,
( spl12_69
| spl12_70
| spl12_71
| spl12_72 ),
inference(avatar_split_clause,[],[f309,f716,f712,f708,f704]) ).
fof(f721,definition,
( spl12_73
<=> e23 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_73])],[avatar_definition]) ).
fof(f723,plain,
( e23 = op2(e23,e22)
| ~ spl12_73 ),
inference(avatar_component_clause,[],[f721]) ).
fof(f725,definition,
( spl12_74
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_74])],[avatar_definition]) ).
fof(f727,plain,
( e22 = op2(e23,e22)
| ~ spl12_74 ),
inference(avatar_component_clause,[],[f725]) ).
fof(f729,definition,
( spl12_75
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_75])],[avatar_definition]) ).
fof(f731,plain,
( e21 = op2(e23,e22)
| ~ spl12_75 ),
inference(avatar_component_clause,[],[f729]) ).
fof(f733,definition,
( spl12_76
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_76])],[avatar_definition]) ).
fof(f735,plain,
( e20 = op2(e23,e22)
| ~ spl12_76 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f742,definition,
( spl12_78
<=> e22 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_78])],[avatar_definition]) ).
fof(f744,plain,
( e22 = op2(e23,e21)
| ~ spl12_78 ),
inference(avatar_component_clause,[],[f742]) ).
fof(f746,definition,
( spl12_79
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_79])],[avatar_definition]) ).
fof(f748,plain,
( e21 = op2(e23,e21)
| ~ spl12_79 ),
inference(avatar_component_clause,[],[f746]) ).
fof(f750,definition,
( spl12_80
<=> e20 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_80])],[avatar_definition]) ).
fof(f752,plain,
( e20 = op2(e23,e21)
| ~ spl12_80 ),
inference(avatar_component_clause,[],[f750]) ).
fof(f755,definition,
( spl12_81
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_81])],[avatar_definition]) ).
fof(f757,plain,
( e23 = op2(e23,e20)
| ~ spl12_81 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f759,definition,
( spl12_82
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_82])],[avatar_definition]) ).
fof(f761,plain,
( e22 = op2(e23,e20)
| ~ spl12_82 ),
inference(avatar_component_clause,[],[f759]) ).
fof(f763,definition,
( spl12_83
<=> e21 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_83])],[avatar_definition]) ).
fof(f765,plain,
( e21 = op2(e23,e20)
| ~ spl12_83 ),
inference(avatar_component_clause,[],[f763]) ).
fof(f767,definition,
( spl12_84
<=> e20 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_84])],[avatar_definition]) ).
fof(f769,plain,
( e20 = op2(e23,e20)
| ~ spl12_84 ),
inference(avatar_component_clause,[],[f767]) ).
fof(f780,definition,
( spl12_87
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_87])],[avatar_definition]) ).
fof(f782,plain,
( e21 = op2(e22,e23)
| ~ spl12_87 ),
inference(avatar_component_clause,[],[f780]) ).
fof(f784,definition,
( spl12_88
<=> e20 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_88])],[avatar_definition]) ).
fof(f786,plain,
( e20 = op2(e22,e23)
| ~ spl12_88 ),
inference(avatar_component_clause,[],[f784]) ).
fof(f789,definition,
( spl12_89
<=> e23 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_89])],[avatar_definition]) ).
fof(f791,plain,
( e23 = op2(e22,e22)
| ~ spl12_89 ),
inference(avatar_component_clause,[],[f789]) ).
fof(f797,definition,
( spl12_91
<=> e21 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_91])],[avatar_definition]) ).
fof(f799,plain,
( e21 = op2(e22,e22)
| ~ spl12_91 ),
inference(avatar_component_clause,[],[f797]) ).
fof(f801,definition,
( spl12_92
<=> e20 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_92])],[avatar_definition]) ).
fof(f803,plain,
( e20 = op2(e22,e22)
| ~ spl12_92 ),
inference(avatar_component_clause,[],[f801]) ).
fof(f810,definition,
( spl12_94
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_94])],[avatar_definition]) ).
fof(f812,plain,
( e22 = op2(e22,e21)
| ~ spl12_94 ),
inference(avatar_component_clause,[],[f810]) ).
fof(f818,definition,
( spl12_96
<=> e20 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_96])],[avatar_definition]) ).
fof(f820,plain,
( e20 = op2(e22,e21)
| ~ spl12_96 ),
inference(avatar_component_clause,[],[f818]) ).
fof(f823,definition,
( spl12_97
<=> e23 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_97])],[avatar_definition]) ).
fof(f825,plain,
( e23 = op2(e22,e20)
| ~ spl12_97 ),
inference(avatar_component_clause,[],[f823]) ).
fof(f827,definition,
( spl12_98
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_98])],[avatar_definition]) ).
fof(f829,plain,
( e22 = op2(e22,e20)
| ~ spl12_98 ),
inference(avatar_component_clause,[],[f827]) ).
fof(f831,definition,
( spl12_99
<=> e21 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_99])],[avatar_definition]) ).
fof(f833,plain,
( e21 = op2(e22,e20)
| ~ spl12_99 ),
inference(avatar_component_clause,[],[f831]) ).
fof(f835,definition,
( spl12_100
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_100])],[avatar_definition]) ).
fof(f837,plain,
( e20 = op2(e22,e20)
| ~ spl12_100 ),
inference(avatar_component_clause,[],[f835]) ).
fof(f844,definition,
( spl12_102
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_102])],[avatar_definition]) ).
fof(f845,plain,
( e22 != op2(e21,e23)
| spl12_102 ),
inference(avatar_component_clause,[],[f844]) ).
fof(f846,plain,
( e22 = op2(e21,e23)
| ~ spl12_102 ),
inference(avatar_component_clause,[],[f844]) ).
fof(f848,definition,
( spl12_103
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_103])],[avatar_definition]) ).
fof(f850,plain,
( e21 = op2(e21,e23)
| ~ spl12_103 ),
inference(avatar_component_clause,[],[f848]) ).
fof(f857,definition,
( spl12_105
<=> e23 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_105])],[avatar_definition]) ).
fof(f859,plain,
( e23 = op2(e21,e22)
| ~ spl12_105 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f865,definition,
( spl12_107
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_107])],[avatar_definition]) ).
fof(f867,plain,
( e21 = op2(e21,e22)
| ~ spl12_107 ),
inference(avatar_component_clause,[],[f865]) ).
fof(f869,definition,
( spl12_108
<=> e20 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_108])],[avatar_definition]) ).
fof(f871,plain,
( e20 = op2(e21,e22)
| ~ spl12_108 ),
inference(avatar_component_clause,[],[f869]) ).
fof(f874,definition,
( spl12_109
<=> e23 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_109])],[avatar_definition]) ).
fof(f876,plain,
( e23 = op2(e21,e21)
| ~ spl12_109 ),
inference(avatar_component_clause,[],[f874]) ).
fof(f878,definition,
( spl12_110
<=> e22 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_110])],[avatar_definition]) ).
fof(f880,plain,
( e22 = op2(e21,e21)
| ~ spl12_110 ),
inference(avatar_component_clause,[],[f878]) ).
fof(f891,definition,
( spl12_113
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_113])],[avatar_definition]) ).
fof(f893,plain,
( e23 = op2(e21,e20)
| ~ spl12_113 ),
inference(avatar_component_clause,[],[f891]) ).
fof(f899,definition,
( spl12_115
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_115])],[avatar_definition]) ).
fof(f901,plain,
( e21 = op2(e21,e20)
| ~ spl12_115 ),
inference(avatar_component_clause,[],[f899]) ).
fof(f908,definition,
( spl12_117
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_117])],[avatar_definition]) ).
fof(f916,definition,
( spl12_119
<=> e21 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_119])],[avatar_definition]) ).
fof(f918,plain,
( e21 = op2(e20,e23)
| ~ spl12_119 ),
inference(avatar_component_clause,[],[f916]) ).
fof(f925,definition,
( spl12_121
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_121])],[avatar_definition]) ).
fof(f927,plain,
( e23 = op2(e20,e22)
| ~ spl12_121 ),
inference(avatar_component_clause,[],[f925]) ).
fof(f929,definition,
( spl12_122
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_122])],[avatar_definition]) ).
fof(f931,plain,
( e22 = op2(e20,e22)
| ~ spl12_122 ),
inference(avatar_component_clause,[],[f929]) ).
fof(f933,definition,
( spl12_123
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_123])],[avatar_definition]) ).
fof(f935,plain,
( e21 = op2(e20,e22)
| ~ spl12_123 ),
inference(avatar_component_clause,[],[f933]) ).
fof(f942,definition,
( spl12_125
<=> e23 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_125])],[avatar_definition]) ).
fof(f944,plain,
( e23 = op2(e20,e21)
| ~ spl12_125 ),
inference(avatar_component_clause,[],[f942]) ).
fof(f946,definition,
( spl12_126
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_126])],[avatar_definition]) ).
fof(f948,plain,
( e22 = op2(e20,e21)
| ~ spl12_126 ),
inference(avatar_component_clause,[],[f946]) ).
fof(f950,definition,
( spl12_127
<=> e21 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_127])],[avatar_definition]) ).
fof(f952,plain,
( e21 = op2(e20,e21)
| ~ spl12_127 ),
inference(avatar_component_clause,[],[f950]) ).
fof(f959,definition,
( spl12_129
<=> op2(e20,e20) = e23 ),
introduced(definition,[new_symbols(definition,[spl12_129])],[avatar_definition]) ).
fof(f961,plain,
( op2(e20,e20) = e23
| ~ spl12_129 ),
inference(avatar_component_clause,[],[f959]) ).
fof(f971,definition,
( spl12_132
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl12_132])],[avatar_definition]) ).
fof(f973,plain,
( e20 = op2(e20,e20)
| ~ spl12_132 ),
inference(avatar_component_clause,[],[f971]) ).
fof(f976,definition,
( spl12_133
<=> e23 = unit2 ),
introduced(definition,[new_symbols(definition,[spl12_133])],[avatar_definition]) ).
fof(f978,plain,
( e23 = unit2
| ~ spl12_133 ),
inference(avatar_component_clause,[],[f976]) ).
fof(f980,definition,
( spl12_134
<=> e22 = unit2 ),
introduced(definition,[new_symbols(definition,[spl12_134])],[avatar_definition]) ).
fof(f982,plain,
( e22 = unit2
| ~ spl12_134 ),
inference(avatar_component_clause,[],[f980]) ).
fof(f984,definition,
( spl12_135
<=> e21 = unit2 ),
introduced(definition,[new_symbols(definition,[spl12_135])],[avatar_definition]) ).
fof(f986,plain,
( e21 = unit2
| ~ spl12_135 ),
inference(avatar_component_clause,[],[f984]) ).
fof(f988,definition,
( spl12_136
<=> e20 = unit2 ),
introduced(definition,[new_symbols(definition,[spl12_136])],[avatar_definition]) ).
fof(f990,plain,
( e20 = unit2
| ~ spl12_136 ),
inference(avatar_component_clause,[],[f988]) ).
fof(f991,plain,
( spl12_133
| spl12_134
| spl12_135
| spl12_136 ),
inference(avatar_split_clause,[],[f300,f988,f984,f980,f976]) ).
fof(f995,plain,
( spl12_70
| spl12_74
| spl12_78
| spl12_82 ),
inference(avatar_split_clause,[],[f271,f759,f742,f725,f708]) ).
fof(f996,plain,
( spl12_71
| spl12_87
| spl12_103
| spl12_119 ),
inference(avatar_split_clause,[],[f272,f916,f848,f780,f712]) ).
fof(f997,plain,
( spl12_71
| spl12_75
| spl12_79
| spl12_83 ),
inference(avatar_split_clause,[],[f273,f763,f746,f729,f712]) ).
fof(f999,plain,
( spl12_72
| spl12_76
| spl12_80
| spl12_84 ),
inference(avatar_split_clause,[],[f275,f767,f750,f733,f716]) ).
fof(f1000,plain,
( spl12_73
| spl12_89
| spl12_105
| spl12_121 ),
inference(avatar_split_clause,[],[f276,f925,f857,f789,f721]) ).
fof(f1004,plain,
( spl12_75
| spl12_91
| spl12_107
| spl12_123 ),
inference(avatar_split_clause,[],[f280,f933,f865,f797,f729]) ).
fof(f1007,plain,
( spl12_88
| spl12_92
| spl12_96
| spl12_100 ),
inference(avatar_split_clause,[],[f283,f835,f818,f801,f784]) ).
fof(f1010,plain,
( spl12_78
| spl12_94
| spl12_110
| spl12_126 ),
inference(avatar_split_clause,[],[f286,f946,f878,f810,f742]) ).
fof(f1016,plain,
( spl12_81
| spl12_97
| spl12_113
| spl12_129 ),
inference(avatar_split_clause,[],[f292,f959,f891,f823,f755]) ).
fof(f1017,plain,
( spl12_117
| spl12_121
| spl12_125
| spl12_129 ),
inference(avatar_split_clause,[],[f293,f959,f942,f925,f908]) ).
fof(f1032,plain,
spl12_41,
inference(avatar_split_clause,[],[f133,f553]) ).
fof(f1033,plain,
e10 = op1(e11,e12),
inference(forward_demodulation,[],[f135,f134]) ).
fof(f1034,plain,
spl12_109,
inference(avatar_split_clause,[],[f130,f874]) ).
fof(f1035,plain,
e20 = op2(e21,e22),
inference(forward_demodulation,[],[f132,f131]) ).
fof(f1038,plain,
e22 = h2(e12),
inference(forward_demodulation,[],[f123,f131]) ).
fof(f1039,plain,
op2(e21,e22) = h2(e10),
inference(forward_demodulation,[],[f124,f131]) ).
fof(f1055,plain,
( h2(op1(e10,e11)) != op2(h2(e10),e21)
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| e20 != h2(e10)
| sP8
| sP7
| sP6 ),
inference(forward_demodulation,[],[f109,f125]) ).
fof(f1181,definition,
( spl12_161
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl12_161])],[avatar_definition]) ).
fof(f1185,definition,
( spl12_162
<=> e23 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl12_162])],[avatar_definition]) ).
fof(f1186,plain,
( e23 = h2(e13)
| ~ spl12_162 ),
inference(avatar_component_clause,[],[f1185]) ).
fof(f1188,plain,
( ~ spl12_161
| ~ spl12_162 ),
inference(avatar_split_clause,[],[f70,f1185,f1181]) ).
fof(f1201,definition,
( spl12_165
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl12_165])],[avatar_definition]) ).
fof(f1210,definition,
( spl12_167
<=> e22 = h2(e12) ),
introduced(definition,[new_symbols(definition,[spl12_167])],[avatar_definition]) ).
fof(f1211,plain,
( e22 = h2(e12)
| ~ spl12_167 ),
inference(avatar_component_clause,[],[f1210]) ).
fof(f1213,plain,
( ~ spl12_165
| ~ spl12_167 ),
inference(avatar_split_clause,[],[f67,f1210,f1201]) ).
fof(f1221,definition,
( spl12_169
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl12_169])],[avatar_definition]) ).
fof(f1234,plain,
~ sP8,
inference(forward_subsumption_resolution,[],[f64,f125]) ).
fof(f1300,plain,
spl12_40,
inference(avatar_split_clause,[],[f1033,f548]) ).
fof(f1301,plain,
spl12_108,
inference(avatar_split_clause,[],[f1035,f869]) ).
fof(f1303,plain,
spl12_167,
inference(avatar_split_clause,[],[f1038,f1210]) ).
fof(f1317,plain,
( h2(op1(e11,e10)) != op2(e21,h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),e21)
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| e20 != h2(e10)
| sP8
| sP7
| sP6 ),
inference(forward_demodulation,[],[f1055,f125]) ).
fof(f1324,plain,
~ spl12_169,
inference(avatar_split_clause,[],[f1234,f1221]) ).
fof(f1336,plain,
( op2(e21,e21) != h2(op1(e11,e11))
| h2(op1(e11,e10)) != op2(e21,h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),e21)
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| e20 != h2(e10)
| sP8
| sP7
| sP6 ),
inference(forward_demodulation,[],[f1317,f125]) ).
fof(f1352,plain,
( h2(e13) != h2(op1(e11,e11))
| h2(op1(e11,e10)) != op2(e21,h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),e21)
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| e20 != h2(e10)
| sP8
| sP7
| sP6 ),
inference(forward_demodulation,[],[f1336,f122]) ).
fof(f1368,plain,
( h2(op1(e11,e12)) != op2(e21,h2(e12))
| h2(e13) != h2(op1(e11,e11))
| h2(op1(e11,e10)) != op2(e21,h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),e21)
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| e20 != h2(e10)
| sP8
| sP7
| sP6 ),
inference(forward_demodulation,[],[f1352,f125]) ).
fof(f1384,plain,
( h2(op1(e11,e13)) != op2(e21,h2(e13))
| h2(op1(e11,e12)) != op2(e21,h2(e12))
| h2(e13) != h2(op1(e11,e11))
| h2(op1(e11,e10)) != op2(e21,h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),e21)
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| e20 != h2(e10)
| sP8
| sP7
| sP6 ),
inference(forward_demodulation,[],[f1368,f125]) ).
fof(f1400,plain,
( h2(op1(e12,e11)) != op2(h2(e12),e21)
| h2(op1(e11,e13)) != op2(e21,h2(e13))
| h2(op1(e11,e12)) != op2(e21,h2(e12))
| h2(e13) != h2(op1(e11,e11))
| h2(op1(e11,e10)) != op2(e21,h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),e21)
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| e20 != h2(e10)
| sP8
| sP7
| sP6 ),
inference(forward_demodulation,[],[f1384,f125]) ).
fof(f1416,plain,
( h2(op1(e13,e11)) != op2(h2(e13),e21)
| h2(op1(e12,e11)) != op2(h2(e12),e21)
| h2(op1(e11,e13)) != op2(e21,h2(e13))
| h2(op1(e11,e12)) != op2(e21,h2(e12))
| h2(e13) != h2(op1(e11,e11))
| h2(op1(e11,e10)) != op2(e21,h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),e21)
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| e20 != h2(e10)
| sP8
| sP7
| sP6 ),
inference(forward_demodulation,[],[f1400,f125]) ).
fof(f1434,definition,
( spl12_186
<=> h2(op1(e13,e13)) = op2(h2(e13),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_186])],[avatar_definition]) ).
fof(f1436,plain,
( h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| spl12_186 ),
inference(avatar_component_clause,[],[f1434]) ).
fof(f1438,definition,
( spl12_187
<=> h2(op1(e13,e12)) = op2(h2(e13),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_187])],[avatar_definition]) ).
fof(f1440,plain,
( h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| spl12_187 ),
inference(avatar_component_clause,[],[f1438]) ).
fof(f1442,definition,
( spl12_188
<=> h2(op1(e13,e10)) = op2(h2(e13),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_188])],[avatar_definition]) ).
fof(f1444,plain,
( h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| spl12_188 ),
inference(avatar_component_clause,[],[f1442]) ).
fof(f1446,definition,
( spl12_189
<=> h2(op1(e12,e13)) = op2(h2(e12),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_189])],[avatar_definition]) ).
fof(f1448,plain,
( h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| spl12_189 ),
inference(avatar_component_clause,[],[f1446]) ).
fof(f1450,definition,
( spl12_190
<=> h2(op1(e12,e12)) = op2(h2(e12),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_190])],[avatar_definition]) ).
fof(f1452,plain,
( h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| spl12_190 ),
inference(avatar_component_clause,[],[f1450]) ).
fof(f1454,definition,
( spl12_191
<=> h2(op1(e12,e10)) = op2(h2(e12),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_191])],[avatar_definition]) ).
fof(f1455,plain,
( h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
| ~ spl12_191 ),
inference(avatar_component_clause,[],[f1454]) ).
fof(f1456,plain,
( h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| spl12_191 ),
inference(avatar_component_clause,[],[f1454]) ).
fof(f1458,definition,
( spl12_192
<=> h2(op1(e10,e13)) = op2(h2(e10),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_192])],[avatar_definition]) ).
fof(f1460,plain,
( h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| spl12_192 ),
inference(avatar_component_clause,[],[f1458]) ).
fof(f1462,definition,
( spl12_193
<=> h2(op1(e10,e12)) = op2(h2(e10),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_193])],[avatar_definition]) ).
fof(f1464,plain,
( h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| spl12_193 ),
inference(avatar_component_clause,[],[f1462]) ).
fof(f1466,definition,
( spl12_194
<=> h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_194])],[avatar_definition]) ).
fof(f1468,plain,
( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| spl12_194 ),
inference(avatar_component_clause,[],[f1466]) ).
fof(f1470,definition,
( spl12_195
<=> h2(op1(e10,e11)) = op2(h2(e10),e21) ),
introduced(definition,[new_symbols(definition,[spl12_195])],[avatar_definition]) ).
fof(f1472,plain,
( h2(op1(e10,e11)) != op2(h2(e10),e21)
| spl12_195 ),
inference(avatar_component_clause,[],[f1470]) ).
fof(f1474,definition,
( spl12_196
<=> h2(op1(e11,e10)) = op2(e21,h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_196])],[avatar_definition]) ).
fof(f1476,plain,
( h2(op1(e11,e10)) != op2(e21,h2(e10))
| spl12_196 ),
inference(avatar_component_clause,[],[f1474]) ).
fof(f1478,definition,
( spl12_197
<=> h2(e13) = h2(op1(e11,e11)) ),
introduced(definition,[new_symbols(definition,[spl12_197])],[avatar_definition]) ).
fof(f1480,plain,
( h2(e13) != h2(op1(e11,e11))
| spl12_197 ),
inference(avatar_component_clause,[],[f1478]) ).
fof(f1482,definition,
( spl12_198
<=> h2(op1(e11,e12)) = op2(e21,h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_198])],[avatar_definition]) ).
fof(f1484,plain,
( h2(op1(e11,e12)) != op2(e21,h2(e12))
| spl12_198 ),
inference(avatar_component_clause,[],[f1482]) ).
fof(f1486,definition,
( spl12_199
<=> h2(op1(e11,e13)) = op2(e21,h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_199])],[avatar_definition]) ).
fof(f1488,plain,
( h2(op1(e11,e13)) != op2(e21,h2(e13))
| spl12_199 ),
inference(avatar_component_clause,[],[f1486]) ).
fof(f1490,definition,
( spl12_200
<=> h2(op1(e12,e11)) = op2(h2(e12),e21) ),
introduced(definition,[new_symbols(definition,[spl12_200])],[avatar_definition]) ).
fof(f1492,plain,
( h2(op1(e12,e11)) != op2(h2(e12),e21)
| spl12_200 ),
inference(avatar_component_clause,[],[f1490]) ).
fof(f1494,definition,
( spl12_201
<=> h2(op1(e13,e11)) = op2(h2(e13),e21) ),
introduced(definition,[new_symbols(definition,[spl12_201])],[avatar_definition]) ).
fof(f1496,plain,
( h2(op1(e13,e11)) != op2(h2(e13),e21)
| spl12_201 ),
inference(avatar_component_clause,[],[f1494]) ).
fof(f1505,definition,
( spl12_203
<=> e20 = h2(e10) ),
introduced(definition,[new_symbols(definition,[spl12_203])],[avatar_definition]) ).
fof(f1506,plain,
( e20 = h2(e10)
| ~ spl12_203 ),
inference(avatar_component_clause,[],[f1505]) ).
fof(f1507,plain,
( e20 != h2(e10)
| spl12_203 ),
inference(avatar_component_clause,[],[f1505]) ).
fof(f1508,plain,
( spl12_161
| spl12_165
| spl12_169
| ~ spl12_203
| ~ spl12_186
| ~ spl12_187
| ~ spl12_188
| ~ spl12_189
| ~ spl12_190
| ~ spl12_191
| ~ spl12_192
| ~ spl12_193
| ~ spl12_194
| ~ spl12_195
| ~ spl12_196
| ~ spl12_197
| ~ spl12_198
| ~ spl12_199
| ~ spl12_200
| ~ spl12_201 ),
inference(avatar_split_clause,[],[f1416,f1494,f1490,f1486,f1482,f1478,f1474,f1470,f1466,f1462,f1458,f1454,f1450,f1446,f1442,f1438,f1434,f1505,f1221,f1201,f1181]) ).
fof(f1526,definition,
( spl12_204
<=> e20 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl12_204])],[avatar_definition]) ).
fof(f1527,plain,
( e20 = h4(e13)
| ~ spl12_204 ),
inference(avatar_component_clause,[],[f1526]) ).
fof(f1686,definition,
( spl12_242
<=> e20 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl12_242])],[avatar_definition]) ).
fof(f1687,plain,
( e20 = h1(e13)
| ~ spl12_242 ),
inference(avatar_component_clause,[],[f1686]) ).
fof(f1816,plain,
( e11 = op1(e11,e12)
| ~ spl12_66 ),
inference(superposition,[],[f362,f661]) ).
fof(f1817,plain,
( e10 = e11
| ~ spl12_40
| ~ spl12_66 ),
inference(forward_demodulation,[],[f1816,f550]) ).
fof(f1818,plain,
( $false
| ~ spl12_40
| ~ spl12_66 ),
inference(forward_subsumption_resolution,[],[f1817,f171]) ).
fof(f1819,plain,
( ~ spl12_40
| ~ spl12_66 ),
inference(avatar_contradiction_clause,[],[f1818]) ).
fof(f1824,plain,
( e11 = op1(e11,e11)
| ~ spl12_67 ),
inference(superposition,[],[f362,f665]) ).
fof(f1827,plain,
( spl12_43
| ~ spl12_67 ),
inference(avatar_split_clause,[],[f1824,f663,f561]) ).
fof(f1838,plain,
( e13 = op1(e13,e10)
| ~ spl12_68 ),
inference(superposition,[],[f358,f669]) ).
fof(f1839,plain,
( e13 = op1(e10,e13)
| ~ spl12_68 ),
inference(superposition,[],[f359,f669]) ).
fof(f1840,plain,
( e12 = op1(e12,e10)
| ~ spl12_68 ),
inference(superposition,[],[f360,f669]) ).
fof(f1841,plain,
( e12 = op1(e10,e12)
| ~ spl12_68 ),
inference(superposition,[],[f361,f669]) ).
fof(f1847,plain,
( spl12_54
| ~ spl12_68 ),
inference(avatar_split_clause,[],[f1841,f667,f608]) ).
fof(f1848,plain,
( spl12_30
| ~ spl12_68 ),
inference(avatar_split_clause,[],[f1840,f667,f506]) ).
fof(f1850,plain,
( e12 = e13
| ~ spl12_14
| ~ spl12_68 ),
inference(forward_demodulation,[],[f1838,f440]) ).
fof(f1853,plain,
( $false
| ~ spl12_14
| ~ spl12_68 ),
inference(forward_subsumption_resolution,[],[f1850,f166]) ).
fof(f1854,plain,
( ~ spl12_14
| ~ spl12_68 ),
inference(avatar_contradiction_clause,[],[f1853]) ).
fof(f1857,plain,
( e11 = e13
| ~ spl12_51
| ~ spl12_68 ),
inference(forward_demodulation,[],[f1839,f597]) ).
fof(f1858,plain,
( e11 = e13
| ~ spl12_15
| ~ spl12_68 ),
inference(forward_demodulation,[],[f1838,f444]) ).
fof(f1859,plain,
( $false
| ~ spl12_51
| ~ spl12_68 ),
inference(forward_subsumption_resolution,[],[f1857,f167]) ).
fof(f1860,plain,
( ~ spl12_51
| ~ spl12_68 ),
inference(avatar_contradiction_clause,[],[f1859]) ).
fof(f1861,plain,
( $false
| ~ spl12_15
| ~ spl12_68 ),
inference(forward_subsumption_resolution,[],[f1858,f167]) ).
fof(f1862,plain,
( ~ spl12_15
| ~ spl12_68 ),
inference(avatar_contradiction_clause,[],[f1861]) ).
fof(f1866,plain,
( e10 = e13
| ~ spl12_52
| ~ spl12_68 ),
inference(forward_demodulation,[],[f1839,f601]) ).
fof(f1868,plain,
( e10 = e13
| ~ spl12_16
| ~ spl12_68 ),
inference(forward_demodulation,[],[f1838,f448]) ).
fof(f1869,plain,
( $false
| ~ spl12_52
| ~ spl12_68 ),
inference(forward_subsumption_resolution,[],[f1866,f169]) ).
fof(f1870,plain,
( ~ spl12_52
| ~ spl12_68 ),
inference(avatar_contradiction_clause,[],[f1869]) ).
fof(f1871,plain,
( $false
| ~ spl12_16
| ~ spl12_68 ),
inference(forward_subsumption_resolution,[],[f1868,f169]) ).
fof(f1872,plain,
( ~ spl12_16
| ~ spl12_68 ),
inference(avatar_contradiction_clause,[],[f1871]) ).
fof(f1879,plain,
( e11 = op1(e10,e11)
| ~ spl12_68 ),
inference(superposition,[],[f363,f669]) ).
fof(f1880,plain,
( spl12_59
| ~ spl12_68 ),
inference(avatar_split_clause,[],[f1879,f667,f629]) ).
fof(f1881,plain,
( e10 = op1(e10,e10)
| ~ spl12_68 ),
inference(superposition,[],[f364,f669]) ).
fof(f1882,plain,
( spl12_64
| ~ spl12_68 ),
inference(avatar_split_clause,[],[f1881,f667,f650]) ).
fof(f1885,plain,
( e12 = e13
| ~ spl12_5
| ~ spl12_6 ),
inference(superposition,[],[f406,f402]) ).
fof(f1889,plain,
( $false
| ~ spl12_5
| ~ spl12_6 ),
inference(forward_subsumption_resolution,[],[f1885,f166]) ).
fof(f1890,plain,
( ~ spl12_5
| ~ spl12_6 ),
inference(avatar_contradiction_clause,[],[f1889]) ).
fof(f1892,plain,
( e11 = e12
| ~ spl12_6
| ~ spl12_7 ),
inference(superposition,[],[f410,f406]) ).
fof(f1896,plain,
( $false
| ~ spl12_6
| ~ spl12_7 ),
inference(forward_subsumption_resolution,[],[f1892,f168]) ).
fof(f1897,plain,
( ~ spl12_6
| ~ spl12_7 ),
inference(avatar_contradiction_clause,[],[f1896]) ).
fof(f1908,plain,
( e10 = e11
| ~ spl12_11
| ~ spl12_12 ),
inference(superposition,[],[f427,f431]) ).
fof(f1909,plain,
( $false
| ~ spl12_11
| ~ spl12_12 ),
inference(forward_subsumption_resolution,[],[f1908,f171]) ).
fof(f1910,plain,
( ~ spl12_11
| ~ spl12_12 ),
inference(avatar_contradiction_clause,[],[f1909]) ).
fof(f1957,plain,
( e11 = e12
| ~ spl12_26
| ~ spl12_27 ),
inference(superposition,[],[f495,f491]) ).
fof(f1961,plain,
( $false
| ~ spl12_26
| ~ spl12_27 ),
inference(forward_subsumption_resolution,[],[f1957,f168]) ).
fof(f1962,plain,
( ~ spl12_26
| ~ spl12_27 ),
inference(avatar_contradiction_clause,[],[f1961]) ).
fof(f1971,plain,
( e12 = e13
| ~ spl12_29
| ~ spl12_30 ),
inference(superposition,[],[f508,f504]) ).
fof(f1975,plain,
( $false
| ~ spl12_29
| ~ spl12_30 ),
inference(forward_subsumption_resolution,[],[f1971,f166]) ).
fof(f1976,plain,
( ~ spl12_29
| ~ spl12_30 ),
inference(avatar_contradiction_clause,[],[f1975]) ).
fof(f1981,plain,
( e10 = e12
| ~ spl12_30
| ~ spl12_32 ),
inference(superposition,[],[f516,f508]) ).
fof(f1985,plain,
( $false
| ~ spl12_30
| ~ spl12_32 ),
inference(forward_subsumption_resolution,[],[f1981,f170]) ).
fof(f1986,plain,
( ~ spl12_30
| ~ spl12_32 ),
inference(avatar_contradiction_clause,[],[f1985]) ).
fof(f1988,plain,
( e11 = e13
| ~ spl12_17
| ~ spl12_19 ),
inference(forward_demodulation,[],[f453,f461]) ).
fof(f1997,plain,
( $false
| ~ spl12_17
| ~ spl12_19 ),
inference(forward_subsumption_resolution,[],[f1988,f167]) ).
fof(f1998,plain,
( ~ spl12_17
| ~ spl12_19 ),
inference(avatar_contradiction_clause,[],[f1997]) ).
fof(f2043,plain,
( e11 = e13
| ~ spl12_1
| ~ spl12_3 ),
inference(superposition,[],[f393,f385]) ).
fof(f2048,plain,
( $false
| ~ spl12_1
| ~ spl12_3 ),
inference(forward_subsumption_resolution,[],[f2043,f167]) ).
fof(f2049,plain,
( ~ spl12_1
| ~ spl12_3 ),
inference(avatar_contradiction_clause,[],[f2048]) ).
fof(f2054,plain,
( e10 = e13
| ~ spl12_1
| ~ spl12_4 ),
inference(superposition,[],[f397,f385]) ).
fof(f2059,plain,
( $false
| ~ spl12_1
| ~ spl12_4 ),
inference(forward_subsumption_resolution,[],[f2054,f169]) ).
fof(f2060,plain,
( ~ spl12_1
| ~ spl12_4 ),
inference(avatar_contradiction_clause,[],[f2059]) ).
fof(f2071,plain,
( e10 = e12
| ~ spl12_10
| ~ spl12_12 ),
inference(superposition,[],[f431,f423]) ).
fof(f2075,plain,
( $false
| ~ spl12_10
| ~ spl12_12 ),
inference(forward_subsumption_resolution,[],[f2071,f170]) ).
fof(f2076,plain,
( ~ spl12_10
| ~ spl12_12 ),
inference(avatar_contradiction_clause,[],[f2075]) ).
fof(f2083,plain,
( e10 = e11
| ~ spl12_19
| ~ spl12_20 ),
inference(superposition,[],[f465,f461]) ).
fof(f2084,plain,
( e10 = e11
| ~ spl12_19
| ~ spl12_20 ),
inference(superposition,[],[f461,f465]) ).
fof(f2086,plain,
( $false
| ~ spl12_19
| ~ spl12_20 ),
inference(forward_subsumption_resolution,[],[f2084,f171]) ).
fof(f2087,plain,
( ~ spl12_19
| ~ spl12_20 ),
inference(avatar_contradiction_clause,[],[f2086]) ).
fof(f2088,plain,
( $false
| ~ spl12_19
| ~ spl12_20 ),
inference(forward_subsumption_resolution,[],[f2083,f171]) ).
fof(f2089,plain,
( ~ spl12_19
| ~ spl12_20 ),
inference(avatar_contradiction_clause,[],[f2088]) ).
fof(f2093,plain,
( e10 = e13
| ~ spl12_25
| ~ spl12_28 ),
inference(superposition,[],[f487,f499]) ).
fof(f2094,plain,
( $false
| ~ spl12_25
| ~ spl12_28 ),
inference(forward_subsumption_resolution,[],[f2093,f169]) ).
fof(f2095,plain,
( ~ spl12_25
| ~ spl12_28 ),
inference(avatar_contradiction_clause,[],[f2094]) ).
fof(f2104,plain,
( e11 = e12
| ~ spl12_34
| ~ spl12_35 ),
inference(superposition,[],[f529,f525]) ).
fof(f2108,plain,
( $false
| ~ spl12_34
| ~ spl12_35 ),
inference(forward_subsumption_resolution,[],[f2104,f168]) ).
fof(f2109,plain,
( ~ spl12_34
| ~ spl12_35 ),
inference(avatar_contradiction_clause,[],[f2108]) ).
fof(f2111,plain,
( e10 = e12
| ~ spl12_34
| ~ spl12_36 ),
inference(superposition,[],[f533,f525]) ).
fof(f2115,plain,
( $false
| ~ spl12_34
| ~ spl12_36 ),
inference(forward_subsumption_resolution,[],[f2111,f170]) ).
fof(f2116,plain,
( ~ spl12_34
| ~ spl12_36 ),
inference(avatar_contradiction_clause,[],[f2115]) ).
fof(f2119,plain,
( e12 = e13
| ~ spl12_41
| ~ spl12_42 ),
inference(superposition,[],[f559,f555]) ).
fof(f2123,plain,
( $false
| ~ spl12_41
| ~ spl12_42 ),
inference(forward_subsumption_resolution,[],[f2119,f166]) ).
fof(f2124,plain,
( ~ spl12_41
| ~ spl12_42 ),
inference(avatar_contradiction_clause,[],[f2123]) ).
fof(f2125,plain,
( e10 = e12
| ~ spl12_26
| ~ spl12_28 ),
inference(forward_demodulation,[],[f491,f499]) ).
fof(f2128,plain,
( $false
| ~ spl12_26
| ~ spl12_28 ),
inference(forward_subsumption_resolution,[],[f2125,f170]) ).
fof(f2129,plain,
( ~ spl12_26
| ~ spl12_28 ),
inference(avatar_contradiction_clause,[],[f2128]) ).
fof(f2135,plain,
( e11 = e12
| ~ spl12_58
| ~ spl12_59 ),
inference(forward_demodulation,[],[f627,f631]) ).
fof(f2137,plain,
( $false
| ~ spl12_58
| ~ spl12_59 ),
inference(forward_subsumption_resolution,[],[f2135,f168]) ).
fof(f2138,plain,
( ~ spl12_58
| ~ spl12_59 ),
inference(avatar_contradiction_clause,[],[f2137]) ).
fof(f2144,plain,
( e10 = e12
| ~ spl12_2
| ~ spl12_4 ),
inference(superposition,[],[f397,f389]) ).
fof(f2149,plain,
( $false
| ~ spl12_2
| ~ spl12_4 ),
inference(forward_subsumption_resolution,[],[f2144,f170]) ).
fof(f2150,plain,
( ~ spl12_2
| ~ spl12_4 ),
inference(avatar_contradiction_clause,[],[f2149]) ).
fof(f2155,plain,
( e10 = e13
| ~ spl12_21
| ~ spl12_24 ),
inference(superposition,[],[f482,f470]) ).
fof(f2159,plain,
( $false
| ~ spl12_21
| ~ spl12_24 ),
inference(forward_subsumption_resolution,[],[f2155,f169]) ).
fof(f2160,plain,
( ~ spl12_21
| ~ spl12_24 ),
inference(avatar_contradiction_clause,[],[f2159]) ).
fof(f2167,plain,
( e11 = e13
| ~ spl12_45
| ~ spl12_47 ),
inference(superposition,[],[f580,f572]) ).
fof(f2171,plain,
( $false
| ~ spl12_45
| ~ spl12_47 ),
inference(forward_subsumption_resolution,[],[f2167,f167]) ).
fof(f2172,plain,
( ~ spl12_45
| ~ spl12_47 ),
inference(avatar_contradiction_clause,[],[f2171]) ).
fof(f2175,plain,
( e12 = e13
| ~ spl12_53
| ~ spl12_54 ),
inference(superposition,[],[f610,f606]) ).
fof(f2179,plain,
( $false
| ~ spl12_53
| ~ spl12_54 ),
inference(forward_subsumption_resolution,[],[f2175,f166]) ).
fof(f2180,plain,
( ~ spl12_53
| ~ spl12_54 ),
inference(avatar_contradiction_clause,[],[f2179]) ).
fof(f2181,plain,
( e10 = e13
| ~ spl12_37
| ~ spl12_40 ),
inference(forward_demodulation,[],[f538,f550]) ).
fof(f2183,plain,
( $false
| ~ spl12_37
| ~ spl12_40 ),
inference(forward_subsumption_resolution,[],[f2181,f169]) ).
fof(f2184,plain,
( ~ spl12_37
| ~ spl12_40 ),
inference(avatar_contradiction_clause,[],[f2183]) ).
fof(f2196,plain,
( e11 = e12
| ~ spl12_54
| ~ spl12_55 ),
inference(superposition,[],[f614,f610]) ).
fof(f2200,plain,
( $false
| ~ spl12_54
| ~ spl12_55 ),
inference(forward_subsumption_resolution,[],[f2196,f168]) ).
fof(f2201,plain,
( ~ spl12_54
| ~ spl12_55 ),
inference(avatar_contradiction_clause,[],[f2200]) ).
fof(f2210,plain,
( e11 = e13
| ~ spl12_57
| ~ spl12_59 ),
inference(superposition,[],[f631,f623]) ).
fof(f2214,plain,
( $false
| ~ spl12_57
| ~ spl12_59 ),
inference(forward_subsumption_resolution,[],[f2210,f167]) ).
fof(f2215,plain,
( ~ spl12_57
| ~ spl12_59 ),
inference(avatar_contradiction_clause,[],[f2214]) ).
fof(f2218,plain,
( e10 = e11
| ~ spl12_59
| ~ spl12_60 ),
inference(superposition,[],[f635,f631]) ).
fof(f2222,plain,
( $false
| ~ spl12_59
| ~ spl12_60 ),
inference(forward_subsumption_resolution,[],[f2218,f171]) ).
fof(f2223,plain,
( ~ spl12_59
| ~ spl12_60 ),
inference(avatar_contradiction_clause,[],[f2222]) ).
fof(f2225,plain,
( e10 = e13
| ~ spl12_61
| ~ spl12_64 ),
inference(superposition,[],[f652,f640]) ).
fof(f2229,plain,
( $false
| ~ spl12_61
| ~ spl12_64 ),
inference(forward_subsumption_resolution,[],[f2225,f169]) ).
fof(f2230,plain,
( ~ spl12_61
| ~ spl12_64 ),
inference(avatar_contradiction_clause,[],[f2229]) ).
fof(f2234,plain,
( e22 = e23
| ~ spl12_73
| ~ spl12_74 ),
inference(superposition,[],[f727,f723]) ).
fof(f2238,plain,
( $false
| ~ spl12_73
| ~ spl12_74 ),
inference(forward_subsumption_resolution,[],[f2234,f160]) ).
fof(f2239,plain,
( ~ spl12_73
| ~ spl12_74 ),
inference(avatar_contradiction_clause,[],[f2238]) ).
fof(f2247,plain,
( e22 = op2(e21,e22)
| ~ spl12_135 ),
inference(superposition,[],[f304,f986]) ).
fof(f2256,plain,
( e20 = e22
| ~ spl12_108
| ~ spl12_135 ),
inference(forward_demodulation,[],[f2247,f871]) ).
fof(f2260,plain,
( $false
| ~ spl12_108
| ~ spl12_135 ),
inference(forward_subsumption_resolution,[],[f2256,f164]) ).
fof(f2261,plain,
( ~ spl12_108
| ~ spl12_135 ),
inference(avatar_contradiction_clause,[],[f2260]) ).
fof(f2282,plain,
( e21 = op2(e21,e22)
| ~ spl12_134 ),
inference(superposition,[],[f305,f982]) ).
fof(f2290,plain,
( e20 = e21
| ~ spl12_108
| ~ spl12_134 ),
inference(forward_demodulation,[],[f2282,f871]) ).
fof(f2291,plain,
( $false
| ~ spl12_108
| ~ spl12_134 ),
inference(forward_subsumption_resolution,[],[f2290,f165]) ).
fof(f2292,plain,
( ~ spl12_108
| ~ spl12_134 ),
inference(avatar_contradiction_clause,[],[f2291]) ).
fof(f2294,plain,
( e23 = op2(e23,e20)
| ~ spl12_136 ),
inference(superposition,[],[f301,f990]) ).
fof(f2296,plain,
( e22 = op2(e22,e20)
| ~ spl12_136 ),
inference(superposition,[],[f303,f990]) ).
fof(f2297,plain,
( e22 = op2(e20,e22)
| ~ spl12_136 ),
inference(superposition,[],[f304,f990]) ).
fof(f2298,plain,
( e21 = op2(e21,e20)
| ~ spl12_136 ),
inference(superposition,[],[f305,f990]) ).
fof(f2299,plain,
( e21 = op2(e20,e21)
| ~ spl12_136 ),
inference(superposition,[],[f306,f990]) ).
fof(f2301,plain,
( e20 = op2(e20,e20)
| ~ spl12_136 ),
inference(superposition,[],[f308,f990]) ).
fof(f2304,plain,
( spl12_132
| ~ spl12_136 ),
inference(avatar_split_clause,[],[f2301,f988,f971]) ).
fof(f2305,plain,
( spl12_127
| ~ spl12_136 ),
inference(avatar_split_clause,[],[f2299,f988,f950]) ).
fof(f2306,plain,
( spl12_115
| ~ spl12_136 ),
inference(avatar_split_clause,[],[f2298,f988,f899]) ).
fof(f2307,plain,
( spl12_122
| ~ spl12_136 ),
inference(avatar_split_clause,[],[f2297,f988,f929]) ).
fof(f2308,plain,
( spl12_98
| ~ spl12_136 ),
inference(avatar_split_clause,[],[f2296,f988,f827]) ).
fof(f2310,plain,
( e22 = e23
| ~ spl12_82
| ~ spl12_136 ),
inference(forward_demodulation,[],[f2294,f761]) ).
fof(f2313,plain,
( $false
| ~ spl12_82
| ~ spl12_136 ),
inference(forward_subsumption_resolution,[],[f2310,f160]) ).
fof(f2314,plain,
( ~ spl12_82
| ~ spl12_136 ),
inference(avatar_contradiction_clause,[],[f2313]) ).
fof(f2329,plain,
( e21 = e22
| ~ spl12_78
| ~ spl12_79 ),
inference(superposition,[],[f744,f748]) ).
fof(f2330,plain,
( $false
| ~ spl12_78
| ~ spl12_79 ),
inference(forward_subsumption_resolution,[],[f2329,f162]) ).
fof(f2331,plain,
( ~ spl12_78
| ~ spl12_79 ),
inference(avatar_contradiction_clause,[],[f2330]) ).
fof(f2335,plain,
( e20 = e21
| ~ spl12_79
| ~ spl12_80 ),
inference(superposition,[],[f752,f748]) ).
fof(f2339,plain,
( $false
| ~ spl12_79
| ~ spl12_80 ),
inference(forward_subsumption_resolution,[],[f2335,f165]) ).
fof(f2340,plain,
( ~ spl12_79
| ~ spl12_80 ),
inference(avatar_contradiction_clause,[],[f2339]) ).
fof(f2381,plain,
( e23 = op2(e23,e20)
| ~ spl12_136 ),
inference(superposition,[],[f301,f990]) ).
fof(f2382,plain,
( e23 = op2(e20,e23)
| ~ spl12_136 ),
inference(superposition,[],[f302,f990]) ).
fof(f2391,plain,
( e21 = e23
| ~ spl12_119
| ~ spl12_136 ),
inference(forward_demodulation,[],[f2382,f918]) ).
fof(f2392,plain,
( e21 = e23
| ~ spl12_83
| ~ spl12_136 ),
inference(forward_demodulation,[],[f2381,f765]) ).
fof(f2393,plain,
( $false
| ~ spl12_119
| ~ spl12_136 ),
inference(forward_subsumption_resolution,[],[f2391,f161]) ).
fof(f2394,plain,
( ~ spl12_119
| ~ spl12_136 ),
inference(avatar_contradiction_clause,[],[f2393]) ).
fof(f2395,plain,
( $false
| ~ spl12_83
| ~ spl12_136 ),
inference(forward_subsumption_resolution,[],[f2392,f161]) ).
fof(f2396,plain,
( ~ spl12_83
| ~ spl12_136 ),
inference(avatar_contradiction_clause,[],[f2395]) ).
fof(f2409,plain,
( e20 = e23
| ~ spl12_69
| ~ spl12_72 ),
inference(superposition,[],[f706,f718]) ).
fof(f2410,plain,
( $false
| ~ spl12_69
| ~ spl12_72 ),
inference(forward_subsumption_resolution,[],[f2409,f163]) ).
fof(f2411,plain,
( ~ spl12_69
| ~ spl12_72 ),
inference(avatar_contradiction_clause,[],[f2410]) ).
fof(f2453,plain,
( e21 = e22
| ~ spl12_126
| ~ spl12_127 ),
inference(forward_demodulation,[],[f948,f952]) ).
fof(f2454,plain,
( $false
| ~ spl12_126
| ~ spl12_127 ),
inference(forward_subsumption_resolution,[],[f2453,f162]) ).
fof(f2455,plain,
( ~ spl12_126
| ~ spl12_127 ),
inference(avatar_contradiction_clause,[],[f2454]) ).
fof(f2461,plain,
( e20 = e21
| ~ spl12_71
| ~ spl12_72 ),
inference(forward_demodulation,[],[f714,f718]) ).
fof(f2466,plain,
( $false
| ~ spl12_71
| ~ spl12_72 ),
inference(forward_subsumption_resolution,[],[f2461,f165]) ).
fof(f2467,plain,
( ~ spl12_71
| ~ spl12_72 ),
inference(avatar_contradiction_clause,[],[f2466]) ).
fof(f2469,plain,
( e21 = e22
| ~ spl12_74
| ~ spl12_75 ),
inference(superposition,[],[f731,f727]) ).
fof(f2474,plain,
( $false
| ~ spl12_74
| ~ spl12_75 ),
inference(forward_subsumption_resolution,[],[f2469,f162]) ).
fof(f2475,plain,
( ~ spl12_74
| ~ spl12_75 ),
inference(avatar_contradiction_clause,[],[f2474]) ).
fof(f2477,plain,
( e22 = e23
| ~ spl12_97
| ~ spl12_98 ),
inference(superposition,[],[f829,f825]) ).
fof(f2481,plain,
( $false
| ~ spl12_97
| ~ spl12_98 ),
inference(forward_subsumption_resolution,[],[f2477,f160]) ).
fof(f2482,plain,
( ~ spl12_97
| ~ spl12_98 ),
inference(avatar_contradiction_clause,[],[f2481]) ).
fof(f2501,plain,
( e21 = e22
| ~ spl12_98
| ~ spl12_99 ),
inference(superposition,[],[f833,f829]) ).
fof(f2505,plain,
( $false
| ~ spl12_98
| ~ spl12_99 ),
inference(forward_subsumption_resolution,[],[f2501,f162]) ).
fof(f2506,plain,
( ~ spl12_98
| ~ spl12_99 ),
inference(avatar_contradiction_clause,[],[f2505]) ).
fof(f2516,plain,
( e21 = e22
| ~ spl12_102
| ~ spl12_103 ),
inference(superposition,[],[f850,f846]) ).
fof(f2520,plain,
( $false
| ~ spl12_102
| ~ spl12_103 ),
inference(forward_subsumption_resolution,[],[f2516,f162]) ).
fof(f2521,plain,
( ~ spl12_102
| ~ spl12_103 ),
inference(avatar_contradiction_clause,[],[f2520]) ).
fof(f2526,plain,
( e20 = e22
| ~ spl12_70
| ~ spl12_72 ),
inference(forward_demodulation,[],[f710,f718]) ).
fof(f2528,plain,
( $false
| ~ spl12_70
| ~ spl12_72 ),
inference(forward_subsumption_resolution,[],[f2526,f164]) ).
fof(f2529,plain,
( ~ spl12_70
| ~ spl12_72 ),
inference(avatar_contradiction_clause,[],[f2528]) ).
fof(f2534,plain,
( e21 = e23
| ~ spl12_89
| ~ spl12_91 ),
inference(superposition,[],[f799,f791]) ).
fof(f2538,plain,
( $false
| ~ spl12_89
| ~ spl12_91 ),
inference(forward_subsumption_resolution,[],[f2534,f161]) ).
fof(f2539,plain,
( ~ spl12_89
| ~ spl12_91 ),
inference(avatar_contradiction_clause,[],[f2538]) ).
fof(f2545,plain,
( e22 = e23
| ~ spl12_109
| ~ spl12_110 ),
inference(superposition,[],[f880,f876]) ).
fof(f2549,plain,
( $false
| ~ spl12_109
| ~ spl12_110 ),
inference(forward_subsumption_resolution,[],[f2545,f160]) ).
fof(f2550,plain,
( ~ spl12_109
| ~ spl12_110 ),
inference(avatar_contradiction_clause,[],[f2549]) ).
fof(f2552,plain,
( e21 = e23
| ~ spl12_113
| ~ spl12_115 ),
inference(superposition,[],[f901,f893]) ).
fof(f2556,plain,
( $false
| ~ spl12_113
| ~ spl12_115 ),
inference(forward_subsumption_resolution,[],[f2552,f161]) ).
fof(f2557,plain,
( ~ spl12_113
| ~ spl12_115 ),
inference(avatar_contradiction_clause,[],[f2556]) ).
fof(f2559,plain,
( e22 = e23
| ~ spl12_121
| ~ spl12_122 ),
inference(superposition,[],[f931,f927]) ).
fof(f2563,plain,
( $false
| ~ spl12_121
| ~ spl12_122 ),
inference(forward_subsumption_resolution,[],[f2559,f160]) ).
fof(f2564,plain,
( ~ spl12_121
| ~ spl12_122 ),
inference(avatar_contradiction_clause,[],[f2563]) ).
fof(f2566,plain,
( e21 = e22
| ~ spl12_122
| ~ spl12_123 ),
inference(superposition,[],[f935,f931]) ).
fof(f2570,plain,
( $false
| ~ spl12_122
| ~ spl12_123 ),
inference(forward_subsumption_resolution,[],[f2566,f162]) ).
fof(f2571,plain,
( ~ spl12_122
| ~ spl12_123 ),
inference(avatar_contradiction_clause,[],[f2570]) ).
fof(f2573,plain,
( e21 = e23
| ~ spl12_125
| ~ spl12_127 ),
inference(superposition,[],[f952,f944]) ).
fof(f2577,plain,
( $false
| ~ spl12_125
| ~ spl12_127 ),
inference(forward_subsumption_resolution,[],[f2573,f161]) ).
fof(f2578,plain,
( ~ spl12_125
| ~ spl12_127 ),
inference(avatar_contradiction_clause,[],[f2577]) ).
fof(f2582,plain,
( e20 = e23
| ~ spl12_129
| ~ spl12_132 ),
inference(superposition,[],[f973,f961]) ).
fof(f2586,plain,
( $false
| ~ spl12_129
| ~ spl12_132 ),
inference(forward_subsumption_resolution,[],[f2582,f163]) ).
fof(f2587,plain,
( ~ spl12_129
| ~ spl12_132 ),
inference(avatar_contradiction_clause,[],[f2586]) ).
fof(f2591,plain,
( e20 = h4(e13)
| ~ spl12_72 ),
inference(superposition,[],[f718,f114]) ).
fof(f2617,plain,
( e23 = h2(e13)
| ~ spl12_109 ),
inference(superposition,[],[f876,f122]) ).
fof(f2618,plain,
( spl12_162
| ~ spl12_109 ),
inference(avatar_split_clause,[],[f2617,f874,f1185]) ).
fof(f2619,plain,
( op2(e23,e23) != h2(op1(e13,e13))
| ~ spl12_162
| spl12_186 ),
inference(superposition,[],[f1436,f1186]) ).
fof(f2623,plain,
( op2(e23,e23) != h2(e10)
| ~ spl12_4
| ~ spl12_162
| spl12_186 ),
inference(forward_demodulation,[],[f2619,f397]) ).
fof(f2624,plain,
( h2(e10) != h4(e13)
| ~ spl12_4
| ~ spl12_162
| spl12_186 ),
inference(forward_demodulation,[],[f2623,f114]) ).
fof(f2625,plain,
( e20 != h2(e10)
| ~ spl12_4
| ~ spl12_162
| spl12_186
| ~ spl12_204 ),
inference(forward_demodulation,[],[f2624,f1527]) ).
fof(f2626,plain,
( ~ spl12_203
| ~ spl12_4
| ~ spl12_162
| spl12_186
| ~ spl12_204 ),
inference(avatar_split_clause,[],[f2625,f1526,f1434,f1185,f395,f1505]) ).
fof(f2628,plain,
( e20 = h1(e13)
| ~ spl12_132 ),
inference(superposition,[],[f973,f126]) ).
fof(f2629,plain,
( spl12_242
| ~ spl12_132 ),
inference(avatar_split_clause,[],[f2628,f971,f1686]) ).
fof(f2636,plain,
( e20 = h2(e10)
| ~ spl12_108 ),
inference(superposition,[],[f1039,f871]) ).
fof(f2640,plain,
( $false
| ~ spl12_108
| spl12_203 ),
inference(forward_subsumption_resolution,[],[f2636,f1507]) ).
fof(f2641,plain,
( ~ spl12_108
| spl12_203 ),
inference(avatar_contradiction_clause,[],[f2640]) ).
fof(f2643,plain,
( h2(op1(e13,e12)) != op2(h2(e13),e22)
| ~ spl12_167
| spl12_187 ),
inference(forward_demodulation,[],[f1440,f1211]) ).
fof(f2645,plain,
( op2(e23,e22) != h2(op1(e13,e12))
| ~ spl12_162
| ~ spl12_167
| spl12_187 ),
inference(forward_demodulation,[],[f2643,f1186]) ).
fof(f2647,plain,
( op2(e23,e22) != h2(e11)
| ~ spl12_7
| ~ spl12_162
| ~ spl12_167
| spl12_187 ),
inference(forward_demodulation,[],[f2645,f410]) ).
fof(f2648,plain,
( e21 != op2(e23,e22)
| ~ spl12_7
| ~ spl12_162
| ~ spl12_167
| spl12_187 ),
inference(forward_demodulation,[],[f2647,f125]) ).
fof(f2649,plain,
( $false
| ~ spl12_7
| ~ spl12_75
| ~ spl12_162
| ~ spl12_167
| spl12_187 ),
inference(forward_subsumption_resolution,[],[f2648,f731]) ).
fof(f2650,plain,
( ~ spl12_7
| ~ spl12_75
| ~ spl12_162
| ~ spl12_167
| spl12_187 ),
inference(avatar_contradiction_clause,[],[f2649]) ).
fof(f2652,plain,
( e20 = e22
| ~ spl12_94
| ~ spl12_96 ),
inference(forward_demodulation,[],[f812,f820]) ).
fof(f2653,plain,
( e20 = e21
| ~ spl12_107
| ~ spl12_108 ),
inference(forward_demodulation,[],[f867,f871]) ).
fof(f2657,plain,
( $false
| ~ spl12_94
| ~ spl12_96 ),
inference(forward_subsumption_resolution,[],[f2652,f164]) ).
fof(f2658,plain,
( ~ spl12_94
| ~ spl12_96 ),
inference(avatar_contradiction_clause,[],[f2657]) ).
fof(f2659,plain,
( $false
| ~ spl12_107
| ~ spl12_108 ),
inference(forward_subsumption_resolution,[],[f2653,f165]) ).
fof(f2660,plain,
( ~ spl12_107
| ~ spl12_108 ),
inference(avatar_contradiction_clause,[],[f2659]) ).
fof(f2665,plain,
( op2(e22,e21) != h2(op1(e12,e11))
| ~ spl12_167
| spl12_200 ),
inference(forward_demodulation,[],[f1492,f1211]) ).
fof(f2670,plain,
( op2(e22,e21) != h2(e10)
| ~ spl12_28
| ~ spl12_167
| spl12_200 ),
inference(forward_demodulation,[],[f2665,f499]) ).
fof(f2672,plain,
( e20 != op2(e22,e21)
| ~ spl12_28
| ~ spl12_167
| spl12_200
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2670,f1506]) ).
fof(f2674,plain,
( $false
| ~ spl12_28
| ~ spl12_96
| ~ spl12_167
| spl12_200
| ~ spl12_203 ),
inference(forward_subsumption_resolution,[],[f2672,f820]) ).
fof(f2675,plain,
( ~ spl12_28
| ~ spl12_96
| ~ spl12_167
| spl12_200
| ~ spl12_203 ),
inference(avatar_contradiction_clause,[],[f2674]) ).
fof(f2676,plain,
( h2(op1(e13,e10)) != op2(h2(e13),e20)
| spl12_188
| ~ spl12_203 ),
inference(forward_demodulation,[],[f1444,f1506]) ).
fof(f2678,plain,
( op2(e23,e20) != h2(op1(e13,e10))
| ~ spl12_162
| spl12_188
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2676,f1186]) ).
fof(f2680,plain,
( op2(e23,e20) != h2(e13)
| ~ spl12_13
| ~ spl12_162
| spl12_188
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2678,f436]) ).
fof(f2682,plain,
( e23 != op2(e23,e20)
| ~ spl12_13
| ~ spl12_162
| spl12_188
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2680,f1186]) ).
fof(f2686,plain,
( h2(op1(e12,e13)) != op2(h2(e12),e23)
| ~ spl12_162
| spl12_189 ),
inference(forward_demodulation,[],[f1448,f1186]) ).
fof(f2688,plain,
( op2(e22,e23) != h2(op1(e12,e13))
| ~ spl12_162
| ~ spl12_167
| spl12_189 ),
inference(forward_demodulation,[],[f2686,f1211]) ).
fof(f2690,plain,
( op2(e22,e23) != h2(e11)
| ~ spl12_19
| ~ spl12_162
| ~ spl12_167
| spl12_189 ),
inference(forward_demodulation,[],[f2688,f461]) ).
fof(f2692,plain,
( e21 != op2(e22,e23)
| ~ spl12_19
| ~ spl12_162
| ~ spl12_167
| spl12_189 ),
inference(forward_demodulation,[],[f2690,f125]) ).
fof(f2693,plain,
( $false
| ~ spl12_19
| ~ spl12_87
| ~ spl12_162
| ~ spl12_167
| spl12_189 ),
inference(forward_subsumption_resolution,[],[f2692,f782]) ).
fof(f2694,plain,
( ~ spl12_19
| ~ spl12_87
| ~ spl12_162
| ~ spl12_167
| spl12_189 ),
inference(avatar_contradiction_clause,[],[f2693]) ).
fof(f2696,plain,
( op2(e22,e22) != h2(op1(e12,e12))
| ~ spl12_167
| spl12_190 ),
inference(forward_demodulation,[],[f1452,f1211]) ).
fof(f2698,plain,
( op2(e22,e22) != h2(e13)
| ~ spl12_21
| ~ spl12_167
| spl12_190 ),
inference(forward_demodulation,[],[f2696,f470]) ).
fof(f2700,plain,
( e23 != op2(e22,e22)
| ~ spl12_21
| ~ spl12_162
| ~ spl12_167
| spl12_190 ),
inference(forward_demodulation,[],[f2698,f1186]) ).
fof(f2702,plain,
( $false
| ~ spl12_21
| ~ spl12_89
| ~ spl12_162
| ~ spl12_167
| spl12_190 ),
inference(forward_subsumption_resolution,[],[f2700,f791]) ).
fof(f2703,plain,
( ~ spl12_21
| ~ spl12_89
| ~ spl12_162
| ~ spl12_167
| spl12_190 ),
inference(avatar_contradiction_clause,[],[f2702]) ).
fof(f2705,plain,
( h2(op1(e12,e10)) != op2(h2(e12),e20)
| spl12_191
| ~ spl12_203 ),
inference(forward_demodulation,[],[f1456,f1506]) ).
fof(f2707,plain,
( op2(e22,e20) != h2(op1(e12,e10))
| ~ spl12_167
| spl12_191
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2705,f1211]) ).
fof(f2709,plain,
( op2(e22,e20) != h2(e12)
| ~ spl12_30
| ~ spl12_167
| spl12_191
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2707,f508]) ).
fof(f2710,plain,
( e22 != op2(e22,e20)
| ~ spl12_30
| ~ spl12_167
| spl12_191
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2709,f1211]) ).
fof(f2713,plain,
( h2(op1(e12,e10)) = op2(h2(e12),e20)
| ~ spl12_191
| ~ spl12_203 ),
inference(forward_demodulation,[],[f1455,f1506]) ).
fof(f2714,plain,
( h2(op1(e10,e13)) != op2(h2(e10),e23)
| ~ spl12_162
| spl12_192 ),
inference(forward_demodulation,[],[f1460,f1186]) ).
fof(f2715,plain,
( op2(e22,e20) = h2(op1(e12,e10))
| ~ spl12_167
| ~ spl12_191
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2713,f1211]) ).
fof(f2716,plain,
( op2(e20,e23) != h2(op1(e10,e13))
| ~ spl12_162
| spl12_192
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2714,f1506]) ).
fof(f2718,plain,
( op2(e20,e23) != h2(e13)
| ~ spl12_49
| ~ spl12_162
| spl12_192
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2716,f589]) ).
fof(f2720,plain,
( e23 != op2(e20,e23)
| ~ spl12_49
| ~ spl12_162
| spl12_192
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2718,f1186]) ).
fof(f2724,plain,
( h2(op1(e10,e12)) != op2(h2(e10),e22)
| ~ spl12_167
| spl12_193 ),
inference(forward_demodulation,[],[f1464,f1211]) ).
fof(f2726,plain,
( op2(e20,e22) != h2(op1(e10,e12))
| ~ spl12_167
| spl12_193
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2724,f1506]) ).
fof(f2728,plain,
( op2(e20,e22) != h2(e12)
| ~ spl12_54
| ~ spl12_167
| spl12_193
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2726,f610]) ).
fof(f2730,plain,
( e22 != op2(e20,e22)
| ~ spl12_54
| ~ spl12_167
| spl12_193
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2728,f1211]) ).
fof(f2743,plain,
( op2(e20,e21) != h2(op1(e10,e11))
| spl12_195
| ~ spl12_203 ),
inference(forward_demodulation,[],[f1472,f1506]) ).
fof(f2745,plain,
( op2(e20,e21) != h2(e11)
| ~ spl12_59
| spl12_195
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2743,f631]) ).
fof(f2747,plain,
( e21 != op2(e20,e21)
| ~ spl12_59
| spl12_195
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2745,f125]) ).
fof(f2751,plain,
( op2(e21,e20) != h2(op1(e11,e10))
| spl12_196
| ~ spl12_203 ),
inference(forward_demodulation,[],[f1476,f1506]) ).
fof(f2753,plain,
( op2(e21,e20) != h2(e11)
| ~ spl12_47
| spl12_196
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2751,f580]) ).
fof(f2755,plain,
( e21 != op2(e21,e20)
| ~ spl12_47
| spl12_196
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2753,f125]) ).
fof(f2759,plain,
( h2(e13) != h2(e13)
| ~ spl12_41
| spl12_197 ),
inference(forward_demodulation,[],[f1480,f555]) ).
fof(f2760,plain,
( $false
| ~ spl12_41
| spl12_197 ),
inference(trivial_inequality_removal,[],[f2759]) ).
fof(f2761,plain,
( ~ spl12_41
| spl12_197 ),
inference(avatar_contradiction_clause,[],[f2760]) ).
fof(f2764,plain,
( op2(e21,e22) != h2(op1(e11,e12))
| ~ spl12_167
| spl12_198 ),
inference(forward_demodulation,[],[f1484,f1211]) ).
fof(f2765,plain,
( op2(e21,e22) != h2(e10)
| ~ spl12_40
| ~ spl12_167
| spl12_198 ),
inference(forward_demodulation,[],[f2764,f550]) ).
fof(f2766,plain,
( $false
| ~ spl12_40
| ~ spl12_167
| spl12_198 ),
inference(forward_subsumption_resolution,[],[f2765,f1039]) ).
fof(f2767,plain,
( ~ spl12_40
| ~ spl12_167
| spl12_198 ),
inference(avatar_contradiction_clause,[],[f2766]) ).
fof(f2769,plain,
( op2(e21,e23) != h2(op1(e11,e13))
| ~ spl12_162
| spl12_199 ),
inference(forward_demodulation,[],[f1488,f1186]) ).
fof(f2771,plain,
( op2(e21,e23) != h2(e12)
| ~ spl12_34
| ~ spl12_162
| spl12_199 ),
inference(forward_demodulation,[],[f2769,f525]) ).
fof(f2772,plain,
( e22 != op2(e21,e23)
| ~ spl12_34
| ~ spl12_162
| ~ spl12_167
| spl12_199 ),
inference(forward_demodulation,[],[f2771,f1211]) ).
fof(f2773,plain,
( $false
| ~ spl12_34
| ~ spl12_102
| ~ spl12_162
| ~ spl12_167
| spl12_199 ),
inference(forward_subsumption_resolution,[],[f2772,f846]) ).
fof(f2774,plain,
( ~ spl12_34
| ~ spl12_102
| ~ spl12_162
| ~ spl12_167
| spl12_199 ),
inference(avatar_contradiction_clause,[],[f2773]) ).
fof(f2776,plain,
( op2(e23,e21) != h2(op1(e13,e11))
| ~ spl12_162
| spl12_201 ),
inference(forward_demodulation,[],[f1496,f1186]) ).
fof(f2778,plain,
( op2(e23,e21) != h2(e12)
| ~ spl12_10
| ~ spl12_162
| spl12_201 ),
inference(forward_demodulation,[],[f2776,f423]) ).
fof(f2780,plain,
( e22 != op2(e23,e21)
| ~ spl12_10
| ~ spl12_162
| ~ spl12_167
| spl12_201 ),
inference(forward_demodulation,[],[f2778,f1211]) ).
fof(f2783,plain,
( e10 = e11
| ~ spl12_3
| ~ spl12_4 ),
inference(forward_demodulation,[],[f393,f397]) ).
fof(f2785,plain,
( e10 = e11
| ~ spl12_27
| ~ spl12_28 ),
inference(forward_demodulation,[],[f495,f499]) ).
fof(f2791,plain,
( $false
| ~ spl12_3
| ~ spl12_4 ),
inference(forward_subsumption_resolution,[],[f2783,f171]) ).
fof(f2792,plain,
( ~ spl12_3
| ~ spl12_4 ),
inference(avatar_contradiction_clause,[],[f2791]) ).
fof(f2793,plain,
( $false
| ~ spl12_27
| ~ spl12_28 ),
inference(forward_subsumption_resolution,[],[f2785,f171]) ).
fof(f2794,plain,
( ~ spl12_27
| ~ spl12_28 ),
inference(avatar_contradiction_clause,[],[f2793]) ).
fof(f2865,plain,
( e21 = e23
| ~ spl12_73
| ~ spl12_75 ),
inference(forward_demodulation,[],[f723,f731]) ).
fof(f2885,plain,
( $false
| ~ spl12_73
| ~ spl12_75 ),
inference(forward_subsumption_resolution,[],[f2865,f161]) ).
fof(f2886,plain,
( ~ spl12_73
| ~ spl12_75 ),
inference(avatar_contradiction_clause,[],[f2885]) ).
fof(f2972,plain,
( op2(e22,e20) = h2(e11)
| ~ spl12_31
| ~ spl12_167
| ~ spl12_191
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2715,f512]) ).
fof(f2980,plain,
( e21 = op2(e22,e20)
| ~ spl12_31
| ~ spl12_167
| ~ spl12_191
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2972,f125]) ).
fof(f2985,plain,
( spl12_99
| ~ spl12_31
| ~ spl12_167
| ~ spl12_191
| ~ spl12_203 ),
inference(avatar_split_clause,[],[f2980,f1505,f1454,f1210,f510,f831]) ).
fof(f2992,plain,
( op2(e20,e20) != h2(op1(e10,e10))
| spl12_194
| ~ spl12_203 ),
inference(forward_demodulation,[],[f1468,f1506]) ).
fof(f3017,plain,
( e11 = op1(e11,e13)
| ~ spl12_65 ),
inference(superposition,[],[f362,f657]) ).
fof(f3081,plain,
( e11 = e13
| ~ spl12_21
| ~ spl12_23 ),
inference(superposition,[],[f478,f470]) ).
fof(f3082,plain,
( e11 = e13
| ~ spl12_21
| ~ spl12_23 ),
inference(superposition,[],[f470,f478]) ).
fof(f3083,plain,
( $false
| ~ spl12_21
| ~ spl12_23 ),
inference(forward_subsumption_resolution,[],[f3082,f167]) ).
fof(f3084,plain,
( ~ spl12_21
| ~ spl12_23 ),
inference(avatar_contradiction_clause,[],[f3083]) ).
fof(f3085,plain,
( $false
| ~ spl12_21
| ~ spl12_23 ),
inference(forward_subsumption_resolution,[],[f3081,f167]) ).
fof(f3086,plain,
( ~ spl12_21
| ~ spl12_23 ),
inference(avatar_contradiction_clause,[],[f3085]) ).
fof(f3088,plain,
( e10 = e11
| ~ spl12_39
| ~ spl12_40 ),
inference(forward_demodulation,[],[f546,f550]) ).
fof(f3089,plain,
( $false
| ~ spl12_39
| ~ spl12_40 ),
inference(forward_subsumption_resolution,[],[f3088,f171]) ).
fof(f3090,plain,
( ~ spl12_39
| ~ spl12_40 ),
inference(avatar_contradiction_clause,[],[f3089]) ).
fof(f3114,plain,
( e20 = e23
| ~ spl12_105
| ~ spl12_108 ),
inference(forward_demodulation,[],[f859,f871]) ).
fof(f3117,plain,
( $false
| ~ spl12_105
| ~ spl12_108 ),
inference(forward_subsumption_resolution,[],[f3114,f163]) ).
fof(f3118,plain,
( ~ spl12_105
| ~ spl12_108 ),
inference(avatar_contradiction_clause,[],[f3117]) ).
fof(f3177,plain,
( e20 = e21
| ~ spl12_75
| ~ spl12_76 ),
inference(superposition,[],[f735,f731]) ).
fof(f3182,plain,
( $false
| ~ spl12_75
| ~ spl12_76 ),
inference(forward_subsumption_resolution,[],[f3177,f165]) ).
fof(f3183,plain,
( ~ spl12_75
| ~ spl12_76 ),
inference(avatar_contradiction_clause,[],[f3182]) ).
fof(f3185,plain,
( e20 = e23
| ~ spl12_81
| ~ spl12_84 ),
inference(superposition,[],[f769,f757]) ).
fof(f3189,plain,
( $false
| ~ spl12_81
| ~ spl12_84 ),
inference(forward_subsumption_resolution,[],[f3185,f163]) ).
fof(f3190,plain,
( ~ spl12_81
| ~ spl12_84 ),
inference(avatar_contradiction_clause,[],[f3189]) ).
fof(f3207,plain,
( e22 = op2(e21,e23)
| ~ spl12_109 ),
inference(superposition,[],[f131,f876]) ).
fof(f3209,plain,
( e12 = op1(e11,e13)
| ~ spl12_41 ),
inference(superposition,[],[f134,f555]) ).
fof(f3210,plain,
( $false
| spl12_34
| ~ spl12_41 ),
inference(forward_subsumption_resolution,[],[f3209,f524]) ).
fof(f3211,plain,
( spl12_34
| ~ spl12_41 ),
inference(avatar_contradiction_clause,[],[f3210]) ).
fof(f3218,plain,
( spl12_35
| ~ spl12_65 ),
inference(avatar_split_clause,[],[f3017,f655,f527]) ).
fof(f3226,plain,
( ~ spl12_78
| ~ spl12_10
| ~ spl12_162
| ~ spl12_167
| spl12_201 ),
inference(avatar_split_clause,[],[f2780,f1494,f1210,f1185,f421,f742]) ).
fof(f3228,plain,
( ~ spl12_81
| ~ spl12_13
| ~ spl12_162
| spl12_188
| ~ spl12_203 ),
inference(avatar_split_clause,[],[f2682,f1505,f1442,f1185,f434,f755]) ).
fof(f3231,plain,
( ~ spl12_98
| ~ spl12_30
| ~ spl12_167
| spl12_191
| ~ spl12_203 ),
inference(avatar_split_clause,[],[f2710,f1505,f1454,f1210,f506,f827]) ).
fof(f3232,plain,
( ~ spl12_115
| ~ spl12_47
| spl12_196
| ~ spl12_203 ),
inference(avatar_split_clause,[],[f2755,f1505,f1474,f578,f899]) ).
fof(f3233,plain,
( ~ spl12_117
| ~ spl12_49
| ~ spl12_162
| spl12_192
| ~ spl12_203 ),
inference(avatar_split_clause,[],[f2720,f1505,f1458,f1185,f587,f908]) ).
fof(f3236,plain,
( ~ spl12_122
| ~ spl12_54
| ~ spl12_167
| spl12_193
| ~ spl12_203 ),
inference(avatar_split_clause,[],[f2730,f1505,f1462,f1210,f608,f929]) ).
fof(f3237,plain,
( ~ spl12_127
| ~ spl12_59
| spl12_195
| ~ spl12_203 ),
inference(avatar_split_clause,[],[f2747,f1505,f1470,f629,f950]) ).
fof(f3254,plain,
( $false
| spl12_102
| ~ spl12_109 ),
inference(forward_subsumption_resolution,[],[f3207,f845]) ).
fof(f3255,plain,
( spl12_102
| ~ spl12_109 ),
inference(avatar_contradiction_clause,[],[f3254]) ).
fof(f3274,plain,
( op2(e20,e20) != h2(e10)
| ~ spl12_64
| spl12_194
| ~ spl12_203 ),
inference(forward_demodulation,[],[f2992,f652]) ).
fof(f3327,plain,
( e20 != op2(e20,e20)
| ~ spl12_64
| spl12_194
| ~ spl12_203 ),
inference(forward_demodulation,[],[f3274,f1506]) ).
fof(f3357,plain,
( e20 != h1(e13)
| ~ spl12_64
| spl12_194
| ~ spl12_203 ),
inference(forward_demodulation,[],[f3327,f126]) ).
fof(f3376,plain,
( $false
| ~ spl12_64
| spl12_194
| ~ spl12_203
| ~ spl12_242 ),
inference(forward_subsumption_resolution,[],[f3357,f1687]) ).
fof(f3377,plain,
( ~ spl12_64
| spl12_194
| ~ spl12_203
| ~ spl12_242 ),
inference(avatar_contradiction_clause,[],[f3376]) ).
fof(f3399,plain,
( e21 = op2(e21,e23)
| ~ spl12_133 ),
inference(superposition,[],[f305,f978]) ).
fof(f3404,plain,
( spl12_103
| ~ spl12_133 ),
inference(avatar_split_clause,[],[f3399,f976,f848]) ).
fof(f3408,plain,
( spl12_204
| ~ spl12_72 ),
inference(avatar_split_clause,[],[f2591,f716,f1526]) ).
fof(f3534,plain,
( e10 = e13
| ~ spl12_5
| ~ spl12_8 ),
inference(superposition,[],[f414,f402]) ).
fof(f3538,plain,
( $false
| ~ spl12_5
| ~ spl12_8 ),
inference(forward_subsumption_resolution,[],[f3534,f169]) ).
fof(f3539,plain,
( ~ spl12_5
| ~ spl12_8 ),
inference(avatar_contradiction_clause,[],[f3538]) ).
fof(f3540,plain,
( e11 = e12
| ~ spl12_2
| ~ spl12_3 ),
inference(forward_demodulation,[],[f389,f393]) ).
fof(f3552,plain,
( $false
| ~ spl12_2
| ~ spl12_3 ),
inference(forward_subsumption_resolution,[],[f3540,f168]) ).
fof(f3553,plain,
( ~ spl12_2
| ~ spl12_3 ),
inference(avatar_contradiction_clause,[],[f3552]) ).
fof(f3694,plain,
( e12 = op1(e11,e11)
| ~ spl12_43 ),
inference(superposition,[],[f134,f563]) ).
fof(f3698,plain,
( e11 = e12
| ~ spl12_43 ),
inference(forward_demodulation,[],[f3694,f563]) ).
fof(f3701,plain,
( $false
| ~ spl12_43 ),
inference(forward_subsumption_resolution,[],[f3698,f168]) ).
fof(f3702,plain,
~ spl12_43,
inference(avatar_contradiction_clause,[],[f3701]) ).
fof(f3704,plain,
( e10 = e13
| ~ spl12_41
| ~ spl12_44 ),
inference(superposition,[],[f567,f555]) ).
fof(f3711,plain,
( $false
| ~ spl12_41
| ~ spl12_44 ),
inference(forward_subsumption_resolution,[],[f3704,f169]) ).
fof(f3712,plain,
( ~ spl12_41
| ~ spl12_44 ),
inference(avatar_contradiction_clause,[],[f3711]) ).
fof(f3734,plain,
( e20 = e23
| ~ spl12_73
| ~ spl12_76 ),
inference(superposition,[],[f735,f723]) ).
fof(f3736,plain,
( e20 = e23
| ~ spl12_73
| ~ spl12_76 ),
inference(superposition,[],[f723,f735]) ).
fof(f3737,plain,
( $false
| ~ spl12_73
| ~ spl12_76 ),
inference(forward_subsumption_resolution,[],[f3736,f163]) ).
fof(f3738,plain,
( ~ spl12_73
| ~ spl12_76 ),
inference(avatar_contradiction_clause,[],[f3737]) ).
fof(f3739,plain,
( $false
| ~ spl12_73
| ~ spl12_76 ),
inference(forward_subsumption_resolution,[],[f3734,f163]) ).
fof(f3740,plain,
( ~ spl12_73
| ~ spl12_76 ),
inference(avatar_contradiction_clause,[],[f3739]) ).
fof(f3742,plain,
( e20 = e22
| ~ spl12_78
| ~ spl12_80 ),
inference(superposition,[],[f752,f744]) ).
fof(f3743,plain,
( e20 = e22
| ~ spl12_78
| ~ spl12_80 ),
inference(superposition,[],[f744,f752]) ).
fof(f3744,plain,
( $false
| ~ spl12_78
| ~ spl12_80 ),
inference(forward_subsumption_resolution,[],[f3743,f164]) ).
fof(f3745,plain,
( ~ spl12_78
| ~ spl12_80 ),
inference(avatar_contradiction_clause,[],[f3744]) ).
fof(f3746,plain,
( $false
| ~ spl12_78
| ~ spl12_80 ),
inference(forward_subsumption_resolution,[],[f3742,f164]) ).
fof(f3747,plain,
( ~ spl12_78
| ~ spl12_80 ),
inference(avatar_contradiction_clause,[],[f3746]) ).
fof(f3748,plain,
( e21 = e22
| ~ spl12_70
| ~ spl12_71 ),
inference(forward_demodulation,[],[f710,f714]) ).
fof(f3769,plain,
( $false
| ~ spl12_70
| ~ spl12_71 ),
inference(forward_subsumption_resolution,[],[f3748,f162]) ).
fof(f3770,plain,
( ~ spl12_70
| ~ spl12_71 ),
inference(avatar_contradiction_clause,[],[f3769]) ).
fof(f3889,plain,
( e20 = e22
| ~ spl12_98
| ~ spl12_100 ),
inference(superposition,[],[f837,f829]) ).
fof(f3894,plain,
( $false
| ~ spl12_98
| ~ spl12_100 ),
inference(forward_subsumption_resolution,[],[f3889,f164]) ).
fof(f3895,plain,
( ~ spl12_98
| ~ spl12_100 ),
inference(avatar_contradiction_clause,[],[f3894]) ).
fof(f3897,plain,
( e20 = e21
| ~ spl12_87
| ~ spl12_88 ),
inference(superposition,[],[f786,f782]) ).
fof(f3903,plain,
( $false
| ~ spl12_87
| ~ spl12_88 ),
inference(forward_subsumption_resolution,[],[f3897,f165]) ).
fof(f3904,plain,
( ~ spl12_87
| ~ spl12_88 ),
inference(avatar_contradiction_clause,[],[f3903]) ).
fof(f3957,plain,
( e20 = e23
| ~ spl12_89
| ~ spl12_92 ),
inference(superposition,[],[f803,f791]) ).
fof(f3967,plain,
( $false
| ~ spl12_89
| ~ spl12_92 ),
inference(forward_subsumption_resolution,[],[f3957,f163]) ).
fof(f3968,plain,
( ~ spl12_89
| ~ spl12_92 ),
inference(avatar_contradiction_clause,[],[f3967]) ).
cnf(s1,plain,
( spl12_1
| spl12_2
| spl12_3
| spl12_4 ),
inference(sat_conversion,[],[f398]) ).
cnf(s17,plain,
( spl12_65
| spl12_66
| spl12_67
| spl12_68 ),
inference(sat_conversion,[],[f670]) ).
cnf(s21,plain,
( spl12_2
| spl12_6
| spl12_10
| spl12_14 ),
inference(sat_conversion,[],[f674]) ).
cnf(s22,plain,
( spl12_3
| spl12_19
| spl12_35
| spl12_51 ),
inference(sat_conversion,[],[f675]) ).
cnf(s23,plain,
( spl12_3
| spl12_7
| spl12_11
| spl12_15 ),
inference(sat_conversion,[],[f676]) ).
cnf(s24,plain,
( spl12_4
| spl12_20
| spl12_36
| spl12_52 ),
inference(sat_conversion,[],[f677]) ).
cnf(s25,plain,
( spl12_4
| spl12_8
| spl12_12
| spl12_16 ),
inference(sat_conversion,[],[f678]) ).
cnf(s26,plain,
( spl12_5
| spl12_21
| spl12_37
| spl12_53 ),
inference(sat_conversion,[],[f679]) ).
cnf(s27,plain,
( spl12_17
| spl12_21
| spl12_25
| spl12_29 ),
inference(sat_conversion,[],[f680]) ).
cnf(s30,plain,
( spl12_7
| spl12_23
| spl12_39
| spl12_55 ),
inference(sat_conversion,[],[f683]) ).
cnf(s31,plain,
( spl12_19
| spl12_23
| spl12_27
| spl12_31 ),
inference(sat_conversion,[],[f684]) ).
cnf(s33,plain,
( spl12_20
| spl12_24
| spl12_28
| spl12_32 ),
inference(sat_conversion,[],[f686]) ).
cnf(s36,plain,
( spl12_10
| spl12_26
| spl12_42
| spl12_58 ),
inference(sat_conversion,[],[f689]) ).
cnf(s39,plain,
( spl12_35
| spl12_39
| spl12_43
| spl12_47 ),
inference(sat_conversion,[],[f692]) ).
cnf(s40,plain,
( spl12_12
| spl12_28
| spl12_44
| spl12_60 ),
inference(sat_conversion,[],[f693]) ).
cnf(s42,plain,
( spl12_13
| spl12_29
| spl12_45
| spl12_61 ),
inference(sat_conversion,[],[f695]) ).
cnf(s43,plain,
( spl12_49
| spl12_53
| spl12_57
| spl12_61 ),
inference(sat_conversion,[],[f696]) ).
cnf(s50,plain,
( spl12_69
| spl12_70
| spl12_71
| spl12_72 ),
inference(sat_conversion,[],[f719]) ).
cnf(s66,plain,
( spl12_133
| spl12_134
| spl12_135
| spl12_136 ),
inference(sat_conversion,[],[f991]) ).
cnf(s70,plain,
( spl12_70
| spl12_74
| spl12_78
| spl12_82 ),
inference(sat_conversion,[],[f995]) ).
cnf(s71,plain,
( spl12_71
| spl12_87
| spl12_103
| spl12_119 ),
inference(sat_conversion,[],[f996]) ).
cnf(s72,plain,
( spl12_71
| spl12_75
| spl12_79
| spl12_83 ),
inference(sat_conversion,[],[f997]) ).
cnf(s74,plain,
( spl12_72
| spl12_76
| spl12_80
| spl12_84 ),
inference(sat_conversion,[],[f999]) ).
cnf(s75,plain,
( spl12_73
| spl12_89
| spl12_105
| spl12_121 ),
inference(sat_conversion,[],[f1000]) ).
cnf(s79,plain,
( spl12_75
| spl12_91
| spl12_107
| spl12_123 ),
inference(sat_conversion,[],[f1004]) ).
cnf(s82,plain,
( spl12_88
| spl12_92
| spl12_96
| spl12_100 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s85,plain,
( spl12_78
| spl12_94
| spl12_110
| spl12_126 ),
inference(sat_conversion,[],[f1010]) ).
cnf(s91,plain,
( spl12_81
| spl12_97
| spl12_113
| spl12_129 ),
inference(sat_conversion,[],[f1016]) ).
cnf(s92,plain,
( spl12_117
| spl12_121
| spl12_125
| spl12_129 ),
inference(sat_conversion,[],[f1017]) ).
cnf(s107,plain,
spl12_41,
inference(sat_conversion,[],[f1032]) ).
cnf(s108,plain,
spl12_109,
inference(sat_conversion,[],[f1034]) ).
cnf(s127,plain,
( ~ spl12_161
| ~ spl12_162 ),
inference(sat_conversion,[],[f1188]) ).
cnf(s131,plain,
( ~ spl12_165
| ~ spl12_167 ),
inference(sat_conversion,[],[f1213]) ).
cnf(s145,plain,
spl12_40,
inference(sat_conversion,[],[f1300]) ).
cnf(s146,plain,
spl12_108,
inference(sat_conversion,[],[f1301]) ).
cnf(s147,plain,
spl12_167,
inference(sat_conversion,[],[f1303]) ).
cnf(s150,plain,
~ spl12_169,
inference(sat_conversion,[],[f1324]) ).
cnf(s153,plain,
( spl12_161
| spl12_165
| spl12_169
| ~ spl12_186
| ~ spl12_187
| ~ spl12_188
| ~ spl12_189
| ~ spl12_190
| ~ spl12_191
| ~ spl12_192
| ~ spl12_193
| ~ spl12_194
| ~ spl12_195
| ~ spl12_196
| ~ spl12_197
| ~ spl12_198
| ~ spl12_199
| ~ spl12_200
| ~ spl12_201
| ~ spl12_203 ),
inference(sat_conversion,[],[f1508]) ).
cnf(s177,plain,
( ~ spl12_40
| ~ spl12_66 ),
inference(sat_conversion,[],[f1819]) ).
cnf(s178,plain,
( spl12_43
| ~ spl12_67 ),
inference(sat_conversion,[],[f1827]) ).
cnf(s184,plain,
( spl12_54
| ~ spl12_68 ),
inference(sat_conversion,[],[f1847]) ).
cnf(s185,plain,
( spl12_30
| ~ spl12_68 ),
inference(sat_conversion,[],[f1848]) ).
cnf(s187,plain,
( ~ spl12_14
| ~ spl12_68 ),
inference(sat_conversion,[],[f1854]) ).
cnf(s188,plain,
( ~ spl12_51
| ~ spl12_68 ),
inference(sat_conversion,[],[f1860]) ).
cnf(s189,plain,
( ~ spl12_15
| ~ spl12_68 ),
inference(sat_conversion,[],[f1862]) ).
cnf(s190,plain,
( ~ spl12_52
| ~ spl12_68 ),
inference(sat_conversion,[],[f1870]) ).
cnf(s191,plain,
( ~ spl12_16
| ~ spl12_68 ),
inference(sat_conversion,[],[f1872]) ).
cnf(s192,plain,
( spl12_59
| ~ spl12_68 ),
inference(sat_conversion,[],[f1880]) ).
cnf(s193,plain,
( spl12_64
| ~ spl12_68 ),
inference(sat_conversion,[],[f1882]) ).
cnf(s195,plain,
( ~ spl12_5
| ~ spl12_6 ),
inference(sat_conversion,[],[f1890]) ).
cnf(s197,plain,
( ~ spl12_6
| ~ spl12_7 ),
inference(sat_conversion,[],[f1897]) ).
cnf(s200,plain,
( ~ spl12_11
| ~ spl12_12 ),
inference(sat_conversion,[],[f1910]) ).
cnf(s215,plain,
( ~ spl12_26
| ~ spl12_27 ),
inference(sat_conversion,[],[f1962]) ).
cnf(s218,plain,
( ~ spl12_29
| ~ spl12_30 ),
inference(sat_conversion,[],[f1976]) ).
cnf(s220,plain,
( ~ spl12_30
| ~ spl12_32 ),
inference(sat_conversion,[],[f1986]) ).
cnf(s222,plain,
( ~ spl12_17
| ~ spl12_19 ),
inference(sat_conversion,[],[f1998]) ).
cnf(s230,plain,
( ~ spl12_1
| ~ spl12_3 ),
inference(sat_conversion,[],[f2049]) ).
cnf(s232,plain,
( ~ spl12_1
| ~ spl12_4 ),
inference(sat_conversion,[],[f2060]) ).
cnf(s236,plain,
( ~ spl12_10
| ~ spl12_12 ),
inference(sat_conversion,[],[f2076]) ).
cnf(s237,plain,
( ~ spl12_19
| ~ spl12_20 ),
inference(sat_conversion,[],[f2087]) ).
cnf(s238,plain,
( ~ spl12_19
| ~ spl12_20 ),
inference(sat_conversion,[],[f2089]) ).
cnf(s239,plain,
( ~ spl12_25
| ~ spl12_28 ),
inference(sat_conversion,[],[f2095]) ).
cnf(s242,plain,
( ~ spl12_34
| ~ spl12_35 ),
inference(sat_conversion,[],[f2109]) ).
cnf(s244,plain,
( ~ spl12_34
| ~ spl12_36 ),
inference(sat_conversion,[],[f2116]) ).
cnf(s246,plain,
( ~ spl12_41
| ~ spl12_42 ),
inference(sat_conversion,[],[f2124]) ).
cnf(s247,plain,
( ~ spl12_26
| ~ spl12_28 ),
inference(sat_conversion,[],[f2129]) ).
cnf(s249,plain,
( ~ spl12_58
| ~ spl12_59 ),
inference(sat_conversion,[],[f2138]) ).
cnf(s251,plain,
( ~ spl12_2
| ~ spl12_4 ),
inference(sat_conversion,[],[f2150]) ).
cnf(s253,plain,
( ~ spl12_21
| ~ spl12_24 ),
inference(sat_conversion,[],[f2160]) ).
cnf(s255,plain,
( ~ spl12_45
| ~ spl12_47 ),
inference(sat_conversion,[],[f2172]) ).
cnf(s257,plain,
( ~ spl12_53
| ~ spl12_54 ),
inference(sat_conversion,[],[f2180]) ).
cnf(s258,plain,
( ~ spl12_37
| ~ spl12_40 ),
inference(sat_conversion,[],[f2184]) ).
cnf(s261,plain,
( ~ spl12_54
| ~ spl12_55 ),
inference(sat_conversion,[],[f2201]) ).
cnf(s265,plain,
( ~ spl12_57
| ~ spl12_59 ),
inference(sat_conversion,[],[f2215]) ).
cnf(s267,plain,
( ~ spl12_59
| ~ spl12_60 ),
inference(sat_conversion,[],[f2223]) ).
cnf(s269,plain,
( ~ spl12_61
| ~ spl12_64 ),
inference(sat_conversion,[],[f2230]) ).
cnf(s271,plain,
( ~ spl12_73
| ~ spl12_74 ),
inference(sat_conversion,[],[f2239]) ).
cnf(s278,plain,
( ~ spl12_108
| ~ spl12_135 ),
inference(sat_conversion,[],[f2261]) ).
cnf(s285,plain,
( ~ spl12_108
| ~ spl12_134 ),
inference(sat_conversion,[],[f2292]) ).
cnf(s286,plain,
( spl12_132
| ~ spl12_136 ),
inference(sat_conversion,[],[f2304]) ).
cnf(s288,plain,
( spl12_127
| ~ spl12_136 ),
inference(sat_conversion,[],[f2305]) ).
cnf(s289,plain,
( spl12_115
| ~ spl12_136 ),
inference(sat_conversion,[],[f2306]) ).
cnf(s290,plain,
( spl12_122
| ~ spl12_136 ),
inference(sat_conversion,[],[f2307]) ).
cnf(s291,plain,
( spl12_98
| ~ spl12_136 ),
inference(sat_conversion,[],[f2308]) ).
cnf(s293,plain,
( ~ spl12_82
| ~ spl12_136 ),
inference(sat_conversion,[],[f2314]) ).
cnf(s294,plain,
( ~ spl12_78
| ~ spl12_79 ),
inference(sat_conversion,[],[f2331]) ).
cnf(s297,plain,
( ~ spl12_79
| ~ spl12_80 ),
inference(sat_conversion,[],[f2340]) ).
cnf(s308,plain,
( ~ spl12_119
| ~ spl12_136 ),
inference(sat_conversion,[],[f2394]) ).
cnf(s309,plain,
( ~ spl12_83
| ~ spl12_136 ),
inference(sat_conversion,[],[f2396]) ).
cnf(s311,plain,
( ~ spl12_69
| ~ spl12_72 ),
inference(sat_conversion,[],[f2411]) ).
cnf(s324,plain,
( ~ spl12_126
| ~ spl12_127 ),
inference(sat_conversion,[],[f2455]) ).
cnf(s326,plain,
( ~ spl12_71
| ~ spl12_72 ),
inference(sat_conversion,[],[f2467]) ).
cnf(s328,plain,
( ~ spl12_74
| ~ spl12_75 ),
inference(sat_conversion,[],[f2475]) ).
cnf(s330,plain,
( ~ spl12_97
| ~ spl12_98 ),
inference(sat_conversion,[],[f2482]) ).
cnf(s335,plain,
( ~ spl12_98
| ~ spl12_99 ),
inference(sat_conversion,[],[f2506]) ).
cnf(s339,plain,
( ~ spl12_102
| ~ spl12_103 ),
inference(sat_conversion,[],[f2521]) ).
cnf(s341,plain,
( ~ spl12_70
| ~ spl12_72 ),
inference(sat_conversion,[],[f2529]) ).
cnf(s343,plain,
( ~ spl12_89
| ~ spl12_91 ),
inference(sat_conversion,[],[f2539]) ).
cnf(s345,plain,
( ~ spl12_109
| ~ spl12_110 ),
inference(sat_conversion,[],[f2550]) ).
cnf(s347,plain,
( ~ spl12_113
| ~ spl12_115 ),
inference(sat_conversion,[],[f2557]) ).
cnf(s349,plain,
( ~ spl12_121
| ~ spl12_122 ),
inference(sat_conversion,[],[f2564]) ).
cnf(s351,plain,
( ~ spl12_122
| ~ spl12_123 ),
inference(sat_conversion,[],[f2571]) ).
cnf(s353,plain,
( ~ spl12_125
| ~ spl12_127 ),
inference(sat_conversion,[],[f2578]) ).
cnf(s355,plain,
( ~ spl12_129
| ~ spl12_132 ),
inference(sat_conversion,[],[f2587]) ).
cnf(s362,plain,
( ~ spl12_109
| spl12_162 ),
inference(sat_conversion,[],[f2618]) ).
cnf(s364,plain,
( ~ spl12_4
| ~ spl12_162
| spl12_186
| ~ spl12_203
| ~ spl12_204 ),
inference(sat_conversion,[],[f2626]) ).
cnf(s365,plain,
( ~ spl12_132
| spl12_242 ),
inference(sat_conversion,[],[f2629]) ).
cnf(s369,plain,
( ~ spl12_108
| spl12_203 ),
inference(sat_conversion,[],[f2641]) ).
cnf(s370,plain,
( ~ spl12_7
| ~ spl12_75
| ~ spl12_162
| ~ spl12_167
| spl12_187 ),
inference(sat_conversion,[],[f2650]) ).
cnf(s371,plain,
( ~ spl12_94
| ~ spl12_96 ),
inference(sat_conversion,[],[f2658]) ).
cnf(s372,plain,
( ~ spl12_107
| ~ spl12_108 ),
inference(sat_conversion,[],[f2660]) ).
cnf(s373,plain,
( ~ spl12_28
| ~ spl12_96
| ~ spl12_167
| spl12_200
| ~ spl12_203 ),
inference(sat_conversion,[],[f2675]) ).
cnf(s375,plain,
( ~ spl12_19
| ~ spl12_87
| ~ spl12_162
| ~ spl12_167
| spl12_189 ),
inference(sat_conversion,[],[f2694]) ).
cnf(s376,plain,
( ~ spl12_21
| ~ spl12_89
| ~ spl12_162
| ~ spl12_167
| spl12_190 ),
inference(sat_conversion,[],[f2703]) ).
cnf(s383,plain,
( ~ spl12_41
| spl12_197 ),
inference(sat_conversion,[],[f2761]) ).
cnf(s384,plain,
( ~ spl12_40
| ~ spl12_167
| spl12_198 ),
inference(sat_conversion,[],[f2767]) ).
cnf(s385,plain,
( ~ spl12_34
| ~ spl12_102
| ~ spl12_162
| ~ spl12_167
| spl12_199 ),
inference(sat_conversion,[],[f2774]) ).
cnf(s387,plain,
( ~ spl12_3
| ~ spl12_4 ),
inference(sat_conversion,[],[f2792]) ).
cnf(s388,plain,
( ~ spl12_27
| ~ spl12_28 ),
inference(sat_conversion,[],[f2794]) ).
cnf(s399,plain,
( ~ spl12_73
| ~ spl12_75 ),
inference(sat_conversion,[],[f2886]) ).
cnf(s407,plain,
( ~ spl12_31
| spl12_99
| ~ spl12_167
| ~ spl12_191
| ~ spl12_203 ),
inference(sat_conversion,[],[f2985]) ).
cnf(s417,plain,
( ~ spl12_21
| ~ spl12_23 ),
inference(sat_conversion,[],[f3084]) ).
cnf(s418,plain,
( ~ spl12_21
| ~ spl12_23 ),
inference(sat_conversion,[],[f3086]) ).
cnf(s419,plain,
( ~ spl12_39
| ~ spl12_40 ),
inference(sat_conversion,[],[f3090]) ).
cnf(s423,plain,
( ~ spl12_105
| ~ spl12_108 ),
inference(sat_conversion,[],[f3118]) ).
cnf(s432,plain,
( ~ spl12_75
| ~ spl12_76 ),
inference(sat_conversion,[],[f3183]) ).
cnf(s434,plain,
( ~ spl12_81
| ~ spl12_84 ),
inference(sat_conversion,[],[f3190]) ).
cnf(s435,plain,
( spl12_34
| ~ spl12_41 ),
inference(sat_conversion,[],[f3211]) ).
cnf(s436,plain,
( spl12_35
| ~ spl12_65 ),
inference(sat_conversion,[],[f3218]) ).
cnf(s438,plain,
( ~ spl12_10
| ~ spl12_78
| ~ spl12_162
| ~ spl12_167
| spl12_201 ),
inference(sat_conversion,[],[f3226]) ).
cnf(s439,plain,
( ~ spl12_13
| ~ spl12_81
| ~ spl12_162
| spl12_188
| ~ spl12_203 ),
inference(sat_conversion,[],[f3228]) ).
cnf(s440,plain,
( ~ spl12_30
| ~ spl12_98
| ~ spl12_167
| spl12_191
| ~ spl12_203 ),
inference(sat_conversion,[],[f3231]) ).
cnf(s441,plain,
( ~ spl12_47
| ~ spl12_115
| spl12_196
| ~ spl12_203 ),
inference(sat_conversion,[],[f3232]) ).
cnf(s442,plain,
( ~ spl12_49
| ~ spl12_117
| ~ spl12_162
| spl12_192
| ~ spl12_203 ),
inference(sat_conversion,[],[f3233]) ).
cnf(s443,plain,
( ~ spl12_54
| ~ spl12_122
| ~ spl12_167
| spl12_193
| ~ spl12_203 ),
inference(sat_conversion,[],[f3236]) ).
cnf(s444,plain,
( ~ spl12_59
| ~ spl12_127
| spl12_195
| ~ spl12_203 ),
inference(sat_conversion,[],[f3237]) ).
cnf(s448,plain,
( spl12_102
| ~ spl12_109 ),
inference(sat_conversion,[],[f3255]) ).
cnf(s459,plain,
( ~ spl12_64
| spl12_194
| ~ spl12_203
| ~ spl12_242 ),
inference(sat_conversion,[],[f3377]) ).
cnf(s460,plain,
( spl12_103
| ~ spl12_133 ),
inference(sat_conversion,[],[f3404]) ).
cnf(s462,plain,
( ~ spl12_72
| spl12_204 ),
inference(sat_conversion,[],[f3408]) ).
cnf(s473,plain,
( ~ spl12_5
| ~ spl12_8 ),
inference(sat_conversion,[],[f3539]) ).
cnf(s474,plain,
( ~ spl12_2
| ~ spl12_3 ),
inference(sat_conversion,[],[f3553]) ).
cnf(s498,plain,
~ spl12_43,
inference(sat_conversion,[],[f3702]) ).
cnf(s501,plain,
( ~ spl12_41
| ~ spl12_44 ),
inference(sat_conversion,[],[f3712]) ).
cnf(s505,plain,
( ~ spl12_73
| ~ spl12_76 ),
inference(sat_conversion,[],[f3738]) ).
cnf(s506,plain,
( ~ spl12_73
| ~ spl12_76 ),
inference(sat_conversion,[],[f3740]) ).
cnf(s507,plain,
( ~ spl12_78
| ~ spl12_80 ),
inference(sat_conversion,[],[f3745]) ).
cnf(s508,plain,
( ~ spl12_78
| ~ spl12_80 ),
inference(sat_conversion,[],[f3747]) ).
cnf(s513,plain,
( ~ spl12_70
| ~ spl12_71 ),
inference(sat_conversion,[],[f3770]) ).
cnf(s539,plain,
( ~ spl12_98
| ~ spl12_100 ),
inference(sat_conversion,[],[f3895]) ).
cnf(s541,plain,
( ~ spl12_87
| ~ spl12_88 ),
inference(sat_conversion,[],[f3904]) ).
cnf(s555,plain,
( ~ spl12_89
| ~ spl12_92 ),
inference(sat_conversion,[],[f3968]) ).
cnf(s556,plain,
~ spl12_67,
inference(rat,[],[s178,s498]) ).
cnf(s558,plain,
~ spl12_105,
inference(rat,[],[s423,s146]) ).
cnf(s559,plain,
~ spl12_107,
inference(rat,[],[s372,s146]) ).
cnf(s560,plain,
spl12_203,
inference(rat,[],[s369,s146]) ).
cnf(s561,plain,
~ spl12_134,
inference(rat,[],[s285,s146]) ).
cnf(s562,plain,
~ spl12_135,
inference(rat,[],[s278,s146]) ).
cnf(s563,plain,
~ spl12_39,
inference(rat,[],[s419,s145]) ).
cnf(s564,plain,
spl12_198,
inference(rat,[],[s384,s147,s145]) ).
cnf(s565,plain,
~ spl12_37,
inference(rat,[],[s258,s145]) ).
cnf(s567,plain,
~ spl12_66,
inference(rat,[],[s177,s145]) ).
cnf(s568,plain,
~ spl12_165,
inference(rat,[],[s131,s147]) ).
cnf(s569,plain,
spl12_102,
inference(rat,[],[s448,s108]) ).
cnf(s570,plain,
spl12_162,
inference(rat,[],[s362,s108]) ).
cnf(s571,plain,
~ spl12_110,
inference(rat,[],[s345,s108]) ).
cnf(s572,plain,
~ spl12_103,
inference(rat,[],[s339,s569]) ).
cnf(s573,plain,
~ spl12_161,
inference(rat,[],[s127,s570]) ).
cnf(s575,plain,
~ spl12_133,
inference(rat,[],[s460,s572]) ).
cnf(s576,plain,
~ spl12_44,
inference(rat,[],[s501,s107]) ).
cnf(s577,plain,
spl12_34,
inference(rat,[],[s435,s107]) ).
cnf(s578,plain,
spl12_197,
inference(rat,[],[s383,s107]) ).
cnf(s579,plain,
~ spl12_42,
inference(rat,[],[s246,s107]) ).
cnf(s580,plain,
spl12_199,
inference(rat,[],[s385,s569,s147,s570,s577]) ).
cnf(s581,plain,
~ spl12_36,
inference(rat,[],[s244,s577]) ).
cnf(s582,plain,
~ spl12_35,
inference(rat,[],[s242,s577]) ).
cnf(s583,plain,
~ spl12_65,
inference(rat,[],[s436,s582]) ).
cnf(s587,plain,
( spl12_78
| spl12_94
| spl12_126 ),
inference(rat,[],[s85,s571]) ).
cnf(s588,plain,
( spl12_75
| spl12_91
| spl12_123 ),
inference(rat,[],[s79,s559]) ).
cnf(s590,plain,
( spl12_73
| spl12_89
| spl12_121 ),
inference(rat,[],[s75,s558]) ).
cnf(s591,plain,
( spl12_71
| spl12_87
| spl12_119 ),
inference(rat,[],[s71,s572]) ).
cnf(s592,plain,
spl12_136,
inference(rat,[],[s66,s562,s561,s575]) ).
cnf(s594,plain,
~ spl12_83,
inference(rat,[],[s309,s592]) ).
cnf(s595,plain,
~ spl12_119,
inference(rat,[],[s308,s592]) ).
cnf(s596,plain,
~ spl12_82,
inference(rat,[],[s293,s592]) ).
cnf(s598,plain,
spl12_98,
inference(rat,[],[s291,s592]) ).
cnf(s599,plain,
spl12_122,
inference(rat,[],[s290,s592]) ).
cnf(s600,plain,
spl12_115,
inference(rat,[],[s289,s592]) ).
cnf(s601,plain,
spl12_127,
inference(rat,[],[s288,s592]) ).
cnf(s602,plain,
spl12_132,
inference(rat,[],[s286,s592]) ).
cnf(s603,plain,
~ spl12_100,
inference(rat,[],[s539,s598]) ).
cnf(s604,plain,
~ spl12_99,
inference(rat,[],[s335,s598]) ).
cnf(s605,plain,
~ spl12_97,
inference(rat,[],[s330,s598]) ).
cnf(s606,plain,
~ spl12_123,
inference(rat,[],[s351,s599]) ).
cnf(s607,plain,
~ spl12_121,
inference(rat,[],[s349,s599]) ).
cnf(s608,plain,
~ spl12_113,
inference(rat,[],[s347,s600]) ).
cnf(s609,plain,
~ spl12_125,
inference(rat,[],[s353,s601]) ).
cnf(s610,plain,
~ spl12_126,
inference(rat,[],[s324,s601]) ).
cnf(s612,plain,
spl12_242,
inference(rat,[],[s365,s602]) ).
cnf(s613,plain,
~ spl12_129,
inference(rat,[],[s355,s602]) ).
cnf(s614,plain,
spl12_81,
inference(rat,[],[s91,s613,s608,s605]) ).
cnf(s615,plain,
spl12_117,
inference(rat,[],[s92,s613,s609,s607]) ).
cnf(s617,plain,
~ spl12_84,
inference(rat,[],[s434,s614]) ).
cnf(s618,plain,
( spl12_12
| spl12_28
| spl12_60 ),
inference(rat,[],[s40,s576]) ).
cnf(s619,plain,
spl12_47,
inference(rat,[],[s39,s498,s563,s582]) ).
cnf(s620,plain,
spl12_196,
inference(rat,[],[s441,s560,s600,s619]) ).
cnf(s621,plain,
~ spl12_45,
inference(rat,[],[s255,s619]) ).
cnf(s624,plain,
( spl12_10
| spl12_26
| spl12_58 ),
inference(rat,[],[s36,s579]) ).
cnf(s625,plain,
( spl12_7
| spl12_23
| spl12_55 ),
inference(rat,[],[s30,s563]) ).
cnf(s627,plain,
( spl12_5
| spl12_21
| spl12_53 ),
inference(rat,[],[s26,s565]) ).
cnf(s628,plain,
( spl12_4
| spl12_20
| spl12_52 ),
inference(rat,[],[s24,s581]) ).
cnf(s629,plain,
( spl12_3
| spl12_19
| spl12_51 ),
inference(rat,[],[s22,s582]) ).
cnf(s630,plain,
spl12_68,
inference(rat,[],[s17,s556,s567,s583]) ).
cnf(s631,plain,
spl12_64,
inference(rat,[],[s193,s630]) ).
cnf(s632,plain,
spl12_59,
inference(rat,[],[s192,s630]) ).
cnf(s633,plain,
~ spl12_16,
inference(rat,[],[s191,s630]) ).
cnf(s634,plain,
~ spl12_52,
inference(rat,[],[s190,s630]) ).
cnf(s635,plain,
~ spl12_15,
inference(rat,[],[s189,s630]) ).
cnf(s636,plain,
~ spl12_51,
inference(rat,[],[s188,s630]) ).
cnf(s637,plain,
~ spl12_14,
inference(rat,[],[s187,s630]) ).
cnf(s639,plain,
spl12_30,
inference(rat,[],[s185,s630]) ).
cnf(s640,plain,
spl12_54,
inference(rat,[],[s184,s630]) ).
cnf(s641,plain,
spl12_194,
inference(rat,[],[s459,s612,s560,s631]) ).
cnf(s643,plain,
~ spl12_61,
inference(rat,[],[s269,s631]) ).
cnf(s644,plain,
spl12_195,
inference(rat,[],[s444,s560,s601,s632]) ).
cnf(s645,plain,
~ spl12_60,
inference(rat,[],[s267,s632]) ).
cnf(s646,plain,
~ spl12_57,
inference(rat,[],[s265,s632]) ).
cnf(s647,plain,
~ spl12_58,
inference(rat,[],[s249,s632]) ).
cnf(s648,plain,
spl12_191,
inference(rat,[],[s440,s560,s598,s147,s639]) ).
cnf(s649,plain,
~ spl12_32,
inference(rat,[],[s220,s639]) ).
cnf(s650,plain,
~ spl12_29,
inference(rat,[],[s218,s639]) ).
cnf(s651,plain,
spl12_193,
inference(rat,[],[s443,s560,s599,s147,s640]) ).
cnf(s653,plain,
~ spl12_55,
inference(rat,[],[s261,s640]) ).
cnf(s654,plain,
~ spl12_53,
inference(rat,[],[s257,s640]) ).
cnf(s655,plain,
~ spl12_31,
inference(rat,[],[s407,s560,s604,s147,s648]) ).
cnf(s656,plain,
spl12_13,
inference(rat,[],[s42,s643,s621,s650]) ).
cnf(s657,plain,
spl12_49,
inference(rat,[],[s43,s643,s646,s654]) ).
cnf(s658,plain,
spl12_188,
inference(rat,[],[s439,s560,s614,s570,s656]) ).
cnf(s659,plain,
spl12_192,
inference(rat,[],[s442,s560,s615,s570,s657]) ).
cnf(s660,plain,
( ~ spl12_89
| ~ spl12_186
| ~ spl12_189
| spl12_88
| ~ spl12_10
| ~ spl12_28
| ~ spl12_21 ),
inference(rat,[],[s438,s153,s587,s370,s371,s373,s588,s82,s343,s376,s555,s625,s418,s570,s147,s150,s568,s573,s658,s648,s659,s651,s641,s644,s620,s578,s564,s580,s560,s610,s606,s603,s653]) ).
cnf(s661,plain,
( spl12_71
| spl12_70
| spl12_69
| ~ spl12_10
| ~ spl12_21
| ~ spl12_4
| ~ spl12_19 ),
inference(rat,[],[s294,s70,s72,s271,s399,s590,s660,s364,s462,s375,s541,s50,s591,s33,s253,s238,s596,s594,s607,s570,s560,s147,s595,s649]) ).
cnf(s662,plain,
( ~ spl12_75
| spl12_72
| spl12_70 ),
inference(rat,[],[s507,s70,s74,s328,s432,s596,s617]) ).
cnf(s663,plain,
( spl12_72
| spl12_70 ),
inference(rat,[],[s507,s70,s74,s271,s506,s590,s343,s588,s662,s606,s607,s617,s596]) ).
cnf(s664,plain,
( spl12_70
| spl12_69
| ~ spl12_19
| ~ spl12_10
| ~ spl12_21
| ~ spl12_4 ),
inference(rat,[],[s663,s326,s661]) ).
cnf(s665,plain,
( ~ spl12_75
| ~ spl12_70 ),
inference(rat,[],[s371,s82,s587,s555,s508,s590,s74,s399,s432,s341,s541,s591,s513,s603,s610,s607,s617,s595]) ).
cnf(s666,plain,
~ spl12_70,
inference(rat,[],[s505,s74,s590,s297,s343,s72,s588,s665,s341,s513,s617,s607,s594,s606]) ).
cnf(s668,plain,
spl12_72,
inference(rat,[],[s663,s666]) ).
cnf(s669,plain,
~ spl12_69,
inference(rat,[],[s311,s668]) ).
cnf(s678,plain,
( ~ spl12_10
| ~ spl12_4
| ~ spl12_19 ),
inference(rat,[],[s239,s27,s618,s664,s236,s222,s650,s645,s666,s669]) ).
cnf(s679,plain,
( spl12_3
| spl12_2
| spl12_1 ),
inference(rat,[],[s200,s23,s618,s197,s247,s21,s624,s678,s1,s629,s635,s645,s637,s647,s636]) ).
cnf(s680,plain,
( spl12_12
| spl12_4 ),
inference(rat,[],[s417,s627,s31,s473,s388,s25,s618,s238,s628,s654,s655,s633,s645,s634]) ).
cnf(s681,plain,
( spl12_2
| spl12_1 ),
inference(rat,[],[s417,s627,s31,s195,s215,s21,s624,s236,s680,s238,s628,s387,s679,s634,s647,s637,s655,s654]) ).
cnf(s682,plain,
~ spl12_2,
inference(rat,[],[s237,s628,s629,s251,s474,s634,s636]) ).
cnf(s683,plain,
spl12_1,
inference(rat,[],[s681,s682]) ).
cnf(s685,plain,
~ spl12_4,
inference(rat,[],[s232,s683]) ).
cnf(s686,plain,
~ spl12_3,
inference(rat,[],[s230,s683]) ).
cnf(s689,plain,
spl12_20,
inference(rat,[],[s628,s634,s685]) ).
cnf(s691,plain,
spl12_19,
inference(rat,[],[s629,s636,s686]) ).
cnf(s693,plain,
$false,
inference(rat,[],[s237,s689,s691]) ).
fof(f3969,plain,
$false,
inference(avatar_sat_refutation,[],[s693]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG038+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.17 % Computer : n015.cluster.edu
% 0.11/0.17 % Model : x86_64 x86_64
% 0.11/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.17 % Memory : 8046.5625MB
% 0.11/0.17 % OS : Linux 6.8.0-71-generic
% 0.11/0.17 % CPULimit : 300
% 0.11/0.17 % WCLimit : 300
% 0.11/0.17 % DateTime : Mon Sep 28 19:23:17 UTC 2026
% 0.11/0.17 % CPUTime :
% 0.11/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.21 Running first-order theorem proving
% 0.11/0.21 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
% 4.70/1.32 % (2928296)Detected formulas, will run a generic FOF schedule.
% 4.70/1.32 % (2928305)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2497708479:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.70/1.32 % (2928305)Instruction limit reached!
% 4.70/1.32 % (2928305)------------------------------
% 4.70/1.32 % (2928305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.32 % (2928305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.32 % (2928305)CaDiCaL version: 2.1.3
% 4.70/1.32 % (2928305)Termination reason: Instruction limit
% 4.70/1.32 % (2928305)Termination phase: Saturation
% 4.70/1.32 % (2928305)Time elapsed: 0.026 s
% 4.70/1.32 % (2928305)Peak memory usage: 88 MB
% 4.70/1.32 % (2928305)Instructions burned: 120 (million)
% 4.70/1.32 % (2928306)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1955926857:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.70/1.32 % (2928301)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=3200619413:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.70/1.32 % (2928304)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2521609985:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.70/1.32 % (2928302)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=3089613452:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.70/1.32 % (2928303)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=4001606800:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.70/1.32 % (2928307)dis-21_1_sil=8000:lcm=predicate:random_seed=1077162983:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.70/1.32 % (2928307)Refutation not found, incomplete strategy
% 4.70/1.32 % (2928307)------------------------------
% 4.70/1.32 % (2928307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.32 % (2928307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.32 % (2928307)CaDiCaL version: 2.1.3
% 4.70/1.32 % (2928307)Termination reason: Refutation not found, incomplete strategy
% 4.70/1.32 % (2928307)Time elapsed: 0.016 s
% 4.70/1.32 % (2928307)Peak memory usage: 89 MB
% 4.70/1.32 % (2928307)Instructions burned: 31 (million)
% 4.70/1.32 % (2928304)Instruction limit reached!
% 4.70/1.32 % (2928304)------------------------------
% 4.70/1.32 % (2928304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.32 % (2928304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.32 % (2928304)CaDiCaL version: 2.1.3
% 4.70/1.32 % (2928304)Termination reason: Instruction limit
% 4.70/1.32 % (2928304)Termination phase: Saturation
% 4.70/1.32 % (2928304)Time elapsed: 0.050 s
% 4.70/1.32 % (2928304)Peak memory usage: 90 MB
% 4.70/1.32 % (2928304)Instructions burned: 111 (million)
% 4.70/1.32 % (2928309)lrs+10_1_sil=8000:sp=occurrence:random_seed=3559358132:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 4.70/1.32 % (2928306)Instruction limit reached!
% 4.70/1.32 % (2928306)------------------------------
% 4.70/1.32 % (2928306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.32 % (2928306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.32 % (2928306)CaDiCaL version: 2.1.3
% 4.70/1.32 % (2928306)Termination reason: Instruction limit
% 4.70/1.32 % (2928306)Termination phase: Saturation
% 4.70/1.32 % (2928306)Time elapsed: 0.072 s
% 4.70/1.32 % (2928306)Peak memory usage: 89 MB
% 4.70/1.32 % (2928306)Instructions burned: 140 (million)
% 4.70/1.32 % (2928309)Refutation not found, incomplete strategy
% 4.70/1.32 % (2928309)------------------------------
% 4.70/1.32 % (2928309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.32 % (2928309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.32 % (2928309)CaDiCaL version: 2.1.3
% 4.70/1.32 % (2928309)Termination reason: Refutation not found, incomplete strategy
% 4.70/1.32 % (2928309)Time elapsed: 0.035 s
% 4.70/1.32 % (2928309)Peak memory usage: 90 MB
% 4.70/1.32 % (2928309)Instructions burned: 132 (million)
% 4.70/1.34 % (2928316)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1599813518:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.70/1.34 % (2928318)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2267169162:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 4.70/1.34 % (2928309)------------------------------
% 4.70/1.34 % (2928309)------------------------------
% 4.70/1.34 % (2928318)First to succeed.
% 4.70/1.34 % (2928307)------------------------------
% 4.70/1.34 % (2928307)------------------------------
% 4.70/1.34 % (2928316)Refutation not found, incomplete strategy
% 4.70/1.34 % (2928316)------------------------------
% 4.70/1.34 % (2928316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.34 % (2928316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.34 % (2928316)CaDiCaL version: 2.1.3
% 4.70/1.34 % (2928316)Termination reason: Refutation not found, incomplete strategy
% 4.70/1.34 % (2928316)Time elapsed: 0.076 s
% 4.70/1.34 % (2928316)Peak memory usage: 90 MB
% 4.70/1.34 % (2928316)Instructions burned: 148 (million)
% 4.70/1.34 % (2928318)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2928296"
% 4.70/1.34 % (2928321)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=965544755:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 4.70/1.34 [W928 19:23:18.320140132 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.320173505 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.320209425 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.320222206 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.320248682 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.320259989 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.320346923 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.320373813 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.320410550 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.320422957 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.320449334 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.320473694 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.321846040 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.321878887 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.321915547 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.321927124 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.321956994 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 [W928 19:23:18.321979027 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.70/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.34 % (2928322)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1482236370:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 4.70/1.34 % (2928321)Instruction limit reached!
% 4.70/1.34 % (2928321)------------------------------
% 4.70/1.34 % (2928321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.34 % (2928321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.34 % (2928321)CaDiCaL version: 2.1.3
% 4.70/1.34 % (2928321)Termination reason: Instruction limit
% 4.70/1.34 % (2928321)Termination phase: Saturation
% 4.70/1.34 % (2928321)Time elapsed: 0.078 s
% 4.70/1.34 % (2928321)Peak memory usage: 91 MB
% 4.70/1.34 % (2928321)Instructions burned: 248 (million)
% 4.70/1.34 % (2928316)------------------------------
% 4.70/1.34 % (2928316)------------------------------
% 4.70/1.34 % (2928326)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3046436408:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 4.70/1.34 % (2928322)Instruction limit reached!
% 4.70/1.34 % (2928322)------------------------------
% 4.70/1.34 % (2928322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.34 % (2928322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.34 % (2928322)CaDiCaL version: 2.1.3
% 4.70/1.34 % (2928322)Termination reason: Instruction limit
% 4.70/1.34 % (2928322)Termination phase: Saturation
% 4.70/1.34 % (2928322)Time elapsed: 0.105 s
% 4.70/1.34 % (2928322)Peak memory usage: 88 MB
% 4.70/1.34 % (2928322)Instructions burned: 295 (million)
% 4.70/1.34 % (2928318)Refutation found. Thanks to Tanya!
% 4.70/1.34 % SZS status Theorem for theBenchmark
% 4.70/1.34 % SZS output start Proof for theBenchmark
% See solution above
% 5.46/1.54 % (2928318)------------------------------
% 5.46/1.54 % (2928318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.46/1.54 % (2928318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.46/1.54 % (2928318)CaDiCaL version: 2.1.3
% 5.46/1.54 % (2928318)Termination reason: Refutation
% 5.46/1.54 % (2928318)Time elapsed: 0.078 s
% 5.46/1.54 % (2928318)Peak memory usage: 91 MB
% 5.46/1.54 % (2928318)Instructions burned: 158 (million)
% 5.46/1.54 % (2928318)------------------------------
% 5.46/1.54 % (2928318)------------------------------
% 5.46/1.54 % (2928296)Success in time 0.692 s
% 5.46/1.54 % Vampire exiting
%------------------------------------------------------------------------------