%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG121+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 : n019.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:11:57 AM UTC 2026
% Result : Theorem 3.67s 1.17s
% Output : Refutation 4.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 192
% Syntax : Number of formulae : 1072 ( 152 unt; 176 def)
% Number of atoms : 4132 (2143 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 5043 (1983 ~;2240 |; 686 &)
% ( 134 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 178 ( 176 usr; 177 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,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',ax2) ).
fof(f3,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',ax3) ).
fof(f4,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',ax4) ).
fof(f5,axiom,
( op1(e10,e10) != op1(e11,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e12,e10) != op1(e13,e10)
& op1(e10,e11) != op1(e11,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e12,e11) != op1(e13,e11)
& op1(e10,e12) != op1(e11,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e12,e12) != op1(e13,e12)
& op1(e10,e13) != op1(e11,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e12,e13) != op1(e13,e13)
& op1(e10,e10) != op1(e10,e11)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e12) != op1(e10,e13)
& op1(e11,e10) != op1(e11,e11)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e12) != op1(e11,e13)
& op1(e12,e10) != op1(e12,e11)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e12) != op1(e12,e13)
& op1(e13,e10) != op1(e13,e11)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e12) != op1(e13,e13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( op2(e20,e20) != op2(e21,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e22,e20) != op2(e23,e20)
& op2(e20,e21) != op2(e21,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e22,e21) != op2(e23,e21)
& op2(e20,e22) != op2(e21,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e22,e22) != op2(e23,e22)
& op2(e20,e23) != op2(e21,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e22,e23) != op2(e23,e23)
& op2(e20,e20) != op2(e20,e21)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e22) != op2(e20,e23)
& op2(e21,e20) != op2(e21,e21)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e22) != op2(e21,e23)
& op2(e22,e20) != op2(e22,e21)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e22) != op2(e22,e23)
& op2(e23,e20) != op2(e23,e21)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e22) != op2(e23,e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
fof(f10,axiom,
( ( op1(e10,e10) = e10
| op1(e11,e11) = e11
| op1(e12,e12) = e12
| op1(e13,e13) = e13 )
& ( op1(e10,e10) != e10
| op1(e10,e10) = e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) = e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) = e10 )
& ( op1(e10,e10) != e13
| op1(e10,e13) = e10 )
& ( op1(e11,e11) != e10
| op1(e11,e10) = e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) = e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) = e11 )
& ( op1(e11,e11) != e13
| op1(e11,e13) = e11 )
& ( op1(e12,e12) != e10
| op1(e12,e10) = e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) = e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) = e12 )
& ( op1(e12,e12) != e13
| op1(e12,e13) = e12 )
& ( op1(e13,e13) != e10
| op1(e13,e10) = e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) = e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) = e13 )
& ( op1(e13,e13) != e13
| op1(e13,e13) = e13 )
& ( ( op1(e10,e10) = e10
& op1(e10,e10) = e10
& op1(e10,e10) != e10 )
| ( op1(e10,e11) = e10
& op1(e11,e10) = e10
& op1(e11,e11) != e11 )
| ( op1(e10,e12) = e10
& op1(e12,e10) = e10
& op1(e12,e12) != e12 )
| ( op1(e10,e13) = e10
& op1(e13,e10) = e10
& op1(e13,e13) != e13 )
| ( op1(e11,e10) = e11
& op1(e10,e11) = e11
& op1(e10,e10) != e10 )
| ( op1(e11,e11) = e11
& op1(e11,e11) = e11
& op1(e11,e11) != e11 )
| ( op1(e11,e12) = e11
& op1(e12,e11) = e11
& op1(e12,e12) != e12 )
| ( op1(e11,e13) = e11
& op1(e13,e11) = e11
& op1(e13,e13) != e13 )
| ( op1(e12,e10) = e12
& op1(e10,e12) = e12
& op1(e10,e10) != e10 )
| ( op1(e12,e11) = e12
& op1(e11,e12) = e12
& op1(e11,e11) != e11 )
| ( op1(e12,e12) = e12
& op1(e12,e12) = e12
& op1(e12,e12) != e12 )
| ( op1(e12,e13) = e12
& op1(e13,e12) = e12
& op1(e13,e13) != e13 )
| ( op1(e13,e10) = e13
& op1(e10,e13) = e13
& op1(e10,e10) != e10 )
| ( op1(e13,e11) = e13
& op1(e11,e13) = e13
& op1(e11,e11) != e11 )
| ( op1(e13,e12) = e13
& op1(e12,e13) = e13
& op1(e12,e12) != e12 )
| ( op1(e13,e13) = e13
& op1(e13,e13) = e13
& op1(e13,e13) != e13 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( ( op2(e20,e20) = e20
| op2(e21,e21) = e21
| op2(e22,e22) = e22
| op2(e23,e23) = e23 )
& ( op2(e20,e20) != e20
| op2(e20,e20) = e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) = e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) = e20 )
& ( op2(e20,e20) != e23
| op2(e20,e23) = e20 )
& ( op2(e21,e21) != e20
| op2(e21,e20) = e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) = e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) = e21 )
& ( op2(e21,e21) != e23
| op2(e21,e23) = e21 )
& ( op2(e22,e22) != e20
| op2(e22,e20) = e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) = e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) = e22 )
& ( op2(e22,e22) != e23
| op2(e22,e23) = e22 )
& ( op2(e23,e23) != e20
| op2(e23,e20) = e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) = e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) = e23 )
& ( op2(e23,e23) != e23
| op2(e23,e23) = e23 )
& ( ( op2(e20,e20) = e20
& op2(e20,e20) = e20
& op2(e20,e20) != e20 )
| ( op2(e20,e21) = e20
& op2(e21,e20) = e20
& op2(e21,e21) != e21 )
| ( op2(e20,e22) = e20
& op2(e22,e20) = e20
& op2(e22,e22) != e22 )
| ( op2(e20,e23) = e20
& op2(e23,e20) = e20
& op2(e23,e23) != e23 )
| ( op2(e21,e20) = e21
& op2(e20,e21) = e21
& op2(e20,e20) != e20 )
| ( op2(e21,e21) = e21
& op2(e21,e21) = e21
& op2(e21,e21) != e21 )
| ( op2(e21,e22) = e21
& op2(e22,e21) = e21
& op2(e22,e22) != e22 )
| ( op2(e21,e23) = e21
& op2(e23,e21) = e21
& op2(e23,e23) != e23 )
| ( op2(e22,e20) = e22
& op2(e20,e22) = e22
& op2(e20,e20) != e20 )
| ( op2(e22,e21) = e22
& op2(e21,e22) = e22
& op2(e21,e21) != e21 )
| ( op2(e22,e22) = e22
& op2(e22,e22) = e22
& op2(e22,e22) != e22 )
| ( op2(e22,e23) = e22
& op2(e23,e22) = e22
& op2(e23,e23) != e23 )
| ( op2(e23,e20) = e23
& op2(e20,e23) = e23
& op2(e20,e20) != e20 )
| ( op2(e23,e21) = e23
& op2(e21,e23) = e23
& op2(e21,e21) != e21 )
| ( op2(e23,e22) = e23
& op2(e22,e23) = e23
& op2(e22,e22) != e22 )
| ( op2(e23,e23) = e23
& op2(e23,e23) = e23
& op2(e23,e23) != e23 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e10 = op1(e13,e13)
& e11 = op1(op1(e13,e13),op1(e13,e13))
& e12 = op1(op1(op1(e13,e13),op1(e13,e13)),e13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e20 = op2(e23,e23)
& e21 = op2(op2(e23,e23),op2(e23,e23))
& e22 = op2(op2(op2(e23,e23),op2(e23,e23)),e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( h1(e13) = e20
& h1(e10) = op2(e20,e20)
& h1(e11) = op2(op2(e20,e20),op2(e20,e20))
& h1(e12) = op2(op2(op2(e20,e20),op2(e20,e20)),e20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
( h2(e13) = e21
& h2(e10) = op2(e21,e21)
& h2(e11) = op2(op2(e21,e21),op2(e21,e21))
& h2(e12) = op2(op2(op2(e21,e21),op2(e21,e21)),e21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
( h3(e13) = e22
& h3(e10) = op2(e22,e22)
& h3(e11) = op2(op2(e22,e22),op2(e22,e22))
& h3(e12) = op2(op2(op2(e22,e22),op2(e22,e22)),e22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
( h4(e13) = e23
& h4(e10) = op2(e23,e23)
& h4(e11) = op2(op2(e23,e23),op2(e23,e23))
& h4(e12) = op2(op2(op2(e23,e23),op2(e23,e23)),e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
fof(f18,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(f19,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)],[f18]) ).
fof(f20,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,[],[f19]) ).
fof(f21,definition,
( ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f22,definition,
( ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f25,definition,
( ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f26,definition,
( ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f27,definition,
( ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f29,definition,
( ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f30,definition,
( ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f31,definition,
( ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f32,definition,
( ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f33,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,[],[f20,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21]) ).
fof(f34,definition,
( ( op1(e13,e13) = e13
& op1(e13,e13) = e13
& op1(e13,e13) != e13 )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f35,definition,
( ( op1(e13,e12) = e13
& op1(e12,e13) = e13
& op1(e12,e12) != e12 )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f36,definition,
( ( op1(e13,e11) = e13
& op1(e11,e13) = e13
& op1(e11,e11) != e11 )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f37,definition,
( ( op1(e13,e10) = e13
& op1(e10,e13) = e13
& op1(e10,e10) != e10 )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f38,definition,
( ( op1(e12,e13) = e12
& op1(e13,e12) = e12
& op1(e13,e13) != e13 )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f39,definition,
( ( op1(e12,e12) = e12
& op1(e12,e12) = e12
& op1(e12,e12) != e12 )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f40,definition,
( ( op1(e12,e11) = e12
& op1(e11,e12) = e12
& op1(e11,e11) != e11 )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f41,definition,
( ( op1(e12,e10) = e12
& op1(e10,e12) = e12
& op1(e10,e10) != e10 )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f42,definition,
( ( op1(e11,e13) = e11
& op1(e13,e11) = e11
& op1(e13,e13) != e13 )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f43,definition,
( ( op1(e11,e12) = e11
& op1(e12,e11) = e11
& op1(e12,e12) != e12 )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f44,definition,
( ( op1(e11,e11) = e11
& op1(e11,e11) = e11
& op1(e11,e11) != e11 )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f45,definition,
( ( op1(e11,e10) = e11
& op1(e10,e11) = e11
& op1(e10,e10) != e10 )
| ~ sP23 ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f46,definition,
( ( op1(e10,e13) = e10
& op1(e13,e10) = e10
& op1(e13,e13) != e13 )
| ~ sP24 ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f47,definition,
( ( op1(e10,e12) = e10
& op1(e12,e10) = e10
& op1(e12,e12) != e12 )
| ~ sP25 ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f48,definition,
( ( op1(e10,e11) = e10
& op1(e11,e10) = e10
& op1(e11,e11) != e11 )
| ~ sP26 ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f49,plain,
( ( op1(e10,e10) = e10
| op1(e11,e11) = e11
| op1(e12,e12) = e12
| op1(e13,e13) = e13 )
& ( op1(e10,e10) != e10
| op1(e10,e10) = e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) = e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) = e10 )
& ( op1(e10,e10) != e13
| op1(e10,e13) = e10 )
& ( op1(e11,e11) != e10
| op1(e11,e10) = e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) = e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) = e11 )
& ( op1(e11,e11) != e13
| op1(e11,e13) = e11 )
& ( op1(e12,e12) != e10
| op1(e12,e10) = e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) = e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) = e12 )
& ( op1(e12,e12) != e13
| op1(e12,e13) = e12 )
& ( op1(e13,e13) != e10
| op1(e13,e10) = e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) = e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) = e13 )
& ( op1(e13,e13) != e13
| op1(e13,e13) = e13 )
& ( ( op1(e10,e10) = e10
& op1(e10,e10) = e10
& op1(e10,e10) != e10 )
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12 ) ),
inference(definition_folding,[],[f10,f48,f47,f46,f45,f44,f43,f42,f41,f40,f39,f38,f37,f36,f35,f34]) ).
fof(f50,definition,
( ( op2(e23,e23) = e23
& op2(e23,e23) = e23
& op2(e23,e23) != e23 )
| ~ sP27 ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f51,definition,
( ( op2(e23,e22) = e23
& op2(e22,e23) = e23
& op2(e22,e22) != e22 )
| ~ sP28 ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f52,definition,
( ( op2(e23,e21) = e23
& op2(e21,e23) = e23
& op2(e21,e21) != e21 )
| ~ sP29 ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f53,definition,
( ( op2(e23,e20) = e23
& op2(e20,e23) = e23
& op2(e20,e20) != e20 )
| ~ sP30 ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f54,definition,
( ( op2(e22,e23) = e22
& op2(e23,e22) = e22
& op2(e23,e23) != e23 )
| ~ sP31 ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f55,definition,
( ( op2(e22,e22) = e22
& op2(e22,e22) = e22
& op2(e22,e22) != e22 )
| ~ sP32 ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f56,definition,
( ( op2(e22,e21) = e22
& op2(e21,e22) = e22
& op2(e21,e21) != e21 )
| ~ sP33 ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f57,definition,
( ( op2(e22,e20) = e22
& op2(e20,e22) = e22
& op2(e20,e20) != e20 )
| ~ sP34 ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f58,definition,
( ( op2(e21,e23) = e21
& op2(e23,e21) = e21
& op2(e23,e23) != e23 )
| ~ sP35 ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f59,definition,
( ( op2(e21,e22) = e21
& op2(e22,e21) = e21
& op2(e22,e22) != e22 )
| ~ sP36 ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f60,definition,
( ( op2(e21,e21) = e21
& op2(e21,e21) = e21
& op2(e21,e21) != e21 )
| ~ sP37 ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f61,definition,
( ( op2(e21,e20) = e21
& op2(e20,e21) = e21
& op2(e20,e20) != e20 )
| ~ sP38 ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f62,definition,
( ( op2(e20,e23) = e20
& op2(e23,e20) = e20
& op2(e23,e23) != e23 )
| ~ sP39 ),
introduced(definition,[new_symbols(definition,[sP39])],[predicate_definition_introduction]) ).
fof(f63,definition,
( ( op2(e20,e22) = e20
& op2(e22,e20) = e20
& op2(e22,e22) != e22 )
| ~ sP40 ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f64,definition,
( ( op2(e20,e21) = e20
& op2(e21,e20) = e20
& op2(e21,e21) != e21 )
| ~ sP41 ),
introduced(definition,[new_symbols(definition,[sP41])],[predicate_definition_introduction]) ).
fof(f65,plain,
( ( op2(e20,e20) = e20
| op2(e21,e21) = e21
| op2(e22,e22) = e22
| op2(e23,e23) = e23 )
& ( op2(e20,e20) != e20
| op2(e20,e20) = e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) = e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) = e20 )
& ( op2(e20,e20) != e23
| op2(e20,e23) = e20 )
& ( op2(e21,e21) != e20
| op2(e21,e20) = e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) = e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) = e21 )
& ( op2(e21,e21) != e23
| op2(e21,e23) = e21 )
& ( op2(e22,e22) != e20
| op2(e22,e20) = e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) = e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) = e22 )
& ( op2(e22,e22) != e23
| op2(e22,e23) = e22 )
& ( op2(e23,e23) != e20
| op2(e23,e20) = e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) = e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) = e23 )
& ( op2(e23,e23) != e23
| op2(e23,e23) = e23 )
& ( ( op2(e20,e20) = e20
& op2(e20,e20) = e20
& op2(e20,e20) != e20 )
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP29
| sP28
| sP27 ) ),
inference(definition_folding,[],[f11,f64,f63,f62,f61,f60,f59,f58,f57,f56,f55,f54,f53,f52,f51,f50]) ).
fof(f72,plain,
( ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ~ sP5 ),
inference(nnf_transformation,[],[f26]) ).
fof(f73,plain,
( ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ~ sP4 ),
inference(nnf_transformation,[],[f25]) ).
fof(f74,plain,
( ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) )
| ~ sP3 ),
inference(nnf_transformation,[],[f24]) ).
fof(f78,plain,
( ( op1(e10,e11) = e10
& op1(e11,e10) = e10
& op1(e11,e11) != e11 )
| ~ sP26 ),
inference(nnf_transformation,[],[f48]) ).
fof(f79,plain,
( ( op1(e10,e12) = e10
& op1(e12,e10) = e10
& op1(e12,e12) != e12 )
| ~ sP25 ),
inference(nnf_transformation,[],[f47]) ).
fof(f80,plain,
( ( op1(e10,e13) = e10
& op1(e13,e10) = e10
& op1(e13,e13) != e13 )
| ~ sP24 ),
inference(nnf_transformation,[],[f46]) ).
fof(f81,plain,
( ( op1(e11,e10) = e11
& op1(e10,e11) = e11
& op1(e10,e10) != e10 )
| ~ sP23 ),
inference(nnf_transformation,[],[f45]) ).
fof(f82,plain,
( ( op1(e11,e11) = e11
& op1(e11,e11) = e11
& op1(e11,e11) != e11 )
| ~ sP22 ),
inference(nnf_transformation,[],[f44]) ).
fof(f83,plain,
( ( op1(e11,e12) = e11
& op1(e12,e11) = e11
& op1(e12,e12) != e12 )
| ~ sP21 ),
inference(nnf_transformation,[],[f43]) ).
fof(f84,plain,
( ( op1(e11,e13) = e11
& op1(e13,e11) = e11
& op1(e13,e13) != e13 )
| ~ sP20 ),
inference(nnf_transformation,[],[f42]) ).
fof(f85,plain,
( ( op1(e12,e10) = e12
& op1(e10,e12) = e12
& op1(e10,e10) != e10 )
| ~ sP19 ),
inference(nnf_transformation,[],[f41]) ).
fof(f86,plain,
( ( op1(e12,e11) = e12
& op1(e11,e12) = e12
& op1(e11,e11) != e11 )
| ~ sP18 ),
inference(nnf_transformation,[],[f40]) ).
fof(f87,plain,
( ( op1(e12,e12) = e12
& op1(e12,e12) = e12
& op1(e12,e12) != e12 )
| ~ sP17 ),
inference(nnf_transformation,[],[f39]) ).
fof(f88,plain,
( ( op1(e12,e13) = e12
& op1(e13,e12) = e12
& op1(e13,e13) != e13 )
| ~ sP16 ),
inference(nnf_transformation,[],[f38]) ).
fof(f89,plain,
( ( op1(e13,e10) = e13
& op1(e10,e13) = e13
& op1(e10,e10) != e10 )
| ~ sP15 ),
inference(nnf_transformation,[],[f37]) ).
fof(f90,plain,
( ( op1(e13,e11) = e13
& op1(e11,e13) = e13
& op1(e11,e11) != e11 )
| ~ sP14 ),
inference(nnf_transformation,[],[f36]) ).
fof(f91,plain,
( ( op1(e13,e12) = e13
& op1(e12,e13) = e13
& op1(e12,e12) != e12 )
| ~ sP13 ),
inference(nnf_transformation,[],[f35]) ).
fof(f92,plain,
( ( op1(e13,e13) = e13
& op1(e13,e13) = e13
& op1(e13,e13) != e13 )
| ~ sP12 ),
inference(nnf_transformation,[],[f34]) ).
fof(f134,plain,
( e21 != h3(e11)
| ~ sP5 ),
inference(cnf_transformation,[],[f72]) ).
fof(f136,plain,
( e22 != h3(e13)
| ~ sP4 ),
inference(cnf_transformation,[],[f73]) ).
fof(f141,plain,
( e23 != h3(e12)
| ~ sP3 ),
inference(cnf_transformation,[],[f74]) ).
fof(f163,plain,
( 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)
| sP5
| sP4
| sP3 ),
inference(cnf_transformation,[],[f33]) ).
fof(f172,plain,
e12 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f173,plain,
e11 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f174,plain,
e11 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f175,plain,
e10 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f176,plain,
e10 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f177,plain,
e10 != e11,
inference(cnf_transformation,[],[f7]) ).
fof(f178,plain,
e12 = op1(op1(op1(e13,e13),op1(e13,e13)),e13),
inference(cnf_transformation,[],[f12]) ).
fof(f179,plain,
e11 = op1(op1(e13,e13),op1(e13,e13)),
inference(cnf_transformation,[],[f12]) ).
fof(f180,plain,
e10 = op1(e13,e13),
inference(cnf_transformation,[],[f12]) ).
fof(f182,plain,
( e10 = op1(e11,e10)
| ~ sP26 ),
inference(cnf_transformation,[],[f78]) ).
fof(f184,plain,
( e12 != op1(e12,e12)
| ~ sP25 ),
inference(cnf_transformation,[],[f79]) ).
fof(f188,plain,
( e10 = op1(e13,e10)
| ~ sP24 ),
inference(cnf_transformation,[],[f80]) ).
fof(f191,plain,
( e11 = op1(e10,e11)
| ~ sP23 ),
inference(cnf_transformation,[],[f81]) ).
fof(f195,plain,
( e11 = op1(e11,e11)
| ~ sP22 ),
inference(cnf_transformation,[],[f82]) ).
fof(f196,plain,
( e12 != op1(e12,e12)
| ~ sP21 ),
inference(cnf_transformation,[],[f83]) ).
fof(f201,plain,
( e11 = op1(e11,e13)
| ~ sP20 ),
inference(cnf_transformation,[],[f84]) ).
fof(f203,plain,
( e12 = op1(e10,e12)
| ~ sP19 ),
inference(cnf_transformation,[],[f85]) ).
fof(f206,plain,
( e12 = op1(e11,e12)
| ~ sP18 ),
inference(cnf_transformation,[],[f86]) ).
fof(f208,plain,
( e12 != op1(e12,e12)
| ~ sP17 ),
inference(cnf_transformation,[],[f87]) ).
fof(f213,plain,
( e12 = op1(e12,e13)
| ~ sP16 ),
inference(cnf_transformation,[],[f88]) ).
fof(f215,plain,
( e13 = op1(e10,e13)
| ~ sP15 ),
inference(cnf_transformation,[],[f89]) ).
fof(f218,plain,
( e13 = op1(e11,e13)
| ~ sP14 ),
inference(cnf_transformation,[],[f90]) ).
fof(f222,plain,
( e13 = op1(e13,e12)
| ~ sP13 ),
inference(cnf_transformation,[],[f91]) ).
fof(f225,plain,
( e13 = op1(e13,e13)
| ~ sP12 ),
inference(cnf_transformation,[],[f92]) ).
fof(f228,plain,
( e10 = op1(e10,e10)
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12 ),
inference(cnf_transformation,[],[f49]) ).
fof(f232,plain,
( e10 != op1(e13,e13)
| e13 = op1(e13,e10) ),
inference(cnf_transformation,[],[f49]) ).
fof(f233,plain,
( e13 != op1(e12,e12)
| e12 = op1(e12,e13) ),
inference(cnf_transformation,[],[f49]) ).
fof(f235,plain,
( e11 != op1(e12,e12)
| e12 = op1(e12,e11) ),
inference(cnf_transformation,[],[f49]) ).
fof(f236,plain,
( e10 != op1(e12,e12)
| e12 = op1(e12,e10) ),
inference(cnf_transformation,[],[f49]) ).
fof(f237,plain,
( e13 != op1(e11,e11)
| e11 = op1(e11,e13) ),
inference(cnf_transformation,[],[f49]) ).
fof(f241,plain,
( op1(e10,e10) != e13
| e10 = op1(e10,e13) ),
inference(cnf_transformation,[],[f49]) ).
fof(f243,plain,
( op1(e10,e10) != e11
| e10 = op1(e10,e11) ),
inference(cnf_transformation,[],[f49]) ).
fof(f245,plain,
( e10 = op1(e10,e10)
| e11 = op1(e11,e11)
| e12 = op1(e12,e12)
| e13 = op1(e13,e13) ),
inference(cnf_transformation,[],[f49]) ).
fof(f252,plain,
op1(e12,e12) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f258,plain,
op1(e11,e12) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f264,plain,
op1(e10,e12) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f268,plain,
op1(e10,e10) != op1(e10,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f275,plain,
op1(e10,e13) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f279,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f283,plain,
op1(e11,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f285,plain,
op1(e10,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f294,plain,
( e13 = op1(e10,e13)
| e13 = op1(e11,e13)
| e13 = op1(e12,e13)
| e13 = op1(e13,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f297,plain,
( e12 = op1(e13,e10)
| e12 = op1(e13,e11)
| e12 = op1(e13,e12)
| e12 = op1(e13,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f298,plain,
( e11 = op1(e10,e13)
| e11 = op1(e11,e13)
| e11 = op1(e12,e13)
| e11 = op1(e13,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f299,plain,
( e11 = op1(e13,e10)
| e11 = op1(e13,e11)
| e11 = op1(e13,e12)
| e11 = op1(e13,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f302,plain,
( e13 = op1(e10,e12)
| e13 = op1(e11,e12)
| e13 = op1(e12,e12)
| e13 = op1(e13,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f306,plain,
( e11 = op1(e10,e12)
| e11 = op1(e11,e12)
| e11 = op1(e12,e12)
| e11 = op1(e13,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f308,plain,
( e10 = op1(e10,e12)
| e10 = op1(e11,e12)
| e10 = op1(e12,e12)
| e10 = op1(e13,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f310,plain,
( e13 = op1(e10,e11)
| e13 = op1(e11,e11)
| e13 = op1(e12,e11)
| e13 = op1(e13,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f311,plain,
( e13 = op1(e11,e10)
| e13 = op1(e11,e11)
| e13 = op1(e11,e12)
| e13 = op1(e11,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f314,plain,
( e11 = op1(e10,e11)
| e11 = op1(e11,e11)
| e11 = op1(e12,e11)
| e11 = op1(e13,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f319,plain,
( op1(e10,e10) = e13
| e13 = op1(e10,e11)
| e13 = op1(e10,e12)
| e13 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f321,plain,
( op1(e10,e10) = e12
| e12 = op1(e10,e11)
| e12 = op1(e10,e12)
| e12 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f324,plain,
( e10 = op1(e10,e10)
| e10 = op1(e11,e10)
| e10 = op1(e12,e10)
| e10 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f342,plain,
e22 = op2(op2(op2(e23,e23),op2(e23,e23)),e23),
inference(cnf_transformation,[],[f13]) ).
fof(f343,plain,
e21 = op2(op2(e23,e23),op2(e23,e23)),
inference(cnf_transformation,[],[f13]) ).
fof(f344,plain,
e20 = op2(e23,e23),
inference(cnf_transformation,[],[f13]) ).
fof(f395,plain,
( e21 != op2(e23,e23)
| e23 = op2(e23,e21) ),
inference(cnf_transformation,[],[f65]) ).
fof(f396,plain,
( e20 != op2(e23,e23)
| e23 = op2(e23,e20) ),
inference(cnf_transformation,[],[f65]) ).
fof(f399,plain,
( e21 != op2(e22,e22)
| e22 = op2(e22,e21) ),
inference(cnf_transformation,[],[f65]) ).
fof(f401,plain,
( e23 != op2(e21,e21)
| e21 = op2(e21,e23) ),
inference(cnf_transformation,[],[f65]) ).
fof(f407,plain,
( op2(e20,e20) != e21
| e20 = op2(e20,e21) ),
inference(cnf_transformation,[],[f65]) ).
fof(f426,plain,
e22 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f427,plain,
e21 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f428,plain,
e21 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f429,plain,
e20 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f430,plain,
e20 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f432,plain,
op2(e23,e22) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f436,plain,
op2(e23,e20) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f440,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f445,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f461,plain,
op2(e20,e23) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f465,plain,
op2(e20,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f466,plain,
op2(e20,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f468,plain,
op2(e22,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f473,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f483,plain,
( e22 = op2(e23,e20)
| e22 = op2(e23,e21)
| e22 = op2(e23,e22)
| e22 = op2(e23,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f484,plain,
( e21 = op2(e20,e23)
| e21 = op2(e21,e23)
| e21 = op2(e22,e23)
| e21 = op2(e23,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f488,plain,
( e23 = op2(e20,e22)
| e23 = op2(e21,e22)
| e23 = op2(e22,e22)
| e23 = op2(e23,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f491,plain,
( e22 = op2(e22,e20)
| e22 = op2(e22,e21)
| e22 = op2(e22,e22)
| e22 = op2(e22,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f496,plain,
( e23 = op2(e20,e21)
| e23 = op2(e21,e21)
| e23 = op2(e22,e21)
| e23 = op2(e23,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f503,plain,
( e20 = op2(e21,e20)
| e20 = op2(e21,e21)
| e20 = op2(e21,e22)
| e20 = op2(e21,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f505,plain,
( op2(e20,e20) = e23
| e23 = op2(e20,e21)
| e23 = op2(e20,e22)
| e23 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f507,plain,
( op2(e20,e20) = e22
| e22 = op2(e20,e21)
| e22 = op2(e20,e22)
| e22 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f513,plain,
( e20 = op2(e23,e22)
| e21 = op2(e23,e22)
| e22 = op2(e23,e22)
| e23 = op2(e23,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f517,plain,
( e20 = op2(e22,e22)
| e21 = op2(e22,e22)
| e22 = op2(e22,e22)
| e23 = op2(e22,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f522,plain,
( e20 = op2(e21,e21)
| e21 = op2(e21,e21)
| e22 = op2(e21,e21)
| e23 = op2(e21,e21) ),
inference(cnf_transformation,[],[f3]) ).
fof(f529,plain,
h1(e11) = op2(op2(e20,e20),op2(e20,e20)),
inference(cnf_transformation,[],[f14]) ).
fof(f530,plain,
op2(e20,e20) = h1(e10),
inference(cnf_transformation,[],[f14]) ).
fof(f534,plain,
op2(e21,e21) = h2(e10),
inference(cnf_transformation,[],[f15]) ).
fof(f536,plain,
h3(e12) = op2(op2(op2(e22,e22),op2(e22,e22)),e22),
inference(cnf_transformation,[],[f16]) ).
fof(f537,plain,
h3(e11) = op2(op2(e22,e22),op2(e22,e22)),
inference(cnf_transformation,[],[f16]) ).
fof(f538,plain,
op2(e22,e22) = h3(e10),
inference(cnf_transformation,[],[f16]) ).
fof(f539,plain,
e22 = h3(e13),
inference(cnf_transformation,[],[f16]) ).
fof(f541,plain,
op2(op2(e23,e23),op2(e23,e23)) = h4(e11),
inference(cnf_transformation,[],[f17]) ).
fof(f542,plain,
op2(e23,e23) = h4(e10),
inference(cnf_transformation,[],[f17]) ).
fof(f546,definition,
( spl42_1
<=> e23 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl42_1])],[avatar_definition]) ).
fof(f548,plain,
( e23 = op2(e23,e22)
| ~ spl42_1 ),
inference(avatar_component_clause,[],[f546]) ).
fof(f550,definition,
( spl42_2
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl42_2])],[avatar_definition]) ).
fof(f552,plain,
( e22 = op2(e23,e22)
| ~ spl42_2 ),
inference(avatar_component_clause,[],[f550]) ).
fof(f554,definition,
( spl42_3
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl42_3])],[avatar_definition]) ).
fof(f556,plain,
( e21 = op2(e23,e22)
| ~ spl42_3 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f558,definition,
( spl42_4
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl42_4])],[avatar_definition]) ).
fof(f560,plain,
( e20 = op2(e23,e22)
| ~ spl42_4 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f561,plain,
( spl42_1
| spl42_2
| spl42_3
| spl42_4 ),
inference(avatar_split_clause,[],[f513,f558,f554,f550,f546]) ).
fof(f563,definition,
( spl42_5
<=> e23 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl42_5])],[avatar_definition]) ).
fof(f565,plain,
( e23 = op2(e23,e21)
| ~ spl42_5 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f567,definition,
( spl42_6
<=> e22 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl42_6])],[avatar_definition]) ).
fof(f569,plain,
( e22 = op2(e23,e21)
| ~ spl42_6 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f580,definition,
( spl42_9
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl42_9])],[avatar_definition]) ).
fof(f582,plain,
( e23 = op2(e23,e20)
| ~ spl42_9 ),
inference(avatar_component_clause,[],[f580]) ).
fof(f584,definition,
( spl42_10
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl42_10])],[avatar_definition]) ).
fof(f586,plain,
( e22 = op2(e23,e20)
| ~ spl42_10 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f601,definition,
( spl42_14
<=> e22 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl42_14])],[avatar_definition]) ).
fof(f603,plain,
( e22 = op2(e22,e23)
| ~ spl42_14 ),
inference(avatar_component_clause,[],[f601]) ).
fof(f605,definition,
( spl42_15
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl42_15])],[avatar_definition]) ).
fof(f607,plain,
( e21 = op2(e22,e23)
| ~ spl42_15 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f613,plain,
( e20 = h3(e10)
| e21 = op2(e22,e22)
| e22 = op2(e22,e22)
| e23 = op2(e22,e22) ),
inference(forward_demodulation,[],[f517,f538]) ).
fof(f615,definition,
( spl42_17
<=> e23 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl42_17])],[avatar_definition]) ).
fof(f617,plain,
( e23 = op2(e22,e21)
| ~ spl42_17 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f619,definition,
( spl42_18
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl42_18])],[avatar_definition]) ).
fof(f636,definition,
( spl42_22
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl42_22])],[avatar_definition]) ).
fof(f638,plain,
( e22 = op2(e22,e20)
| ~ spl42_22 ),
inference(avatar_component_clause,[],[f636]) ).
fof(f653,definition,
( spl42_26
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl42_26])],[avatar_definition]) ).
fof(f655,plain,
( e22 = op2(e21,e23)
| ~ spl42_26 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f657,definition,
( spl42_27
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl42_27])],[avatar_definition]) ).
fof(f659,plain,
( e21 = op2(e21,e23)
| ~ spl42_27 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f661,definition,
( spl42_28
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl42_28])],[avatar_definition]) ).
fof(f663,plain,
( e20 = op2(e21,e23)
| ~ spl42_28 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f666,definition,
( spl42_29
<=> e23 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl42_29])],[avatar_definition]) ).
fof(f668,plain,
( e23 = op2(e21,e22)
| ~ spl42_29 ),
inference(avatar_component_clause,[],[f666]) ).
fof(f678,definition,
( spl42_32
<=> e20 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl42_32])],[avatar_definition]) ).
fof(f680,plain,
( e20 = op2(e21,e22)
| ~ spl42_32 ),
inference(avatar_component_clause,[],[f678]) ).
fof(f682,plain,
( e20 = h2(e10)
| e21 = op2(e21,e21)
| e22 = op2(e21,e21)
| e23 = op2(e21,e21) ),
inference(forward_demodulation,[],[f522,f534]) ).
fof(f696,definition,
( spl42_36
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl42_36])],[avatar_definition]) ).
fof(f698,plain,
( e20 = op2(e21,e20)
| ~ spl42_36 ),
inference(avatar_component_clause,[],[f696]) ).
fof(f701,definition,
( spl42_37
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl42_37])],[avatar_definition]) ).
fof(f703,plain,
( e23 = op2(e20,e23)
| ~ spl42_37 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f705,definition,
( spl42_38
<=> e22 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl42_38])],[avatar_definition]) ).
fof(f709,definition,
( spl42_39
<=> e21 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl42_39])],[avatar_definition]) ).
fof(f711,plain,
( e21 = op2(e20,e23)
| ~ spl42_39 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f718,definition,
( spl42_41
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl42_41])],[avatar_definition]) ).
fof(f720,plain,
( e23 = op2(e20,e22)
| ~ spl42_41 ),
inference(avatar_component_clause,[],[f718]) ).
fof(f722,definition,
( spl42_42
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl42_42])],[avatar_definition]) ).
fof(f724,plain,
( e22 = op2(e20,e22)
| ~ spl42_42 ),
inference(avatar_component_clause,[],[f722]) ).
fof(f735,definition,
( spl42_45
<=> e23 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl42_45])],[avatar_definition]) ).
fof(f737,plain,
( e23 = op2(e20,e21)
| ~ spl42_45 ),
inference(avatar_component_clause,[],[f735]) ).
fof(f739,definition,
( spl42_46
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl42_46])],[avatar_definition]) ).
fof(f741,plain,
( e22 = op2(e20,e21)
| ~ spl42_46 ),
inference(avatar_component_clause,[],[f739]) ).
fof(f747,definition,
( spl42_48
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl42_48])],[avatar_definition]) ).
fof(f749,plain,
( e20 = op2(e20,e21)
| ~ spl42_48 ),
inference(avatar_component_clause,[],[f747]) ).
fof(f755,plain,
( e22 = h4(e10)
| e22 = op2(e23,e20)
| e22 = op2(e23,e21)
| e22 = op2(e23,e22) ),
inference(forward_demodulation,[],[f483,f542]) ).
fof(f756,plain,
( e21 = h4(e10)
| e21 = op2(e20,e23)
| e21 = op2(e21,e23)
| e21 = op2(e22,e23) ),
inference(forward_demodulation,[],[f484,f542]) ).
fof(f760,plain,
( e23 = h3(e10)
| e23 = op2(e20,e22)
| e23 = op2(e21,e22)
| e23 = op2(e23,e22) ),
inference(forward_demodulation,[],[f488,f538]) ).
fof(f763,plain,
( e22 = h3(e10)
| e22 = op2(e22,e20)
| e22 = op2(e22,e21)
| e22 = op2(e22,e23) ),
inference(forward_demodulation,[],[f491,f538]) ).
fof(f768,plain,
( e23 = h2(e10)
| e23 = op2(e20,e21)
| e23 = op2(e22,e21)
| e23 = op2(e23,e21) ),
inference(forward_demodulation,[],[f496,f534]) ).
fof(f775,plain,
( e20 = h2(e10)
| e20 = op2(e21,e20)
| e20 = op2(e21,e22)
| e20 = op2(e21,e23) ),
inference(forward_demodulation,[],[f503,f534]) ).
fof(f777,plain,
( e23 = h1(e10)
| e23 = op2(e20,e21)
| e23 = op2(e20,e22)
| e23 = op2(e20,e23) ),
inference(forward_demodulation,[],[f505,f530]) ).
fof(f779,plain,
( e22 = h1(e10)
| e22 = op2(e20,e21)
| e22 = op2(e20,e22)
| e22 = op2(e20,e23) ),
inference(forward_demodulation,[],[f507,f530]) ).
fof(f784,plain,
op2(e23,e22) != h4(e10),
inference(forward_demodulation,[],[f432,f542]) ).
fof(f788,plain,
op2(e22,e21) != h3(e10),
inference(forward_demodulation,[],[f440,f538]) ).
fof(f790,plain,
op2(e21,e23) != h2(e10),
inference(forward_demodulation,[],[f445,f534]) ).
fof(f801,plain,
op2(e20,e22) != h3(e10),
inference(forward_demodulation,[],[f466,f538]) ).
fof(f804,plain,
op2(e20,e21) != h2(e10),
inference(forward_demodulation,[],[f473,f534]) ).
fof(f812,plain,
( e21 != h4(e10)
| e23 = op2(e23,e21) ),
inference(forward_demodulation,[],[f395,f542]) ).
fof(f813,plain,
( e20 != h4(e10)
| e23 = op2(e23,e20) ),
inference(forward_demodulation,[],[f396,f542]) ).
fof(f815,plain,
( e21 != h3(e10)
| e22 = op2(e22,e21) ),
inference(forward_demodulation,[],[f399,f538]) ).
fof(f817,plain,
( e23 != h2(e10)
| e21 = op2(e21,e23) ),
inference(forward_demodulation,[],[f401,f534]) ).
fof(f822,plain,
( e21 != h1(e10)
| e20 = op2(e20,e21) ),
inference(forward_demodulation,[],[f407,f530]) ).
fof(f917,plain,
e22 = op2(h4(e11),e23),
inference(forward_demodulation,[],[f342,f541]) ).
fof(f918,plain,
e21 = op2(h4(e10),h4(e10)),
inference(forward_demodulation,[],[f343,f542]) ).
fof(f920,definition,
( spl42_61
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl42_61])],[avatar_definition]) ).
fof(f922,plain,
( e13 = op1(e13,e13)
| ~ spl42_61 ),
inference(avatar_component_clause,[],[f920]) ).
fof(f924,definition,
( spl42_62
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl42_62])],[avatar_definition]) ).
fof(f926,plain,
( e12 = op1(e13,e13)
| ~ spl42_62 ),
inference(avatar_component_clause,[],[f924]) ).
fof(f928,definition,
( spl42_63
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl42_63])],[avatar_definition]) ).
fof(f930,plain,
( e11 = op1(e13,e13)
| ~ spl42_63 ),
inference(avatar_component_clause,[],[f928]) ).
fof(f932,definition,
( spl42_64
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl42_64])],[avatar_definition]) ).
fof(f934,plain,
( e10 = op1(e13,e13)
| ~ spl42_64 ),
inference(avatar_component_clause,[],[f932]) ).
fof(f937,definition,
( spl42_65
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl42_65])],[avatar_definition]) ).
fof(f939,plain,
( e13 = op1(e13,e12)
| ~ spl42_65 ),
inference(avatar_component_clause,[],[f937]) ).
fof(f941,definition,
( spl42_66
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl42_66])],[avatar_definition]) ).
fof(f943,plain,
( e12 = op1(e13,e12)
| ~ spl42_66 ),
inference(avatar_component_clause,[],[f941]) ).
fof(f945,definition,
( spl42_67
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl42_67])],[avatar_definition]) ).
fof(f947,plain,
( e11 = op1(e13,e12)
| ~ spl42_67 ),
inference(avatar_component_clause,[],[f945]) ).
fof(f949,definition,
( spl42_68
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl42_68])],[avatar_definition]) ).
fof(f951,plain,
( e10 = op1(e13,e12)
| ~ spl42_68 ),
inference(avatar_component_clause,[],[f949]) ).
fof(f954,definition,
( spl42_69
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl42_69])],[avatar_definition]) ).
fof(f956,plain,
( e13 = op1(e13,e11)
| ~ spl42_69 ),
inference(avatar_component_clause,[],[f954]) ).
fof(f958,definition,
( spl42_70
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl42_70])],[avatar_definition]) ).
fof(f960,plain,
( e12 = op1(e13,e11)
| ~ spl42_70 ),
inference(avatar_component_clause,[],[f958]) ).
fof(f962,definition,
( spl42_71
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl42_71])],[avatar_definition]) ).
fof(f964,plain,
( e11 = op1(e13,e11)
| ~ spl42_71 ),
inference(avatar_component_clause,[],[f962]) ).
fof(f971,definition,
( spl42_73
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl42_73])],[avatar_definition]) ).
fof(f973,plain,
( e13 = op1(e13,e10)
| ~ spl42_73 ),
inference(avatar_component_clause,[],[f971]) ).
fof(f975,definition,
( spl42_74
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl42_74])],[avatar_definition]) ).
fof(f977,plain,
( e12 = op1(e13,e10)
| ~ spl42_74 ),
inference(avatar_component_clause,[],[f975]) ).
fof(f979,definition,
( spl42_75
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl42_75])],[avatar_definition]) ).
fof(f981,plain,
( e11 = op1(e13,e10)
| ~ spl42_75 ),
inference(avatar_component_clause,[],[f979]) ).
fof(f983,definition,
( spl42_76
<=> e10 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl42_76])],[avatar_definition]) ).
fof(f985,plain,
( e10 = op1(e13,e10)
| ~ spl42_76 ),
inference(avatar_component_clause,[],[f983]) ).
fof(f988,definition,
( spl42_77
<=> e13 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl42_77])],[avatar_definition]) ).
fof(f990,plain,
( e13 = op1(e12,e13)
| ~ spl42_77 ),
inference(avatar_component_clause,[],[f988]) ).
fof(f992,definition,
( spl42_78
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl42_78])],[avatar_definition]) ).
fof(f994,plain,
( e12 = op1(e12,e13)
| ~ spl42_78 ),
inference(avatar_component_clause,[],[f992]) ).
fof(f996,definition,
( spl42_79
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl42_79])],[avatar_definition]) ).
fof(f998,plain,
( e11 = op1(e12,e13)
| ~ spl42_79 ),
inference(avatar_component_clause,[],[f996]) ).
fof(f1005,definition,
( spl42_81
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl42_81])],[avatar_definition]) ).
fof(f1007,plain,
( e13 = op1(e12,e12)
| ~ spl42_81 ),
inference(avatar_component_clause,[],[f1005]) ).
fof(f1009,definition,
( spl42_82
<=> e12 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl42_82])],[avatar_definition]) ).
fof(f1011,plain,
( e12 = op1(e12,e12)
| ~ spl42_82 ),
inference(avatar_component_clause,[],[f1009]) ).
fof(f1013,definition,
( spl42_83
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl42_83])],[avatar_definition]) ).
fof(f1017,definition,
( spl42_84
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl42_84])],[avatar_definition]) ).
fof(f1019,plain,
( e10 = op1(e12,e12)
| ~ spl42_84 ),
inference(avatar_component_clause,[],[f1017]) ).
fof(f1022,definition,
( spl42_85
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl42_85])],[avatar_definition]) ).
fof(f1024,plain,
( e13 = op1(e12,e11)
| ~ spl42_85 ),
inference(avatar_component_clause,[],[f1022]) ).
fof(f1026,definition,
( spl42_86
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl42_86])],[avatar_definition]) ).
fof(f1028,plain,
( e12 = op1(e12,e11)
| ~ spl42_86 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1030,definition,
( spl42_87
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl42_87])],[avatar_definition]) ).
fof(f1032,plain,
( e11 = op1(e12,e11)
| ~ spl42_87 ),
inference(avatar_component_clause,[],[f1030]) ).
fof(f1043,definition,
( spl42_90
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl42_90])],[avatar_definition]) ).
fof(f1045,plain,
( e12 = op1(e12,e10)
| ~ spl42_90 ),
inference(avatar_component_clause,[],[f1043]) ).
fof(f1051,definition,
( spl42_92
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl42_92])],[avatar_definition]) ).
fof(f1053,plain,
( e10 = op1(e12,e10)
| ~ spl42_92 ),
inference(avatar_component_clause,[],[f1051]) ).
fof(f1056,definition,
( spl42_93
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl42_93])],[avatar_definition]) ).
fof(f1058,plain,
( e13 = op1(e11,e13)
| ~ spl42_93 ),
inference(avatar_component_clause,[],[f1056]) ).
fof(f1060,definition,
( spl42_94
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl42_94])],[avatar_definition]) ).
fof(f1062,plain,
( e12 = op1(e11,e13)
| ~ spl42_94 ),
inference(avatar_component_clause,[],[f1060]) ).
fof(f1064,definition,
( spl42_95
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl42_95])],[avatar_definition]) ).
fof(f1066,plain,
( e11 = op1(e11,e13)
| ~ spl42_95 ),
inference(avatar_component_clause,[],[f1064]) ).
fof(f1073,definition,
( spl42_97
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl42_97])],[avatar_definition]) ).
fof(f1075,plain,
( e13 = op1(e11,e12)
| ~ spl42_97 ),
inference(avatar_component_clause,[],[f1073]) ).
fof(f1077,definition,
( spl42_98
<=> e12 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl42_98])],[avatar_definition]) ).
fof(f1081,definition,
( spl42_99
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl42_99])],[avatar_definition]) ).
fof(f1083,plain,
( e11 = op1(e11,e12)
| ~ spl42_99 ),
inference(avatar_component_clause,[],[f1081]) ).
fof(f1085,definition,
( spl42_100
<=> e10 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl42_100])],[avatar_definition]) ).
fof(f1087,plain,
( e10 = op1(e11,e12)
| ~ spl42_100 ),
inference(avatar_component_clause,[],[f1085]) ).
fof(f1090,definition,
( spl42_101
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl42_101])],[avatar_definition]) ).
fof(f1098,definition,
( spl42_103
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl42_103])],[avatar_definition]) ).
fof(f1100,plain,
( e11 = op1(e11,e11)
| ~ spl42_103 ),
inference(avatar_component_clause,[],[f1098]) ).
fof(f1107,definition,
( spl42_105
<=> e13 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl42_105])],[avatar_definition]) ).
fof(f1109,plain,
( e13 = op1(e11,e10)
| ~ spl42_105 ),
inference(avatar_component_clause,[],[f1107]) ).
fof(f1119,definition,
( spl42_108
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl42_108])],[avatar_definition]) ).
fof(f1121,plain,
( e10 = op1(e11,e10)
| ~ spl42_108 ),
inference(avatar_component_clause,[],[f1119]) ).
fof(f1124,definition,
( spl42_109
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl42_109])],[avatar_definition]) ).
fof(f1126,plain,
( e13 = op1(e10,e13)
| ~ spl42_109 ),
inference(avatar_component_clause,[],[f1124]) ).
fof(f1128,definition,
( spl42_110
<=> e12 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl42_110])],[avatar_definition]) ).
fof(f1132,definition,
( spl42_111
<=> e11 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl42_111])],[avatar_definition]) ).
fof(f1134,plain,
( e11 = op1(e10,e13)
| ~ spl42_111 ),
inference(avatar_component_clause,[],[f1132]) ).
fof(f1136,definition,
( spl42_112
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl42_112])],[avatar_definition]) ).
fof(f1138,plain,
( e10 = op1(e10,e13)
| ~ spl42_112 ),
inference(avatar_component_clause,[],[f1136]) ).
fof(f1141,definition,
( spl42_113
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl42_113])],[avatar_definition]) ).
fof(f1143,plain,
( e13 = op1(e10,e12)
| ~ spl42_113 ),
inference(avatar_component_clause,[],[f1141]) ).
fof(f1145,definition,
( spl42_114
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl42_114])],[avatar_definition]) ).
fof(f1147,plain,
( e12 = op1(e10,e12)
| ~ spl42_114 ),
inference(avatar_component_clause,[],[f1145]) ).
fof(f1149,definition,
( spl42_115
<=> e11 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl42_115])],[avatar_definition]) ).
fof(f1151,plain,
( e11 = op1(e10,e12)
| ~ spl42_115 ),
inference(avatar_component_clause,[],[f1149]) ).
fof(f1153,definition,
( spl42_116
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl42_116])],[avatar_definition]) ).
fof(f1155,plain,
( e10 = op1(e10,e12)
| ~ spl42_116 ),
inference(avatar_component_clause,[],[f1153]) ).
fof(f1158,definition,
( spl42_117
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl42_117])],[avatar_definition]) ).
fof(f1160,plain,
( e13 = op1(e10,e11)
| ~ spl42_117 ),
inference(avatar_component_clause,[],[f1158]) ).
fof(f1162,definition,
( spl42_118
<=> e12 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl42_118])],[avatar_definition]) ).
fof(f1164,plain,
( e12 = op1(e10,e11)
| ~ spl42_118 ),
inference(avatar_component_clause,[],[f1162]) ).
fof(f1166,definition,
( spl42_119
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl42_119])],[avatar_definition]) ).
fof(f1168,plain,
( e11 = op1(e10,e11)
| ~ spl42_119 ),
inference(avatar_component_clause,[],[f1166]) ).
fof(f1170,definition,
( spl42_120
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl42_120])],[avatar_definition]) ).
fof(f1172,plain,
( e10 = op1(e10,e11)
| ~ spl42_120 ),
inference(avatar_component_clause,[],[f1170]) ).
fof(f1175,definition,
( spl42_121
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl42_121])],[avatar_definition]) ).
fof(f1179,definition,
( spl42_122
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[spl42_122])],[avatar_definition]) ).
fof(f1181,plain,
( op1(e10,e10) = e12
| ~ spl42_122 ),
inference(avatar_component_clause,[],[f1179]) ).
fof(f1183,definition,
( spl42_123
<=> op1(e10,e10) = e11 ),
introduced(definition,[new_symbols(definition,[spl42_123])],[avatar_definition]) ).
fof(f1185,plain,
( op1(e10,e10) = e11
| ~ spl42_123 ),
inference(avatar_component_clause,[],[f1183]) ).
fof(f1187,definition,
( spl42_124
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl42_124])],[avatar_definition]) ).
fof(f1189,plain,
( e10 = op1(e10,e10)
| ~ spl42_124 ),
inference(avatar_component_clause,[],[f1187]) ).
fof(f1191,plain,
( spl42_61
| spl42_77
| spl42_93
| spl42_109 ),
inference(avatar_split_clause,[],[f294,f1124,f1056,f988,f920]) ).
fof(f1194,plain,
( spl42_62
| spl42_66
| spl42_70
| spl42_74 ),
inference(avatar_split_clause,[],[f297,f975,f958,f941,f924]) ).
fof(f1195,plain,
( spl42_63
| spl42_79
| spl42_95
| spl42_111 ),
inference(avatar_split_clause,[],[f298,f1132,f1064,f996,f928]) ).
fof(f1196,plain,
( spl42_63
| spl42_67
| spl42_71
| spl42_75 ),
inference(avatar_split_clause,[],[f299,f979,f962,f945,f928]) ).
fof(f1199,plain,
( spl42_65
| spl42_81
| spl42_97
| spl42_113 ),
inference(avatar_split_clause,[],[f302,f1141,f1073,f1005,f937]) ).
fof(f1203,plain,
( spl42_67
| spl42_83
| spl42_99
| spl42_115 ),
inference(avatar_split_clause,[],[f306,f1149,f1081,f1013,f945]) ).
fof(f1205,plain,
( spl42_68
| spl42_84
| spl42_100
| spl42_116 ),
inference(avatar_split_clause,[],[f308,f1153,f1085,f1017,f949]) ).
fof(f1207,plain,
( spl42_69
| spl42_85
| spl42_101
| spl42_117 ),
inference(avatar_split_clause,[],[f310,f1158,f1090,f1022,f954]) ).
fof(f1208,plain,
( spl42_93
| spl42_97
| spl42_101
| spl42_105 ),
inference(avatar_split_clause,[],[f311,f1107,f1090,f1073,f1056]) ).
fof(f1211,plain,
( spl42_71
| spl42_87
| spl42_103
| spl42_119 ),
inference(avatar_split_clause,[],[f314,f1166,f1098,f1030,f962]) ).
fof(f1216,plain,
( spl42_109
| spl42_113
| spl42_117
| spl42_121 ),
inference(avatar_split_clause,[],[f319,f1175,f1158,f1141,f1124]) ).
fof(f1218,plain,
( spl42_110
| spl42_114
| spl42_118
| spl42_122 ),
inference(avatar_split_clause,[],[f321,f1179,f1162,f1145,f1128]) ).
fof(f1221,plain,
( spl42_76
| spl42_92
| spl42_108
| spl42_124 ),
inference(avatar_split_clause,[],[f324,f1187,f1119,f1051,f983]) ).
fof(f1224,definition,
( spl42_125
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl42_125])],[avatar_definition]) ).
fof(f1228,definition,
( spl42_126
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl42_126])],[avatar_definition]) ).
fof(f1232,definition,
( spl42_127
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl42_127])],[avatar_definition]) ).
fof(f1236,definition,
( spl42_128
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl42_128])],[avatar_definition]) ).
fof(f1240,definition,
( spl42_129
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl42_129])],[avatar_definition]) ).
fof(f1244,definition,
( spl42_130
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl42_130])],[avatar_definition]) ).
fof(f1248,definition,
( spl42_131
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl42_131])],[avatar_definition]) ).
fof(f1252,definition,
( spl42_132
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl42_132])],[avatar_definition]) ).
fof(f1256,definition,
( spl42_133
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl42_133])],[avatar_definition]) ).
fof(f1260,definition,
( spl42_134
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl42_134])],[avatar_definition]) ).
fof(f1264,definition,
( spl42_135
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl42_135])],[avatar_definition]) ).
fof(f1268,definition,
( spl42_136
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl42_136])],[avatar_definition]) ).
fof(f1272,definition,
( spl42_137
<=> sP24 ),
introduced(definition,[new_symbols(definition,[spl42_137])],[avatar_definition]) ).
fof(f1276,definition,
( spl42_138
<=> sP25 ),
introduced(definition,[new_symbols(definition,[spl42_138])],[avatar_definition]) ).
fof(f1280,definition,
( spl42_139
<=> sP26 ),
introduced(definition,[new_symbols(definition,[spl42_139])],[avatar_definition]) ).
fof(f1285,plain,
( spl42_125
| spl42_126
| spl42_127
| spl42_128
| spl42_129
| spl42_130
| spl42_131
| spl42_132
| spl42_133
| spl42_134
| spl42_135
| spl42_136
| spl42_137
| spl42_138
| spl42_139
| spl42_124 ),
inference(avatar_split_clause,[],[f228,f1187,f1280,f1276,f1272,f1268,f1264,f1260,f1256,f1252,f1248,f1244,f1240,f1236,f1232,f1228,f1224]) ).
fof(f1288,plain,
( spl42_73
| ~ spl42_64 ),
inference(avatar_split_clause,[],[f232,f932,f971]) ).
fof(f1289,plain,
( spl42_78
| ~ spl42_81 ),
inference(avatar_split_clause,[],[f233,f1005,f992]) ).
fof(f1290,plain,
( spl42_86
| ~ spl42_83 ),
inference(avatar_split_clause,[],[f235,f1013,f1026]) ).
fof(f1291,plain,
( spl42_90
| ~ spl42_84 ),
inference(avatar_split_clause,[],[f236,f1017,f1043]) ).
fof(f1292,plain,
( spl42_95
| ~ spl42_101 ),
inference(avatar_split_clause,[],[f237,f1090,f1064]) ).
fof(f1295,plain,
( spl42_112
| ~ spl42_121 ),
inference(avatar_split_clause,[],[f241,f1175,f1136]) ).
fof(f1297,plain,
( spl42_120
| ~ spl42_123 ),
inference(avatar_split_clause,[],[f243,f1183,f1170]) ).
fof(f1298,plain,
( spl42_61
| spl42_82
| spl42_103
| spl42_124 ),
inference(avatar_split_clause,[],[f245,f1187,f1098,f1009,f920]) ).
fof(f1301,plain,
( ~ spl42_125
| spl42_61 ),
inference(avatar_split_clause,[],[f225,f920,f1224]) ).
fof(f1304,plain,
( ~ spl42_126
| spl42_65 ),
inference(avatar_split_clause,[],[f222,f937,f1228]) ).
fof(f1306,plain,
( ~ spl42_127
| spl42_93 ),
inference(avatar_split_clause,[],[f218,f1056,f1232]) ).
fof(f1309,plain,
( ~ spl42_128
| spl42_109 ),
inference(avatar_split_clause,[],[f215,f1124,f1236]) ).
fof(f1313,plain,
( ~ spl42_129
| spl42_78 ),
inference(avatar_split_clause,[],[f213,f992,f1240]) ).
fof(f1314,plain,
( ~ spl42_130
| ~ spl42_82 ),
inference(avatar_split_clause,[],[f208,f1009,f1244]) ).
fof(f1318,plain,
( ~ spl42_131
| spl42_98 ),
inference(avatar_split_clause,[],[f206,f1077,f1248]) ).
fof(f1321,plain,
( ~ spl42_132
| spl42_114 ),
inference(avatar_split_clause,[],[f203,f1145,f1252]) ).
fof(f1325,plain,
( ~ spl42_133
| spl42_95 ),
inference(avatar_split_clause,[],[f201,f1064,f1256]) ).
fof(f1326,plain,
( ~ spl42_134
| ~ spl42_82 ),
inference(avatar_split_clause,[],[f196,f1009,f1260]) ).
fof(f1331,plain,
( ~ spl42_135
| spl42_103 ),
inference(avatar_split_clause,[],[f195,f1098,f1264]) ).
fof(f1333,plain,
( ~ spl42_136
| spl42_119 ),
inference(avatar_split_clause,[],[f191,f1166,f1268]) ).
fof(f1336,plain,
( ~ spl42_137
| spl42_76 ),
inference(avatar_split_clause,[],[f188,f983,f1272]) ).
fof(f1338,plain,
( ~ spl42_138
| ~ spl42_82 ),
inference(avatar_split_clause,[],[f184,f1009,f1276]) ).
fof(f1342,plain,
( ~ spl42_139
| spl42_108 ),
inference(avatar_split_clause,[],[f182,f1119,f1280]) ).
fof(f1344,plain,
spl42_64,
inference(avatar_split_clause,[],[f180,f932]) ).
fof(f1352,plain,
( h3(op1(e10,e13)) != op2(h3(e10),e22)
| 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(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)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f163,f539]) ).
fof(f1397,definition,
( spl42_147
<=> e22 = h4(e10) ),
introduced(definition,[new_symbols(definition,[spl42_147])],[avatar_definition]) ).
fof(f1398,plain,
( e22 = h4(e10)
| ~ spl42_147 ),
inference(avatar_component_clause,[],[f1397]) ).
fof(f1412,definition,
( spl42_150
<=> e21 = h4(e11) ),
introduced(definition,[new_symbols(definition,[spl42_150])],[avatar_definition]) ).
fof(f1413,plain,
( e21 = h4(e11)
| ~ spl42_150 ),
inference(avatar_component_clause,[],[f1412]) ).
fof(f1417,definition,
( spl42_151
<=> e21 = h4(e10) ),
introduced(definition,[new_symbols(definition,[spl42_151])],[avatar_definition]) ).
fof(f1423,definition,
( spl42_152
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl42_152])],[avatar_definition]) ).
fof(f1427,definition,
( spl42_153
<=> e23 = h3(e12) ),
introduced(definition,[new_symbols(definition,[spl42_153])],[avatar_definition]) ).
fof(f1428,plain,
( e23 = h3(e12)
| ~ spl42_153 ),
inference(avatar_component_clause,[],[f1427]) ).
fof(f1430,plain,
( ~ spl42_152
| ~ spl42_153 ),
inference(avatar_split_clause,[],[f141,f1427,f1423]) ).
fof(f1437,definition,
( spl42_155
<=> e23 = h3(e10) ),
introduced(definition,[new_symbols(definition,[spl42_155])],[avatar_definition]) ).
fof(f1441,plain,
~ sP4,
inference(forward_subsumption_resolution,[],[f136,f539]) ).
fof(f1443,definition,
( spl42_156
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl42_156])],[avatar_definition]) ).
fof(f1457,definition,
( spl42_159
<=> e22 = h3(e10) ),
introduced(definition,[new_symbols(definition,[spl42_159])],[avatar_definition]) ).
fof(f1463,definition,
( spl42_160
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl42_160])],[avatar_definition]) ).
fof(f1472,definition,
( spl42_162
<=> e21 = h3(e11) ),
introduced(definition,[new_symbols(definition,[spl42_162])],[avatar_definition]) ).
fof(f1473,plain,
( e21 = h3(e11)
| ~ spl42_162 ),
inference(avatar_component_clause,[],[f1472]) ).
fof(f1475,plain,
( ~ spl42_160
| ~ spl42_162 ),
inference(avatar_split_clause,[],[f134,f1472,f1463]) ).
fof(f1477,definition,
( spl42_163
<=> e21 = h3(e10) ),
introduced(definition,[new_symbols(definition,[spl42_163])],[avatar_definition]) ).
fof(f1497,definition,
( spl42_167
<=> e23 = h2(e10) ),
introduced(definition,[new_symbols(definition,[spl42_167])],[avatar_definition]) ).
fof(f1517,definition,
( spl42_171
<=> e22 = h2(e10) ),
introduced(definition,[new_symbols(definition,[spl42_171])],[avatar_definition]) ).
fof(f1537,definition,
( spl42_175
<=> e21 = h2(e10) ),
introduced(definition,[new_symbols(definition,[spl42_175])],[avatar_definition]) ).
fof(f1538,plain,
( e21 = h2(e10)
| ~ spl42_175 ),
inference(avatar_component_clause,[],[f1537]) ).
fof(f1557,definition,
( spl42_179
<=> e23 = h1(e10) ),
introduced(definition,[new_symbols(definition,[spl42_179])],[avatar_definition]) ).
fof(f1558,plain,
( e23 = h1(e10)
| ~ spl42_179 ),
inference(avatar_component_clause,[],[f1557]) ).
fof(f1577,definition,
( spl42_183
<=> e22 = h1(e10) ),
introduced(definition,[new_symbols(definition,[spl42_183])],[avatar_definition]) ).
fof(f1578,plain,
( e22 = h1(e10)
| ~ spl42_183 ),
inference(avatar_component_clause,[],[f1577]) ).
fof(f1592,definition,
( spl42_186
<=> e21 = h1(e11) ),
introduced(definition,[new_symbols(definition,[spl42_186])],[avatar_definition]) ).
fof(f1593,plain,
( e21 = h1(e11)
| ~ spl42_186 ),
inference(avatar_component_clause,[],[f1592]) ).
fof(f1597,definition,
( spl42_187
<=> e21 = h1(e10) ),
introduced(definition,[new_symbols(definition,[spl42_187])],[avatar_definition]) ).
fof(f1598,plain,
( e21 = h1(e10)
| ~ spl42_187 ),
inference(avatar_component_clause,[],[f1597]) ).
fof(f1602,plain,
( e21 = h3(e10)
| e20 = h3(e10)
| e22 = op2(e22,e22)
| e23 = op2(e22,e22) ),
inference(forward_demodulation,[],[f613,f538]) ).
fof(f1603,plain,
( e21 = h2(e10)
| e20 = h2(e10)
| e22 = op2(e21,e21)
| e23 = op2(e21,e21) ),
inference(forward_demodulation,[],[f682,f534]) ).
fof(f1608,plain,
( spl42_2
| spl42_6
| spl42_10
| spl42_147 ),
inference(avatar_split_clause,[],[f755,f1397,f584,f567,f550]) ).
fof(f1609,plain,
( spl42_15
| spl42_27
| spl42_39
| spl42_151 ),
inference(avatar_split_clause,[],[f756,f1417,f709,f657,f605]) ).
fof(f1612,definition,
( spl42_188
<=> e20 = h4(e10) ),
introduced(definition,[new_symbols(definition,[spl42_188])],[avatar_definition]) ).
fof(f1614,plain,
( e20 = h4(e10)
| ~ spl42_188 ),
inference(avatar_component_clause,[],[f1612]) ).
fof(f1617,plain,
( spl42_1
| spl42_29
| spl42_41
| spl42_155 ),
inference(avatar_split_clause,[],[f760,f1437,f718,f666,f546]) ).
fof(f1620,plain,
( spl42_14
| spl42_18
| spl42_22
| spl42_159 ),
inference(avatar_split_clause,[],[f763,f1457,f636,f619,f601]) ).
fof(f1624,definition,
( spl42_189
<=> e20 = h3(e10) ),
introduced(definition,[new_symbols(definition,[spl42_189])],[avatar_definition]) ).
fof(f1626,plain,
( e20 = h3(e10)
| ~ spl42_189 ),
inference(avatar_component_clause,[],[f1624]) ).
fof(f1629,plain,
( spl42_5
| spl42_17
| spl42_45
| spl42_167 ),
inference(avatar_split_clause,[],[f768,f1497,f735,f615,f563]) ).
fof(f1636,definition,
( spl42_190
<=> e20 = h2(e10) ),
introduced(definition,[new_symbols(definition,[spl42_190])],[avatar_definition]) ).
fof(f1640,plain,
( spl42_28
| spl42_32
| spl42_36
| spl42_190 ),
inference(avatar_split_clause,[],[f775,f1636,f696,f678,f661]) ).
fof(f1642,plain,
( spl42_37
| spl42_41
| spl42_45
| spl42_179 ),
inference(avatar_split_clause,[],[f777,f1557,f735,f718,f701]) ).
fof(f1644,plain,
( spl42_38
| spl42_42
| spl42_46
| spl42_183 ),
inference(avatar_split_clause,[],[f779,f1577,f739,f722,f705]) ).
fof(f1669,plain,
( spl42_5
| ~ spl42_151 ),
inference(avatar_split_clause,[],[f812,f1417,f563]) ).
fof(f1670,plain,
( spl42_9
| ~ spl42_188 ),
inference(avatar_split_clause,[],[f813,f1612,f580]) ).
fof(f1672,plain,
( spl42_18
| ~ spl42_163 ),
inference(avatar_split_clause,[],[f815,f1477,f619]) ).
fof(f1674,plain,
( spl42_27
| ~ spl42_167 ),
inference(avatar_split_clause,[],[f817,f1497,f657]) ).
fof(f1679,plain,
( spl42_48
| ~ spl42_187 ),
inference(avatar_split_clause,[],[f822,f1597,f747]) ).
fof(f1709,plain,
( h3(op1(e11,e13)) != op2(h3(e11),e22)
| h3(op1(e10,e13)) != op2(h3(e10),e22)
| 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(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(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)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1352,f539]) ).
fof(f1719,plain,
~ spl42_156,
inference(avatar_split_clause,[],[f1441,f1443]) ).
fof(f1722,plain,
( e22 = h3(e10)
| e21 = h3(e10)
| e20 = h3(e10)
| e23 = op2(e22,e22) ),
inference(forward_demodulation,[],[f1602,f538]) ).
fof(f1723,plain,
( e22 = h2(e10)
| e21 = h2(e10)
| e20 = h2(e10)
| e23 = op2(e21,e21) ),
inference(forward_demodulation,[],[f1603,f534]) ).
fof(f1733,plain,
( h3(op1(e12,e13)) != op2(h3(e12),e22)
| h3(op1(e11,e13)) != op2(h3(e11),e22)
| h3(op1(e10,e13)) != op2(h3(e10),e22)
| 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(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(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(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)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1709,f539]) ).
fof(f1743,plain,
( e23 = h3(e10)
| e22 = h3(e10)
| e21 = h3(e10)
| e20 = h3(e10) ),
inference(forward_demodulation,[],[f1722,f538]) ).
fof(f1744,plain,
( e23 = h2(e10)
| e22 = h2(e10)
| e21 = h2(e10)
| e20 = h2(e10) ),
inference(forward_demodulation,[],[f1723,f534]) ).
fof(f1754,plain,
( h3(op1(e13,e10)) != op2(e22,h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),e22)
| h3(op1(e11,e13)) != op2(h3(e11),e22)
| h3(op1(e10,e13)) != op2(h3(e10),e22)
| 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(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(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(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)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1733,f539]) ).
fof(f1764,plain,
( spl42_189
| spl42_163
| spl42_159
| spl42_155 ),
inference(avatar_split_clause,[],[f1743,f1437,f1457,f1477,f1624]) ).
fof(f1765,plain,
( spl42_190
| spl42_175
| spl42_171
| spl42_167 ),
inference(avatar_split_clause,[],[f1744,f1497,f1517,f1537,f1636]) ).
fof(f1775,plain,
( h3(op1(e13,e11)) != op2(e22,h3(e11))
| h3(op1(e13,e10)) != op2(e22,h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),e22)
| h3(op1(e11,e13)) != op2(h3(e11),e22)
| h3(op1(e10,e13)) != op2(h3(e10),e22)
| 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(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(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(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1754,f539]) ).
fof(f1791,plain,
( h3(op1(e13,e12)) != op2(e22,h3(e12))
| h3(op1(e13,e11)) != op2(e22,h3(e11))
| h3(op1(e13,e10)) != op2(e22,h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),e22)
| h3(op1(e11,e13)) != op2(h3(e11),e22)
| h3(op1(e10,e13)) != op2(h3(e10),e22)
| 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(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(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(e13,e13)) != op2(h3(e13),h3(e13))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1775,f539]) ).
fof(f1807,plain,
( op2(e22,e22) != h3(op1(e13,e13))
| h3(op1(e13,e12)) != op2(e22,h3(e12))
| h3(op1(e13,e11)) != op2(e22,h3(e11))
| h3(op1(e13,e10)) != op2(e22,h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),e22)
| h3(op1(e11,e13)) != op2(h3(e11),e22)
| h3(op1(e10,e13)) != op2(h3(e10),e22)
| 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(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(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))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1791,f539]) ).
fof(f1823,plain,
( h3(e10) != h3(op1(e13,e13))
| h3(op1(e13,e12)) != op2(e22,h3(e12))
| h3(op1(e13,e11)) != op2(e22,h3(e11))
| h3(op1(e13,e10)) != op2(e22,h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),e22)
| h3(op1(e11,e13)) != op2(h3(e11),e22)
| h3(op1(e10,e13)) != op2(h3(e10),e22)
| 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(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(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))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1807,f538]) ).
fof(f1842,definition,
( spl42_196
<=> h3(op1(e12,e12)) = op2(h3(e12),h3(e12)) ),
introduced(definition,[new_symbols(definition,[spl42_196])],[avatar_definition]) ).
fof(f1844,plain,
( h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| spl42_196 ),
inference(avatar_component_clause,[],[f1842]) ).
fof(f1846,definition,
( spl42_197
<=> h3(op1(e12,e11)) = op2(h3(e12),h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl42_197])],[avatar_definition]) ).
fof(f1848,plain,
( h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| spl42_197 ),
inference(avatar_component_clause,[],[f1846]) ).
fof(f1850,definition,
( spl42_198
<=> h3(op1(e12,e10)) = op2(h3(e12),h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl42_198])],[avatar_definition]) ).
fof(f1852,plain,
( h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| spl42_198 ),
inference(avatar_component_clause,[],[f1850]) ).
fof(f1854,definition,
( spl42_199
<=> h3(op1(e11,e12)) = op2(h3(e11),h3(e12)) ),
introduced(definition,[new_symbols(definition,[spl42_199])],[avatar_definition]) ).
fof(f1856,plain,
( h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| spl42_199 ),
inference(avatar_component_clause,[],[f1854]) ).
fof(f1858,definition,
( spl42_200
<=> h3(op1(e11,e11)) = op2(h3(e11),h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl42_200])],[avatar_definition]) ).
fof(f1860,plain,
( h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| spl42_200 ),
inference(avatar_component_clause,[],[f1858]) ).
fof(f1862,definition,
( spl42_201
<=> h3(op1(e11,e10)) = op2(h3(e11),h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl42_201])],[avatar_definition]) ).
fof(f1864,plain,
( h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| spl42_201 ),
inference(avatar_component_clause,[],[f1862]) ).
fof(f1866,definition,
( spl42_202
<=> h3(op1(e10,e12)) = op2(h3(e10),h3(e12)) ),
introduced(definition,[new_symbols(definition,[spl42_202])],[avatar_definition]) ).
fof(f1867,plain,
( h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
| ~ spl42_202 ),
inference(avatar_component_clause,[],[f1866]) ).
fof(f1868,plain,
( h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| spl42_202 ),
inference(avatar_component_clause,[],[f1866]) ).
fof(f1870,definition,
( spl42_203
<=> h3(op1(e10,e11)) = op2(h3(e10),h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl42_203])],[avatar_definition]) ).
fof(f1872,plain,
( h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| spl42_203 ),
inference(avatar_component_clause,[],[f1870]) ).
fof(f1874,definition,
( spl42_204
<=> h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl42_204])],[avatar_definition]) ).
fof(f1876,plain,
( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| spl42_204 ),
inference(avatar_component_clause,[],[f1874]) ).
fof(f1878,definition,
( spl42_205
<=> h3(op1(e10,e13)) = op2(h3(e10),e22) ),
introduced(definition,[new_symbols(definition,[spl42_205])],[avatar_definition]) ).
fof(f1880,plain,
( h3(op1(e10,e13)) != op2(h3(e10),e22)
| spl42_205 ),
inference(avatar_component_clause,[],[f1878]) ).
fof(f1882,definition,
( spl42_206
<=> h3(op1(e11,e13)) = op2(h3(e11),e22) ),
introduced(definition,[new_symbols(definition,[spl42_206])],[avatar_definition]) ).
fof(f1884,plain,
( h3(op1(e11,e13)) != op2(h3(e11),e22)
| spl42_206 ),
inference(avatar_component_clause,[],[f1882]) ).
fof(f1886,definition,
( spl42_207
<=> h3(op1(e12,e13)) = op2(h3(e12),e22) ),
introduced(definition,[new_symbols(definition,[spl42_207])],[avatar_definition]) ).
fof(f1888,plain,
( h3(op1(e12,e13)) != op2(h3(e12),e22)
| spl42_207 ),
inference(avatar_component_clause,[],[f1886]) ).
fof(f1890,definition,
( spl42_208
<=> h3(op1(e13,e10)) = op2(e22,h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl42_208])],[avatar_definition]) ).
fof(f1892,plain,
( h3(op1(e13,e10)) != op2(e22,h3(e10))
| spl42_208 ),
inference(avatar_component_clause,[],[f1890]) ).
fof(f1894,definition,
( spl42_209
<=> h3(op1(e13,e11)) = op2(e22,h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl42_209])],[avatar_definition]) ).
fof(f1896,plain,
( h3(op1(e13,e11)) != op2(e22,h3(e11))
| spl42_209 ),
inference(avatar_component_clause,[],[f1894]) ).
fof(f1898,definition,
( spl42_210
<=> h3(op1(e13,e12)) = op2(e22,h3(e12)) ),
introduced(definition,[new_symbols(definition,[spl42_210])],[avatar_definition]) ).
fof(f1900,plain,
( h3(op1(e13,e12)) != op2(e22,h3(e12))
| spl42_210 ),
inference(avatar_component_clause,[],[f1898]) ).
fof(f1902,definition,
( spl42_211
<=> h3(e10) = h3(op1(e13,e13)) ),
introduced(definition,[new_symbols(definition,[spl42_211])],[avatar_definition]) ).
fof(f1904,plain,
( h3(e10) != h3(op1(e13,e13))
| spl42_211 ),
inference(avatar_component_clause,[],[f1902]) ).
fof(f1911,plain,
( spl42_152
| spl42_156
| spl42_160
| ~ spl42_189
| ~ spl42_196
| ~ spl42_197
| ~ spl42_198
| ~ spl42_199
| ~ spl42_200
| ~ spl42_201
| ~ spl42_202
| ~ spl42_203
| ~ spl42_204
| ~ spl42_205
| ~ spl42_206
| ~ spl42_207
| ~ spl42_208
| ~ spl42_209
| ~ spl42_210
| ~ spl42_211 ),
inference(avatar_split_clause,[],[f1823,f1902,f1898,f1894,f1890,f1886,f1882,f1878,f1874,f1870,f1866,f1862,f1858,f1854,f1850,f1846,f1842,f1624,f1463,f1443,f1423]) ).
fof(f2022,definition,
( spl42_239
<=> h1(op1(e10,e11)) = op2(h1(e10),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl42_239])],[avatar_definition]) ).
fof(f2023,plain,
( h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
| ~ spl42_239 ),
inference(avatar_component_clause,[],[f2022]) ).
fof(f2024,plain,
( h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| spl42_239 ),
inference(avatar_component_clause,[],[f2022]) ).
fof(f2208,plain,
( e21 = e22
| ~ spl42_26
| ~ spl42_27 ),
inference(forward_demodulation,[],[f655,f659]) ).
fof(f2211,plain,
( $false
| ~ spl42_26
| ~ spl42_27 ),
inference(forward_subsumption_resolution,[],[f2208,f428]) ).
fof(f2212,plain,
( ~ spl42_26
| ~ spl42_27 ),
inference(avatar_contradiction_clause,[],[f2211]) ).
fof(f2215,plain,
( e20 = e23
| ~ spl42_29
| ~ spl42_32 ),
inference(forward_demodulation,[],[f668,f680]) ).
fof(f2219,plain,
( $false
| ~ spl42_29
| ~ spl42_32 ),
inference(forward_subsumption_resolution,[],[f2215,f429]) ).
fof(f2220,plain,
( ~ spl42_29
| ~ spl42_32 ),
inference(avatar_contradiction_clause,[],[f2219]) ).
fof(f2231,plain,
( e21 = e22
| ~ spl42_14
| ~ spl42_15 ),
inference(superposition,[],[f607,f603]) ).
fof(f2235,plain,
( $false
| ~ spl42_14
| ~ spl42_15 ),
inference(forward_subsumption_resolution,[],[f2231,f428]) ).
fof(f2236,plain,
( ~ spl42_14
| ~ spl42_15 ),
inference(avatar_contradiction_clause,[],[f2235]) ).
fof(f2293,plain,
( e22 = e23
| ~ spl42_5
| ~ spl42_6 ),
inference(superposition,[],[f569,f565]) ).
fof(f2297,plain,
( $false
| ~ spl42_5
| ~ spl42_6 ),
inference(forward_subsumption_resolution,[],[f2293,f426]) ).
fof(f2298,plain,
( ~ spl42_5
| ~ spl42_6 ),
inference(avatar_contradiction_clause,[],[f2297]) ).
fof(f2310,plain,
( e22 = e23
| ~ spl42_9
| ~ spl42_10 ),
inference(superposition,[],[f586,f582]) ).
fof(f2314,plain,
( $false
| ~ spl42_9
| ~ spl42_10 ),
inference(forward_subsumption_resolution,[],[f2310,f426]) ).
fof(f2315,plain,
( ~ spl42_9
| ~ spl42_10 ),
inference(avatar_contradiction_clause,[],[f2314]) ).
fof(f2330,plain,
( e20 = e22
| ~ spl42_26
| ~ spl42_28 ),
inference(superposition,[],[f663,f655]) ).
fof(f2336,plain,
( $false
| ~ spl42_26
| ~ spl42_28 ),
inference(forward_subsumption_resolution,[],[f2330,f430]) ).
fof(f2337,plain,
( ~ spl42_26
| ~ spl42_28 ),
inference(avatar_contradiction_clause,[],[f2336]) ).
fof(f2361,plain,
( e22 = e23
| ~ spl42_41
| ~ spl42_42 ),
inference(forward_demodulation,[],[f720,f724]) ).
fof(f2363,plain,
( $false
| ~ spl42_41
| ~ spl42_42 ),
inference(forward_subsumption_resolution,[],[f2361,f426]) ).
fof(f2364,plain,
( ~ spl42_41
| ~ spl42_42 ),
inference(avatar_contradiction_clause,[],[f2363]) ).
fof(f2415,plain,
( e21 = e23
| ~ spl42_179
| ~ spl42_187 ),
inference(forward_demodulation,[],[f1558,f1598]) ).
fof(f2418,plain,
( $false
| ~ spl42_179
| ~ spl42_187 ),
inference(forward_subsumption_resolution,[],[f2415,f427]) ).
fof(f2419,plain,
( ~ spl42_179
| ~ spl42_187 ),
inference(avatar_contradiction_clause,[],[f2418]) ).
fof(f2448,plain,
( e20 = e22
| ~ spl42_46
| ~ spl42_48 ),
inference(forward_demodulation,[],[f741,f749]) ).
fof(f2453,plain,
( h3(op1(e11,e10)) != op2(h3(e11),e20)
| ~ spl42_189
| spl42_201 ),
inference(forward_demodulation,[],[f1864,f1626]) ).
fof(f2459,plain,
( $false
| ~ spl42_46
| ~ spl42_48 ),
inference(forward_subsumption_resolution,[],[f2448,f430]) ).
fof(f2460,plain,
( ~ spl42_46
| ~ spl42_48 ),
inference(avatar_contradiction_clause,[],[f2459]) ).
fof(f2583,plain,
( e21 = e22
| ~ spl42_183
| ~ spl42_187 ),
inference(superposition,[],[f1598,f1578]) ).
fof(f2589,plain,
( $false
| ~ spl42_183
| ~ spl42_187 ),
inference(forward_subsumption_resolution,[],[f2583,f428]) ).
fof(f2590,plain,
( ~ spl42_183
| ~ spl42_187 ),
inference(avatar_contradiction_clause,[],[f2589]) ).
fof(f2639,plain,
( e20 = e22
| ~ spl42_147
| ~ spl42_188 ),
inference(forward_demodulation,[],[f1398,f1614]) ).
fof(f2640,plain,
( $false
| ~ spl42_147
| ~ spl42_188 ),
inference(forward_subsumption_resolution,[],[f2639,f430]) ).
fof(f2641,plain,
( ~ spl42_147
| ~ spl42_188 ),
inference(avatar_contradiction_clause,[],[f2640]) ).
fof(f2720,plain,
( e21 = e23
| ~ spl42_37
| ~ spl42_39 ),
inference(forward_demodulation,[],[f703,f711]) ).
fof(f2732,plain,
( $false
| ~ spl42_37
| ~ spl42_39 ),
inference(forward_subsumption_resolution,[],[f2720,f427]) ).
fof(f2733,plain,
( ~ spl42_37
| ~ spl42_39 ),
inference(avatar_contradiction_clause,[],[f2732]) ).
fof(f2862,plain,
( e20 = e23
| ~ spl42_45
| ~ spl42_48 ),
inference(superposition,[],[f749,f737]) ).
fof(f2866,plain,
( $false
| ~ spl42_45
| ~ spl42_48 ),
inference(forward_subsumption_resolution,[],[f2862,f429]) ).
fof(f2867,plain,
( ~ spl42_45
| ~ spl42_48 ),
inference(avatar_contradiction_clause,[],[f2866]) ).
fof(f2885,plain,
( e11 = e13
| ~ spl42_73
| ~ spl42_75 ),
inference(superposition,[],[f981,f973]) ).
fof(f2889,plain,
( $false
| ~ spl42_73
| ~ spl42_75 ),
inference(forward_subsumption_resolution,[],[f2885,f173]) ).
fof(f2890,plain,
( ~ spl42_73
| ~ spl42_75 ),
inference(avatar_contradiction_clause,[],[f2889]) ).
fof(f2892,plain,
( e11 = e12
| ~ spl42_66
| ~ spl42_67 ),
inference(superposition,[],[f947,f943]) ).
fof(f2896,plain,
( $false
| ~ spl42_66
| ~ spl42_67 ),
inference(forward_subsumption_resolution,[],[f2892,f174]) ).
fof(f2897,plain,
( ~ spl42_66
| ~ spl42_67 ),
inference(avatar_contradiction_clause,[],[f2896]) ).
fof(f2898,plain,
( e10 = e12
| ~ spl42_62
| ~ spl42_64 ),
inference(forward_demodulation,[],[f926,f934]) ).
fof(f2899,plain,
( e11 = e13
| ~ spl42_65
| ~ spl42_67 ),
inference(forward_demodulation,[],[f939,f947]) ).
fof(f2902,plain,
( $false
| ~ spl42_62
| ~ spl42_64 ),
inference(forward_subsumption_resolution,[],[f2898,f176]) ).
fof(f2903,plain,
( ~ spl42_62
| ~ spl42_64 ),
inference(avatar_contradiction_clause,[],[f2902]) ).
fof(f2904,plain,
( $false
| ~ spl42_65
| ~ spl42_67 ),
inference(forward_subsumption_resolution,[],[f2899,f173]) ).
fof(f2905,plain,
( ~ spl42_65
| ~ spl42_67 ),
inference(avatar_contradiction_clause,[],[f2904]) ).
fof(f2913,plain,
( e11 = e13
| ~ spl42_77
| ~ spl42_79 ),
inference(superposition,[],[f998,f990]) ).
fof(f2917,plain,
( $false
| ~ spl42_77
| ~ spl42_79 ),
inference(forward_subsumption_resolution,[],[f2913,f173]) ).
fof(f2918,plain,
( ~ spl42_77
| ~ spl42_79 ),
inference(avatar_contradiction_clause,[],[f2917]) ).
fof(f2925,plain,
( e10 = e11
| ~ spl42_111
| ~ spl42_112 ),
inference(forward_demodulation,[],[f1134,f1138]) ).
fof(f2926,plain,
( $false
| ~ spl42_111
| ~ spl42_112 ),
inference(forward_subsumption_resolution,[],[f2925,f177]) ).
fof(f2927,plain,
( ~ spl42_111
| ~ spl42_112 ),
inference(avatar_contradiction_clause,[],[f2926]) ).
fof(f2942,plain,
( e12 = e13
| ~ spl42_85
| ~ spl42_86 ),
inference(superposition,[],[f1028,f1024]) ).
fof(f2946,plain,
( $false
| ~ spl42_85
| ~ spl42_86 ),
inference(forward_subsumption_resolution,[],[f2942,f172]) ).
fof(f2947,plain,
( ~ spl42_85
| ~ spl42_86 ),
inference(avatar_contradiction_clause,[],[f2946]) ).
fof(f2964,plain,
( e12 = e13
| ~ spl42_93
| ~ spl42_94 ),
inference(forward_demodulation,[],[f1058,f1062]) ).
fof(f2966,plain,
( $false
| ~ spl42_93
| ~ spl42_94 ),
inference(forward_subsumption_resolution,[],[f2964,f172]) ).
fof(f2967,plain,
( ~ spl42_93
| ~ spl42_94 ),
inference(avatar_contradiction_clause,[],[f2966]) ).
fof(f2977,plain,
( e11 = e12
| ~ spl42_78
| ~ spl42_79 ),
inference(superposition,[],[f998,f994]) ).
fof(f2981,plain,
( $false
| ~ spl42_78
| ~ spl42_79 ),
inference(forward_subsumption_resolution,[],[f2977,f174]) ).
fof(f2982,plain,
( ~ spl42_78
| ~ spl42_79 ),
inference(avatar_contradiction_clause,[],[f2981]) ).
fof(f2983,plain,
( e10 = e11
| ~ spl42_63
| ~ spl42_64 ),
inference(forward_demodulation,[],[f930,f934]) ).
fof(f2984,plain,
( e12 = e13
| ~ spl42_69
| ~ spl42_70 ),
inference(forward_demodulation,[],[f956,f960]) ).
fof(f2986,plain,
( $false
| ~ spl42_63
| ~ spl42_64 ),
inference(forward_subsumption_resolution,[],[f2983,f177]) ).
fof(f2987,plain,
( ~ spl42_63
| ~ spl42_64 ),
inference(avatar_contradiction_clause,[],[f2986]) ).
fof(f2988,plain,
( $false
| ~ spl42_69
| ~ spl42_70 ),
inference(forward_subsumption_resolution,[],[f2984,f172]) ).
fof(f2989,plain,
( ~ spl42_69
| ~ spl42_70 ),
inference(avatar_contradiction_clause,[],[f2988]) ).
fof(f2994,plain,
( e10 = e12
| ~ spl42_114
| ~ spl42_116 ),
inference(forward_demodulation,[],[f1147,f1155]) ).
fof(f2998,plain,
( $false
| ~ spl42_114
| ~ spl42_116 ),
inference(forward_subsumption_resolution,[],[f2994,f176]) ).
fof(f2999,plain,
( ~ spl42_114
| ~ spl42_116 ),
inference(avatar_contradiction_clause,[],[f2998]) ).
fof(f3006,plain,
( e11 = e13
| ~ spl42_85
| ~ spl42_87 ),
inference(superposition,[],[f1032,f1024]) ).
fof(f3010,plain,
( $false
| ~ spl42_85
| ~ spl42_87 ),
inference(forward_subsumption_resolution,[],[f3006,f173]) ).
fof(f3011,plain,
( ~ spl42_85
| ~ spl42_87 ),
inference(avatar_contradiction_clause,[],[f3010]) ).
fof(f3079,plain,
( e11 = e13
| ~ spl42_109
| ~ spl42_111 ),
inference(forward_demodulation,[],[f1126,f1134]) ).
fof(f3082,plain,
( $false
| ~ spl42_109
| ~ spl42_111 ),
inference(forward_subsumption_resolution,[],[f3079,f173]) ).
fof(f3083,plain,
( ~ spl42_109
| ~ spl42_111 ),
inference(avatar_contradiction_clause,[],[f3082]) ).
fof(f3091,plain,
( e11 = e13
| ~ spl42_69
| ~ spl42_71 ),
inference(superposition,[],[f964,f956]) ).
fof(f3096,plain,
( $false
| ~ spl42_69
| ~ spl42_71 ),
inference(forward_subsumption_resolution,[],[f3091,f173]) ).
fof(f3097,plain,
( ~ spl42_69
| ~ spl42_71 ),
inference(avatar_contradiction_clause,[],[f3096]) ).
fof(f3102,plain,
( e12 = e13
| ~ spl42_73
| ~ spl42_74 ),
inference(superposition,[],[f977,f973]) ).
fof(f3106,plain,
( $false
| ~ spl42_73
| ~ spl42_74 ),
inference(forward_subsumption_resolution,[],[f3102,f172]) ).
fof(f3107,plain,
( ~ spl42_73
| ~ spl42_74 ),
inference(avatar_contradiction_clause,[],[f3106]) ).
fof(f3111,plain,
( e10 = e13
| ~ spl42_117
| ~ spl42_120 ),
inference(forward_demodulation,[],[f1160,f1172]) ).
fof(f3114,plain,
( h1(op1(e10,e11)) != op2(e21,h1(e11))
| ~ spl42_187
| spl42_239 ),
inference(forward_demodulation,[],[f2024,f1598]) ).
fof(f3118,plain,
( $false
| ~ spl42_117
| ~ spl42_120 ),
inference(forward_subsumption_resolution,[],[f3111,f175]) ).
fof(f3119,plain,
( ~ spl42_117
| ~ spl42_120 ),
inference(avatar_contradiction_clause,[],[f3118]) ).
fof(f3120,plain,
( h1(e10) != op2(e21,h1(e11))
| ~ spl42_120
| ~ spl42_187
| spl42_239 ),
inference(forward_demodulation,[],[f3114,f1172]) ).
fof(f3121,plain,
( e21 != op2(e21,h1(e11))
| ~ spl42_120
| ~ spl42_187
| spl42_239 ),
inference(forward_demodulation,[],[f3120,f1598]) ).
fof(f3165,plain,
( e11 = e13
| ~ spl42_97
| ~ spl42_99 ),
inference(forward_demodulation,[],[f1075,f1083]) ).
fof(f3168,plain,
( $false
| ~ spl42_97
| ~ spl42_99 ),
inference(forward_subsumption_resolution,[],[f3165,f173]) ).
fof(f3169,plain,
( ~ spl42_97
| ~ spl42_99 ),
inference(avatar_contradiction_clause,[],[f3168]) ).
fof(f3170,plain,
( e12 = e13
| ~ spl42_65
| ~ spl42_66 ),
inference(forward_demodulation,[],[f939,f943]) ).
fof(f3173,plain,
( $false
| ~ spl42_65
| ~ spl42_66 ),
inference(forward_subsumption_resolution,[],[f3170,f172]) ).
fof(f3174,plain,
( ~ spl42_65
| ~ spl42_66 ),
inference(avatar_contradiction_clause,[],[f3173]) ).
fof(f3187,plain,
( e10 = e12
| ~ spl42_90
| ~ spl42_92 ),
inference(superposition,[],[f1053,f1045]) ).
fof(f3191,plain,
( $false
| ~ spl42_90
| ~ spl42_92 ),
inference(forward_subsumption_resolution,[],[f3187,f176]) ).
fof(f3192,plain,
( ~ spl42_90
| ~ spl42_92 ),
inference(avatar_contradiction_clause,[],[f3191]) ).
fof(f3196,plain,
( e10 = e13
| ~ spl42_105
| ~ spl42_108 ),
inference(forward_demodulation,[],[f1109,f1121]) ).
fof(f3201,plain,
( $false
| ~ spl42_105
| ~ spl42_108 ),
inference(forward_subsumption_resolution,[],[f3196,f175]) ).
fof(f3202,plain,
( ~ spl42_105
| ~ spl42_108 ),
inference(avatar_contradiction_clause,[],[f3201]) ).
fof(f3216,plain,
( e10 = e13
| ~ spl42_61
| ~ spl42_64 ),
inference(forward_demodulation,[],[f922,f934]) ).
fof(f3217,plain,
( e11 = e12
| ~ spl42_70
| ~ spl42_71 ),
inference(forward_demodulation,[],[f960,f964]) ).
fof(f3221,plain,
( e10 = e13
| ~ spl42_97
| ~ spl42_100 ),
inference(forward_demodulation,[],[f1075,f1087]) ).
fof(f3238,plain,
( $false
| ~ spl42_61
| ~ spl42_64 ),
inference(forward_subsumption_resolution,[],[f3216,f175]) ).
fof(f3239,plain,
( ~ spl42_61
| ~ spl42_64 ),
inference(avatar_contradiction_clause,[],[f3238]) ).
fof(f3240,plain,
( $false
| ~ spl42_70
| ~ spl42_71 ),
inference(forward_subsumption_resolution,[],[f3217,f174]) ).
fof(f3241,plain,
( ~ spl42_70
| ~ spl42_71 ),
inference(avatar_contradiction_clause,[],[f3240]) ).
fof(f3242,plain,
( $false
| ~ spl42_97
| ~ spl42_100 ),
inference(forward_subsumption_resolution,[],[f3221,f175]) ).
fof(f3243,plain,
( ~ spl42_97
| ~ spl42_100 ),
inference(avatar_contradiction_clause,[],[f3242]) ).
fof(f3254,plain,
( e10 = e13
| ~ spl42_73
| ~ spl42_76 ),
inference(superposition,[],[f985,f973]) ).
fof(f3258,plain,
( $false
| ~ spl42_73
| ~ spl42_76 ),
inference(forward_subsumption_resolution,[],[f3254,f175]) ).
fof(f3259,plain,
( ~ spl42_73
| ~ spl42_76 ),
inference(avatar_contradiction_clause,[],[f3258]) ).
fof(f3268,plain,
( e11 = e12
| ~ spl42_94
| ~ spl42_95 ),
inference(superposition,[],[f1066,f1062]) ).
fof(f3274,plain,
( $false
| ~ spl42_94
| ~ spl42_95 ),
inference(forward_subsumption_resolution,[],[f3268,f174]) ).
fof(f3275,plain,
( ~ spl42_94
| ~ spl42_95 ),
inference(avatar_contradiction_clause,[],[f3274]) ).
fof(f3277,plain,
( e12 = e13
| ~ spl42_81
| ~ spl42_82 ),
inference(forward_demodulation,[],[f1007,f1011]) ).
fof(f3285,plain,
( $false
| ~ spl42_81
| ~ spl42_82 ),
inference(forward_subsumption_resolution,[],[f3277,f172]) ).
fof(f3286,plain,
( ~ spl42_81
| ~ spl42_82 ),
inference(avatar_contradiction_clause,[],[f3285]) ).
fof(f3336,plain,
( e10 = e11
| ~ spl42_67
| ~ spl42_68 ),
inference(forward_demodulation,[],[f947,f951]) ).
fof(f3340,plain,
( e10 = e11
| ~ spl42_119
| ~ spl42_120 ),
inference(forward_demodulation,[],[f1168,f1172]) ).
fof(f3348,plain,
( $false
| ~ spl42_67
| ~ spl42_68 ),
inference(forward_subsumption_resolution,[],[f3336,f177]) ).
fof(f3349,plain,
( ~ spl42_67
| ~ spl42_68 ),
inference(avatar_contradiction_clause,[],[f3348]) ).
fof(f3352,plain,
( $false
| ~ spl42_119
| ~ spl42_120 ),
inference(forward_subsumption_resolution,[],[f3340,f177]) ).
fof(f3353,plain,
( ~ spl42_119
| ~ spl42_120 ),
inference(avatar_contradiction_clause,[],[f3352]) ).
fof(f3417,plain,
e20 = h4(e10),
inference(superposition,[],[f344,f542]) ).
fof(f3418,plain,
spl42_188,
inference(avatar_split_clause,[],[f3417,f1612]) ).
fof(f3486,plain,
( e23 != h3(e10)
| ~ spl42_17 ),
inference(superposition,[],[f788,f617]) ).
fof(f3489,plain,
( e22 != h2(e10)
| ~ spl42_26 ),
inference(superposition,[],[f790,f655]) ).
fof(f3507,plain,
( e22 != h3(e10)
| ~ spl42_42 ),
inference(superposition,[],[f801,f724]) ).
fof(f3511,plain,
( e20 != h2(e10)
| ~ spl42_48 ),
inference(superposition,[],[f804,f749]) ).
fof(f3527,plain,
( e12 != op1(e12,e12)
| ~ spl42_78 ),
inference(superposition,[],[f252,f994]) ).
fof(f3545,plain,
( e13 != op1(e10,e12)
| ~ spl42_109 ),
inference(superposition,[],[f264,f1126]) ).
fof(f3551,plain,
( op1(e10,e10) != e11
| ~ spl42_115 ),
inference(superposition,[],[f268,f1151]) ).
fof(f3570,plain,
( e12 != op1(e10,e12)
| ~ spl42_66 ),
inference(superposition,[],[f279,f943]) ).
fof(f3578,plain,
( e11 != op1(e11,e11)
| ~ spl42_71 ),
inference(superposition,[],[f283,f964]) ).
fof(f3619,plain,
( e22 != op2(e20,e23)
| ~ spl42_26 ),
inference(superposition,[],[f461,f655]) ).
fof(f3626,plain,
( e22 != op2(e22,e21)
| ~ spl42_6 ),
inference(superposition,[],[f468,f569]) ).
fof(f3636,plain,
( op2(e20,e20) = e21
| ~ spl42_188 ),
inference(superposition,[],[f918,f1614]) ).
fof(f3639,plain,
( op1(e10,e10) = e11
| ~ spl42_64 ),
inference(superposition,[],[f179,f934]) ).
fof(f3640,plain,
( e10 = e11
| ~ spl42_64
| ~ spl42_124 ),
inference(forward_demodulation,[],[f3639,f1189]) ).
fof(f3641,plain,
( $false
| ~ spl42_64
| ~ spl42_124 ),
inference(forward_subsumption_resolution,[],[f3640,f177]) ).
fof(f3642,plain,
( ~ spl42_64
| ~ spl42_124 ),
inference(avatar_contradiction_clause,[],[f3641]) ).
fof(f3649,plain,
( spl42_123
| ~ spl42_64 ),
inference(avatar_split_clause,[],[f3639,f932,f1183]) ).
fof(f3684,plain,
( ~ spl42_113
| ~ spl42_109 ),
inference(avatar_split_clause,[],[f3545,f1124,f1141]) ).
fof(f3702,plain,
( $false
| ~ spl42_78
| ~ spl42_82 ),
inference(forward_subsumption_resolution,[],[f3527,f1011]) ).
fof(f3703,plain,
( ~ spl42_78
| ~ spl42_82 ),
inference(avatar_contradiction_clause,[],[f3702]) ).
fof(f3715,plain,
( h3(e10) != op2(h3(e11),e20)
| ~ spl42_108
| ~ spl42_189
| spl42_201 ),
inference(forward_demodulation,[],[f2453,f1121]) ).
fof(f3725,plain,
( e20 != op2(h3(e11),e20)
| ~ spl42_108
| ~ spl42_189
| spl42_201 ),
inference(forward_demodulation,[],[f3715,f1626]) ).
fof(f3744,plain,
( e12 != op1(e10,e11)
| ~ spl42_70 ),
inference(superposition,[],[f285,f960]) ).
fof(f3747,plain,
( $false
| ~ spl42_70
| ~ spl42_118 ),
inference(forward_subsumption_resolution,[],[f3744,f1164]) ).
fof(f3748,plain,
( ~ spl42_70
| ~ spl42_118 ),
inference(avatar_contradiction_clause,[],[f3747]) ).
fof(f3753,plain,
( ~ spl42_114
| ~ spl42_66 ),
inference(avatar_split_clause,[],[f3570,f941,f1145]) ).
fof(f3757,plain,
( $false
| ~ spl42_71
| ~ spl42_103 ),
inference(forward_subsumption_resolution,[],[f3578,f1100]) ).
fof(f3758,plain,
( ~ spl42_71
| ~ spl42_103 ),
inference(avatar_contradiction_clause,[],[f3757]) ).
fof(f3763,plain,
( $false
| ~ spl42_115
| ~ spl42_123 ),
inference(forward_subsumption_resolution,[],[f3551,f1185]) ).
fof(f3764,plain,
( ~ spl42_115
| ~ spl42_123 ),
inference(avatar_contradiction_clause,[],[f3763]) ).
fof(f3827,plain,
( e12 != op1(e11,e12)
| ~ spl42_94 ),
inference(superposition,[],[f258,f1062]) ).
fof(f3830,plain,
( e12 != op1(e10,e13)
| ~ spl42_94 ),
inference(superposition,[],[f275,f1062]) ).
fof(f3862,plain,
( op2(e21,e21) = h1(e11)
| ~ spl42_188 ),
inference(superposition,[],[f529,f3636]) ).
fof(f3866,plain,
( h1(e11) = h2(e10)
| ~ spl42_188 ),
inference(superposition,[],[f534,f3862]) ).
fof(f3867,plain,
( e21 = h1(e11)
| ~ spl42_175
| ~ spl42_188 ),
inference(forward_demodulation,[],[f3866,f1538]) ).
fof(f3869,plain,
( spl42_186
| ~ spl42_175
| ~ spl42_188 ),
inference(avatar_split_clause,[],[f3867,f1612,f1537,f1592]) ).
fof(f3870,plain,
( e21 != op2(e21,e21)
| ~ spl42_120
| ~ spl42_186
| ~ spl42_187
| spl42_239 ),
inference(superposition,[],[f3121,f1593]) ).
fof(f3871,plain,
( e21 != h2(e10)
| ~ spl42_120
| ~ spl42_186
| ~ spl42_187
| spl42_239 ),
inference(forward_demodulation,[],[f3870,f534]) ).
fof(f3872,plain,
( $false
| ~ spl42_120
| ~ spl42_175
| ~ spl42_186
| ~ spl42_187
| spl42_239 ),
inference(forward_subsumption_resolution,[],[f3871,f1538]) ).
fof(f3873,plain,
( ~ spl42_120
| ~ spl42_175
| ~ spl42_186
| ~ spl42_187
| spl42_239 ),
inference(avatar_contradiction_clause,[],[f3872]) ).
fof(f3875,plain,
( h1(op1(e10,e11)) = op2(h1(e10),e21)
| ~ spl42_186
| ~ spl42_239 ),
inference(forward_demodulation,[],[f2023,f1593]) ).
fof(f3877,plain,
( op2(e21,e21) = h1(op1(e10,e11))
| ~ spl42_186
| ~ spl42_187
| ~ spl42_239 ),
inference(forward_demodulation,[],[f3875,f1598]) ).
fof(f3878,plain,
( op2(e21,e21) = h1(e10)
| ~ spl42_120
| ~ spl42_186
| ~ spl42_187
| ~ spl42_239 ),
inference(forward_demodulation,[],[f3877,f1172]) ).
fof(f3879,plain,
( e21 = op2(e21,e21)
| ~ spl42_120
| ~ spl42_186
| ~ spl42_187
| ~ spl42_239 ),
inference(forward_demodulation,[],[f3878,f1598]) ).
fof(f3898,plain,
h3(e11) = op2(h3(e10),h3(e10)),
inference(superposition,[],[f537,f538]) ).
fof(f3899,plain,
( op2(e20,e20) = h3(e11)
| ~ spl42_189 ),
inference(forward_demodulation,[],[f3898,f1626]) ).
fof(f3900,plain,
( h1(e10) = h3(e11)
| ~ spl42_189 ),
inference(forward_demodulation,[],[f3899,f530]) ).
fof(f3901,plain,
( e21 = h3(e11)
| ~ spl42_187
| ~ spl42_189 ),
inference(forward_demodulation,[],[f3900,f1598]) ).
fof(f3902,plain,
( spl42_162
| ~ spl42_187
| ~ spl42_189 ),
inference(avatar_split_clause,[],[f3901,f1624,f1597,f1472]) ).
fof(f3903,plain,
( e20 != op2(e21,e20)
| ~ spl42_108
| ~ spl42_162
| ~ spl42_189
| spl42_201 ),
inference(superposition,[],[f3725,f1473]) ).
fof(f3904,plain,
( $false
| ~ spl42_36
| ~ spl42_108
| ~ spl42_162
| ~ spl42_189
| spl42_201 ),
inference(forward_subsumption_resolution,[],[f3903,f698]) ).
fof(f3905,plain,
( ~ spl42_36
| ~ spl42_108
| ~ spl42_162
| ~ spl42_189
| spl42_201 ),
inference(avatar_contradiction_clause,[],[f3904]) ).
fof(f3906,plain,
( h3(e10) != op2(h3(e12),h3(e12))
| ~ spl42_84
| spl42_196 ),
inference(forward_demodulation,[],[f1844,f1019]) ).
fof(f3908,plain,
( e20 != op2(h3(e12),h3(e12))
| ~ spl42_84
| ~ spl42_189
| spl42_196 ),
inference(forward_demodulation,[],[f3906,f1626]) ).
fof(f3912,plain,
h4(e11) = op2(h4(e10),h4(e10)),
inference(superposition,[],[f541,f542]) ).
fof(f3913,plain,
op2(e20,e20) = h4(e11),
inference(superposition,[],[f541,f344]) ).
fof(f3914,plain,
h1(e10) = h4(e11),
inference(forward_demodulation,[],[f3913,f530]) ).
fof(f3915,plain,
e21 = h4(e11),
inference(forward_demodulation,[],[f3912,f918]) ).
fof(f3917,plain,
spl42_150,
inference(avatar_split_clause,[],[f3915,f1412]) ).
fof(f3919,plain,
( e22 = op2(e21,e23)
| ~ spl42_150 ),
inference(superposition,[],[f917,f1413]) ).
fof(f3921,plain,
e12 = op1(e11,e13),
inference(superposition,[],[f178,f179]) ).
fof(f4217,plain,
h3(e12) = op2(op2(h3(e10),h3(e10)),e22),
inference(superposition,[],[f536,f538]) ).
fof(f4220,plain,
( h3(e12) = op2(op2(e20,e20),e22)
| ~ spl42_189 ),
inference(forward_demodulation,[],[f4217,f1626]) ).
fof(f4222,plain,
( h3(e12) = op2(h1(e10),e22)
| ~ spl42_189 ),
inference(forward_demodulation,[],[f4220,f530]) ).
fof(f4224,plain,
( op2(e21,e22) = h3(e12)
| ~ spl42_187
| ~ spl42_189 ),
inference(forward_demodulation,[],[f4222,f1598]) ).
fof(f4225,plain,
( e23 = h3(e12)
| ~ spl42_29
| ~ spl42_187
| ~ spl42_189 ),
inference(forward_demodulation,[],[f4224,f668]) ).
fof(f4226,plain,
( spl42_153
| ~ spl42_29
| ~ spl42_187
| ~ spl42_189 ),
inference(avatar_split_clause,[],[f4225,f1624,f1597,f666,f1427]) ).
fof(f4227,plain,
( e20 != op2(e23,e23)
| ~ spl42_84
| ~ spl42_153
| ~ spl42_189
| spl42_196 ),
inference(superposition,[],[f3908,f1428]) ).
fof(f4228,plain,
( $false
| ~ spl42_84
| ~ spl42_153
| ~ spl42_189
| spl42_196 ),
inference(forward_subsumption_resolution,[],[f4227,f344]) ).
fof(f4229,plain,
( ~ spl42_84
| ~ spl42_153
| ~ spl42_189
| spl42_196 ),
inference(avatar_contradiction_clause,[],[f4228]) ).
fof(f4231,plain,
( h3(op1(e12,e10)) != op2(h3(e12),e20)
| ~ spl42_189
| spl42_198 ),
inference(forward_demodulation,[],[f1852,f1626]) ).
fof(f4233,plain,
( op2(e23,e20) != h3(op1(e12,e10))
| ~ spl42_153
| ~ spl42_189
| spl42_198 ),
inference(forward_demodulation,[],[f4231,f1428]) ).
fof(f4235,plain,
( op2(e23,e20) != h3(e12)
| ~ spl42_90
| ~ spl42_153
| ~ spl42_189
| spl42_198 ),
inference(forward_demodulation,[],[f4233,f1045]) ).
fof(f4236,plain,
( e23 != op2(e23,e20)
| ~ spl42_90
| ~ spl42_153
| ~ spl42_189
| spl42_198 ),
inference(forward_demodulation,[],[f4235,f1428]) ).
fof(f4237,plain,
( $false
| ~ spl42_9
| ~ spl42_90
| ~ spl42_153
| ~ spl42_189
| spl42_198 ),
inference(forward_subsumption_resolution,[],[f4236,f582]) ).
fof(f4238,plain,
( ~ spl42_9
| ~ spl42_90
| ~ spl42_153
| ~ spl42_189
| spl42_198 ),
inference(avatar_contradiction_clause,[],[f4237]) ).
fof(f4239,plain,
( h3(op1(e12,e11)) != op2(h3(e12),e21)
| ~ spl42_162
| spl42_197 ),
inference(forward_demodulation,[],[f1848,f1473]) ).
fof(f4241,plain,
( op2(e23,e21) != h3(op1(e12,e11))
| ~ spl42_153
| ~ spl42_162
| spl42_197 ),
inference(forward_demodulation,[],[f4239,f1428]) ).
fof(f4243,plain,
( op2(e23,e21) != h3(e13)
| ~ spl42_85
| ~ spl42_153
| ~ spl42_162
| spl42_197 ),
inference(forward_demodulation,[],[f4241,f1024]) ).
fof(f4245,plain,
( e22 != op2(e23,e21)
| ~ spl42_85
| ~ spl42_153
| ~ spl42_162
| spl42_197 ),
inference(forward_demodulation,[],[f4243,f539]) ).
fof(f4247,plain,
( $false
| ~ spl42_6
| ~ spl42_85
| ~ spl42_153
| ~ spl42_162
| spl42_197 ),
inference(forward_subsumption_resolution,[],[f4245,f569]) ).
fof(f4248,plain,
( ~ spl42_6
| ~ spl42_85
| ~ spl42_153
| ~ spl42_162
| spl42_197 ),
inference(avatar_contradiction_clause,[],[f4247]) ).
fof(f4250,plain,
( op2(e21,e21) != h3(op1(e11,e11))
| ~ spl42_162
| spl42_200 ),
inference(forward_demodulation,[],[f1860,f1473]) ).
fof(f4252,plain,
( op2(e21,e21) != h3(e11)
| ~ spl42_103
| ~ spl42_162
| spl42_200 ),
inference(forward_demodulation,[],[f4250,f1100]) ).
fof(f4254,plain,
( e21 != op2(e21,e21)
| ~ spl42_103
| ~ spl42_162
| spl42_200 ),
inference(forward_demodulation,[],[f4252,f1473]) ).
fof(f4256,plain,
( $false
| ~ spl42_103
| ~ spl42_120
| ~ spl42_162
| ~ spl42_186
| ~ spl42_187
| spl42_200
| ~ spl42_239 ),
inference(forward_subsumption_resolution,[],[f4254,f3879]) ).
fof(f4257,plain,
( ~ spl42_103
| ~ spl42_120
| ~ spl42_162
| ~ spl42_186
| ~ spl42_187
| spl42_200
| ~ spl42_239 ),
inference(avatar_contradiction_clause,[],[f4256]) ).
fof(f4258,plain,
( h3(op1(e11,e12)) != op2(h3(e11),e23)
| ~ spl42_153
| spl42_199 ),
inference(forward_demodulation,[],[f1856,f1428]) ).
fof(f4260,plain,
( op2(e21,e23) != h3(op1(e11,e12))
| ~ spl42_153
| ~ spl42_162
| spl42_199 ),
inference(forward_demodulation,[],[f4258,f1473]) ).
fof(f4262,plain,
( op2(e21,e23) != h3(e13)
| ~ spl42_97
| ~ spl42_153
| ~ spl42_162
| spl42_199 ),
inference(forward_demodulation,[],[f4260,f1075]) ).
fof(f4264,plain,
( e22 != op2(e21,e23)
| ~ spl42_97
| ~ spl42_153
| ~ spl42_162
| spl42_199 ),
inference(forward_demodulation,[],[f4262,f539]) ).
fof(f4265,plain,
( $false
| ~ spl42_26
| ~ spl42_97
| ~ spl42_153
| ~ spl42_162
| spl42_199 ),
inference(forward_subsumption_resolution,[],[f4264,f655]) ).
fof(f4266,plain,
( ~ spl42_26
| ~ spl42_97
| ~ spl42_153
| ~ spl42_162
| spl42_199 ),
inference(avatar_contradiction_clause,[],[f4265]) ).
fof(f4268,plain,
( h3(op1(e10,e11)) != op2(h3(e10),e21)
| ~ spl42_162
| spl42_203 ),
inference(forward_demodulation,[],[f1872,f1473]) ).
fof(f4270,plain,
( op2(e20,e21) != h3(op1(e10,e11))
| ~ spl42_162
| ~ spl42_189
| spl42_203 ),
inference(forward_demodulation,[],[f4268,f1626]) ).
fof(f4272,plain,
( op2(e20,e21) != h3(e10)
| ~ spl42_120
| ~ spl42_162
| ~ spl42_189
| spl42_203 ),
inference(forward_demodulation,[],[f4270,f1172]) ).
fof(f4274,plain,
( e20 != op2(e20,e21)
| ~ spl42_120
| ~ spl42_162
| ~ spl42_189
| spl42_203 ),
inference(forward_demodulation,[],[f4272,f1626]) ).
fof(f4275,plain,
( $false
| ~ spl42_48
| ~ spl42_120
| ~ spl42_162
| ~ spl42_189
| spl42_203 ),
inference(forward_subsumption_resolution,[],[f4274,f749]) ).
fof(f4276,plain,
( ~ spl42_48
| ~ spl42_120
| ~ spl42_162
| ~ spl42_189
| spl42_203 ),
inference(avatar_contradiction_clause,[],[f4275]) ).
fof(f4277,plain,
( h3(op1(e10,e12)) != op2(h3(e10),e23)
| ~ spl42_153
| spl42_202 ),
inference(forward_demodulation,[],[f1868,f1428]) ).
fof(f4279,plain,
( op2(e20,e23) != h3(op1(e10,e12))
| ~ spl42_153
| ~ spl42_189
| spl42_202 ),
inference(forward_demodulation,[],[f4277,f1626]) ).
fof(f4281,plain,
( op2(e20,e23) != h3(e12)
| ~ spl42_114
| ~ spl42_153
| ~ spl42_189
| spl42_202 ),
inference(forward_demodulation,[],[f4279,f1147]) ).
fof(f4283,plain,
( e23 != op2(e20,e23)
| ~ spl42_114
| ~ spl42_153
| ~ spl42_189
| spl42_202 ),
inference(forward_demodulation,[],[f4281,f1428]) ).
fof(f4285,plain,
( $false
| ~ spl42_37
| ~ spl42_114
| ~ spl42_153
| ~ spl42_189
| spl42_202 ),
inference(forward_subsumption_resolution,[],[f4283,f703]) ).
fof(f4286,plain,
( ~ spl42_37
| ~ spl42_114
| ~ spl42_153
| ~ spl42_189
| spl42_202 ),
inference(avatar_contradiction_clause,[],[f4285]) ).
fof(f4287,plain,
( h3(op1(e10,e12)) = op2(h3(e10),e23)
| ~ spl42_153
| ~ spl42_202 ),
inference(forward_demodulation,[],[f1867,f1428]) ).
fof(f4288,plain,
( op2(e20,e22) != h3(op1(e10,e13))
| ~ spl42_189
| spl42_205 ),
inference(forward_demodulation,[],[f1880,f1626]) ).
fof(f4289,plain,
( op2(e20,e23) = h3(op1(e10,e12))
| ~ spl42_153
| ~ spl42_189
| ~ spl42_202 ),
inference(forward_demodulation,[],[f4287,f1626]) ).
fof(f4290,plain,
( op2(e20,e22) != h3(e13)
| ~ spl42_109
| ~ spl42_189
| spl42_205 ),
inference(forward_demodulation,[],[f4288,f1126]) ).
fof(f4292,plain,
( e22 != op2(e20,e22)
| ~ spl42_109
| ~ spl42_189
| spl42_205 ),
inference(forward_demodulation,[],[f4290,f539]) ).
fof(f4294,plain,
( $false
| ~ spl42_42
| ~ spl42_109
| ~ spl42_189
| spl42_205 ),
inference(forward_subsumption_resolution,[],[f4292,f724]) ).
fof(f4295,plain,
( ~ spl42_42
| ~ spl42_109
| ~ spl42_189
| spl42_205 ),
inference(avatar_contradiction_clause,[],[f4294]) ).
fof(f4296,plain,
( op2(e20,e20) != h3(op1(e10,e10))
| ~ spl42_189
| spl42_204 ),
inference(forward_demodulation,[],[f1876,f1626]) ).
fof(f4298,plain,
( op2(e20,e20) != h3(e11)
| ~ spl42_123
| ~ spl42_189
| spl42_204 ),
inference(forward_demodulation,[],[f4296,f1185]) ).
fof(f4300,plain,
( op2(e20,e20) != e21
| ~ spl42_123
| ~ spl42_162
| ~ spl42_189
| spl42_204 ),
inference(forward_demodulation,[],[f4298,f1473]) ).
fof(f4302,plain,
( $false
| ~ spl42_123
| ~ spl42_162
| ~ spl42_188
| ~ spl42_189
| spl42_204 ),
inference(forward_subsumption_resolution,[],[f4300,f3636]) ).
fof(f4303,plain,
( ~ spl42_123
| ~ spl42_162
| ~ spl42_188
| ~ spl42_189
| spl42_204 ),
inference(avatar_contradiction_clause,[],[f4302]) ).
fof(f4305,plain,
( op2(e23,e22) != h3(op1(e12,e13))
| ~ spl42_153
| spl42_207 ),
inference(forward_demodulation,[],[f1888,f1428]) ).
fof(f4307,plain,
( op2(e23,e22) != h3(e11)
| ~ spl42_79
| ~ spl42_153
| spl42_207 ),
inference(forward_demodulation,[],[f4305,f998]) ).
fof(f4309,plain,
( e21 != op2(e23,e22)
| ~ spl42_79
| ~ spl42_153
| ~ spl42_162
| spl42_207 ),
inference(forward_demodulation,[],[f4307,f1473]) ).
fof(f4310,plain,
( $false
| ~ spl42_3
| ~ spl42_79
| ~ spl42_153
| ~ spl42_162
| spl42_207 ),
inference(forward_subsumption_resolution,[],[f4309,f556]) ).
fof(f4311,plain,
( ~ spl42_3
| ~ spl42_79
| ~ spl42_153
| ~ spl42_162
| spl42_207 ),
inference(avatar_contradiction_clause,[],[f4310]) ).
fof(f4312,plain,
( op2(e21,e22) != h3(op1(e11,e13))
| ~ spl42_162
| spl42_206 ),
inference(forward_demodulation,[],[f1884,f1473]) ).
fof(f4314,plain,
( op2(e21,e22) != h3(e12)
| ~ spl42_94
| ~ spl42_162
| spl42_206 ),
inference(forward_demodulation,[],[f4312,f1062]) ).
fof(f4316,plain,
( e23 != op2(e21,e22)
| ~ spl42_94
| ~ spl42_153
| ~ spl42_162
| spl42_206 ),
inference(forward_demodulation,[],[f4314,f1428]) ).
fof(f4318,plain,
( $false
| ~ spl42_29
| ~ spl42_94
| ~ spl42_153
| ~ spl42_162
| spl42_206 ),
inference(forward_subsumption_resolution,[],[f4316,f668]) ).
fof(f4319,plain,
( ~ spl42_29
| ~ spl42_94
| ~ spl42_153
| ~ spl42_162
| spl42_206 ),
inference(avatar_contradiction_clause,[],[f4318]) ).
fof(f4321,plain,
( op2(e22,e21) != h3(op1(e13,e11))
| ~ spl42_162
| spl42_209 ),
inference(forward_demodulation,[],[f1896,f1473]) ).
fof(f4323,plain,
( op2(e22,e21) != h3(e12)
| ~ spl42_70
| ~ spl42_162
| spl42_209 ),
inference(forward_demodulation,[],[f4321,f960]) ).
fof(f4325,plain,
( e23 != op2(e22,e21)
| ~ spl42_70
| ~ spl42_153
| ~ spl42_162
| spl42_209 ),
inference(forward_demodulation,[],[f4323,f1428]) ).
fof(f4326,plain,
( $false
| ~ spl42_17
| ~ spl42_70
| ~ spl42_153
| ~ spl42_162
| spl42_209 ),
inference(forward_subsumption_resolution,[],[f4325,f617]) ).
fof(f4327,plain,
( ~ spl42_17
| ~ spl42_70
| ~ spl42_153
| ~ spl42_162
| spl42_209 ),
inference(avatar_contradiction_clause,[],[f4326]) ).
fof(f4328,plain,
( op2(e22,e20) != h3(op1(e13,e10))
| ~ spl42_189
| spl42_208 ),
inference(forward_demodulation,[],[f1892,f1626]) ).
fof(f4330,plain,
( op2(e22,e20) != h3(e13)
| ~ spl42_73
| ~ spl42_189
| spl42_208 ),
inference(forward_demodulation,[],[f4328,f973]) ).
fof(f4332,plain,
( e22 != op2(e22,e20)
| ~ spl42_73
| ~ spl42_189
| spl42_208 ),
inference(forward_demodulation,[],[f4330,f539]) ).
fof(f4334,plain,
( $false
| ~ spl42_22
| ~ spl42_73
| ~ spl42_189
| spl42_208 ),
inference(forward_subsumption_resolution,[],[f4332,f638]) ).
fof(f4335,plain,
( ~ spl42_22
| ~ spl42_73
| ~ spl42_189
| spl42_208 ),
inference(avatar_contradiction_clause,[],[f4334]) ).
fof(f4337,plain,
( h3(e10) != h3(e10)
| ~ spl42_64
| spl42_211 ),
inference(forward_demodulation,[],[f1904,f934]) ).
fof(f4338,plain,
( $false
| ~ spl42_64
| spl42_211 ),
inference(trivial_inequality_removal,[],[f4337]) ).
fof(f4339,plain,
( ~ spl42_64
| spl42_211 ),
inference(avatar_contradiction_clause,[],[f4338]) ).
fof(f4342,plain,
( op2(e22,e23) != h3(op1(e13,e12))
| ~ spl42_153
| spl42_210 ),
inference(forward_demodulation,[],[f1900,f1428]) ).
fof(f4343,plain,
( op2(e22,e23) != h3(e11)
| ~ spl42_67
| ~ spl42_153
| spl42_210 ),
inference(forward_demodulation,[],[f4342,f947]) ).
fof(f4344,plain,
( e21 != op2(e22,e23)
| ~ spl42_67
| ~ spl42_153
| ~ spl42_162
| spl42_210 ),
inference(forward_demodulation,[],[f4343,f1473]) ).
fof(f4345,plain,
( $false
| ~ spl42_15
| ~ spl42_67
| ~ spl42_153
| ~ spl42_162
| spl42_210 ),
inference(forward_subsumption_resolution,[],[f4344,f607]) ).
fof(f4346,plain,
( ~ spl42_15
| ~ spl42_67
| ~ spl42_153
| ~ spl42_162
| spl42_210 ),
inference(avatar_contradiction_clause,[],[f4345]) ).
fof(f4371,plain,
( e21 = h1(e10)
| ~ spl42_150 ),
inference(forward_demodulation,[],[f3914,f1413]) ).
fof(f4411,plain,
( spl42_26
| ~ spl42_150 ),
inference(avatar_split_clause,[],[f3919,f1412,f653]) ).
fof(f4436,plain,
( spl42_187
| ~ spl42_150 ),
inference(avatar_split_clause,[],[f4371,f1412,f1597]) ).
fof(f4545,plain,
( ~ spl42_18
| ~ spl42_6 ),
inference(avatar_split_clause,[],[f3626,f567,f619]) ).
fof(f4555,plain,
( ~ spl42_155
| ~ spl42_17 ),
inference(avatar_split_clause,[],[f3486,f615,f1437]) ).
fof(f4563,plain,
( ~ spl42_171
| ~ spl42_26 ),
inference(avatar_split_clause,[],[f3489,f653,f1517]) ).
fof(f4565,plain,
( ~ spl42_38
| ~ spl42_26 ),
inference(avatar_split_clause,[],[f3619,f653,f705]) ).
fof(f4573,plain,
( ~ spl42_159
| ~ spl42_42 ),
inference(avatar_split_clause,[],[f3507,f722,f1457]) ).
fof(f4575,plain,
( ~ spl42_190
| ~ spl42_48 ),
inference(avatar_split_clause,[],[f3511,f747,f1636]) ).
fof(f4578,plain,
( e11 = e12
| ~ spl42_122
| ~ spl42_123 ),
inference(forward_demodulation,[],[f1181,f1185]) ).
fof(f4671,plain,
( $false
| ~ spl42_122
| ~ spl42_123 ),
inference(forward_subsumption_resolution,[],[f4578,f174]) ).
fof(f4672,plain,
( ~ spl42_122
| ~ spl42_123 ),
inference(avatar_contradiction_clause,[],[f4671]) ).
fof(f4780,plain,
( op2(e20,e23) = h3(e13)
| ~ spl42_113
| ~ spl42_153
| ~ spl42_189
| ~ spl42_202 ),
inference(forward_demodulation,[],[f4289,f1143]) ).
fof(f4808,plain,
spl42_94,
inference(avatar_split_clause,[],[f3921,f1060]) ).
fof(f4818,plain,
( e22 = op2(e20,e23)
| ~ spl42_113
| ~ spl42_153
| ~ spl42_189
| ~ spl42_202 ),
inference(forward_demodulation,[],[f4780,f539]) ).
fof(f4838,plain,
( spl42_38
| ~ spl42_113
| ~ spl42_153
| ~ spl42_189
| ~ spl42_202 ),
inference(avatar_split_clause,[],[f4818,f1866,f1624,f1427,f1141,f705]) ).
fof(f4847,plain,
( ~ spl42_98
| ~ spl42_94 ),
inference(avatar_split_clause,[],[f3827,f1060,f1077]) ).
fof(f4848,plain,
( ~ spl42_110
| ~ spl42_94 ),
inference(avatar_split_clause,[],[f3830,f1060,f1128]) ).
fof(f4949,plain,
( e22 != op2(e20,e22)
| ~ spl42_2 ),
inference(superposition,[],[f465,f552]) ).
fof(f4954,plain,
( $false
| ~ spl42_2
| ~ spl42_42 ),
inference(forward_subsumption_resolution,[],[f4949,f724]) ).
fof(f4955,plain,
( ~ spl42_2
| ~ spl42_42 ),
inference(avatar_contradiction_clause,[],[f4954]) ).
fof(f4971,plain,
( e20 != h4(e10)
| ~ spl42_4 ),
inference(superposition,[],[f784,f560]) ).
fof(f4975,plain,
( $false
| ~ spl42_4
| ~ spl42_188 ),
inference(forward_subsumption_resolution,[],[f4971,f1614]) ).
fof(f4976,plain,
( ~ spl42_4
| ~ spl42_188 ),
inference(avatar_contradiction_clause,[],[f4975]) ).
fof(f4988,plain,
( e23 != op2(e23,e20)
| ~ spl42_1 ),
inference(superposition,[],[f436,f548]) ).
fof(f4996,plain,
( $false
| ~ spl42_1
| ~ spl42_9 ),
inference(forward_subsumption_resolution,[],[f4988,f582]) ).
fof(f4997,plain,
( ~ spl42_1
| ~ spl42_9 ),
inference(avatar_contradiction_clause,[],[f4996]) ).
cnf(s1,plain,
( spl42_1
| spl42_2
| spl42_3
| spl42_4 ),
inference(sat_conversion,[],[f561]) ).
cnf(s53,plain,
( spl42_61
| spl42_77
| spl42_93
| spl42_109 ),
inference(sat_conversion,[],[f1191]) ).
cnf(s56,plain,
( spl42_62
| spl42_66
| spl42_70
| spl42_74 ),
inference(sat_conversion,[],[f1194]) ).
cnf(s57,plain,
( spl42_63
| spl42_79
| spl42_95
| spl42_111 ),
inference(sat_conversion,[],[f1195]) ).
cnf(s58,plain,
( spl42_63
| spl42_67
| spl42_71
| spl42_75 ),
inference(sat_conversion,[],[f1196]) ).
cnf(s61,plain,
( spl42_65
| spl42_81
| spl42_97
| spl42_113 ),
inference(sat_conversion,[],[f1199]) ).
cnf(s65,plain,
( spl42_67
| spl42_83
| spl42_99
| spl42_115 ),
inference(sat_conversion,[],[f1203]) ).
cnf(s67,plain,
( spl42_68
| spl42_84
| spl42_100
| spl42_116 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s69,plain,
( spl42_69
| spl42_85
| spl42_101
| spl42_117 ),
inference(sat_conversion,[],[f1207]) ).
cnf(s70,plain,
( spl42_93
| spl42_97
| spl42_101
| spl42_105 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s73,plain,
( spl42_71
| spl42_87
| spl42_103
| spl42_119 ),
inference(sat_conversion,[],[f1211]) ).
cnf(s78,plain,
( spl42_109
| spl42_113
| spl42_117
| spl42_121 ),
inference(sat_conversion,[],[f1216]) ).
cnf(s80,plain,
( spl42_110
| spl42_114
| spl42_118
| spl42_122 ),
inference(sat_conversion,[],[f1218]) ).
cnf(s83,plain,
( spl42_76
| spl42_92
| spl42_108
| spl42_124 ),
inference(sat_conversion,[],[f1221]) ).
cnf(s87,plain,
( spl42_124
| spl42_125
| spl42_126
| spl42_127
| spl42_128
| spl42_129
| spl42_130
| spl42_131
| spl42_132
| spl42_133
| spl42_134
| spl42_135
| spl42_136
| spl42_137
| spl42_138
| spl42_139 ),
inference(sat_conversion,[],[f1285]) ).
cnf(s90,plain,
( ~ spl42_64
| spl42_73 ),
inference(sat_conversion,[],[f1288]) ).
cnf(s91,plain,
( spl42_78
| ~ spl42_81 ),
inference(sat_conversion,[],[f1289]) ).
cnf(s92,plain,
( ~ spl42_83
| spl42_86 ),
inference(sat_conversion,[],[f1290]) ).
cnf(s93,plain,
( ~ spl42_84
| spl42_90 ),
inference(sat_conversion,[],[f1291]) ).
cnf(s94,plain,
( spl42_95
| ~ spl42_101 ),
inference(sat_conversion,[],[f1292]) ).
cnf(s97,plain,
( spl42_112
| ~ spl42_121 ),
inference(sat_conversion,[],[f1295]) ).
cnf(s99,plain,
( spl42_120
| ~ spl42_123 ),
inference(sat_conversion,[],[f1297]) ).
cnf(s100,plain,
( spl42_61
| spl42_82
| spl42_103
| spl42_124 ),
inference(sat_conversion,[],[f1298]) ).
cnf(s103,plain,
( spl42_61
| ~ spl42_125 ),
inference(sat_conversion,[],[f1301]) ).
cnf(s106,plain,
( spl42_65
| ~ spl42_126 ),
inference(sat_conversion,[],[f1304]) ).
cnf(s108,plain,
( spl42_93
| ~ spl42_127 ),
inference(sat_conversion,[],[f1306]) ).
cnf(s111,plain,
( spl42_109
| ~ spl42_128 ),
inference(sat_conversion,[],[f1309]) ).
cnf(s115,plain,
( spl42_78
| ~ spl42_129 ),
inference(sat_conversion,[],[f1313]) ).
cnf(s116,plain,
( ~ spl42_82
| ~ spl42_130 ),
inference(sat_conversion,[],[f1314]) ).
cnf(s120,plain,
( spl42_98
| ~ spl42_131 ),
inference(sat_conversion,[],[f1318]) ).
cnf(s123,plain,
( spl42_114
| ~ spl42_132 ),
inference(sat_conversion,[],[f1321]) ).
cnf(s127,plain,
( spl42_95
| ~ spl42_133 ),
inference(sat_conversion,[],[f1325]) ).
cnf(s128,plain,
( ~ spl42_82
| ~ spl42_134 ),
inference(sat_conversion,[],[f1326]) ).
cnf(s133,plain,
( spl42_103
| ~ spl42_135 ),
inference(sat_conversion,[],[f1331]) ).
cnf(s135,plain,
( spl42_119
| ~ spl42_136 ),
inference(sat_conversion,[],[f1333]) ).
cnf(s138,plain,
( spl42_76
| ~ spl42_137 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s140,plain,
( ~ spl42_82
| ~ spl42_138 ),
inference(sat_conversion,[],[f1338]) ).
cnf(s144,plain,
( spl42_108
| ~ spl42_139 ),
inference(sat_conversion,[],[f1342]) ).
cnf(s146,plain,
spl42_64,
inference(sat_conversion,[],[f1344]) ).
cnf(s156,plain,
( ~ spl42_152
| ~ spl42_153 ),
inference(sat_conversion,[],[f1430]) ).
cnf(s163,plain,
( ~ spl42_160
| ~ spl42_162 ),
inference(sat_conversion,[],[f1475]) ).
cnf(s186,plain,
( spl42_2
| spl42_6
| spl42_10
| spl42_147 ),
inference(sat_conversion,[],[f1608]) ).
cnf(s187,plain,
( spl42_15
| spl42_27
| spl42_39
| spl42_151 ),
inference(sat_conversion,[],[f1609]) ).
cnf(s191,plain,
( spl42_1
| spl42_29
| spl42_41
| spl42_155 ),
inference(sat_conversion,[],[f1617]) ).
cnf(s194,plain,
( spl42_14
| spl42_18
| spl42_22
| spl42_159 ),
inference(sat_conversion,[],[f1620]) ).
cnf(s199,plain,
( spl42_5
| spl42_17
| spl42_45
| spl42_167 ),
inference(sat_conversion,[],[f1629]) ).
cnf(s206,plain,
( spl42_28
| spl42_32
| spl42_36
| spl42_190 ),
inference(sat_conversion,[],[f1640]) ).
cnf(s208,plain,
( spl42_37
| spl42_41
| spl42_45
| spl42_179 ),
inference(sat_conversion,[],[f1642]) ).
cnf(s210,plain,
( spl42_38
| spl42_42
| spl42_46
| spl42_183 ),
inference(sat_conversion,[],[f1644]) ).
cnf(s219,plain,
( spl42_5
| ~ spl42_151 ),
inference(sat_conversion,[],[f1669]) ).
cnf(s220,plain,
( spl42_9
| ~ spl42_188 ),
inference(sat_conversion,[],[f1670]) ).
cnf(s222,plain,
( spl42_18
| ~ spl42_163 ),
inference(sat_conversion,[],[f1672]) ).
cnf(s224,plain,
( spl42_27
| ~ spl42_167 ),
inference(sat_conversion,[],[f1674]) ).
cnf(s229,plain,
( spl42_48
| ~ spl42_187 ),
inference(sat_conversion,[],[f1679]) ).
cnf(s252,plain,
~ spl42_156,
inference(sat_conversion,[],[f1719]) ).
cnf(s255,plain,
( spl42_155
| spl42_159
| spl42_163
| spl42_189 ),
inference(sat_conversion,[],[f1764]) ).
cnf(s256,plain,
( spl42_167
| spl42_171
| spl42_175
| spl42_190 ),
inference(sat_conversion,[],[f1765]) ).
cnf(s261,plain,
( spl42_152
| spl42_156
| spl42_160
| ~ spl42_189
| ~ spl42_196
| ~ spl42_197
| ~ spl42_198
| ~ spl42_199
| ~ spl42_200
| ~ spl42_201
| ~ spl42_202
| ~ spl42_203
| ~ spl42_204
| ~ spl42_205
| ~ spl42_206
| ~ spl42_207
| ~ spl42_208
| ~ spl42_209
| ~ spl42_210
| ~ spl42_211 ),
inference(sat_conversion,[],[f1911]) ).
cnf(s284,plain,
( ~ spl42_26
| ~ spl42_27 ),
inference(sat_conversion,[],[f2212]) ).
cnf(s286,plain,
( ~ spl42_29
| ~ spl42_32 ),
inference(sat_conversion,[],[f2220]) ).
cnf(s291,plain,
( ~ spl42_14
| ~ spl42_15 ),
inference(sat_conversion,[],[f2236]) ).
cnf(s303,plain,
( ~ spl42_5
| ~ spl42_6 ),
inference(sat_conversion,[],[f2298]) ).
cnf(s307,plain,
( ~ spl42_9
| ~ spl42_10 ),
inference(sat_conversion,[],[f2315]) ).
cnf(s311,plain,
( ~ spl42_26
| ~ spl42_28 ),
inference(sat_conversion,[],[f2337]) ).
cnf(s317,plain,
( ~ spl42_41
| ~ spl42_42 ),
inference(sat_conversion,[],[f2364]) ).
cnf(s327,plain,
( ~ spl42_179
| ~ spl42_187 ),
inference(sat_conversion,[],[f2419]) ).
cnf(s332,plain,
( ~ spl42_46
| ~ spl42_48 ),
inference(sat_conversion,[],[f2460]) ).
cnf(s350,plain,
( ~ spl42_183
| ~ spl42_187 ),
inference(sat_conversion,[],[f2590]) ).
cnf(s357,plain,
( ~ spl42_147
| ~ spl42_188 ),
inference(sat_conversion,[],[f2641]) ).
cnf(s369,plain,
( ~ spl42_37
| ~ spl42_39 ),
inference(sat_conversion,[],[f2733]) ).
cnf(s383,plain,
( ~ spl42_45
| ~ spl42_48 ),
inference(sat_conversion,[],[f2867]) ).
cnf(s388,plain,
( ~ spl42_73
| ~ spl42_75 ),
inference(sat_conversion,[],[f2890]) ).
cnf(s390,plain,
( ~ spl42_66
| ~ spl42_67 ),
inference(sat_conversion,[],[f2897]) ).
cnf(s391,plain,
( ~ spl42_62
| ~ spl42_64 ),
inference(sat_conversion,[],[f2903]) ).
cnf(s392,plain,
( ~ spl42_65
| ~ spl42_67 ),
inference(sat_conversion,[],[f2905]) ).
cnf(s395,plain,
( ~ spl42_77
| ~ spl42_79 ),
inference(sat_conversion,[],[f2918]) ).
cnf(s397,plain,
( ~ spl42_111
| ~ spl42_112 ),
inference(sat_conversion,[],[f2927]) ).
cnf(s402,plain,
( ~ spl42_85
| ~ spl42_86 ),
inference(sat_conversion,[],[f2947]) ).
cnf(s406,plain,
( ~ spl42_93
| ~ spl42_94 ),
inference(sat_conversion,[],[f2967]) ).
cnf(s410,plain,
( ~ spl42_78
| ~ spl42_79 ),
inference(sat_conversion,[],[f2982]) ).
cnf(s411,plain,
( ~ spl42_63
| ~ spl42_64 ),
inference(sat_conversion,[],[f2987]) ).
cnf(s412,plain,
( ~ spl42_69
| ~ spl42_70 ),
inference(sat_conversion,[],[f2989]) ).
cnf(s414,plain,
( ~ spl42_114
| ~ spl42_116 ),
inference(sat_conversion,[],[f2999]) ).
cnf(s416,plain,
( ~ spl42_85
| ~ spl42_87 ),
inference(sat_conversion,[],[f3011]) ).
cnf(s430,plain,
( ~ spl42_109
| ~ spl42_111 ),
inference(sat_conversion,[],[f3083]) ).
cnf(s432,plain,
( ~ spl42_69
| ~ spl42_71 ),
inference(sat_conversion,[],[f3097]) ).
cnf(s434,plain,
( ~ spl42_73
| ~ spl42_74 ),
inference(sat_conversion,[],[f3107]) ).
cnf(s435,plain,
( ~ spl42_117
| ~ spl42_120 ),
inference(sat_conversion,[],[f3119]) ).
cnf(s443,plain,
( ~ spl42_97
| ~ spl42_99 ),
inference(sat_conversion,[],[f3169]) ).
cnf(s444,plain,
( ~ spl42_65
| ~ spl42_66 ),
inference(sat_conversion,[],[f3174]) ).
cnf(s447,plain,
( ~ spl42_90
| ~ spl42_92 ),
inference(sat_conversion,[],[f3192]) ).
cnf(s448,plain,
( ~ spl42_105
| ~ spl42_108 ),
inference(sat_conversion,[],[f3202]) ).
cnf(s452,plain,
( ~ spl42_61
| ~ spl42_64 ),
inference(sat_conversion,[],[f3239]) ).
cnf(s453,plain,
( ~ spl42_70
| ~ spl42_71 ),
inference(sat_conversion,[],[f3241]) ).
cnf(s454,plain,
( ~ spl42_97
| ~ spl42_100 ),
inference(sat_conversion,[],[f3243]) ).
cnf(s456,plain,
( ~ spl42_73
| ~ spl42_76 ),
inference(sat_conversion,[],[f3259]) ).
cnf(s458,plain,
( ~ spl42_94
| ~ spl42_95 ),
inference(sat_conversion,[],[f3275]) ).
cnf(s459,plain,
( ~ spl42_81
| ~ spl42_82 ),
inference(sat_conversion,[],[f3286]) ).
cnf(s469,plain,
( ~ spl42_67
| ~ spl42_68 ),
inference(sat_conversion,[],[f3349]) ).
cnf(s471,plain,
( ~ spl42_119
| ~ spl42_120 ),
inference(sat_conversion,[],[f3353]) ).
cnf(s480,plain,
spl42_188,
inference(sat_conversion,[],[f3418]) ).
cnf(s485,plain,
( ~ spl42_64
| ~ spl42_124 ),
inference(sat_conversion,[],[f3642]) ).
cnf(s486,plain,
( ~ spl42_64
| spl42_123 ),
inference(sat_conversion,[],[f3649]) ).
cnf(s496,plain,
( ~ spl42_109
| ~ spl42_113 ),
inference(sat_conversion,[],[f3684]) ).
cnf(s499,plain,
( ~ spl42_78
| ~ spl42_82 ),
inference(sat_conversion,[],[f3703]) ).
cnf(s501,plain,
( ~ spl42_70
| ~ spl42_118 ),
inference(sat_conversion,[],[f3748]) ).
cnf(s503,plain,
( ~ spl42_66
| ~ spl42_114 ),
inference(sat_conversion,[],[f3753]) ).
cnf(s504,plain,
( ~ spl42_71
| ~ spl42_103 ),
inference(sat_conversion,[],[f3758]) ).
cnf(s505,plain,
( ~ spl42_115
| ~ spl42_123 ),
inference(sat_conversion,[],[f3764]) ).
cnf(s508,plain,
( ~ spl42_175
| spl42_186
| ~ spl42_188 ),
inference(sat_conversion,[],[f3869]) ).
cnf(s510,plain,
( ~ spl42_120
| ~ spl42_175
| ~ spl42_186
| ~ spl42_187
| spl42_239 ),
inference(sat_conversion,[],[f3873]) ).
cnf(s514,plain,
( spl42_162
| ~ spl42_187
| ~ spl42_189 ),
inference(sat_conversion,[],[f3902]) ).
cnf(s515,plain,
( ~ spl42_36
| ~ spl42_108
| ~ spl42_162
| ~ spl42_189
| spl42_201 ),
inference(sat_conversion,[],[f3905]) ).
cnf(s516,plain,
spl42_150,
inference(sat_conversion,[],[f3917]) ).
cnf(s558,plain,
( ~ spl42_29
| spl42_153
| ~ spl42_187
| ~ spl42_189 ),
inference(sat_conversion,[],[f4226]) ).
cnf(s559,plain,
( ~ spl42_84
| ~ spl42_153
| ~ spl42_189
| spl42_196 ),
inference(sat_conversion,[],[f4229]) ).
cnf(s560,plain,
( ~ spl42_9
| ~ spl42_90
| ~ spl42_153
| ~ spl42_189
| spl42_198 ),
inference(sat_conversion,[],[f4238]) ).
cnf(s561,plain,
( ~ spl42_6
| ~ spl42_85
| ~ spl42_153
| ~ spl42_162
| spl42_197 ),
inference(sat_conversion,[],[f4248]) ).
cnf(s562,plain,
( ~ spl42_103
| ~ spl42_120
| ~ spl42_162
| ~ spl42_186
| ~ spl42_187
| spl42_200
| ~ spl42_239 ),
inference(sat_conversion,[],[f4257]) ).
cnf(s563,plain,
( ~ spl42_26
| ~ spl42_97
| ~ spl42_153
| ~ spl42_162
| spl42_199 ),
inference(sat_conversion,[],[f4266]) ).
cnf(s564,plain,
( ~ spl42_48
| ~ spl42_120
| ~ spl42_162
| ~ spl42_189
| spl42_203 ),
inference(sat_conversion,[],[f4276]) ).
cnf(s565,plain,
( ~ spl42_37
| ~ spl42_114
| ~ spl42_153
| ~ spl42_189
| spl42_202 ),
inference(sat_conversion,[],[f4286]) ).
cnf(s566,plain,
( ~ spl42_42
| ~ spl42_109
| ~ spl42_189
| spl42_205 ),
inference(sat_conversion,[],[f4295]) ).
cnf(s567,plain,
( ~ spl42_123
| ~ spl42_162
| ~ spl42_188
| ~ spl42_189
| spl42_204 ),
inference(sat_conversion,[],[f4303]) ).
cnf(s568,plain,
( ~ spl42_3
| ~ spl42_79
| ~ spl42_153
| ~ spl42_162
| spl42_207 ),
inference(sat_conversion,[],[f4311]) ).
cnf(s569,plain,
( ~ spl42_29
| ~ spl42_94
| ~ spl42_153
| ~ spl42_162
| spl42_206 ),
inference(sat_conversion,[],[f4319]) ).
cnf(s570,plain,
( ~ spl42_17
| ~ spl42_70
| ~ spl42_153
| ~ spl42_162
| spl42_209 ),
inference(sat_conversion,[],[f4327]) ).
cnf(s571,plain,
( ~ spl42_22
| ~ spl42_73
| ~ spl42_189
| spl42_208 ),
inference(sat_conversion,[],[f4335]) ).
cnf(s572,plain,
( ~ spl42_64
| spl42_211 ),
inference(sat_conversion,[],[f4339]) ).
cnf(s573,plain,
( ~ spl42_15
| ~ spl42_67
| ~ spl42_153
| ~ spl42_162
| spl42_210 ),
inference(sat_conversion,[],[f4346]) ).
cnf(s579,plain,
( spl42_26
| ~ spl42_150 ),
inference(sat_conversion,[],[f4411]) ).
cnf(s584,plain,
( ~ spl42_150
| spl42_187 ),
inference(sat_conversion,[],[f4436]) ).
cnf(s612,plain,
( ~ spl42_6
| ~ spl42_18 ),
inference(sat_conversion,[],[f4545]) ).
cnf(s620,plain,
( ~ spl42_17
| ~ spl42_155 ),
inference(sat_conversion,[],[f4555]) ).
cnf(s624,plain,
( ~ spl42_26
| ~ spl42_171 ),
inference(sat_conversion,[],[f4563]) ).
cnf(s625,plain,
( ~ spl42_26
| ~ spl42_38 ),
inference(sat_conversion,[],[f4565]) ).
cnf(s631,plain,
( ~ spl42_42
| ~ spl42_159 ),
inference(sat_conversion,[],[f4573]) ).
cnf(s632,plain,
( ~ spl42_48
| ~ spl42_190 ),
inference(sat_conversion,[],[f4575]) ).
cnf(s636,plain,
( ~ spl42_122
| ~ spl42_123 ),
inference(sat_conversion,[],[f4672]) ).
cnf(s639,plain,
spl42_94,
inference(sat_conversion,[],[f4808]) ).
cnf(s641,plain,
( spl42_38
| ~ spl42_113
| ~ spl42_153
| ~ spl42_189
| ~ spl42_202 ),
inference(sat_conversion,[],[f4838]) ).
cnf(s647,plain,
( ~ spl42_94
| ~ spl42_98 ),
inference(sat_conversion,[],[f4847]) ).
cnf(s648,plain,
( ~ spl42_94
| ~ spl42_110 ),
inference(sat_conversion,[],[f4848]) ).
cnf(s649,plain,
( ~ spl42_2
| ~ spl42_42 ),
inference(sat_conversion,[],[f4955]) ).
cnf(s652,plain,
( ~ spl42_4
| ~ spl42_188 ),
inference(sat_conversion,[],[f4976]) ).
cnf(s654,plain,
( ~ spl42_1
| ~ spl42_9 ),
inference(sat_conversion,[],[f4997]) ).
cnf(s655,plain,
~ spl42_110,
inference(rat,[],[s648,s639]) ).
cnf(s656,plain,
~ spl42_98,
inference(rat,[],[s647,s639]) ).
cnf(s658,plain,
( ~ spl42_29
| ~ spl42_153
| ~ spl42_162
| spl42_206 ),
inference(rat,[],[s569,s639]) ).
cnf(s661,plain,
spl42_187,
inference(rat,[],[s584,s516]) ).
cnf(s662,plain,
spl42_26,
inference(rat,[],[s579,s516]) ).
cnf(s663,plain,
~ spl42_38,
inference(rat,[],[s625,s662]) ).
cnf(s664,plain,
~ spl42_171,
inference(rat,[],[s624,s662]) ).
cnf(s666,plain,
( spl42_162
| ~ spl42_189 ),
inference(rat,[],[s514,s661]) ).
cnf(s668,plain,
( ~ spl42_120
| ~ spl42_175
| ~ spl42_186
| spl42_239 ),
inference(rat,[],[s510,s661]) ).
cnf(s669,plain,
~ spl42_4,
inference(rat,[],[s652,s480]) ).
cnf(s670,plain,
~ spl42_95,
inference(rat,[],[s458,s639]) ).
cnf(s671,plain,
~ spl42_93,
inference(rat,[],[s406,s639]) ).
cnf(s672,plain,
~ spl42_147,
inference(rat,[],[s357,s480]) ).
cnf(s673,plain,
~ spl42_183,
inference(rat,[],[s350,s661]) ).
cnf(s674,plain,
~ spl42_179,
inference(rat,[],[s327,s661]) ).
cnf(s676,plain,
~ spl42_28,
inference(rat,[],[s311,s662]) ).
cnf(s678,plain,
~ spl42_27,
inference(rat,[],[s284,s662]) ).
cnf(s682,plain,
( spl42_167
| spl42_175
| spl42_190 ),
inference(rat,[],[s256,s664]) ).
cnf(s684,plain,
spl42_48,
inference(rat,[],[s229,s661]) ).
cnf(s685,plain,
~ spl42_190,
inference(rat,[],[s632,s684]) ).
cnf(s686,plain,
~ spl42_45,
inference(rat,[],[s383,s684]) ).
cnf(s687,plain,
~ spl42_46,
inference(rat,[],[s332,s684]) ).
cnf(s689,plain,
~ spl42_167,
inference(rat,[],[s224,s678]) ).
cnf(s690,plain,
spl42_175,
inference(rat,[],[s682,s685,s689]) ).
cnf(s693,plain,
spl42_186,
inference(rat,[],[s508,s480,s690]) ).
cnf(s698,plain,
spl42_9,
inference(rat,[],[s220,s480]) ).
cnf(s699,plain,
~ spl42_1,
inference(rat,[],[s654,s698]) ).
cnf(s701,plain,
~ spl42_10,
inference(rat,[],[s307,s698]) ).
cnf(s705,plain,
spl42_42,
inference(rat,[],[s210,s673,s687,s663]) ).
cnf(s706,plain,
~ spl42_2,
inference(rat,[],[s649,s705]) ).
cnf(s707,plain,
~ spl42_159,
inference(rat,[],[s631,s705]) ).
cnf(s709,plain,
~ spl42_41,
inference(rat,[],[s317,s705]) ).
cnf(s712,plain,
spl42_37,
inference(rat,[],[s208,s674,s686,s709]) ).
cnf(s713,plain,
~ spl42_39,
inference(rat,[],[s369,s712]) ).
cnf(s714,plain,
( spl42_32
| spl42_36 ),
inference(rat,[],[s206,s685,s676]) ).
cnf(s717,plain,
( spl42_5
| spl42_17 ),
inference(rat,[],[s199,s689,s686]) ).
cnf(s719,plain,
( spl42_14
| spl42_18
| spl42_22 ),
inference(rat,[],[s194,s707]) ).
cnf(s720,plain,
( spl42_29
| spl42_155 ),
inference(rat,[],[s191,s709,s699]) ).
cnf(s721,plain,
( spl42_15
| spl42_151 ),
inference(rat,[],[s187,s713,s678]) ).
cnf(s722,plain,
spl42_6,
inference(rat,[],[s186,s672,s701,s706]) ).
cnf(s723,plain,
~ spl42_18,
inference(rat,[],[s612,s722]) ).
cnf(s725,plain,
~ spl42_5,
inference(rat,[],[s303,s722]) ).
cnf(s727,plain,
~ spl42_163,
inference(rat,[],[s222,s723]) ).
cnf(s728,plain,
~ spl42_151,
inference(rat,[],[s219,s725]) ).
cnf(s729,plain,
spl42_17,
inference(rat,[],[s717,s725]) ).
cnf(s730,plain,
spl42_15,
inference(rat,[],[s721,s728]) ).
cnf(s731,plain,
~ spl42_155,
inference(rat,[],[s620,s729]) ).
cnf(s737,plain,
~ spl42_14,
inference(rat,[],[s291,s730]) ).
cnf(s738,plain,
spl42_189,
inference(rat,[],[s255,s727,s707,s731]) ).
cnf(s739,plain,
spl42_29,
inference(rat,[],[s720,s731]) ).
cnf(s740,plain,
spl42_22,
inference(rat,[],[s719,s723,s737]) ).
cnf(s741,plain,
spl42_162,
inference(rat,[],[s666,s738]) ).
cnf(s742,plain,
spl42_153,
inference(rat,[],[s558,s738,s661,s739]) ).
cnf(s744,plain,
~ spl42_32,
inference(rat,[],[s286,s739]) ).
cnf(s747,plain,
spl42_206,
inference(rat,[],[s658,s739,s741,s742]) ).
cnf(s748,plain,
spl42_36,
inference(rat,[],[s714,s744]) ).
cnf(s755,plain,
~ spl42_160,
inference(rat,[],[s163,s741]) ).
cnf(s756,plain,
~ spl42_152,
inference(rat,[],[s156,s742]) ).
cnf(s758,plain,
spl42_211,
inference(rat,[],[s572,s146]) ).
cnf(s761,plain,
spl42_123,
inference(rat,[],[s486,s146]) ).
cnf(s762,plain,
~ spl42_124,
inference(rat,[],[s485,s146]) ).
cnf(s763,plain,
~ spl42_61,
inference(rat,[],[s452,s146]) ).
cnf(s764,plain,
~ spl42_63,
inference(rat,[],[s411,s146]) ).
cnf(s765,plain,
~ spl42_62,
inference(rat,[],[s391,s146]) ).
cnf(s766,plain,
~ spl42_122,
inference(rat,[],[s636,s761]) ).
cnf(s767,plain,
spl42_204,
inference(rat,[],[s567,s741,s738,s480,s761]) ).
cnf(s769,plain,
~ spl42_115,
inference(rat,[],[s505,s761]) ).
cnf(s770,plain,
~ spl42_133,
inference(rat,[],[s127,s670]) ).
cnf(s771,plain,
~ spl42_131,
inference(rat,[],[s120,s656]) ).
cnf(s772,plain,
~ spl42_127,
inference(rat,[],[s108,s671]) ).
cnf(s773,plain,
~ spl42_125,
inference(rat,[],[s103,s763]) ).
cnf(s774,plain,
( spl42_82
| spl42_103 ),
inference(rat,[],[s100,s762,s763]) ).
cnf(s775,plain,
spl42_120,
inference(rat,[],[s99,s761]) ).
cnf(s776,plain,
spl42_203,
inference(rat,[],[s564,s741,s738,s684,s775]) ).
cnf(s778,plain,
spl42_239,
inference(rat,[],[s668,s693,s690,s775]) ).
cnf(s779,plain,
~ spl42_119,
inference(rat,[],[s471,s775]) ).
cnf(s780,plain,
~ spl42_117,
inference(rat,[],[s435,s775]) ).
cnf(s783,plain,
~ spl42_136,
inference(rat,[],[s135,s779]) ).
cnf(s784,plain,
~ spl42_101,
inference(rat,[],[s94,s670]) ).
cnf(s785,plain,
spl42_73,
inference(rat,[],[s90,s146]) ).
cnf(s786,plain,
spl42_208,
inference(rat,[],[s571,s740,s738,s785]) ).
cnf(s789,plain,
~ spl42_76,
inference(rat,[],[s456,s785]) ).
cnf(s790,plain,
~ spl42_74,
inference(rat,[],[s434,s785]) ).
cnf(s791,plain,
~ spl42_75,
inference(rat,[],[s388,s785]) ).
cnf(s792,plain,
~ spl42_137,
inference(rat,[],[s138,s789]) ).
cnf(s793,plain,
( spl42_126
| spl42_128
| spl42_129
| spl42_130
| spl42_132
| spl42_134
| spl42_135
| spl42_138
| spl42_139 ),
inference(rat,[],[s87,s792,s783,s770,s771,s772,s773,s762]) ).
cnf(s795,plain,
( spl42_92
| spl42_108 ),
inference(rat,[],[s83,s762,s789]) ).
cnf(s796,plain,
( spl42_114
| spl42_118 ),
inference(rat,[],[s80,s766,s655]) ).
cnf(s798,plain,
( spl42_109
| spl42_113
| spl42_121 ),
inference(rat,[],[s78,s780]) ).
cnf(s800,plain,
( spl42_71
| spl42_87
| spl42_103 ),
inference(rat,[],[s73,s779]) ).
cnf(s801,plain,
( spl42_97
| spl42_105 ),
inference(rat,[],[s70,s784,s671]) ).
cnf(s802,plain,
( spl42_69
| spl42_85 ),
inference(rat,[],[s69,s780,s784]) ).
cnf(s803,plain,
( spl42_67
| spl42_83
| spl42_99 ),
inference(rat,[],[s65,s769]) ).
cnf(s805,plain,
( spl42_67
| spl42_71 ),
inference(rat,[],[s58,s791,s764]) ).
cnf(s806,plain,
( spl42_79
| spl42_111 ),
inference(rat,[],[s57,s670,s764]) ).
cnf(s807,plain,
( spl42_66
| spl42_70 ),
inference(rat,[],[s56,s790,s765]) ).
cnf(s808,plain,
( spl42_77
| spl42_109 ),
inference(rat,[],[s53,s671,s763]) ).
cnf(s820,plain,
spl42_3,
inference(rat,[],[s1,s669,s706,s699]) ).
cnf(s822,plain,
( ~ spl42_109
| ~ spl42_70
| spl42_65 ),
inference(rat,[],[s515,s795,s261,s447,s560,s93,s559,s67,s454,s563,s61,s91,s410,s568,s806,s430,s566,s570,s414,s573,s469,s805,s561,s641,s565,s796,s501,s562,s800,s416,s802,s412,s453,s741,s738,s748,s252,s755,s756,s776,s767,s747,s786,s758,s698,s742,s662,s820,s705,s778,s775,s661,s693,s663,s712,s722,s730,s729]) ).
cnf(s823,plain,
( spl42_109
| spl42_113 ),
inference(rat,[],[s806,s397,s395,s97,s808,s798]) ).
cnf(s824,plain,
( ~ spl42_70
| spl42_65 ),
inference(rat,[],[s823,s822,s641,s565,s796,s501,s663,s738,s742,s712]) ).
cnf(s825,plain,
spl42_65,
inference(rat,[],[s793,s111,s144,s496,s448,s61,s801,s443,s803,s92,s115,s402,s116,s128,s140,s459,s499,s802,s774,s133,s432,s504,s805,s123,s390,s503,s807,s824,s106]) ).
cnf(s826,plain,
~ spl42_66,
inference(rat,[],[s444,s825]) ).
cnf(s827,plain,
~ spl42_67,
inference(rat,[],[s392,s825]) ).
cnf(s829,plain,
spl42_70,
inference(rat,[],[s807,s826]) ).
cnf(s830,plain,
spl42_71,
inference(rat,[],[s805,s827]) ).
cnf(s837,plain,
$false,
inference(rat,[],[s453,s830,s829]) ).
fof(f4998,plain,
$false,
inference(avatar_sat_refutation,[],[s837]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG121+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.08/0.18 % Computer : n019.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 19:30:48 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 3.67/1.17 % (145716)Detected formulas, will run a generic FOF schedule.
% 3.67/1.17 % (145724)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=860591193:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.67/1.17 % (145724)Instruction limit reached!
% 3.67/1.17 % (145724)------------------------------
% 3.67/1.17 % (145724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.67/1.17 % (145724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.17 % (145724)CaDiCaL version: 2.1.3
% 3.67/1.17 % (145724)Termination reason: Instruction limit
% 3.67/1.17 % (145724)Termination phase: Saturation
% 3.67/1.17 % (145724)Time elapsed: 0.028 s
% 3.67/1.17 % (145724)Peak memory usage: 90 MB
% 3.67/1.17 % (145724)Instructions burned: 110 (million)
% 3.67/1.17 % (145726)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2118409368:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.67/1.17 % (145725)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1011283505:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.67/1.17 % (145723)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=2818481243:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.67/1.17 % (145722)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=111646260:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.67/1.17 % (145727)dis-21_1_sil=8000:lcm=predicate:random_seed=4293213609: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)
% 3.67/1.17 % (145721)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=1162486702:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.67/1.17 % (145727)Refutation not found, incomplete strategy
% 3.67/1.17 % (145727)------------------------------
% 3.67/1.17 % (145727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.67/1.17 % (145727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.17 % (145727)CaDiCaL version: 2.1.3
% 3.67/1.17 % (145727)Termination reason: Refutation not found, incomplete strategy
% 3.67/1.17 % (145727)Time elapsed: 0.018 s
% 3.67/1.17 % (145727)Peak memory usage: 89 MB
% 3.67/1.17 % (145727)Instructions burned: 34 (million)
% 3.67/1.17 % (145725)Instruction limit reached!
% 3.67/1.17 % (145725)------------------------------
% 3.67/1.17 % (145725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.67/1.17 % (145725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.17 % (145725)CaDiCaL version: 2.1.3
% 3.67/1.17 % (145725)Termination reason: Instruction limit
% 3.67/1.17 % (145725)Termination phase: Saturation
% 3.67/1.17 % (145725)Time elapsed: 0.052 s
% 3.67/1.17 % (145725)Peak memory usage: 88 MB
% 3.67/1.17 % (145725)Instructions burned: 120 (million)
% 3.67/1.17 % (145726)Instruction limit reached!
% 3.67/1.17 % (145726)------------------------------
% 3.67/1.17 % (145726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.67/1.17 % (145726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.17 % (145726)CaDiCaL version: 2.1.3
% 3.67/1.17 % (145726)Termination reason: Instruction limit
% 3.67/1.17 % (145726)Termination phase: Saturation
% 3.67/1.17 % (145726)Time elapsed: 0.076 s
% 3.67/1.17 % (145726)Peak memory usage: 89 MB
% 3.67/1.17 % (145726)Instructions burned: 141 (million)
% 3.67/1.17 % (145729)lrs+10_1_sil=8000:sp=occurrence:random_seed=3232157344:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.67/1.17 % (145729)First to succeed.
% 3.67/1.17 % (145729)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-145716"
% 3.67/1.17 % (145736)lrs+10_1_sil=32000:urr=on:br=off:random_seed=921642061:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.67/1.17 % (145737)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1648584035:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 3.67/1.17 % (145727)------------------------------
% 3.67/1.17 % (145727)------------------------------
% 3.67/1.17 % (145736)Instruction limit reached!
% 3.67/1.17 % (145736)------------------------------
% 3.67/1.17 % (145736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.67/1.17 % (145736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.17 % (145736)CaDiCaL version: 2.1.3
% 3.67/1.17 % (145736)Termination reason: Instruction limit
% 3.67/1.17 % (145736)Termination phase: Saturation
% 3.67/1.17 % (145736)Time elapsed: 0.080 s
% 3.67/1.17 % (145736)Peak memory usage: 90 MB
% 3.67/1.17 % (145736)Instructions burned: 157 (million)
% 3.67/1.17 % (145729)Refutation found. Thanks to Tanya!
% 3.67/1.17 % SZS status Theorem for theBenchmark
% 3.67/1.17 % SZS output start Proof for theBenchmark
% See solution above
% 4.13/1.36 % (145729)------------------------------
% 4.13/1.36 % (145729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.13/1.36 % (145729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/1.36 % (145729)CaDiCaL version: 2.1.3
% 4.13/1.36 % (145729)Termination reason: Refutation
% 4.13/1.36 % (145729)Time elapsed: 0.056 s
% 4.13/1.36 % (145729)Peak memory usage: 91 MB
% 4.13/1.36 % (145729)Instructions burned: 208 (million)
% 4.13/1.36 % (145729)------------------------------
% 4.13/1.36 % (145729)------------------------------
% 4.13/1.36 % (145716)Success in time 0.506 s
% 4.13/1.36 % Vampire exiting
%------------------------------------------------------------------------------