%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG037+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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:20:35 AM UTC 2026
% Result : Theorem 1.02s 0.39s
% Output : Refutation 1.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 129
% Syntax : Number of formulae : 881 ( 160 unt; 114 def)
% Number of atoms : 3769 (1992 equ)
% Maximal formula atoms : 384 ( 4 avg)
% Number of connectives : 4511 (1623 ~;2037 |; 737 &)
% ( 114 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 3 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 122 ( 120 usr; 121 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
( op1(unit1,e10) = e10
& op1(e10,unit1) = e10
& op1(unit1,e11) = e11
& op1(e11,unit1) = e11
& op1(unit1,e12) = e12
& op1(e12,unit1) = e12
& op1(unit1,e13) = e13
& op1(e13,unit1) = e13
& ( unit1 = e10
| unit1 = e11
| unit1 = e12
| unit1 = e13 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e11) = e10
| op1(e10,e12) = e10
| op1(e10,e13) = e10 )
& ( op1(e10,e10) = e10
| op1(e11,e10) = e10
| op1(e12,e10) = e10
| op1(e13,e10) = e10 )
& ( op1(e10,e10) = e11
| op1(e10,e11) = e11
| op1(e10,e12) = e11
| op1(e10,e13) = e11 )
& ( op1(e10,e10) = e11
| op1(e11,e10) = e11
| op1(e12,e10) = e11
| op1(e13,e10) = e11 )
& ( op1(e10,e10) = e12
| op1(e10,e11) = e12
| op1(e10,e12) = e12
| op1(e10,e13) = e12 )
& ( op1(e10,e10) = e12
| op1(e11,e10) = e12
| op1(e12,e10) = e12
| op1(e13,e10) = e12 )
& ( op1(e10,e10) = e13
| op1(e10,e11) = e13
| op1(e10,e12) = e13
| op1(e10,e13) = e13 )
& ( op1(e10,e10) = e13
| op1(e11,e10) = e13
| op1(e12,e10) = e13
| op1(e13,e10) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e11) = e10
| op1(e11,e12) = e10
| op1(e11,e13) = e10 )
& ( op1(e10,e11) = e10
| op1(e11,e11) = e10
| op1(e12,e11) = e10
| op1(e13,e11) = e10 )
& ( op1(e11,e10) = e11
| op1(e11,e11) = e11
| op1(e11,e12) = e11
| op1(e11,e13) = e11 )
& ( op1(e10,e11) = e11
| op1(e11,e11) = e11
| op1(e12,e11) = e11
| op1(e13,e11) = e11 )
& ( op1(e11,e10) = e12
| op1(e11,e11) = e12
| op1(e11,e12) = e12
| op1(e11,e13) = e12 )
& ( op1(e10,e11) = e12
| op1(e11,e11) = e12
| op1(e12,e11) = e12
| op1(e13,e11) = e12 )
& ( op1(e11,e10) = e13
| op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e11,e13) = e13 )
& ( op1(e10,e11) = e13
| op1(e11,e11) = e13
| op1(e12,e11) = e13
| op1(e13,e11) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e11) = e10
| op1(e12,e12) = e10
| op1(e12,e13) = e10 )
& ( op1(e10,e12) = e10
| op1(e11,e12) = e10
| op1(e12,e12) = e10
| op1(e13,e12) = e10 )
& ( op1(e12,e10) = e11
| op1(e12,e11) = e11
| op1(e12,e12) = e11
| op1(e12,e13) = e11 )
& ( op1(e10,e12) = e11
| op1(e11,e12) = e11
| op1(e12,e12) = e11
| op1(e13,e12) = e11 )
& ( op1(e12,e10) = e12
| op1(e12,e11) = e12
| op1(e12,e12) = e12
| op1(e12,e13) = e12 )
& ( op1(e10,e12) = e12
| op1(e11,e12) = e12
| op1(e12,e12) = e12
| op1(e13,e12) = e12 )
& ( op1(e12,e10) = e13
| op1(e12,e11) = e13
| op1(e12,e12) = e13
| op1(e12,e13) = e13 )
& ( op1(e10,e12) = e13
| op1(e11,e12) = e13
| op1(e12,e12) = e13
| op1(e13,e12) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10 )
& ( op1(e10,e13) = e10
| op1(e11,e13) = e10
| op1(e12,e13) = e10
| op1(e13,e13) = e10 )
& ( op1(e13,e10) = e11
| op1(e13,e11) = e11
| op1(e13,e12) = e11
| op1(e13,e13) = e11 )
& ( op1(e10,e13) = e11
| op1(e11,e13) = e11
| op1(e12,e13) = e11
| op1(e13,e13) = e11 )
& ( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12
| op1(e13,e13) = e12 )
& ( op1(e10,e13) = e12
| op1(e11,e13) = e12
| op1(e12,e13) = e12
| op1(e13,e13) = e12 )
& ( op1(e13,e10) = e13
| op1(e13,e11) = e13
| op1(e13,e12) = e13
| op1(e13,e13) = e13 )
& ( op1(e10,e13) = e13
| op1(e11,e13) = e13
| op1(e12,e13) = e13
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f5,axiom,
( op2(unit2,e20) = e20
& op2(e20,unit2) = e20
& op2(unit2,e21) = e21
& op2(e21,unit2) = e21
& op2(unit2,e22) = e22
& op2(e22,unit2) = e22
& op2(unit2,e23) = e23
& op2(e23,unit2) = e23
& ( unit2 = e20
| unit2 = e21
| unit2 = e22
| unit2 = e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e22) = e20
| op2(e20,e23) = e20 )
& ( op2(e20,e20) = e20
| op2(e21,e20) = e20
| op2(e22,e20) = e20
| op2(e23,e20) = e20 )
& ( op2(e20,e20) = e21
| op2(e20,e21) = e21
| op2(e20,e22) = e21
| op2(e20,e23) = e21 )
& ( op2(e20,e20) = e21
| op2(e21,e20) = e21
| op2(e22,e20) = e21
| op2(e23,e20) = e21 )
& ( op2(e20,e20) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 )
& ( op2(e20,e20) = e22
| op2(e21,e20) = e22
| op2(e22,e20) = e22
| op2(e23,e20) = e22 )
& ( op2(e20,e20) = e23
| op2(e20,e21) = e23
| op2(e20,e22) = e23
| op2(e20,e23) = e23 )
& ( op2(e20,e20) = e23
| op2(e21,e20) = e23
| op2(e22,e20) = e23
| op2(e23,e20) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e21) = e20
| op2(e21,e22) = e20
| op2(e21,e23) = e20 )
& ( op2(e20,e21) = e20
| op2(e21,e21) = e20
| op2(e22,e21) = e20
| op2(e23,e21) = e20 )
& ( op2(e21,e20) = e21
| op2(e21,e21) = e21
| op2(e21,e22) = e21
| op2(e21,e23) = e21 )
& ( op2(e20,e21) = e21
| op2(e21,e21) = e21
| op2(e22,e21) = e21
| op2(e23,e21) = e21 )
& ( op2(e21,e20) = e22
| op2(e21,e21) = e22
| op2(e21,e22) = e22
| op2(e21,e23) = e22 )
& ( op2(e20,e21) = e22
| op2(e21,e21) = e22
| op2(e22,e21) = e22
| op2(e23,e21) = e22 )
& ( op2(e21,e20) = e23
| op2(e21,e21) = e23
| op2(e21,e22) = e23
| op2(e21,e23) = e23 )
& ( op2(e20,e21) = e23
| op2(e21,e21) = e23
| op2(e22,e21) = e23
| op2(e23,e21) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e21) = e20
| op2(e22,e22) = e20
| op2(e22,e23) = e20 )
& ( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e22,e22) = e20
| op2(e23,e22) = e20 )
& ( op2(e22,e20) = e21
| op2(e22,e21) = e21
| op2(e22,e22) = e21
| op2(e22,e23) = e21 )
& ( op2(e20,e22) = e21
| op2(e21,e22) = e21
| op2(e22,e22) = e21
| op2(e23,e22) = e21 )
& ( op2(e22,e20) = e22
| op2(e22,e21) = e22
| op2(e22,e22) = e22
| op2(e22,e23) = e22 )
& ( op2(e20,e22) = e22
| op2(e21,e22) = e22
| op2(e22,e22) = e22
| op2(e23,e22) = e22 )
& ( op2(e22,e20) = e23
| op2(e22,e21) = e23
| op2(e22,e22) = e23
| op2(e22,e23) = e23 )
& ( op2(e20,e22) = e23
| op2(e21,e22) = e23
| op2(e22,e22) = e23
| op2(e23,e22) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e23) = e20 )
& ( op2(e20,e23) = e20
| op2(e21,e23) = e20
| op2(e22,e23) = e20
| op2(e23,e23) = e20 )
& ( op2(e23,e20) = e21
| op2(e23,e21) = e21
| op2(e23,e22) = e21
| op2(e23,e23) = e21 )
& ( op2(e20,e23) = e21
| op2(e21,e23) = e21
| op2(e22,e23) = e21
| op2(e23,e23) = e21 )
& ( op2(e23,e20) = e22
| op2(e23,e21) = e22
| op2(e23,e22) = e22
| op2(e23,e23) = e22 )
& ( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22
| op2(e23,e23) = e22 )
& ( op2(e23,e20) = e23
| op2(e23,e21) = e23
| op2(e23,e22) = e23
| op2(e23,e23) = e23 )
& ( op2(e20,e23) = e23
| op2(e21,e23) = e23
| op2(e22,e23) = e23
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f9,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
fof(f10,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
fof(f12,axiom,
( ( op1(e10,e10) = e10
& op1(e11,e11) = e10
& op1(e12,e12) = e10
& op1(e13,e13) = e10 )
| ( op1(e10,e10) = e11
& op1(e11,e11) = e11
& op1(e12,e12) = e11
& op1(e13,e13) = e11 )
| ( op1(e10,e10) = e12
& op1(e11,e11) = e12
& op1(e12,e12) = e12
& op1(e13,e13) = e12 )
| ( op1(e10,e10) = e13
& op1(e11,e11) = e13
& op1(e12,e12) = e13
& op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( ( op2(e20,e20) = e20
& op2(e21,e21) = e20
& op2(e22,e22) = e20
& op2(e23,e23) = e20 )
| ( op2(e20,e20) = e21
& op2(e21,e21) = e21
& op2(e22,e22) = e21
& op2(e23,e23) = e21 )
| ( op2(e20,e20) = e22
& op2(e21,e21) = e22
& op2(e22,e22) = e22
& op2(e23,e23) = e22 )
| ( op2(e20,e20) = e23
& op2(e21,e21) = e23
& op2(e22,e22) = e23
& op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( e10 = op1(e11,e11)
& e12 = op1(e13,e11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
( e20 = op2(e21,e21)
& e22 = op2(e23,e21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
fof(f17,axiom,
( h2(e11) = e20
& h2(e13) = e22
& h2(e10) = op2(e20,e20)
& h2(e12) = op2(e22,e20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
fof(f20,axiom,
( h5(e11) = e21
& h5(e13) = e22
& h5(e10) = op2(e21,e21)
& h5(e12) = op2(e22,e21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax20) ).
fof(f21,axiom,
( h6(e11) = e21
& h6(e13) = e23
& h6(e10) = op2(e21,e21)
& h6(e12) = op2(e23,e21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax21) ).
fof(f27,axiom,
( h12(e11) = e23
& h12(e13) = e22
& h12(e10) = op2(e23,e23)
& h12(e12) = op2(e22,e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax27) ).
fof(f28,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/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f29,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)],[f28]) ).
fof(f30,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,[],[f29]) ).
fof(f47,plain,
( e13 = unit1
| e12 = unit1
| e11 = unit1
| e10 = unit1 ),
inference(cnf_transformation,[],[f2]) ).
fof(f48,plain,
e13 = op1(e13,unit1),
inference(cnf_transformation,[],[f2]) ).
fof(f49,plain,
e13 = op1(unit1,e13),
inference(cnf_transformation,[],[f2]) ).
fof(f50,plain,
e12 = op1(e12,unit1),
inference(cnf_transformation,[],[f2]) ).
fof(f51,plain,
e12 = op1(unit1,e12),
inference(cnf_transformation,[],[f2]) ).
fof(f52,plain,
e11 = op1(e11,unit1),
inference(cnf_transformation,[],[f2]) ).
fof(f53,plain,
e11 = op1(unit1,e11),
inference(cnf_transformation,[],[f2]) ).
fof(f70,plain,
( e13 = op1(e11,e13)
| e13 = op1(e11,e12)
| e13 = op1(e11,e11)
| e13 = op1(e11,e10) ),
inference(cnf_transformation,[],[f3]) ).
fof(f71,plain,
( e13 = op1(e13,e11)
| e13 = op1(e12,e11)
| e13 = op1(e11,e11)
| e13 = op1(e10,e11) ),
inference(cnf_transformation,[],[f3]) ).
fof(f74,plain,
( e11 = op1(e12,e13)
| e11 = op1(e12,e12)
| e11 = op1(e12,e11)
| e11 = op1(e12,e10) ),
inference(cnf_transformation,[],[f3]) ).
fof(f82,plain,
( e11 = op1(e13,e13)
| e11 = op1(e13,e12)
| e11 = op1(e13,e11)
| e11 = op1(e13,e10) ),
inference(cnf_transformation,[],[f3]) ).
fof(f85,plain,
( e12 = op1(e13,e13)
| e12 = op1(e12,e13)
| e12 = op1(e11,e13)
| e12 = op1(e10,e13) ),
inference(cnf_transformation,[],[f3]) ).
fof(f104,plain,
( e23 = unit2
| e22 = unit2
| e21 = unit2
| e20 = unit2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f105,plain,
e23 = op2(e23,unit2),
inference(cnf_transformation,[],[f5]) ).
fof(f106,plain,
e23 = op2(unit2,e23),
inference(cnf_transformation,[],[f5]) ).
fof(f107,plain,
e22 = op2(e22,unit2),
inference(cnf_transformation,[],[f5]) ).
fof(f108,plain,
e22 = op2(unit2,e22),
inference(cnf_transformation,[],[f5]) ).
fof(f109,plain,
e21 = op2(e21,unit2),
inference(cnf_transformation,[],[f5]) ).
fof(f110,plain,
e21 = op2(unit2,e21),
inference(cnf_transformation,[],[f5]) ).
fof(f111,plain,
e20 = op2(e20,unit2),
inference(cnf_transformation,[],[f5]) ).
fof(f128,plain,
( e23 = op2(e23,e21)
| e23 = op2(e22,e21)
| e23 = op2(e21,e21)
| e23 = op2(e20,e21) ),
inference(cnf_transformation,[],[f6]) ).
fof(f131,plain,
( e21 = op2(e22,e23)
| e21 = op2(e22,e22)
| e21 = op2(e22,e21)
| e21 = op2(e22,e20) ),
inference(cnf_transformation,[],[f6]) ).
fof(f136,plain,
( e23 = op2(e23,e22)
| e23 = op2(e22,e22)
| e23 = op2(e21,e22)
| e23 = op2(e20,e22) ),
inference(cnf_transformation,[],[f6]) ).
fof(f139,plain,
( e21 = op2(e23,e23)
| e21 = op2(e23,e22)
| e21 = op2(e23,e21)
| e21 = op2(e23,e20) ),
inference(cnf_transformation,[],[f6]) ).
fof(f142,plain,
( e22 = op2(e23,e23)
| e22 = op2(e22,e23)
| e22 = op2(e21,e23)
| e22 = op2(e20,e23) ),
inference(cnf_transformation,[],[f6]) ).
fof(f241,plain,
e12 != e13,
inference(cnf_transformation,[],[f9]) ).
fof(f242,plain,
e11 != e13,
inference(cnf_transformation,[],[f9]) ).
fof(f243,plain,
e11 != e12,
inference(cnf_transformation,[],[f9]) ).
fof(f244,plain,
e10 != e13,
inference(cnf_transformation,[],[f9]) ).
fof(f245,plain,
e10 != e12,
inference(cnf_transformation,[],[f9]) ).
fof(f246,plain,
e10 != e11,
inference(cnf_transformation,[],[f9]) ).
fof(f247,plain,
e22 != e23,
inference(cnf_transformation,[],[f10]) ).
fof(f248,plain,
e21 != e23,
inference(cnf_transformation,[],[f10]) ).
fof(f249,plain,
e21 != e22,
inference(cnf_transformation,[],[f10]) ).
fof(f251,plain,
e20 != e22,
inference(cnf_transformation,[],[f10]) ).
fof(f252,plain,
e20 != e21,
inference(cnf_transformation,[],[f10]) ).
fof(f269,plain,
( e10 = op1(e13,e13)
| ~ sP1 ),
inference(cnf_transformation,[],[f12]) ).
fof(f270,plain,
( e10 = op1(e12,e12)
| ~ sP1 ),
inference(cnf_transformation,[],[f12]) ).
fof(f272,plain,
( e10 = op1(e10,e10)
| ~ sP1 ),
inference(cnf_transformation,[],[f12]) ).
fof(f275,plain,
( e11 = op1(e11,e11)
| ~ sP0 ),
inference(cnf_transformation,[],[f12]) ).
fof(f283,plain,
( e13 = op1(e11,e11)
| e12 = op1(e11,e11)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f12]) ).
fof(f293,plain,
( e20 = op2(e23,e23)
| ~ sP3 ),
inference(cnf_transformation,[],[f13]) ).
fof(f294,plain,
( e20 = op2(e22,e22)
| ~ sP3 ),
inference(cnf_transformation,[],[f13]) ).
fof(f296,plain,
( e20 = op2(e20,e20)
| ~ sP3 ),
inference(cnf_transformation,[],[f13]) ).
fof(f299,plain,
( e21 = op2(e21,e21)
| ~ sP2 ),
inference(cnf_transformation,[],[f13]) ).
fof(f307,plain,
( e23 = op2(e21,e21)
| e22 = op2(e21,e21)
| sP2
| sP3 ),
inference(cnf_transformation,[],[f13]) ).
fof(f311,plain,
( e23 = op2(e22,e22)
| e22 = op2(e21,e21)
| sP2
| sP3 ),
inference(cnf_transformation,[],[f13]) ).
fof(f317,plain,
e12 = op1(e13,e11),
inference(cnf_transformation,[],[f14]) ).
fof(f318,plain,
e10 = op1(e11,e11),
inference(cnf_transformation,[],[f14]) ).
fof(f319,plain,
e22 = op2(e23,e21),
inference(cnf_transformation,[],[f15]) ).
fof(f320,plain,
e20 = op2(e21,e21),
inference(cnf_transformation,[],[f15]) ).
fof(f327,plain,
e22 = h2(e13),
inference(cnf_transformation,[],[f17]) ).
fof(f328,plain,
e20 = h2(e11),
inference(cnf_transformation,[],[f17]) ).
fof(f337,plain,
op2(e22,e21) = h5(e12),
inference(cnf_transformation,[],[f20]) ).
fof(f338,plain,
op2(e21,e21) = h5(e10),
inference(cnf_transformation,[],[f20]) ).
fof(f339,plain,
e22 = h5(e13),
inference(cnf_transformation,[],[f20]) ).
fof(f340,plain,
e21 = h5(e11),
inference(cnf_transformation,[],[f20]) ).
fof(f343,plain,
e23 = h6(e13),
inference(cnf_transformation,[],[f21]) ).
fof(f344,plain,
e21 = h6(e11),
inference(cnf_transformation,[],[f21]) ).
fof(f367,plain,
e22 = h12(e13),
inference(cnf_transformation,[],[f27]) ).
fof(f404,plain,
( e20 != h5(e10)
| ~ sP19 ),
inference(cnf_transformation,[],[f30]) ).
fof(f407,plain,
( e21 != h5(e11)
| ~ sP18 ),
inference(cnf_transformation,[],[f30]) ).
fof(f537,plain,
( e23 != h5(e12)
| e22 != h5(e13)
| sP18
| sP19
| h5(op1(e13,e13)) != op2(h5(e13),h5(e13))
| h5(op1(e13,e12)) != op2(h5(e13),h5(e12))
| h5(op1(e13,e11)) != op2(h5(e13),h5(e11))
| h5(op1(e13,e10)) != op2(h5(e13),h5(e10))
| h5(op1(e12,e13)) != op2(h5(e12),h5(e13))
| h5(op1(e12,e12)) != op2(h5(e12),h5(e12))
| h5(op1(e12,e11)) != op2(h5(e12),h5(e11))
| h5(op1(e12,e10)) != op2(h5(e12),h5(e10))
| h5(op1(e11,e13)) != op2(h5(e11),h5(e13))
| h5(op1(e11,e12)) != op2(h5(e11),h5(e12))
| h5(op1(e11,e11)) != op2(h5(e11),h5(e11))
| h5(op1(e11,e10)) != op2(h5(e11),h5(e10))
| h5(op1(e10,e13)) != op2(h5(e10),h5(e13))
| h5(op1(e10,e12)) != op2(h5(e10),h5(e12))
| h5(op1(e10,e11)) != op2(h5(e10),h5(e11))
| h5(op1(e10,e10)) != op2(h5(e10),h5(e10)) ),
inference(cnf_transformation,[],[f30]) ).
fof(f666,plain,
( e13 = op1(e11,e11)
| e12 = op1(e11,e11)
| sP0
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f283]) ).
fof(f673,plain,
( e10 = op1(e10,e10)
| sP1 ),
inference(consistent_polarity_flipping,[],[f272]) ).
fof(f675,plain,
( e10 = op1(e12,e12)
| sP1 ),
inference(consistent_polarity_flipping,[],[f270]) ).
fof(f676,plain,
( e10 = op1(e13,e13)
| sP1 ),
inference(consistent_polarity_flipping,[],[f269]) ).
fof(f682,plain,
( e23 = op2(e22,e22)
| e22 = op2(e21,e21)
| ~ sP2
| sP3 ),
inference(consistent_polarity_flipping,[],[f311]) ).
fof(f686,plain,
( e23 = op2(e21,e21)
| e22 = op2(e21,e21)
| ~ sP2
| sP3 ),
inference(consistent_polarity_flipping,[],[f307]) ).
fof(f694,plain,
( e21 = op2(e21,e21)
| sP2 ),
inference(consistent_polarity_flipping,[],[f299]) ).
fof(f904,definition,
( spl28_14
<=> e20 = h2(e11) ),
introduced(definition,[new_symbols(definition,[spl28_14])],[avatar_definition]) ).
fof(f905,plain,
( e20 = h2(e11)
| ~ spl28_14 ),
inference(avatar_component_clause,[],[f904]) ).
fof(f918,definition,
( spl28_17
<=> e21 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl28_17])],[avatar_definition]) ).
fof(f919,plain,
( e21 = h2(e13)
| ~ spl28_17 ),
inference(avatar_component_clause,[],[f918]) ).
fof(f920,plain,
( e21 != h2(e13)
| spl28_17 ),
inference(avatar_component_clause,[],[f918]) ).
fof(f928,definition,
( spl28_19
<=> e21 = h2(e11) ),
introduced(definition,[new_symbols(definition,[spl28_19])],[avatar_definition]) ).
fof(f929,plain,
( e21 = h2(e11)
| ~ spl28_19 ),
inference(avatar_component_clause,[],[f928]) ).
fof(f930,plain,
( e21 != h2(e11)
| spl28_19 ),
inference(avatar_component_clause,[],[f928]) ).
fof(f1034,definition,
( spl28_41
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl28_41])],[avatar_definition]) ).
fof(f1053,definition,
( spl28_45
<=> e20 = h5(e10) ),
introduced(definition,[new_symbols(definition,[spl28_45])],[avatar_definition]) ).
fof(f1054,plain,
( e20 = h5(e10)
| ~ spl28_45 ),
inference(avatar_component_clause,[],[f1053]) ).
fof(f1056,plain,
( ~ spl28_41
| ~ spl28_45 ),
inference(avatar_split_clause,[],[f404,f1053,f1034]) ).
fof(f1058,definition,
( spl28_46
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl28_46])],[avatar_definition]) ).
fof(f1072,definition,
( spl28_49
<=> e21 = h5(e11) ),
introduced(definition,[new_symbols(definition,[spl28_49])],[avatar_definition]) ).
fof(f1073,plain,
( e21 = h5(e11)
| ~ spl28_49 ),
inference(avatar_component_clause,[],[f1072]) ).
fof(f1075,plain,
( ~ spl28_46
| ~ spl28_49 ),
inference(avatar_split_clause,[],[f407,f1072,f1058]) ).
fof(f1086,definition,
( spl28_52
<=> e20 = h6(e13) ),
introduced(definition,[new_symbols(definition,[spl28_52])],[avatar_definition]) ).
fof(f1087,plain,
( e20 = h6(e13)
| ~ spl28_52 ),
inference(avatar_component_clause,[],[f1086]) ).
fof(f1088,plain,
( e20 != h6(e13)
| spl28_52 ),
inference(avatar_component_clause,[],[f1086]) ).
fof(f1096,definition,
( spl28_54
<=> e20 = h6(e11) ),
introduced(definition,[new_symbols(definition,[spl28_54])],[avatar_definition]) ).
fof(f1097,plain,
( e20 = h6(e11)
| ~ spl28_54 ),
inference(avatar_component_clause,[],[f1096]) ).
fof(f1098,plain,
( e20 != h6(e11)
| spl28_54 ),
inference(avatar_component_clause,[],[f1096]) ).
fof(f1120,definition,
( spl28_59
<=> e21 = h6(e11) ),
introduced(definition,[new_symbols(definition,[spl28_59])],[avatar_definition]) ).
fof(f1121,plain,
( e21 = h6(e11)
| ~ spl28_59 ),
inference(avatar_component_clause,[],[f1120]) ).
fof(f1374,definition,
( spl28_112
<=> e20 = h12(e13) ),
introduced(definition,[new_symbols(definition,[spl28_112])],[avatar_definition]) ).
fof(f1375,plain,
( e20 = h12(e13)
| ~ spl28_112 ),
inference(avatar_component_clause,[],[f1374]) ).
fof(f1376,plain,
( e20 != h12(e13)
| spl28_112 ),
inference(avatar_component_clause,[],[f1374]) ).
fof(f1594,definition,
( spl28_161
<=> e22 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl28_161])],[avatar_definition]) ).
fof(f1595,plain,
( e22 = h2(e13)
| ~ spl28_161 ),
inference(avatar_component_clause,[],[f1594]) ).
fof(f1866,definition,
( spl28_217
<=> h5(op1(e10,e10)) = op2(h5(e10),h5(e10)) ),
introduced(definition,[new_symbols(definition,[spl28_217])],[avatar_definition]) ).
fof(f1868,plain,
( h5(op1(e10,e10)) != op2(h5(e10),h5(e10))
| spl28_217 ),
inference(avatar_component_clause,[],[f1866]) ).
fof(f1870,definition,
( spl28_218
<=> h5(op1(e10,e11)) = op2(h5(e10),h5(e11)) ),
introduced(definition,[new_symbols(definition,[spl28_218])],[avatar_definition]) ).
fof(f1872,plain,
( h5(op1(e10,e11)) != op2(h5(e10),h5(e11))
| spl28_218 ),
inference(avatar_component_clause,[],[f1870]) ).
fof(f1874,definition,
( spl28_219
<=> h5(op1(e10,e12)) = op2(h5(e10),h5(e12)) ),
introduced(definition,[new_symbols(definition,[spl28_219])],[avatar_definition]) ).
fof(f1876,plain,
( h5(op1(e10,e12)) != op2(h5(e10),h5(e12))
| spl28_219 ),
inference(avatar_component_clause,[],[f1874]) ).
fof(f1878,definition,
( spl28_220
<=> h5(op1(e10,e13)) = op2(h5(e10),h5(e13)) ),
introduced(definition,[new_symbols(definition,[spl28_220])],[avatar_definition]) ).
fof(f1880,plain,
( h5(op1(e10,e13)) != op2(h5(e10),h5(e13))
| spl28_220 ),
inference(avatar_component_clause,[],[f1878]) ).
fof(f1882,definition,
( spl28_221
<=> h5(op1(e11,e10)) = op2(h5(e11),h5(e10)) ),
introduced(definition,[new_symbols(definition,[spl28_221])],[avatar_definition]) ).
fof(f1884,plain,
( h5(op1(e11,e10)) != op2(h5(e11),h5(e10))
| spl28_221 ),
inference(avatar_component_clause,[],[f1882]) ).
fof(f1886,definition,
( spl28_222
<=> h5(op1(e11,e11)) = op2(h5(e11),h5(e11)) ),
introduced(definition,[new_symbols(definition,[spl28_222])],[avatar_definition]) ).
fof(f1888,plain,
( h5(op1(e11,e11)) != op2(h5(e11),h5(e11))
| spl28_222 ),
inference(avatar_component_clause,[],[f1886]) ).
fof(f1890,definition,
( spl28_223
<=> h5(op1(e11,e12)) = op2(h5(e11),h5(e12)) ),
introduced(definition,[new_symbols(definition,[spl28_223])],[avatar_definition]) ).
fof(f1892,plain,
( h5(op1(e11,e12)) != op2(h5(e11),h5(e12))
| spl28_223 ),
inference(avatar_component_clause,[],[f1890]) ).
fof(f1894,definition,
( spl28_224
<=> h5(op1(e11,e13)) = op2(h5(e11),h5(e13)) ),
introduced(definition,[new_symbols(definition,[spl28_224])],[avatar_definition]) ).
fof(f1896,plain,
( h5(op1(e11,e13)) != op2(h5(e11),h5(e13))
| spl28_224 ),
inference(avatar_component_clause,[],[f1894]) ).
fof(f1898,definition,
( spl28_225
<=> h5(op1(e12,e10)) = op2(h5(e12),h5(e10)) ),
introduced(definition,[new_symbols(definition,[spl28_225])],[avatar_definition]) ).
fof(f1900,plain,
( h5(op1(e12,e10)) != op2(h5(e12),h5(e10))
| spl28_225 ),
inference(avatar_component_clause,[],[f1898]) ).
fof(f1902,definition,
( spl28_226
<=> h5(op1(e12,e11)) = op2(h5(e12),h5(e11)) ),
introduced(definition,[new_symbols(definition,[spl28_226])],[avatar_definition]) ).
fof(f1904,plain,
( h5(op1(e12,e11)) != op2(h5(e12),h5(e11))
| spl28_226 ),
inference(avatar_component_clause,[],[f1902]) ).
fof(f1906,definition,
( spl28_227
<=> h5(op1(e12,e12)) = op2(h5(e12),h5(e12)) ),
introduced(definition,[new_symbols(definition,[spl28_227])],[avatar_definition]) ).
fof(f1908,plain,
( h5(op1(e12,e12)) != op2(h5(e12),h5(e12))
| spl28_227 ),
inference(avatar_component_clause,[],[f1906]) ).
fof(f1910,definition,
( spl28_228
<=> h5(op1(e12,e13)) = op2(h5(e12),h5(e13)) ),
introduced(definition,[new_symbols(definition,[spl28_228])],[avatar_definition]) ).
fof(f1912,plain,
( h5(op1(e12,e13)) != op2(h5(e12),h5(e13))
| spl28_228 ),
inference(avatar_component_clause,[],[f1910]) ).
fof(f1914,definition,
( spl28_229
<=> h5(op1(e13,e10)) = op2(h5(e13),h5(e10)) ),
introduced(definition,[new_symbols(definition,[spl28_229])],[avatar_definition]) ).
fof(f1916,plain,
( h5(op1(e13,e10)) != op2(h5(e13),h5(e10))
| spl28_229 ),
inference(avatar_component_clause,[],[f1914]) ).
fof(f1918,definition,
( spl28_230
<=> h5(op1(e13,e11)) = op2(h5(e13),h5(e11)) ),
introduced(definition,[new_symbols(definition,[spl28_230])],[avatar_definition]) ).
fof(f1920,plain,
( h5(op1(e13,e11)) != op2(h5(e13),h5(e11))
| spl28_230 ),
inference(avatar_component_clause,[],[f1918]) ).
fof(f1922,definition,
( spl28_231
<=> h5(op1(e13,e12)) = op2(h5(e13),h5(e12)) ),
introduced(definition,[new_symbols(definition,[spl28_231])],[avatar_definition]) ).
fof(f1924,plain,
( h5(op1(e13,e12)) != op2(h5(e13),h5(e12))
| spl28_231 ),
inference(avatar_component_clause,[],[f1922]) ).
fof(f1926,definition,
( spl28_232
<=> h5(op1(e13,e13)) = op2(h5(e13),h5(e13)) ),
introduced(definition,[new_symbols(definition,[spl28_232])],[avatar_definition]) ).
fof(f1928,plain,
( h5(op1(e13,e13)) != op2(h5(e13),h5(e13))
| spl28_232 ),
inference(avatar_component_clause,[],[f1926]) ).
fof(f1930,definition,
( spl28_233
<=> e22 = h5(e13) ),
introduced(definition,[new_symbols(definition,[spl28_233])],[avatar_definition]) ).
fof(f1931,plain,
( e22 = h5(e13)
| ~ spl28_233 ),
inference(avatar_component_clause,[],[f1930]) ).
fof(f1962,definition,
( spl28_239
<=> e23 = h5(e12) ),
introduced(definition,[new_symbols(definition,[spl28_239])],[avatar_definition]) ).
fof(f1963,plain,
( e23 = h5(e12)
| ~ spl28_239 ),
inference(avatar_component_clause,[],[f1962]) ).
fof(f1965,plain,
( ~ spl28_217
| ~ spl28_218
| ~ spl28_219
| ~ spl28_220
| ~ spl28_221
| ~ spl28_222
| ~ spl28_223
| ~ spl28_224
| ~ spl28_225
| ~ spl28_226
| ~ spl28_227
| ~ spl28_228
| ~ spl28_229
| ~ spl28_230
| ~ spl28_231
| ~ spl28_232
| spl28_41
| spl28_46
| ~ spl28_233
| ~ spl28_239 ),
inference(avatar_split_clause,[],[f537,f1962,f1930,f1058,f1034,f1926,f1922,f1918,f1914,f1910,f1906,f1902,f1898,f1894,f1890,f1886,f1882,f1878,f1874,f1870,f1866]) ).
fof(f2082,definition,
( spl28_264
<=> e23 = h6(e13) ),
introduced(definition,[new_symbols(definition,[spl28_264])],[avatar_definition]) ).
fof(f2083,plain,
( e23 = h6(e13)
| ~ spl28_264 ),
inference(avatar_component_clause,[],[f2082]) ).
fof(f2714,definition,
( spl28_401
<=> e22 = h12(e13) ),
introduced(definition,[new_symbols(definition,[spl28_401])],[avatar_definition]) ).
fof(f2715,plain,
( e22 = h12(e13)
| ~ spl28_401 ),
inference(avatar_component_clause,[],[f2714]) ).
fof(f2761,plain,
spl28_401,
inference(avatar_split_clause,[],[f367,f2714]) ).
fof(f2773,plain,
spl28_264,
inference(avatar_split_clause,[],[f343,f2082]) ).
fof(f2774,plain,
spl28_59,
inference(avatar_split_clause,[],[f344,f1120]) ).
fof(f2775,plain,
spl28_233,
inference(avatar_split_clause,[],[f339,f1930]) ).
fof(f2776,plain,
spl28_49,
inference(avatar_split_clause,[],[f340,f1072]) ).
fof(f2781,plain,
spl28_161,
inference(avatar_split_clause,[],[f327,f1594]) ).
fof(f2782,plain,
spl28_14,
inference(avatar_split_clause,[],[f328,f904]) ).
fof(f2786,definition,
( spl28_409
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl28_409])],[avatar_definition]) ).
fof(f2790,definition,
( spl28_410
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl28_410])],[avatar_definition]) ).
fof(f2792,plain,
( e20 = op2(e23,e23)
| ~ spl28_410 ),
inference(avatar_component_clause,[],[f2790]) ).
fof(f2793,plain,
( ~ spl28_409
| spl28_410 ),
inference(avatar_split_clause,[],[f293,f2790,f2786]) ).
fof(f2795,definition,
( spl28_411
<=> e20 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl28_411])],[avatar_definition]) ).
fof(f2796,plain,
( e20 != op2(e22,e22)
| spl28_411 ),
inference(avatar_component_clause,[],[f2795]) ).
fof(f2797,plain,
( e20 = op2(e22,e22)
| ~ spl28_411 ),
inference(avatar_component_clause,[],[f2795]) ).
fof(f2798,plain,
( ~ spl28_409
| spl28_411 ),
inference(avatar_split_clause,[],[f294,f2795,f2786]) ).
fof(f2800,definition,
( spl28_412
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl28_412])],[avatar_definition]) ).
fof(f2802,plain,
( e20 = op2(e21,e21)
| ~ spl28_412 ),
inference(avatar_component_clause,[],[f2800]) ).
fof(f2805,definition,
( spl28_413
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl28_413])],[avatar_definition]) ).
fof(f2807,plain,
( e20 = op2(e20,e20)
| ~ spl28_413 ),
inference(avatar_component_clause,[],[f2805]) ).
fof(f2808,plain,
( ~ spl28_409
| spl28_413 ),
inference(avatar_split_clause,[],[f296,f2805,f2786]) ).
fof(f2810,definition,
( spl28_414
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl28_414])],[avatar_definition]) ).
fof(f2814,definition,
( spl28_415
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl28_415])],[avatar_definition]) ).
fof(f2815,plain,
( e21 != op2(e23,e23)
| spl28_415 ),
inference(avatar_component_clause,[],[f2814]) ).
fof(f2816,plain,
( e21 = op2(e23,e23)
| ~ spl28_415 ),
inference(avatar_component_clause,[],[f2814]) ).
fof(f2819,definition,
( spl28_416
<=> e21 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl28_416])],[avatar_definition]) ).
fof(f2821,plain,
( e21 = op2(e22,e22)
| ~ spl28_416 ),
inference(avatar_component_clause,[],[f2819]) ).
fof(f2824,definition,
( spl28_417
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl28_417])],[avatar_definition]) ).
fof(f2826,plain,
( e21 = op2(e21,e21)
| ~ spl28_417 ),
inference(avatar_component_clause,[],[f2824]) ).
fof(f2827,plain,
( spl28_414
| spl28_417 ),
inference(avatar_split_clause,[],[f694,f2824,f2810]) ).
fof(f2829,definition,
( spl28_418
<=> op2(e20,e20) = e21 ),
introduced(definition,[new_symbols(definition,[spl28_418])],[avatar_definition]) ).
fof(f2830,plain,
( op2(e20,e20) != e21
| spl28_418 ),
inference(avatar_component_clause,[],[f2829]) ).
fof(f2831,plain,
( op2(e20,e20) = e21
| ~ spl28_418 ),
inference(avatar_component_clause,[],[f2829]) ).
fof(f2834,definition,
( spl28_419
<=> e22 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl28_419])],[avatar_definition]) ).
fof(f2836,plain,
( e22 = op2(e23,e23)
| ~ spl28_419 ),
inference(avatar_component_clause,[],[f2834]) ).
fof(f2843,definition,
( spl28_421
<=> e22 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl28_421])],[avatar_definition]) ).
fof(f2844,plain,
( e22 != op2(e22,e22)
| spl28_421 ),
inference(avatar_component_clause,[],[f2843]) ).
fof(f2845,plain,
( e22 = op2(e22,e22)
| ~ spl28_421 ),
inference(avatar_component_clause,[],[f2843]) ).
fof(f2848,definition,
( spl28_422
<=> e22 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl28_422])],[avatar_definition]) ).
fof(f2850,plain,
( e22 = op2(e21,e21)
| ~ spl28_422 ),
inference(avatar_component_clause,[],[f2848]) ).
fof(f2858,definition,
( spl28_424
<=> e23 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl28_424])],[avatar_definition]) ).
fof(f2860,plain,
( e23 = op2(e21,e21)
| ~ spl28_424 ),
inference(avatar_component_clause,[],[f2858]) ).
fof(f2863,plain,
( spl28_409
| ~ spl28_414
| spl28_422
| spl28_424 ),
inference(avatar_split_clause,[],[f686,f2858,f2848,f2810,f2786]) ).
fof(f2866,definition,
( spl28_425
<=> e23 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl28_425])],[avatar_definition]) ).
fof(f2868,plain,
( e23 = op2(e22,e22)
| ~ spl28_425 ),
inference(avatar_component_clause,[],[f2866]) ).
fof(f2871,plain,
( spl28_409
| ~ spl28_414
| spl28_422
| spl28_425 ),
inference(avatar_split_clause,[],[f682,f2866,f2848,f2810,f2786]) ).
fof(f2874,definition,
( spl28_426
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl28_426])],[avatar_definition]) ).
fof(f2876,plain,
( e23 = op2(e23,e23)
| ~ spl28_426 ),
inference(avatar_component_clause,[],[f2874]) ).
fof(f2882,definition,
( spl28_427
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl28_427])],[avatar_definition]) ).
fof(f2886,definition,
( spl28_428
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl28_428])],[avatar_definition]) ).
fof(f2888,plain,
( e10 = op1(e13,e13)
| ~ spl28_428 ),
inference(avatar_component_clause,[],[f2886]) ).
fof(f2889,plain,
( spl28_427
| spl28_428 ),
inference(avatar_split_clause,[],[f676,f2886,f2882]) ).
fof(f2891,definition,
( spl28_429
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl28_429])],[avatar_definition]) ).
fof(f2893,plain,
( e10 = op1(e12,e12)
| ~ spl28_429 ),
inference(avatar_component_clause,[],[f2891]) ).
fof(f2894,plain,
( spl28_427
| spl28_429 ),
inference(avatar_split_clause,[],[f675,f2891,f2882]) ).
fof(f2896,definition,
( spl28_430
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl28_430])],[avatar_definition]) ).
fof(f2898,plain,
( e10 = op1(e11,e11)
| ~ spl28_430 ),
inference(avatar_component_clause,[],[f2896]) ).
fof(f2901,definition,
( spl28_431
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl28_431])],[avatar_definition]) ).
fof(f2903,plain,
( e10 = op1(e10,e10)
| ~ spl28_431 ),
inference(avatar_component_clause,[],[f2901]) ).
fof(f2904,plain,
( spl28_427
| spl28_431 ),
inference(avatar_split_clause,[],[f673,f2901,f2882]) ).
fof(f2906,definition,
( spl28_432
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl28_432])],[avatar_definition]) ).
fof(f2910,definition,
( spl28_433
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl28_433])],[avatar_definition]) ).
fof(f2912,plain,
( e11 = op1(e13,e13)
| ~ spl28_433 ),
inference(avatar_component_clause,[],[f2910]) ).
fof(f2915,definition,
( spl28_434
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl28_434])],[avatar_definition]) ).
fof(f2917,plain,
( e11 = op1(e12,e12)
| ~ spl28_434 ),
inference(avatar_component_clause,[],[f2915]) ).
fof(f2920,definition,
( spl28_435
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl28_435])],[avatar_definition]) ).
fof(f2921,plain,
( e11 != op1(e11,e11)
| spl28_435 ),
inference(avatar_component_clause,[],[f2920]) ).
fof(f2922,plain,
( e11 = op1(e11,e11)
| ~ spl28_435 ),
inference(avatar_component_clause,[],[f2920]) ).
fof(f2923,plain,
( ~ spl28_432
| spl28_435 ),
inference(avatar_split_clause,[],[f275,f2920,f2906]) ).
fof(f2930,definition,
( spl28_437
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl28_437])],[avatar_definition]) ).
fof(f2932,plain,
( e12 = op1(e13,e13)
| ~ spl28_437 ),
inference(avatar_component_clause,[],[f2930]) ).
fof(f2939,definition,
( spl28_439
<=> e12 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl28_439])],[avatar_definition]) ).
fof(f2941,plain,
( e12 = op1(e12,e12)
| ~ spl28_439 ),
inference(avatar_component_clause,[],[f2939]) ).
fof(f2944,definition,
( spl28_440
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl28_440])],[avatar_definition]) ).
fof(f2946,plain,
( e12 = op1(e11,e11)
| ~ spl28_440 ),
inference(avatar_component_clause,[],[f2944]) ).
fof(f2954,definition,
( spl28_442
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl28_442])],[avatar_definition]) ).
fof(f2956,plain,
( e13 = op1(e11,e11)
| ~ spl28_442 ),
inference(avatar_component_clause,[],[f2954]) ).
fof(f2959,plain,
( ~ spl28_427
| spl28_432
| spl28_440
| spl28_442 ),
inference(avatar_split_clause,[],[f666,f2954,f2944,f2906,f2882]) ).
fof(f2970,definition,
( spl28_444
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl28_444])],[avatar_definition]) ).
fof(f2972,plain,
( e13 = op1(e13,e13)
| ~ spl28_444 ),
inference(avatar_component_clause,[],[f2970]) ).
fof(f3004,definition,
( spl28_451
<=> e21 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl28_451])],[avatar_definition]) ).
fof(f3006,plain,
( e21 = op2(e20,e21)
| ~ spl28_451 ),
inference(avatar_component_clause,[],[f3004]) ).
fof(f3017,definition,
( spl28_454
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl28_454])],[avatar_definition]) ).
fof(f3019,plain,
( e21 = op2(e21,e20)
| ~ spl28_454 ),
inference(avatar_component_clause,[],[f3017]) ).
fof(f3021,definition,
( spl28_455
<=> e21 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl28_455])],[avatar_definition]) ).
fof(f3023,plain,
( e21 = op2(e22,e20)
| ~ spl28_455 ),
inference(avatar_component_clause,[],[f3021]) ).
fof(f3025,definition,
( spl28_456
<=> e21 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl28_456])],[avatar_definition]) ).
fof(f3027,plain,
( e21 = op2(e23,e20)
| ~ spl28_456 ),
inference(avatar_component_clause,[],[f3025]) ).
fof(f3034,definition,
( spl28_458
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl28_458])],[avatar_definition]) ).
fof(f3036,plain,
( e22 = op2(e20,e22)
| ~ spl28_458 ),
inference(avatar_component_clause,[],[f3034]) ).
fof(f3038,definition,
( spl28_459
<=> e22 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl28_459])],[avatar_definition]) ).
fof(f3040,plain,
( e22 = op2(e20,e23)
| ~ spl28_459 ),
inference(avatar_component_clause,[],[f3038]) ).
fof(f3047,definition,
( spl28_461
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl28_461])],[avatar_definition]) ).
fof(f3049,plain,
( e22 = op2(e22,e20)
| ~ spl28_461 ),
inference(avatar_component_clause,[],[f3047]) ).
fof(f3056,definition,
( spl28_463
<=> e23 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl28_463])],[avatar_definition]) ).
fof(f3058,plain,
( e23 = op2(e20,e21)
| ~ spl28_463 ),
inference(avatar_component_clause,[],[f3056]) ).
fof(f3060,definition,
( spl28_464
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl28_464])],[avatar_definition]) ).
fof(f3062,plain,
( e23 = op2(e20,e22)
| ~ spl28_464 ),
inference(avatar_component_clause,[],[f3060]) ).
fof(f3064,definition,
( spl28_465
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl28_465])],[avatar_definition]) ).
fof(f3066,plain,
( e23 = op2(e20,e23)
| ~ spl28_465 ),
inference(avatar_component_clause,[],[f3064]) ).
fof(f3077,definition,
( spl28_468
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl28_468])],[avatar_definition]) ).
fof(f3079,plain,
( e23 = op2(e23,e20)
| ~ spl28_468 ),
inference(avatar_component_clause,[],[f3077]) ).
fof(f3109,definition,
( spl28_475
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl28_475])],[avatar_definition]) ).
fof(f3111,plain,
( e21 = op2(e22,e21)
| ~ spl28_475 ),
inference(avatar_component_clause,[],[f3109]) ).
fof(f3113,definition,
( spl28_476
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl28_476])],[avatar_definition]) ).
fof(f3115,plain,
( e21 = op2(e23,e21)
| ~ spl28_476 ),
inference(avatar_component_clause,[],[f3113]) ).
fof(f3122,definition,
( spl28_478
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl28_478])],[avatar_definition]) ).
fof(f3124,plain,
( e22 = op2(e21,e23)
| ~ spl28_478 ),
inference(avatar_component_clause,[],[f3122]) ).
fof(f3131,definition,
( spl28_480
<=> e22 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl28_480])],[avatar_definition]) ).
fof(f3133,plain,
( e22 = op2(e23,e21)
| ~ spl28_480 ),
inference(avatar_component_clause,[],[f3131]) ).
fof(f3136,definition,
( spl28_481
<=> e23 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl28_481])],[avatar_definition]) ).
fof(f3138,plain,
( e23 = op2(e21,e22)
| ~ spl28_481 ),
inference(avatar_component_clause,[],[f3136]) ).
fof(f3145,definition,
( spl28_483
<=> e23 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl28_483])],[avatar_definition]) ).
fof(f3147,plain,
( e23 = op2(e22,e21)
| ~ spl28_483 ),
inference(avatar_component_clause,[],[f3145]) ).
fof(f3149,definition,
( spl28_484
<=> e23 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl28_484])],[avatar_definition]) ).
fof(f3151,plain,
( e23 = op2(e23,e21)
| ~ spl28_484 ),
inference(avatar_component_clause,[],[f3149]) ).
fof(f3152,plain,
( spl28_463
| spl28_424
| spl28_483
| spl28_484 ),
inference(avatar_split_clause,[],[f128,f3149,f3145,f2858,f3056]) ).
fof(f3164,definition,
( spl28_487
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl28_487])],[avatar_definition]) ).
fof(f3166,plain,
( e21 = op2(e22,e23)
| ~ spl28_487 ),
inference(avatar_component_clause,[],[f3164]) ).
fof(f3167,plain,
( spl28_455
| spl28_475
| spl28_416
| spl28_487 ),
inference(avatar_split_clause,[],[f131,f3164,f2819,f3109,f3021]) ).
fof(f3169,definition,
( spl28_488
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl28_488])],[avatar_definition]) ).
fof(f3171,plain,
( e21 = op2(e23,e22)
| ~ spl28_488 ),
inference(avatar_component_clause,[],[f3169]) ).
fof(f3174,definition,
( spl28_489
<=> e22 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl28_489])],[avatar_definition]) ).
fof(f3176,plain,
( e22 = op2(e22,e23)
| ~ spl28_489 ),
inference(avatar_component_clause,[],[f3174]) ).
fof(f3189,definition,
( spl28_492
<=> e23 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl28_492])],[avatar_definition]) ).
fof(f3191,plain,
( e23 = op2(e23,e22)
| ~ spl28_492 ),
inference(avatar_component_clause,[],[f3189]) ).
fof(f3192,plain,
( spl28_464
| spl28_481
| spl28_425
| spl28_492 ),
inference(avatar_split_clause,[],[f136,f3189,f2866,f3136,f3060]) ).
fof(f3195,plain,
( spl28_456
| spl28_476
| spl28_488
| spl28_415 ),
inference(avatar_split_clause,[],[f139,f2814,f3169,f3113,f3025]) ).
fof(f3198,plain,
( spl28_459
| spl28_478
| spl28_489
| spl28_419 ),
inference(avatar_split_clause,[],[f142,f2834,f3174,f3122,f3038]) ).
fof(f3202,definition,
( spl28_493
<=> e20 = unit2 ),
introduced(definition,[new_symbols(definition,[spl28_493])],[avatar_definition]) ).
fof(f3203,plain,
( e20 != unit2
| spl28_493 ),
inference(avatar_component_clause,[],[f3202]) ).
fof(f3204,plain,
( e20 = unit2
| ~ spl28_493 ),
inference(avatar_component_clause,[],[f3202]) ).
fof(f3206,definition,
( spl28_494
<=> e21 = unit2 ),
introduced(definition,[new_symbols(definition,[spl28_494])],[avatar_definition]) ).
fof(f3208,plain,
( e21 = unit2
| ~ spl28_494 ),
inference(avatar_component_clause,[],[f3206]) ).
fof(f3210,definition,
( spl28_495
<=> e22 = unit2 ),
introduced(definition,[new_symbols(definition,[spl28_495])],[avatar_definition]) ).
fof(f3212,plain,
( e22 = unit2
| ~ spl28_495 ),
inference(avatar_component_clause,[],[f3210]) ).
fof(f3214,definition,
( spl28_496
<=> e23 = unit2 ),
introduced(definition,[new_symbols(definition,[spl28_496])],[avatar_definition]) ).
fof(f3216,plain,
( e23 = unit2
| ~ spl28_496 ),
inference(avatar_component_clause,[],[f3214]) ).
fof(f3217,plain,
( spl28_493
| spl28_494
| spl28_495
| spl28_496 ),
inference(avatar_split_clause,[],[f104,f3214,f3210,f3206,f3202]) ).
fof(f3261,definition,
( spl28_503
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl28_503])],[avatar_definition]) ).
fof(f3263,plain,
( e11 = op1(e10,e11)
| ~ spl28_503 ),
inference(avatar_component_clause,[],[f3261]) ).
fof(f3274,definition,
( spl28_506
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl28_506])],[avatar_definition]) ).
fof(f3276,plain,
( e11 = op1(e11,e10)
| ~ spl28_506 ),
inference(avatar_component_clause,[],[f3274]) ).
fof(f3278,definition,
( spl28_507
<=> e11 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl28_507])],[avatar_definition]) ).
fof(f3280,plain,
( e11 = op1(e12,e10)
| ~ spl28_507 ),
inference(avatar_component_clause,[],[f3278]) ).
fof(f3282,definition,
( spl28_508
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl28_508])],[avatar_definition]) ).
fof(f3284,plain,
( e11 = op1(e13,e10)
| ~ spl28_508 ),
inference(avatar_component_clause,[],[f3282]) ).
fof(f3291,definition,
( spl28_510
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl28_510])],[avatar_definition]) ).
fof(f3293,plain,
( e12 = op1(e10,e12)
| ~ spl28_510 ),
inference(avatar_component_clause,[],[f3291]) ).
fof(f3295,definition,
( spl28_511
<=> e12 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl28_511])],[avatar_definition]) ).
fof(f3297,plain,
( e12 = op1(e10,e13)
| ~ spl28_511 ),
inference(avatar_component_clause,[],[f3295]) ).
fof(f3304,definition,
( spl28_513
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl28_513])],[avatar_definition]) ).
fof(f3306,plain,
( e12 = op1(e12,e10)
| ~ spl28_513 ),
inference(avatar_component_clause,[],[f3304]) ).
fof(f3313,definition,
( spl28_515
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl28_515])],[avatar_definition]) ).
fof(f3315,plain,
( e13 = op1(e10,e11)
| ~ spl28_515 ),
inference(avatar_component_clause,[],[f3313]) ).
fof(f3321,definition,
( spl28_517
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl28_517])],[avatar_definition]) ).
fof(f3323,plain,
( e13 = op1(e10,e13)
| ~ spl28_517 ),
inference(avatar_component_clause,[],[f3321]) ).
fof(f3326,definition,
( spl28_518
<=> e13 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl28_518])],[avatar_definition]) ).
fof(f3328,plain,
( e13 = op1(e11,e10)
| ~ spl28_518 ),
inference(avatar_component_clause,[],[f3326]) ).
fof(f3334,definition,
( spl28_520
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl28_520])],[avatar_definition]) ).
fof(f3336,plain,
( e13 = op1(e13,e10)
| ~ spl28_520 ),
inference(avatar_component_clause,[],[f3334]) ).
fof(f3366,definition,
( spl28_527
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl28_527])],[avatar_definition]) ).
fof(f3368,plain,
( e11 = op1(e12,e11)
| ~ spl28_527 ),
inference(avatar_component_clause,[],[f3366]) ).
fof(f3370,definition,
( spl28_528
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl28_528])],[avatar_definition]) ).
fof(f3372,plain,
( e11 = op1(e13,e11)
| ~ spl28_528 ),
inference(avatar_component_clause,[],[f3370]) ).
fof(f3379,definition,
( spl28_530
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl28_530])],[avatar_definition]) ).
fof(f3381,plain,
( e12 = op1(e11,e13)
| ~ spl28_530 ),
inference(avatar_component_clause,[],[f3379]) ).
fof(f3388,definition,
( spl28_532
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl28_532])],[avatar_definition]) ).
fof(f3390,plain,
( e12 = op1(e13,e11)
| ~ spl28_532 ),
inference(avatar_component_clause,[],[f3388]) ).
fof(f3393,definition,
( spl28_533
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl28_533])],[avatar_definition]) ).
fof(f3395,plain,
( e13 = op1(e11,e12)
| ~ spl28_533 ),
inference(avatar_component_clause,[],[f3393]) ).
fof(f3397,definition,
( spl28_534
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl28_534])],[avatar_definition]) ).
fof(f3399,plain,
( e13 = op1(e11,e13)
| ~ spl28_534 ),
inference(avatar_component_clause,[],[f3397]) ).
fof(f3400,plain,
( spl28_518
| spl28_442
| spl28_533
| spl28_534 ),
inference(avatar_split_clause,[],[f70,f3397,f3393,f2954,f3326]) ).
fof(f3402,definition,
( spl28_535
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl28_535])],[avatar_definition]) ).
fof(f3404,plain,
( e13 = op1(e12,e11)
| ~ spl28_535 ),
inference(avatar_component_clause,[],[f3402]) ).
fof(f3406,definition,
( spl28_536
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl28_536])],[avatar_definition]) ).
fof(f3408,plain,
( e13 = op1(e13,e11)
| ~ spl28_536 ),
inference(avatar_component_clause,[],[f3406]) ).
fof(f3409,plain,
( spl28_515
| spl28_442
| spl28_535
| spl28_536 ),
inference(avatar_split_clause,[],[f71,f3406,f3402,f2954,f3313]) ).
fof(f3421,definition,
( spl28_539
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl28_539])],[avatar_definition]) ).
fof(f3423,plain,
( e11 = op1(e12,e13)
| ~ spl28_539 ),
inference(avatar_component_clause,[],[f3421]) ).
fof(f3424,plain,
( spl28_507
| spl28_527
| spl28_434
| spl28_539 ),
inference(avatar_split_clause,[],[f74,f3421,f2915,f3366,f3278]) ).
fof(f3426,definition,
( spl28_540
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl28_540])],[avatar_definition]) ).
fof(f3428,plain,
( e11 = op1(e13,e12)
| ~ spl28_540 ),
inference(avatar_component_clause,[],[f3426]) ).
fof(f3431,definition,
( spl28_541
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl28_541])],[avatar_definition]) ).
fof(f3433,plain,
( e12 = op1(e12,e13)
| ~ spl28_541 ),
inference(avatar_component_clause,[],[f3431]) ).
fof(f3452,plain,
( spl28_508
| spl28_528
| spl28_540
| spl28_433 ),
inference(avatar_split_clause,[],[f82,f2910,f3426,f3370,f3282]) ).
fof(f3455,plain,
( spl28_511
| spl28_530
| spl28_541
| spl28_437 ),
inference(avatar_split_clause,[],[f85,f2930,f3431,f3379,f3295]) ).
fof(f3459,definition,
( spl28_545
<=> e10 = unit1 ),
introduced(definition,[new_symbols(definition,[spl28_545])],[avatar_definition]) ).
fof(f3461,plain,
( e10 = unit1
| ~ spl28_545 ),
inference(avatar_component_clause,[],[f3459]) ).
fof(f3463,definition,
( spl28_546
<=> e11 = unit1 ),
introduced(definition,[new_symbols(definition,[spl28_546])],[avatar_definition]) ).
fof(f3465,plain,
( e11 = unit1
| ~ spl28_546 ),
inference(avatar_component_clause,[],[f3463]) ).
fof(f3467,definition,
( spl28_547
<=> e12 = unit1 ),
introduced(definition,[new_symbols(definition,[spl28_547])],[avatar_definition]) ).
fof(f3469,plain,
( e12 = unit1
| ~ spl28_547 ),
inference(avatar_component_clause,[],[f3467]) ).
fof(f3471,definition,
( spl28_548
<=> e13 = unit1 ),
introduced(definition,[new_symbols(definition,[spl28_548])],[avatar_definition]) ).
fof(f3473,plain,
( e13 = unit1
| ~ spl28_548 ),
inference(avatar_component_clause,[],[f3471]) ).
fof(f3474,plain,
( spl28_545
| spl28_546
| spl28_547
| spl28_548 ),
inference(avatar_split_clause,[],[f47,f3471,f3467,f3463,f3459]) ).
fof(f3491,plain,
( e20 != e21
| ~ spl28_14
| spl28_19 ),
inference(superposition,[],[f930,f905]) ).
fof(f3492,plain,
( e20 != e21
| spl28_54
| ~ spl28_59 ),
inference(superposition,[],[f1098,f1121]) ).
fof(f3497,plain,
( e20 != e22
| spl28_112
| ~ spl28_401 ),
inference(superposition,[],[f1376,f2715]) ).
fof(f3501,plain,
( e13 = op1(e13,e10)
| ~ spl28_545 ),
inference(forward_demodulation,[],[f48,f3461]) ).
fof(f3502,plain,
( spl28_520
| ~ spl28_545 ),
inference(avatar_split_clause,[],[f3501,f3459,f3334]) ).
fof(f3503,plain,
( e13 = op1(e10,e13)
| ~ spl28_545 ),
inference(forward_demodulation,[],[f49,f3461]) ).
fof(f3504,plain,
( spl28_517
| ~ spl28_545 ),
inference(avatar_split_clause,[],[f3503,f3459,f3321]) ).
fof(f3505,plain,
( e12 = op1(e12,e10)
| ~ spl28_545 ),
inference(forward_demodulation,[],[f50,f3461]) ).
fof(f3506,plain,
( spl28_513
| ~ spl28_545 ),
inference(avatar_split_clause,[],[f3505,f3459,f3304]) ).
fof(f3507,plain,
( e12 = op1(e10,e12)
| ~ spl28_545 ),
inference(forward_demodulation,[],[f51,f3461]) ).
fof(f3508,plain,
( spl28_510
| ~ spl28_545 ),
inference(avatar_split_clause,[],[f3507,f3459,f3291]) ).
fof(f3509,plain,
( e11 = op1(e11,e10)
| ~ spl28_545 ),
inference(forward_demodulation,[],[f52,f3461]) ).
fof(f3510,plain,
( spl28_506
| ~ spl28_545 ),
inference(avatar_split_clause,[],[f3509,f3459,f3274]) ).
fof(f3511,plain,
( e11 = op1(e10,e11)
| ~ spl28_545 ),
inference(forward_demodulation,[],[f53,f3461]) ).
fof(f3512,plain,
( spl28_503
| ~ spl28_545 ),
inference(avatar_split_clause,[],[f3511,f3459,f3261]) ).
fof(f3516,plain,
( e23 = op2(e23,e20)
| ~ spl28_493 ),
inference(forward_demodulation,[],[f105,f3204]) ).
fof(f3517,plain,
( spl28_468
| ~ spl28_493 ),
inference(avatar_split_clause,[],[f3516,f3202,f3077]) ).
fof(f3518,plain,
( e23 = op2(e20,e23)
| ~ spl28_493 ),
inference(forward_demodulation,[],[f106,f3204]) ).
fof(f3519,plain,
( spl28_465
| ~ spl28_493 ),
inference(avatar_split_clause,[],[f3518,f3202,f3064]) ).
fof(f3520,plain,
( e22 = op2(e22,e20)
| ~ spl28_493 ),
inference(forward_demodulation,[],[f107,f3204]) ).
fof(f3521,plain,
( spl28_461
| ~ spl28_493 ),
inference(avatar_split_clause,[],[f3520,f3202,f3047]) ).
fof(f3522,plain,
( e22 = op2(e20,e22)
| ~ spl28_493 ),
inference(forward_demodulation,[],[f108,f3204]) ).
fof(f3523,plain,
( spl28_458
| ~ spl28_493 ),
inference(avatar_split_clause,[],[f3522,f3202,f3034]) ).
fof(f3524,plain,
( e21 = op2(e21,e20)
| ~ spl28_493 ),
inference(forward_demodulation,[],[f109,f3204]) ).
fof(f3525,plain,
( spl28_454
| ~ spl28_493 ),
inference(avatar_split_clause,[],[f3524,f3202,f3017]) ).
fof(f3526,plain,
( e21 = op2(e20,e21)
| ~ spl28_493 ),
inference(forward_demodulation,[],[f110,f3204]) ).
fof(f3527,plain,
( spl28_451
| ~ spl28_493 ),
inference(avatar_split_clause,[],[f3526,f3202,f3004]) ).
fof(f3528,plain,
( e20 = op2(e20,e20)
| ~ spl28_493 ),
inference(forward_demodulation,[],[f111,f3204]) ).
fof(f3529,plain,
( spl28_413
| ~ spl28_493 ),
inference(avatar_split_clause,[],[f3528,f3202,f2805]) ).
fof(f3531,plain,
spl28_532,
inference(avatar_split_clause,[],[f317,f3388]) ).
fof(f3532,plain,
spl28_430,
inference(avatar_split_clause,[],[f318,f2896]) ).
fof(f3533,plain,
spl28_480,
inference(avatar_split_clause,[],[f319,f3131]) ).
fof(f3534,plain,
spl28_412,
inference(avatar_split_clause,[],[f320,f2800]) ).
fof(f3535,plain,
( e20 = e21
| ~ spl28_412
| ~ spl28_417 ),
inference(superposition,[],[f2826,f2802]) ).
fof(f3539,plain,
( $false
| ~ spl28_14
| spl28_19
| ~ spl28_412
| ~ spl28_417 ),
inference(forward_subsumption_resolution,[],[f3535,f3491]) ).
fof(f3540,plain,
( ~ spl28_14
| spl28_19
| ~ spl28_412
| ~ spl28_417 ),
inference(avatar_contradiction_clause,[],[f3539]) ).
fof(f3542,plain,
( e20 = e21
| ~ spl28_14
| ~ spl28_19 ),
inference(superposition,[],[f929,f905]) ).
fof(f3544,plain,
( e20 = e21
| ~ spl28_413
| ~ spl28_418 ),
inference(superposition,[],[f2831,f2807]) ).
fof(f3548,plain,
( $false
| spl28_54
| ~ spl28_59
| ~ spl28_413
| ~ spl28_418 ),
inference(forward_subsumption_resolution,[],[f3544,f3492]) ).
fof(f3549,plain,
( spl28_54
| ~ spl28_59
| ~ spl28_413
| ~ spl28_418 ),
inference(avatar_contradiction_clause,[],[f3548]) ).
fof(f3550,plain,
( e20 = e21
| ~ spl28_54
| ~ spl28_59 ),
inference(forward_demodulation,[],[f1097,f1121]) ).
fof(f3560,plain,
( $false
| ~ spl28_54
| ~ spl28_59 ),
inference(forward_subsumption_resolution,[],[f252,f3550]) ).
fof(f3561,plain,
( ~ spl28_54
| ~ spl28_59 ),
inference(avatar_contradiction_clause,[],[f3560]) ).
fof(f3562,plain,
( e20 != e21
| spl28_54
| ~ spl28_59 ),
inference(forward_demodulation,[],[f1098,f1121]) ).
fof(f3570,plain,
( e21 = e22
| ~ spl28_17
| ~ spl28_161 ),
inference(forward_demodulation,[],[f919,f1595]) ).
fof(f3591,plain,
( $false
| ~ spl28_17
| ~ spl28_161 ),
inference(forward_subsumption_resolution,[],[f249,f3570]) ).
fof(f3592,plain,
( ~ spl28_17
| ~ spl28_161 ),
inference(avatar_contradiction_clause,[],[f3591]) ).
fof(f3593,plain,
( e21 != e22
| spl28_17
| ~ spl28_161 ),
inference(forward_demodulation,[],[f920,f1595]) ).
fof(f3597,plain,
( $false
| ~ spl28_14
| ~ spl28_19
| spl28_54
| ~ spl28_59 ),
inference(forward_subsumption_resolution,[],[f3542,f3562]) ).
fof(f3598,plain,
( ~ spl28_14
| ~ spl28_19
| spl28_54
| ~ spl28_59 ),
inference(avatar_contradiction_clause,[],[f3597]) ).
fof(f3607,plain,
( e20 = e23
| ~ spl28_52
| ~ spl28_264 ),
inference(forward_demodulation,[],[f1087,f2083]) ).
fof(f3613,plain,
( e21 != op2(e23,e23)
| ~ spl28_52
| ~ spl28_264
| spl28_418 ),
inference(superposition,[],[f2830,f3607]) ).
fof(f3624,plain,
( e20 != e23
| spl28_52
| ~ spl28_264 ),
inference(forward_demodulation,[],[f1088,f2083]) ).
fof(f3625,plain,
( e20 = e22
| ~ spl28_410
| ~ spl28_419 ),
inference(forward_demodulation,[],[f2792,f2836]) ).
fof(f3626,plain,
( $false
| spl28_112
| ~ spl28_401
| ~ spl28_410
| ~ spl28_419 ),
inference(forward_subsumption_resolution,[],[f3625,f3497]) ).
fof(f3627,plain,
( spl28_112
| ~ spl28_401
| ~ spl28_410
| ~ spl28_419 ),
inference(avatar_contradiction_clause,[],[f3626]) ).
fof(f3628,plain,
( e20 = e22
| ~ spl28_112
| ~ spl28_401 ),
inference(forward_demodulation,[],[f1375,f2715]) ).
fof(f3638,plain,
( $false
| ~ spl28_112
| ~ spl28_401 ),
inference(forward_subsumption_resolution,[],[f251,f3628]) ).
fof(f3639,plain,
( ~ spl28_112
| ~ spl28_401 ),
inference(avatar_contradiction_clause,[],[f3638]) ).
fof(f3640,plain,
( e20 != e22
| spl28_112
| ~ spl28_401 ),
inference(forward_demodulation,[],[f1376,f2715]) ).
fof(f3644,plain,
( e20 = e22
| ~ spl28_411
| ~ spl28_421 ),
inference(superposition,[],[f2845,f2797]) ).
fof(f3649,plain,
( $false
| spl28_112
| ~ spl28_401
| ~ spl28_411
| ~ spl28_421 ),
inference(forward_subsumption_resolution,[],[f3644,f3640]) ).
fof(f3650,plain,
( spl28_112
| ~ spl28_401
| ~ spl28_411
| ~ spl28_421 ),
inference(avatar_contradiction_clause,[],[f3649]) ).
fof(f3652,plain,
( e20 = e22
| ~ spl28_412
| ~ spl28_422 ),
inference(superposition,[],[f2850,f2802]) ).
fof(f3657,plain,
( $false
| spl28_112
| ~ spl28_401
| ~ spl28_412
| ~ spl28_422 ),
inference(forward_subsumption_resolution,[],[f3652,f3640]) ).
fof(f3658,plain,
( spl28_112
| ~ spl28_401
| ~ spl28_412
| ~ spl28_422 ),
inference(avatar_contradiction_clause,[],[f3657]) ).
fof(f3669,plain,
( e20 = e23
| ~ spl28_412
| ~ spl28_424 ),
inference(superposition,[],[f2860,f2802]) ).
fof(f3675,plain,
( $false
| spl28_52
| ~ spl28_264
| ~ spl28_412
| ~ spl28_424 ),
inference(forward_subsumption_resolution,[],[f3669,f3624]) ).
fof(f3676,plain,
( spl28_52
| ~ spl28_264
| ~ spl28_412
| ~ spl28_424 ),
inference(avatar_contradiction_clause,[],[f3675]) ).
fof(f3692,plain,
( e20 = e23
| ~ spl28_411
| ~ spl28_425 ),
inference(superposition,[],[f2868,f2797]) ).
fof(f3698,plain,
( $false
| spl28_52
| ~ spl28_264
| ~ spl28_411
| ~ spl28_425 ),
inference(forward_subsumption_resolution,[],[f3692,f3624]) ).
fof(f3699,plain,
( spl28_52
| ~ spl28_264
| ~ spl28_411
| ~ spl28_425 ),
inference(avatar_contradiction_clause,[],[f3698]) ).
fof(f3701,plain,
( e20 = e23
| ~ spl28_410
| ~ spl28_426 ),
inference(superposition,[],[f2876,f2792]) ).
fof(f3707,plain,
( $false
| spl28_52
| ~ spl28_264
| ~ spl28_410
| ~ spl28_426 ),
inference(forward_subsumption_resolution,[],[f3701,f3624]) ).
fof(f3708,plain,
( spl28_52
| ~ spl28_264
| ~ spl28_410
| ~ spl28_426 ),
inference(avatar_contradiction_clause,[],[f3707]) ).
fof(f3710,plain,
( e10 = e11
| ~ spl28_430
| ~ spl28_435 ),
inference(superposition,[],[f2922,f2898]) ).
fof(f3714,plain,
( $false
| ~ spl28_430
| ~ spl28_435 ),
inference(forward_subsumption_resolution,[],[f3710,f246]) ).
fof(f3715,plain,
( ~ spl28_430
| ~ spl28_435 ),
inference(avatar_contradiction_clause,[],[f3714]) ).
fof(f3725,plain,
( e13 = op1(e13,e13)
| ~ spl28_548 ),
inference(forward_demodulation,[],[f48,f3473]) ).
fof(f3726,plain,
( spl28_444
| ~ spl28_548 ),
inference(avatar_split_clause,[],[f3725,f3471,f2970]) ).
fof(f3741,plain,
( e12 = op1(e12,e12)
| ~ spl28_547 ),
inference(forward_demodulation,[],[f50,f3469]) ).
fof(f3742,plain,
( spl28_439
| ~ spl28_547 ),
inference(avatar_split_clause,[],[f3741,f3467,f2939]) ).
fof(f3779,plain,
( e10 = e12
| ~ spl28_428
| ~ spl28_437 ),
inference(forward_demodulation,[],[f2888,f2932]) ).
fof(f3780,plain,
( e10 = e11
| ~ spl28_429
| ~ spl28_434 ),
inference(forward_demodulation,[],[f2893,f2917]) ).
fof(f3781,plain,
( $false
| ~ spl28_428
| ~ spl28_437 ),
inference(forward_subsumption_resolution,[],[f3779,f245]) ).
fof(f3782,plain,
( ~ spl28_428
| ~ spl28_437 ),
inference(avatar_contradiction_clause,[],[f3781]) ).
fof(f3783,plain,
( $false
| ~ spl28_429
| ~ spl28_434 ),
inference(forward_subsumption_resolution,[],[f3780,f246]) ).
fof(f3784,plain,
( ~ spl28_429
| ~ spl28_434 ),
inference(avatar_contradiction_clause,[],[f3783]) ).
fof(f3787,plain,
( e10 = e12
| ~ spl28_429
| ~ spl28_439 ),
inference(superposition,[],[f2941,f2893]) ).
fof(f3792,plain,
( $false
| ~ spl28_429
| ~ spl28_439 ),
inference(forward_subsumption_resolution,[],[f3787,f245]) ).
fof(f3793,plain,
( ~ spl28_429
| ~ spl28_439 ),
inference(avatar_contradiction_clause,[],[f3792]) ).
fof(f3795,plain,
( e10 = e12
| ~ spl28_430
| ~ spl28_440 ),
inference(superposition,[],[f2946,f2898]) ).
fof(f3800,plain,
( $false
| ~ spl28_430
| ~ spl28_440 ),
inference(forward_subsumption_resolution,[],[f3795,f245]) ).
fof(f3801,plain,
( ~ spl28_430
| ~ spl28_440 ),
inference(avatar_contradiction_clause,[],[f3800]) ).
fof(f3816,plain,
( e10 = e13
| ~ spl28_430
| ~ spl28_442 ),
inference(superposition,[],[f2956,f2898]) ).
fof(f3822,plain,
( $false
| ~ spl28_430
| ~ spl28_442 ),
inference(forward_subsumption_resolution,[],[f3816,f244]) ).
fof(f3823,plain,
( ~ spl28_430
| ~ spl28_442 ),
inference(avatar_contradiction_clause,[],[f3822]) ).
fof(f3834,plain,
( e10 = e13
| ~ spl28_428
| ~ spl28_444 ),
inference(superposition,[],[f2972,f2888]) ).
fof(f3840,plain,
( $false
| ~ spl28_428
| ~ spl28_444 ),
inference(forward_subsumption_resolution,[],[f3834,f244]) ).
fof(f3841,plain,
( ~ spl28_428
| ~ spl28_444 ),
inference(avatar_contradiction_clause,[],[f3840]) ).
fof(f3893,plain,
( e20 = e21
| ~ spl28_411
| ~ spl28_416 ),
inference(superposition,[],[f2821,f2797]) ).
fof(f3899,plain,
( $false
| spl28_54
| ~ spl28_59
| ~ spl28_411
| ~ spl28_416 ),
inference(forward_subsumption_resolution,[],[f3893,f3562]) ).
fof(f3900,plain,
( spl28_54
| ~ spl28_59
| ~ spl28_411
| ~ spl28_416 ),
inference(avatar_contradiction_clause,[],[f3899]) ).
fof(f3910,plain,
( e20 = e21
| ~ spl28_410
| ~ spl28_415 ),
inference(superposition,[],[f2816,f2792]) ).
fof(f3916,plain,
( $false
| spl28_54
| ~ spl28_59
| ~ spl28_410
| ~ spl28_415 ),
inference(forward_subsumption_resolution,[],[f3910,f3562]) ).
fof(f3917,plain,
( spl28_54
| ~ spl28_59
| ~ spl28_410
| ~ spl28_415 ),
inference(avatar_contradiction_clause,[],[f3916]) ).
fof(f3926,plain,
( e21 = e22
| ~ spl28_455
| ~ spl28_461 ),
inference(superposition,[],[f3049,f3023]) ).
fof(f3930,plain,
( $false
| spl28_17
| ~ spl28_161
| ~ spl28_455
| ~ spl28_461 ),
inference(forward_subsumption_resolution,[],[f3926,f3593]) ).
fof(f3931,plain,
( spl28_17
| ~ spl28_161
| ~ spl28_455
| ~ spl28_461 ),
inference(avatar_contradiction_clause,[],[f3930]) ).
fof(f3934,plain,
( e21 = e23
| ~ spl28_451
| ~ spl28_463 ),
inference(superposition,[],[f3058,f3006]) ).
fof(f3938,plain,
( $false
| ~ spl28_451
| ~ spl28_463 ),
inference(forward_subsumption_resolution,[],[f3934,f248]) ).
fof(f3939,plain,
( ~ spl28_451
| ~ spl28_463 ),
inference(avatar_contradiction_clause,[],[f3938]) ).
fof(f3941,plain,
( e22 = e23
| ~ spl28_458
| ~ spl28_464 ),
inference(forward_demodulation,[],[f3062,f3036]) ).
fof(f3942,plain,
( $false
| ~ spl28_458
| ~ spl28_464 ),
inference(forward_subsumption_resolution,[],[f3941,f247]) ).
fof(f3943,plain,
( ~ spl28_458
| ~ spl28_464 ),
inference(avatar_contradiction_clause,[],[f3942]) ).
fof(f3945,plain,
( e22 = e23
| ~ spl28_459
| ~ spl28_465 ),
inference(forward_demodulation,[],[f3066,f3040]) ).
fof(f3946,plain,
( $false
| ~ spl28_459
| ~ spl28_465 ),
inference(forward_subsumption_resolution,[],[f3945,f247]) ).
fof(f3947,plain,
( ~ spl28_459
| ~ spl28_465 ),
inference(avatar_contradiction_clause,[],[f3946]) ).
fof(f3963,plain,
( e21 = e23
| ~ spl28_456
| ~ spl28_468 ),
inference(superposition,[],[f3079,f3027]) ).
fof(f3967,plain,
( $false
| ~ spl28_456
| ~ spl28_468 ),
inference(forward_subsumption_resolution,[],[f3963,f248]) ).
fof(f3968,plain,
( ~ spl28_456
| ~ spl28_468 ),
inference(avatar_contradiction_clause,[],[f3967]) ).
fof(f4018,plain,
( e21 = e22
| ~ spl28_476
| ~ spl28_480 ),
inference(superposition,[],[f3133,f3115]) ).
fof(f4022,plain,
( $false
| spl28_17
| ~ spl28_161
| ~ spl28_476
| ~ spl28_480 ),
inference(forward_subsumption_resolution,[],[f4018,f3593]) ).
fof(f4023,plain,
( spl28_17
| ~ spl28_161
| ~ spl28_476
| ~ spl28_480 ),
inference(avatar_contradiction_clause,[],[f4022]) ).
fof(f4035,plain,
( e21 = e23
| ~ spl28_475
| ~ spl28_483 ),
inference(superposition,[],[f3147,f3111]) ).
fof(f4039,plain,
( $false
| ~ spl28_475
| ~ spl28_483 ),
inference(forward_subsumption_resolution,[],[f4035,f248]) ).
fof(f4040,plain,
( ~ spl28_475
| ~ spl28_483 ),
inference(avatar_contradiction_clause,[],[f4039]) ).
fof(f4125,plain,
( e10 = e11
| ~ spl28_428
| ~ spl28_433 ),
inference(superposition,[],[f2912,f2888]) ).
fof(f4131,plain,
( $false
| ~ spl28_428
| ~ spl28_433 ),
inference(forward_subsumption_resolution,[],[f4125,f246]) ).
fof(f4132,plain,
( ~ spl28_428
| ~ spl28_433 ),
inference(avatar_contradiction_clause,[],[f4131]) ).
fof(f4146,plain,
( e11 = e12
| ~ spl28_507
| ~ spl28_513 ),
inference(superposition,[],[f3306,f3280]) ).
fof(f4150,plain,
( $false
| ~ spl28_507
| ~ spl28_513 ),
inference(forward_subsumption_resolution,[],[f4146,f243]) ).
fof(f4151,plain,
( ~ spl28_507
| ~ spl28_513 ),
inference(avatar_contradiction_clause,[],[f4150]) ).
fof(f4154,plain,
( e11 = e13
| ~ spl28_503
| ~ spl28_515 ),
inference(superposition,[],[f3315,f3263]) ).
fof(f4162,plain,
( $false
| ~ spl28_503
| ~ spl28_515 ),
inference(forward_subsumption_resolution,[],[f4154,f242]) ).
fof(f4163,plain,
( ~ spl28_503
| ~ spl28_515 ),
inference(avatar_contradiction_clause,[],[f4162]) ).
fof(f4176,plain,
( e11 = e13
| ~ spl28_506
| ~ spl28_518 ),
inference(superposition,[],[f3328,f3276]) ).
fof(f4181,plain,
( $false
| ~ spl28_506
| ~ spl28_518 ),
inference(forward_subsumption_resolution,[],[f4176,f242]) ).
fof(f4182,plain,
( ~ spl28_506
| ~ spl28_518 ),
inference(avatar_contradiction_clause,[],[f4181]) ).
fof(f4184,plain,
( e11 = e13
| ~ spl28_508
| ~ spl28_520 ),
inference(superposition,[],[f3336,f3284]) ).
fof(f4188,plain,
( $false
| ~ spl28_508
| ~ spl28_520 ),
inference(forward_subsumption_resolution,[],[f4184,f242]) ).
fof(f4189,plain,
( ~ spl28_508
| ~ spl28_520 ),
inference(avatar_contradiction_clause,[],[f4188]) ).
fof(f4248,plain,
( e11 = op1(e11,e11)
| ~ spl28_546 ),
inference(forward_demodulation,[],[f52,f3465]) ).
fof(f4249,plain,
( $false
| spl28_435
| ~ spl28_546 ),
inference(forward_subsumption_resolution,[],[f4248,f2921]) ).
fof(f4250,plain,
( spl28_435
| ~ spl28_546 ),
inference(avatar_contradiction_clause,[],[f4249]) ).
fof(f4278,plain,
( e11 = e12
| ~ spl28_528
| ~ spl28_532 ),
inference(superposition,[],[f3390,f3372]) ).
fof(f4282,plain,
( $false
| ~ spl28_528
| ~ spl28_532 ),
inference(forward_subsumption_resolution,[],[f4278,f243]) ).
fof(f4283,plain,
( ~ spl28_528
| ~ spl28_532 ),
inference(avatar_contradiction_clause,[],[f4282]) ).
fof(f4299,plain,
( e11 = e13
| ~ spl28_527
| ~ spl28_535 ),
inference(superposition,[],[f3404,f3368]) ).
fof(f4306,plain,
( $false
| ~ spl28_527
| ~ spl28_535 ),
inference(forward_subsumption_resolution,[],[f4299,f242]) ).
fof(f4307,plain,
( ~ spl28_527
| ~ spl28_535 ),
inference(avatar_contradiction_clause,[],[f4306]) ).
fof(f4309,plain,
( e12 = e13
| ~ spl28_532
| ~ spl28_536 ),
inference(forward_demodulation,[],[f3408,f3390]) ).
fof(f4310,plain,
( $false
| ~ spl28_532
| ~ spl28_536 ),
inference(forward_subsumption_resolution,[],[f4309,f241]) ).
fof(f4311,plain,
( ~ spl28_532
| ~ spl28_536 ),
inference(avatar_contradiction_clause,[],[f4310]) ).
fof(f4333,plain,
( e11 = e12
| ~ spl28_539
| ~ spl28_541 ),
inference(superposition,[],[f3433,f3423]) ).
fof(f4337,plain,
( $false
| ~ spl28_539
| ~ spl28_541 ),
inference(forward_subsumption_resolution,[],[f4333,f243]) ).
fof(f4338,plain,
( ~ spl28_539
| ~ spl28_541 ),
inference(avatar_contradiction_clause,[],[f4337]) ).
fof(f4339,plain,
( e12 = e13
| ~ spl28_511
| ~ spl28_517 ),
inference(superposition,[],[f3297,f3323]) ).
fof(f4345,plain,
( $false
| ~ spl28_511
| ~ spl28_517 ),
inference(forward_subsumption_resolution,[],[f4339,f241]) ).
fof(f4346,plain,
( ~ spl28_511
| ~ spl28_517 ),
inference(avatar_contradiction_clause,[],[f4345]) ).
fof(f4348,plain,
( e12 = e13
| ~ spl28_530
| ~ spl28_534 ),
inference(superposition,[],[f3381,f3399]) ).
fof(f4352,plain,
( $false
| ~ spl28_530
| ~ spl28_534 ),
inference(forward_subsumption_resolution,[],[f4348,f241]) ).
fof(f4353,plain,
( ~ spl28_530
| ~ spl28_534 ),
inference(avatar_contradiction_clause,[],[f4352]) ).
fof(f4622,plain,
( e23 = op2(e23,e21)
| ~ spl28_494 ),
inference(forward_demodulation,[],[f105,f3208]) ).
fof(f4623,plain,
( e22 = e23
| ~ spl28_480
| ~ spl28_494 ),
inference(forward_demodulation,[],[f4622,f3133]) ).
fof(f4624,plain,
( $false
| ~ spl28_480
| ~ spl28_494 ),
inference(forward_subsumption_resolution,[],[f4623,f247]) ).
fof(f4625,plain,
( ~ spl28_480
| ~ spl28_494 ),
inference(avatar_contradiction_clause,[],[f4624]) ).
fof(f4628,plain,
( e23 = op2(e23,e22)
| ~ spl28_495 ),
inference(forward_demodulation,[],[f105,f3212]) ).
fof(f4629,plain,
( spl28_492
| ~ spl28_495 ),
inference(avatar_split_clause,[],[f4628,f3210,f3189]) ).
fof(f4632,plain,
( e22 = op2(e22,e22)
| ~ spl28_495 ),
inference(forward_demodulation,[],[f107,f3212]) ).
fof(f4633,plain,
( $false
| spl28_421
| ~ spl28_495 ),
inference(forward_subsumption_resolution,[],[f4632,f2844]) ).
fof(f4634,plain,
( spl28_421
| ~ spl28_495 ),
inference(avatar_contradiction_clause,[],[f4633]) ).
fof(f4638,plain,
( e23 = op2(e23,e23)
| ~ spl28_496 ),
inference(forward_demodulation,[],[f105,f3216]) ).
fof(f4798,plain,
( e21 = e22
| ~ spl28_487
| ~ spl28_489 ),
inference(superposition,[],[f3176,f3166]) ).
fof(f4802,plain,
( $false
| spl28_17
| ~ spl28_161
| ~ spl28_487
| ~ spl28_489 ),
inference(forward_subsumption_resolution,[],[f4798,f3593]) ).
fof(f4803,plain,
( spl28_17
| ~ spl28_161
| ~ spl28_487
| ~ spl28_489 ),
inference(avatar_contradiction_clause,[],[f4802]) ).
fof(f4805,plain,
( e22 = e23
| ~ spl28_480
| ~ spl28_484 ),
inference(forward_demodulation,[],[f3151,f3133]) ).
fof(f4810,plain,
( $false
| ~ spl28_480
| ~ spl28_484 ),
inference(forward_subsumption_resolution,[],[f4805,f247]) ).
fof(f4811,plain,
( ~ spl28_480
| ~ spl28_484 ),
inference(avatar_contradiction_clause,[],[f4810]) ).
fof(f4832,plain,
( e21 = e23
| ~ spl28_488
| ~ spl28_492 ),
inference(superposition,[],[f3191,f3171]) ).
fof(f4833,plain,
( e21 = e23
| ~ spl28_488
| ~ spl28_492 ),
inference(superposition,[],[f3171,f3191]) ).
fof(f4834,plain,
( $false
| ~ spl28_488
| ~ spl28_492 ),
inference(forward_subsumption_resolution,[],[f4833,f248]) ).
fof(f4835,plain,
( ~ spl28_488
| ~ spl28_492 ),
inference(avatar_contradiction_clause,[],[f4834]) ).
fof(f4836,plain,
( $false
| ~ spl28_488
| ~ spl28_492 ),
inference(forward_subsumption_resolution,[],[f4832,f248]) ).
fof(f4837,plain,
( ~ spl28_488
| ~ spl28_492 ),
inference(avatar_contradiction_clause,[],[f4836]) ).
fof(f5159,plain,
( e23 = h5(e12)
| ~ spl28_483 ),
inference(forward_demodulation,[],[f337,f3147]) ).
fof(f5160,plain,
( spl28_239
| ~ spl28_483 ),
inference(avatar_split_clause,[],[f5159,f3145,f1962]) ).
fof(f5161,plain,
( e20 = h5(e10)
| ~ spl28_412 ),
inference(forward_demodulation,[],[f338,f2802]) ).
fof(f5162,plain,
( spl28_45
| ~ spl28_412 ),
inference(avatar_split_clause,[],[f5161,f2800,f1053]) ).
fof(f5163,plain,
( op2(e20,e20) != h5(op1(e10,e10))
| ~ spl28_45
| spl28_217 ),
inference(superposition,[],[f1868,f1054]) ).
fof(f5164,plain,
( op2(e20,e20) != h5(e10)
| ~ spl28_45
| spl28_217
| ~ spl28_431 ),
inference(forward_demodulation,[],[f5163,f2903]) ).
fof(f5165,plain,
( e20 != op2(e20,e20)
| ~ spl28_45
| spl28_217
| ~ spl28_431 ),
inference(forward_demodulation,[],[f5164,f1054]) ).
fof(f5166,plain,
( $false
| ~ spl28_45
| spl28_217
| ~ spl28_413
| ~ spl28_431 ),
inference(forward_subsumption_resolution,[],[f5165,f2807]) ).
fof(f5167,plain,
( ~ spl28_45
| spl28_217
| ~ spl28_413
| ~ spl28_431 ),
inference(avatar_contradiction_clause,[],[f5166]) ).
fof(f5169,plain,
( h5(op1(e10,e11)) != op2(h5(e10),e21)
| ~ spl28_49
| spl28_218 ),
inference(forward_demodulation,[],[f1872,f1073]) ).
fof(f5171,plain,
( op2(e20,e21) != h5(op1(e10,e11))
| ~ spl28_45
| ~ spl28_49
| spl28_218 ),
inference(forward_demodulation,[],[f5169,f1054]) ).
fof(f5173,plain,
( op2(e20,e21) != h5(e11)
| ~ spl28_45
| ~ spl28_49
| spl28_218
| ~ spl28_503 ),
inference(forward_demodulation,[],[f5171,f3263]) ).
fof(f5174,plain,
( e21 != op2(e20,e21)
| ~ spl28_45
| ~ spl28_49
| spl28_218
| ~ spl28_503 ),
inference(forward_demodulation,[],[f5173,f1073]) ).
fof(f5175,plain,
( $false
| ~ spl28_45
| ~ spl28_49
| spl28_218
| ~ spl28_451
| ~ spl28_503 ),
inference(forward_subsumption_resolution,[],[f5174,f3006]) ).
fof(f5176,plain,
( ~ spl28_45
| ~ spl28_49
| spl28_218
| ~ spl28_451
| ~ spl28_503 ),
inference(avatar_contradiction_clause,[],[f5175]) ).
fof(f5178,plain,
( h5(op1(e10,e12)) != op2(h5(e10),e23)
| spl28_219
| ~ spl28_239 ),
inference(forward_demodulation,[],[f1876,f1963]) ).
fof(f5180,plain,
( op2(e20,e23) != h5(op1(e10,e12))
| ~ spl28_45
| spl28_219
| ~ spl28_239 ),
inference(forward_demodulation,[],[f5178,f1054]) ).
fof(f5182,plain,
( op2(e20,e23) != h5(e12)
| ~ spl28_45
| spl28_219
| ~ spl28_239
| ~ spl28_510 ),
inference(forward_demodulation,[],[f5180,f3293]) ).
fof(f5184,plain,
( e23 != op2(e20,e23)
| ~ spl28_45
| spl28_219
| ~ spl28_239
| ~ spl28_510 ),
inference(forward_demodulation,[],[f5182,f1963]) ).
fof(f5185,plain,
( $false
| ~ spl28_45
| spl28_219
| ~ spl28_239
| ~ spl28_465
| ~ spl28_510 ),
inference(forward_subsumption_resolution,[],[f5184,f3066]) ).
fof(f5186,plain,
( ~ spl28_45
| spl28_219
| ~ spl28_239
| ~ spl28_465
| ~ spl28_510 ),
inference(avatar_contradiction_clause,[],[f5185]) ).
fof(f5188,plain,
( h5(op1(e10,e13)) != op2(h5(e10),e22)
| spl28_220
| ~ spl28_233 ),
inference(forward_demodulation,[],[f1880,f1931]) ).
fof(f5190,plain,
( op2(e20,e22) != h5(op1(e10,e13))
| ~ spl28_45
| spl28_220
| ~ spl28_233 ),
inference(forward_demodulation,[],[f5188,f1054]) ).
fof(f5192,plain,
( op2(e20,e22) != h5(e13)
| ~ spl28_45
| spl28_220
| ~ spl28_233
| ~ spl28_517 ),
inference(forward_demodulation,[],[f5190,f3323]) ).
fof(f5194,plain,
( e22 != op2(e20,e22)
| ~ spl28_45
| spl28_220
| ~ spl28_233
| ~ spl28_517 ),
inference(forward_demodulation,[],[f5192,f1931]) ).
fof(f5195,plain,
( $false
| ~ spl28_45
| spl28_220
| ~ spl28_233
| ~ spl28_458
| ~ spl28_517 ),
inference(forward_subsumption_resolution,[],[f5194,f3036]) ).
fof(f5196,plain,
( ~ spl28_45
| spl28_220
| ~ spl28_233
| ~ spl28_458
| ~ spl28_517 ),
inference(avatar_contradiction_clause,[],[f5195]) ).
fof(f5198,plain,
( h5(op1(e11,e10)) != op2(h5(e11),e20)
| ~ spl28_45
| spl28_221 ),
inference(forward_demodulation,[],[f1884,f1054]) ).
fof(f5200,plain,
( op2(e21,e20) != h5(op1(e11,e10))
| ~ spl28_45
| ~ spl28_49
| spl28_221 ),
inference(forward_demodulation,[],[f5198,f1073]) ).
fof(f5202,plain,
( op2(e21,e20) != h5(e11)
| ~ spl28_45
| ~ spl28_49
| spl28_221
| ~ spl28_506 ),
inference(forward_demodulation,[],[f5200,f3276]) ).
fof(f5204,plain,
( e21 != op2(e21,e20)
| ~ spl28_45
| ~ spl28_49
| spl28_221
| ~ spl28_506 ),
inference(forward_demodulation,[],[f5202,f1073]) ).
fof(f5205,plain,
( $false
| ~ spl28_45
| ~ spl28_49
| spl28_221
| ~ spl28_454
| ~ spl28_506 ),
inference(forward_subsumption_resolution,[],[f5204,f3019]) ).
fof(f5206,plain,
( ~ spl28_45
| ~ spl28_49
| spl28_221
| ~ spl28_454
| ~ spl28_506 ),
inference(avatar_contradiction_clause,[],[f5205]) ).
fof(f5208,plain,
( op2(e21,e21) != h5(op1(e11,e11))
| ~ spl28_49
| spl28_222 ),
inference(forward_demodulation,[],[f1888,f1073]) ).
fof(f5210,plain,
( op2(e21,e21) != h5(e10)
| ~ spl28_49
| spl28_222
| ~ spl28_430 ),
inference(forward_demodulation,[],[f5208,f2898]) ).
fof(f5212,plain,
( e20 != op2(e21,e21)
| ~ spl28_45
| ~ spl28_49
| spl28_222
| ~ spl28_430 ),
inference(forward_demodulation,[],[f5210,f1054]) ).
fof(f5214,plain,
( $false
| ~ spl28_45
| ~ spl28_49
| spl28_222
| ~ spl28_412
| ~ spl28_430 ),
inference(forward_subsumption_resolution,[],[f5212,f2802]) ).
fof(f5215,plain,
( ~ spl28_45
| ~ spl28_49
| spl28_222
| ~ spl28_412
| ~ spl28_430 ),
inference(avatar_contradiction_clause,[],[f5214]) ).
fof(f5217,plain,
( h5(op1(e11,e12)) != op2(h5(e11),e23)
| spl28_223
| ~ spl28_239 ),
inference(forward_demodulation,[],[f1892,f1963]) ).
fof(f5219,plain,
( op2(e21,e23) != h5(op1(e11,e12))
| ~ spl28_49
| spl28_223
| ~ spl28_239 ),
inference(forward_demodulation,[],[f5217,f1073]) ).
fof(f5221,plain,
( op2(e21,e23) != h5(e13)
| ~ spl28_49
| spl28_223
| ~ spl28_239
| ~ spl28_533 ),
inference(forward_demodulation,[],[f5219,f3395]) ).
fof(f5222,plain,
( e22 != op2(e21,e23)
| ~ spl28_49
| spl28_223
| ~ spl28_233
| ~ spl28_239
| ~ spl28_533 ),
inference(forward_demodulation,[],[f5221,f1931]) ).
fof(f5223,plain,
( $false
| ~ spl28_49
| spl28_223
| ~ spl28_233
| ~ spl28_239
| ~ spl28_478
| ~ spl28_533 ),
inference(forward_subsumption_resolution,[],[f5222,f3124]) ).
fof(f5224,plain,
( ~ spl28_49
| spl28_223
| ~ spl28_233
| ~ spl28_239
| ~ spl28_478
| ~ spl28_533 ),
inference(avatar_contradiction_clause,[],[f5223]) ).
fof(f5226,plain,
( h5(op1(e11,e13)) != op2(h5(e11),e22)
| spl28_224
| ~ spl28_233 ),
inference(forward_demodulation,[],[f1896,f1931]) ).
fof(f5228,plain,
( op2(e21,e22) != h5(op1(e11,e13))
| ~ spl28_49
| spl28_224
| ~ spl28_233 ),
inference(forward_demodulation,[],[f5226,f1073]) ).
fof(f5230,plain,
( op2(e21,e22) != h5(e12)
| ~ spl28_49
| spl28_224
| ~ spl28_233
| ~ spl28_530 ),
inference(forward_demodulation,[],[f5228,f3381]) ).
fof(f5232,plain,
( e23 != op2(e21,e22)
| ~ spl28_49
| spl28_224
| ~ spl28_233
| ~ spl28_239
| ~ spl28_530 ),
inference(forward_demodulation,[],[f5230,f1963]) ).
fof(f5233,plain,
( $false
| ~ spl28_49
| spl28_224
| ~ spl28_233
| ~ spl28_239
| ~ spl28_481
| ~ spl28_530 ),
inference(forward_subsumption_resolution,[],[f5232,f3138]) ).
fof(f5234,plain,
( ~ spl28_49
| spl28_224
| ~ spl28_233
| ~ spl28_239
| ~ spl28_481
| ~ spl28_530 ),
inference(avatar_contradiction_clause,[],[f5233]) ).
fof(f5236,plain,
( h5(op1(e12,e10)) != op2(h5(e12),e20)
| ~ spl28_45
| spl28_225 ),
inference(forward_demodulation,[],[f1900,f1054]) ).
fof(f5238,plain,
( op2(e23,e20) != h5(op1(e12,e10))
| ~ spl28_45
| spl28_225
| ~ spl28_239 ),
inference(forward_demodulation,[],[f5236,f1963]) ).
fof(f5240,plain,
( op2(e23,e20) != h5(e12)
| ~ spl28_45
| spl28_225
| ~ spl28_239
| ~ spl28_513 ),
inference(forward_demodulation,[],[f5238,f3306]) ).
fof(f5242,plain,
( e23 != op2(e23,e20)
| ~ spl28_45
| spl28_225
| ~ spl28_239
| ~ spl28_513 ),
inference(forward_demodulation,[],[f5240,f1963]) ).
fof(f5243,plain,
( $false
| ~ spl28_45
| spl28_225
| ~ spl28_239
| ~ spl28_468
| ~ spl28_513 ),
inference(forward_subsumption_resolution,[],[f5242,f3079]) ).
fof(f5244,plain,
( ~ spl28_45
| spl28_225
| ~ spl28_239
| ~ spl28_468
| ~ spl28_513 ),
inference(avatar_contradiction_clause,[],[f5243]) ).
fof(f5246,plain,
( h5(op1(e12,e11)) != op2(h5(e12),e21)
| ~ spl28_49
| spl28_226 ),
inference(forward_demodulation,[],[f1904,f1073]) ).
fof(f5248,plain,
( op2(e23,e21) != h5(op1(e12,e11))
| ~ spl28_49
| spl28_226
| ~ spl28_239 ),
inference(forward_demodulation,[],[f5246,f1963]) ).
fof(f5250,plain,
( op2(e23,e21) != h5(e13)
| ~ spl28_49
| spl28_226
| ~ spl28_239
| ~ spl28_535 ),
inference(forward_demodulation,[],[f5248,f3404]) ).
fof(f5252,plain,
( e22 != op2(e23,e21)
| ~ spl28_49
| spl28_226
| ~ spl28_233
| ~ spl28_239
| ~ spl28_535 ),
inference(forward_demodulation,[],[f5250,f1931]) ).
fof(f5253,plain,
( $false
| ~ spl28_49
| spl28_226
| ~ spl28_233
| ~ spl28_239
| ~ spl28_480
| ~ spl28_535 ),
inference(forward_subsumption_resolution,[],[f5252,f3133]) ).
fof(f5254,plain,
( ~ spl28_49
| spl28_226
| ~ spl28_233
| ~ spl28_239
| ~ spl28_480
| ~ spl28_535 ),
inference(avatar_contradiction_clause,[],[f5253]) ).
fof(f5256,plain,
( op2(e23,e23) != h5(op1(e12,e12))
| spl28_227
| ~ spl28_239 ),
inference(forward_demodulation,[],[f1908,f1963]) ).
fof(f5258,plain,
( op2(e23,e23) != h5(e10)
| spl28_227
| ~ spl28_239
| ~ spl28_429 ),
inference(forward_demodulation,[],[f5256,f2893]) ).
fof(f5260,plain,
( e20 != op2(e23,e23)
| ~ spl28_45
| spl28_227
| ~ spl28_239
| ~ spl28_429 ),
inference(forward_demodulation,[],[f5258,f1054]) ).
fof(f5262,plain,
( $false
| ~ spl28_45
| spl28_227
| ~ spl28_239
| ~ spl28_410
| ~ spl28_429 ),
inference(forward_subsumption_resolution,[],[f5260,f2792]) ).
fof(f5263,plain,
( ~ spl28_45
| spl28_227
| ~ spl28_239
| ~ spl28_410
| ~ spl28_429 ),
inference(avatar_contradiction_clause,[],[f5262]) ).
fof(f5265,plain,
( h5(op1(e12,e13)) != op2(h5(e12),e22)
| spl28_228
| ~ spl28_233 ),
inference(forward_demodulation,[],[f1912,f1931]) ).
fof(f5267,plain,
( op2(e23,e22) != h5(op1(e12,e13))
| spl28_228
| ~ spl28_233
| ~ spl28_239 ),
inference(forward_demodulation,[],[f5265,f1963]) ).
fof(f5269,plain,
( op2(e23,e22) != h5(e11)
| spl28_228
| ~ spl28_233
| ~ spl28_239
| ~ spl28_539 ),
inference(forward_demodulation,[],[f5267,f3423]) ).
fof(f5270,plain,
( e21 != op2(e23,e22)
| ~ spl28_49
| spl28_228
| ~ spl28_233
| ~ spl28_239
| ~ spl28_539 ),
inference(forward_demodulation,[],[f5269,f1073]) ).
fof(f5271,plain,
( $false
| ~ spl28_49
| spl28_228
| ~ spl28_233
| ~ spl28_239
| ~ spl28_488
| ~ spl28_539 ),
inference(forward_subsumption_resolution,[],[f5270,f3171]) ).
fof(f5272,plain,
( ~ spl28_49
| spl28_228
| ~ spl28_233
| ~ spl28_239
| ~ spl28_488
| ~ spl28_539 ),
inference(avatar_contradiction_clause,[],[f5271]) ).
fof(f5274,plain,
( h5(op1(e13,e10)) != op2(h5(e13),e20)
| ~ spl28_45
| spl28_229 ),
inference(forward_demodulation,[],[f1916,f1054]) ).
fof(f5276,plain,
( op2(e22,e20) != h5(op1(e13,e10))
| ~ spl28_45
| spl28_229
| ~ spl28_233 ),
inference(forward_demodulation,[],[f5274,f1931]) ).
fof(f5278,plain,
( op2(e22,e20) != h5(e13)
| ~ spl28_45
| spl28_229
| ~ spl28_233
| ~ spl28_520 ),
inference(forward_demodulation,[],[f5276,f3336]) ).
fof(f5280,plain,
( e22 != op2(e22,e20)
| ~ spl28_45
| spl28_229
| ~ spl28_233
| ~ spl28_520 ),
inference(forward_demodulation,[],[f5278,f1931]) ).
fof(f5281,plain,
( $false
| ~ spl28_45
| spl28_229
| ~ spl28_233
| ~ spl28_461
| ~ spl28_520 ),
inference(forward_subsumption_resolution,[],[f5280,f3049]) ).
fof(f5282,plain,
( ~ spl28_45
| spl28_229
| ~ spl28_233
| ~ spl28_461
| ~ spl28_520 ),
inference(avatar_contradiction_clause,[],[f5281]) ).
fof(f5284,plain,
( h5(op1(e13,e11)) != op2(h5(e13),e21)
| ~ spl28_49
| spl28_230 ),
inference(forward_demodulation,[],[f1920,f1073]) ).
fof(f5286,plain,
( op2(e22,e21) != h5(op1(e13,e11))
| ~ spl28_49
| spl28_230
| ~ spl28_233 ),
inference(forward_demodulation,[],[f5284,f1931]) ).
fof(f5288,plain,
( op2(e22,e21) != h5(e12)
| ~ spl28_49
| spl28_230
| ~ spl28_233
| ~ spl28_532 ),
inference(forward_demodulation,[],[f5286,f3390]) ).
fof(f5290,plain,
( e23 != op2(e22,e21)
| ~ spl28_49
| spl28_230
| ~ spl28_233
| ~ spl28_239
| ~ spl28_532 ),
inference(forward_demodulation,[],[f5288,f1963]) ).
fof(f5294,plain,
( h5(op1(e13,e12)) != op2(h5(e13),e23)
| spl28_231
| ~ spl28_239 ),
inference(forward_demodulation,[],[f1924,f1963]) ).
fof(f5296,plain,
( op2(e22,e23) != h5(op1(e13,e12))
| spl28_231
| ~ spl28_233
| ~ spl28_239 ),
inference(forward_demodulation,[],[f5294,f1931]) ).
fof(f5298,plain,
( op2(e22,e23) != h5(e11)
| spl28_231
| ~ spl28_233
| ~ spl28_239
| ~ spl28_540 ),
inference(forward_demodulation,[],[f5296,f3428]) ).
fof(f5300,plain,
( e21 != op2(e22,e23)
| ~ spl28_49
| spl28_231
| ~ spl28_233
| ~ spl28_239
| ~ spl28_540 ),
inference(forward_demodulation,[],[f5298,f1073]) ).
fof(f5301,plain,
( $false
| ~ spl28_49
| spl28_231
| ~ spl28_233
| ~ spl28_239
| ~ spl28_487
| ~ spl28_540 ),
inference(forward_subsumption_resolution,[],[f5300,f3166]) ).
fof(f5302,plain,
( ~ spl28_49
| spl28_231
| ~ spl28_233
| ~ spl28_239
| ~ spl28_487
| ~ spl28_540 ),
inference(avatar_contradiction_clause,[],[f5301]) ).
fof(f5304,plain,
( op2(e22,e22) != h5(op1(e13,e13))
| spl28_232
| ~ spl28_233 ),
inference(forward_demodulation,[],[f1928,f1931]) ).
fof(f5306,plain,
( op2(e22,e22) != h5(e10)
| spl28_232
| ~ spl28_233
| ~ spl28_428 ),
inference(forward_demodulation,[],[f5304,f2888]) ).
fof(f5308,plain,
( e20 != op2(e22,e22)
| ~ spl28_45
| spl28_232
| ~ spl28_233
| ~ spl28_428 ),
inference(forward_demodulation,[],[f5306,f1054]) ).
fof(f5310,plain,
( $false
| ~ spl28_45
| spl28_232
| ~ spl28_233
| ~ spl28_411
| ~ spl28_428 ),
inference(forward_subsumption_resolution,[],[f5308,f2797]) ).
fof(f5311,plain,
( ~ spl28_45
| spl28_232
| ~ spl28_233
| ~ spl28_411
| ~ spl28_428 ),
inference(avatar_contradiction_clause,[],[f5310]) ).
fof(f5341,plain,
( ~ spl28_483
| ~ spl28_49
| spl28_230
| ~ spl28_233
| ~ spl28_239
| ~ spl28_532 ),
inference(avatar_split_clause,[],[f5290,f3388,f1962,f1930,f1918,f1072,f3145]) ).
fof(f5380,plain,
( e21 = op2(e23,e21)
| ~ spl28_52
| ~ spl28_264
| ~ spl28_451 ),
inference(superposition,[],[f3006,f3607]) ).
fof(f5409,plain,
( e21 = e22
| ~ spl28_52
| ~ spl28_264
| ~ spl28_451
| ~ spl28_480 ),
inference(forward_demodulation,[],[f5380,f3133]) ).
fof(f5411,plain,
( $false
| spl28_17
| ~ spl28_52
| ~ spl28_161
| ~ spl28_264
| ~ spl28_451
| ~ spl28_480 ),
inference(forward_subsumption_resolution,[],[f5409,f3593]) ).
fof(f5412,plain,
( spl28_17
| ~ spl28_52
| ~ spl28_161
| ~ spl28_264
| ~ spl28_451
| ~ spl28_480 ),
inference(avatar_contradiction_clause,[],[f5411]) ).
fof(f5447,plain,
( e21 = op2(e23,e23)
| ~ spl28_52
| ~ spl28_264
| ~ spl28_456 ),
inference(forward_demodulation,[],[f3027,f3607]) ).
fof(f5453,plain,
( e23 != unit2
| ~ spl28_52
| ~ spl28_264
| spl28_493 ),
inference(forward_demodulation,[],[f3203,f3607]) ).
fof(f5456,plain,
( spl28_426
| ~ spl28_496 ),
inference(avatar_split_clause,[],[f4638,f3214,f2874]) ).
fof(f5522,plain,
( $false
| ~ spl28_52
| ~ spl28_264
| spl28_415
| ~ spl28_456 ),
inference(forward_subsumption_resolution,[],[f5447,f2815]) ).
fof(f5523,plain,
( ~ spl28_52
| ~ spl28_264
| spl28_415
| ~ spl28_456 ),
inference(avatar_contradiction_clause,[],[f5522]) ).
fof(f5528,plain,
( ~ spl28_496
| ~ spl28_52
| ~ spl28_264
| spl28_493 ),
inference(avatar_split_clause,[],[f5453,f3202,f2082,f1086,f3214]) ).
fof(f5647,plain,
( e23 != op2(e22,e22)
| ~ spl28_52
| ~ spl28_264
| spl28_411 ),
inference(forward_demodulation,[],[f2796,f3607]) ).
fof(f5657,plain,
( spl28_421
| ~ spl28_495 ),
inference(avatar_split_clause,[],[f4632,f3210,f2843]) ).
fof(f5662,plain,
( ~ spl28_415
| ~ spl28_52
| ~ spl28_264
| spl28_418 ),
inference(avatar_split_clause,[],[f3613,f2829,f2082,f1086,f2814]) ).
fof(f5713,plain,
( ~ spl28_425
| ~ spl28_52
| ~ spl28_264
| spl28_411 ),
inference(avatar_split_clause,[],[f5647,f2795,f2082,f1086,f2866]) ).
cnf(s36,plain,
( ~ spl28_41
| ~ spl28_45 ),
inference(sat_conversion,[],[f1056]) ).
cnf(s39,plain,
( ~ spl28_46
| ~ spl28_49 ),
inference(sat_conversion,[],[f1075]) ).
cnf(s169,plain,
( spl28_41
| spl28_46
| ~ spl28_217
| ~ spl28_218
| ~ spl28_219
| ~ spl28_220
| ~ spl28_221
| ~ spl28_222
| ~ spl28_223
| ~ spl28_224
| ~ spl28_225
| ~ spl28_226
| ~ spl28_227
| ~ spl28_228
| ~ spl28_229
| ~ spl28_230
| ~ spl28_231
| ~ spl28_232
| ~ spl28_233
| ~ spl28_239 ),
inference(sat_conversion,[],[f1965]) ).
cnf(s289,plain,
spl28_401,
inference(sat_conversion,[],[f2761]) ).
cnf(s301,plain,
spl28_264,
inference(sat_conversion,[],[f2773]) ).
cnf(s302,plain,
spl28_59,
inference(sat_conversion,[],[f2774]) ).
cnf(s303,plain,
spl28_233,
inference(sat_conversion,[],[f2775]) ).
cnf(s304,plain,
spl28_49,
inference(sat_conversion,[],[f2776]) ).
cnf(s309,plain,
spl28_161,
inference(sat_conversion,[],[f2781]) ).
cnf(s310,plain,
spl28_14,
inference(sat_conversion,[],[f2782]) ).
cnf(s313,plain,
( ~ spl28_409
| spl28_410 ),
inference(sat_conversion,[],[f2793]) ).
cnf(s314,plain,
( ~ spl28_409
| spl28_411 ),
inference(sat_conversion,[],[f2798]) ).
cnf(s316,plain,
( ~ spl28_409
| spl28_413 ),
inference(sat_conversion,[],[f2808]) ).
cnf(s319,plain,
( spl28_414
| spl28_417 ),
inference(sat_conversion,[],[f2827]) ).
cnf(s327,plain,
( spl28_409
| ~ spl28_414
| spl28_422
| spl28_424 ),
inference(sat_conversion,[],[f2863]) ).
cnf(s331,plain,
( spl28_409
| ~ spl28_414
| spl28_422
| spl28_425 ),
inference(sat_conversion,[],[f2871]) ).
cnf(s337,plain,
( spl28_427
| spl28_428 ),
inference(sat_conversion,[],[f2889]) ).
cnf(s338,plain,
( spl28_427
| spl28_429 ),
inference(sat_conversion,[],[f2894]) ).
cnf(s340,plain,
( spl28_427
| spl28_431 ),
inference(sat_conversion,[],[f2904]) ).
cnf(s343,plain,
( ~ spl28_432
| spl28_435 ),
inference(sat_conversion,[],[f2923]) ).
cnf(s351,plain,
( ~ spl28_427
| spl28_432
| spl28_440
| spl28_442 ),
inference(sat_conversion,[],[f2959]) ).
cnf(s376,plain,
( spl28_424
| spl28_463
| spl28_483
| spl28_484 ),
inference(sat_conversion,[],[f3152]) ).
cnf(s379,plain,
( spl28_416
| spl28_455
| spl28_475
| spl28_487 ),
inference(sat_conversion,[],[f3167]) ).
cnf(s384,plain,
( spl28_425
| spl28_464
| spl28_481
| spl28_492 ),
inference(sat_conversion,[],[f3192]) ).
cnf(s387,plain,
( spl28_415
| spl28_456
| spl28_476
| spl28_488 ),
inference(sat_conversion,[],[f3195]) ).
cnf(s390,plain,
( spl28_419
| spl28_459
| spl28_478
| spl28_489 ),
inference(sat_conversion,[],[f3198]) ).
cnf(s393,plain,
( spl28_493
| spl28_494
| spl28_495
| spl28_496 ),
inference(sat_conversion,[],[f3217]) ).
cnf(s424,plain,
( spl28_442
| spl28_518
| spl28_533
| spl28_534 ),
inference(sat_conversion,[],[f3400]) ).
cnf(s425,plain,
( spl28_442
| spl28_515
| spl28_535
| spl28_536 ),
inference(sat_conversion,[],[f3409]) ).
cnf(s428,plain,
( spl28_434
| spl28_507
| spl28_527
| spl28_539 ),
inference(sat_conversion,[],[f3424]) ).
cnf(s436,plain,
( spl28_433
| spl28_508
| spl28_528
| spl28_540 ),
inference(sat_conversion,[],[f3452]) ).
cnf(s439,plain,
( spl28_437
| spl28_511
| spl28_530
| spl28_541 ),
inference(sat_conversion,[],[f3455]) ).
cnf(s442,plain,
( spl28_545
| spl28_546
| spl28_547
| spl28_548 ),
inference(sat_conversion,[],[f3474]) ).
cnf(s459,plain,
( spl28_520
| ~ spl28_545 ),
inference(sat_conversion,[],[f3502]) ).
cnf(s460,plain,
( spl28_517
| ~ spl28_545 ),
inference(sat_conversion,[],[f3504]) ).
cnf(s461,plain,
( spl28_513
| ~ spl28_545 ),
inference(sat_conversion,[],[f3506]) ).
cnf(s462,plain,
( spl28_510
| ~ spl28_545 ),
inference(sat_conversion,[],[f3508]) ).
cnf(s463,plain,
( spl28_506
| ~ spl28_545 ),
inference(sat_conversion,[],[f3510]) ).
cnf(s464,plain,
( spl28_503
| ~ spl28_545 ),
inference(sat_conversion,[],[f3512]) ).
cnf(s467,plain,
( spl28_468
| ~ spl28_493 ),
inference(sat_conversion,[],[f3517]) ).
cnf(s468,plain,
( spl28_465
| ~ spl28_493 ),
inference(sat_conversion,[],[f3519]) ).
cnf(s469,plain,
( spl28_461
| ~ spl28_493 ),
inference(sat_conversion,[],[f3521]) ).
cnf(s470,plain,
( spl28_458
| ~ spl28_493 ),
inference(sat_conversion,[],[f3523]) ).
cnf(s471,plain,
( spl28_454
| ~ spl28_493 ),
inference(sat_conversion,[],[f3525]) ).
cnf(s472,plain,
( spl28_451
| ~ spl28_493 ),
inference(sat_conversion,[],[f3527]) ).
cnf(s473,plain,
( spl28_413
| ~ spl28_493 ),
inference(sat_conversion,[],[f3529]) ).
cnf(s475,plain,
spl28_532,
inference(sat_conversion,[],[f3531]) ).
cnf(s476,plain,
spl28_430,
inference(sat_conversion,[],[f3532]) ).
cnf(s477,plain,
spl28_480,
inference(sat_conversion,[],[f3533]) ).
cnf(s478,plain,
spl28_412,
inference(sat_conversion,[],[f3534]) ).
cnf(s480,plain,
( ~ spl28_14
| spl28_19
| ~ spl28_412
| ~ spl28_417 ),
inference(sat_conversion,[],[f3540]) ).
cnf(s482,plain,
( spl28_54
| ~ spl28_59
| ~ spl28_413
| ~ spl28_418 ),
inference(sat_conversion,[],[f3549]) ).
cnf(s483,plain,
( ~ spl28_54
| ~ spl28_59 ),
inference(sat_conversion,[],[f3561]) ).
cnf(s493,plain,
( ~ spl28_17
| ~ spl28_161 ),
inference(sat_conversion,[],[f3592]) ).
cnf(s494,plain,
( ~ spl28_14
| ~ spl28_19
| spl28_54
| ~ spl28_59 ),
inference(sat_conversion,[],[f3598]) ).
cnf(s499,plain,
( spl28_112
| ~ spl28_401
| ~ spl28_410
| ~ spl28_419 ),
inference(sat_conversion,[],[f3627]) ).
cnf(s501,plain,
( ~ spl28_112
| ~ spl28_401 ),
inference(sat_conversion,[],[f3639]) ).
cnf(s503,plain,
( spl28_112
| ~ spl28_401
| ~ spl28_411
| ~ spl28_421 ),
inference(sat_conversion,[],[f3650]) ).
cnf(s505,plain,
( spl28_112
| ~ spl28_401
| ~ spl28_412
| ~ spl28_422 ),
inference(sat_conversion,[],[f3658]) ).
cnf(s509,plain,
( spl28_52
| ~ spl28_264
| ~ spl28_412
| ~ spl28_424 ),
inference(sat_conversion,[],[f3676]) ).
cnf(s514,plain,
( spl28_52
| ~ spl28_264
| ~ spl28_411
| ~ spl28_425 ),
inference(sat_conversion,[],[f3699]) ).
cnf(s516,plain,
( spl28_52
| ~ spl28_264
| ~ spl28_410
| ~ spl28_426 ),
inference(sat_conversion,[],[f3708]) ).
cnf(s518,plain,
( ~ spl28_430
| ~ spl28_435 ),
inference(sat_conversion,[],[f3715]) ).
cnf(s521,plain,
( spl28_444
| ~ spl28_548 ),
inference(sat_conversion,[],[f3726]) ).
cnf(s527,plain,
( spl28_439
| ~ spl28_547 ),
inference(sat_conversion,[],[f3742]) ).
cnf(s552,plain,
( ~ spl28_428
| ~ spl28_437 ),
inference(sat_conversion,[],[f3782]) ).
cnf(s553,plain,
( ~ spl28_429
| ~ spl28_434 ),
inference(sat_conversion,[],[f3784]) ).
cnf(s555,plain,
( ~ spl28_429
| ~ spl28_439 ),
inference(sat_conversion,[],[f3793]) ).
cnf(s557,plain,
( ~ spl28_430
| ~ spl28_440 ),
inference(sat_conversion,[],[f3801]) ).
cnf(s561,plain,
( ~ spl28_430
| ~ spl28_442 ),
inference(sat_conversion,[],[f3823]) ).
cnf(s565,plain,
( ~ spl28_428
| ~ spl28_444 ),
inference(sat_conversion,[],[f3841]) ).
cnf(s581,plain,
( spl28_54
| ~ spl28_59
| ~ spl28_411
| ~ spl28_416 ),
inference(sat_conversion,[],[f3900]) ).
cnf(s585,plain,
( spl28_54
| ~ spl28_59
| ~ spl28_410
| ~ spl28_415 ),
inference(sat_conversion,[],[f3917]) ).
cnf(s589,plain,
( spl28_17
| ~ spl28_161
| ~ spl28_455
| ~ spl28_461 ),
inference(sat_conversion,[],[f3931]) ).
cnf(s591,plain,
( ~ spl28_451
| ~ spl28_463 ),
inference(sat_conversion,[],[f3939]) ).
cnf(s592,plain,
( ~ spl28_458
| ~ spl28_464 ),
inference(sat_conversion,[],[f3943]) ).
cnf(s593,plain,
( ~ spl28_459
| ~ spl28_465 ),
inference(sat_conversion,[],[f3947]) ).
cnf(s598,plain,
( ~ spl28_456
| ~ spl28_468 ),
inference(sat_conversion,[],[f3968]) ).
cnf(s613,plain,
( spl28_17
| ~ spl28_161
| ~ spl28_476
| ~ spl28_480 ),
inference(sat_conversion,[],[f4023]) ).
cnf(s617,plain,
( ~ spl28_475
| ~ spl28_483 ),
inference(sat_conversion,[],[f4040]) ).
cnf(s639,plain,
( ~ spl28_428
| ~ spl28_433 ),
inference(sat_conversion,[],[f4132]) ).
cnf(s643,plain,
( ~ spl28_507
| ~ spl28_513 ),
inference(sat_conversion,[],[f4151]) ).
cnf(s645,plain,
( ~ spl28_503
| ~ spl28_515 ),
inference(sat_conversion,[],[f4163]) ).
cnf(s649,plain,
( ~ spl28_506
| ~ spl28_518 ),
inference(sat_conversion,[],[f4182]) ).
cnf(s651,plain,
( ~ spl28_508
| ~ spl28_520 ),
inference(sat_conversion,[],[f4189]) ).
cnf(s670,plain,
( spl28_435
| ~ spl28_546 ),
inference(sat_conversion,[],[f4250]) ).
cnf(s680,plain,
( ~ spl28_528
| ~ spl28_532 ),
inference(sat_conversion,[],[f4283]) ).
cnf(s685,plain,
( ~ spl28_527
| ~ spl28_535 ),
inference(sat_conversion,[],[f4307]) ).
cnf(s686,plain,
( ~ spl28_532
| ~ spl28_536 ),
inference(sat_conversion,[],[f4311]) ).
cnf(s692,plain,
( ~ spl28_539
| ~ spl28_541 ),
inference(sat_conversion,[],[f4338]) ).
cnf(s694,plain,
( ~ spl28_511
| ~ spl28_517 ),
inference(sat_conversion,[],[f4346]) ).
cnf(s696,plain,
( ~ spl28_530
| ~ spl28_534 ),
inference(sat_conversion,[],[f4353]) ).
cnf(s739,plain,
( ~ spl28_480
| ~ spl28_494 ),
inference(sat_conversion,[],[f4625]) ).
cnf(s740,plain,
( spl28_492
| ~ spl28_495 ),
inference(sat_conversion,[],[f4629]) ).
cnf(s742,plain,
( spl28_421
| ~ spl28_495 ),
inference(sat_conversion,[],[f4634]) ).
cnf(s773,plain,
( spl28_17
| ~ spl28_161
| ~ spl28_487
| ~ spl28_489 ),
inference(sat_conversion,[],[f4803]) ).
cnf(s775,plain,
( ~ spl28_480
| ~ spl28_484 ),
inference(sat_conversion,[],[f4811]) ).
cnf(s778,plain,
( ~ spl28_488
| ~ spl28_492 ),
inference(sat_conversion,[],[f4835]) ).
cnf(s779,plain,
( ~ spl28_488
| ~ spl28_492 ),
inference(sat_conversion,[],[f4837]) ).
cnf(s816,plain,
( spl28_239
| ~ spl28_483 ),
inference(sat_conversion,[],[f5160]) ).
cnf(s817,plain,
( spl28_45
| ~ spl28_412 ),
inference(sat_conversion,[],[f5162]) ).
cnf(s818,plain,
( ~ spl28_45
| spl28_217
| ~ spl28_413
| ~ spl28_431 ),
inference(sat_conversion,[],[f5167]) ).
cnf(s819,plain,
( ~ spl28_45
| ~ spl28_49
| spl28_218
| ~ spl28_451
| ~ spl28_503 ),
inference(sat_conversion,[],[f5176]) ).
cnf(s820,plain,
( ~ spl28_45
| spl28_219
| ~ spl28_239
| ~ spl28_465
| ~ spl28_510 ),
inference(sat_conversion,[],[f5186]) ).
cnf(s821,plain,
( ~ spl28_45
| spl28_220
| ~ spl28_233
| ~ spl28_458
| ~ spl28_517 ),
inference(sat_conversion,[],[f5196]) ).
cnf(s822,plain,
( ~ spl28_45
| ~ spl28_49
| spl28_221
| ~ spl28_454
| ~ spl28_506 ),
inference(sat_conversion,[],[f5206]) ).
cnf(s823,plain,
( ~ spl28_45
| ~ spl28_49
| spl28_222
| ~ spl28_412
| ~ spl28_430 ),
inference(sat_conversion,[],[f5215]) ).
cnf(s824,plain,
( ~ spl28_49
| spl28_223
| ~ spl28_233
| ~ spl28_239
| ~ spl28_478
| ~ spl28_533 ),
inference(sat_conversion,[],[f5224]) ).
cnf(s825,plain,
( ~ spl28_49
| spl28_224
| ~ spl28_233
| ~ spl28_239
| ~ spl28_481
| ~ spl28_530 ),
inference(sat_conversion,[],[f5234]) ).
cnf(s826,plain,
( ~ spl28_45
| spl28_225
| ~ spl28_239
| ~ spl28_468
| ~ spl28_513 ),
inference(sat_conversion,[],[f5244]) ).
cnf(s827,plain,
( ~ spl28_49
| spl28_226
| ~ spl28_233
| ~ spl28_239
| ~ spl28_480
| ~ spl28_535 ),
inference(sat_conversion,[],[f5254]) ).
cnf(s828,plain,
( ~ spl28_45
| spl28_227
| ~ spl28_239
| ~ spl28_410
| ~ spl28_429 ),
inference(sat_conversion,[],[f5263]) ).
cnf(s829,plain,
( ~ spl28_49
| spl28_228
| ~ spl28_233
| ~ spl28_239
| ~ spl28_488
| ~ spl28_539 ),
inference(sat_conversion,[],[f5272]) ).
cnf(s830,plain,
( ~ spl28_45
| spl28_229
| ~ spl28_233
| ~ spl28_461
| ~ spl28_520 ),
inference(sat_conversion,[],[f5282]) ).
cnf(s832,plain,
( ~ spl28_49
| spl28_231
| ~ spl28_233
| ~ spl28_239
| ~ spl28_487
| ~ spl28_540 ),
inference(sat_conversion,[],[f5302]) ).
cnf(s833,plain,
( ~ spl28_45
| spl28_232
| ~ spl28_233
| ~ spl28_411
| ~ spl28_428 ),
inference(sat_conversion,[],[f5311]) ).
cnf(s838,plain,
( ~ spl28_49
| spl28_230
| ~ spl28_233
| ~ spl28_239
| ~ spl28_483
| ~ spl28_532 ),
inference(sat_conversion,[],[f5341]) ).
cnf(s849,plain,
( spl28_17
| ~ spl28_52
| ~ spl28_161
| ~ spl28_264
| ~ spl28_451
| ~ spl28_480 ),
inference(sat_conversion,[],[f5412]) ).
cnf(s851,plain,
( spl28_426
| ~ spl28_496 ),
inference(sat_conversion,[],[f5456]) ).
cnf(s873,plain,
( ~ spl28_52
| ~ spl28_264
| spl28_415
| ~ spl28_456 ),
inference(sat_conversion,[],[f5523]) ).
cnf(s878,plain,
( ~ spl28_52
| ~ spl28_264
| spl28_493
| ~ spl28_496 ),
inference(sat_conversion,[],[f5528]) ).
cnf(s933,plain,
( spl28_421
| ~ spl28_495 ),
inference(sat_conversion,[],[f5657]) ).
cnf(s937,plain,
( ~ spl28_52
| ~ spl28_264
| ~ spl28_415
| spl28_418 ),
inference(sat_conversion,[],[f5662]) ).
cnf(s942,plain,
( ~ spl28_52
| ~ spl28_264
| spl28_411
| ~ spl28_425 ),
inference(sat_conversion,[],[f5713]) ).
cnf(s965,plain,
spl28_45,
inference(rat,[],[s817,s478]) ).
cnf(s967,plain,
~ spl28_484,
inference(rat,[],[s775,s477]) ).
cnf(s968,plain,
~ spl28_494,
inference(rat,[],[s739,s477]) ).
cnf(s969,plain,
~ spl28_442,
inference(rat,[],[s561,s476]) ).
cnf(s970,plain,
~ spl28_440,
inference(rat,[],[s557,s476]) ).
cnf(s971,plain,
~ spl28_435,
inference(rat,[],[s518,s476]) ).
cnf(s972,plain,
~ spl28_546,
inference(rat,[],[s670,s971]) ).
cnf(s973,plain,
~ spl28_536,
inference(rat,[],[s686,s475]) ).
cnf(s974,plain,
~ spl28_528,
inference(rat,[],[s680,s475]) ).
cnf(s975,plain,
( spl28_545
| spl28_547
| spl28_548 ),
inference(rat,[],[s442,s972]) ).
cnf(s977,plain,
( spl28_433
| spl28_508
| spl28_540 ),
inference(rat,[],[s436,s974]) ).
cnf(s978,plain,
( spl28_515
| spl28_535 ),
inference(rat,[],[s425,s973,s969]) ).
cnf(s979,plain,
( spl28_518
| spl28_533
| spl28_534 ),
inference(rat,[],[s424,s969]) ).
cnf(s983,plain,
( spl28_493
| spl28_495
| spl28_496 ),
inference(rat,[],[s393,s968]) ).
cnf(s985,plain,
( spl28_424
| spl28_463
| spl28_483 ),
inference(rat,[],[s376,s967]) ).
cnf(s989,plain,
( ~ spl28_427
| spl28_432 ),
inference(rat,[],[s351,s969,s970]) ).
cnf(s993,plain,
~ spl28_432,
inference(rat,[],[s343,s971]) ).
cnf(s994,plain,
~ spl28_427,
inference(rat,[],[s989,s993]) ).
cnf(s995,plain,
spl28_431,
inference(rat,[],[s340,s994]) ).
cnf(s999,plain,
spl28_429,
inference(rat,[],[s338,s994]) ).
cnf(s1001,plain,
~ spl28_439,
inference(rat,[],[s555,s999]) ).
cnf(s1002,plain,
~ spl28_434,
inference(rat,[],[s553,s999]) ).
cnf(s1003,plain,
~ spl28_547,
inference(rat,[],[s527,s1001]) ).
cnf(s1004,plain,
spl28_428,
inference(rat,[],[s337,s994]) ).
cnf(s1005,plain,
~ spl28_433,
inference(rat,[],[s639,s1004]) ).
cnf(s1006,plain,
~ spl28_444,
inference(rat,[],[s565,s1004]) ).
cnf(s1007,plain,
~ spl28_437,
inference(rat,[],[s552,s1004]) ).
cnf(s1008,plain,
~ spl28_548,
inference(rat,[],[s521,s1006]) ).
cnf(s1009,plain,
spl28_545,
inference(rat,[],[s975,s1003,s1008]) ).
cnf(s1010,plain,
spl28_503,
inference(rat,[],[s464,s1009]) ).
cnf(s1011,plain,
spl28_506,
inference(rat,[],[s463,s1009]) ).
cnf(s1012,plain,
spl28_510,
inference(rat,[],[s462,s1009]) ).
cnf(s1013,plain,
spl28_513,
inference(rat,[],[s461,s1009]) ).
cnf(s1014,plain,
spl28_517,
inference(rat,[],[s460,s1009]) ).
cnf(s1015,plain,
spl28_520,
inference(rat,[],[s459,s1009]) ).
cnf(s1016,plain,
~ spl28_515,
inference(rat,[],[s645,s1010]) ).
cnf(s1018,plain,
~ spl28_518,
inference(rat,[],[s649,s1011]) ).
cnf(s1022,plain,
~ spl28_507,
inference(rat,[],[s643,s1013]) ).
cnf(s1023,plain,
~ spl28_511,
inference(rat,[],[s694,s1014]) ).
cnf(s1025,plain,
~ spl28_508,
inference(rat,[],[s651,s1015]) ).
cnf(s1026,plain,
spl28_535,
inference(rat,[],[s978,s1016]) ).
cnf(s1027,plain,
spl28_540,
inference(rat,[],[s977,s1005,s1025]) ).
cnf(s1028,plain,
~ spl28_527,
inference(rat,[],[s685,s1026]) ).
cnf(s1031,plain,
spl28_539,
inference(rat,[],[s428,s1022,s1002,s1028]) ).
cnf(s1033,plain,
~ spl28_541,
inference(rat,[],[s692,s1031]) ).
cnf(s1035,plain,
spl28_530,
inference(rat,[],[s439,s1023,s1007,s1033]) ).
cnf(s1036,plain,
~ spl28_534,
inference(rat,[],[s696,s1035]) ).
cnf(s1038,plain,
spl28_533,
inference(rat,[],[s979,s1018,s1036]) ).
cnf(s1040,plain,
~ spl28_17,
inference(rat,[],[s493,s309]) ).
cnf(s1041,plain,
~ spl28_476,
inference(rat,[],[s613,s477,s309,s1040]) ).
cnf(s1043,plain,
spl28_222,
inference(rat,[],[s823,s476,s478,s965,s304]) ).
cnf(s1044,plain,
~ spl28_54,
inference(rat,[],[s483,s302]) ).
cnf(s1045,plain,
~ spl28_19,
inference(rat,[],[s494,s302,s310,s1044]) ).
cnf(s1046,plain,
~ spl28_417,
inference(rat,[],[s480,s310,s478,s1045]) ).
cnf(s1047,plain,
spl28_414,
inference(rat,[],[s319,s1046]) ).
cnf(s1048,plain,
~ spl28_112,
inference(rat,[],[s501,s289]) ).
cnf(s1049,plain,
~ spl28_422,
inference(rat,[],[s505,s289,s478,s1048]) ).
cnf(s1091,plain,
( spl28_41
| spl28_46
| ~ spl28_217
| ~ spl28_218
| ~ spl28_219
| ~ spl28_220
| ~ spl28_221
| ~ spl28_223
| ~ spl28_224
| ~ spl28_225
| ~ spl28_226
| ~ spl28_227
| ~ spl28_228
| ~ spl28_229
| ~ spl28_230
| ~ spl28_231
| ~ spl28_232
| ~ spl28_239 ),
inference(rat,[],[s169,s303,s1043]) ).
cnf(s1129,plain,
~ spl28_46,
inference(rat,[],[s39,s304]) ).
cnf(s1130,plain,
~ spl28_41,
inference(rat,[],[s36,s965]) ).
cnf(s1137,plain,
spl28_413,
inference(rat,[],[s742,s983,s503,s878,s942,s509,s327,s331,s316,s473,s289,s1048,s301,s478,s1047,s1049]) ).
cnf(s1141,plain,
spl28_217,
inference(rat,[],[s818,s995,s965,s1137]) ).
cnf(s1146,plain,
~ spl28_418,
inference(rat,[],[s482,s1044,s302,s1137]) ).
cnf(s1161,plain,
( ~ spl28_52
| spl28_493 ),
inference(rat,[],[s778,s387,s740,s873,s983,s937,s878,s1146,s301,s1041]) ).
cnf(s1162,plain,
spl28_493,
inference(rat,[],[s983,s851,s933,s516,s503,s313,s314,s327,s509,s1161,s301,s289,s1048,s1047,s1049,s478]) ).
cnf(s1163,plain,
spl28_451,
inference(rat,[],[s472,s1162]) ).
cnf(s1164,plain,
spl28_454,
inference(rat,[],[s471,s1162]) ).
cnf(s1165,plain,
spl28_458,
inference(rat,[],[s470,s1162]) ).
cnf(s1166,plain,
spl28_461,
inference(rat,[],[s469,s1162]) ).
cnf(s1167,plain,
spl28_465,
inference(rat,[],[s468,s1162]) ).
cnf(s1168,plain,
spl28_468,
inference(rat,[],[s467,s1162]) ).
cnf(s1170,plain,
~ spl28_463,
inference(rat,[],[s591,s1163]) ).
cnf(s1173,plain,
spl28_218,
inference(rat,[],[s819,s1010,s304,s965,s1163]) ).
cnf(s1175,plain,
~ spl28_52,
inference(rat,[],[s849,s477,s301,s1040,s309,s1163]) ).
cnf(s1184,plain,
spl28_221,
inference(rat,[],[s822,s1011,s304,s965,s1164]) ).
cnf(s1193,plain,
~ spl28_464,
inference(rat,[],[s592,s1165]) ).
cnf(s1195,plain,
spl28_220,
inference(rat,[],[s821,s1014,s303,s965,s1165]) ).
cnf(s1200,plain,
~ spl28_455,
inference(rat,[],[s589,s1040,s309,s1166]) ).
cnf(s1201,plain,
spl28_229,
inference(rat,[],[s830,s1015,s303,s965,s1166]) ).
cnf(s1204,plain,
~ spl28_459,
inference(rat,[],[s593,s1167]) ).
cnf(s1207,plain,
~ spl28_456,
inference(rat,[],[s598,s1168]) ).
cnf(s1212,plain,
~ spl28_424,
inference(rat,[],[s509,s301,s478,s1175]) ).
cnf(s1232,plain,
spl28_409,
inference(rat,[],[s327,s1049,s1047,s1212]) ).
cnf(s1233,plain,
spl28_483,
inference(rat,[],[s985,s1170,s1212]) ).
cnf(s1234,plain,
spl28_411,
inference(rat,[],[s314,s1232]) ).
cnf(s1235,plain,
spl28_410,
inference(rat,[],[s313,s1232]) ).
cnf(s1236,plain,
spl28_239,
inference(rat,[],[s816,s1233]) ).
cnf(s1237,plain,
~ spl28_475,
inference(rat,[],[s617,s1233]) ).
cnf(s1238,plain,
spl28_232,
inference(rat,[],[s833,s1004,s303,s965,s1234]) ).
cnf(s1239,plain,
~ spl28_416,
inference(rat,[],[s581,s1044,s302,s1234]) ).
cnf(s1240,plain,
~ spl28_425,
inference(rat,[],[s514,s1175,s301,s1234]) ).
cnf(s1246,plain,
~ spl28_415,
inference(rat,[],[s585,s1044,s302,s1235]) ).
cnf(s1248,plain,
~ spl28_419,
inference(rat,[],[s499,s1048,s289,s1235]) ).
cnf(s1253,plain,
spl28_227,
inference(rat,[],[s828,s999,s1235,s965,s1236]) ).
cnf(s1254,plain,
spl28_225,
inference(rat,[],[s826,s1013,s1168,s965,s1236]) ).
cnf(s1255,plain,
spl28_219,
inference(rat,[],[s820,s1012,s1167,s965,s1236]) ).
cnf(s1256,plain,
spl28_230,
inference(rat,[],[s838,s475,s1233,s303,s304,s1236]) ).
cnf(s1257,plain,
spl28_226,
inference(rat,[],[s827,s1026,s477,s303,s304,s1236]) ).
cnf(s1258,plain,
spl28_487,
inference(rat,[],[s379,s1200,s1239,s1237]) ).
cnf(s1260,plain,
spl28_488,
inference(rat,[],[s387,s1207,s1041,s1246]) ).
cnf(s1263,plain,
~ spl28_489,
inference(rat,[],[s773,s1040,s309,s1258]) ).
cnf(s1265,plain,
spl28_231,
inference(rat,[],[s832,s1027,s1236,s303,s304,s1258]) ).
cnf(s1266,plain,
~ spl28_492,
inference(rat,[],[s779,s1260]) ).
cnf(s1268,plain,
spl28_228,
inference(rat,[],[s829,s1031,s1236,s303,s304,s1260]) ).
cnf(s1269,plain,
spl28_478,
inference(rat,[],[s390,s1204,s1248,s1263]) ).
cnf(s1270,plain,
spl28_481,
inference(rat,[],[s384,s1193,s1240,s1266]) ).
cnf(s1273,plain,
spl28_223,
inference(rat,[],[s824,s1038,s1236,s303,s304,s1269]) ).
cnf(s1276,plain,
spl28_224,
inference(rat,[],[s825,s1035,s1236,s303,s304,s1270]) ).
cnf(s1281,plain,
$false,
inference(rat,[],[s1091,s1236,s1238,s1265,s1256,s1201,s1268,s1253,s1257,s1254,s1255,s1173,s1184,s1195,s1141,s1130,s1129,s1276,s1273]) ).
fof(f5810,plain,
$false,
inference(avatar_sat_refutation,[],[s1281]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG037+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n009.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 19:20:01 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.02/0.39 % (3366369)Will run a generic schedule for satisfiability detection.
% 1.02/0.39 % (3366378)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4199427903:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.02/0.39 % (3366375)% WARNING: option uhcvi not known.
% 1.02/0.39 % (3366374)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2989139302_2999 on theBenchmark for (2999ds/0Mi)
% 1.02/0.39 % (3366375)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4229539026:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.02/0.39 % (3366376)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1488882868:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.02/0.39 % (3366377)dis+10_1_sil=32000:sp=arity:random_seed=2359577005:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.02/0.39 % (3366380)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3042767671:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.02/0.39 % (3366379)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3166601475:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.02/0.39 % (3366378)Instruction limit reached!
% 1.02/0.39 % (3366378)------------------------------
% 1.02/0.39 % (3366378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.39 % (3366378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.39 % (3366378)CaDiCaL version: 2.1.3
% 1.02/0.39 % (3366378)Termination reason: Instruction limit
% 1.02/0.39 % (3366378)Termination phase: Saturation
% 1.02/0.39 % (3366378)Time elapsed: 0.028 s
% 1.02/0.39 % (3366378)Peak memory usage: 13 MB
% 1.02/0.39 % (3366378)Instructions burned: 120 (million)
% 1.02/0.39 % (3366388)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2118761424:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.02/0.39 % (3366377)Instruction limit reached!
% 1.02/0.39 % (3366377)------------------------------
% 1.02/0.39 % (3366377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.39 % (3366377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.39 % (3366377)CaDiCaL version: 2.1.3
% 1.02/0.39 % (3366377)Termination reason: Instruction limit
% 1.02/0.39 % (3366377)Termination phase: Saturation
% 1.02/0.39 % (3366377)Time elapsed: 0.049 s
% 1.02/0.39 % (3366377)Peak memory usage: 13 MB
% 1.02/0.39 % (3366377)Instructions burned: 104 (million)
% 1.02/0.39 % Detected minimum model sizes of [8]
% 1.02/0.39 % Detected maximum model sizes of [max]
% 1.02/0.39 % TRYING [8]
% 1.02/0.39 % (3366379)Instruction limit reached!
% 1.02/0.39 % (3366379)------------------------------
% 1.02/0.39 % (3366379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.39 % (3366379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.39 % (3366379)CaDiCaL version: 2.1.3
% 1.02/0.39 % (3366379)Termination reason: Instruction limit
% 1.02/0.39 % (3366379)Termination phase: Saturation
% 1.02/0.39 % (3366379)Time elapsed: 0.064 s
% 1.02/0.39 % (3366379)Peak memory usage: 13 MB
% 1.02/0.39 % (3366379)Instructions burned: 131 (million)
% 1.02/0.39 % (3366390)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2720795822:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.02/0.39 % Detected minimum model sizes of [8]
% 1.02/0.39 % Detected maximum model sizes of [max]
% 1.02/0.39 % TRYING [8]
% 1.02/0.39 % (3366391)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=831964634:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.02/0.39 % (3366380)Instruction limit reached!
% 1.02/0.39 % (3366380)------------------------------
% 1.02/0.39 % (3366380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.39 % (3366380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.39 % (3366380)CaDiCaL version: 2.1.3
% 1.02/0.39 % (3366380)Termination reason: Instruction limit
% 1.02/0.39 % (3366380)Termination phase: Saturation
% 1.02/0.39 % (3366380)Time elapsed: 0.086 s
% 1.02/0.39 % (3366380)Peak memory usage: 15 MB
% 1.02/0.39 % (3366380)Instructions burned: 159 (million)
% 1.02/0.39 % (3366375) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3366369-3366375"...
% 1.02/0.39 % (3366394)ott-21_1_sil=16000:fs=off:random_seed=542062200:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.02/0.39 % (3366375)...printing done.
% 1.02/0.39 % (3366375)Refutation found. Thanks to Tanya!
% 1.02/0.39 % SZS status Theorem for theBenchmark
% 1.02/0.39 % SZS output start Proof for theBenchmark
% See solution above
% 1.02/0.40 % (3366375)------------------------------
% 1.02/0.40 % (3366375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.40 % (3366375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.40 % (3366375)CaDiCaL version: 2.1.3
% 1.02/0.40 % (3366375)Termination reason: Refutation
% 1.02/0.40 % (3366375)Time elapsed: 0.117 s
% 1.02/0.40 % (3366375)Peak memory usage: 15 MB
% 1.02/0.40 % (3366375)Instructions burned: 253 (million)
% 1.02/0.40 % (3366369)Success in time 0.165 s
% 1.02/0.40 % Vampire exiting
%------------------------------------------------------------------------------