%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG113+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:22:47 AM UTC 2026
% Result : Theorem 0.62s 0.42s
% Output : Refutation 0.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 134
% Syntax : Number of formulae : 863 ( 179 unt; 118 def)
% Number of atoms : 3792 (2132 equ)
% Maximal formula atoms : 384 ( 4 avg)
% Number of connectives : 4602 (1673 ~;1999 |; 812 &)
% ( 118 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 122 ( 120 usr; 121 prp; 0-2 aty)
% Number of functors : 22 ( 22 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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f10,axiom,
( op1(e10,e10) = e10
& op1(e11,e11) = e11
& op1(e12,e12) = e12
& op1(e13,e13) = e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( op2(e20,e20) = e20
& op2(e21,e21) = e21
& op2(e22,e22) = e22
& op2(e23,e23) = e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e10 = op1(e12,e13)
& e11 = op1(op1(e12,e13),e13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e20 = op2(e22,e23)
& e21 = op2(op2(e22,e23),e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( h1(e12) = e20
& h1(e13) = e21
& h1(e10) = op2(e20,e21)
& h1(e11) = op2(op2(e20,e21),e21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
( h2(e12) = e20
& h2(e13) = e22
& h2(e10) = op2(e20,e22)
& h2(e11) = op2(op2(e20,e22),e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
( h3(e12) = e20
& h3(e13) = e23
& h3(e10) = op2(e20,e23)
& h3(e11) = op2(op2(e20,e23),e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f18,axiom,
( h5(e12) = e21
& h5(e13) = e22
& h5(e10) = op2(e21,e22)
& h5(e11) = op2(op2(e21,e22),e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
fof(f26,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 ) )
| ( h5(op1(e10,e10)) = op2(h5(e10),h5(e10))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& ( h5(e10) = e20
| h5(e11) = e20
| h5(e12) = e20
| h5(e13) = e20 )
& ( h5(e10) = e21
| h5(e11) = e21
| h5(e12) = e21
| h5(e13) = e21 )
& ( h5(e10) = e22
| h5(e11) = e22
| h5(e12) = e22
| h5(e13) = e22 )
& ( h5(e10) = e23
| h5(e11) = e23
| h5(e12) = e23
| h5(e13) = e23 ) )
| ( h6(op1(e10,e10)) = op2(h6(e10),h6(e10))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& ( h6(e10) = e20
| h6(e11) = e20
| h6(e12) = e20
| h6(e13) = e20 )
& ( h6(e10) = e21
| h6(e11) = e21
| h6(e12) = e21
| h6(e13) = e21 )
& ( h6(e10) = e22
| h6(e11) = e22
| h6(e12) = e22
| h6(e13) = e22 )
& ( h6(e10) = e23
| h6(e11) = e23
| h6(e12) = e23
| h6(e13) = e23 ) )
| ( h7(op1(e10,e10)) = op2(h7(e10),h7(e10))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& ( h7(e10) = e20
| h7(e11) = e20
| h7(e12) = e20
| h7(e13) = e20 )
& ( h7(e10) = e21
| h7(e11) = e21
| h7(e12) = e21
| h7(e13) = e21 )
& ( h7(e10) = e22
| h7(e11) = e22
| h7(e12) = e22
| h7(e13) = e22 )
& ( h7(e10) = e23
| h7(e11) = e23
| h7(e12) = e23
| h7(e13) = e23 ) )
| ( h8(op1(e10,e10)) = op2(h8(e10),h8(e10))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& ( h8(e10) = e20
| h8(e11) = e20
| h8(e12) = e20
| h8(e13) = e20 )
& ( h8(e10) = e21
| h8(e11) = e21
| h8(e12) = e21
| h8(e13) = e21 )
& ( h8(e10) = e22
| h8(e11) = e22
| h8(e12) = e22
| h8(e13) = e22 )
& ( h8(e10) = e23
| h8(e11) = e23
| h8(e12) = e23
| h8(e13) = e23 ) )
| ( h9(op1(e10,e10)) = op2(h9(e10),h9(e10))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& ( h9(e10) = e20
| h9(e11) = e20
| h9(e12) = e20
| h9(e13) = e20 )
& ( h9(e10) = e21
| h9(e11) = e21
| h9(e12) = e21
| h9(e13) = e21 )
& ( h9(e10) = e22
| h9(e11) = e22
| h9(e12) = e22
| h9(e13) = e22 )
& ( h9(e10) = e23
| h9(e11) = e23
| h9(e12) = e23
| h9(e13) = e23 ) )
| ( h10(op1(e10,e10)) = op2(h10(e10),h10(e10))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& ( h10(e10) = e20
| h10(e11) = e20
| h10(e12) = e20
| h10(e13) = e20 )
& ( h10(e10) = e21
| h10(e11) = e21
| h10(e12) = e21
| h10(e13) = e21 )
& ( h10(e10) = e22
| h10(e11) = e22
| h10(e12) = e22
| h10(e13) = e22 )
& ( h10(e10) = e23
| h10(e11) = e23
| h10(e12) = e23
| h10(e13) = e23 ) )
| ( h11(op1(e10,e10)) = op2(h11(e10),h11(e10))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& ( h11(e10) = e20
| h11(e11) = e20
| h11(e12) = e20
| h11(e13) = e20 )
& ( h11(e10) = e21
| h11(e11) = e21
| h11(e12) = e21
| h11(e13) = e21 )
& ( h11(e10) = e22
| h11(e11) = e22
| h11(e12) = e22
| h11(e13) = e22 )
& ( h11(e10) = e23
| h11(e11) = e23
| h11(e12) = e23
| h11(e13) = e23 ) )
| ( h12(op1(e10,e10)) = op2(h12(e10),h12(e10))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& ( h12(e10) = e20
| h12(e11) = e20
| h12(e12) = e20
| h12(e13) = e20 )
& ( h12(e10) = e21
| h12(e11) = e21
| h12(e12) = e21
| h12(e13) = e21 )
& ( h12(e10) = e22
| h12(e11) = e22
| h12(e12) = e22
| h12(e13) = e22 )
& ( h12(e10) = e23
| h12(e11) = e23
| h12(e12) = e23
| h12(e13) = e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f27,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 ) )
| ( h5(op1(e10,e10)) = op2(h5(e10),h5(e10))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& ( h5(e10) = e20
| h5(e11) = e20
| h5(e12) = e20
| h5(e13) = e20 )
& ( h5(e10) = e21
| h5(e11) = e21
| h5(e12) = e21
| h5(e13) = e21 )
& ( h5(e10) = e22
| h5(e11) = e22
| h5(e12) = e22
| h5(e13) = e22 )
& ( h5(e10) = e23
| h5(e11) = e23
| h5(e12) = e23
| h5(e13) = e23 ) )
| ( h6(op1(e10,e10)) = op2(h6(e10),h6(e10))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& ( h6(e10) = e20
| h6(e11) = e20
| h6(e12) = e20
| h6(e13) = e20 )
& ( h6(e10) = e21
| h6(e11) = e21
| h6(e12) = e21
| h6(e13) = e21 )
& ( h6(e10) = e22
| h6(e11) = e22
| h6(e12) = e22
| h6(e13) = e22 )
& ( h6(e10) = e23
| h6(e11) = e23
| h6(e12) = e23
| h6(e13) = e23 ) )
| ( h7(op1(e10,e10)) = op2(h7(e10),h7(e10))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& ( h7(e10) = e20
| h7(e11) = e20
| h7(e12) = e20
| h7(e13) = e20 )
& ( h7(e10) = e21
| h7(e11) = e21
| h7(e12) = e21
| h7(e13) = e21 )
& ( h7(e10) = e22
| h7(e11) = e22
| h7(e12) = e22
| h7(e13) = e22 )
& ( h7(e10) = e23
| h7(e11) = e23
| h7(e12) = e23
| h7(e13) = e23 ) )
| ( h8(op1(e10,e10)) = op2(h8(e10),h8(e10))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& ( h8(e10) = e20
| h8(e11) = e20
| h8(e12) = e20
| h8(e13) = e20 )
& ( h8(e10) = e21
| h8(e11) = e21
| h8(e12) = e21
| h8(e13) = e21 )
& ( h8(e10) = e22
| h8(e11) = e22
| h8(e12) = e22
| h8(e13) = e22 )
& ( h8(e10) = e23
| h8(e11) = e23
| h8(e12) = e23
| h8(e13) = e23 ) )
| ( h9(op1(e10,e10)) = op2(h9(e10),h9(e10))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& ( h9(e10) = e20
| h9(e11) = e20
| h9(e12) = e20
| h9(e13) = e20 )
& ( h9(e10) = e21
| h9(e11) = e21
| h9(e12) = e21
| h9(e13) = e21 )
& ( h9(e10) = e22
| h9(e11) = e22
| h9(e12) = e22
| h9(e13) = e22 )
& ( h9(e10) = e23
| h9(e11) = e23
| h9(e12) = e23
| h9(e13) = e23 ) )
| ( h10(op1(e10,e10)) = op2(h10(e10),h10(e10))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& ( h10(e10) = e20
| h10(e11) = e20
| h10(e12) = e20
| h10(e13) = e20 )
& ( h10(e10) = e21
| h10(e11) = e21
| h10(e12) = e21
| h10(e13) = e21 )
& ( h10(e10) = e22
| h10(e11) = e22
| h10(e12) = e22
| h10(e13) = e22 )
& ( h10(e10) = e23
| h10(e11) = e23
| h10(e12) = e23
| h10(e13) = e23 ) )
| ( h11(op1(e10,e10)) = op2(h11(e10),h11(e10))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& ( h11(e10) = e20
| h11(e11) = e20
| h11(e12) = e20
| h11(e13) = e20 )
& ( h11(e10) = e21
| h11(e11) = e21
| h11(e12) = e21
| h11(e13) = e21 )
& ( h11(e10) = e22
| h11(e11) = e22
| h11(e12) = e22
| h11(e13) = e22 )
& ( h11(e10) = e23
| h11(e11) = e23
| h11(e12) = e23
| h11(e13) = e23 ) )
| ( h12(op1(e10,e10)) = op2(h12(e10),h12(e10))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& ( h12(e10) = e20
| h12(e11) = e20
| h12(e12) = e20
| h12(e13) = e20 )
& ( h12(e10) = e21
| h12(e11) = e21
| h12(e12) = e21
| h12(e13) = e21 )
& ( h12(e10) = e22
| h12(e11) = e22
| h12(e12) = e22
| h12(e13) = e22 )
& ( h12(e10) = e23
| h12(e11) = e23
| h12(e12) = e23
| h12(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f28,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) ) )
& ( h5(op1(e10,e10)) != op2(h5(e10),h5(e10))
| h5(op1(e10,e11)) != op2(h5(e10),h5(e11))
| h5(op1(e10,e12)) != op2(h5(e10),h5(e12))
| h5(op1(e10,e13)) != op2(h5(e10),h5(e13))
| h5(op1(e11,e10)) != op2(h5(e11),h5(e10))
| h5(op1(e11,e11)) != op2(h5(e11),h5(e11))
| h5(op1(e11,e12)) != op2(h5(e11),h5(e12))
| h5(op1(e11,e13)) != op2(h5(e11),h5(e13))
| h5(op1(e12,e10)) != op2(h5(e12),h5(e10))
| h5(op1(e12,e11)) != op2(h5(e12),h5(e11))
| h5(op1(e12,e12)) != op2(h5(e12),h5(e12))
| h5(op1(e12,e13)) != op2(h5(e12),h5(e13))
| h5(op1(e13,e10)) != op2(h5(e13),h5(e10))
| h5(op1(e13,e11)) != op2(h5(e13),h5(e11))
| h5(op1(e13,e12)) != op2(h5(e13),h5(e12))
| h5(op1(e13,e13)) != op2(h5(e13),h5(e13))
| ( e20 != h5(e10)
& e20 != h5(e11)
& e20 != h5(e12)
& e20 != h5(e13) )
| ( e21 != h5(e10)
& e21 != h5(e11)
& e21 != h5(e12)
& e21 != h5(e13) )
| ( e22 != h5(e10)
& e22 != h5(e11)
& e22 != h5(e12)
& e22 != h5(e13) )
| ( e23 != h5(e10)
& e23 != h5(e11)
& e23 != h5(e12)
& e23 != h5(e13) ) )
& ( h6(op1(e10,e10)) != op2(h6(e10),h6(e10))
| h6(op1(e10,e11)) != op2(h6(e10),h6(e11))
| h6(op1(e10,e12)) != op2(h6(e10),h6(e12))
| h6(op1(e10,e13)) != op2(h6(e10),h6(e13))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| ( e20 != h6(e10)
& e20 != h6(e11)
& e20 != h6(e12)
& e20 != h6(e13) )
| ( e21 != h6(e10)
& e21 != h6(e11)
& e21 != h6(e12)
& e21 != h6(e13) )
| ( e22 != h6(e10)
& e22 != h6(e11)
& e22 != h6(e12)
& e22 != h6(e13) )
| ( e23 != h6(e10)
& e23 != h6(e11)
& e23 != h6(e12)
& e23 != h6(e13) ) )
& ( h7(op1(e10,e10)) != op2(h7(e10),h7(e10))
| h7(op1(e10,e11)) != op2(h7(e10),h7(e11))
| h7(op1(e10,e12)) != op2(h7(e10),h7(e12))
| h7(op1(e10,e13)) != op2(h7(e10),h7(e13))
| h7(op1(e11,e10)) != op2(h7(e11),h7(e10))
| h7(op1(e11,e11)) != op2(h7(e11),h7(e11))
| h7(op1(e11,e12)) != op2(h7(e11),h7(e12))
| h7(op1(e11,e13)) != op2(h7(e11),h7(e13))
| h7(op1(e12,e10)) != op2(h7(e12),h7(e10))
| h7(op1(e12,e11)) != op2(h7(e12),h7(e11))
| h7(op1(e12,e12)) != op2(h7(e12),h7(e12))
| h7(op1(e12,e13)) != op2(h7(e12),h7(e13))
| h7(op1(e13,e10)) != op2(h7(e13),h7(e10))
| h7(op1(e13,e11)) != op2(h7(e13),h7(e11))
| h7(op1(e13,e12)) != op2(h7(e13),h7(e12))
| h7(op1(e13,e13)) != op2(h7(e13),h7(e13))
| ( e20 != h7(e10)
& e20 != h7(e11)
& e20 != h7(e12)
& e20 != h7(e13) )
| ( e21 != h7(e10)
& e21 != h7(e11)
& e21 != h7(e12)
& e21 != h7(e13) )
| ( e22 != h7(e10)
& e22 != h7(e11)
& e22 != h7(e12)
& e22 != h7(e13) )
| ( e23 != h7(e10)
& e23 != h7(e11)
& e23 != h7(e12)
& e23 != h7(e13) ) )
& ( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h8(e11))
| h8(op1(e10,e12)) != op2(h8(e10),h8(e12))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e11,e10)) != op2(h8(e11),h8(e10))
| h8(op1(e11,e11)) != op2(h8(e11),h8(e11))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| ( e20 != h8(e10)
& e20 != h8(e11)
& e20 != h8(e12)
& e20 != h8(e13) )
| ( e21 != h8(e10)
& e21 != h8(e11)
& e21 != h8(e12)
& e21 != h8(e13) )
| ( e22 != h8(e10)
& e22 != h8(e11)
& e22 != h8(e12)
& e22 != h8(e13) )
| ( e23 != h8(e10)
& e23 != h8(e11)
& e23 != h8(e12)
& e23 != h8(e13) ) )
& ( h9(op1(e10,e10)) != op2(h9(e10),h9(e10))
| h9(op1(e10,e11)) != op2(h9(e10),h9(e11))
| h9(op1(e10,e12)) != op2(h9(e10),h9(e12))
| h9(op1(e10,e13)) != op2(h9(e10),h9(e13))
| h9(op1(e11,e10)) != op2(h9(e11),h9(e10))
| h9(op1(e11,e11)) != op2(h9(e11),h9(e11))
| h9(op1(e11,e12)) != op2(h9(e11),h9(e12))
| h9(op1(e11,e13)) != op2(h9(e11),h9(e13))
| h9(op1(e12,e10)) != op2(h9(e12),h9(e10))
| h9(op1(e12,e11)) != op2(h9(e12),h9(e11))
| h9(op1(e12,e12)) != op2(h9(e12),h9(e12))
| h9(op1(e12,e13)) != op2(h9(e12),h9(e13))
| h9(op1(e13,e10)) != op2(h9(e13),h9(e10))
| h9(op1(e13,e11)) != op2(h9(e13),h9(e11))
| h9(op1(e13,e12)) != op2(h9(e13),h9(e12))
| h9(op1(e13,e13)) != op2(h9(e13),h9(e13))
| ( e20 != h9(e10)
& e20 != h9(e11)
& e20 != h9(e12)
& e20 != h9(e13) )
| ( e21 != h9(e10)
& e21 != h9(e11)
& e21 != h9(e12)
& e21 != h9(e13) )
| ( e22 != h9(e10)
& e22 != h9(e11)
& e22 != h9(e12)
& e22 != h9(e13) )
| ( e23 != h9(e10)
& e23 != h9(e11)
& e23 != h9(e12)
& e23 != h9(e13) ) )
& ( h10(op1(e10,e10)) != op2(h10(e10),h10(e10))
| h10(op1(e10,e11)) != op2(h10(e10),h10(e11))
| h10(op1(e10,e12)) != op2(h10(e10),h10(e12))
| h10(op1(e10,e13)) != op2(h10(e10),h10(e13))
| h10(op1(e11,e10)) != op2(h10(e11),h10(e10))
| h10(op1(e11,e11)) != op2(h10(e11),h10(e11))
| h10(op1(e11,e12)) != op2(h10(e11),h10(e12))
| h10(op1(e11,e13)) != op2(h10(e11),h10(e13))
| h10(op1(e12,e10)) != op2(h10(e12),h10(e10))
| h10(op1(e12,e11)) != op2(h10(e12),h10(e11))
| h10(op1(e12,e12)) != op2(h10(e12),h10(e12))
| h10(op1(e12,e13)) != op2(h10(e12),h10(e13))
| h10(op1(e13,e10)) != op2(h10(e13),h10(e10))
| h10(op1(e13,e11)) != op2(h10(e13),h10(e11))
| h10(op1(e13,e12)) != op2(h10(e13),h10(e12))
| h10(op1(e13,e13)) != op2(h10(e13),h10(e13))
| ( e20 != h10(e10)
& e20 != h10(e11)
& e20 != h10(e12)
& e20 != h10(e13) )
| ( e21 != h10(e10)
& e21 != h10(e11)
& e21 != h10(e12)
& e21 != h10(e13) )
| ( e22 != h10(e10)
& e22 != h10(e11)
& e22 != h10(e12)
& e22 != h10(e13) )
| ( e23 != h10(e10)
& e23 != h10(e11)
& e23 != h10(e12)
& e23 != h10(e13) ) )
& ( h11(op1(e10,e10)) != op2(h11(e10),h11(e10))
| h11(op1(e10,e11)) != op2(h11(e10),h11(e11))
| h11(op1(e10,e12)) != op2(h11(e10),h11(e12))
| h11(op1(e10,e13)) != op2(h11(e10),h11(e13))
| h11(op1(e11,e10)) != op2(h11(e11),h11(e10))
| h11(op1(e11,e11)) != op2(h11(e11),h11(e11))
| h11(op1(e11,e12)) != op2(h11(e11),h11(e12))
| h11(op1(e11,e13)) != op2(h11(e11),h11(e13))
| h11(op1(e12,e10)) != op2(h11(e12),h11(e10))
| h11(op1(e12,e11)) != op2(h11(e12),h11(e11))
| h11(op1(e12,e12)) != op2(h11(e12),h11(e12))
| h11(op1(e12,e13)) != op2(h11(e12),h11(e13))
| h11(op1(e13,e10)) != op2(h11(e13),h11(e10))
| h11(op1(e13,e11)) != op2(h11(e13),h11(e11))
| h11(op1(e13,e12)) != op2(h11(e13),h11(e12))
| h11(op1(e13,e13)) != op2(h11(e13),h11(e13))
| ( e20 != h11(e10)
& e20 != h11(e11)
& e20 != h11(e12)
& e20 != h11(e13) )
| ( e21 != h11(e10)
& e21 != h11(e11)
& e21 != h11(e12)
& e21 != h11(e13) )
| ( e22 != h11(e10)
& e22 != h11(e11)
& e22 != h11(e12)
& e22 != h11(e13) )
| ( e23 != h11(e10)
& e23 != h11(e11)
& e23 != h11(e12)
& e23 != h11(e13) ) )
& ( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),h12(e11))
| h12(op1(e10,e12)) != op2(h12(e10),h12(e12))
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e11,e10)) != op2(h12(e11),h12(e10))
| h12(op1(e11,e11)) != op2(h12(e11),h12(e11))
| h12(op1(e11,e12)) != op2(h12(e11),h12(e12))
| h12(op1(e11,e13)) != op2(h12(e11),h12(e13))
| h12(op1(e12,e10)) != op2(h12(e12),h12(e10))
| h12(op1(e12,e11)) != op2(h12(e12),h12(e11))
| h12(op1(e12,e12)) != op2(h12(e12),h12(e12))
| h12(op1(e12,e13)) != op2(h12(e12),h12(e13))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e13,e11)) != op2(h12(e13),h12(e11))
| h12(op1(e13,e12)) != op2(h12(e13),h12(e12))
| h12(op1(e13,e13)) != op2(h12(e13),h12(e13))
| ( e20 != h12(e10)
& e20 != h12(e11)
& e20 != h12(e12)
& e20 != h12(e13) )
| ( e21 != h12(e10)
& e21 != h12(e11)
& e21 != h12(e12)
& e21 != h12(e13) )
| ( e22 != h12(e10)
& e22 != h12(e11)
& e22 != h12(e12)
& e22 != h12(e13) )
| ( e23 != h12(e10)
& e23 != h12(e11)
& e23 != h12(e12)
& e23 != h12(e13) ) ) ),
inference(ennf_transformation,[],[f27]) ).
fof(f48,plain,
( e11 = op1(e13,e10)
| e11 = op1(e12,e10)
| e11 = op1(e11,e10)
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[],[f2]) ).
fof(f49,plain,
( e12 = op1(e10,e13)
| e12 = op1(e10,e12)
| e12 = op1(e10,e11)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f2]) ).
fof(f50,plain,
( e12 = op1(e13,e10)
| e12 = op1(e12,e10)
| e12 = op1(e11,e10)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f2]) ).
fof(f51,plain,
( e13 = op1(e10,e13)
| e13 = op1(e10,e12)
| e13 = op1(e10,e11)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f2]) ).
fof(f53,plain,
( e10 = op1(e11,e13)
| e10 = op1(e11,e12)
| e10 = op1(e11,e11)
| e10 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f54,plain,
( e10 = op1(e13,e11)
| e10 = op1(e12,e11)
| e10 = op1(e11,e11)
| e10 = op1(e10,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f58,plain,
( e12 = op1(e13,e11)
| e12 = op1(e12,e11)
| e12 = op1(e11,e11)
| e12 = op1(e10,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f59,plain,
( e13 = op1(e11,e13)
| e13 = op1(e11,e12)
| e13 = op1(e11,e11)
| e13 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f63,plain,
( e11 = op1(e12,e13)
| e11 = op1(e12,e12)
| e11 = op1(e12,e11)
| e11 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f67,plain,
( e13 = op1(e12,e13)
| e13 = op1(e12,e12)
| e13 = op1(e12,e11)
| e13 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f71,plain,
( e11 = op1(e13,e13)
| e11 = op1(e13,e12)
| e11 = op1(e13,e11)
| e11 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f72,plain,
( e11 = op1(e13,e13)
| e11 = op1(e12,e13)
| e11 = op1(e11,e13)
| e11 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f74,plain,
( e12 = op1(e13,e13)
| e12 = op1(e12,e13)
| e12 = op1(e11,e13)
| e12 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f79,plain,
( e23 = op2(e20,e22)
| e22 = op2(e20,e22)
| e21 = op2(e20,e22)
| e20 = op2(e20,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f81,plain,
( e23 = op2(e21,e20)
| e22 = op2(e21,e20)
| e21 = op2(e21,e20)
| e20 = op2(e21,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f85,plain,
( e23 = op2(e22,e20)
| e22 = op2(e22,e20)
| e21 = op2(e22,e20)
| e20 = op2(e22,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f86,plain,
( e23 = op2(e22,e21)
| e22 = op2(e22,e21)
| e21 = op2(e22,e21)
| e20 = op2(e22,e21) ),
inference(cnf_transformation,[],[f3]) ).
fof(f97,plain,
( e22 = op2(e20,e23)
| e22 = op2(e20,e22)
| e22 = op2(e20,e21)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f4]) ).
fof(f98,plain,
( e22 = op2(e23,e20)
| e22 = op2(e22,e20)
| e22 = op2(e21,e20)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f4]) ).
fof(f101,plain,
( e20 = op2(e21,e23)
| e20 = op2(e21,e22)
| e20 = op2(e21,e21)
| e20 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f102,plain,
( e20 = op2(e23,e21)
| e20 = op2(e22,e21)
| e20 = op2(e21,e21)
| e20 = op2(e20,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f119,plain,
( e21 = op2(e23,e23)
| e21 = op2(e23,e22)
| e21 = op2(e23,e21)
| e21 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f122,plain,
( e22 = op2(e23,e23)
| e22 = op2(e22,e23)
| e22 = op2(e21,e23)
| e22 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f138,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f150,plain,
op1(e11,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f172,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f180,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f181,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f182,plain,
op2(e22,e20) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f183,plain,
op2(e22,e20) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f184,plain,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f188,plain,
op2(e21,e20) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f190,plain,
op2(e21,e20) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f191,plain,
op2(e20,e22) != op2(e20,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f195,plain,
op2(e20,e20) != op2(e20,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f196,plain,
op2(e20,e20) != op2(e20,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f207,plain,
op2(e20,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f210,plain,
op2(e21,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f211,plain,
op2(e21,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f220,plain,
op2(e20,e20) != op2(e21,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f221,plain,
e12 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f222,plain,
e11 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f223,plain,
e11 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f224,plain,
e10 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f225,plain,
e10 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f226,plain,
e10 != e11,
inference(cnf_transformation,[],[f7]) ).
fof(f227,plain,
e22 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f228,plain,
e21 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f229,plain,
e21 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f232,plain,
e20 != e21,
inference(cnf_transformation,[],[f8]) ).
fof(f249,plain,
e13 = op1(e13,e13),
inference(cnf_transformation,[],[f10]) ).
fof(f250,plain,
e12 = op1(e12,e12),
inference(cnf_transformation,[],[f10]) ).
fof(f251,plain,
e11 = op1(e11,e11),
inference(cnf_transformation,[],[f10]) ).
fof(f252,plain,
e10 = op1(e10,e10),
inference(cnf_transformation,[],[f10]) ).
fof(f253,plain,
e23 = op2(e23,e23),
inference(cnf_transformation,[],[f11]) ).
fof(f254,plain,
e22 = op2(e22,e22),
inference(cnf_transformation,[],[f11]) ).
fof(f255,plain,
e21 = op2(e21,e21),
inference(cnf_transformation,[],[f11]) ).
fof(f256,plain,
e20 = op2(e20,e20),
inference(cnf_transformation,[],[f11]) ).
fof(f258,plain,
e10 = op1(e12,e13),
inference(cnf_transformation,[],[f12]) ).
fof(f259,plain,
e21 = op2(op2(e22,e23),e23),
inference(cnf_transformation,[],[f13]) ).
fof(f260,plain,
e20 = op2(e22,e23),
inference(cnf_transformation,[],[f13]) ).
fof(f261,plain,
h1(e11) = op2(op2(e20,e21),e21),
inference(cnf_transformation,[],[f14]) ).
fof(f262,plain,
op2(e20,e21) = h1(e10),
inference(cnf_transformation,[],[f14]) ).
fof(f263,plain,
e21 = h1(e13),
inference(cnf_transformation,[],[f14]) ).
fof(f264,plain,
e20 = h1(e12),
inference(cnf_transformation,[],[f14]) ).
fof(f267,plain,
e22 = h2(e13),
inference(cnf_transformation,[],[f15]) ).
fof(f268,plain,
e20 = h2(e12),
inference(cnf_transformation,[],[f15]) ).
fof(f271,plain,
e23 = h3(e13),
inference(cnf_transformation,[],[f16]) ).
fof(f279,plain,
e22 = h5(e13),
inference(cnf_transformation,[],[f18]) ).
fof(f310,plain,
( e20 != h1(e12)
| ~ sP23 ),
inference(cnf_transformation,[],[f28]) ).
fof(f313,plain,
( e21 != h1(e13)
| ~ sP22 ),
inference(cnf_transformation,[],[f28]) ).
fof(f412,plain,
( e23 != h1(e11)
| e22 != h1(e10)
| sP22
| sP23
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e10)) != op2(h1(e10),h1(e10)) ),
inference(cnf_transformation,[],[f28]) ).
fof(f717,plain,
( e23 != h1(e11)
| e22 != h1(e10)
| sP22
| ~ sP23
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e10)) != op2(h1(e10),h1(e10)) ),
inference(consistent_polarity_flipping,[],[f412]) ).
fof(f763,plain,
( e20 != h1(e12)
| sP23 ),
inference(consistent_polarity_flipping,[],[f310]) ).
fof(f766,definition,
( spl24_1
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl24_1])],[avatar_definition]) ).
fof(f775,definition,
( spl24_3
<=> e20 = h1(e12) ),
introduced(definition,[new_symbols(definition,[spl24_3])],[avatar_definition]) ).
fof(f776,plain,
( e20 = h1(e12)
| ~ spl24_3 ),
inference(avatar_component_clause,[],[f775]) ).
fof(f778,plain,
( spl24_1
| ~ spl24_3 ),
inference(avatar_split_clause,[],[f763,f775,f766]) ).
fof(f790,definition,
( spl24_6
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl24_6])],[avatar_definition]) ).
fof(f794,definition,
( spl24_7
<=> e21 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl24_7])],[avatar_definition]) ).
fof(f795,plain,
( e21 = h1(e13)
| ~ spl24_7 ),
inference(avatar_component_clause,[],[f794]) ).
fof(f797,plain,
( ~ spl24_6
| ~ spl24_7 ),
inference(avatar_split_clause,[],[f313,f794,f790]) ).
fof(f823,definition,
( spl24_13
<=> e20 = h2(e12) ),
introduced(definition,[new_symbols(definition,[spl24_13])],[avatar_definition]) ).
fof(f824,plain,
( e20 = h2(e12)
| ~ spl24_13 ),
inference(avatar_component_clause,[],[f823]) ).
fof(f842,definition,
( spl24_17
<=> e21 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl24_17])],[avatar_definition]) ).
fof(f843,plain,
( e21 = h2(e13)
| ~ spl24_17 ),
inference(avatar_component_clause,[],[f842]) ).
fof(f844,plain,
( e21 != h2(e13)
| spl24_17 ),
inference(avatar_component_clause,[],[f842]) ).
fof(f847,definition,
( spl24_18
<=> e21 = h2(e12) ),
introduced(definition,[new_symbols(definition,[spl24_18])],[avatar_definition]) ).
fof(f848,plain,
( e21 = h2(e12)
| ~ spl24_18 ),
inference(avatar_component_clause,[],[f847]) ).
fof(f849,plain,
( e21 != h2(e12)
| spl24_18 ),
inference(avatar_component_clause,[],[f847]) ).
fof(f890,definition,
( spl24_27
<=> e21 = h3(e13) ),
introduced(definition,[new_symbols(definition,[spl24_27])],[avatar_definition]) ).
fof(f891,plain,
( e21 = h3(e13)
| ~ spl24_27 ),
inference(avatar_component_clause,[],[f890]) ).
fof(f892,plain,
( e21 != h3(e13)
| spl24_27 ),
inference(avatar_component_clause,[],[f890]) ).
fof(f962,definition,
( spl24_42
<=> e20 = h5(e13) ),
introduced(definition,[new_symbols(definition,[spl24_42])],[avatar_definition]) ).
fof(f963,plain,
( e20 = h5(e13)
| ~ spl24_42 ),
inference(avatar_component_clause,[],[f962]) ).
fof(f964,plain,
( e20 != h5(e13)
| spl24_42 ),
inference(avatar_component_clause,[],[f962]) ).
fof(f1342,definition,
( spl24_121
<=> h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl24_121])],[avatar_definition]) ).
fof(f1344,plain,
( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| spl24_121 ),
inference(avatar_component_clause,[],[f1342]) ).
fof(f1346,definition,
( spl24_122
<=> h1(op1(e10,e11)) = op2(h1(e10),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl24_122])],[avatar_definition]) ).
fof(f1348,plain,
( h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| spl24_122 ),
inference(avatar_component_clause,[],[f1346]) ).
fof(f1350,definition,
( spl24_123
<=> h1(op1(e10,e12)) = op2(h1(e10),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl24_123])],[avatar_definition]) ).
fof(f1352,plain,
( h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| spl24_123 ),
inference(avatar_component_clause,[],[f1350]) ).
fof(f1354,definition,
( spl24_124
<=> h1(op1(e10,e13)) = op2(h1(e10),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl24_124])],[avatar_definition]) ).
fof(f1356,plain,
( h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| spl24_124 ),
inference(avatar_component_clause,[],[f1354]) ).
fof(f1358,definition,
( spl24_125
<=> h1(op1(e11,e10)) = op2(h1(e11),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl24_125])],[avatar_definition]) ).
fof(f1360,plain,
( h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| spl24_125 ),
inference(avatar_component_clause,[],[f1358]) ).
fof(f1362,definition,
( spl24_126
<=> h1(op1(e11,e11)) = op2(h1(e11),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl24_126])],[avatar_definition]) ).
fof(f1364,plain,
( h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| spl24_126 ),
inference(avatar_component_clause,[],[f1362]) ).
fof(f1366,definition,
( spl24_127
<=> h1(op1(e11,e12)) = op2(h1(e11),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl24_127])],[avatar_definition]) ).
fof(f1368,plain,
( h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| spl24_127 ),
inference(avatar_component_clause,[],[f1366]) ).
fof(f1370,definition,
( spl24_128
<=> h1(op1(e11,e13)) = op2(h1(e11),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl24_128])],[avatar_definition]) ).
fof(f1372,plain,
( h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| spl24_128 ),
inference(avatar_component_clause,[],[f1370]) ).
fof(f1374,definition,
( spl24_129
<=> h1(op1(e12,e10)) = op2(h1(e12),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl24_129])],[avatar_definition]) ).
fof(f1376,plain,
( h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| spl24_129 ),
inference(avatar_component_clause,[],[f1374]) ).
fof(f1378,definition,
( spl24_130
<=> h1(op1(e12,e11)) = op2(h1(e12),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl24_130])],[avatar_definition]) ).
fof(f1380,plain,
( h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| spl24_130 ),
inference(avatar_component_clause,[],[f1378]) ).
fof(f1382,definition,
( spl24_131
<=> h1(op1(e12,e12)) = op2(h1(e12),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl24_131])],[avatar_definition]) ).
fof(f1384,plain,
( h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| spl24_131 ),
inference(avatar_component_clause,[],[f1382]) ).
fof(f1386,definition,
( spl24_132
<=> h1(op1(e12,e13)) = op2(h1(e12),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl24_132])],[avatar_definition]) ).
fof(f1388,plain,
( h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| spl24_132 ),
inference(avatar_component_clause,[],[f1386]) ).
fof(f1390,definition,
( spl24_133
<=> h1(op1(e13,e10)) = op2(h1(e13),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl24_133])],[avatar_definition]) ).
fof(f1392,plain,
( h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| spl24_133 ),
inference(avatar_component_clause,[],[f1390]) ).
fof(f1394,definition,
( spl24_134
<=> h1(op1(e13,e11)) = op2(h1(e13),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl24_134])],[avatar_definition]) ).
fof(f1396,plain,
( h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| spl24_134 ),
inference(avatar_component_clause,[],[f1394]) ).
fof(f1398,definition,
( spl24_135
<=> h1(op1(e13,e12)) = op2(h1(e13),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl24_135])],[avatar_definition]) ).
fof(f1400,plain,
( h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| spl24_135 ),
inference(avatar_component_clause,[],[f1398]) ).
fof(f1402,definition,
( spl24_136
<=> h1(op1(e13,e13)) = op2(h1(e13),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl24_136])],[avatar_definition]) ).
fof(f1404,plain,
( h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| spl24_136 ),
inference(avatar_component_clause,[],[f1402]) ).
fof(f1425,definition,
( spl24_141
<=> e22 = h1(e10) ),
introduced(definition,[new_symbols(definition,[spl24_141])],[avatar_definition]) ).
fof(f1426,plain,
( e22 = h1(e10)
| ~ spl24_141 ),
inference(avatar_component_clause,[],[f1425]) ).
fof(f1430,definition,
( spl24_142
<=> e23 = h1(e11) ),
introduced(definition,[new_symbols(definition,[spl24_142])],[avatar_definition]) ).
fof(f1431,plain,
( e23 = h1(e11)
| ~ spl24_142 ),
inference(avatar_component_clause,[],[f1430]) ).
fof(f1436,plain,
( ~ spl24_121
| ~ spl24_122
| ~ spl24_123
| ~ spl24_124
| ~ spl24_125
| ~ spl24_126
| ~ spl24_127
| ~ spl24_128
| ~ spl24_129
| ~ spl24_130
| ~ spl24_131
| ~ spl24_132
| ~ spl24_133
| ~ spl24_134
| ~ spl24_135
| ~ spl24_136
| ~ spl24_1
| spl24_6
| ~ spl24_141
| ~ spl24_142 ),
inference(avatar_split_clause,[],[f717,f1430,f1425,f790,f766,f1402,f1398,f1394,f1390,f1386,f1382,f1378,f1374,f1370,f1366,f1362,f1358,f1354,f1350,f1346,f1342]) ).
fof(f1518,definition,
( spl24_161
<=> e22 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl24_161])],[avatar_definition]) ).
fof(f1519,plain,
( e22 = h2(e13)
| ~ spl24_161 ),
inference(avatar_component_clause,[],[f1518]) ).
fof(f1670,definition,
( spl24_192
<=> e23 = h3(e13) ),
introduced(definition,[new_symbols(definition,[spl24_192])],[avatar_definition]) ).
fof(f1671,plain,
( e23 = h3(e13)
| ~ spl24_192 ),
inference(avatar_component_clause,[],[f1670]) ).
fof(f1854,definition,
( spl24_233
<=> e22 = h5(e13) ),
introduced(definition,[new_symbols(definition,[spl24_233])],[avatar_definition]) ).
fof(f1855,plain,
( e22 = h5(e13)
| ~ spl24_233 ),
inference(avatar_component_clause,[],[f1854]) ).
fof(f2699,plain,
spl24_233,
inference(avatar_split_clause,[],[f279,f1854]) ).
fof(f2703,plain,
spl24_192,
inference(avatar_split_clause,[],[f271,f1670]) ).
fof(f2705,plain,
spl24_161,
inference(avatar_split_clause,[],[f267,f1518]) ).
fof(f2706,plain,
spl24_13,
inference(avatar_split_clause,[],[f268,f823]) ).
fof(f2707,plain,
spl24_7,
inference(avatar_split_clause,[],[f263,f794]) ).
fof(f2708,plain,
spl24_3,
inference(avatar_split_clause,[],[f264,f775]) ).
fof(f2710,definition,
( spl24_409
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl24_409])],[avatar_definition]) ).
fof(f2712,plain,
( e20 = op2(e20,e20)
| ~ spl24_409 ),
inference(avatar_component_clause,[],[f2710]) ).
fof(f2714,definition,
( spl24_410
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl24_410])],[avatar_definition]) ).
fof(f2718,definition,
( spl24_411
<=> e20 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl24_411])],[avatar_definition]) ).
fof(f2727,definition,
( spl24_413
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl24_413])],[avatar_definition]) ).
fof(f2731,definition,
( spl24_414
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl24_414])],[avatar_definition]) ).
fof(f2748,definition,
( spl24_418
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl24_418])],[avatar_definition]) ).
fof(f2752,definition,
( spl24_419
<=> e21 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl24_419])],[avatar_definition]) ).
fof(f2754,plain,
( e21 = op2(e20,e23)
| ~ spl24_419 ),
inference(avatar_component_clause,[],[f2752]) ).
fof(f2757,definition,
( spl24_420
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl24_420])],[avatar_definition]) ).
fof(f2761,definition,
( spl24_421
<=> e21 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl24_421])],[avatar_definition]) ).
fof(f2765,definition,
( spl24_422
<=> e21 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl24_422])],[avatar_definition]) ).
fof(f2767,plain,
( e21 = op2(e23,e20)
| ~ spl24_422 ),
inference(avatar_component_clause,[],[f2765]) ).
fof(f2770,definition,
( spl24_423
<=> op2(e20,e20) = e22 ),
introduced(definition,[new_symbols(definition,[spl24_423])],[avatar_definition]) ).
fof(f2772,plain,
( op2(e20,e20) = e22
| ~ spl24_423 ),
inference(avatar_component_clause,[],[f2770]) ).
fof(f2774,definition,
( spl24_424
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl24_424])],[avatar_definition]) ).
fof(f2776,plain,
( e22 = op2(e20,e21)
| ~ spl24_424 ),
inference(avatar_component_clause,[],[f2774]) ).
fof(f2778,definition,
( spl24_425
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl24_425])],[avatar_definition]) ).
fof(f2782,definition,
( spl24_426
<=> e22 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl24_426])],[avatar_definition]) ).
fof(f2784,plain,
( e22 = op2(e20,e23)
| ~ spl24_426 ),
inference(avatar_component_clause,[],[f2782]) ).
fof(f2785,plain,
( spl24_423
| spl24_424
| spl24_425
| spl24_426 ),
inference(avatar_split_clause,[],[f97,f2782,f2778,f2774,f2770]) ).
fof(f2787,definition,
( spl24_427
<=> e22 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl24_427])],[avatar_definition]) ).
fof(f2791,definition,
( spl24_428
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl24_428])],[avatar_definition]) ).
fof(f2795,definition,
( spl24_429
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl24_429])],[avatar_definition]) ).
fof(f2797,plain,
( e22 = op2(e23,e20)
| ~ spl24_429 ),
inference(avatar_component_clause,[],[f2795]) ).
fof(f2798,plain,
( spl24_423
| spl24_427
| spl24_428
| spl24_429 ),
inference(avatar_split_clause,[],[f98,f2795,f2791,f2787,f2770]) ).
fof(f2808,definition,
( spl24_432
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl24_432])],[avatar_definition]) ).
fof(f2810,plain,
( e23 = op2(e20,e22)
| ~ spl24_432 ),
inference(avatar_component_clause,[],[f2808]) ).
fof(f2817,definition,
( spl24_434
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl24_434])],[avatar_definition]) ).
fof(f2821,definition,
( spl24_435
<=> e23 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl24_435])],[avatar_definition]) ).
fof(f2830,definition,
( spl24_437
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl24_437])],[avatar_definition]) ).
fof(f2832,plain,
( e20 = op2(e21,e21)
| ~ spl24_437 ),
inference(avatar_component_clause,[],[f2830]) ).
fof(f2834,definition,
( spl24_438
<=> e20 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl24_438])],[avatar_definition]) ).
fof(f2836,plain,
( e20 = op2(e21,e22)
| ~ spl24_438 ),
inference(avatar_component_clause,[],[f2834]) ).
fof(f2838,definition,
( spl24_439
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl24_439])],[avatar_definition]) ).
fof(f2840,plain,
( e20 = op2(e21,e23)
| ~ spl24_439 ),
inference(avatar_component_clause,[],[f2838]) ).
fof(f2841,plain,
( spl24_413
| spl24_437
| spl24_438
| spl24_439 ),
inference(avatar_split_clause,[],[f101,f2838,f2834,f2830,f2727]) ).
fof(f2843,definition,
( spl24_440
<=> e20 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl24_440])],[avatar_definition]) ).
fof(f2847,definition,
( spl24_441
<=> e20 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl24_441])],[avatar_definition]) ).
fof(f2850,plain,
( spl24_410
| spl24_437
| spl24_440
| spl24_441 ),
inference(avatar_split_clause,[],[f102,f2847,f2843,f2830,f2714]) ).
fof(f2852,definition,
( spl24_442
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl24_442])],[avatar_definition]) ).
fof(f2854,plain,
( e21 = op2(e21,e21)
| ~ spl24_442 ),
inference(avatar_component_clause,[],[f2852]) ).
fof(f2865,definition,
( spl24_445
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl24_445])],[avatar_definition]) ).
fof(f2869,definition,
( spl24_446
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl24_446])],[avatar_definition]) ).
fof(f2882,definition,
( spl24_449
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl24_449])],[avatar_definition]) ).
fof(f2884,plain,
( e22 = op2(e21,e23)
| ~ spl24_449 ),
inference(avatar_component_clause,[],[f2882]) ).
fof(f2887,definition,
( spl24_450
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl24_450])],[avatar_definition]) ).
fof(f2909,definition,
( spl24_455
<=> e23 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl24_455])],[avatar_definition]) ).
fof(f2911,plain,
( e23 = op2(e22,e21)
| ~ spl24_455 ),
inference(avatar_component_clause,[],[f2909]) ).
fof(f2922,definition,
( spl24_458
<=> e20 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl24_458])],[avatar_definition]) ).
fof(f2924,plain,
( e20 = op2(e22,e23)
| ~ spl24_458 ),
inference(avatar_component_clause,[],[f2922]) ).
fof(f2936,definition,
( spl24_461
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl24_461])],[avatar_definition]) ).
fof(f2938,plain,
( e21 = op2(e22,e23)
| ~ spl24_461 ),
inference(avatar_component_clause,[],[f2936]) ).
fof(f2941,definition,
( spl24_462
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl24_462])],[avatar_definition]) ).
fof(f2943,plain,
( e21 = op2(e23,e22)
| ~ spl24_462 ),
inference(avatar_component_clause,[],[f2941]) ).
fof(f2946,definition,
( spl24_463
<=> e22 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl24_463])],[avatar_definition]) ).
fof(f2948,plain,
( e22 = op2(e22,e22)
| ~ spl24_463 ),
inference(avatar_component_clause,[],[f2946]) ).
fof(f2950,definition,
( spl24_464
<=> e22 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl24_464])],[avatar_definition]) ).
fof(f2952,plain,
( e22 = op2(e22,e23)
| ~ spl24_464 ),
inference(avatar_component_clause,[],[f2950]) ).
fof(f2980,definition,
( spl24_470
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl24_470])],[avatar_definition]) ).
fof(f2982,plain,
( e21 = op2(e23,e23)
| ~ spl24_470 ),
inference(avatar_component_clause,[],[f2980]) ).
fof(f2983,plain,
( spl24_422
| spl24_446
| spl24_462
| spl24_470 ),
inference(avatar_split_clause,[],[f119,f2980,f2941,f2869,f2765]) ).
fof(f2986,definition,
( spl24_471
<=> e22 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl24_471])],[avatar_definition]) ).
fof(f2988,plain,
( e22 = op2(e23,e23)
| ~ spl24_471 ),
inference(avatar_component_clause,[],[f2986]) ).
fof(f2990,plain,
( spl24_426
| spl24_449
| spl24_464
| spl24_471 ),
inference(avatar_split_clause,[],[f122,f2986,f2950,f2882,f2782]) ).
fof(f2992,definition,
( spl24_472
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl24_472])],[avatar_definition]) ).
fof(f2994,plain,
( e23 = op2(e23,e23)
| ~ spl24_472 ),
inference(avatar_component_clause,[],[f2992]) ).
fof(f2999,plain,
( spl24_411
| spl24_418
| spl24_425
| spl24_432 ),
inference(avatar_split_clause,[],[f79,f2808,f2778,f2748,f2718]) ).
fof(f3001,plain,
( spl24_413
| spl24_420
| spl24_427
| spl24_434 ),
inference(avatar_split_clause,[],[f81,f2817,f2787,f2757,f2727]) ).
fof(f3005,plain,
( spl24_414
| spl24_421
| spl24_428
| spl24_435 ),
inference(avatar_split_clause,[],[f85,f2821,f2791,f2761,f2731]) ).
fof(f3006,plain,
( spl24_440
| spl24_445
| spl24_450
| spl24_455 ),
inference(avatar_split_clause,[],[f86,f2909,f2887,f2865,f2843]) ).
fof(f3014,definition,
( spl24_473
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl24_473])],[avatar_definition]) ).
fof(f3016,plain,
( e10 = op1(e10,e10)
| ~ spl24_473 ),
inference(avatar_component_clause,[],[f3014]) ).
fof(f3018,definition,
( spl24_474
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl24_474])],[avatar_definition]) ).
fof(f3020,plain,
( e10 = op1(e10,e11)
| ~ spl24_474 ),
inference(avatar_component_clause,[],[f3018]) ).
fof(f3031,definition,
( spl24_477
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl24_477])],[avatar_definition]) ).
fof(f3044,definition,
( spl24_480
<=> op1(e10,e10) = e11 ),
introduced(definition,[new_symbols(definition,[spl24_480])],[avatar_definition]) ).
fof(f3046,plain,
( op1(e10,e10) = e11
| ~ spl24_480 ),
inference(avatar_component_clause,[],[f3044]) ).
fof(f3056,definition,
( spl24_483
<=> e11 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl24_483])],[avatar_definition]) ).
fof(f3058,plain,
( e11 = op1(e10,e13)
| ~ spl24_483 ),
inference(avatar_component_clause,[],[f3056]) ).
fof(f3061,definition,
( spl24_484
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl24_484])],[avatar_definition]) ).
fof(f3063,plain,
( e11 = op1(e11,e10)
| ~ spl24_484 ),
inference(avatar_component_clause,[],[f3061]) ).
fof(f3065,definition,
( spl24_485
<=> e11 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl24_485])],[avatar_definition]) ).
fof(f3067,plain,
( e11 = op1(e12,e10)
| ~ spl24_485 ),
inference(avatar_component_clause,[],[f3065]) ).
fof(f3069,definition,
( spl24_486
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl24_486])],[avatar_definition]) ).
fof(f3071,plain,
( e11 = op1(e13,e10)
| ~ spl24_486 ),
inference(avatar_component_clause,[],[f3069]) ).
fof(f3072,plain,
( spl24_480
| spl24_484
| spl24_485
| spl24_486 ),
inference(avatar_split_clause,[],[f48,f3069,f3065,f3061,f3044]) ).
fof(f3074,definition,
( spl24_487
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[spl24_487])],[avatar_definition]) ).
fof(f3076,plain,
( op1(e10,e10) = e12
| ~ spl24_487 ),
inference(avatar_component_clause,[],[f3074]) ).
fof(f3078,definition,
( spl24_488
<=> e12 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl24_488])],[avatar_definition]) ).
fof(f3080,plain,
( e12 = op1(e10,e11)
| ~ spl24_488 ),
inference(avatar_component_clause,[],[f3078]) ).
fof(f3082,definition,
( spl24_489
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl24_489])],[avatar_definition]) ).
fof(f3084,plain,
( e12 = op1(e10,e12)
| ~ spl24_489 ),
inference(avatar_component_clause,[],[f3082]) ).
fof(f3086,definition,
( spl24_490
<=> e12 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl24_490])],[avatar_definition]) ).
fof(f3088,plain,
( e12 = op1(e10,e13)
| ~ spl24_490 ),
inference(avatar_component_clause,[],[f3086]) ).
fof(f3089,plain,
( spl24_487
| spl24_488
| spl24_489
| spl24_490 ),
inference(avatar_split_clause,[],[f49,f3086,f3082,f3078,f3074]) ).
fof(f3091,definition,
( spl24_491
<=> e12 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl24_491])],[avatar_definition]) ).
fof(f3093,plain,
( e12 = op1(e11,e10)
| ~ spl24_491 ),
inference(avatar_component_clause,[],[f3091]) ).
fof(f3095,definition,
( spl24_492
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl24_492])],[avatar_definition]) ).
fof(f3097,plain,
( e12 = op1(e12,e10)
| ~ spl24_492 ),
inference(avatar_component_clause,[],[f3095]) ).
fof(f3099,definition,
( spl24_493
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl24_493])],[avatar_definition]) ).
fof(f3101,plain,
( e12 = op1(e13,e10)
| ~ spl24_493 ),
inference(avatar_component_clause,[],[f3099]) ).
fof(f3102,plain,
( spl24_487
| spl24_491
| spl24_492
| spl24_493 ),
inference(avatar_split_clause,[],[f50,f3099,f3095,f3091,f3074]) ).
fof(f3104,definition,
( spl24_494
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl24_494])],[avatar_definition]) ).
fof(f3106,plain,
( op1(e10,e10) = e13
| ~ spl24_494 ),
inference(avatar_component_clause,[],[f3104]) ).
fof(f3108,definition,
( spl24_495
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl24_495])],[avatar_definition]) ).
fof(f3110,plain,
( e13 = op1(e10,e11)
| ~ spl24_495 ),
inference(avatar_component_clause,[],[f3108]) ).
fof(f3112,definition,
( spl24_496
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl24_496])],[avatar_definition]) ).
fof(f3114,plain,
( e13 = op1(e10,e12)
| ~ spl24_496 ),
inference(avatar_component_clause,[],[f3112]) ).
fof(f3116,definition,
( spl24_497
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl24_497])],[avatar_definition]) ).
fof(f3118,plain,
( e13 = op1(e10,e13)
| ~ spl24_497 ),
inference(avatar_component_clause,[],[f3116]) ).
fof(f3119,plain,
( spl24_494
| spl24_495
| spl24_496
| spl24_497 ),
inference(avatar_split_clause,[],[f51,f3116,f3112,f3108,f3104]) ).
fof(f3121,definition,
( spl24_498
<=> e13 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl24_498])],[avatar_definition]) ).
fof(f3123,plain,
( e13 = op1(e11,e10)
| ~ spl24_498 ),
inference(avatar_component_clause,[],[f3121]) ).
fof(f3125,definition,
( spl24_499
<=> e13 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl24_499])],[avatar_definition]) ).
fof(f3127,plain,
( e13 = op1(e12,e10)
| ~ spl24_499 ),
inference(avatar_component_clause,[],[f3125]) ).
fof(f3134,definition,
( spl24_501
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl24_501])],[avatar_definition]) ).
fof(f3136,plain,
( e10 = op1(e11,e11)
| ~ spl24_501 ),
inference(avatar_component_clause,[],[f3134]) ).
fof(f3138,definition,
( spl24_502
<=> e10 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl24_502])],[avatar_definition]) ).
fof(f3140,plain,
( e10 = op1(e11,e12)
| ~ spl24_502 ),
inference(avatar_component_clause,[],[f3138]) ).
fof(f3142,definition,
( spl24_503
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl24_503])],[avatar_definition]) ).
fof(f3144,plain,
( e10 = op1(e11,e13)
| ~ spl24_503 ),
inference(avatar_component_clause,[],[f3142]) ).
fof(f3145,plain,
( spl24_477
| spl24_501
| spl24_502
| spl24_503 ),
inference(avatar_split_clause,[],[f53,f3142,f3138,f3134,f3031]) ).
fof(f3147,definition,
( spl24_504
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl24_504])],[avatar_definition]) ).
fof(f3149,plain,
( e10 = op1(e12,e11)
| ~ spl24_504 ),
inference(avatar_component_clause,[],[f3147]) ).
fof(f3151,definition,
( spl24_505
<=> e10 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl24_505])],[avatar_definition]) ).
fof(f3153,plain,
( e10 = op1(e13,e11)
| ~ spl24_505 ),
inference(avatar_component_clause,[],[f3151]) ).
fof(f3154,plain,
( spl24_474
| spl24_501
| spl24_504
| spl24_505 ),
inference(avatar_split_clause,[],[f54,f3151,f3147,f3134,f3018]) ).
fof(f3156,definition,
( spl24_506
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl24_506])],[avatar_definition]) ).
fof(f3158,plain,
( e11 = op1(e11,e11)
| ~ spl24_506 ),
inference(avatar_component_clause,[],[f3156]) ).
fof(f3164,definition,
( spl24_508
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl24_508])],[avatar_definition]) ).
fof(f3169,definition,
( spl24_509
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl24_509])],[avatar_definition]) ).
fof(f3171,plain,
( e11 = op1(e12,e11)
| ~ spl24_509 ),
inference(avatar_component_clause,[],[f3169]) ).
fof(f3173,definition,
( spl24_510
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl24_510])],[avatar_definition]) ).
fof(f3175,plain,
( e11 = op1(e13,e11)
| ~ spl24_510 ),
inference(avatar_component_clause,[],[f3173]) ).
fof(f3178,definition,
( spl24_511
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl24_511])],[avatar_definition]) ).
fof(f3180,plain,
( e12 = op1(e11,e11)
| ~ spl24_511 ),
inference(avatar_component_clause,[],[f3178]) ).
fof(f3186,definition,
( spl24_513
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl24_513])],[avatar_definition]) ).
fof(f3188,plain,
( e12 = op1(e11,e13)
| ~ spl24_513 ),
inference(avatar_component_clause,[],[f3186]) ).
fof(f3191,definition,
( spl24_514
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl24_514])],[avatar_definition]) ).
fof(f3193,plain,
( e12 = op1(e12,e11)
| ~ spl24_514 ),
inference(avatar_component_clause,[],[f3191]) ).
fof(f3195,definition,
( spl24_515
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl24_515])],[avatar_definition]) ).
fof(f3197,plain,
( e12 = op1(e13,e11)
| ~ spl24_515 ),
inference(avatar_component_clause,[],[f3195]) ).
fof(f3198,plain,
( spl24_488
| spl24_511
| spl24_514
| spl24_515 ),
inference(avatar_split_clause,[],[f58,f3195,f3191,f3178,f3078]) ).
fof(f3200,definition,
( spl24_516
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl24_516])],[avatar_definition]) ).
fof(f3202,plain,
( e13 = op1(e11,e11)
| ~ spl24_516 ),
inference(avatar_component_clause,[],[f3200]) ).
fof(f3204,definition,
( spl24_517
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl24_517])],[avatar_definition]) ).
fof(f3206,plain,
( e13 = op1(e11,e12)
| ~ spl24_517 ),
inference(avatar_component_clause,[],[f3204]) ).
fof(f3208,definition,
( spl24_518
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl24_518])],[avatar_definition]) ).
fof(f3211,plain,
( spl24_498
| spl24_516
| spl24_517
| spl24_518 ),
inference(avatar_split_clause,[],[f59,f3208,f3204,f3200,f3121]) ).
fof(f3213,definition,
( spl24_519
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl24_519])],[avatar_definition]) ).
fof(f3215,plain,
( e13 = op1(e12,e11)
| ~ spl24_519 ),
inference(avatar_component_clause,[],[f3213]) ).
fof(f3226,definition,
( spl24_522
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl24_522])],[avatar_definition]) ).
fof(f3228,plain,
( e10 = op1(e12,e13)
| ~ spl24_522 ),
inference(avatar_component_clause,[],[f3226]) ).
fof(f3236,definition,
( spl24_524
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl24_524])],[avatar_definition]) ).
fof(f3238,plain,
( e11 = op1(e12,e12)
| ~ spl24_524 ),
inference(avatar_component_clause,[],[f3236]) ).
fof(f3240,definition,
( spl24_525
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl24_525])],[avatar_definition]) ).
fof(f3242,plain,
( e11 = op1(e12,e13)
| ~ spl24_525 ),
inference(avatar_component_clause,[],[f3240]) ).
fof(f3243,plain,
( spl24_485
| spl24_509
| spl24_524
| spl24_525 ),
inference(avatar_split_clause,[],[f63,f3240,f3236,f3169,f3065]) ).
fof(f3245,definition,
( spl24_526
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl24_526])],[avatar_definition]) ).
fof(f3247,plain,
( e11 = op1(e13,e12)
| ~ spl24_526 ),
inference(avatar_component_clause,[],[f3245]) ).
fof(f3250,definition,
( spl24_527
<=> e12 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl24_527])],[avatar_definition]) ).
fof(f3252,plain,
( e12 = op1(e12,e12)
| ~ spl24_527 ),
inference(avatar_component_clause,[],[f3250]) ).
fof(f3254,definition,
( spl24_528
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl24_528])],[avatar_definition]) ).
fof(f3256,plain,
( e12 = op1(e12,e13)
| ~ spl24_528 ),
inference(avatar_component_clause,[],[f3254]) ).
fof(f3264,definition,
( spl24_530
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl24_530])],[avatar_definition]) ).
fof(f3266,plain,
( e13 = op1(e12,e12)
| ~ spl24_530 ),
inference(avatar_component_clause,[],[f3264]) ).
fof(f3268,definition,
( spl24_531
<=> e13 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl24_531])],[avatar_definition]) ).
fof(f3270,plain,
( e13 = op1(e12,e13)
| ~ spl24_531 ),
inference(avatar_component_clause,[],[f3268]) ).
fof(f3271,plain,
( spl24_499
| spl24_519
| spl24_530
| spl24_531 ),
inference(avatar_split_clause,[],[f67,f3268,f3264,f3213,f3125]) ).
fof(f3284,definition,
( spl24_534
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl24_534])],[avatar_definition]) ).
fof(f3286,plain,
( e11 = op1(e13,e13)
| ~ spl24_534 ),
inference(avatar_component_clause,[],[f3284]) ).
fof(f3287,plain,
( spl24_486
| spl24_510
| spl24_526
| spl24_534 ),
inference(avatar_split_clause,[],[f71,f3284,f3245,f3173,f3069]) ).
fof(f3288,plain,
( spl24_483
| spl24_508
| spl24_525
| spl24_534 ),
inference(avatar_split_clause,[],[f72,f3284,f3240,f3164,f3056]) ).
fof(f3290,definition,
( spl24_535
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl24_535])],[avatar_definition]) ).
fof(f3292,plain,
( e12 = op1(e13,e13)
| ~ spl24_535 ),
inference(avatar_component_clause,[],[f3290]) ).
fof(f3294,plain,
( spl24_490
| spl24_513
| spl24_528
| spl24_535 ),
inference(avatar_split_clause,[],[f74,f3290,f3254,f3186,f3086]) ).
fof(f3296,definition,
( spl24_536
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl24_536])],[avatar_definition]) ).
fof(f3298,plain,
( e13 = op1(e13,e13)
| ~ spl24_536 ),
inference(avatar_component_clause,[],[f3296]) ).
fof(f3317,plain,
( e20 != e21
| ~ spl24_13
| spl24_18 ),
inference(forward_demodulation,[],[f849,f824]) ).
fof(f3324,plain,
( e20 != e22
| spl24_42
| ~ spl24_233 ),
inference(superposition,[],[f964,f1855]) ).
fof(f3333,plain,
( h1(op1(e10,e13)) != op2(h1(e10),e21)
| ~ spl24_7
| spl24_124 ),
inference(forward_demodulation,[],[f1356,f795]) ).
fof(f3335,plain,
spl24_536,
inference(avatar_split_clause,[],[f249,f3296]) ).
fof(f3336,plain,
spl24_527,
inference(avatar_split_clause,[],[f250,f3250]) ).
fof(f3337,plain,
spl24_506,
inference(avatar_split_clause,[],[f251,f3156]) ).
fof(f3338,plain,
spl24_473,
inference(avatar_split_clause,[],[f252,f3014]) ).
fof(f3339,plain,
spl24_472,
inference(avatar_split_clause,[],[f253,f2992]) ).
fof(f3340,plain,
spl24_463,
inference(avatar_split_clause,[],[f254,f2946]) ).
fof(f3341,plain,
spl24_442,
inference(avatar_split_clause,[],[f255,f2852]) ).
fof(f3342,plain,
spl24_409,
inference(avatar_split_clause,[],[f256,f2710]) ).
fof(f3343,plain,
spl24_522,
inference(avatar_split_clause,[],[f258,f3226]) ).
fof(f3344,plain,
spl24_458,
inference(avatar_split_clause,[],[f260,f2922]) ).
fof(f3351,plain,
( e21 = e22
| ~ spl24_17
| ~ spl24_161 ),
inference(forward_demodulation,[],[f843,f1519]) ).
fof(f3370,plain,
( $false
| ~ spl24_17
| ~ spl24_161 ),
inference(forward_subsumption_resolution,[],[f229,f3351]) ).
fof(f3371,plain,
( ~ spl24_17
| ~ spl24_161 ),
inference(avatar_contradiction_clause,[],[f3370]) ).
fof(f3372,plain,
( e21 != e22
| spl24_17
| ~ spl24_161 ),
inference(forward_demodulation,[],[f844,f1519]) ).
fof(f3407,plain,
( e21 = e22
| ~ spl24_419
| ~ spl24_426 ),
inference(superposition,[],[f2784,f2754]) ).
fof(f3411,plain,
( $false
| spl24_17
| ~ spl24_161
| ~ spl24_419
| ~ spl24_426 ),
inference(forward_subsumption_resolution,[],[f3407,f3372]) ).
fof(f3412,plain,
( spl24_17
| ~ spl24_161
| ~ spl24_419
| ~ spl24_426 ),
inference(avatar_contradiction_clause,[],[f3411]) ).
fof(f3428,plain,
( e21 = e22
| ~ spl24_422
| ~ spl24_429 ),
inference(superposition,[],[f2797,f2767]) ).
fof(f3432,plain,
( $false
| spl24_17
| ~ spl24_161
| ~ spl24_422
| ~ spl24_429 ),
inference(forward_subsumption_resolution,[],[f3428,f3372]) ).
fof(f3433,plain,
( spl24_17
| ~ spl24_161
| ~ spl24_422
| ~ spl24_429 ),
inference(avatar_contradiction_clause,[],[f3432]) ).
fof(f3450,plain,
( e21 = e23
| ~ spl24_27
| ~ spl24_192 ),
inference(forward_demodulation,[],[f891,f1671]) ).
fof(f3463,plain,
( $false
| ~ spl24_27
| ~ spl24_192 ),
inference(forward_subsumption_resolution,[],[f228,f3450]) ).
fof(f3464,plain,
( ~ spl24_27
| ~ spl24_192 ),
inference(avatar_contradiction_clause,[],[f3463]) ).
fof(f3465,plain,
( e21 != e23
| spl24_27
| ~ spl24_192 ),
inference(forward_demodulation,[],[f892,f1671]) ).
fof(f3470,plain,
( e20 = e21
| ~ spl24_13
| ~ spl24_18 ),
inference(forward_demodulation,[],[f848,f824]) ).
fof(f3512,plain,
( $false
| ~ spl24_13
| ~ spl24_18 ),
inference(forward_subsumption_resolution,[],[f232,f3470]) ).
fof(f3513,plain,
( ~ spl24_13
| ~ spl24_18 ),
inference(avatar_contradiction_clause,[],[f3512]) ).
fof(f3519,plain,
( e20 = e22
| ~ spl24_409
| ~ spl24_423 ),
inference(superposition,[],[f2772,f2712]) ).
fof(f3523,plain,
( $false
| spl24_42
| ~ spl24_233
| ~ spl24_409
| ~ spl24_423 ),
inference(forward_subsumption_resolution,[],[f3519,f3324]) ).
fof(f3524,plain,
( spl24_42
| ~ spl24_233
| ~ spl24_409
| ~ spl24_423 ),
inference(avatar_contradiction_clause,[],[f3523]) ).
fof(f3525,plain,
( e20 = e22
| ~ spl24_42
| ~ spl24_233 ),
inference(forward_demodulation,[],[f963,f1855]) ).
fof(f3531,plain,
( e21 = op2(e22,e23)
| ~ spl24_42
| ~ spl24_233
| ~ spl24_419 ),
inference(superposition,[],[f2754,f3525]) ).
fof(f3549,plain,
( spl24_461
| ~ spl24_42
| ~ spl24_233
| ~ spl24_419 ),
inference(avatar_split_clause,[],[f3531,f2752,f1854,f962,f2936]) ).
fof(f3551,plain,
( e20 != e22
| spl24_42
| ~ spl24_233 ),
inference(forward_demodulation,[],[f964,f1855]) ).
fof(f3631,plain,
( e20 = e21
| ~ spl24_437
| ~ spl24_442 ),
inference(forward_demodulation,[],[f2854,f2832]) ).
fof(f3632,plain,
( $false
| ~ spl24_13
| spl24_18
| ~ spl24_437
| ~ spl24_442 ),
inference(forward_subsumption_resolution,[],[f3631,f3317]) ).
fof(f3633,plain,
( ~ spl24_13
| spl24_18
| ~ spl24_437
| ~ spl24_442 ),
inference(avatar_contradiction_clause,[],[f3632]) ).
fof(f3681,plain,
( e20 = e22
| ~ spl24_439
| ~ spl24_449 ),
inference(superposition,[],[f2884,f2840]) ).
fof(f3685,plain,
( $false
| spl24_42
| ~ spl24_233
| ~ spl24_439
| ~ spl24_449 ),
inference(forward_subsumption_resolution,[],[f3681,f3551]) ).
fof(f3686,plain,
( spl24_42
| ~ spl24_233
| ~ spl24_439
| ~ spl24_449 ),
inference(avatar_contradiction_clause,[],[f3685]) ).
fof(f3760,plain,
( h1(e11) != op2(h1(e10),e21)
| ~ spl24_7
| spl24_124
| ~ spl24_483 ),
inference(superposition,[],[f3333,f3058]) ).
fof(f3775,plain,
( e11 = e12
| ~ spl24_483
| ~ spl24_490 ),
inference(superposition,[],[f3088,f3058]) ).
fof(f3781,plain,
( $false
| ~ spl24_483
| ~ spl24_490 ),
inference(forward_subsumption_resolution,[],[f3775,f223]) ).
fof(f3782,plain,
( ~ spl24_483
| ~ spl24_490 ),
inference(avatar_contradiction_clause,[],[f3781]) ).
fof(f3783,plain,
( e10 = e11
| ~ spl24_473
| ~ spl24_480 ),
inference(forward_demodulation,[],[f3046,f3016]) ).
fof(f3785,plain,
( $false
| ~ spl24_473
| ~ spl24_480 ),
inference(forward_subsumption_resolution,[],[f3783,f226]) ).
fof(f3786,plain,
( ~ spl24_473
| ~ spl24_480 ),
inference(avatar_contradiction_clause,[],[f3785]) ).
fof(f3796,plain,
( e11 = e12
| ~ spl24_485
| ~ spl24_492 ),
inference(superposition,[],[f3097,f3067]) ).
fof(f3800,plain,
( $false
| ~ spl24_485
| ~ spl24_492 ),
inference(forward_subsumption_resolution,[],[f3796,f223]) ).
fof(f3801,plain,
( ~ spl24_485
| ~ spl24_492 ),
inference(avatar_contradiction_clause,[],[f3800]) ).
fof(f3803,plain,
( e11 = e12
| ~ spl24_486
| ~ spl24_493 ),
inference(superposition,[],[f3101,f3071]) ).
fof(f3807,plain,
( $false
| ~ spl24_486
| ~ spl24_493 ),
inference(forward_subsumption_resolution,[],[f3803,f223]) ).
fof(f3808,plain,
( ~ spl24_486
| ~ spl24_493 ),
inference(avatar_contradiction_clause,[],[f3807]) ).
fof(f3811,plain,
( e12 = e13
| ~ spl24_488
| ~ spl24_495 ),
inference(superposition,[],[f3110,f3080]) ).
fof(f3815,plain,
( $false
| ~ spl24_488
| ~ spl24_495 ),
inference(forward_subsumption_resolution,[],[f3811,f221]) ).
fof(f3816,plain,
( ~ spl24_488
| ~ spl24_495 ),
inference(avatar_contradiction_clause,[],[f3815]) ).
fof(f3828,plain,
( e11 = e13
| ~ spl24_483
| ~ spl24_497 ),
inference(superposition,[],[f3118,f3058]) ).
fof(f3835,plain,
( $false
| ~ spl24_483
| ~ spl24_497 ),
inference(forward_subsumption_resolution,[],[f3828,f222]) ).
fof(f3836,plain,
( ~ spl24_483
| ~ spl24_497 ),
inference(avatar_contradiction_clause,[],[f3835]) ).
fof(f3840,plain,
( e12 = e13
| ~ spl24_491
| ~ spl24_498 ),
inference(superposition,[],[f3123,f3093]) ).
fof(f3844,plain,
( $false
| ~ spl24_491
| ~ spl24_498 ),
inference(forward_subsumption_resolution,[],[f3840,f221]) ).
fof(f3845,plain,
( ~ spl24_491
| ~ spl24_498 ),
inference(avatar_contradiction_clause,[],[f3844]) ).
fof(f3848,plain,
( e11 = e13
| ~ spl24_485
| ~ spl24_499 ),
inference(superposition,[],[f3127,f3067]) ).
fof(f3853,plain,
( $false
| ~ spl24_485
| ~ spl24_499 ),
inference(forward_subsumption_resolution,[],[f3848,f222]) ).
fof(f3854,plain,
( ~ spl24_485
| ~ spl24_499 ),
inference(avatar_contradiction_clause,[],[f3853]) ).
fof(f3856,plain,
( e10 = e12
| ~ spl24_473
| ~ spl24_487 ),
inference(superposition,[],[f3076,f3016]) ).
fof(f3860,plain,
( $false
| ~ spl24_473
| ~ spl24_487 ),
inference(forward_subsumption_resolution,[],[f3856,f225]) ).
fof(f3861,plain,
( ~ spl24_473
| ~ spl24_487 ),
inference(avatar_contradiction_clause,[],[f3860]) ).
fof(f3862,plain,
( e12 = e13
| ~ spl24_492
| ~ spl24_499 ),
inference(forward_demodulation,[],[f3097,f3127]) ).
fof(f3863,plain,
( $false
| ~ spl24_492
| ~ spl24_499 ),
inference(forward_subsumption_resolution,[],[f3862,f221]) ).
fof(f3864,plain,
( ~ spl24_492
| ~ spl24_499 ),
inference(avatar_contradiction_clause,[],[f3863]) ).
fof(f3878,plain,
( e10 = e11
| ~ spl24_501
| ~ spl24_506 ),
inference(forward_demodulation,[],[f3158,f3136]) ).
fof(f3879,plain,
( $false
| ~ spl24_501
| ~ spl24_506 ),
inference(forward_subsumption_resolution,[],[f3878,f226]) ).
fof(f3880,plain,
( ~ spl24_501
| ~ spl24_506 ),
inference(avatar_contradiction_clause,[],[f3879]) ).
fof(f3882,plain,
( e11 = e12
| ~ spl24_506
| ~ spl24_511 ),
inference(superposition,[],[f3180,f3158]) ).
fof(f3887,plain,
( $false
| ~ spl24_506
| ~ spl24_511 ),
inference(forward_subsumption_resolution,[],[f3882,f223]) ).
fof(f3888,plain,
( ~ spl24_506
| ~ spl24_511 ),
inference(avatar_contradiction_clause,[],[f3887]) ).
fof(f3903,plain,
( e11 = e13
| ~ spl24_506
| ~ spl24_516 ),
inference(superposition,[],[f3202,f3158]) ).
fof(f3909,plain,
( $false
| ~ spl24_506
| ~ spl24_516 ),
inference(forward_subsumption_resolution,[],[f3903,f222]) ).
fof(f3910,plain,
( ~ spl24_506
| ~ spl24_516 ),
inference(avatar_contradiction_clause,[],[f3909]) ).
fof(f3912,plain,
( e10 = e13
| ~ spl24_504
| ~ spl24_519 ),
inference(superposition,[],[f3215,f3149]) ).
fof(f3918,plain,
( $false
| ~ spl24_504
| ~ spl24_519 ),
inference(forward_subsumption_resolution,[],[f3912,f224]) ).
fof(f3919,plain,
( ~ spl24_504
| ~ spl24_519 ),
inference(avatar_contradiction_clause,[],[f3918]) ).
fof(f3949,plain,
( e10 = e12
| ~ spl24_505
| ~ spl24_515 ),
inference(superposition,[],[f3197,f3153]) ).
fof(f3953,plain,
( $false
| ~ spl24_505
| ~ spl24_515 ),
inference(forward_subsumption_resolution,[],[f3949,f225]) ).
fof(f3954,plain,
( ~ spl24_505
| ~ spl24_515 ),
inference(avatar_contradiction_clause,[],[f3953]) ).
fof(f3961,plain,
( e10 = e11
| ~ spl24_522
| ~ spl24_525 ),
inference(forward_demodulation,[],[f3242,f3228]) ).
fof(f3962,plain,
( $false
| ~ spl24_522
| ~ spl24_525 ),
inference(forward_subsumption_resolution,[],[f3961,f226]) ).
fof(f3963,plain,
( ~ spl24_522
| ~ spl24_525 ),
inference(avatar_contradiction_clause,[],[f3962]) ).
fof(f3973,plain,
( e11 = e12
| ~ spl24_524
| ~ spl24_527 ),
inference(superposition,[],[f3252,f3238]) ).
fof(f3978,plain,
( $false
| ~ spl24_524
| ~ spl24_527 ),
inference(forward_subsumption_resolution,[],[f3973,f223]) ).
fof(f3979,plain,
( ~ spl24_524
| ~ spl24_527 ),
inference(avatar_contradiction_clause,[],[f3978]) ).
fof(f3991,plain,
( e10 = e12
| ~ spl24_503
| ~ spl24_513 ),
inference(superposition,[],[f3188,f3144]) ).
fof(f3995,plain,
( $false
| ~ spl24_503
| ~ spl24_513 ),
inference(forward_subsumption_resolution,[],[f3991,f225]) ).
fof(f3996,plain,
( ~ spl24_503
| ~ spl24_513 ),
inference(avatar_contradiction_clause,[],[f3995]) ).
fof(f3999,plain,
( e12 = e13
| ~ spl24_527
| ~ spl24_530 ),
inference(superposition,[],[f3266,f3252]) ).
fof(f4003,plain,
( $false
| ~ spl24_527
| ~ spl24_530 ),
inference(forward_subsumption_resolution,[],[f3999,f221]) ).
fof(f4004,plain,
( ~ spl24_527
| ~ spl24_530 ),
inference(avatar_contradiction_clause,[],[f4003]) ).
fof(f4005,plain,
( e10 = e13
| ~ spl24_502
| ~ spl24_517 ),
inference(superposition,[],[f3206,f3140]) ).
fof(f4010,plain,
( $false
| ~ spl24_502
| ~ spl24_517 ),
inference(forward_subsumption_resolution,[],[f4005,f224]) ).
fof(f4011,plain,
( ~ spl24_502
| ~ spl24_517 ),
inference(avatar_contradiction_clause,[],[f4010]) ).
fof(f4014,plain,
( e10 = e13
| ~ spl24_522
| ~ spl24_531 ),
inference(superposition,[],[f3270,f3228]) ).
fof(f4018,plain,
( $false
| ~ spl24_522
| ~ spl24_531 ),
inference(forward_subsumption_resolution,[],[f4014,f224]) ).
fof(f4019,plain,
( ~ spl24_522
| ~ spl24_531 ),
inference(avatar_contradiction_clause,[],[f4018]) ).
fof(f4021,plain,
( e12 = e13
| ~ spl24_514
| ~ spl24_519 ),
inference(superposition,[],[f3215,f3193]) ).
fof(f4028,plain,
( $false
| ~ spl24_514
| ~ spl24_519 ),
inference(forward_subsumption_resolution,[],[f4021,f221]) ).
fof(f4029,plain,
( ~ spl24_514
| ~ spl24_519 ),
inference(avatar_contradiction_clause,[],[f4028]) ).
fof(f4030,plain,
( e10 = e13
| ~ spl24_474
| ~ spl24_495 ),
inference(forward_demodulation,[],[f3020,f3110]) ).
fof(f4032,plain,
( $false
| ~ spl24_474
| ~ spl24_495 ),
inference(forward_subsumption_resolution,[],[f4030,f224]) ).
fof(f4033,plain,
( ~ spl24_474
| ~ spl24_495 ),
inference(avatar_contradiction_clause,[],[f4032]) ).
fof(f4036,plain,
( e10 = e13
| ~ spl24_473
| ~ spl24_494 ),
inference(superposition,[],[f3106,f3016]) ).
fof(f4041,plain,
( $false
| ~ spl24_473
| ~ spl24_494 ),
inference(forward_subsumption_resolution,[],[f4036,f224]) ).
fof(f4042,plain,
( ~ spl24_473
| ~ spl24_494 ),
inference(avatar_contradiction_clause,[],[f4041]) ).
fof(f4045,plain,
( e12 = e13
| ~ spl24_489
| ~ spl24_496 ),
inference(superposition,[],[f3114,f3084]) ).
fof(f4050,plain,
( $false
| ~ spl24_489
| ~ spl24_496 ),
inference(forward_subsumption_resolution,[],[f4045,f221]) ).
fof(f4051,plain,
( ~ spl24_489
| ~ spl24_496 ),
inference(avatar_contradiction_clause,[],[f4050]) ).
fof(f4052,plain,
( e11 = e13
| ~ spl24_484
| ~ spl24_498 ),
inference(forward_demodulation,[],[f3063,f3123]) ).
fof(f4053,plain,
( $false
| ~ spl24_484
| ~ spl24_498 ),
inference(forward_subsumption_resolution,[],[f4052,f222]) ).
fof(f4054,plain,
( ~ spl24_484
| ~ spl24_498 ),
inference(avatar_contradiction_clause,[],[f4053]) ).
fof(f4093,plain,
( e10 = e12
| ~ spl24_474
| ~ spl24_488 ),
inference(superposition,[],[f3080,f3020]) ).
fof(f4098,plain,
( $false
| ~ spl24_474
| ~ spl24_488 ),
inference(forward_subsumption_resolution,[],[f4093,f225]) ).
fof(f4099,plain,
( ~ spl24_474
| ~ spl24_488 ),
inference(avatar_contradiction_clause,[],[f4098]) ).
fof(f4122,plain,
( e11 = e13
| ~ spl24_509
| ~ spl24_519 ),
inference(superposition,[],[f3215,f3171]) ).
fof(f4130,plain,
( $false
| ~ spl24_509
| ~ spl24_519 ),
inference(forward_subsumption_resolution,[],[f4122,f222]) ).
fof(f4131,plain,
( ~ spl24_509
| ~ spl24_519 ),
inference(avatar_contradiction_clause,[],[f4130]) ).
fof(f4165,plain,
( e10 = e11
| ~ spl24_505
| ~ spl24_510 ),
inference(forward_demodulation,[],[f3175,f3153]) ).
fof(f4169,plain,
( $false
| ~ spl24_505
| ~ spl24_510 ),
inference(forward_subsumption_resolution,[],[f4165,f226]) ).
fof(f4170,plain,
( ~ spl24_505
| ~ spl24_510 ),
inference(avatar_contradiction_clause,[],[f4169]) ).
fof(f4191,plain,
( e10 = e12
| ~ spl24_522
| ~ spl24_528 ),
inference(superposition,[],[f3256,f3228]) ).
fof(f4196,plain,
( $false
| ~ spl24_522
| ~ spl24_528 ),
inference(forward_subsumption_resolution,[],[f4191,f225]) ).
fof(f4197,plain,
( ~ spl24_522
| ~ spl24_528 ),
inference(avatar_contradiction_clause,[],[f4196]) ).
fof(f4242,plain,
( e11 = e13
| ~ spl24_534
| ~ spl24_536 ),
inference(superposition,[],[f3298,f3286]) ).
fof(f4248,plain,
( $false
| ~ spl24_534
| ~ spl24_536 ),
inference(forward_subsumption_resolution,[],[f4242,f222]) ).
fof(f4249,plain,
( ~ spl24_534
| ~ spl24_536 ),
inference(avatar_contradiction_clause,[],[f4248]) ).
fof(f4260,plain,
( e22 = h1(e10)
| ~ spl24_424 ),
inference(forward_demodulation,[],[f262,f2776]) ).
fof(f4261,plain,
( spl24_141
| ~ spl24_424 ),
inference(avatar_split_clause,[],[f4260,f2774,f1425]) ).
fof(f4262,plain,
( op2(e22,e21) != h1(e11)
| ~ spl24_7
| spl24_124
| ~ spl24_141
| ~ spl24_483 ),
inference(superposition,[],[f3760,f1426]) ).
fof(f4326,plain,
( e22 = e23
| ~ spl24_471
| ~ spl24_472 ),
inference(forward_demodulation,[],[f2988,f2994]) ).
fof(f4332,plain,
( $false
| ~ spl24_471
| ~ spl24_472 ),
inference(forward_subsumption_resolution,[],[f4326,f227]) ).
fof(f4333,plain,
( ~ spl24_471
| ~ spl24_472 ),
inference(avatar_contradiction_clause,[],[f4332]) ).
fof(f4338,plain,
( e21 = e23
| ~ spl24_470
| ~ spl24_472 ),
inference(forward_demodulation,[],[f2982,f2994]) ).
fof(f4342,plain,
( $false
| spl24_27
| ~ spl24_192
| ~ spl24_470
| ~ spl24_472 ),
inference(forward_subsumption_resolution,[],[f4338,f3465]) ).
fof(f4343,plain,
( spl24_27
| ~ spl24_192
| ~ spl24_470
| ~ spl24_472 ),
inference(avatar_contradiction_clause,[],[f4342]) ).
fof(f4369,plain,
( e20 = e22
| ~ spl24_458
| ~ spl24_464 ),
inference(superposition,[],[f2952,f2924]) ).
fof(f4373,plain,
( $false
| spl24_42
| ~ spl24_233
| ~ spl24_458
| ~ spl24_464 ),
inference(forward_subsumption_resolution,[],[f4369,f3551]) ).
fof(f4374,plain,
( spl24_42
| ~ spl24_233
| ~ spl24_458
| ~ spl24_464 ),
inference(avatar_contradiction_clause,[],[f4373]) ).
fof(f4500,plain,
( e13 != op1(e11,e13)
| ~ spl24_536 ),
inference(forward_demodulation,[],[f150,f3298]) ).
fof(f4540,plain,
( e20 != op2(e22,e21)
| ~ spl24_458 ),
inference(forward_demodulation,[],[f180,f2924]) ).
fof(f4541,plain,
( e22 != op2(e22,e21)
| ~ spl24_463 ),
inference(forward_demodulation,[],[f181,f2948]) ).
fof(f4543,plain,
( e20 != op2(e22,e20)
| ~ spl24_458 ),
inference(forward_demodulation,[],[f182,f2924]) ).
fof(f4544,plain,
( ~ spl24_414
| ~ spl24_458 ),
inference(avatar_split_clause,[],[f4543,f2922,f2731]) ).
fof(f4546,plain,
( e22 != op2(e22,e20)
| ~ spl24_463 ),
inference(forward_demodulation,[],[f183,f2948]) ).
fof(f4547,plain,
( e23 != op2(e22,e20)
| ~ spl24_455 ),
inference(forward_demodulation,[],[f184,f2911]) ).
fof(f4551,plain,
( e22 != op2(e21,e20)
| ~ spl24_449 ),
inference(forward_demodulation,[],[f188,f2884]) ).
fof(f4554,plain,
( e21 != op2(e21,e20)
| ~ spl24_442 ),
inference(forward_demodulation,[],[f190,f2854]) ).
fof(f4555,plain,
( e21 != op2(e20,e22)
| ~ spl24_419 ),
inference(forward_demodulation,[],[f191,f2754]) ).
fof(f4580,plain,
( e22 != op2(e20,e22)
| ~ spl24_463 ),
inference(forward_demodulation,[],[f207,f2948]) ).
fof(f4599,plain,
( e21 = op2(e20,e23)
| ~ spl24_458 ),
inference(forward_demodulation,[],[f259,f2924]) ).
fof(f4600,plain,
( op2(e22,e21) = h1(e11)
| ~ spl24_424 ),
inference(forward_demodulation,[],[f261,f2776]) ).
fof(f4601,plain,
( $false
| ~ spl24_7
| spl24_124
| ~ spl24_141
| ~ spl24_424
| ~ spl24_483 ),
inference(forward_subsumption_resolution,[],[f4600,f4262]) ).
fof(f4602,plain,
( ~ spl24_7
| spl24_124
| ~ spl24_141
| ~ spl24_424
| ~ spl24_483 ),
inference(avatar_contradiction_clause,[],[f4601]) ).
fof(f4603,plain,
( op2(e22,e22) != h1(op1(e10,e10))
| spl24_121
| ~ spl24_141 ),
inference(forward_demodulation,[],[f1344,f1426]) ).
fof(f4605,plain,
( e23 = h1(e11)
| ~ spl24_424
| ~ spl24_455 ),
inference(forward_demodulation,[],[f4600,f2911]) ).
fof(f4606,plain,
( op2(e22,e22) != h1(e10)
| spl24_121
| ~ spl24_141
| ~ spl24_473 ),
inference(forward_demodulation,[],[f4603,f3016]) ).
fof(f4610,plain,
( e22 != op2(e22,e22)
| spl24_121
| ~ spl24_141
| ~ spl24_473 ),
inference(forward_demodulation,[],[f4606,f1426]) ).
fof(f4612,plain,
( $false
| spl24_121
| ~ spl24_141
| ~ spl24_463
| ~ spl24_473 ),
inference(forward_subsumption_resolution,[],[f4610,f2948]) ).
fof(f4613,plain,
( spl24_121
| ~ spl24_141
| ~ spl24_463
| ~ spl24_473 ),
inference(avatar_contradiction_clause,[],[f4612]) ).
fof(f4618,plain,
( h1(op1(e10,e11)) != op2(e22,h1(e11))
| spl24_122
| ~ spl24_141 ),
inference(forward_demodulation,[],[f1348,f1426]) ).
fof(f4619,plain,
( spl24_142
| ~ spl24_424
| ~ spl24_455 ),
inference(avatar_split_clause,[],[f4605,f2909,f2774,f1430]) ).
fof(f4622,plain,
( h1(e12) != op2(e22,h1(e11))
| spl24_122
| ~ spl24_141
| ~ spl24_488 ),
inference(forward_demodulation,[],[f4618,f3080]) ).
fof(f4624,plain,
( e20 != op2(e22,h1(e11))
| ~ spl24_3
| spl24_122
| ~ spl24_141
| ~ spl24_488 ),
inference(forward_demodulation,[],[f4622,f776]) ).
fof(f4626,plain,
( e20 != op2(e22,e23)
| ~ spl24_3
| spl24_122
| ~ spl24_141
| ~ spl24_142
| ~ spl24_488 ),
inference(forward_demodulation,[],[f4624,f1431]) ).
fof(f4627,plain,
( $false
| ~ spl24_3
| spl24_122
| ~ spl24_141
| ~ spl24_142
| ~ spl24_458
| ~ spl24_488 ),
inference(forward_subsumption_resolution,[],[f4626,f2924]) ).
fof(f4628,plain,
( ~ spl24_3
| spl24_122
| ~ spl24_141
| ~ spl24_142
| ~ spl24_458
| ~ spl24_488 ),
inference(avatar_contradiction_clause,[],[f4627]) ).
fof(f4632,plain,
( ~ spl24_450
| ~ spl24_463 ),
inference(avatar_split_clause,[],[f4541,f2946,f2887]) ).
fof(f4634,plain,
( e21 != op2(e22,e21)
| ~ spl24_442 ),
inference(forward_demodulation,[],[f211,f2854]) ).
fof(f4639,plain,
( e21 != op2(e23,e21)
| ~ spl24_442 ),
inference(forward_demodulation,[],[f210,f2854]) ).
fof(f4641,plain,
( ~ spl24_440
| ~ spl24_458 ),
inference(avatar_split_clause,[],[f4540,f2922,f2843]) ).
fof(f4646,plain,
( ~ spl24_446
| ~ spl24_442 ),
inference(avatar_split_clause,[],[f4639,f2852,f2869]) ).
fof(f4648,plain,
( h1(op1(e10,e12)) != op2(h1(e10),e20)
| ~ spl24_3
| spl24_123 ),
inference(forward_demodulation,[],[f1352,f776]) ).
fof(f4654,plain,
( op2(e22,e20) != h1(op1(e10,e12))
| ~ spl24_3
| spl24_123
| ~ spl24_141 ),
inference(forward_demodulation,[],[f4648,f1426]) ).
fof(f4656,plain,
( op2(e22,e20) != h1(e13)
| ~ spl24_3
| spl24_123
| ~ spl24_141
| ~ spl24_496 ),
inference(forward_demodulation,[],[f4654,f3114]) ).
fof(f4657,plain,
( e21 != op2(e22,e20)
| ~ spl24_3
| ~ spl24_7
| spl24_123
| ~ spl24_141
| ~ spl24_496 ),
inference(forward_demodulation,[],[f4656,f795]) ).
fof(f4661,plain,
( h1(op1(e11,e10)) != op2(h1(e11),e22)
| spl24_125
| ~ spl24_141 ),
inference(forward_demodulation,[],[f1360,f1426]) ).
fof(f4663,plain,
( h1(e13) != op2(h1(e11),e22)
| spl24_125
| ~ spl24_141
| ~ spl24_498 ),
inference(forward_demodulation,[],[f4661,f3123]) ).
fof(f4665,plain,
( e21 != op2(h1(e11),e22)
| ~ spl24_7
| spl24_125
| ~ spl24_141
| ~ spl24_498 ),
inference(forward_demodulation,[],[f4663,f795]) ).
fof(f4671,plain,
( e21 != op2(e23,e22)
| ~ spl24_7
| spl24_125
| ~ spl24_141
| ~ spl24_142
| ~ spl24_498 ),
inference(forward_demodulation,[],[f4665,f1431]) ).
fof(f4672,plain,
( $false
| ~ spl24_7
| spl24_125
| ~ spl24_141
| ~ spl24_142
| ~ spl24_462
| ~ spl24_498 ),
inference(forward_subsumption_resolution,[],[f4671,f2943]) ).
fof(f4673,plain,
( ~ spl24_7
| spl24_125
| ~ spl24_141
| ~ spl24_142
| ~ spl24_462
| ~ spl24_498 ),
inference(avatar_contradiction_clause,[],[f4672]) ).
fof(f4675,plain,
( op2(e23,e23) != h1(op1(e11,e11))
| spl24_126
| ~ spl24_142 ),
inference(forward_demodulation,[],[f1364,f1431]) ).
fof(f4677,plain,
( op2(e23,e23) != h1(e11)
| spl24_126
| ~ spl24_142
| ~ spl24_506 ),
inference(forward_demodulation,[],[f4675,f3158]) ).
fof(f4679,plain,
( e23 != op2(e23,e23)
| spl24_126
| ~ spl24_142
| ~ spl24_506 ),
inference(forward_demodulation,[],[f4677,f1431]) ).
fof(f4681,plain,
( $false
| spl24_126
| ~ spl24_142
| ~ spl24_472
| ~ spl24_506 ),
inference(forward_subsumption_resolution,[],[f4679,f2994]) ).
fof(f4682,plain,
( spl24_126
| ~ spl24_142
| ~ spl24_472
| ~ spl24_506 ),
inference(avatar_contradiction_clause,[],[f4681]) ).
fof(f4684,plain,
( h1(op1(e11,e12)) != op2(h1(e11),e20)
| ~ spl24_3
| spl24_127 ),
inference(forward_demodulation,[],[f1368,f776]) ).
fof(f4686,plain,
( op2(e23,e20) != h1(op1(e11,e12))
| ~ spl24_3
| spl24_127
| ~ spl24_142 ),
inference(forward_demodulation,[],[f4684,f1431]) ).
fof(f4688,plain,
( op2(e23,e20) != h1(e10)
| ~ spl24_3
| spl24_127
| ~ spl24_142
| ~ spl24_502 ),
inference(forward_demodulation,[],[f4686,f3140]) ).
fof(f4689,plain,
( e22 != op2(e23,e20)
| ~ spl24_3
| spl24_127
| ~ spl24_141
| ~ spl24_142
| ~ spl24_502 ),
inference(forward_demodulation,[],[f4688,f1426]) ).
fof(f4690,plain,
( $false
| ~ spl24_3
| spl24_127
| ~ spl24_141
| ~ spl24_142
| ~ spl24_429
| ~ spl24_502 ),
inference(forward_subsumption_resolution,[],[f4689,f2797]) ).
fof(f4691,plain,
( ~ spl24_3
| spl24_127
| ~ spl24_141
| ~ spl24_142
| ~ spl24_429
| ~ spl24_502 ),
inference(avatar_contradiction_clause,[],[f4690]) ).
fof(f4693,plain,
( h1(op1(e11,e13)) != op2(h1(e11),e21)
| ~ spl24_7
| spl24_128 ),
inference(forward_demodulation,[],[f1372,f795]) ).
fof(f4695,plain,
( op2(e23,e21) != h1(op1(e11,e13))
| ~ spl24_7
| spl24_128
| ~ spl24_142 ),
inference(forward_demodulation,[],[f4693,f1431]) ).
fof(f4697,plain,
( op2(e23,e21) != h1(e12)
| ~ spl24_7
| spl24_128
| ~ spl24_142
| ~ spl24_513 ),
inference(forward_demodulation,[],[f4695,f3188]) ).
fof(f4699,plain,
( e20 != op2(e23,e21)
| ~ spl24_3
| ~ spl24_7
| spl24_128
| ~ spl24_142
| ~ spl24_513 ),
inference(forward_demodulation,[],[f4697,f776]) ).
fof(f4700,plain,
( ~ spl24_441
| ~ spl24_3
| ~ spl24_7
| spl24_128
| ~ spl24_142
| ~ spl24_513 ),
inference(avatar_split_clause,[],[f4699,f3186,f1430,f1370,f794,f775,f2847]) ).
fof(f4702,plain,
( h1(op1(e12,e10)) != op2(h1(e12),e22)
| spl24_129
| ~ spl24_141 ),
inference(forward_demodulation,[],[f1376,f1426]) ).
fof(f4704,plain,
( op2(e20,e22) != h1(op1(e12,e10))
| ~ spl24_3
| spl24_129
| ~ spl24_141 ),
inference(forward_demodulation,[],[f4702,f776]) ).
fof(f4706,plain,
( op2(e20,e22) != h1(e11)
| ~ spl24_3
| spl24_129
| ~ spl24_141
| ~ spl24_485 ),
inference(forward_demodulation,[],[f4704,f3067]) ).
fof(f4708,plain,
( e23 != op2(e20,e22)
| ~ spl24_3
| spl24_129
| ~ spl24_141
| ~ spl24_142
| ~ spl24_485 ),
inference(forward_demodulation,[],[f4706,f1431]) ).
fof(f4710,plain,
( $false
| ~ spl24_3
| spl24_129
| ~ spl24_141
| ~ spl24_142
| ~ spl24_432
| ~ spl24_485 ),
inference(forward_subsumption_resolution,[],[f4708,f2810]) ).
fof(f4711,plain,
( ~ spl24_3
| spl24_129
| ~ spl24_141
| ~ spl24_142
| ~ spl24_432
| ~ spl24_485 ),
inference(avatar_contradiction_clause,[],[f4710]) ).
fof(f4713,plain,
( h1(op1(e12,e11)) != op2(h1(e12),e23)
| spl24_130
| ~ spl24_142 ),
inference(forward_demodulation,[],[f1380,f1431]) ).
fof(f4715,plain,
( op2(e20,e23) != h1(op1(e12,e11))
| ~ spl24_3
| spl24_130
| ~ spl24_142 ),
inference(forward_demodulation,[],[f4713,f776]) ).
fof(f4717,plain,
( op2(e20,e23) != h1(e13)
| ~ spl24_3
| spl24_130
| ~ spl24_142
| ~ spl24_519 ),
inference(forward_demodulation,[],[f4715,f3215]) ).
fof(f4719,plain,
( e21 != op2(e20,e23)
| ~ spl24_3
| ~ spl24_7
| spl24_130
| ~ spl24_142
| ~ spl24_519 ),
inference(forward_demodulation,[],[f4717,f795]) ).
fof(f4720,plain,
( $false
| ~ spl24_3
| ~ spl24_7
| spl24_130
| ~ spl24_142
| ~ spl24_419
| ~ spl24_519 ),
inference(forward_subsumption_resolution,[],[f4719,f2754]) ).
fof(f4721,plain,
( ~ spl24_3
| ~ spl24_7
| spl24_130
| ~ spl24_142
| ~ spl24_419
| ~ spl24_519 ),
inference(avatar_contradiction_clause,[],[f4720]) ).
fof(f4723,plain,
( op2(e20,e20) != h1(op1(e12,e12))
| ~ spl24_3
| spl24_131 ),
inference(forward_demodulation,[],[f1384,f776]) ).
fof(f4725,plain,
( op2(e20,e20) != h1(e12)
| ~ spl24_3
| spl24_131
| ~ spl24_527 ),
inference(forward_demodulation,[],[f4723,f3252]) ).
fof(f4727,plain,
( e20 != op2(e20,e20)
| ~ spl24_3
| spl24_131
| ~ spl24_527 ),
inference(forward_demodulation,[],[f4725,f776]) ).
fof(f4729,plain,
( $false
| ~ spl24_3
| spl24_131
| ~ spl24_409
| ~ spl24_527 ),
inference(forward_subsumption_resolution,[],[f4727,f2712]) ).
fof(f4730,plain,
( ~ spl24_3
| spl24_131
| ~ spl24_409
| ~ spl24_527 ),
inference(avatar_contradiction_clause,[],[f4729]) ).
fof(f4732,plain,
( h1(op1(e12,e13)) != op2(h1(e12),e21)
| ~ spl24_7
| spl24_132 ),
inference(forward_demodulation,[],[f1388,f795]) ).
fof(f4734,plain,
( op2(e20,e21) != h1(op1(e12,e13))
| ~ spl24_3
| ~ spl24_7
| spl24_132 ),
inference(forward_demodulation,[],[f4732,f776]) ).
fof(f4736,plain,
( op2(e20,e21) != h1(e10)
| ~ spl24_3
| ~ spl24_7
| spl24_132
| ~ spl24_522 ),
inference(forward_demodulation,[],[f4734,f3228]) ).
fof(f4737,plain,
( e22 != op2(e20,e21)
| ~ spl24_3
| ~ spl24_7
| spl24_132
| ~ spl24_141
| ~ spl24_522 ),
inference(forward_demodulation,[],[f4736,f1426]) ).
fof(f4741,plain,
( h1(op1(e13,e10)) != op2(h1(e13),e22)
| spl24_133
| ~ spl24_141 ),
inference(forward_demodulation,[],[f1392,f1426]) ).
fof(f4743,plain,
( op2(e21,e22) != h1(op1(e13,e10))
| ~ spl24_7
| spl24_133
| ~ spl24_141 ),
inference(forward_demodulation,[],[f4741,f795]) ).
fof(f4745,plain,
( op2(e21,e22) != h1(e12)
| ~ spl24_7
| spl24_133
| ~ spl24_141
| ~ spl24_493 ),
inference(forward_demodulation,[],[f4743,f3101]) ).
fof(f4747,plain,
( e20 != op2(e21,e22)
| ~ spl24_3
| ~ spl24_7
| spl24_133
| ~ spl24_141
| ~ spl24_493 ),
inference(forward_demodulation,[],[f4745,f776]) ).
fof(f4748,plain,
( $false
| ~ spl24_3
| ~ spl24_7
| spl24_133
| ~ spl24_141
| ~ spl24_438
| ~ spl24_493 ),
inference(forward_subsumption_resolution,[],[f4747,f2836]) ).
fof(f4749,plain,
( ~ spl24_3
| ~ spl24_7
| spl24_133
| ~ spl24_141
| ~ spl24_438
| ~ spl24_493 ),
inference(avatar_contradiction_clause,[],[f4748]) ).
fof(f4751,plain,
( h1(op1(e13,e11)) != op2(h1(e13),e23)
| spl24_134
| ~ spl24_142 ),
inference(forward_demodulation,[],[f1396,f1431]) ).
fof(f4753,plain,
( op2(e21,e23) != h1(op1(e13,e11))
| ~ spl24_7
| spl24_134
| ~ spl24_142 ),
inference(forward_demodulation,[],[f4751,f795]) ).
fof(f4755,plain,
( op2(e21,e23) != h1(e10)
| ~ spl24_7
| spl24_134
| ~ spl24_142
| ~ spl24_505 ),
inference(forward_demodulation,[],[f4753,f3153]) ).
fof(f4757,plain,
( e22 != op2(e21,e23)
| ~ spl24_7
| spl24_134
| ~ spl24_141
| ~ spl24_142
| ~ spl24_505 ),
inference(forward_demodulation,[],[f4755,f1426]) ).
fof(f4758,plain,
( $false
| ~ spl24_7
| spl24_134
| ~ spl24_141
| ~ spl24_142
| ~ spl24_449
| ~ spl24_505 ),
inference(forward_subsumption_resolution,[],[f4757,f2884]) ).
fof(f4759,plain,
( ~ spl24_7
| spl24_134
| ~ spl24_141
| ~ spl24_142
| ~ spl24_449
| ~ spl24_505 ),
inference(avatar_contradiction_clause,[],[f4758]) ).
fof(f4761,plain,
( h1(op1(e13,e12)) != op2(h1(e13),e20)
| ~ spl24_3
| spl24_135 ),
inference(forward_demodulation,[],[f1400,f776]) ).
fof(f4763,plain,
( op2(e21,e20) != h1(op1(e13,e12))
| ~ spl24_3
| ~ spl24_7
| spl24_135 ),
inference(forward_demodulation,[],[f4761,f795]) ).
fof(f4765,plain,
( op2(e21,e20) != h1(e11)
| ~ spl24_3
| ~ spl24_7
| spl24_135
| ~ spl24_526 ),
inference(forward_demodulation,[],[f4763,f3247]) ).
fof(f4767,plain,
( e23 != op2(e21,e20)
| ~ spl24_3
| ~ spl24_7
| spl24_135
| ~ spl24_142
| ~ spl24_526 ),
inference(forward_demodulation,[],[f4765,f1431]) ).
fof(f4771,plain,
( op2(e21,e21) != h1(op1(e13,e13))
| ~ spl24_7
| spl24_136 ),
inference(forward_demodulation,[],[f1404,f795]) ).
fof(f4773,plain,
( op2(e21,e21) != h1(e13)
| ~ spl24_7
| spl24_136
| ~ spl24_536 ),
inference(forward_demodulation,[],[f4771,f3298]) ).
fof(f4775,plain,
( e21 != op2(e21,e21)
| ~ spl24_7
| spl24_136
| ~ spl24_536 ),
inference(forward_demodulation,[],[f4773,f795]) ).
fof(f4777,plain,
( $false
| ~ spl24_7
| spl24_136
| ~ spl24_442
| ~ spl24_536 ),
inference(forward_subsumption_resolution,[],[f4775,f2854]) ).
fof(f4778,plain,
( ~ spl24_7
| spl24_136
| ~ spl24_442
| ~ spl24_536 ),
inference(avatar_contradiction_clause,[],[f4777]) ).
fof(f4783,plain,
( ~ spl24_421
| ~ spl24_3
| ~ spl24_7
| spl24_123
| ~ spl24_141
| ~ spl24_496 ),
inference(avatar_split_clause,[],[f4657,f3112,f1425,f1350,f794,f775,f2761]) ).
fof(f4786,plain,
( e20 = e21
| ~ spl24_458
| ~ spl24_461 ),
inference(forward_demodulation,[],[f2938,f2924]) ).
fof(f4787,plain,
( ~ spl24_428
| ~ spl24_463 ),
inference(avatar_split_clause,[],[f4546,f2946,f2791]) ).
fof(f4799,plain,
( $false
| ~ spl24_13
| spl24_18
| ~ spl24_458
| ~ spl24_461 ),
inference(forward_subsumption_resolution,[],[f4786,f3317]) ).
fof(f4800,plain,
( ~ spl24_13
| spl24_18
| ~ spl24_458
| ~ spl24_461 ),
inference(avatar_contradiction_clause,[],[f4799]) ).
fof(f4807,plain,
( ~ spl24_445
| ~ spl24_442 ),
inference(avatar_split_clause,[],[f4634,f2852,f2865]) ).
fof(f4808,plain,
( ~ spl24_435
| ~ spl24_455 ),
inference(avatar_split_clause,[],[f4547,f2909,f2821]) ).
fof(f4811,plain,
( e20 != op2(e21,e20)
| ~ spl24_409 ),
inference(forward_demodulation,[],[f220,f2712]) ).
fof(f4813,plain,
( ~ spl24_420
| ~ spl24_442 ),
inference(avatar_split_clause,[],[f4554,f2852,f2757]) ).
fof(f4817,plain,
( ~ spl24_413
| ~ spl24_409 ),
inference(avatar_split_clause,[],[f4811,f2710,f2727]) ).
fof(f4831,plain,
( ~ spl24_424
| ~ spl24_3
| ~ spl24_7
| spl24_132
| ~ spl24_141
| ~ spl24_522 ),
inference(avatar_split_clause,[],[f4737,f3226,f1425,f1386,f794,f775,f2774]) ).
fof(f4840,plain,
( e20 != op2(e20,e22)
| ~ spl24_409 ),
inference(forward_demodulation,[],[f195,f2712]) ).
fof(f4842,plain,
( ~ spl24_425
| ~ spl24_463 ),
inference(avatar_split_clause,[],[f4580,f2946,f2778]) ).
fof(f4846,plain,
( e20 != op2(e20,e21)
| ~ spl24_409 ),
inference(forward_demodulation,[],[f196,f2712]) ).
fof(f4851,plain,
( spl24_419
| ~ spl24_458 ),
inference(avatar_split_clause,[],[f4599,f2922,f2752]) ).
fof(f4865,plain,
( ~ spl24_411
| ~ spl24_409 ),
inference(avatar_split_clause,[],[f4840,f2710,f2718]) ).
fof(f4867,plain,
( ~ spl24_410
| ~ spl24_409 ),
inference(avatar_split_clause,[],[f4846,f2710,f2714]) ).
fof(f4884,plain,
( ~ spl24_434
| ~ spl24_3
| ~ spl24_7
| spl24_135
| ~ spl24_142
| ~ spl24_526 ),
inference(avatar_split_clause,[],[f4767,f3245,f1430,f1398,f794,f775,f2817]) ).
fof(f4885,plain,
( ~ spl24_418
| ~ spl24_419 ),
inference(avatar_split_clause,[],[f4555,f2752,f2748]) ).
fof(f4896,plain,
( ~ spl24_427
| ~ spl24_449 ),
inference(avatar_split_clause,[],[f4551,f2882,f2787]) ).
fof(f4925,plain,
( e12 = e13
| ~ spl24_535
| ~ spl24_536 ),
inference(forward_demodulation,[],[f3292,f3298]) ).
fof(f4926,plain,
( ~ spl24_518
| ~ spl24_536 ),
inference(avatar_split_clause,[],[f4500,f3296,f3208]) ).
fof(f4928,plain,
( e11 != op1(e11,e13)
| ~ spl24_506 ),
inference(forward_demodulation,[],[f138,f3158]) ).
fof(f4932,plain,
( e10 != op1(e11,e10)
| ~ spl24_473 ),
inference(forward_demodulation,[],[f172,f3016]) ).
fof(f4944,plain,
( $false
| ~ spl24_535
| ~ spl24_536 ),
inference(forward_subsumption_resolution,[],[f4925,f221]) ).
fof(f4945,plain,
( ~ spl24_535
| ~ spl24_536 ),
inference(avatar_contradiction_clause,[],[f4944]) ).
fof(f4946,plain,
( ~ spl24_508
| ~ spl24_506 ),
inference(avatar_split_clause,[],[f4928,f3156,f3164]) ).
fof(f4948,plain,
( ~ spl24_477
| ~ spl24_473 ),
inference(avatar_split_clause,[],[f4932,f3014,f3031]) ).
cnf(s2,plain,
( spl24_1
| ~ spl24_3 ),
inference(sat_conversion,[],[f778]) ).
cnf(s5,plain,
( ~ spl24_6
| ~ spl24_7 ),
inference(sat_conversion,[],[f797]) ).
cnf(s104,plain,
( ~ spl24_1
| spl24_6
| ~ spl24_121
| ~ spl24_122
| ~ spl24_123
| ~ spl24_124
| ~ spl24_125
| ~ spl24_126
| ~ spl24_127
| ~ spl24_128
| ~ spl24_129
| ~ spl24_130
| ~ spl24_131
| ~ spl24_132
| ~ spl24_133
| ~ spl24_134
| ~ spl24_135
| ~ spl24_136
| ~ spl24_141
| ~ spl24_142 ),
inference(sat_conversion,[],[f1436]) ).
cnf(s303,plain,
spl24_233,
inference(sat_conversion,[],[f2699]) ).
cnf(s307,plain,
spl24_192,
inference(sat_conversion,[],[f2703]) ).
cnf(s309,plain,
spl24_161,
inference(sat_conversion,[],[f2705]) ).
cnf(s310,plain,
spl24_13,
inference(sat_conversion,[],[f2706]) ).
cnf(s311,plain,
spl24_7,
inference(sat_conversion,[],[f2707]) ).
cnf(s312,plain,
spl24_3,
inference(sat_conversion,[],[f2708]) ).
cnf(s317,plain,
( spl24_423
| spl24_424
| spl24_425
| spl24_426 ),
inference(sat_conversion,[],[f2785]) ).
cnf(s318,plain,
( spl24_423
| spl24_427
| spl24_428
| spl24_429 ),
inference(sat_conversion,[],[f2798]) ).
cnf(s321,plain,
( spl24_413
| spl24_437
| spl24_438
| spl24_439 ),
inference(sat_conversion,[],[f2841]) ).
cnf(s322,plain,
( spl24_410
| spl24_437
| spl24_440
| spl24_441 ),
inference(sat_conversion,[],[f2850]) ).
cnf(s339,plain,
( spl24_422
| spl24_446
| spl24_462
| spl24_470 ),
inference(sat_conversion,[],[f2983]) ).
cnf(s342,plain,
( spl24_426
| spl24_449
| spl24_464
| spl24_471 ),
inference(sat_conversion,[],[f2990]) ).
cnf(s347,plain,
( spl24_411
| spl24_418
| spl24_425
| spl24_432 ),
inference(sat_conversion,[],[f2999]) ).
cnf(s349,plain,
( spl24_413
| spl24_420
| spl24_427
| spl24_434 ),
inference(sat_conversion,[],[f3001]) ).
cnf(s353,plain,
( spl24_414
| spl24_421
| spl24_428
| spl24_435 ),
inference(sat_conversion,[],[f3005]) ).
cnf(s354,plain,
( spl24_440
| spl24_445
| spl24_450
| spl24_455 ),
inference(sat_conversion,[],[f3006]) ).
cnf(s364,plain,
( spl24_480
| spl24_484
| spl24_485
| spl24_486 ),
inference(sat_conversion,[],[f3072]) ).
cnf(s365,plain,
( spl24_487
| spl24_488
| spl24_489
| spl24_490 ),
inference(sat_conversion,[],[f3089]) ).
cnf(s366,plain,
( spl24_487
| spl24_491
| spl24_492
| spl24_493 ),
inference(sat_conversion,[],[f3102]) ).
cnf(s367,plain,
( spl24_494
| spl24_495
| spl24_496
| spl24_497 ),
inference(sat_conversion,[],[f3119]) ).
cnf(s369,plain,
( spl24_477
| spl24_501
| spl24_502
| spl24_503 ),
inference(sat_conversion,[],[f3145]) ).
cnf(s370,plain,
( spl24_474
| spl24_501
| spl24_504
| spl24_505 ),
inference(sat_conversion,[],[f3154]) ).
cnf(s374,plain,
( spl24_488
| spl24_511
| spl24_514
| spl24_515 ),
inference(sat_conversion,[],[f3198]) ).
cnf(s375,plain,
( spl24_498
| spl24_516
| spl24_517
| spl24_518 ),
inference(sat_conversion,[],[f3211]) ).
cnf(s379,plain,
( spl24_485
| spl24_509
| spl24_524
| spl24_525 ),
inference(sat_conversion,[],[f3243]) ).
cnf(s383,plain,
( spl24_499
| spl24_519
| spl24_530
| spl24_531 ),
inference(sat_conversion,[],[f3271]) ).
cnf(s387,plain,
( spl24_486
| spl24_510
| spl24_526
| spl24_534 ),
inference(sat_conversion,[],[f3287]) ).
cnf(s388,plain,
( spl24_483
| spl24_508
| spl24_525
| spl24_534 ),
inference(sat_conversion,[],[f3288]) ).
cnf(s390,plain,
( spl24_490
| spl24_513
| spl24_528
| spl24_535 ),
inference(sat_conversion,[],[f3294]) ).
cnf(s409,plain,
spl24_536,
inference(sat_conversion,[],[f3335]) ).
cnf(s410,plain,
spl24_527,
inference(sat_conversion,[],[f3336]) ).
cnf(s411,plain,
spl24_506,
inference(sat_conversion,[],[f3337]) ).
cnf(s412,plain,
spl24_473,
inference(sat_conversion,[],[f3338]) ).
cnf(s413,plain,
spl24_472,
inference(sat_conversion,[],[f3339]) ).
cnf(s414,plain,
spl24_463,
inference(sat_conversion,[],[f3340]) ).
cnf(s415,plain,
spl24_442,
inference(sat_conversion,[],[f3341]) ).
cnf(s416,plain,
spl24_409,
inference(sat_conversion,[],[f3342]) ).
cnf(s417,plain,
spl24_522,
inference(sat_conversion,[],[f3343]) ).
cnf(s418,plain,
spl24_458,
inference(sat_conversion,[],[f3344]) ).
cnf(s426,plain,
( ~ spl24_17
| ~ spl24_161 ),
inference(sat_conversion,[],[f3371]) ).
cnf(s436,plain,
( spl24_17
| ~ spl24_161
| ~ spl24_419
| ~ spl24_426 ),
inference(sat_conversion,[],[f3412]) ).
cnf(s442,plain,
( spl24_17
| ~ spl24_161
| ~ spl24_422
| ~ spl24_429 ),
inference(sat_conversion,[],[f3433]) ).
cnf(s449,plain,
( ~ spl24_27
| ~ spl24_192 ),
inference(sat_conversion,[],[f3464]) ).
cnf(s461,plain,
( ~ spl24_13
| ~ spl24_18 ),
inference(sat_conversion,[],[f3513]) ).
cnf(s464,plain,
( spl24_42
| ~ spl24_233
| ~ spl24_409
| ~ spl24_423 ),
inference(sat_conversion,[],[f3524]) ).
cnf(s473,plain,
( ~ spl24_42
| ~ spl24_233
| ~ spl24_419
| spl24_461 ),
inference(sat_conversion,[],[f3549]) ).
cnf(s498,plain,
( ~ spl24_13
| spl24_18
| ~ spl24_437
| ~ spl24_442 ),
inference(sat_conversion,[],[f3633]) ).
cnf(s510,plain,
( spl24_42
| ~ spl24_233
| ~ spl24_439
| ~ spl24_449 ),
inference(sat_conversion,[],[f3686]) ).
cnf(s531,plain,
( ~ spl24_483
| ~ spl24_490 ),
inference(sat_conversion,[],[f3782]) ).
cnf(s532,plain,
( ~ spl24_473
| ~ spl24_480 ),
inference(sat_conversion,[],[f3786]) ).
cnf(s536,plain,
( ~ spl24_485
| ~ spl24_492 ),
inference(sat_conversion,[],[f3801]) ).
cnf(s538,plain,
( ~ spl24_486
| ~ spl24_493 ),
inference(sat_conversion,[],[f3808]) ).
cnf(s540,plain,
( ~ spl24_488
| ~ spl24_495 ),
inference(sat_conversion,[],[f3816]) ).
cnf(s544,plain,
( ~ spl24_483
| ~ spl24_497 ),
inference(sat_conversion,[],[f3836]) ).
cnf(s546,plain,
( ~ spl24_491
| ~ spl24_498 ),
inference(sat_conversion,[],[f3845]) ).
cnf(s548,plain,
( ~ spl24_485
| ~ spl24_499 ),
inference(sat_conversion,[],[f3854]) ).
cnf(s550,plain,
( ~ spl24_473
| ~ spl24_487 ),
inference(sat_conversion,[],[f3861]) ).
cnf(s551,plain,
( ~ spl24_492
| ~ spl24_499 ),
inference(sat_conversion,[],[f3864]) ).
cnf(s554,plain,
( ~ spl24_501
| ~ spl24_506 ),
inference(sat_conversion,[],[f3880]) ).
cnf(s556,plain,
( ~ spl24_506
| ~ spl24_511 ),
inference(sat_conversion,[],[f3888]) ).
cnf(s562,plain,
( ~ spl24_506
| ~ spl24_516 ),
inference(sat_conversion,[],[f3910]) ).
cnf(s564,plain,
( ~ spl24_504
| ~ spl24_519 ),
inference(sat_conversion,[],[f3919]) ).
cnf(s571,plain,
( ~ spl24_505
| ~ spl24_515 ),
inference(sat_conversion,[],[f3954]) ).
cnf(s572,plain,
( ~ spl24_522
| ~ spl24_525 ),
inference(sat_conversion,[],[f3963]) ).
cnf(s576,plain,
( ~ spl24_524
| ~ spl24_527 ),
inference(sat_conversion,[],[f3979]) ).
cnf(s580,plain,
( ~ spl24_503
| ~ spl24_513 ),
inference(sat_conversion,[],[f3996]) ).
cnf(s582,plain,
( ~ spl24_527
| ~ spl24_530 ),
inference(sat_conversion,[],[f4004]) ).
cnf(s584,plain,
( ~ spl24_502
| ~ spl24_517 ),
inference(sat_conversion,[],[f4011]) ).
cnf(s586,plain,
( ~ spl24_522
| ~ spl24_531 ),
inference(sat_conversion,[],[f4019]) ).
cnf(s588,plain,
( ~ spl24_514
| ~ spl24_519 ),
inference(sat_conversion,[],[f4029]) ).
cnf(s589,plain,
( ~ spl24_474
| ~ spl24_495 ),
inference(sat_conversion,[],[f4033]) ).
cnf(s591,plain,
( ~ spl24_473
| ~ spl24_494 ),
inference(sat_conversion,[],[f4042]) ).
cnf(s593,plain,
( ~ spl24_489
| ~ spl24_496 ),
inference(sat_conversion,[],[f4051]) ).
cnf(s594,plain,
( ~ spl24_484
| ~ spl24_498 ),
inference(sat_conversion,[],[f4054]) ).
cnf(s600,plain,
( ~ spl24_474
| ~ spl24_488 ),
inference(sat_conversion,[],[f4099]) ).
cnf(s604,plain,
( ~ spl24_509
| ~ spl24_519 ),
inference(sat_conversion,[],[f4131]) ).
cnf(s613,plain,
( ~ spl24_505
| ~ spl24_510 ),
inference(sat_conversion,[],[f4170]) ).
cnf(s618,plain,
( ~ spl24_522
| ~ spl24_528 ),
inference(sat_conversion,[],[f4197]) ).
cnf(s627,plain,
( ~ spl24_534
| ~ spl24_536 ),
inference(sat_conversion,[],[f4249]) ).
cnf(s628,plain,
( spl24_141
| ~ spl24_424 ),
inference(sat_conversion,[],[f4261]) ).
cnf(s644,plain,
( ~ spl24_471
| ~ spl24_472 ),
inference(sat_conversion,[],[f4333]) ).
cnf(s647,plain,
( spl24_27
| ~ spl24_192
| ~ spl24_470
| ~ spl24_472 ),
inference(sat_conversion,[],[f4343]) ).
cnf(s654,plain,
( spl24_42
| ~ spl24_233
| ~ spl24_458
| ~ spl24_464 ),
inference(sat_conversion,[],[f4374]) ).
cnf(s677,plain,
( ~ spl24_414
| ~ spl24_458 ),
inference(sat_conversion,[],[f4544]) ).
cnf(s680,plain,
( ~ spl24_7
| spl24_124
| ~ spl24_141
| ~ spl24_424
| ~ spl24_483 ),
inference(sat_conversion,[],[f4602]) ).
cnf(s682,plain,
( spl24_121
| ~ spl24_141
| ~ spl24_463
| ~ spl24_473 ),
inference(sat_conversion,[],[f4613]) ).
cnf(s684,plain,
( spl24_142
| ~ spl24_424
| ~ spl24_455 ),
inference(sat_conversion,[],[f4619]) ).
cnf(s686,plain,
( ~ spl24_3
| spl24_122
| ~ spl24_141
| ~ spl24_142
| ~ spl24_458
| ~ spl24_488 ),
inference(sat_conversion,[],[f4628]) ).
cnf(s689,plain,
( ~ spl24_450
| ~ spl24_463 ),
inference(sat_conversion,[],[f4632]) ).
cnf(s691,plain,
( ~ spl24_440
| ~ spl24_458 ),
inference(sat_conversion,[],[f4641]) ).
cnf(s695,plain,
( ~ spl24_442
| ~ spl24_446 ),
inference(sat_conversion,[],[f4646]) ).
cnf(s701,plain,
( ~ spl24_7
| spl24_125
| ~ spl24_141
| ~ spl24_142
| ~ spl24_462
| ~ spl24_498 ),
inference(sat_conversion,[],[f4673]) ).
cnf(s702,plain,
( spl24_126
| ~ spl24_142
| ~ spl24_472
| ~ spl24_506 ),
inference(sat_conversion,[],[f4682]) ).
cnf(s703,plain,
( ~ spl24_3
| spl24_127
| ~ spl24_141
| ~ spl24_142
| ~ spl24_429
| ~ spl24_502 ),
inference(sat_conversion,[],[f4691]) ).
cnf(s704,plain,
( ~ spl24_3
| ~ spl24_7
| spl24_128
| ~ spl24_142
| ~ spl24_441
| ~ spl24_513 ),
inference(sat_conversion,[],[f4700]) ).
cnf(s706,plain,
( ~ spl24_3
| spl24_129
| ~ spl24_141
| ~ spl24_142
| ~ spl24_432
| ~ spl24_485 ),
inference(sat_conversion,[],[f4711]) ).
cnf(s707,plain,
( ~ spl24_3
| ~ spl24_7
| spl24_130
| ~ spl24_142
| ~ spl24_419
| ~ spl24_519 ),
inference(sat_conversion,[],[f4721]) ).
cnf(s708,plain,
( ~ spl24_3
| spl24_131
| ~ spl24_409
| ~ spl24_527 ),
inference(sat_conversion,[],[f4730]) ).
cnf(s710,plain,
( ~ spl24_3
| ~ spl24_7
| spl24_133
| ~ spl24_141
| ~ spl24_438
| ~ spl24_493 ),
inference(sat_conversion,[],[f4749]) ).
cnf(s711,plain,
( ~ spl24_7
| spl24_134
| ~ spl24_141
| ~ spl24_142
| ~ spl24_449
| ~ spl24_505 ),
inference(sat_conversion,[],[f4759]) ).
cnf(s713,plain,
( ~ spl24_7
| spl24_136
| ~ spl24_442
| ~ spl24_536 ),
inference(sat_conversion,[],[f4778]) ).
cnf(s714,plain,
( ~ spl24_3
| ~ spl24_7
| spl24_123
| ~ spl24_141
| ~ spl24_421
| ~ spl24_496 ),
inference(sat_conversion,[],[f4783]) ).
cnf(s715,plain,
( ~ spl24_428
| ~ spl24_463 ),
inference(sat_conversion,[],[f4787]) ).
cnf(s719,plain,
( ~ spl24_13
| spl24_18
| ~ spl24_458
| ~ spl24_461 ),
inference(sat_conversion,[],[f4800]) ).
cnf(s724,plain,
( ~ spl24_442
| ~ spl24_445 ),
inference(sat_conversion,[],[f4807]) ).
cnf(s725,plain,
( ~ spl24_435
| ~ spl24_455 ),
inference(sat_conversion,[],[f4808]) ).
cnf(s728,plain,
( ~ spl24_420
| ~ spl24_442 ),
inference(sat_conversion,[],[f4813]) ).
cnf(s730,plain,
( ~ spl24_409
| ~ spl24_413 ),
inference(sat_conversion,[],[f4817]) ).
cnf(s733,plain,
( ~ spl24_3
| ~ spl24_7
| spl24_132
| ~ spl24_141
| ~ spl24_424
| ~ spl24_522 ),
inference(sat_conversion,[],[f4831]) ).
cnf(s741,plain,
( ~ spl24_425
| ~ spl24_463 ),
inference(sat_conversion,[],[f4842]) ).
cnf(s745,plain,
( spl24_419
| ~ spl24_458 ),
inference(sat_conversion,[],[f4851]) ).
cnf(s752,plain,
( ~ spl24_409
| ~ spl24_411 ),
inference(sat_conversion,[],[f4865]) ).
cnf(s754,plain,
( ~ spl24_409
| ~ spl24_410 ),
inference(sat_conversion,[],[f4867]) ).
cnf(s763,plain,
( ~ spl24_3
| ~ spl24_7
| spl24_135
| ~ spl24_142
| ~ spl24_434
| ~ spl24_526 ),
inference(sat_conversion,[],[f4884]) ).
cnf(s764,plain,
( ~ spl24_418
| ~ spl24_419 ),
inference(sat_conversion,[],[f4885]) ).
cnf(s771,plain,
( ~ spl24_427
| ~ spl24_449 ),
inference(sat_conversion,[],[f4896]) ).
cnf(s790,plain,
( ~ spl24_518
| ~ spl24_536 ),
inference(sat_conversion,[],[f4926]) ).
cnf(s795,plain,
( ~ spl24_535
| ~ spl24_536 ),
inference(sat_conversion,[],[f4945]) ).
cnf(s796,plain,
( ~ spl24_506
| ~ spl24_508 ),
inference(sat_conversion,[],[f4946]) ).
cnf(s798,plain,
( ~ spl24_473
| ~ spl24_477 ),
inference(sat_conversion,[],[f4948]) ).
cnf(s803,plain,
spl24_419,
inference(rat,[],[s745,s418]) ).
cnf(s804,plain,
~ spl24_440,
inference(rat,[],[s691,s418]) ).
cnf(s806,plain,
~ spl24_414,
inference(rat,[],[s677,s418]) ).
cnf(s809,plain,
~ spl24_418,
inference(rat,[],[s764,s803]) ).
cnf(s813,plain,
~ spl24_528,
inference(rat,[],[s618,s417]) ).
cnf(s814,plain,
~ spl24_531,
inference(rat,[],[s586,s417]) ).
cnf(s815,plain,
~ spl24_525,
inference(rat,[],[s572,s417]) ).
cnf(s817,plain,
~ spl24_410,
inference(rat,[],[s754,s416]) ).
cnf(s818,plain,
~ spl24_411,
inference(rat,[],[s752,s416]) ).
cnf(s819,plain,
~ spl24_413,
inference(rat,[],[s730,s416]) ).
cnf(s820,plain,
~ spl24_420,
inference(rat,[],[s728,s415]) ).
cnf(s821,plain,
~ spl24_445,
inference(rat,[],[s724,s415]) ).
cnf(s822,plain,
~ spl24_446,
inference(rat,[],[s695,s415]) ).
cnf(s823,plain,
~ spl24_425,
inference(rat,[],[s741,s414]) ).
cnf(s824,plain,
~ spl24_428,
inference(rat,[],[s715,s414]) ).
cnf(s825,plain,
~ spl24_450,
inference(rat,[],[s689,s414]) ).
cnf(s831,plain,
~ spl24_471,
inference(rat,[],[s644,s413]) ).
cnf(s833,plain,
~ spl24_477,
inference(rat,[],[s798,s412]) ).
cnf(s834,plain,
~ spl24_494,
inference(rat,[],[s591,s412]) ).
cnf(s835,plain,
~ spl24_487,
inference(rat,[],[s550,s412]) ).
cnf(s836,plain,
~ spl24_480,
inference(rat,[],[s532,s412]) ).
cnf(s837,plain,
~ spl24_508,
inference(rat,[],[s796,s411]) ).
cnf(s838,plain,
~ spl24_516,
inference(rat,[],[s562,s411]) ).
cnf(s839,plain,
~ spl24_511,
inference(rat,[],[s556,s411]) ).
cnf(s840,plain,
~ spl24_501,
inference(rat,[],[s554,s411]) ).
cnf(s841,plain,
~ spl24_530,
inference(rat,[],[s582,s410]) ).
cnf(s843,plain,
~ spl24_524,
inference(rat,[],[s576,s410]) ).
cnf(s844,plain,
~ spl24_535,
inference(rat,[],[s795,s409]) ).
cnf(s846,plain,
~ spl24_518,
inference(rat,[],[s790,s409]) ).
cnf(s847,plain,
~ spl24_534,
inference(rat,[],[s627,s409]) ).
cnf(s853,plain,
( spl24_490
| spl24_513 ),
inference(rat,[],[s390,s844,s813]) ).
cnf(s855,plain,
spl24_483,
inference(rat,[],[s388,s847,s815,s837]) ).
cnf(s856,plain,
~ spl24_497,
inference(rat,[],[s544,s855]) ).
cnf(s857,plain,
~ spl24_490,
inference(rat,[],[s531,s855]) ).
cnf(s858,plain,
spl24_513,
inference(rat,[],[s853,s857]) ).
cnf(s859,plain,
~ spl24_503,
inference(rat,[],[s580,s858]) ).
cnf(s860,plain,
( spl24_486
| spl24_510
| spl24_526 ),
inference(rat,[],[s387,s847]) ).
cnf(s863,plain,
( spl24_499
| spl24_519 ),
inference(rat,[],[s383,s814,s841]) ).
cnf(s865,plain,
( spl24_485
| spl24_509 ),
inference(rat,[],[s379,s815,s843]) ).
cnf(s868,plain,
( spl24_498
| spl24_517 ),
inference(rat,[],[s375,s846,s838]) ).
cnf(s869,plain,
( spl24_488
| spl24_514
| spl24_515 ),
inference(rat,[],[s374,s839]) ).
cnf(s870,plain,
( spl24_474
| spl24_504
| spl24_505 ),
inference(rat,[],[s370,s840]) ).
cnf(s871,plain,
spl24_502,
inference(rat,[],[s369,s859,s840,s833]) ).
cnf(s872,plain,
~ spl24_517,
inference(rat,[],[s584,s871]) ).
cnf(s874,plain,
spl24_498,
inference(rat,[],[s868,s872]) ).
cnf(s875,plain,
~ spl24_484,
inference(rat,[],[s594,s874]) ).
cnf(s876,plain,
~ spl24_491,
inference(rat,[],[s546,s874]) ).
cnf(s877,plain,
( spl24_495
| spl24_496 ),
inference(rat,[],[s367,s856,s834]) ).
cnf(s878,plain,
( spl24_492
| spl24_493 ),
inference(rat,[],[s366,s876,s835]) ).
cnf(s879,plain,
( spl24_488
| spl24_489 ),
inference(rat,[],[s365,s857,s835]) ).
cnf(s880,plain,
( spl24_485
| spl24_486 ),
inference(rat,[],[s364,s875,s836]) ).
cnf(s884,plain,
spl24_455,
inference(rat,[],[s354,s825,s821,s804]) ).
cnf(s885,plain,
~ spl24_435,
inference(rat,[],[s725,s884]) ).
cnf(s887,plain,
spl24_421,
inference(rat,[],[s353,s885,s824,s806]) ).
cnf(s891,plain,
( spl24_427
| spl24_434 ),
inference(rat,[],[s349,s820,s819]) ).
cnf(s892,plain,
spl24_432,
inference(rat,[],[s347,s823,s809,s818]) ).
cnf(s895,plain,
( spl24_426
| spl24_449
| spl24_464 ),
inference(rat,[],[s342,s831]) ).
cnf(s897,plain,
( spl24_422
| spl24_462
| spl24_470 ),
inference(rat,[],[s339,s822]) ).
cnf(s903,plain,
( spl24_437
| spl24_441 ),
inference(rat,[],[s322,s804,s817]) ).
cnf(s904,plain,
( spl24_437
| spl24_438
| spl24_439 ),
inference(rat,[],[s321,s819]) ).
cnf(s906,plain,
( spl24_423
| spl24_427
| spl24_429 ),
inference(rat,[],[s318,s824]) ).
cnf(s907,plain,
( spl24_423
| spl24_424
| spl24_426 ),
inference(rat,[],[s317,s823]) ).
cnf(s908,plain,
spl24_131,
inference(rat,[],[s708,s410,s416,s312]) ).
cnf(s909,plain,
spl24_136,
inference(rat,[],[s713,s409,s415,s311]) ).
cnf(s910,plain,
~ spl24_18,
inference(rat,[],[s461,s310]) ).
cnf(s911,plain,
~ spl24_461,
inference(rat,[],[s719,s310,s418,s910]) ).
cnf(s912,plain,
~ spl24_437,
inference(rat,[],[s498,s415,s310,s910]) ).
cnf(s914,plain,
spl24_441,
inference(rat,[],[s903,s912]) ).
cnf(s917,plain,
~ spl24_17,
inference(rat,[],[s426,s309]) ).
cnf(s920,plain,
~ spl24_426,
inference(rat,[],[s436,s309,s803,s917]) ).
cnf(s922,plain,
~ spl24_27,
inference(rat,[],[s449,s307]) ).
cnf(s923,plain,
~ spl24_470,
inference(rat,[],[s647,s413,s307,s922]) ).
cnf(s925,plain,
~ spl24_42,
inference(rat,[],[s473,s911,s803,s303]) ).
cnf(s926,plain,
~ spl24_464,
inference(rat,[],[s654,s303,s418,s925]) ).
cnf(s928,plain,
~ spl24_423,
inference(rat,[],[s464,s303,s416,s925]) ).
cnf(s929,plain,
spl24_449,
inference(rat,[],[s895,s920,s926]) ).
cnf(s930,plain,
spl24_424,
inference(rat,[],[s907,s920,s928]) ).
cnf(s931,plain,
~ spl24_427,
inference(rat,[],[s771,s929]) ).
cnf(s934,plain,
~ spl24_439,
inference(rat,[],[s510,s925,s303,s929]) ).
cnf(s936,plain,
spl24_142,
inference(rat,[],[s684,s884,s930]) ).
cnf(s937,plain,
spl24_141,
inference(rat,[],[s628,s930]) ).
cnf(s939,plain,
spl24_434,
inference(rat,[],[s891,s931]) ).
cnf(s940,plain,
spl24_429,
inference(rat,[],[s906,s928,s931]) ).
cnf(s941,plain,
spl24_438,
inference(rat,[],[s904,s912,s934]) ).
cnf(s942,plain,
spl24_126,
inference(rat,[],[s702,s411,s413,s936]) ).
cnf(s943,plain,
spl24_128,
inference(rat,[],[s704,s858,s914,s311,s312,s936]) ).
cnf(s944,plain,
spl24_121,
inference(rat,[],[s682,s412,s414,s937]) ).
cnf(s945,plain,
spl24_127,
inference(rat,[],[s703,s871,s940,s936,s312,s937]) ).
cnf(s946,plain,
spl24_132,
inference(rat,[],[s733,s417,s930,s311,s312,s937]) ).
cnf(s947,plain,
spl24_124,
inference(rat,[],[s680,s855,s930,s311,s937]) ).
cnf(s950,plain,
~ spl24_422,
inference(rat,[],[s442,s917,s309,s940]) ).
cnf(s956,plain,
spl24_462,
inference(rat,[],[s897,s923,s950]) ).
cnf(s961,plain,
spl24_125,
inference(rat,[],[s701,s874,s937,s936,s311,s956]) ).
cnf(s1102,plain,
( ~ spl24_1
| spl24_6
| ~ spl24_122
| ~ spl24_123
| ~ spl24_129
| ~ spl24_130
| ~ spl24_133
| ~ spl24_134
| ~ spl24_135 ),
inference(rat,[],[s104,s936,s937,s909,s946,s908,s943,s945,s942,s961,s947,s944]) ).
cnf(s1126,plain,
~ spl24_6,
inference(rat,[],[s5,s311]) ).
cnf(s1127,plain,
spl24_1,
inference(rat,[],[s2,s312]) ).
cnf(s1128,plain,
spl24_485,
inference(rat,[],[s551,s878,s863,s538,s604,s880,s865]) ).
cnf(s1129,plain,
~ spl24_499,
inference(rat,[],[s548,s1128]) ).
cnf(s1130,plain,
~ spl24_492,
inference(rat,[],[s536,s1128]) ).
cnf(s1131,plain,
spl24_129,
inference(rat,[],[s706,s937,s892,s936,s312,s1128]) ).
cnf(s1132,plain,
spl24_519,
inference(rat,[],[s863,s1129]) ).
cnf(s1133,plain,
spl24_493,
inference(rat,[],[s878,s1130]) ).
cnf(s1135,plain,
~ spl24_514,
inference(rat,[],[s588,s1132]) ).
cnf(s1136,plain,
~ spl24_504,
inference(rat,[],[s564,s1132]) ).
cnf(s1137,plain,
spl24_130,
inference(rat,[],[s707,s936,s803,s311,s312,s1132]) ).
cnf(s1138,plain,
~ spl24_486,
inference(rat,[],[s538,s1133]) ).
cnf(s1139,plain,
spl24_133,
inference(rat,[],[s710,s937,s941,s311,s312,s1133]) ).
cnf(s1140,plain,
spl24_488,
inference(rat,[],[s589,s870,s877,s571,s593,s869,s879,s1136,s1135]) ).
cnf(s1141,plain,
~ spl24_474,
inference(rat,[],[s600,s1140]) ).
cnf(s1142,plain,
~ spl24_495,
inference(rat,[],[s540,s1140]) ).
cnf(s1144,plain,
spl24_122,
inference(rat,[],[s686,s937,s418,s936,s312,s1140]) ).
cnf(s1145,plain,
spl24_505,
inference(rat,[],[s870,s1136,s1141]) ).
cnf(s1146,plain,
spl24_496,
inference(rat,[],[s877,s1142]) ).
cnf(s1147,plain,
~ spl24_510,
inference(rat,[],[s613,s1145]) ).
cnf(s1150,plain,
spl24_134,
inference(rat,[],[s711,s937,s929,s936,s311,s1145]) ).
cnf(s1153,plain,
spl24_123,
inference(rat,[],[s714,s937,s887,s311,s312,s1146]) ).
cnf(s1154,plain,
spl24_526,
inference(rat,[],[s860,s1138,s1147]) ).
cnf(s1155,plain,
~ spl24_135,
inference(rat,[],[s1102,s1139,s1137,s1131,s1153,s1144,s1127,s1126,s1150]) ).
cnf(s1158,plain,
$false,
inference(rat,[],[s763,s936,s939,s311,s312,s1154,s1155]) ).
fof(f4953,plain,
$false,
inference(avatar_sat_refutation,[],[s1158]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG113+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 % Computer : n004.cluster.edu
% 0.08/0.21 % Model : x86_64 x86_64
% 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.21 % Memory : 8046.5625MB
% 0.08/0.21 % OS : Linux 6.8.0-71-generic
% 0.08/0.21 % CPULimit : 300
% 0.08/0.21 % WCLimit : 300
% 0.08/0.21 % DateTime : Mon Sep 28 19:30:07 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.24 Running first-order model finding
% 0.08/0.24 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.62/0.42 % (673518)Will run a generic schedule for satisfiability detection.
% 0.62/0.42 % (673523)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=388658721_2999 on theBenchmark for (2999ds/0Mi)
% 0.62/0.42 % (673524)% WARNING: option uhcvi not known.
% 0.62/0.42 % (673528)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1146225618:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.62/0.42 % (673524)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4143632110:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.62/0.42 % (673525)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3860448973:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.62/0.42 % (673526)dis+10_1_sil=32000:sp=arity:random_seed=367736224:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.62/0.42 % (673527)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1858622430:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.62/0.42 % (673529)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1596278369:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.62/0.42 % Detected minimum model sizes of [8]
% 0.62/0.42 % Detected maximum model sizes of [max]
% 0.62/0.42 % TRYING [8]
% 0.62/0.42 % (673526)Instruction limit reached!
% 0.62/0.42 % (673526)------------------------------
% 0.62/0.42 % (673526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.42 % (673526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.42 % (673526)CaDiCaL version: 2.1.3
% 0.62/0.42 % (673526)Termination reason: Instruction limit
% 0.62/0.42 % (673526)Termination phase: Saturation
% 0.62/0.42 % (673526)Time elapsed: 0.049 s
% 0.62/0.42 % (673526)Peak memory usage: 13 MB
% 0.62/0.42 % (673526)Instructions burned: 103 (million)
% 0.62/0.42 % (673527)Instruction limit reached!
% 0.62/0.42 % (673527)------------------------------
% 0.62/0.42 % (673527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.42 % (673527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.42 % (673527)CaDiCaL version: 2.1.3
% 0.62/0.42 % (673527)Termination reason: Instruction limit
% 0.62/0.42 % (673527)Termination phase: Saturation
% 0.62/0.42 % (673527)Time elapsed: 0.049 s
% 0.62/0.42 % (673527)Peak memory usage: 13 MB
% 0.62/0.42 % (673527)Instructions burned: 117 (million)
% 0.62/0.42 % (673528)Instruction limit reached!
% 0.62/0.42 % (673528)------------------------------
% 0.62/0.42 % (673528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.42 % (673528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.42 % (673528)CaDiCaL version: 2.1.3
% 0.62/0.42 % (673528)Termination reason: Instruction limit
% 0.62/0.42 % (673528)Termination phase: Saturation
% 0.62/0.42 % (673528)Time elapsed: 0.064 s
% 0.62/0.42 % (673528)Peak memory usage: 14 MB
% 0.62/0.42 % (673528)Instructions burned: 131 (million)
% 0.62/0.42 % (673537)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=182481195:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.62/0.42 % (673538)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1818691331:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.62/0.42 % (673529)Instruction limit reached!
% 0.62/0.42 % (673529)------------------------------
% 0.62/0.42 % (673529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.42 % (673529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.42 % (673529)CaDiCaL version: 2.1.3
% 0.62/0.42 % (673529)Termination reason: Instruction limit
% 0.62/0.42 % (673529)Termination phase: Saturation
% 0.62/0.42 % (673529)Time elapsed: 0.083 s
% 0.62/0.42 % (673529)Peak memory usage: 14 MB
% 0.62/0.42 % (673529)Instructions burned: 159 (million)
% 0.62/0.42 % (673539)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2137486157:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.62/0.42 % (673543)ott-21_1_sil=16000:fs=off:random_seed=688389876:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.62/0.42 % (673524) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-673518-673524"...
% 0.62/0.42 % Detected minimum model sizes of [8]
% 0.62/0.42 % Detected maximum model sizes of [max]
% 0.62/0.42 % TRYING [8]
% 0.62/0.42 % (673524)...printing done.
% 0.62/0.42 % (673524)Refutation found. Thanks to Tanya!
% 0.62/0.42 % SZS status Theorem for theBenchmark
% 0.62/0.42 % SZS output start Proof for theBenchmark
% See solution above
% 0.62/0.42 % (673524)------------------------------
% 0.62/0.42 % (673524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.42 % (673524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.42 % (673524)CaDiCaL version: 2.1.3
% 0.62/0.42 % (673524)Termination reason: Refutation
% 0.62/0.42 % (673524)Time elapsed: 0.119 s
% 0.62/0.42 % (673524)Peak memory usage: 16 MB
% 0.62/0.42 % (673524)Instructions burned: 239 (million)
% 0.62/0.42 % (673518)Success in time 0.169 s
% 0.62/0.42 % Vampire exiting
%------------------------------------------------------------------------------