%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG015+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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:04 AM UTC 2026
% Result : Theorem 2.70s 0.76s
% Output : Refutation 2.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 131
% Syntax : Number of formulae : 784 ( 182 unt; 110 def)
% Number of atoms : 3365 (1989 equ)
% Maximal formula atoms : 384 ( 4 avg)
% Number of connectives : 4077 (1496 ~;1650 |; 821 &)
% ( 110 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 118 ( 116 usr; 117 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e10) = e11
| op1(e10,e10) = e12
| op1(e10,e10) = e13 )
& ( op1(e10,e11) = e10
| op1(e10,e11) = e11
| op1(e10,e11) = e12
| op1(e10,e11) = e13 )
& ( op1(e10,e12) = e10
| op1(e10,e12) = e11
| op1(e10,e12) = e12
| op1(e10,e12) = e13 )
& ( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e12
| op1(e10,e13) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 )
& ( op1(e11,e11) = e10
| op1(e11,e11) = e11
| op1(e11,e11) = e12
| op1(e11,e11) = e13 )
& ( op1(e11,e12) = e10
| op1(e11,e12) = e11
| op1(e11,e12) = e12
| op1(e11,e12) = e13 )
& ( op1(e11,e13) = e10
| op1(e11,e13) = e11
| op1(e11,e13) = e12
| op1(e11,e13) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e10) = e11
| op1(e12,e10) = e12
| op1(e12,e10) = e13 )
& ( op1(e12,e11) = e10
| op1(e12,e11) = e11
| op1(e12,e11) = e12
| op1(e12,e11) = e13 )
& ( op1(e12,e12) = e10
| op1(e12,e12) = e11
| op1(e12,e12) = e12
| op1(e12,e12) = e13 )
& ( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12
| op1(e12,e13) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e10) = e11
| op1(e13,e10) = e12
| op1(e13,e10) = e13 )
& ( op1(e13,e11) = e10
| op1(e13,e11) = e11
| op1(e13,e11) = e12
| op1(e13,e11) = e13 )
& ( op1(e13,e12) = e10
| op1(e13,e12) = e11
| op1(e13,e12) = e12
| op1(e13,e12) = e13 )
& ( op1(e13,e13) = e10
| op1(e13,e13) = e11
| op1(e13,e13) = e12
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f3,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/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( op1(e10,inv1(e10)) = unit1
& op1(inv1(e10),e10) = unit1
& op1(e11,inv1(e11)) = unit1
& op1(inv1(e11),e11) = unit1
& op1(e12,inv1(e12)) = unit1
& op1(inv1(e12),e12) = unit1
& op1(e13,inv1(e13)) = unit1
& op1(inv1(e13),e13) = unit1
& ( inv1(e10) = e10
| inv1(e10) = e11
| inv1(e10) = e12
| inv1(e10) = e13 )
& ( inv1(e11) = e10
| inv1(e11) = e11
| inv1(e11) = e12
| inv1(e11) = e13 )
& ( inv1(e12) = e10
| inv1(e12) = e11
| inv1(e12) = e12
| inv1(e12) = e13 )
& ( inv1(e13) = e10
| inv1(e13) = e11
| inv1(e13) = e12
| inv1(e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e20) = e21
| op2(e20,e20) = e22
| op2(e20,e20) = e23 )
& ( op2(e20,e21) = e20
| op2(e20,e21) = e21
| op2(e20,e21) = e22
| op2(e20,e21) = e23 )
& ( op2(e20,e22) = e20
| op2(e20,e22) = e21
| op2(e20,e22) = e22
| op2(e20,e22) = e23 )
& ( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22
| op2(e20,e23) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e20) = e21
| op2(e21,e20) = e22
| op2(e21,e20) = e23 )
& ( op2(e21,e21) = e20
| op2(e21,e21) = e21
| op2(e21,e21) = e22
| op2(e21,e21) = e23 )
& ( op2(e21,e22) = e20
| op2(e21,e22) = e21
| op2(e21,e22) = e22
| op2(e21,e22) = e23 )
& ( op2(e21,e23) = e20
| op2(e21,e23) = e21
| op2(e21,e23) = e22
| op2(e21,e23) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e20) = e21
| op2(e22,e20) = e22
| op2(e22,e20) = e23 )
& ( op2(e22,e21) = e20
| op2(e22,e21) = e21
| op2(e22,e21) = e22
| op2(e22,e21) = e23 )
& ( op2(e22,e22) = e20
| op2(e22,e22) = e21
| op2(e22,e22) = e22
| op2(e22,e22) = e23 )
& ( op2(e22,e23) = e20
| op2(e22,e23) = e21
| op2(e22,e23) = e22
| op2(e22,e23) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e20) = e21
| op2(e23,e20) = e22
| op2(e23,e20) = e23 )
& ( op2(e23,e21) = e20
| op2(e23,e21) = e21
| op2(e23,e21) = e22
| op2(e23,e21) = e23 )
& ( op2(e23,e22) = e20
| op2(e23,e22) = e21
| op2(e23,e22) = e22
| op2(e23,e22) = e23 )
& ( op2(e23,e23) = e20
| op2(e23,e23) = e21
| op2(e23,e23) = e22
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f7,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/sandbox/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( op2(e20,inv2(e20)) = unit2
& op2(inv2(e20),e20) = unit2
& op2(e21,inv2(e21)) = unit2
& op2(inv2(e21),e21) = unit2
& op2(e22,inv2(e22)) = unit2
& op2(inv2(e22),e22) = unit2
& op2(e23,inv2(e23)) = unit2
& op2(inv2(e23),e23) = unit2
& ( inv2(e20) = e20
| inv2(e20) = e21
| inv2(e20) = e22
| inv2(e20) = e23 )
& ( inv2(e21) = e20
| inv2(e21) = e21
| inv2(e21) = e22
| inv2(e21) = e23 )
& ( inv2(e22) = e20
| inv2(e22) = e21
| inv2(e22) = e22
| inv2(e22) = e23 )
& ( inv2(e23) = e20
| inv2(e23) = e21
| inv2(e23) = e22
| inv2(e23) = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f9,axiom,
inv1(unit1) = unit1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax9) ).
fof(f13,axiom,
inv2(unit2) = unit2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f17,axiom,
( op1(e10,e10) != op1(e11,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e12,e10) != op1(e13,e10)
& op1(e10,e11) != op1(e11,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e12,e11) != op1(e13,e11)
& op1(e10,e12) != op1(e11,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e12,e12) != op1(e13,e12)
& op1(e10,e13) != op1(e11,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e12,e13) != op1(e13,e13)
& op1(e10,e10) != op1(e10,e11)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e12) != op1(e10,e13)
& op1(e11,e10) != op1(e11,e11)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e12) != op1(e11,e13)
& op1(e12,e10) != op1(e12,e11)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e12) != op1(e12,e13)
& op1(e13,e10) != op1(e13,e11)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e12) != op1(e13,e13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f18,axiom,
( op2(e20,e20) != op2(e21,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e22,e20) != op2(e23,e20)
& op2(e20,e21) != op2(e21,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e22,e21) != op2(e23,e21)
& op2(e20,e22) != op2(e21,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e22,e22) != op2(e23,e22)
& op2(e20,e23) != op2(e21,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e22,e23) != op2(e23,e23)
& op2(e20,e20) != op2(e20,e21)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e22) != op2(e20,e23)
& op2(e21,e20) != op2(e21,e21)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e22) != op2(e21,e23)
& op2(e22,e20) != op2(e22,e21)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e22) != op2(e22,e23)
& op2(e23,e20) != op2(e23,e21)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e22) != op2(e23,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
fof(f19,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax19) ).
fof(f20,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax20) ).
fof(f22,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/sandbox/benchmark/theBenchmark.p',ax22) ).
fof(f23,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/sandbox/benchmark/theBenchmark.p',ax23) ).
fof(f24,axiom,
( e10 = op1(e13,e13)
& e11 = op1(e12,e13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
fof(f25,axiom,
( e20 = op2(e23,e23)
& e21 = op2(e22,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax25) ).
fof(f28,axiom,
( h3(e12) = e20
& h3(e13) = e23
& h3(e10) = op2(e23,e23)
& h3(e11) = op2(e20,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax28) ).
fof(f31,axiom,
( h6(e12) = e21
& h6(e13) = e23
& h6(e10) = op2(e23,e23)
& h6(e11) = op2(e21,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax31) ).
fof(f33,axiom,
( h8(e12) = e22
& h8(e13) = e21
& h8(e10) = op2(e21,e21)
& h8(e11) = op2(e22,e21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax33) ).
fof(f34,axiom,
( h9(e12) = e22
& h9(e13) = e23
& h9(e10) = op2(e23,e23)
& h9(e11) = op2(e22,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax34) ).
fof(f38,conjecture,
( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) )
| ( h5(op1(e10,e10)) = op2(h5(e10),h5(e10))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& ( h5(e10) = e20
| h5(e11) = e20
| h5(e12) = e20
| h5(e13) = e20 )
& ( h5(e10) = e21
| h5(e11) = e21
| h5(e12) = e21
| h5(e13) = e21 )
& ( h5(e10) = e22
| h5(e11) = e22
| h5(e12) = e22
| h5(e13) = e22 )
& ( h5(e10) = e23
| h5(e11) = e23
| h5(e12) = e23
| h5(e13) = e23 ) )
| ( h6(op1(e10,e10)) = op2(h6(e10),h6(e10))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& ( h6(e10) = e20
| h6(e11) = e20
| h6(e12) = e20
| h6(e13) = e20 )
& ( h6(e10) = e21
| h6(e11) = e21
| h6(e12) = e21
| h6(e13) = e21 )
& ( h6(e10) = e22
| h6(e11) = e22
| h6(e12) = e22
| h6(e13) = e22 )
& ( h6(e10) = e23
| h6(e11) = e23
| h6(e12) = e23
| h6(e13) = e23 ) )
| ( h7(op1(e10,e10)) = op2(h7(e10),h7(e10))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& ( h7(e10) = e20
| h7(e11) = e20
| h7(e12) = e20
| h7(e13) = e20 )
& ( h7(e10) = e21
| h7(e11) = e21
| h7(e12) = e21
| h7(e13) = e21 )
& ( h7(e10) = e22
| h7(e11) = e22
| h7(e12) = e22
| h7(e13) = e22 )
& ( h7(e10) = e23
| h7(e11) = e23
| h7(e12) = e23
| h7(e13) = e23 ) )
| ( h8(op1(e10,e10)) = op2(h8(e10),h8(e10))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& ( h8(e10) = e20
| h8(e11) = e20
| h8(e12) = e20
| h8(e13) = e20 )
& ( h8(e10) = e21
| h8(e11) = e21
| h8(e12) = e21
| h8(e13) = e21 )
& ( h8(e10) = e22
| h8(e11) = e22
| h8(e12) = e22
| h8(e13) = e22 )
& ( h8(e10) = e23
| h8(e11) = e23
| h8(e12) = e23
| h8(e13) = e23 ) )
| ( h9(op1(e10,e10)) = op2(h9(e10),h9(e10))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& ( h9(e10) = e20
| h9(e11) = e20
| h9(e12) = e20
| h9(e13) = e20 )
& ( h9(e10) = e21
| h9(e11) = e21
| h9(e12) = e21
| h9(e13) = e21 )
& ( h9(e10) = e22
| h9(e11) = e22
| h9(e12) = e22
| h9(e13) = e22 )
& ( h9(e10) = e23
| h9(e11) = e23
| h9(e12) = e23
| h9(e13) = e23 ) )
| ( h10(op1(e10,e10)) = op2(h10(e10),h10(e10))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& ( h10(e10) = e20
| h10(e11) = e20
| h10(e12) = e20
| h10(e13) = e20 )
& ( h10(e10) = e21
| h10(e11) = e21
| h10(e12) = e21
| h10(e13) = e21 )
& ( h10(e10) = e22
| h10(e11) = e22
| h10(e12) = e22
| h10(e13) = e22 )
& ( h10(e10) = e23
| h10(e11) = e23
| h10(e12) = e23
| h10(e13) = e23 ) )
| ( h11(op1(e10,e10)) = op2(h11(e10),h11(e10))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& ( h11(e10) = e20
| h11(e11) = e20
| h11(e12) = e20
| h11(e13) = e20 )
& ( h11(e10) = e21
| h11(e11) = e21
| h11(e12) = e21
| h11(e13) = e21 )
& ( h11(e10) = e22
| h11(e11) = e22
| h11(e12) = e22
| h11(e13) = e22 )
& ( h11(e10) = e23
| h11(e11) = e23
| h11(e12) = e23
| h11(e13) = e23 ) )
| ( h12(op1(e10,e10)) = op2(h12(e10),h12(e10))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& ( h12(e10) = e20
| h12(e11) = e20
| h12(e12) = e20
| h12(e13) = e20 )
& ( h12(e10) = e21
| h12(e11) = e21
| h12(e12) = e21
| h12(e13) = e21 )
& ( h12(e10) = e22
| h12(e11) = e22
| h12(e12) = e22
| h12(e13) = e22 )
& ( h12(e10) = e23
| h12(e11) = e23
| h12(e12) = e23
| h12(e13) = e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f39,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)],[f38]) ).
fof(f42,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,[],[f39]) ).
fof(f49,plain,
( e13 = op1(e11,e12)
| e12 = op1(e11,e12)
| e11 = op1(e11,e12)
| e10 = op1(e11,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f50,plain,
( e13 = op1(e11,e13)
| e12 = op1(e11,e13)
| e11 = op1(e11,e13)
| e10 = op1(e11,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f52,plain,
( e13 = op1(e12,e11)
| e12 = op1(e12,e11)
| e11 = op1(e12,e11)
| e10 = op1(e12,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f56,plain,
( e13 = op1(e13,e11)
| e12 = op1(e13,e11)
| e11 = op1(e13,e11)
| e10 = op1(e13,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f57,plain,
( e13 = op1(e13,e12)
| e12 = op1(e13,e12)
| e11 = op1(e13,e12)
| e10 = op1(e13,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f123,plain,
( e13 = unit1
| e12 = unit1
| e11 = unit1
| e10 = unit1 ),
inference(cnf_transformation,[],[f3]) ).
fof(f124,plain,
e13 = op1(e13,unit1),
inference(cnf_transformation,[],[f3]) ).
fof(f125,plain,
e13 = op1(unit1,e13),
inference(cnf_transformation,[],[f3]) ).
fof(f126,plain,
e12 = op1(e12,unit1),
inference(cnf_transformation,[],[f3]) ).
fof(f127,plain,
e12 = op1(unit1,e12),
inference(cnf_transformation,[],[f3]) ).
fof(f128,plain,
e11 = op1(e11,unit1),
inference(cnf_transformation,[],[f3]) ).
fof(f129,plain,
e11 = op1(unit1,e11),
inference(cnf_transformation,[],[f3]) ).
fof(f138,plain,
unit1 = op1(inv1(e12),e12),
inference(cnf_transformation,[],[f4]) ).
fof(f150,plain,
( e23 = op2(e21,e22)
| e22 = op2(e21,e22)
| e21 = op2(e21,e22)
| e20 = op2(e21,e22) ),
inference(cnf_transformation,[],[f5]) ).
fof(f151,plain,
( e23 = op2(e21,e23)
| e22 = op2(e21,e23)
| e21 = op2(e21,e23)
| e20 = op2(e21,e23) ),
inference(cnf_transformation,[],[f5]) ).
fof(f153,plain,
( e23 = op2(e22,e21)
| e22 = op2(e22,e21)
| e21 = op2(e22,e21)
| e20 = op2(e22,e21) ),
inference(cnf_transformation,[],[f5]) ).
fof(f157,plain,
( e23 = op2(e23,e21)
| e22 = op2(e23,e21)
| e21 = op2(e23,e21)
| e20 = op2(e23,e21) ),
inference(cnf_transformation,[],[f5]) ).
fof(f158,plain,
( e23 = op2(e23,e22)
| e22 = op2(e23,e22)
| e21 = op2(e23,e22)
| e20 = op2(e23,e22) ),
inference(cnf_transformation,[],[f5]) ).
fof(f224,plain,
( e23 = unit2
| e22 = unit2
| e21 = unit2
| e20 = unit2 ),
inference(cnf_transformation,[],[f7]) ).
fof(f225,plain,
e23 = op2(e23,unit2),
inference(cnf_transformation,[],[f7]) ).
fof(f226,plain,
e23 = op2(unit2,e23),
inference(cnf_transformation,[],[f7]) ).
fof(f227,plain,
e22 = op2(e22,unit2),
inference(cnf_transformation,[],[f7]) ).
fof(f228,plain,
e22 = op2(unit2,e22),
inference(cnf_transformation,[],[f7]) ).
fof(f229,plain,
e21 = op2(e21,unit2),
inference(cnf_transformation,[],[f7]) ).
fof(f230,plain,
e21 = op2(unit2,e21),
inference(cnf_transformation,[],[f7]) ).
fof(f239,plain,
unit2 = op2(inv2(e22),e22),
inference(cnf_transformation,[],[f8]) ).
fof(f245,plain,
unit1 = inv1(unit1),
inference(cnf_transformation,[],[f9]) ).
fof(f268,plain,
unit2 = inv2(unit2),
inference(cnf_transformation,[],[f13]) ).
fof(f291,plain,
op1(e13,e12) != op1(e13,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f292,plain,
op1(e13,e11) != op1(e13,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f295,plain,
op1(e13,e10) != op1(e13,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f296,plain,
op1(e13,e10) != op1(e13,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f298,plain,
op1(e12,e11) != op1(e12,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f299,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f302,plain,
op1(e12,e10) != op1(e12,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f303,plain,
op1(e11,e12) != op1(e11,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f304,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f305,plain,
op1(e11,e11) != op1(e11,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f307,plain,
op1(e11,e10) != op1(e11,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f317,plain,
op1(e11,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f320,plain,
op1(e10,e13) != op1(e11,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f324,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f330,plain,
op1(e10,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f339,plain,
op2(e23,e22) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f340,plain,
op2(e23,e21) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f341,plain,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f343,plain,
op2(e23,e20) != op2(e23,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f344,plain,
op2(e23,e20) != op2(e23,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f346,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f347,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f350,plain,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f351,plain,
op2(e21,e22) != op2(e21,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f353,plain,
op2(e21,e21) != op2(e21,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f355,plain,
op2(e21,e20) != op2(e21,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f364,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f365,plain,
op2(e21,e23) != op2(e22,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f368,plain,
op2(e20,e23) != op2(e21,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f372,plain,
op2(e20,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f390,plain,
e10 != e13,
inference(cnf_transformation,[],[f19]) ).
fof(f391,plain,
e10 != e12,
inference(cnf_transformation,[],[f19]) ).
fof(f392,plain,
e10 != e11,
inference(cnf_transformation,[],[f19]) ).
fof(f396,plain,
e20 != e23,
inference(cnf_transformation,[],[f20]) ).
fof(f397,plain,
e20 != e22,
inference(cnf_transformation,[],[f20]) ).
fof(f398,plain,
e20 != e21,
inference(cnf_transformation,[],[f20]) ).
fof(f416,plain,
( e10 = op1(e12,e12)
| ~ sP1 ),
inference(cnf_transformation,[],[f22]) ).
fof(f417,plain,
( e10 = op1(e11,e11)
| ~ sP1 ),
inference(cnf_transformation,[],[f22]) ).
fof(f418,plain,
( e10 = op1(e10,e10)
| ~ sP1 ),
inference(cnf_transformation,[],[f22]) ).
fof(f419,plain,
( e11 = op1(e13,e13)
| ~ sP0 ),
inference(cnf_transformation,[],[f22]) ).
fof(f435,plain,
( e13 = op1(e13,e13)
| e12 = op1(e13,e13)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f22]) ).
fof(f440,plain,
( e20 = op2(e22,e22)
| ~ sP3 ),
inference(cnf_transformation,[],[f23]) ).
fof(f441,plain,
( e20 = op2(e21,e21)
| ~ sP3 ),
inference(cnf_transformation,[],[f23]) ).
fof(f442,plain,
( e20 = op2(e20,e20)
| ~ sP3 ),
inference(cnf_transformation,[],[f23]) ).
fof(f443,plain,
( e21 = op2(e23,e23)
| ~ sP2 ),
inference(cnf_transformation,[],[f23]) ).
fof(f459,plain,
( e23 = op2(e23,e23)
| e22 = op2(e23,e23)
| sP2
| sP3 ),
inference(cnf_transformation,[],[f23]) ).
fof(f463,plain,
e11 = op1(e12,e13),
inference(cnf_transformation,[],[f24]) ).
fof(f464,plain,
e10 = op1(e13,e13),
inference(cnf_transformation,[],[f24]) ).
fof(f465,plain,
e21 = op2(e22,e23),
inference(cnf_transformation,[],[f25]) ).
fof(f466,plain,
e20 = op2(e23,e23),
inference(cnf_transformation,[],[f25]) ).
fof(f478,plain,
e20 = h3(e12),
inference(cnf_transformation,[],[f28]) ).
fof(f489,plain,
e23 = h6(e13),
inference(cnf_transformation,[],[f31]) ).
fof(f498,plain,
e22 = h8(e12),
inference(cnf_transformation,[],[f33]) ).
fof(f499,plain,
op2(e22,e23) = h9(e11),
inference(cnf_transformation,[],[f34]) ).
fof(f500,plain,
op2(e23,e23) = h9(e10),
inference(cnf_transformation,[],[f34]) ).
fof(f501,plain,
e23 = h9(e13),
inference(cnf_transformation,[],[f34]) ).
fof(f502,plain,
e22 = h9(e12),
inference(cnf_transformation,[],[f34]) ).
fof(f582,plain,
( e20 != h9(e10)
| ~ sP11 ),
inference(cnf_transformation,[],[f42]) ).
fof(f585,plain,
( e21 != h9(e11)
| ~ sP10 ),
inference(cnf_transformation,[],[f42]) ).
fof(f752,plain,
( e23 != h9(e13)
| e22 != h9(e12)
| sP10
| sP11
| h9(op1(e13,e13)) != op2(h9(e13),h9(e13))
| h9(op1(e13,e12)) != op2(h9(e13),h9(e12))
| h9(op1(e13,e11)) != op2(h9(e13),h9(e11))
| h9(op1(e13,e10)) != op2(h9(e13),h9(e10))
| h9(op1(e12,e13)) != op2(h9(e12),h9(e13))
| h9(op1(e12,e12)) != op2(h9(e12),h9(e12))
| h9(op1(e12,e11)) != op2(h9(e12),h9(e11))
| h9(op1(e12,e10)) != op2(h9(e12),h9(e10))
| h9(op1(e11,e13)) != op2(h9(e11),h9(e13))
| h9(op1(e11,e12)) != op2(h9(e11),h9(e12))
| h9(op1(e11,e11)) != op2(h9(e11),h9(e11))
| h9(op1(e11,e10)) != op2(h9(e11),h9(e10))
| h9(op1(e10,e13)) != op2(h9(e10),h9(e13))
| h9(op1(e10,e12)) != op2(h9(e10),h9(e12))
| h9(op1(e10,e11)) != op2(h9(e10),h9(e11))
| h9(op1(e10,e10)) != op2(h9(e10),h9(e10)) ),
inference(cnf_transformation,[],[f42]) ).
fof(f806,plain,
( e23 = op2(e23,e23)
| e22 = op2(e23,e23)
| ~ sP2
| ~ sP3 ),
inference(consistent_polarity_flipping,[],[f459]) ).
fof(f822,plain,
( e21 = op2(e23,e23)
| sP2 ),
inference(consistent_polarity_flipping,[],[f443]) ).
fof(f823,plain,
( e20 = op2(e20,e20)
| sP3 ),
inference(consistent_polarity_flipping,[],[f442]) ).
fof(f824,plain,
( e20 = op2(e21,e21)
| sP3 ),
inference(consistent_polarity_flipping,[],[f441]) ).
fof(f825,plain,
( e20 = op2(e22,e22)
| sP3 ),
inference(consistent_polarity_flipping,[],[f440]) ).
fof(f861,plain,
( e23 != h9(e13)
| e22 != h9(e12)
| ~ sP10
| sP11
| h9(op1(e13,e13)) != op2(h9(e13),h9(e13))
| h9(op1(e13,e12)) != op2(h9(e13),h9(e12))
| h9(op1(e13,e11)) != op2(h9(e13),h9(e11))
| h9(op1(e13,e10)) != op2(h9(e13),h9(e10))
| h9(op1(e12,e13)) != op2(h9(e12),h9(e13))
| h9(op1(e12,e12)) != op2(h9(e12),h9(e12))
| h9(op1(e12,e11)) != op2(h9(e12),h9(e11))
| h9(op1(e12,e10)) != op2(h9(e12),h9(e10))
| h9(op1(e11,e13)) != op2(h9(e11),h9(e13))
| h9(op1(e11,e12)) != op2(h9(e11),h9(e12))
| h9(op1(e11,e11)) != op2(h9(e11),h9(e11))
| h9(op1(e11,e10)) != op2(h9(e11),h9(e10))
| h9(op1(e10,e13)) != op2(h9(e10),h9(e13))
| h9(op1(e10,e12)) != op2(h9(e10),h9(e12))
| h9(op1(e10,e11)) != op2(h9(e10),h9(e11))
| h9(op1(e10,e10)) != op2(h9(e10),h9(e10)) ),
inference(consistent_polarity_flipping,[],[f752]) ).
fof(f964,plain,
( e21 != h9(e11)
| sP10 ),
inference(consistent_polarity_flipping,[],[f585]) ).
fof(f1101,definition,
( spl28_23
<=> e20 = h3(e12) ),
introduced(definition,[new_symbols(definition,[spl28_23])],[avatar_definition]) ).
fof(f1102,plain,
( e20 = h3(e12)
| ~ spl28_23 ),
inference(avatar_component_clause,[],[f1101]) ).
fof(f1125,definition,
( spl28_28
<=> e21 = h3(e12) ),
introduced(definition,[new_symbols(definition,[spl28_28])],[avatar_definition]) ).
fof(f1126,plain,
( e21 = h3(e12)
| ~ spl28_28 ),
inference(avatar_component_clause,[],[f1125]) ).
fof(f1127,plain,
( e21 != h3(e12)
| spl28_28 ),
inference(avatar_component_clause,[],[f1125]) ).
fof(f1240,definition,
( spl28_52
<=> e20 = h6(e13) ),
introduced(definition,[new_symbols(definition,[spl28_52])],[avatar_definition]) ).
fof(f1241,plain,
( e20 = h6(e13)
| ~ spl28_52 ),
inference(avatar_component_clause,[],[f1240]) ).
fof(f1242,plain,
( e20 != h6(e13)
| spl28_52 ),
inference(avatar_component_clause,[],[f1240]) ).
fof(f1341,definition,
( spl28_73
<=> e20 = h8(e12) ),
introduced(definition,[new_symbols(definition,[spl28_73])],[avatar_definition]) ).
fof(f1342,plain,
( e20 = h8(e12)
| ~ spl28_73 ),
inference(avatar_component_clause,[],[f1341]) ).
fof(f1343,plain,
( e20 != h8(e12)
| spl28_73 ),
inference(avatar_component_clause,[],[f1341]) ).
fof(f1380,definition,
( spl28_81
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl28_81])],[avatar_definition]) ).
fof(f1399,definition,
( spl28_85
<=> e20 = h9(e10) ),
introduced(definition,[new_symbols(definition,[spl28_85])],[avatar_definition]) ).
fof(f1400,plain,
( e20 = h9(e10)
| ~ spl28_85 ),
inference(avatar_component_clause,[],[f1399]) ).
fof(f1402,plain,
( ~ spl28_81
| ~ spl28_85 ),
inference(avatar_split_clause,[],[f582,f1399,f1380]) ).
fof(f1404,definition,
( spl28_86
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl28_86])],[avatar_definition]) ).
fof(f1418,definition,
( spl28_89
<=> e21 = h9(e11) ),
introduced(definition,[new_symbols(definition,[spl28_89])],[avatar_definition]) ).
fof(f1419,plain,
( e21 = h9(e11)
| ~ spl28_89 ),
inference(avatar_component_clause,[],[f1418]) ).
fof(f1421,plain,
( spl28_86
| ~ spl28_89 ),
inference(avatar_split_clause,[],[f964,f1418,f1404]) ).
fof(f2236,definition,
( spl28_264
<=> e23 = h6(e13) ),
introduced(definition,[new_symbols(definition,[spl28_264])],[avatar_definition]) ).
fof(f2237,plain,
( e23 = h6(e13)
| ~ spl28_264 ),
inference(avatar_component_clause,[],[f2236]) ).
fof(f2429,definition,
( spl28_307
<=> e22 = h8(e12) ),
introduced(definition,[new_symbols(definition,[spl28_307])],[avatar_definition]) ).
fof(f2430,plain,
( e22 = h8(e12)
| ~ spl28_307 ),
inference(avatar_component_clause,[],[f2429]) ).
fof(f2468,definition,
( spl28_313
<=> h9(op1(e10,e10)) = op2(h9(e10),h9(e10)) ),
introduced(definition,[new_symbols(definition,[spl28_313])],[avatar_definition]) ).
fof(f2470,plain,
( h9(op1(e10,e10)) != op2(h9(e10),h9(e10))
| spl28_313 ),
inference(avatar_component_clause,[],[f2468]) ).
fof(f2472,definition,
( spl28_314
<=> h9(op1(e10,e11)) = op2(h9(e10),h9(e11)) ),
introduced(definition,[new_symbols(definition,[spl28_314])],[avatar_definition]) ).
fof(f2474,plain,
( h9(op1(e10,e11)) != op2(h9(e10),h9(e11))
| spl28_314 ),
inference(avatar_component_clause,[],[f2472]) ).
fof(f2476,definition,
( spl28_315
<=> h9(op1(e10,e12)) = op2(h9(e10),h9(e12)) ),
introduced(definition,[new_symbols(definition,[spl28_315])],[avatar_definition]) ).
fof(f2478,plain,
( h9(op1(e10,e12)) != op2(h9(e10),h9(e12))
| spl28_315 ),
inference(avatar_component_clause,[],[f2476]) ).
fof(f2480,definition,
( spl28_316
<=> h9(op1(e10,e13)) = op2(h9(e10),h9(e13)) ),
introduced(definition,[new_symbols(definition,[spl28_316])],[avatar_definition]) ).
fof(f2482,plain,
( h9(op1(e10,e13)) != op2(h9(e10),h9(e13))
| spl28_316 ),
inference(avatar_component_clause,[],[f2480]) ).
fof(f2484,definition,
( spl28_317
<=> h9(op1(e11,e10)) = op2(h9(e11),h9(e10)) ),
introduced(definition,[new_symbols(definition,[spl28_317])],[avatar_definition]) ).
fof(f2486,plain,
( h9(op1(e11,e10)) != op2(h9(e11),h9(e10))
| spl28_317 ),
inference(avatar_component_clause,[],[f2484]) ).
fof(f2488,definition,
( spl28_318
<=> h9(op1(e11,e11)) = op2(h9(e11),h9(e11)) ),
introduced(definition,[new_symbols(definition,[spl28_318])],[avatar_definition]) ).
fof(f2490,plain,
( h9(op1(e11,e11)) != op2(h9(e11),h9(e11))
| spl28_318 ),
inference(avatar_component_clause,[],[f2488]) ).
fof(f2492,definition,
( spl28_319
<=> h9(op1(e11,e12)) = op2(h9(e11),h9(e12)) ),
introduced(definition,[new_symbols(definition,[spl28_319])],[avatar_definition]) ).
fof(f2494,plain,
( h9(op1(e11,e12)) != op2(h9(e11),h9(e12))
| spl28_319 ),
inference(avatar_component_clause,[],[f2492]) ).
fof(f2496,definition,
( spl28_320
<=> h9(op1(e11,e13)) = op2(h9(e11),h9(e13)) ),
introduced(definition,[new_symbols(definition,[spl28_320])],[avatar_definition]) ).
fof(f2498,plain,
( h9(op1(e11,e13)) != op2(h9(e11),h9(e13))
| spl28_320 ),
inference(avatar_component_clause,[],[f2496]) ).
fof(f2500,definition,
( spl28_321
<=> h9(op1(e12,e10)) = op2(h9(e12),h9(e10)) ),
introduced(definition,[new_symbols(definition,[spl28_321])],[avatar_definition]) ).
fof(f2502,plain,
( h9(op1(e12,e10)) != op2(h9(e12),h9(e10))
| spl28_321 ),
inference(avatar_component_clause,[],[f2500]) ).
fof(f2504,definition,
( spl28_322
<=> h9(op1(e12,e11)) = op2(h9(e12),h9(e11)) ),
introduced(definition,[new_symbols(definition,[spl28_322])],[avatar_definition]) ).
fof(f2506,plain,
( h9(op1(e12,e11)) != op2(h9(e12),h9(e11))
| spl28_322 ),
inference(avatar_component_clause,[],[f2504]) ).
fof(f2508,definition,
( spl28_323
<=> h9(op1(e12,e12)) = op2(h9(e12),h9(e12)) ),
introduced(definition,[new_symbols(definition,[spl28_323])],[avatar_definition]) ).
fof(f2510,plain,
( h9(op1(e12,e12)) != op2(h9(e12),h9(e12))
| spl28_323 ),
inference(avatar_component_clause,[],[f2508]) ).
fof(f2512,definition,
( spl28_324
<=> h9(op1(e12,e13)) = op2(h9(e12),h9(e13)) ),
introduced(definition,[new_symbols(definition,[spl28_324])],[avatar_definition]) ).
fof(f2514,plain,
( h9(op1(e12,e13)) != op2(h9(e12),h9(e13))
| spl28_324 ),
inference(avatar_component_clause,[],[f2512]) ).
fof(f2516,definition,
( spl28_325
<=> h9(op1(e13,e10)) = op2(h9(e13),h9(e10)) ),
introduced(definition,[new_symbols(definition,[spl28_325])],[avatar_definition]) ).
fof(f2518,plain,
( h9(op1(e13,e10)) != op2(h9(e13),h9(e10))
| spl28_325 ),
inference(avatar_component_clause,[],[f2516]) ).
fof(f2520,definition,
( spl28_326
<=> h9(op1(e13,e11)) = op2(h9(e13),h9(e11)) ),
introduced(definition,[new_symbols(definition,[spl28_326])],[avatar_definition]) ).
fof(f2522,plain,
( h9(op1(e13,e11)) != op2(h9(e13),h9(e11))
| spl28_326 ),
inference(avatar_component_clause,[],[f2520]) ).
fof(f2524,definition,
( spl28_327
<=> h9(op1(e13,e12)) = op2(h9(e13),h9(e12)) ),
introduced(definition,[new_symbols(definition,[spl28_327])],[avatar_definition]) ).
fof(f2526,plain,
( h9(op1(e13,e12)) != op2(h9(e13),h9(e12))
| spl28_327 ),
inference(avatar_component_clause,[],[f2524]) ).
fof(f2528,definition,
( spl28_328
<=> h9(op1(e13,e13)) = op2(h9(e13),h9(e13)) ),
introduced(definition,[new_symbols(definition,[spl28_328])],[avatar_definition]) ).
fof(f2530,plain,
( h9(op1(e13,e13)) != op2(h9(e13),h9(e13))
| spl28_328 ),
inference(avatar_component_clause,[],[f2528]) ).
fof(f2541,definition,
( spl28_331
<=> e22 = h9(e12) ),
introduced(definition,[new_symbols(definition,[spl28_331])],[avatar_definition]) ).
fof(f2542,plain,
( e22 = h9(e12)
| ~ spl28_331 ),
inference(avatar_component_clause,[],[f2541]) ).
fof(f2572,definition,
( spl28_336
<=> e23 = h9(e13) ),
introduced(definition,[new_symbols(definition,[spl28_336])],[avatar_definition]) ).
fof(f2573,plain,
( e23 = h9(e13)
| ~ spl28_336 ),
inference(avatar_component_clause,[],[f2572]) ).
fof(f2576,plain,
( ~ spl28_313
| ~ spl28_314
| ~ spl28_315
| ~ spl28_316
| ~ spl28_317
| ~ spl28_318
| ~ spl28_319
| ~ spl28_320
| ~ spl28_321
| ~ spl28_322
| ~ spl28_323
| ~ spl28_324
| ~ spl28_325
| ~ spl28_326
| ~ spl28_327
| ~ spl28_328
| spl28_81
| ~ spl28_86
| ~ spl28_331
| ~ spl28_336 ),
inference(avatar_split_clause,[],[f861,f2572,f2541,f1404,f1380,f2528,f2524,f2520,f2516,f2512,f2508,f2504,f2500,f2496,f2492,f2488,f2484,f2480,f2476,f2472,f2468]) ).
fof(f2921,plain,
spl28_336,
inference(avatar_split_clause,[],[f501,f2572]) ).
fof(f2922,plain,
spl28_331,
inference(avatar_split_clause,[],[f502,f2541]) ).
fof(f2924,plain,
spl28_307,
inference(avatar_split_clause,[],[f498,f2429]) ).
fof(f2927,plain,
spl28_264,
inference(avatar_split_clause,[],[f489,f2236]) ).
fof(f2934,plain,
spl28_23,
inference(avatar_split_clause,[],[f478,f1101]) ).
fof(f2940,definition,
( spl28_409
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl28_409])],[avatar_definition]) ).
fof(f2944,definition,
( spl28_410
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl28_410])],[avatar_definition]) ).
fof(f2946,plain,
( e20 = op2(e23,e23)
| ~ spl28_410 ),
inference(avatar_component_clause,[],[f2944]) ).
fof(f2949,definition,
( spl28_411
<=> e20 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl28_411])],[avatar_definition]) ).
fof(f2951,plain,
( e20 = op2(e22,e22)
| ~ spl28_411 ),
inference(avatar_component_clause,[],[f2949]) ).
fof(f2952,plain,
( spl28_409
| spl28_411 ),
inference(avatar_split_clause,[],[f825,f2949,f2940]) ).
fof(f2954,definition,
( spl28_412
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl28_412])],[avatar_definition]) ).
fof(f2956,plain,
( e20 = op2(e21,e21)
| ~ spl28_412 ),
inference(avatar_component_clause,[],[f2954]) ).
fof(f2957,plain,
( spl28_409
| spl28_412 ),
inference(avatar_split_clause,[],[f824,f2954,f2940]) ).
fof(f2959,definition,
( spl28_413
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl28_413])],[avatar_definition]) ).
fof(f2961,plain,
( e20 = op2(e20,e20)
| ~ spl28_413 ),
inference(avatar_component_clause,[],[f2959]) ).
fof(f2962,plain,
( spl28_409
| spl28_413 ),
inference(avatar_split_clause,[],[f823,f2959,f2940]) ).
fof(f2964,definition,
( spl28_414
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl28_414])],[avatar_definition]) ).
fof(f2968,definition,
( spl28_415
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl28_415])],[avatar_definition]) ).
fof(f2970,plain,
( e21 = op2(e23,e23)
| ~ spl28_415 ),
inference(avatar_component_clause,[],[f2968]) ).
fof(f2971,plain,
( spl28_414
| spl28_415 ),
inference(avatar_split_clause,[],[f822,f2968,f2964]) ).
fof(f2988,definition,
( spl28_419
<=> e22 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl28_419])],[avatar_definition]) ).
fof(f2990,plain,
( e22 = op2(e23,e23)
| ~ spl28_419 ),
inference(avatar_component_clause,[],[f2988]) ).
fof(f3028,definition,
( spl28_426
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl28_426])],[avatar_definition]) ).
fof(f3030,plain,
( e23 = op2(e23,e23)
| ~ spl28_426 ),
inference(avatar_component_clause,[],[f3028]) ).
fof(f3031,plain,
( ~ spl28_409
| ~ spl28_414
| spl28_419
| spl28_426 ),
inference(avatar_split_clause,[],[f806,f3028,f2988,f2964,f2940]) ).
fof(f3036,definition,
( spl28_427
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl28_427])],[avatar_definition]) ).
fof(f3040,definition,
( spl28_428
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl28_428])],[avatar_definition]) ).
fof(f3042,plain,
( e10 = op1(e13,e13)
| ~ spl28_428 ),
inference(avatar_component_clause,[],[f3040]) ).
fof(f3045,definition,
( spl28_429
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl28_429])],[avatar_definition]) ).
fof(f3047,plain,
( e10 = op1(e12,e12)
| ~ spl28_429 ),
inference(avatar_component_clause,[],[f3045]) ).
fof(f3048,plain,
( ~ spl28_427
| spl28_429 ),
inference(avatar_split_clause,[],[f416,f3045,f3036]) ).
fof(f3050,definition,
( spl28_430
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl28_430])],[avatar_definition]) ).
fof(f3052,plain,
( e10 = op1(e11,e11)
| ~ spl28_430 ),
inference(avatar_component_clause,[],[f3050]) ).
fof(f3053,plain,
( ~ spl28_427
| spl28_430 ),
inference(avatar_split_clause,[],[f417,f3050,f3036]) ).
fof(f3055,definition,
( spl28_431
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl28_431])],[avatar_definition]) ).
fof(f3057,plain,
( e10 = op1(e10,e10)
| ~ spl28_431 ),
inference(avatar_component_clause,[],[f3055]) ).
fof(f3058,plain,
( ~ spl28_427
| spl28_431 ),
inference(avatar_split_clause,[],[f418,f3055,f3036]) ).
fof(f3060,definition,
( spl28_432
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl28_432])],[avatar_definition]) ).
fof(f3064,definition,
( spl28_433
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl28_433])],[avatar_definition]) ).
fof(f3066,plain,
( e11 = op1(e13,e13)
| ~ spl28_433 ),
inference(avatar_component_clause,[],[f3064]) ).
fof(f3067,plain,
( ~ spl28_432
| spl28_433 ),
inference(avatar_split_clause,[],[f419,f3064,f3060]) ).
fof(f3084,definition,
( spl28_437
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl28_437])],[avatar_definition]) ).
fof(f3086,plain,
( e12 = op1(e13,e13)
| ~ spl28_437 ),
inference(avatar_component_clause,[],[f3084]) ).
fof(f3124,definition,
( spl28_444
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl28_444])],[avatar_definition]) ).
fof(f3126,plain,
( e13 = op1(e13,e13)
| ~ spl28_444 ),
inference(avatar_component_clause,[],[f3124]) ).
fof(f3127,plain,
( spl28_427
| spl28_432
| spl28_437
| spl28_444 ),
inference(avatar_split_clause,[],[f435,f3124,f3084,f3060,f3036]) ).
fof(f3262,definition,
( spl28_471
<=> e22 = inv2(e22) ),
introduced(definition,[new_symbols(definition,[spl28_471])],[avatar_definition]) ).
fof(f3264,plain,
( e22 = inv2(e22)
| ~ spl28_471 ),
inference(avatar_component_clause,[],[f3262]) ).
fof(f3272,definition,
( spl28_473
<=> e20 = unit2 ),
introduced(definition,[new_symbols(definition,[spl28_473])],[avatar_definition]) ).
fof(f3274,plain,
( e20 = unit2
| ~ spl28_473 ),
inference(avatar_component_clause,[],[f3272]) ).
fof(f3276,definition,
( spl28_474
<=> e21 = unit2 ),
introduced(definition,[new_symbols(definition,[spl28_474])],[avatar_definition]) ).
fof(f3278,plain,
( e21 = unit2
| ~ spl28_474 ),
inference(avatar_component_clause,[],[f3276]) ).
fof(f3280,definition,
( spl28_475
<=> e22 = unit2 ),
introduced(definition,[new_symbols(definition,[spl28_475])],[avatar_definition]) ).
fof(f3282,plain,
( e22 = unit2
| ~ spl28_475 ),
inference(avatar_component_clause,[],[f3280]) ).
fof(f3284,definition,
( spl28_476
<=> e23 = unit2 ),
introduced(definition,[new_symbols(definition,[spl28_476])],[avatar_definition]) ).
fof(f3286,plain,
( e23 = unit2
| ~ spl28_476 ),
inference(avatar_component_clause,[],[f3284]) ).
fof(f3287,plain,
( spl28_473
| spl28_474
| spl28_475
| spl28_476 ),
inference(avatar_split_clause,[],[f224,f3284,f3280,f3276,f3272]) ).
fof(f3294,definition,
( spl28_478
<=> e21 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl28_478])],[avatar_definition]) ).
fof(f3315,definition,
( spl28_483
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl28_483])],[avatar_definition]) ).
fof(f3317,plain,
( e22 = op2(e20,e22)
| ~ spl28_483 ),
inference(avatar_component_clause,[],[f3315]) ).
fof(f3336,definition,
( spl28_488
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl28_488])],[avatar_definition]) ).
fof(f3338,plain,
( e23 = op2(e20,e23)
| ~ spl28_488 ),
inference(avatar_component_clause,[],[f3336]) ).
fof(f3345,definition,
( spl28_490
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl28_490])],[avatar_definition]) ).
fof(f3347,plain,
( e21 = op2(e21,e20)
| ~ spl28_490 ),
inference(avatar_component_clause,[],[f3345]) ).
fof(f3359,definition,
( spl28_493
<=> e20 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl28_493])],[avatar_definition]) ).
fof(f3361,plain,
( e20 = op2(e21,e22)
| ~ spl28_493 ),
inference(avatar_component_clause,[],[f3359]) ).
fof(f3363,definition,
( spl28_494
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl28_494])],[avatar_definition]) ).
fof(f3367,definition,
( spl28_495
<=> e22 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl28_495])],[avatar_definition]) ).
fof(f3369,plain,
( e22 = op2(e21,e22)
| ~ spl28_495 ),
inference(avatar_component_clause,[],[f3367]) ).
fof(f3371,definition,
( spl28_496
<=> e23 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl28_496])],[avatar_definition]) ).
fof(f3374,plain,
( spl28_493
| spl28_494
| spl28_495
| spl28_496 ),
inference(avatar_split_clause,[],[f150,f3371,f3367,f3363,f3359]) ).
fof(f3376,definition,
( spl28_497
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl28_497])],[avatar_definition]) ).
fof(f3380,definition,
( spl28_498
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl28_498])],[avatar_definition]) ).
fof(f3384,definition,
( spl28_499
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl28_499])],[avatar_definition]) ).
fof(f3388,definition,
( spl28_500
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl28_500])],[avatar_definition]) ).
fof(f3391,plain,
( spl28_497
| spl28_498
| spl28_499
| spl28_500 ),
inference(avatar_split_clause,[],[f151,f3388,f3384,f3380,f3376]) ).
fof(f3401,definition,
( spl28_503
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl28_503])],[avatar_definition]) ).
fof(f3403,plain,
( e22 = op2(e22,e20)
| ~ spl28_503 ),
inference(avatar_component_clause,[],[f3401]) ).
fof(f3410,definition,
( spl28_505
<=> e20 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl28_505])],[avatar_definition]) ).
fof(f3414,definition,
( spl28_506
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl28_506])],[avatar_definition]) ).
fof(f3418,definition,
( spl28_507
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl28_507])],[avatar_definition]) ).
fof(f3422,definition,
( spl28_508
<=> e23 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl28_508])],[avatar_definition]) ).
fof(f3425,plain,
( spl28_505
| spl28_506
| spl28_507
| spl28_508 ),
inference(avatar_split_clause,[],[f153,f3422,f3418,f3414,f3410]) ).
fof(f3432,definition,
( spl28_510
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl28_510])],[avatar_definition]) ).
fof(f3434,plain,
( e21 = op2(e22,e23)
| ~ spl28_510 ),
inference(avatar_component_clause,[],[f3432]) ).
fof(f3457,definition,
( spl28_516
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl28_516])],[avatar_definition]) ).
fof(f3459,plain,
( e23 = op2(e23,e20)
| ~ spl28_516 ),
inference(avatar_component_clause,[],[f3457]) ).
fof(f3462,definition,
( spl28_517
<=> e20 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl28_517])],[avatar_definition]) ).
fof(f3466,definition,
( spl28_518
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl28_518])],[avatar_definition]) ).
fof(f3468,plain,
( e21 = op2(e23,e21)
| ~ spl28_518 ),
inference(avatar_component_clause,[],[f3466]) ).
fof(f3470,definition,
( spl28_519
<=> e22 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl28_519])],[avatar_definition]) ).
fof(f3474,definition,
( spl28_520
<=> e23 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl28_520])],[avatar_definition]) ).
fof(f3477,plain,
( spl28_517
| spl28_518
| spl28_519
| spl28_520 ),
inference(avatar_split_clause,[],[f157,f3474,f3470,f3466,f3462]) ).
fof(f3479,definition,
( spl28_521
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl28_521])],[avatar_definition]) ).
fof(f3483,definition,
( spl28_522
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl28_522])],[avatar_definition]) ).
fof(f3487,definition,
( spl28_523
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl28_523])],[avatar_definition]) ).
fof(f3491,definition,
( spl28_524
<=> e23 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl28_524])],[avatar_definition]) ).
fof(f3494,plain,
( spl28_521
| spl28_522
| spl28_523
| spl28_524 ),
inference(avatar_split_clause,[],[f158,f3491,f3487,f3483,f3479]) ).
fof(f3507,definition,
( spl28_527
<=> e12 = inv1(e12) ),
introduced(definition,[new_symbols(definition,[spl28_527])],[avatar_definition]) ).
fof(f3509,plain,
( e12 = inv1(e12)
| ~ spl28_527 ),
inference(avatar_component_clause,[],[f3507]) ).
fof(f3517,definition,
( spl28_529
<=> e10 = unit1 ),
introduced(definition,[new_symbols(definition,[spl28_529])],[avatar_definition]) ).
fof(f3519,plain,
( e10 = unit1
| ~ spl28_529 ),
inference(avatar_component_clause,[],[f3517]) ).
fof(f3521,definition,
( spl28_530
<=> e11 = unit1 ),
introduced(definition,[new_symbols(definition,[spl28_530])],[avatar_definition]) ).
fof(f3523,plain,
( e11 = unit1
| ~ spl28_530 ),
inference(avatar_component_clause,[],[f3521]) ).
fof(f3525,definition,
( spl28_531
<=> e12 = unit1 ),
introduced(definition,[new_symbols(definition,[spl28_531])],[avatar_definition]) ).
fof(f3527,plain,
( e12 = unit1
| ~ spl28_531 ),
inference(avatar_component_clause,[],[f3525]) ).
fof(f3529,definition,
( spl28_532
<=> e13 = unit1 ),
introduced(definition,[new_symbols(definition,[spl28_532])],[avatar_definition]) ).
fof(f3531,plain,
( e13 = unit1
| ~ spl28_532 ),
inference(avatar_component_clause,[],[f3529]) ).
fof(f3532,plain,
( spl28_529
| spl28_530
| spl28_531
| spl28_532 ),
inference(avatar_split_clause,[],[f123,f3529,f3525,f3521,f3517]) ).
fof(f3539,definition,
( spl28_534
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl28_534])],[avatar_definition]) ).
fof(f3541,plain,
( e11 = op1(e10,e11)
| ~ spl28_534 ),
inference(avatar_component_clause,[],[f3539]) ).
fof(f3560,definition,
( spl28_539
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl28_539])],[avatar_definition]) ).
fof(f3562,plain,
( e12 = op1(e10,e12)
| ~ spl28_539 ),
inference(avatar_component_clause,[],[f3560]) ).
fof(f3581,definition,
( spl28_544
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl28_544])],[avatar_definition]) ).
fof(f3583,plain,
( e13 = op1(e10,e13)
| ~ spl28_544 ),
inference(avatar_component_clause,[],[f3581]) ).
fof(f3590,definition,
( spl28_546
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl28_546])],[avatar_definition]) ).
fof(f3592,plain,
( e11 = op1(e11,e10)
| ~ spl28_546 ),
inference(avatar_component_clause,[],[f3590]) ).
fof(f3604,definition,
( spl28_549
<=> e10 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl28_549])],[avatar_definition]) ).
fof(f3608,definition,
( spl28_550
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl28_550])],[avatar_definition]) ).
fof(f3612,definition,
( spl28_551
<=> e12 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl28_551])],[avatar_definition]) ).
fof(f3614,plain,
( e12 = op1(e11,e12)
| ~ spl28_551 ),
inference(avatar_component_clause,[],[f3612]) ).
fof(f3616,definition,
( spl28_552
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl28_552])],[avatar_definition]) ).
fof(f3618,plain,
( e13 = op1(e11,e12)
| ~ spl28_552 ),
inference(avatar_component_clause,[],[f3616]) ).
fof(f3619,plain,
( spl28_549
| spl28_550
| spl28_551
| spl28_552 ),
inference(avatar_split_clause,[],[f49,f3616,f3612,f3608,f3604]) ).
fof(f3621,definition,
( spl28_553
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl28_553])],[avatar_definition]) ).
fof(f3625,definition,
( spl28_554
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl28_554])],[avatar_definition]) ).
fof(f3629,definition,
( spl28_555
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl28_555])],[avatar_definition]) ).
fof(f3631,plain,
( e12 = op1(e11,e13)
| ~ spl28_555 ),
inference(avatar_component_clause,[],[f3629]) ).
fof(f3633,definition,
( spl28_556
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl28_556])],[avatar_definition]) ).
fof(f3636,plain,
( spl28_553
| spl28_554
| spl28_555
| spl28_556 ),
inference(avatar_split_clause,[],[f50,f3633,f3629,f3625,f3621]) ).
fof(f3646,definition,
( spl28_559
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl28_559])],[avatar_definition]) ).
fof(f3648,plain,
( e12 = op1(e12,e10)
| ~ spl28_559 ),
inference(avatar_component_clause,[],[f3646]) ).
fof(f3655,definition,
( spl28_561
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl28_561])],[avatar_definition]) ).
fof(f3659,definition,
( spl28_562
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl28_562])],[avatar_definition]) ).
fof(f3663,definition,
( spl28_563
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl28_563])],[avatar_definition]) ).
fof(f3667,definition,
( spl28_564
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl28_564])],[avatar_definition]) ).
fof(f3669,plain,
( e13 = op1(e12,e11)
| ~ spl28_564 ),
inference(avatar_component_clause,[],[f3667]) ).
fof(f3670,plain,
( spl28_561
| spl28_562
| spl28_563
| spl28_564 ),
inference(avatar_split_clause,[],[f52,f3667,f3663,f3659,f3655]) ).
fof(f3677,definition,
( spl28_566
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl28_566])],[avatar_definition]) ).
fof(f3679,plain,
( e11 = op1(e12,e13)
| ~ spl28_566 ),
inference(avatar_component_clause,[],[f3677]) ).
fof(f3702,definition,
( spl28_572
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl28_572])],[avatar_definition]) ).
fof(f3704,plain,
( e13 = op1(e13,e10)
| ~ spl28_572 ),
inference(avatar_component_clause,[],[f3702]) ).
fof(f3707,definition,
( spl28_573
<=> e10 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl28_573])],[avatar_definition]) ).
fof(f3711,definition,
( spl28_574
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl28_574])],[avatar_definition]) ).
fof(f3715,definition,
( spl28_575
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl28_575])],[avatar_definition]) ).
fof(f3717,plain,
( e12 = op1(e13,e11)
| ~ spl28_575 ),
inference(avatar_component_clause,[],[f3715]) ).
fof(f3719,definition,
( spl28_576
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl28_576])],[avatar_definition]) ).
fof(f3722,plain,
( spl28_573
| spl28_574
| spl28_575
| spl28_576 ),
inference(avatar_split_clause,[],[f56,f3719,f3715,f3711,f3707]) ).
fof(f3724,definition,
( spl28_577
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl28_577])],[avatar_definition]) ).
fof(f3728,definition,
( spl28_578
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl28_578])],[avatar_definition]) ).
fof(f3730,plain,
( e11 = op1(e13,e12)
| ~ spl28_578 ),
inference(avatar_component_clause,[],[f3728]) ).
fof(f3732,definition,
( spl28_579
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl28_579])],[avatar_definition]) ).
fof(f3736,definition,
( spl28_580
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl28_580])],[avatar_definition]) ).
fof(f3739,plain,
( spl28_577
| spl28_578
| spl28_579
| spl28_580 ),
inference(avatar_split_clause,[],[f57,f3736,f3732,f3728,f3724]) ).
fof(f3741,plain,
( e20 != e21
| ~ spl28_23
| spl28_28 ),
inference(forward_demodulation,[],[f1127,f1102]) ).
fof(f3746,plain,
( e20 != e23
| spl28_52
| ~ spl28_264 ),
inference(superposition,[],[f1242,f2237]) ).
fof(f3754,plain,
( h9(op1(e12,e11)) != op2(e22,h9(e11))
| spl28_322
| ~ spl28_331 ),
inference(forward_demodulation,[],[f2506,f2542]) ).
fof(f3780,plain,
( e20 = e21
| ~ spl28_23
| ~ spl28_28 ),
inference(forward_demodulation,[],[f1126,f1102]) ).
fof(f3795,plain,
( $false
| ~ spl28_23
| ~ spl28_28 ),
inference(forward_subsumption_resolution,[],[f398,f3780]) ).
fof(f3796,plain,
( ~ spl28_23
| ~ spl28_28 ),
inference(avatar_contradiction_clause,[],[f3795]) ).
fof(f3835,plain,
( e20 = e22
| ~ spl28_73
| ~ spl28_307 ),
inference(forward_demodulation,[],[f1342,f2430]) ).
fof(f3844,plain,
( e20 != e22
| spl28_73
| ~ spl28_307 ),
inference(forward_demodulation,[],[f1343,f2430]) ).
fof(f3874,plain,
( e12 = inv1(e12)
| ~ spl28_531 ),
inference(forward_demodulation,[],[f245,f3527]) ).
fof(f3875,plain,
( spl28_527
| ~ spl28_531 ),
inference(avatar_split_clause,[],[f3874,f3525,f3507]) ).
fof(f3887,plain,
( e11 = op1(e11,e13)
| ~ spl28_532 ),
inference(forward_demodulation,[],[f128,f3531]) ).
fof(f3888,plain,
( spl28_554
| ~ spl28_532 ),
inference(avatar_split_clause,[],[f3887,f3529,f3625]) ).
fof(f3899,plain,
( e22 = inv2(e22)
| ~ spl28_475 ),
inference(forward_demodulation,[],[f268,f3282]) ).
fof(f3900,plain,
( spl28_471
| ~ spl28_475 ),
inference(avatar_split_clause,[],[f3899,f3280,f3262]) ).
fof(f3931,plain,
( e21 = op2(e21,e23)
| ~ spl28_476 ),
inference(forward_demodulation,[],[f229,f3286]) ).
fof(f3932,plain,
( spl28_498
| ~ spl28_476 ),
inference(avatar_split_clause,[],[f3931,f3284,f3380]) ).
fof(f3963,plain,
spl28_566,
inference(avatar_split_clause,[],[f463,f3677]) ).
fof(f3964,plain,
spl28_428,
inference(avatar_split_clause,[],[f464,f3040]) ).
fof(f3965,plain,
spl28_510,
inference(avatar_split_clause,[],[f465,f3432]) ).
fof(f3966,plain,
spl28_410,
inference(avatar_split_clause,[],[f466,f2944]) ).
fof(f3967,plain,
( e20 = e23
| ~ spl28_410
| ~ spl28_426 ),
inference(superposition,[],[f3030,f2946]) ).
fof(f3971,plain,
( $false
| spl28_52
| ~ spl28_264
| ~ spl28_410
| ~ spl28_426 ),
inference(forward_subsumption_resolution,[],[f3967,f3746]) ).
fof(f3972,plain,
( spl28_52
| ~ spl28_264
| ~ spl28_410
| ~ spl28_426 ),
inference(avatar_contradiction_clause,[],[f3971]) ).
fof(f3973,plain,
( e20 = e23
| ~ spl28_52
| ~ spl28_264 ),
inference(forward_demodulation,[],[f1241,f2237]) ).
fof(f3995,plain,
( e21 = op2(e21,e21)
| ~ spl28_474 ),
inference(forward_demodulation,[],[f229,f3278]) ).
fof(f3996,plain,
( e20 = e21
| ~ spl28_412
| ~ spl28_474 ),
inference(forward_demodulation,[],[f3995,f2956]) ).
fof(f3997,plain,
( $false
| ~ spl28_23
| spl28_28
| ~ spl28_412
| ~ spl28_474 ),
inference(forward_subsumption_resolution,[],[f3996,f3741]) ).
fof(f3998,plain,
( ~ spl28_23
| spl28_28
| ~ spl28_412
| ~ spl28_474 ),
inference(avatar_contradiction_clause,[],[f3997]) ).
fof(f3999,plain,
( e20 = e21
| ~ spl28_410
| ~ spl28_415 ),
inference(forward_demodulation,[],[f2970,f2946]) ).
fof(f4003,plain,
( $false
| ~ spl28_23
| spl28_28
| ~ spl28_410
| ~ spl28_415 ),
inference(forward_subsumption_resolution,[],[f3999,f3741]) ).
fof(f4004,plain,
( ~ spl28_23
| spl28_28
| ~ spl28_410
| ~ spl28_415 ),
inference(avatar_contradiction_clause,[],[f4003]) ).
fof(f4018,plain,
( e20 = e22
| ~ spl28_410
| ~ spl28_419 ),
inference(superposition,[],[f2990,f2946]) ).
fof(f4022,plain,
( $false
| spl28_73
| ~ spl28_307
| ~ spl28_410
| ~ spl28_419 ),
inference(forward_subsumption_resolution,[],[f4018,f3844]) ).
fof(f4023,plain,
( spl28_73
| ~ spl28_307
| ~ spl28_410
| ~ spl28_419 ),
inference(avatar_contradiction_clause,[],[f4022]) ).
fof(f4046,plain,
( $false
| ~ spl28_52
| ~ spl28_264 ),
inference(forward_subsumption_resolution,[],[f396,f3973]) ).
fof(f4047,plain,
( ~ spl28_52
| ~ spl28_264 ),
inference(avatar_contradiction_clause,[],[f4046]) ).
fof(f4064,plain,
( e23 = op2(e23,e20)
| ~ spl28_473 ),
inference(forward_demodulation,[],[f225,f3274]) ).
fof(f4065,plain,
( spl28_516
| ~ spl28_473 ),
inference(avatar_split_clause,[],[f4064,f3272,f3457]) ).
fof(f4066,plain,
( e23 = op2(e20,e23)
| ~ spl28_473 ),
inference(forward_demodulation,[],[f226,f3274]) ).
fof(f4067,plain,
( spl28_488
| ~ spl28_473 ),
inference(avatar_split_clause,[],[f4066,f3272,f3336]) ).
fof(f4068,plain,
( e22 = op2(e22,e20)
| ~ spl28_473 ),
inference(forward_demodulation,[],[f227,f3274]) ).
fof(f4069,plain,
( spl28_503
| ~ spl28_473 ),
inference(avatar_split_clause,[],[f4068,f3272,f3401]) ).
fof(f4070,plain,
( e22 = op2(e20,e22)
| ~ spl28_473 ),
inference(forward_demodulation,[],[f228,f3274]) ).
fof(f4071,plain,
( spl28_483
| ~ spl28_473 ),
inference(avatar_split_clause,[],[f4070,f3272,f3315]) ).
fof(f4072,plain,
( e21 = op2(e21,e20)
| ~ spl28_473 ),
inference(forward_demodulation,[],[f229,f3274]) ).
fof(f4073,plain,
( spl28_490
| ~ spl28_473 ),
inference(avatar_split_clause,[],[f4072,f3272,f3345]) ).
fof(f4074,plain,
( e21 = op2(e20,e21)
| ~ spl28_473 ),
inference(forward_demodulation,[],[f230,f3274]) ).
fof(f4075,plain,
( spl28_478
| ~ spl28_473 ),
inference(avatar_split_clause,[],[f4074,f3272,f3294]) ).
fof(f4122,plain,
( e10 = e13
| ~ spl28_428
| ~ spl28_444 ),
inference(superposition,[],[f3126,f3042]) ).
fof(f4126,plain,
( $false
| ~ spl28_428
| ~ spl28_444 ),
inference(forward_subsumption_resolution,[],[f4122,f390]) ).
fof(f4127,plain,
( ~ spl28_428
| ~ spl28_444 ),
inference(avatar_contradiction_clause,[],[f4126]) ).
fof(f4138,plain,
( e11 = op1(e11,e11)
| ~ spl28_530 ),
inference(forward_demodulation,[],[f128,f3523]) ).
fof(f4139,plain,
( e10 = e11
| ~ spl28_430
| ~ spl28_530 ),
inference(forward_demodulation,[],[f4138,f3052]) ).
fof(f4140,plain,
( $false
| ~ spl28_430
| ~ spl28_530 ),
inference(forward_subsumption_resolution,[],[f4139,f392]) ).
fof(f4141,plain,
( ~ spl28_430
| ~ spl28_530 ),
inference(avatar_contradiction_clause,[],[f4140]) ).
fof(f4142,plain,
( e10 = e11
| ~ spl28_428
| ~ spl28_433 ),
inference(forward_demodulation,[],[f3066,f3042]) ).
fof(f4146,plain,
( $false
| ~ spl28_428
| ~ spl28_433 ),
inference(forward_subsumption_resolution,[],[f4142,f392]) ).
fof(f4147,plain,
( ~ spl28_428
| ~ spl28_433 ),
inference(avatar_contradiction_clause,[],[f4146]) ).
fof(f4161,plain,
( e10 = e12
| ~ spl28_428
| ~ spl28_437 ),
inference(superposition,[],[f3086,f3042]) ).
fof(f4165,plain,
( $false
| ~ spl28_428
| ~ spl28_437 ),
inference(forward_subsumption_resolution,[],[f4161,f391]) ).
fof(f4166,plain,
( ~ spl28_428
| ~ spl28_437 ),
inference(avatar_contradiction_clause,[],[f4165]) ).
fof(f4182,plain,
( e13 = op1(e13,e10)
| ~ spl28_529 ),
inference(forward_demodulation,[],[f124,f3519]) ).
fof(f4183,plain,
( spl28_572
| ~ spl28_529 ),
inference(avatar_split_clause,[],[f4182,f3517,f3702]) ).
fof(f4184,plain,
( e13 = op1(e10,e13)
| ~ spl28_529 ),
inference(forward_demodulation,[],[f125,f3519]) ).
fof(f4185,plain,
( spl28_544
| ~ spl28_529 ),
inference(avatar_split_clause,[],[f4184,f3517,f3581]) ).
fof(f4186,plain,
( e12 = op1(e12,e10)
| ~ spl28_529 ),
inference(forward_demodulation,[],[f126,f3519]) ).
fof(f4187,plain,
( spl28_559
| ~ spl28_529 ),
inference(avatar_split_clause,[],[f4186,f3517,f3646]) ).
fof(f4188,plain,
( e12 = op1(e10,e12)
| ~ spl28_529 ),
inference(forward_demodulation,[],[f127,f3519]) ).
fof(f4189,plain,
( spl28_539
| ~ spl28_529 ),
inference(avatar_split_clause,[],[f4188,f3517,f3560]) ).
fof(f4190,plain,
( e11 = op1(e11,e10)
| ~ spl28_529 ),
inference(forward_demodulation,[],[f128,f3519]) ).
fof(f4191,plain,
( spl28_546
| ~ spl28_529 ),
inference(avatar_split_clause,[],[f4190,f3517,f3590]) ).
fof(f4192,plain,
( e11 = op1(e10,e11)
| ~ spl28_529 ),
inference(forward_demodulation,[],[f129,f3519]) ).
fof(f4193,plain,
( spl28_534
| ~ spl28_529 ),
inference(avatar_split_clause,[],[f4192,f3517,f3539]) ).
fof(f4457,plain,
( h9(e13) != op2(e22,h9(e11))
| spl28_322
| ~ spl28_331
| ~ spl28_564 ),
inference(superposition,[],[f3754,f3669]) ).
fof(f4458,plain,
( e23 != op2(e22,h9(e11))
| spl28_322
| ~ spl28_331
| ~ spl28_336
| ~ spl28_564 ),
inference(forward_demodulation,[],[f4457,f2573]) ).
fof(f4518,plain,
( op2(e22,e22) = unit2
| ~ spl28_471 ),
inference(forward_demodulation,[],[f239,f3264]) ).
fof(f5107,plain,
( e21 = h9(e11)
| ~ spl28_510 ),
inference(forward_demodulation,[],[f499,f3434]) ).
fof(f5110,plain,
( spl28_89
| ~ spl28_510 ),
inference(avatar_split_clause,[],[f5107,f3432,f1418]) ).
fof(f5113,plain,
( e20 = h9(e10)
| ~ spl28_410 ),
inference(forward_demodulation,[],[f500,f2946]) ).
fof(f5114,plain,
( spl28_85
| ~ spl28_410 ),
inference(avatar_split_clause,[],[f5113,f2944,f1399]) ).
fof(f5275,plain,
( e10 != op1(e13,e12)
| ~ spl28_428 ),
inference(forward_demodulation,[],[f291,f3042]) ).
fof(f5278,plain,
( ~ spl28_577
| ~ spl28_428 ),
inference(avatar_split_clause,[],[f5275,f3040,f3724]) ).
fof(f5280,plain,
( e10 != op1(e13,e11)
| ~ spl28_428 ),
inference(forward_demodulation,[],[f292,f3042]) ).
fof(f5283,plain,
( ~ spl28_573
| ~ spl28_428 ),
inference(avatar_split_clause,[],[f5280,f3040,f3707]) ).
fof(f5297,plain,
( e11 != op1(e12,e11)
| ~ spl28_566 ),
inference(forward_demodulation,[],[f298,f3679]) ).
fof(f5299,plain,
( e10 != op1(e12,e11)
| ~ spl28_429 ),
inference(forward_demodulation,[],[f299,f3047]) ).
fof(f5302,plain,
( ~ spl28_562
| ~ spl28_566 ),
inference(avatar_split_clause,[],[f5297,f3677,f3659]) ).
fof(f5303,plain,
( ~ spl28_561
| ~ spl28_429 ),
inference(avatar_split_clause,[],[f5299,f3045,f3655]) ).
fof(f5314,plain,
( e23 != op2(e22,e21)
| ~ spl28_89
| spl28_322
| ~ spl28_331
| ~ spl28_336
| ~ spl28_564 ),
inference(forward_demodulation,[],[f4458,f1419]) ).
fof(f5328,plain,
( ~ spl28_508
| ~ spl28_89
| spl28_322
| ~ spl28_331
| ~ spl28_336
| ~ spl28_564 ),
inference(avatar_split_clause,[],[f5314,f3667,f2572,f2541,f2504,f1418,f3422]) ).
fof(f5356,plain,
( op1(e12,e12) = unit1
| ~ spl28_527 ),
inference(forward_demodulation,[],[f138,f3509]) ).
fof(f5371,plain,
( e10 = unit1
| ~ spl28_429
| ~ spl28_527 ),
inference(forward_demodulation,[],[f5356,f3047]) ).
fof(f5374,plain,
( spl28_529
| ~ spl28_429
| ~ spl28_527 ),
inference(avatar_split_clause,[],[f5371,f3507,f3045,f3517]) ).
fof(f5737,plain,
( e12 != op1(e11,e13)
| ~ spl28_551 ),
inference(forward_demodulation,[],[f303,f3614]) ).
fof(f5740,plain,
( e10 != op1(e11,e13)
| ~ spl28_430 ),
inference(forward_demodulation,[],[f304,f3052]) ).
fof(f5741,plain,
( ~ spl28_555
| ~ spl28_551 ),
inference(avatar_split_clause,[],[f5737,f3612,f3629]) ).
fof(f5742,plain,
( ~ spl28_553
| ~ spl28_430 ),
inference(avatar_split_clause,[],[f5740,f3050,f3621]) ).
fof(f5765,plain,
( e12 != op1(e12,e11)
| ~ spl28_559 ),
inference(forward_demodulation,[],[f302,f3648]) ).
fof(f5776,plain,
( ~ spl28_563
| ~ spl28_559 ),
inference(avatar_split_clause,[],[f5765,f3646,f3663]) ).
fof(f5793,plain,
( h9(op1(e10,e11)) != op2(h9(e10),e21)
| ~ spl28_89
| spl28_314 ),
inference(forward_demodulation,[],[f2474,f1419]) ).
fof(f5810,plain,
( op2(e20,e21) != h9(op1(e10,e11))
| ~ spl28_85
| ~ spl28_89
| spl28_314 ),
inference(forward_demodulation,[],[f5793,f1400]) ).
fof(f5817,plain,
( op2(e20,e21) != h9(e11)
| ~ spl28_85
| ~ spl28_89
| spl28_314
| ~ spl28_534 ),
inference(forward_demodulation,[],[f5810,f3541]) ).
fof(f5819,plain,
( e21 != op2(e20,e21)
| ~ spl28_85
| ~ spl28_89
| spl28_314
| ~ spl28_534 ),
inference(forward_demodulation,[],[f5817,f1419]) ).
fof(f5822,plain,
( op2(e20,e20) != h9(op1(e10,e10))
| ~ spl28_85
| spl28_313 ),
inference(forward_demodulation,[],[f2470,f1400]) ).
fof(f5824,plain,
( op2(e20,e20) != h9(e10)
| ~ spl28_85
| spl28_313
| ~ spl28_431 ),
inference(forward_demodulation,[],[f5822,f3057]) ).
fof(f5826,plain,
( e20 != op2(e20,e20)
| ~ spl28_85
| spl28_313
| ~ spl28_431 ),
inference(forward_demodulation,[],[f5824,f1400]) ).
fof(f5828,plain,
( $false
| ~ spl28_85
| spl28_313
| ~ spl28_413
| ~ spl28_431 ),
inference(forward_subsumption_resolution,[],[f5826,f2961]) ).
fof(f5829,plain,
( ~ spl28_85
| spl28_313
| ~ spl28_413
| ~ spl28_431 ),
inference(avatar_contradiction_clause,[],[f5828]) ).
fof(f5832,plain,
( h9(op1(e10,e12)) != op2(h9(e10),e22)
| spl28_315
| ~ spl28_331 ),
inference(forward_demodulation,[],[f2478,f2542]) ).
fof(f5834,plain,
( op2(e20,e22) != h9(op1(e10,e12))
| ~ spl28_85
| spl28_315
| ~ spl28_331 ),
inference(forward_demodulation,[],[f5832,f1400]) ).
fof(f5836,plain,
( op2(e20,e22) != h9(e12)
| ~ spl28_85
| spl28_315
| ~ spl28_331
| ~ spl28_539 ),
inference(forward_demodulation,[],[f5834,f3562]) ).
fof(f5837,plain,
( e22 != op2(e20,e22)
| ~ spl28_85
| spl28_315
| ~ spl28_331
| ~ spl28_539 ),
inference(forward_demodulation,[],[f5836,f2542]) ).
fof(f5838,plain,
( $false
| ~ spl28_85
| spl28_315
| ~ spl28_331
| ~ spl28_483
| ~ spl28_539 ),
inference(forward_subsumption_resolution,[],[f5837,f3317]) ).
fof(f5839,plain,
( ~ spl28_85
| spl28_315
| ~ spl28_331
| ~ spl28_483
| ~ spl28_539 ),
inference(avatar_contradiction_clause,[],[f5838]) ).
fof(f5841,plain,
( h9(op1(e10,e13)) != op2(h9(e10),e23)
| spl28_316
| ~ spl28_336 ),
inference(forward_demodulation,[],[f2482,f2573]) ).
fof(f5843,plain,
( op2(e20,e23) != h9(op1(e10,e13))
| ~ spl28_85
| spl28_316
| ~ spl28_336 ),
inference(forward_demodulation,[],[f5841,f1400]) ).
fof(f5845,plain,
( op2(e20,e23) != h9(e13)
| ~ spl28_85
| spl28_316
| ~ spl28_336
| ~ spl28_544 ),
inference(forward_demodulation,[],[f5843,f3583]) ).
fof(f5847,plain,
( e23 != op2(e20,e23)
| ~ spl28_85
| spl28_316
| ~ spl28_336
| ~ spl28_544 ),
inference(forward_demodulation,[],[f5845,f2573]) ).
fof(f5848,plain,
( $false
| ~ spl28_85
| spl28_316
| ~ spl28_336
| ~ spl28_488
| ~ spl28_544 ),
inference(forward_subsumption_resolution,[],[f5847,f3338]) ).
fof(f5849,plain,
( ~ spl28_85
| spl28_316
| ~ spl28_336
| ~ spl28_488
| ~ spl28_544 ),
inference(avatar_contradiction_clause,[],[f5848]) ).
fof(f5851,plain,
( h9(op1(e11,e10)) != op2(h9(e11),e20)
| ~ spl28_85
| spl28_317 ),
inference(forward_demodulation,[],[f2486,f1400]) ).
fof(f5853,plain,
( op2(e21,e20) != h9(op1(e11,e10))
| ~ spl28_85
| ~ spl28_89
| spl28_317 ),
inference(forward_demodulation,[],[f5851,f1419]) ).
fof(f5855,plain,
( op2(e21,e20) != h9(e11)
| ~ spl28_85
| ~ spl28_89
| spl28_317
| ~ spl28_546 ),
inference(forward_demodulation,[],[f5853,f3592]) ).
fof(f5857,plain,
( e21 != op2(e21,e20)
| ~ spl28_85
| ~ spl28_89
| spl28_317
| ~ spl28_546 ),
inference(forward_demodulation,[],[f5855,f1419]) ).
fof(f5861,plain,
( op2(e21,e21) != h9(op1(e11,e11))
| ~ spl28_89
| spl28_318 ),
inference(forward_demodulation,[],[f2490,f1419]) ).
fof(f5863,plain,
( op2(e21,e21) != h9(e10)
| ~ spl28_89
| spl28_318
| ~ spl28_430 ),
inference(forward_demodulation,[],[f5861,f3052]) ).
fof(f5865,plain,
( e20 != op2(e21,e21)
| ~ spl28_85
| ~ spl28_89
| spl28_318
| ~ spl28_430 ),
inference(forward_demodulation,[],[f5863,f1400]) ).
fof(f5870,plain,
( h9(op1(e11,e12)) != op2(h9(e11),e22)
| spl28_319
| ~ spl28_331 ),
inference(forward_demodulation,[],[f2494,f2542]) ).
fof(f5872,plain,
( op2(e21,e22) != h9(op1(e11,e12))
| ~ spl28_89
| spl28_319
| ~ spl28_331 ),
inference(forward_demodulation,[],[f5870,f1419]) ).
fof(f5919,plain,
( h9(op1(e11,e13)) != op2(h9(e11),e23)
| spl28_320
| ~ spl28_336 ),
inference(forward_demodulation,[],[f2498,f2573]) ).
fof(f5921,plain,
( op2(e21,e23) != h9(op1(e11,e13))
| ~ spl28_89
| spl28_320
| ~ spl28_336 ),
inference(forward_demodulation,[],[f5919,f1419]) ).
fof(f5982,plain,
( e11 != op1(e11,e13)
| ~ spl28_566 ),
inference(forward_demodulation,[],[f317,f3679]) ).
fof(f6027,plain,
( e13 != op1(e11,e13)
| ~ spl28_544 ),
inference(forward_demodulation,[],[f320,f3583]) ).
fof(f6029,plain,
( e10 != op1(e11,e12)
| ~ spl28_430 ),
inference(forward_demodulation,[],[f305,f3052]) ).
fof(f6030,plain,
( e11 != op1(e11,e12)
| ~ spl28_546 ),
inference(forward_demodulation,[],[f307,f3592]) ).
fof(f6043,plain,
( ~ spl28_556
| ~ spl28_544 ),
inference(avatar_split_clause,[],[f6027,f3581,f3633]) ).
fof(f6044,plain,
( ~ spl28_549
| ~ spl28_430 ),
inference(avatar_split_clause,[],[f6029,f3050,f3604]) ).
fof(f6094,plain,
( op2(e21,e22) != h9(e13)
| ~ spl28_89
| spl28_319
| ~ spl28_331
| ~ spl28_552 ),
inference(forward_demodulation,[],[f5872,f3618]) ).
fof(f6100,plain,
( e23 != op2(e21,e22)
| ~ spl28_89
| spl28_319
| ~ spl28_331
| ~ spl28_336
| ~ spl28_552 ),
inference(forward_demodulation,[],[f6094,f2573]) ).
fof(f6106,plain,
( ~ spl28_496
| ~ spl28_89
| spl28_319
| ~ spl28_331
| ~ spl28_336
| ~ spl28_552 ),
inference(avatar_split_clause,[],[f6100,f3616,f2572,f2541,f2492,f1418,f3371]) ).
fof(f6204,plain,
( ~ spl28_554
| ~ spl28_566 ),
inference(avatar_split_clause,[],[f5982,f3677,f3625]) ).
fof(f6509,plain,
( e13 != op1(e13,e12)
| ~ spl28_572 ),
inference(forward_demodulation,[],[f295,f3704]) ).
fof(f6511,plain,
( e13 != op1(e13,e11)
| ~ spl28_572 ),
inference(forward_demodulation,[],[f296,f3704]) ).
fof(f6520,plain,
( ~ spl28_580
| ~ spl28_572 ),
inference(avatar_split_clause,[],[f6509,f3702,f3736]) ).
fof(f6597,plain,
( ~ spl28_576
| ~ spl28_572 ),
inference(avatar_split_clause,[],[f6511,f3702,f3719]) ).
fof(f6842,plain,
( e20 != op2(e23,e22)
| ~ spl28_410 ),
inference(forward_demodulation,[],[f339,f2946]) ).
fof(f6844,plain,
( e20 != op2(e23,e21)
| ~ spl28_410 ),
inference(forward_demodulation,[],[f340,f2946]) ).
fof(f6855,plain,
( ~ spl28_517
| ~ spl28_410 ),
inference(avatar_split_clause,[],[f6844,f2944,f3462]) ).
fof(f6856,plain,
( e20 = unit2
| ~ spl28_411
| ~ spl28_471 ),
inference(forward_demodulation,[],[f4518,f2951]) ).
fof(f6867,plain,
( spl28_473
| ~ spl28_411
| ~ spl28_471 ),
inference(avatar_split_clause,[],[f6856,f3262,f2949,f3272]) ).
fof(f6896,plain,
( op2(e21,e23) != h9(e12)
| ~ spl28_89
| spl28_320
| ~ spl28_336
| ~ spl28_555 ),
inference(forward_demodulation,[],[f5921,f3631]) ).
fof(f7000,plain,
( e22 != op2(e21,e23)
| ~ spl28_89
| spl28_320
| ~ spl28_331
| ~ spl28_336
| ~ spl28_555 ),
inference(forward_demodulation,[],[f6896,f2542]) ).
fof(f7031,plain,
( ~ spl28_499
| ~ spl28_89
| spl28_320
| ~ spl28_331
| ~ spl28_336
| ~ spl28_555 ),
inference(avatar_split_clause,[],[f7000,f3629,f2572,f2541,f2496,f1418,f3384]) ).
fof(f7077,plain,
( ~ spl28_478
| ~ spl28_85
| ~ spl28_89
| spl28_314
| ~ spl28_534 ),
inference(avatar_split_clause,[],[f5819,f3539,f2472,f1418,f1399,f3294]) ).
fof(f7081,plain,
( ~ spl28_490
| ~ spl28_85
| ~ spl28_89
| spl28_317
| ~ spl28_546 ),
inference(avatar_split_clause,[],[f5857,f3590,f2484,f1418,f1399,f3345]) ).
fof(f7085,plain,
( ~ spl28_412
| ~ spl28_85
| ~ spl28_89
| spl28_318
| ~ spl28_430 ),
inference(avatar_split_clause,[],[f5865,f3050,f2488,f1418,f1399,f2954]) ).
fof(f7106,plain,
( ~ spl28_550
| ~ spl28_546 ),
inference(avatar_split_clause,[],[f6030,f3590,f3608]) ).
fof(f7724,plain,
( $false
| ~ spl28_73
| ~ spl28_307 ),
inference(forward_subsumption_resolution,[],[f397,f3835]) ).
fof(f7725,plain,
( ~ spl28_73
| ~ spl28_307 ),
inference(avatar_contradiction_clause,[],[f7724]) ).
fof(f8578,plain,
( e23 != op2(e23,e21)
| ~ spl28_516 ),
inference(forward_demodulation,[],[f344,f3459]) ).
fof(f8579,plain,
( ~ spl28_520
| ~ spl28_516 ),
inference(avatar_split_clause,[],[f8578,f3457,f3474]) ).
fof(f8604,plain,
( e21 != op2(e22,e21)
| ~ spl28_510 ),
inference(forward_demodulation,[],[f346,f3434]) ).
fof(f8605,plain,
( e20 != op2(e22,e21)
| ~ spl28_411 ),
inference(forward_demodulation,[],[f347,f2951]) ).
fof(f8625,plain,
( e22 != op2(e22,e21)
| ~ spl28_503 ),
inference(forward_demodulation,[],[f350,f3403]) ).
fof(f8626,plain,
( ~ spl28_505
| ~ spl28_411 ),
inference(avatar_split_clause,[],[f8605,f2949,f3410]) ).
fof(f8635,plain,
( ~ spl28_507
| ~ spl28_503 ),
inference(avatar_split_clause,[],[f8625,f3401,f3418]) ).
fof(f8649,plain,
( ~ spl28_506
| ~ spl28_510 ),
inference(avatar_split_clause,[],[f8604,f3432,f3414]) ).
fof(f8887,plain,
( e20 != op2(e21,e21)
| ~ spl28_493 ),
inference(forward_demodulation,[],[f353,f3361]) ).
fof(f8888,plain,
( $false
| ~ spl28_412
| ~ spl28_493 ),
inference(forward_subsumption_resolution,[],[f8887,f2956]) ).
fof(f8889,plain,
( ~ spl28_412
| ~ spl28_493 ),
inference(avatar_contradiction_clause,[],[f8888]) ).
fof(f9048,plain,
( e21 != op2(e21,e22)
| ~ spl28_490 ),
inference(forward_demodulation,[],[f355,f3347]) ).
fof(f9072,plain,
( ~ spl28_494
| ~ spl28_490 ),
inference(avatar_split_clause,[],[f9048,f3345,f3363]) ).
fof(f9116,plain,
( e20 != op2(e21,e23)
| ~ spl28_410 ),
inference(forward_demodulation,[],[f364,f2946]) ).
fof(f9117,plain,
( e21 != op2(e21,e23)
| ~ spl28_510 ),
inference(forward_demodulation,[],[f365,f3434]) ).
fof(f9141,plain,
( e22 != op2(e21,e23)
| ~ spl28_495 ),
inference(forward_demodulation,[],[f351,f3369]) ).
fof(f9144,plain,
( e23 != op2(e21,e23)
| ~ spl28_488 ),
inference(forward_demodulation,[],[f368,f3338]) ).
fof(f9157,plain,
( ~ spl28_499
| ~ spl28_495 ),
inference(avatar_split_clause,[],[f9141,f3367,f3384]) ).
fof(f9159,plain,
( ~ spl28_500
| ~ spl28_488 ),
inference(avatar_split_clause,[],[f9144,f3336,f3388]) ).
fof(f9171,plain,
( op2(e22,e22) != h9(op1(e12,e12))
| spl28_323
| ~ spl28_331 ),
inference(forward_demodulation,[],[f2510,f2542]) ).
fof(f9175,plain,
( op2(e22,e22) != h9(e10)
| spl28_323
| ~ spl28_331
| ~ spl28_429 ),
inference(forward_demodulation,[],[f9171,f3047]) ).
fof(f9179,plain,
( e20 != op2(e22,e22)
| ~ spl28_85
| spl28_323
| ~ spl28_331
| ~ spl28_429 ),
inference(forward_demodulation,[],[f9175,f1400]) ).
fof(f9181,plain,
( $false
| ~ spl28_85
| spl28_323
| ~ spl28_331
| ~ spl28_411
| ~ spl28_429 ),
inference(forward_subsumption_resolution,[],[f9179,f2951]) ).
fof(f9182,plain,
( ~ spl28_85
| spl28_323
| ~ spl28_331
| ~ spl28_411
| ~ spl28_429 ),
inference(avatar_contradiction_clause,[],[f9181]) ).
fof(f9183,plain,
( h9(op1(e12,e10)) != op2(h9(e12),e20)
| ~ spl28_85
| spl28_321 ),
inference(forward_demodulation,[],[f2502,f1400]) ).
fof(f9185,plain,
( op2(e22,e20) != h9(op1(e12,e10))
| ~ spl28_85
| spl28_321
| ~ spl28_331 ),
inference(forward_demodulation,[],[f9183,f2542]) ).
fof(f9187,plain,
( op2(e22,e20) != h9(e12)
| ~ spl28_85
| spl28_321
| ~ spl28_331
| ~ spl28_559 ),
inference(forward_demodulation,[],[f9185,f3648]) ).
fof(f9189,plain,
( e22 != op2(e22,e20)
| ~ spl28_85
| spl28_321
| ~ spl28_331
| ~ spl28_559 ),
inference(forward_demodulation,[],[f9187,f2542]) ).
fof(f9190,plain,
( $false
| ~ spl28_85
| spl28_321
| ~ spl28_331
| ~ spl28_503
| ~ spl28_559 ),
inference(forward_subsumption_resolution,[],[f9189,f3403]) ).
fof(f9191,plain,
( ~ spl28_85
| spl28_321
| ~ spl28_331
| ~ spl28_503
| ~ spl28_559 ),
inference(avatar_contradiction_clause,[],[f9190]) ).
fof(f9193,plain,
( h9(op1(e12,e13)) != op2(h9(e12),e23)
| spl28_324
| ~ spl28_336 ),
inference(forward_demodulation,[],[f2514,f2573]) ).
fof(f9195,plain,
( op2(e22,e23) != h9(op1(e12,e13))
| spl28_324
| ~ spl28_331
| ~ spl28_336 ),
inference(forward_demodulation,[],[f9193,f2542]) ).
fof(f9197,plain,
( op2(e22,e23) != h9(e11)
| spl28_324
| ~ spl28_331
| ~ spl28_336
| ~ spl28_566 ),
inference(forward_demodulation,[],[f9195,f3679]) ).
fof(f9199,plain,
( e21 != op2(e22,e23)
| ~ spl28_89
| spl28_324
| ~ spl28_331
| ~ spl28_336
| ~ spl28_566 ),
inference(forward_demodulation,[],[f9197,f1419]) ).
fof(f9200,plain,
( $false
| ~ spl28_89
| spl28_324
| ~ spl28_331
| ~ spl28_336
| ~ spl28_510
| ~ spl28_566 ),
inference(forward_subsumption_resolution,[],[f9199,f3434]) ).
fof(f9201,plain,
( ~ spl28_89
| spl28_324
| ~ spl28_331
| ~ spl28_336
| ~ spl28_510
| ~ spl28_566 ),
inference(avatar_contradiction_clause,[],[f9200]) ).
fof(f9203,plain,
( h9(op1(e13,e10)) != op2(h9(e13),e20)
| ~ spl28_85
| spl28_325 ),
inference(forward_demodulation,[],[f2518,f1400]) ).
fof(f9205,plain,
( op2(e23,e20) != h9(op1(e13,e10))
| ~ spl28_85
| spl28_325
| ~ spl28_336 ),
inference(forward_demodulation,[],[f9203,f2573]) ).
fof(f9207,plain,
( op2(e23,e20) != h9(e13)
| ~ spl28_85
| spl28_325
| ~ spl28_336
| ~ spl28_572 ),
inference(forward_demodulation,[],[f9205,f3704]) ).
fof(f9209,plain,
( e23 != op2(e23,e20)
| ~ spl28_85
| spl28_325
| ~ spl28_336
| ~ spl28_572 ),
inference(forward_demodulation,[],[f9207,f2573]) ).
fof(f9210,plain,
( $false
| ~ spl28_85
| spl28_325
| ~ spl28_336
| ~ spl28_516
| ~ spl28_572 ),
inference(forward_subsumption_resolution,[],[f9209,f3459]) ).
fof(f9211,plain,
( ~ spl28_85
| spl28_325
| ~ spl28_336
| ~ spl28_516
| ~ spl28_572 ),
inference(avatar_contradiction_clause,[],[f9210]) ).
fof(f9213,plain,
( h9(op1(e13,e11)) != op2(h9(e13),e21)
| ~ spl28_89
| spl28_326 ),
inference(forward_demodulation,[],[f2522,f1419]) ).
fof(f9215,plain,
( op2(e23,e21) != h9(op1(e13,e11))
| ~ spl28_89
| spl28_326
| ~ spl28_336 ),
inference(forward_demodulation,[],[f9213,f2573]) ).
fof(f9217,plain,
( op2(e23,e21) != h9(e12)
| ~ spl28_89
| spl28_326
| ~ spl28_336
| ~ spl28_575 ),
inference(forward_demodulation,[],[f9215,f3717]) ).
fof(f9219,plain,
( e22 != op2(e23,e21)
| ~ spl28_89
| spl28_326
| ~ spl28_331
| ~ spl28_336
| ~ spl28_575 ),
inference(forward_demodulation,[],[f9217,f2542]) ).
fof(f9291,plain,
( ~ spl28_521
| ~ spl28_410 ),
inference(avatar_split_clause,[],[f6842,f2944,f3479]) ).
fof(f9292,plain,
( e21 != op2(e23,e22)
| ~ spl28_518 ),
inference(forward_demodulation,[],[f341,f3468]) ).
fof(f9293,plain,
( e23 != op2(e23,e22)
| ~ spl28_516 ),
inference(forward_demodulation,[],[f343,f3459]) ).
fof(f9299,plain,
( e22 != op2(e23,e22)
| ~ spl28_483 ),
inference(forward_demodulation,[],[f372,f3317]) ).
fof(f9301,plain,
( ~ spl28_522
| ~ spl28_518 ),
inference(avatar_split_clause,[],[f9292,f3466,f3483]) ).
fof(f9303,plain,
( ~ spl28_523
| ~ spl28_483 ),
inference(avatar_split_clause,[],[f9299,f3315,f3487]) ).
fof(f9330,plain,
( ~ spl28_519
| ~ spl28_89
| spl28_326
| ~ spl28_331
| ~ spl28_336
| ~ spl28_575 ),
inference(avatar_split_clause,[],[f9219,f3715,f2572,f2541,f2520,f1418,f3470]) ).
fof(f9334,plain,
( ~ spl28_498
| ~ spl28_510 ),
inference(avatar_split_clause,[],[f9117,f3432,f3380]) ).
fof(f9454,plain,
( ~ spl28_524
| ~ spl28_516 ),
inference(avatar_split_clause,[],[f9293,f3457,f3491]) ).
fof(f9456,plain,
( ~ spl28_497
| ~ spl28_410 ),
inference(avatar_split_clause,[],[f9116,f2944,f3376]) ).
fof(f9599,plain,
( h9(op1(e13,e12)) != op2(h9(e13),e22)
| spl28_327
| ~ spl28_331 ),
inference(forward_demodulation,[],[f2526,f2542]) ).
fof(f9649,plain,
( op2(e23,e22) != h9(op1(e13,e12))
| spl28_327
| ~ spl28_331
| ~ spl28_336 ),
inference(forward_demodulation,[],[f9599,f2573]) ).
fof(f9674,plain,
( op2(e23,e22) != h9(e11)
| spl28_327
| ~ spl28_331
| ~ spl28_336
| ~ spl28_578 ),
inference(forward_demodulation,[],[f9649,f3730]) ).
fof(f9683,plain,
( e21 != op2(e23,e22)
| ~ spl28_89
| spl28_327
| ~ spl28_331
| ~ spl28_336
| ~ spl28_578 ),
inference(forward_demodulation,[],[f9674,f1419]) ).
fof(f9689,plain,
( ~ spl28_522
| ~ spl28_89
| spl28_327
| ~ spl28_331
| ~ spl28_336
| ~ spl28_578 ),
inference(avatar_split_clause,[],[f9683,f3728,f2572,f2541,f2524,f1418,f3483]) ).
fof(f9695,plain,
( op2(e23,e23) != h9(op1(e13,e13))
| spl28_328
| ~ spl28_336 ),
inference(forward_demodulation,[],[f2530,f2573]) ).
fof(f9701,plain,
( op2(e23,e23) != h9(e10)
| spl28_328
| ~ spl28_336
| ~ spl28_428 ),
inference(forward_demodulation,[],[f9695,f3042]) ).
fof(f9707,plain,
( e20 != op2(e23,e23)
| ~ spl28_85
| spl28_328
| ~ spl28_336
| ~ spl28_428 ),
inference(forward_demodulation,[],[f9701,f1400]) ).
fof(f9713,plain,
( $false
| ~ spl28_85
| spl28_328
| ~ spl28_336
| ~ spl28_410
| ~ spl28_428 ),
inference(forward_subsumption_resolution,[],[f9707,f2946]) ).
fof(f9714,plain,
( ~ spl28_85
| spl28_328
| ~ spl28_336
| ~ spl28_410
| ~ spl28_428 ),
inference(avatar_contradiction_clause,[],[f9713]) ).
fof(f9730,plain,
( e12 != op1(e13,e12)
| ~ spl28_539 ),
inference(forward_demodulation,[],[f324,f3562]) ).
fof(f9742,plain,
( e11 != op1(e13,e11)
| ~ spl28_534 ),
inference(forward_demodulation,[],[f330,f3541]) ).
fof(f9766,plain,
( ~ spl28_579
| ~ spl28_539 ),
inference(avatar_split_clause,[],[f9730,f3560,f3732]) ).
fof(f9767,plain,
( ~ spl28_574
| ~ spl28_534 ),
inference(avatar_split_clause,[],[f9742,f3539,f3711]) ).
cnf(s68,plain,
( ~ spl28_81
| ~ spl28_85 ),
inference(sat_conversion,[],[f1402]) ).
cnf(s71,plain,
( spl28_86
| ~ spl28_89 ),
inference(sat_conversion,[],[f1421]) ).
cnf(s238,plain,
( spl28_81
| ~ spl28_86
| ~ spl28_313
| ~ spl28_314
| ~ spl28_315
| ~ spl28_316
| ~ spl28_317
| ~ spl28_318
| ~ spl28_319
| ~ spl28_320
| ~ spl28_321
| ~ spl28_322
| ~ spl28_323
| ~ spl28_324
| ~ spl28_325
| ~ spl28_326
| ~ spl28_327
| ~ spl28_328
| ~ spl28_331
| ~ spl28_336 ),
inference(sat_conversion,[],[f2576]) ).
cnf(s295,plain,
spl28_336,
inference(sat_conversion,[],[f2921]) ).
cnf(s296,plain,
spl28_331,
inference(sat_conversion,[],[f2922]) ).
cnf(s298,plain,
spl28_307,
inference(sat_conversion,[],[f2924]) ).
cnf(s301,plain,
spl28_264,
inference(sat_conversion,[],[f2927]) ).
cnf(s308,plain,
spl28_23,
inference(sat_conversion,[],[f2934]) ).
cnf(s314,plain,
( spl28_409
| spl28_411 ),
inference(sat_conversion,[],[f2952]) ).
cnf(s315,plain,
( spl28_409
| spl28_412 ),
inference(sat_conversion,[],[f2957]) ).
cnf(s316,plain,
( spl28_409
| spl28_413 ),
inference(sat_conversion,[],[f2962]) ).
cnf(s317,plain,
( spl28_414
| spl28_415 ),
inference(sat_conversion,[],[f2971]) ).
cnf(s333,plain,
( ~ spl28_409
| ~ spl28_414
| spl28_419
| spl28_426 ),
inference(sat_conversion,[],[f3031]) ).
cnf(s338,plain,
( ~ spl28_427
| spl28_429 ),
inference(sat_conversion,[],[f3048]) ).
cnf(s339,plain,
( ~ spl28_427
| spl28_430 ),
inference(sat_conversion,[],[f3053]) ).
cnf(s340,plain,
( ~ spl28_427
| spl28_431 ),
inference(sat_conversion,[],[f3058]) ).
cnf(s341,plain,
( ~ spl28_432
| spl28_433 ),
inference(sat_conversion,[],[f3067]) ).
cnf(s357,plain,
( spl28_427
| spl28_432
| spl28_437
| spl28_444 ),
inference(sat_conversion,[],[f3127]) ).
cnf(s389,plain,
( spl28_473
| spl28_474
| spl28_475
| spl28_476 ),
inference(sat_conversion,[],[f3287]) ).
cnf(s396,plain,
( spl28_493
| spl28_494
| spl28_495
| spl28_496 ),
inference(sat_conversion,[],[f3374]) ).
cnf(s397,plain,
( spl28_497
| spl28_498
| spl28_499
| spl28_500 ),
inference(sat_conversion,[],[f3391]) ).
cnf(s399,plain,
( spl28_505
| spl28_506
| spl28_507
| spl28_508 ),
inference(sat_conversion,[],[f3425]) ).
cnf(s403,plain,
( spl28_517
| spl28_518
| spl28_519
| spl28_520 ),
inference(sat_conversion,[],[f3477]) ).
cnf(s404,plain,
( spl28_521
| spl28_522
| spl28_523
| spl28_524 ),
inference(sat_conversion,[],[f3494]) ).
cnf(s410,plain,
( spl28_529
| spl28_530
| spl28_531
| spl28_532 ),
inference(sat_conversion,[],[f3532]) ).
cnf(s417,plain,
( spl28_549
| spl28_550
| spl28_551
| spl28_552 ),
inference(sat_conversion,[],[f3619]) ).
cnf(s418,plain,
( spl28_553
| spl28_554
| spl28_555
| spl28_556 ),
inference(sat_conversion,[],[f3636]) ).
cnf(s420,plain,
( spl28_561
| spl28_562
| spl28_563
| spl28_564 ),
inference(sat_conversion,[],[f3670]) ).
cnf(s424,plain,
( spl28_573
| spl28_574
| spl28_575
| spl28_576 ),
inference(sat_conversion,[],[f3722]) ).
cnf(s425,plain,
( spl28_577
| spl28_578
| spl28_579
| spl28_580 ),
inference(sat_conversion,[],[f3739]) ).
cnf(s435,plain,
( ~ spl28_23
| ~ spl28_28 ),
inference(sat_conversion,[],[f3796]) ).
cnf(s452,plain,
( spl28_527
| ~ spl28_531 ),
inference(sat_conversion,[],[f3875]) ).
cnf(s457,plain,
( ~ spl28_532
| spl28_554 ),
inference(sat_conversion,[],[f3888]) ).
cnf(s462,plain,
( spl28_471
| ~ spl28_475 ),
inference(sat_conversion,[],[f3900]) ).
cnf(s480,plain,
( ~ spl28_476
| spl28_498 ),
inference(sat_conversion,[],[f3932]) ).
cnf(s484,plain,
spl28_566,
inference(sat_conversion,[],[f3963]) ).
cnf(s485,plain,
spl28_428,
inference(sat_conversion,[],[f3964]) ).
cnf(s486,plain,
spl28_510,
inference(sat_conversion,[],[f3965]) ).
cnf(s487,plain,
spl28_410,
inference(sat_conversion,[],[f3966]) ).
cnf(s489,plain,
( spl28_52
| ~ spl28_264
| ~ spl28_410
| ~ spl28_426 ),
inference(sat_conversion,[],[f3972]) ).
cnf(s501,plain,
( ~ spl28_23
| spl28_28
| ~ spl28_412
| ~ spl28_474 ),
inference(sat_conversion,[],[f3998]) ).
cnf(s503,plain,
( ~ spl28_23
| spl28_28
| ~ spl28_410
| ~ spl28_415 ),
inference(sat_conversion,[],[f4004]) ).
cnf(s510,plain,
( spl28_73
| ~ spl28_307
| ~ spl28_410
| ~ spl28_419 ),
inference(sat_conversion,[],[f4023]) ).
cnf(s536,plain,
( ~ spl28_52
| ~ spl28_264 ),
inference(sat_conversion,[],[f4047]) ).
cnf(s539,plain,
( ~ spl28_473
| spl28_516 ),
inference(sat_conversion,[],[f4065]) ).
cnf(s540,plain,
( ~ spl28_473
| spl28_488 ),
inference(sat_conversion,[],[f4067]) ).
cnf(s541,plain,
( ~ spl28_473
| spl28_503 ),
inference(sat_conversion,[],[f4069]) ).
cnf(s542,plain,
( ~ spl28_473
| spl28_483 ),
inference(sat_conversion,[],[f4071]) ).
cnf(s543,plain,
( ~ spl28_473
| spl28_490 ),
inference(sat_conversion,[],[f4073]) ).
cnf(s544,plain,
( ~ spl28_473
| spl28_478 ),
inference(sat_conversion,[],[f4075]) ).
cnf(s557,plain,
( ~ spl28_428
| ~ spl28_444 ),
inference(sat_conversion,[],[f4127]) ).
cnf(s564,plain,
( ~ spl28_430
| ~ spl28_530 ),
inference(sat_conversion,[],[f4141]) ).
cnf(s566,plain,
( ~ spl28_428
| ~ spl28_433 ),
inference(sat_conversion,[],[f4147]) ).
cnf(s573,plain,
( ~ spl28_428
| ~ spl28_437 ),
inference(sat_conversion,[],[f4166]) ).
cnf(s578,plain,
( ~ spl28_529
| spl28_572 ),
inference(sat_conversion,[],[f4183]) ).
cnf(s579,plain,
( ~ spl28_529
| spl28_544 ),
inference(sat_conversion,[],[f4185]) ).
cnf(s580,plain,
( ~ spl28_529
| spl28_559 ),
inference(sat_conversion,[],[f4187]) ).
cnf(s581,plain,
( ~ spl28_529
| spl28_539 ),
inference(sat_conversion,[],[f4189]) ).
cnf(s582,plain,
( ~ spl28_529
| spl28_546 ),
inference(sat_conversion,[],[f4191]) ).
cnf(s583,plain,
( ~ spl28_529
| spl28_534 ),
inference(sat_conversion,[],[f4193]) ).
cnf(s738,plain,
( spl28_89
| ~ spl28_510 ),
inference(sat_conversion,[],[f5110]) ).
cnf(s739,plain,
( spl28_85
| ~ spl28_410 ),
inference(sat_conversion,[],[f5114]) ).
cnf(s763,plain,
( ~ spl28_428
| ~ spl28_577 ),
inference(sat_conversion,[],[f5278]) ).
cnf(s765,plain,
( ~ spl28_428
| ~ spl28_573 ),
inference(sat_conversion,[],[f5283]) ).
cnf(s769,plain,
( ~ spl28_562
| ~ spl28_566 ),
inference(sat_conversion,[],[f5302]) ).
cnf(s770,plain,
( ~ spl28_429
| ~ spl28_561 ),
inference(sat_conversion,[],[f5303]) ).
cnf(s777,plain,
( ~ spl28_89
| spl28_322
| ~ spl28_331
| ~ spl28_336
| ~ spl28_508
| ~ spl28_564 ),
inference(sat_conversion,[],[f5328]) ).
cnf(s793,plain,
( ~ spl28_429
| ~ spl28_527
| spl28_529 ),
inference(sat_conversion,[],[f5374]) ).
cnf(s852,plain,
( ~ spl28_551
| ~ spl28_555 ),
inference(sat_conversion,[],[f5741]) ).
cnf(s853,plain,
( ~ spl28_430
| ~ spl28_553 ),
inference(sat_conversion,[],[f5742]) ).
cnf(s857,plain,
( ~ spl28_559
| ~ spl28_563 ),
inference(sat_conversion,[],[f5776]) ).
cnf(s862,plain,
( ~ spl28_85
| spl28_313
| ~ spl28_413
| ~ spl28_431 ),
inference(sat_conversion,[],[f5829]) ).
cnf(s863,plain,
( ~ spl28_85
| spl28_315
| ~ spl28_331
| ~ spl28_483
| ~ spl28_539 ),
inference(sat_conversion,[],[f5839]) ).
cnf(s864,plain,
( ~ spl28_85
| spl28_316
| ~ spl28_336
| ~ spl28_488
| ~ spl28_544 ),
inference(sat_conversion,[],[f5849]) ).
cnf(s881,plain,
( ~ spl28_544
| ~ spl28_556 ),
inference(sat_conversion,[],[f6043]) ).
cnf(s882,plain,
( ~ spl28_430
| ~ spl28_549 ),
inference(sat_conversion,[],[f6044]) ).
cnf(s887,plain,
( ~ spl28_89
| spl28_319
| ~ spl28_331
| ~ spl28_336
| ~ spl28_496
| ~ spl28_552 ),
inference(sat_conversion,[],[f6106]) ).
cnf(s907,plain,
( ~ spl28_554
| ~ spl28_566 ),
inference(sat_conversion,[],[f6204]) ).
cnf(s939,plain,
( ~ spl28_572
| ~ spl28_580 ),
inference(sat_conversion,[],[f6520]) ).
cnf(s950,plain,
( ~ spl28_572
| ~ spl28_576 ),
inference(sat_conversion,[],[f6597]) ).
cnf(s977,plain,
( ~ spl28_410
| ~ spl28_517 ),
inference(sat_conversion,[],[f6855]) ).
cnf(s982,plain,
( ~ spl28_411
| ~ spl28_471
| spl28_473 ),
inference(sat_conversion,[],[f6867]) ).
cnf(s1093,plain,
( ~ spl28_89
| spl28_320
| ~ spl28_331
| ~ spl28_336
| ~ spl28_499
| ~ spl28_555 ),
inference(sat_conversion,[],[f7031]) ).
cnf(s1115,plain,
( ~ spl28_85
| ~ spl28_89
| spl28_314
| ~ spl28_478
| ~ spl28_534 ),
inference(sat_conversion,[],[f7077]) ).
cnf(s1116,plain,
( ~ spl28_85
| ~ spl28_89
| spl28_317
| ~ spl28_490
| ~ spl28_546 ),
inference(sat_conversion,[],[f7081]) ).
cnf(s1117,plain,
( ~ spl28_85
| ~ spl28_89
| spl28_318
| ~ spl28_412
| ~ spl28_430 ),
inference(sat_conversion,[],[f7085]) ).
cnf(s1135,plain,
( ~ spl28_546
| ~ spl28_550 ),
inference(sat_conversion,[],[f7106]) ).
cnf(s1281,plain,
( ~ spl28_73
| ~ spl28_307 ),
inference(sat_conversion,[],[f7725]) ).
cnf(s1623,plain,
( ~ spl28_516
| ~ spl28_520 ),
inference(sat_conversion,[],[f8579]) ).
cnf(s1632,plain,
( ~ spl28_411
| ~ spl28_505 ),
inference(sat_conversion,[],[f8626]) ).
cnf(s1635,plain,
( ~ spl28_503
| ~ spl28_507 ),
inference(sat_conversion,[],[f8635]) ).
cnf(s1641,plain,
( ~ spl28_506
| ~ spl28_510 ),
inference(sat_conversion,[],[f8649]) ).
cnf(s1674,plain,
( ~ spl28_412
| ~ spl28_493 ),
inference(sat_conversion,[],[f8889]) ).
cnf(s1693,plain,
( ~ spl28_490
| ~ spl28_494 ),
inference(sat_conversion,[],[f9072]) ).
cnf(s1700,plain,
( ~ spl28_495
| ~ spl28_499 ),
inference(sat_conversion,[],[f9157]) ).
cnf(s1701,plain,
( ~ spl28_488
| ~ spl28_500 ),
inference(sat_conversion,[],[f9159]) ).
cnf(s1707,plain,
( ~ spl28_85
| spl28_323
| ~ spl28_331
| ~ spl28_411
| ~ spl28_429 ),
inference(sat_conversion,[],[f9182]) ).
cnf(s1709,plain,
( ~ spl28_85
| spl28_321
| ~ spl28_331
| ~ spl28_503
| ~ spl28_559 ),
inference(sat_conversion,[],[f9191]) ).
cnf(s1710,plain,
( ~ spl28_89
| spl28_324
| ~ spl28_331
| ~ spl28_336
| ~ spl28_510
| ~ spl28_566 ),
inference(sat_conversion,[],[f9201]) ).
cnf(s1711,plain,
( ~ spl28_85
| spl28_325
| ~ spl28_336
| ~ spl28_516
| ~ spl28_572 ),
inference(sat_conversion,[],[f9211]) ).
cnf(s1719,plain,
( ~ spl28_410
| ~ spl28_521 ),
inference(sat_conversion,[],[f9291]) ).
cnf(s1731,plain,
( ~ spl28_518
| ~ spl28_522 ),
inference(sat_conversion,[],[f9301]) ).
cnf(s1733,plain,
( ~ spl28_483
| ~ spl28_523 ),
inference(sat_conversion,[],[f9303]) ).
cnf(s1741,plain,
( ~ spl28_89
| spl28_326
| ~ spl28_331
| ~ spl28_336
| ~ spl28_519
| ~ spl28_575 ),
inference(sat_conversion,[],[f9330]) ).
cnf(s1743,plain,
( ~ spl28_498
| ~ spl28_510 ),
inference(sat_conversion,[],[f9334]) ).
cnf(s1789,plain,
( ~ spl28_516
| ~ spl28_524 ),
inference(sat_conversion,[],[f9454]) ).
cnf(s1791,plain,
( ~ spl28_410
| ~ spl28_497 ),
inference(sat_conversion,[],[f9456]) ).
cnf(s1903,plain,
( ~ spl28_89
| spl28_327
| ~ spl28_331
| ~ spl28_336
| ~ spl28_522
| ~ spl28_578 ),
inference(sat_conversion,[],[f9689]) ).
cnf(s1904,plain,
( ~ spl28_85
| spl28_328
| ~ spl28_336
| ~ spl28_410
| ~ spl28_428 ),
inference(sat_conversion,[],[f9714]) ).
cnf(s1910,plain,
( ~ spl28_539
| ~ spl28_579 ),
inference(sat_conversion,[],[f9766]) ).
cnf(s1911,plain,
( ~ spl28_534
| ~ spl28_574 ),
inference(sat_conversion,[],[f9767]) ).
cnf(s1916,plain,
~ spl28_497,
inference(rat,[],[s1791,s487]) ).
cnf(s1917,plain,
~ spl28_521,
inference(rat,[],[s1719,s487]) ).
cnf(s1918,plain,
~ spl28_517,
inference(rat,[],[s977,s487]) ).
cnf(s1919,plain,
spl28_85,
inference(rat,[],[s739,s487]) ).
cnf(s1924,plain,
~ spl28_498,
inference(rat,[],[s1743,s486]) ).
cnf(s1925,plain,
~ spl28_506,
inference(rat,[],[s1641,s486]) ).
cnf(s1926,plain,
spl28_89,
inference(rat,[],[s738,s486]) ).
cnf(s1927,plain,
~ spl28_573,
inference(rat,[],[s765,s485]) ).
cnf(s1928,plain,
~ spl28_577,
inference(rat,[],[s763,s485]) ).
cnf(s1929,plain,
~ spl28_437,
inference(rat,[],[s573,s485]) ).
cnf(s1930,plain,
~ spl28_433,
inference(rat,[],[s566,s485]) ).
cnf(s1931,plain,
~ spl28_444,
inference(rat,[],[s557,s485]) ).
cnf(s1932,plain,
~ spl28_554,
inference(rat,[],[s907,s484]) ).
cnf(s1933,plain,
~ spl28_562,
inference(rat,[],[s769,s484]) ).
cnf(s1936,plain,
~ spl28_476,
inference(rat,[],[s480,s1924]) ).
cnf(s1937,plain,
~ spl28_532,
inference(rat,[],[s457,s1932]) ).
cnf(s1938,plain,
( spl28_578
| spl28_579
| spl28_580 ),
inference(rat,[],[s425,s1928]) ).
cnf(s1939,plain,
( spl28_574
| spl28_575
| spl28_576 ),
inference(rat,[],[s424,s1927]) ).
cnf(s1940,plain,
( spl28_561
| spl28_563
| spl28_564 ),
inference(rat,[],[s420,s1933]) ).
cnf(s1941,plain,
( spl28_553
| spl28_555
| spl28_556 ),
inference(rat,[],[s418,s1932]) ).
cnf(s1942,plain,
( spl28_529
| spl28_530
| spl28_531 ),
inference(rat,[],[s410,s1937]) ).
cnf(s1943,plain,
( spl28_522
| spl28_523
| spl28_524 ),
inference(rat,[],[s404,s1917]) ).
cnf(s1944,plain,
( spl28_518
| spl28_519
| spl28_520 ),
inference(rat,[],[s403,s1918]) ).
cnf(s1945,plain,
( spl28_505
| spl28_507
| spl28_508 ),
inference(rat,[],[s399,s1925]) ).
cnf(s1946,plain,
( spl28_499
| spl28_500 ),
inference(rat,[],[s397,s1924,s1916]) ).
cnf(s1947,plain,
( spl28_473
| spl28_474
| spl28_475 ),
inference(rat,[],[s389,s1936]) ).
cnf(s1951,plain,
( spl28_427
| spl28_432 ),
inference(rat,[],[s357,s1931,s1929]) ).
cnf(s1955,plain,
~ spl28_432,
inference(rat,[],[s341,s1930]) ).
cnf(s1956,plain,
spl28_427,
inference(rat,[],[s1951,s1955]) ).
cnf(s1957,plain,
spl28_431,
inference(rat,[],[s340,s1956]) ).
cnf(s1960,plain,
spl28_430,
inference(rat,[],[s339,s1956]) ).
cnf(s1961,plain,
~ spl28_549,
inference(rat,[],[s882,s1960]) ).
cnf(s1962,plain,
~ spl28_553,
inference(rat,[],[s853,s1960]) ).
cnf(s1965,plain,
~ spl28_530,
inference(rat,[],[s564,s1960]) ).
cnf(s1966,plain,
spl28_429,
inference(rat,[],[s338,s1956]) ).
cnf(s1967,plain,
~ spl28_561,
inference(rat,[],[s770,s1966]) ).
cnf(s1970,plain,
~ spl28_28,
inference(rat,[],[s435,s308]) ).
cnf(s1972,plain,
~ spl28_415,
inference(rat,[],[s503,s308,s487,s1970]) ).
cnf(s1973,plain,
spl28_414,
inference(rat,[],[s317,s1972]) ).
cnf(s1980,plain,
~ spl28_52,
inference(rat,[],[s536,s301]) ).
cnf(s1981,plain,
~ spl28_426,
inference(rat,[],[s489,s301,s487,s1980]) ).
cnf(s1982,plain,
~ spl28_73,
inference(rat,[],[s1281,s298]) ).
cnf(s1989,plain,
~ spl28_419,
inference(rat,[],[s510,s298,s487,s1982]) ).
cnf(s1990,plain,
~ spl28_409,
inference(rat,[],[s333,s1981,s1973,s1989]) ).
cnf(s1991,plain,
spl28_413,
inference(rat,[],[s316,s1990]) ).
cnf(s1992,plain,
spl28_412,
inference(rat,[],[s315,s1990]) ).
cnf(s1993,plain,
spl28_411,
inference(rat,[],[s314,s1990]) ).
cnf(s1997,plain,
spl28_313,
inference(rat,[],[s862,s1957,s1919,s1991]) ).
cnf(s2003,plain,
~ spl28_493,
inference(rat,[],[s1674,s1992]) ).
cnf(s2007,plain,
spl28_318,
inference(rat,[],[s1117,s1960,s1926,s1919,s1992]) ).
cnf(s2009,plain,
~ spl28_474,
inference(rat,[],[s501,s1970,s308,s1992]) ).
cnf(s2012,plain,
~ spl28_505,
inference(rat,[],[s1632,s1993]) ).
cnf(s2045,plain,
spl28_323,
inference(rat,[],[s1707,s1966,s1993,s1919,s296]) ).
cnf(s2048,plain,
spl28_328,
inference(rat,[],[s1904,s485,s487,s1919,s295]) ).
cnf(s2049,plain,
spl28_324,
inference(rat,[],[s1710,s484,s486,s296,s1926,s295]) ).
cnf(s2093,plain,
( spl28_81
| ~ spl28_86
| ~ spl28_314
| ~ spl28_315
| ~ spl28_316
| ~ spl28_317
| ~ spl28_319
| ~ spl28_320
| ~ spl28_321
| ~ spl28_322
| ~ spl28_325
| ~ spl28_326
| ~ spl28_327 ),
inference(rat,[],[s238,s295,s296,s2048,s2049,s2045,s2007,s1997]) ).
cnf(s2203,plain,
spl28_86,
inference(rat,[],[s71,s1926]) ).
cnf(s2204,plain,
~ spl28_81,
inference(rat,[],[s68,s1919]) ).
cnf(s2218,plain,
spl28_473,
inference(rat,[],[s462,s982,s1947,s1993,s2009]) ).
cnf(s2221,plain,
spl28_478,
inference(rat,[],[s544,s2218]) ).
cnf(s2222,plain,
spl28_490,
inference(rat,[],[s543,s2218]) ).
cnf(s2223,plain,
spl28_483,
inference(rat,[],[s542,s2218]) ).
cnf(s2224,plain,
spl28_503,
inference(rat,[],[s541,s2218]) ).
cnf(s2225,plain,
spl28_488,
inference(rat,[],[s540,s2218]) ).
cnf(s2226,plain,
spl28_516,
inference(rat,[],[s539,s2218]) ).
cnf(s2231,plain,
~ spl28_494,
inference(rat,[],[s1693,s2222]) ).
cnf(s2234,plain,
~ spl28_523,
inference(rat,[],[s1733,s2223]) ).
cnf(s2237,plain,
~ spl28_507,
inference(rat,[],[s1635,s2224]) ).
cnf(s2240,plain,
~ spl28_500,
inference(rat,[],[s1701,s2225]) ).
cnf(s2245,plain,
~ spl28_524,
inference(rat,[],[s1789,s2226]) ).
cnf(s2246,plain,
~ spl28_520,
inference(rat,[],[s1623,s2226]) ).
cnf(s2260,plain,
spl28_522,
inference(rat,[],[s1943,s2245,s2234]) ).
cnf(s2264,plain,
spl28_508,
inference(rat,[],[s1945,s2012,s2237]) ).
cnf(s2267,plain,
spl28_499,
inference(rat,[],[s1946,s2240]) ).
cnf(s2276,plain,
~ spl28_518,
inference(rat,[],[s1731,s2260]) ).
cnf(s2278,plain,
~ spl28_495,
inference(rat,[],[s1700,s2267]) ).
cnf(s2281,plain,
spl28_519,
inference(rat,[],[s1944,s2246,s2276]) ).
cnf(s2285,plain,
spl28_496,
inference(rat,[],[s396,s2231,s2003,s2278]) ).
cnf(s2289,plain,
spl28_529,
inference(rat,[],[s452,s793,s1942,s1966,s1965]) ).
cnf(s2292,plain,
spl28_534,
inference(rat,[],[s583,s2289]) ).
cnf(s2293,plain,
spl28_546,
inference(rat,[],[s582,s2289]) ).
cnf(s2294,plain,
spl28_539,
inference(rat,[],[s581,s2289]) ).
cnf(s2295,plain,
spl28_559,
inference(rat,[],[s580,s2289]) ).
cnf(s2296,plain,
spl28_544,
inference(rat,[],[s579,s2289]) ).
cnf(s2297,plain,
spl28_572,
inference(rat,[],[s578,s2289]) ).
cnf(s2301,plain,
~ spl28_574,
inference(rat,[],[s1911,s2292]) ).
cnf(s2303,plain,
spl28_314,
inference(rat,[],[s1115,s2221,s1926,s1919,s2292]) ).
cnf(s2310,plain,
~ spl28_550,
inference(rat,[],[s1135,s2293]) ).
cnf(s2312,plain,
spl28_317,
inference(rat,[],[s1116,s2222,s1926,s1919,s2293]) ).
cnf(s2319,plain,
~ spl28_579,
inference(rat,[],[s1910,s2294]) ).
cnf(s2330,plain,
spl28_315,
inference(rat,[],[s863,s2223,s296,s1919,s2294]) ).
cnf(s2333,plain,
~ spl28_563,
inference(rat,[],[s857,s2295]) ).
cnf(s2342,plain,
spl28_321,
inference(rat,[],[s1709,s2224,s296,s1919,s2295]) ).
cnf(s2344,plain,
~ spl28_556,
inference(rat,[],[s881,s2296]) ).
cnf(s2359,plain,
spl28_316,
inference(rat,[],[s864,s2225,s295,s1919,s2296]) ).
cnf(s2360,plain,
~ spl28_576,
inference(rat,[],[s950,s2297]) ).
cnf(s2361,plain,
~ spl28_580,
inference(rat,[],[s939,s2297]) ).
cnf(s2370,plain,
spl28_325,
inference(rat,[],[s1711,s2226,s295,s1919,s2297]) ).
cnf(s2373,plain,
spl28_578,
inference(rat,[],[s1938,s2361,s2319]) ).
cnf(s2374,plain,
spl28_564,
inference(rat,[],[s1940,s1967,s2333]) ).
cnf(s2375,plain,
spl28_555,
inference(rat,[],[s1941,s1962,s2344]) ).
cnf(s2376,plain,
spl28_575,
inference(rat,[],[s1939,s2301,s2360]) ).
cnf(s2384,plain,
spl28_327,
inference(rat,[],[s1903,s2260,s295,s296,s1926,s2373]) ).
cnf(s2394,plain,
spl28_322,
inference(rat,[],[s777,s2264,s295,s296,s1926,s2374]) ).
cnf(s2397,plain,
~ spl28_551,
inference(rat,[],[s852,s2375]) ).
cnf(s2398,plain,
spl28_320,
inference(rat,[],[s1093,s2267,s295,s296,s1926,s2375]) ).
cnf(s2416,plain,
spl28_326,
inference(rat,[],[s1741,s2281,s295,s296,s1926,s2376]) ).
cnf(s2419,plain,
spl28_552,
inference(rat,[],[s417,s2310,s1961,s2397]) ).
cnf(s2420,plain,
~ spl28_319,
inference(rat,[],[s2093,s2384,s2416,s2370,s2394,s2342,s2330,s2303,s2312,s2359,s2204,s2203,s2398]) ).
cnf(s2428,plain,
$false,
inference(rat,[],[s887,s2285,s295,s296,s1926,s2419,s2420]) ).
fof(f9787,plain,
$false,
inference(avatar_sat_refutation,[],[s2428]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG015+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.23/0.27 % Computer : n010.cluster.edu
% 0.23/0.27 % Model : x86_64 x86_64
% 0.23/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.23/0.27 % Memory : 8046.5625MB
% 0.23/0.27 % OS : Linux 6.8.0-71-generic
% 0.23/0.27 % CPULimit : 300
% 0.23/0.27 % WCLimit : 300
% 0.23/0.27 % DateTime : Mon Sep 28 19:18:02 UTC 2026
% 0.23/0.28 % CPUTime :
% 0.23/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.23/0.31 Running first-order model finding
% 0.23/0.31 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.70/0.76 % (2231046)Will run a generic schedule for satisfiability detection.
% 2.70/0.76 % (2231056)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4193684025:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.70/0.76 % (2231052)% WARNING: option uhcvi not known.
% 2.70/0.76 % (2231055)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1440334763:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.70/0.76 % (2231051)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=581786566_2999 on theBenchmark for (2999ds/0Mi)
% 2.70/0.76 % (2231052)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1629595766:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.70/0.76 % (2231054)dis+10_1_sil=32000:sp=arity:random_seed=4233578160:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.70/0.76 % (2231053)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=71167185:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.70/0.76 % (2231057)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=501962189:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.70/0.76 % (2231056)Instruction limit reached!
% 2.70/0.76 % (2231056)------------------------------
% 2.70/0.76 % (2231056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.70/0.76 % (2231056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.70/0.76 % (2231056)CaDiCaL version: 2.1.3
% 2.70/0.76 % (2231056)Termination reason: Instruction limit
% 2.70/0.76 % (2231056)Termination phase: Saturation
% 2.70/0.76 % (2231056)Time elapsed: 0.063 s
% 2.70/0.76 % (2231056)Peak memory usage: 14 MB
% 2.70/0.76 % (2231056)Instructions burned: 132 (million)
% 2.70/0.76 % (2231065)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=921484171:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.70/0.76 % (2231054)Instruction limit reached!
% 2.70/0.76 % (2231054)------------------------------
% 2.70/0.76 % (2231054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.70/0.76 % (2231054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.70/0.76 % (2231054)CaDiCaL version: 2.1.3
% 2.70/0.76 % (2231054)Termination reason: Instruction limit
% 2.70/0.76 % (2231054)Termination phase: Saturation
% 2.70/0.76 % (2231054)Time elapsed: 0.090 s
% 2.70/0.76 % (2231054)Peak memory usage: 13 MB
% 2.70/0.76 % (2231054)Instructions burned: 104 (million)
% 2.70/0.76 % (2231055)Instruction limit reached!
% 2.70/0.76 % (2231055)------------------------------
% 2.70/0.76 % (2231055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.70/0.76 % (2231055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.70/0.76 % (2231055)CaDiCaL version: 2.1.3
% 2.70/0.76 % (2231055)Termination reason: Instruction limit
% 2.70/0.76 % (2231055)Termination phase: Saturation
% 2.70/0.76 % (2231055)Time elapsed: 0.095 s
% 2.70/0.76 % (2231055)Peak memory usage: 14 MB
% 2.70/0.76 % (2231055)Instructions burned: 116 (million)
% 2.70/0.76 % (2231067)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3708111567:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 2.70/0.76 % Detected minimum model sizes of [8]
% 2.70/0.76 % Detected maximum model sizes of [max]
% 2.70/0.76 % TRYING [8]
% 2.70/0.76 % (2231068)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=2711427998:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 2.70/0.76 % (2231057)Instruction limit reached!
% 2.70/0.76 % (2231057)------------------------------
% 2.70/0.76 % (2231057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.70/0.76 % (2231057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.70/0.76 % (2231057)CaDiCaL version: 2.1.3
% 2.70/0.76 % (2231057)Termination reason: Instruction limit
% 2.70/0.76 % (2231057)Termination phase: Saturation
% 2.70/0.76 % (2231057)Time elapsed: 0.148 s
% 2.70/0.76 % (2231057)Peak memory usage: 14 MB
% 2.70/0.76 % (2231057)Instructions burned: 159 (million)
% 2.70/0.76 % Detected minimum model sizes of [8]
% 2.70/0.76 % Detected maximum model sizes of [max]
% 2.70/0.76 % TRYING [8]
% 2.70/0.76 % (2231071)ott-21_1_sil=16000:fs=off:random_seed=3124949728:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.70/0.76 % (2231067)Instruction limit reached!
% 2.70/0.76 % (2231067)------------------------------
% 2.70/0.76 % (2231067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.70/0.76 % (2231067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.70/0.76 % (2231067)CaDiCaL version: 2.1.3
% 2.70/0.76 % (2231067)Termination reason: Instruction limit
% 2.70/0.76 % (2231067)Termination phase: Saturation
% 2.70/0.76 % (2231067)Time elapsed: 0.121 s
% 2.70/0.76 % (2231067)Peak memory usage: 14 MB
% 2.70/0.76 % (2231067)Instructions burned: 131 (million)
% 2.70/0.76 % (2231073)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1675275653:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 2.70/0.76 % (2231071)Instruction limit reached!
% 2.70/0.76 % (2231071)------------------------------
% 2.70/0.76 % (2231071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.70/0.76 % (2231071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.70/0.76 % (2231071)CaDiCaL version: 2.1.3
% 2.70/0.76 % (2231071)Termination reason: Instruction limit
% 2.70/0.76 % (2231071)Termination phase: Saturation
% 2.70/0.76 % (2231071)Time elapsed: 0.163 s
% 2.70/0.76 % (2231071)Peak memory usage: 12 MB
% 2.70/0.76 % (2231071)Instructions burned: 181 (million)
% 2.70/0.76 % (2231052) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2231046-2231052"...
% 2.70/0.76 % (2231075)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3214002243:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 2.70/0.76 % (2231065)Instruction limit reached!
% 2.70/0.76 % (2231065)------------------------------
% 2.70/0.76 % (2231065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.70/0.76 % (2231052)...printing done.
% 2.70/0.76 % (2231065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.70/0.76 % (2231065)CaDiCaL version: 2.1.3
% 2.70/0.76 % (2231065)Termination reason: Instruction limit
% 2.70/0.76 % (2231065)Termination phase: Finite model building constraint generation
% 2.70/0.76 % (2231065)Time elapsed: 0.310 s
% 2.70/0.76 % (2231065)Peak memory usage: 52 MB
% 2.70/0.76 % (2231065)Instructions burned: 716 (million)
% 2.70/0.76 % (2231052)Refutation found. Thanks to Tanya!
% 2.70/0.76 % SZS status Theorem for theBenchmark
% 2.70/0.76 % SZS output start Proof for theBenchmark
% See solution above
% 2.70/0.77 % (2231052)------------------------------
% 2.70/0.77 % (2231052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.70/0.77 % (2231052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.70/0.77 % (2231052)CaDiCaL version: 2.1.3
% 2.70/0.77 % (2231052)Termination reason: Refutation
% 2.70/0.77 % (2231052)Time elapsed: 0.383 s
% 2.70/0.77 % (2231052)Peak memory usage: 17 MB
% 2.70/0.77 % (2231052)Instructions burned: 438 (million)
% 2.70/0.77 % (2231046)Success in time 0.445 s
% 2.70/0.77 % Vampire exiting
%------------------------------------------------------------------------------