%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG016+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.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:07:33 AM UTC 2026
% Result : Theorem 4.90s 1.42s
% Output : Refutation 5.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 152
% Syntax : Number of formulae : 1021 ( 225 unt; 134 def)
% Number of atoms : 3417 (1786 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 4188 (1792 ~;1735 |; 523 &)
% ( 122 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 64 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 136 ( 134 usr; 135 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 9 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(f6,axiom,
( op2(op2(e20,e20),e20) = op2(e20,op2(e20,e20))
& op2(op2(e20,e20),e21) = op2(e20,op2(e20,e21))
& op2(op2(e20,e20),e22) = op2(e20,op2(e20,e22))
& op2(op2(e20,e20),e23) = op2(e20,op2(e20,e23))
& op2(op2(e20,e21),e20) = op2(e20,op2(e21,e20))
& op2(op2(e20,e21),e21) = op2(e20,op2(e21,e21))
& op2(op2(e20,e21),e22) = op2(e20,op2(e21,e22))
& op2(op2(e20,e21),e23) = op2(e20,op2(e21,e23))
& op2(op2(e20,e22),e20) = op2(e20,op2(e22,e20))
& op2(op2(e20,e22),e21) = op2(e20,op2(e22,e21))
& op2(op2(e20,e22),e22) = op2(e20,op2(e22,e22))
& op2(op2(e20,e22),e23) = op2(e20,op2(e22,e23))
& op2(op2(e20,e23),e20) = op2(e20,op2(e23,e20))
& op2(op2(e20,e23),e21) = op2(e20,op2(e23,e21))
& op2(op2(e20,e23),e22) = op2(e20,op2(e23,e22))
& op2(op2(e20,e23),e23) = op2(e20,op2(e23,e23))
& op2(op2(e21,e20),e20) = op2(e21,op2(e20,e20))
& op2(op2(e21,e20),e21) = op2(e21,op2(e20,e21))
& op2(op2(e21,e20),e22) = op2(e21,op2(e20,e22))
& op2(op2(e21,e20),e23) = op2(e21,op2(e20,e23))
& op2(op2(e21,e21),e20) = op2(e21,op2(e21,e20))
& op2(op2(e21,e21),e21) = op2(e21,op2(e21,e21))
& op2(op2(e21,e21),e22) = op2(e21,op2(e21,e22))
& op2(op2(e21,e21),e23) = op2(e21,op2(e21,e23))
& op2(op2(e21,e22),e20) = op2(e21,op2(e22,e20))
& op2(op2(e21,e22),e21) = op2(e21,op2(e22,e21))
& op2(op2(e21,e22),e22) = op2(e21,op2(e22,e22))
& op2(op2(e21,e22),e23) = op2(e21,op2(e22,e23))
& op2(op2(e21,e23),e20) = op2(e21,op2(e23,e20))
& op2(op2(e21,e23),e21) = op2(e21,op2(e23,e21))
& op2(op2(e21,e23),e22) = op2(e21,op2(e23,e22))
& op2(op2(e21,e23),e23) = op2(e21,op2(e23,e23))
& op2(op2(e22,e20),e20) = op2(e22,op2(e20,e20))
& op2(op2(e22,e20),e21) = op2(e22,op2(e20,e21))
& op2(op2(e22,e20),e22) = op2(e22,op2(e20,e22))
& op2(op2(e22,e20),e23) = op2(e22,op2(e20,e23))
& op2(op2(e22,e21),e20) = op2(e22,op2(e21,e20))
& op2(op2(e22,e21),e21) = op2(e22,op2(e21,e21))
& op2(op2(e22,e21),e22) = op2(e22,op2(e21,e22))
& op2(op2(e22,e21),e23) = op2(e22,op2(e21,e23))
& op2(op2(e22,e22),e20) = op2(e22,op2(e22,e20))
& op2(op2(e22,e22),e21) = op2(e22,op2(e22,e21))
& op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22))
& op2(op2(e22,e22),e23) = op2(e22,op2(e22,e23))
& op2(op2(e22,e23),e20) = op2(e22,op2(e23,e20))
& op2(op2(e22,e23),e21) = op2(e22,op2(e23,e21))
& op2(op2(e22,e23),e22) = op2(e22,op2(e23,e22))
& op2(op2(e22,e23),e23) = op2(e22,op2(e23,e23))
& op2(op2(e23,e20),e20) = op2(e23,op2(e20,e20))
& op2(op2(e23,e20),e21) = op2(e23,op2(e20,e21))
& op2(op2(e23,e20),e22) = op2(e23,op2(e20,e22))
& op2(op2(e23,e20),e23) = op2(e23,op2(e20,e23))
& op2(op2(e23,e21),e20) = op2(e23,op2(e21,e20))
& op2(op2(e23,e21),e21) = op2(e23,op2(e21,e21))
& op2(op2(e23,e21),e22) = op2(e23,op2(e21,e22))
& op2(op2(e23,e21),e23) = op2(e23,op2(e21,e23))
& op2(op2(e23,e22),e20) = op2(e23,op2(e22,e20))
& op2(op2(e23,e22),e21) = op2(e23,op2(e22,e21))
& op2(op2(e23,e22),e22) = op2(e23,op2(e22,e22))
& op2(op2(e23,e22),e23) = op2(e23,op2(e22,e23))
& op2(op2(e23,e23),e20) = op2(e23,op2(e23,e20))
& op2(op2(e23,e23),e21) = op2(e23,op2(e23,e21))
& op2(op2(e23,e23),e22) = op2(e23,op2(e23,e22))
& op2(op2(e23,e23),e23) = op2(e23,op2(e23,e23)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f9,axiom,
inv1(unit1) = unit1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax9) ).
fof(f10,axiom,
( inv1(inv1(e10)) = e10
& inv1(inv1(e11)) = e11
& inv1(inv1(e12)) = e12
& inv1(inv1(e13)) = e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( ( inv1(e10) = e10
=> inv1(e10) = e10 )
& ( inv1(e10) = e11
=> inv1(e11) = e10 )
& ( inv1(e10) = e12
=> inv1(e12) = e10 )
& ( inv1(e10) = e13
=> inv1(e13) = e10 )
& ( inv1(e11) = e10
=> inv1(e10) = e11 )
& ( inv1(e11) = e11
=> inv1(e11) = e11 )
& ( inv1(e11) = e12
=> inv1(e12) = e11 )
& ( inv1(e11) = e13
=> inv1(e13) = e11 )
& ( inv1(e12) = e10
=> inv1(e10) = e12 )
& ( inv1(e12) = e11
=> inv1(e11) = e12 )
& ( inv1(e12) = e12
=> inv1(e12) = e12 )
& ( inv1(e12) = e13
=> inv1(e13) = e12 )
& ( inv1(e13) = e10
=> inv1(e10) = e13 )
& ( inv1(e13) = e11
=> inv1(e11) = e13 )
& ( inv1(e13) = e12
=> inv1(e12) = e13 )
& ( inv1(e13) = e13
=> inv1(e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
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(f24,axiom,
( e10 = op1(op1(e12,op1(e12,e12)),e12)
& e11 = op1(e12,op1(e12,e12))
& e13 = op1(e12,e12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
fof(f25,axiom,
( e20 = op2(op2(e22,op2(e22,e22)),e22)
& e21 = op2(e22,op2(e22,e22))
& e23 = op2(e22,e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax25) ).
fof(f26,axiom,
( h1(e12) = e20
& h1(e10) = op2(op2(e20,op2(e20,e20)),e20)
& h1(e11) = op2(e20,op2(e20,e20))
& h1(e13) = op2(e20,e20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax26) ).
fof(f27,axiom,
( h2(e12) = e21
& h2(e10) = op2(op2(e21,op2(e21,e21)),e21)
& h2(e11) = op2(e21,op2(e21,e21))
& h2(e13) = op2(e21,e21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax27) ).
fof(f28,axiom,
( h3(e12) = e22
& h3(e10) = op2(op2(e22,op2(e22,e22)),e22)
& h3(e11) = op2(e22,op2(e22,e22))
& h3(e13) = op2(e22,e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax28) ).
fof(f29,axiom,
( h4(e12) = e23
& h4(e10) = op2(op2(e23,op2(e23,e23)),e23)
& h4(e11) = op2(e23,op2(e23,e23))
& h4(e13) = op2(e23,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax29) ).
fof(f30,conjecture,
( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f31,negated_conjecture,
~ ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f30]) ).
fof(f32,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) ) )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) ) )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) ) )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) ) ) ),
inference(ennf_transformation,[],[f31]) ).
fof(f35,plain,
( ( inv1(e10) = e10
| e10 != inv1(e10) )
& ( inv1(e11) = e10
| e11 != inv1(e10) )
& ( inv1(e12) = e10
| e12 != inv1(e10) )
& ( inv1(e13) = e10
| e13 != inv1(e10) )
& ( inv1(e10) = e11
| e10 != inv1(e11) )
& ( inv1(e11) = e11
| e11 != inv1(e11) )
& ( inv1(e12) = e11
| e12 != inv1(e11) )
& ( inv1(e13) = e11
| e13 != inv1(e11) )
& ( inv1(e10) = e12
| e10 != inv1(e12) )
& ( inv1(e11) = e12
| e11 != inv1(e12) )
& ( inv1(e12) = e12
| e12 != inv1(e12) )
& ( inv1(e13) = e12
| e13 != inv1(e12) )
& ( inv1(e10) = e13
| e10 != inv1(e13) )
& ( inv1(e11) = e13
| e11 != inv1(e13) )
& ( inv1(e12) = e13
| e12 != inv1(e13) )
& ( inv1(e13) = e13
| e13 != inv1(e13) ) ),
inference(ennf_transformation,[],[f11]) ).
fof(f36,definition,
( ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f37,definition,
( ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f38,definition,
( ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f39,definition,
( ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f40,definition,
( ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f41,definition,
( ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f42,definition,
( ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f43,definition,
( ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f44,definition,
( ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f45,definition,
( ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f46,definition,
( ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f47,definition,
( ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f48,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| sP11
| sP10
| sP9 )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| sP8
| sP7
| sP6 )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| sP5
| sP4
| sP3 )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| sP2
| sP1
| sP0 ) ),
inference(definition_folding,[],[f32,f47,f46,f45,f44,f43,f42,f41,f40,f39,f38,f37,f36]) ).
fof(f55,plain,
( ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ~ sP5 ),
inference(nnf_transformation,[],[f41]) ).
fof(f56,plain,
( ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ~ sP4 ),
inference(nnf_transformation,[],[f40]) ).
fof(f57,plain,
( ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) )
| ~ sP3 ),
inference(nnf_transformation,[],[f39]) ).
fof(f87,plain,
( e21 != h3(e11)
| ~ sP5 ),
inference(cnf_transformation,[],[f55]) ).
fof(f90,plain,
( e22 != h3(e12)
| ~ sP4 ),
inference(cnf_transformation,[],[f56]) ).
fof(f93,plain,
( e23 != h3(e13)
| ~ sP3 ),
inference(cnf_transformation,[],[f57]) ).
fof(f116,plain,
( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(cnf_transformation,[],[f48]) ).
fof(f125,plain,
e12 != e13,
inference(cnf_transformation,[],[f19]) ).
fof(f128,plain,
e10 != e13,
inference(cnf_transformation,[],[f19]) ).
fof(f129,plain,
e10 != e12,
inference(cnf_transformation,[],[f19]) ).
fof(f130,plain,
e10 != e11,
inference(cnf_transformation,[],[f19]) ).
fof(f131,plain,
e13 = op1(e12,e12),
inference(cnf_transformation,[],[f24]) ).
fof(f132,plain,
e11 = op1(e12,op1(e12,e12)),
inference(cnf_transformation,[],[f24]) ).
fof(f133,plain,
e10 = op1(op1(e12,op1(e12,e12)),e12),
inference(cnf_transformation,[],[f24]) ).
fof(f138,plain,
op1(e13,e12) != op1(e13,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f139,plain,
op1(e13,e11) != op1(e13,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f140,plain,
op1(e13,e11) != op1(e13,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f143,plain,
op1(e13,e10) != op1(e13,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f151,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f152,plain,
op1(e11,e11) != op1(e11,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f155,plain,
op1(e11,e10) != op1(e11,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f163,plain,
op1(e11,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f164,plain,
op1(e11,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f167,plain,
op1(e10,e13) != op1(e11,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f168,plain,
op1(e12,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f171,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f186,plain,
( e10 = inv1(e13)
| e11 = inv1(e13)
| e12 = inv1(e13)
| e13 = inv1(e13) ),
inference(cnf_transformation,[],[f4]) ).
fof(f187,plain,
( e10 = inv1(e12)
| e11 = inv1(e12)
| e12 = inv1(e12)
| e13 = inv1(e12) ),
inference(cnf_transformation,[],[f4]) ).
fof(f190,plain,
unit1 = op1(inv1(e13),e13),
inference(cnf_transformation,[],[f4]) ).
fof(f192,plain,
unit1 = op1(inv1(e12),e12),
inference(cnf_transformation,[],[f4]) ).
fof(f193,plain,
unit1 = op1(e12,inv1(e12)),
inference(cnf_transformation,[],[f4]) ).
fof(f198,plain,
( e10 = unit1
| e11 = unit1
| e12 = unit1
| e13 = unit1 ),
inference(cnf_transformation,[],[f3]) ).
fof(f199,plain,
e13 = op1(e13,unit1),
inference(cnf_transformation,[],[f3]) ).
fof(f200,plain,
e13 = op1(unit1,e13),
inference(cnf_transformation,[],[f3]) ).
fof(f201,plain,
e12 = op1(e12,unit1),
inference(cnf_transformation,[],[f3]) ).
fof(f202,plain,
e12 = op1(unit1,e12),
inference(cnf_transformation,[],[f3]) ).
fof(f203,plain,
e11 = op1(e11,unit1),
inference(cnf_transformation,[],[f3]) ).
fof(f204,plain,
e11 = op1(unit1,e11),
inference(cnf_transformation,[],[f3]) ).
fof(f205,plain,
e10 = op1(e10,unit1),
inference(cnf_transformation,[],[f3]) ).
fof(f272,plain,
( e10 = op1(e13,e12)
| e11 = op1(e13,e12)
| e12 = op1(e13,e12)
| e13 = op1(e13,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f273,plain,
( e10 = op1(e13,e11)
| e11 = op1(e13,e11)
| e12 = op1(e13,e11)
| e13 = op1(e13,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f279,plain,
( e10 = op1(e11,e13)
| e11 = op1(e11,e13)
| e12 = op1(e11,e13)
| e13 = op1(e11,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f281,plain,
( e10 = op1(e11,e11)
| e11 = op1(e11,e11)
| e12 = op1(e11,e11)
| e13 = op1(e11,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f309,plain,
e23 = op2(e22,e22),
inference(cnf_transformation,[],[f25]) ).
fof(f310,plain,
e21 = op2(e22,op2(e22,e22)),
inference(cnf_transformation,[],[f25]) ).
fof(f311,plain,
e20 = op2(op2(e22,op2(e22,e22)),e22),
inference(cnf_transformation,[],[f25]) ).
fof(f317,plain,
op2(e23,e21) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f318,plain,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f319,plain,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f320,plain,
op2(e23,e20) != op2(e23,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f321,plain,
op2(e23,e20) != op2(e23,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f323,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f324,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f325,plain,
op2(e22,e20) != op2(e22,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f326,plain,
op2(e22,e20) != op2(e22,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f327,plain,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f328,plain,
op2(e21,e22) != op2(e21,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f330,plain,
op2(e21,e21) != op2(e21,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f332,plain,
op2(e21,e20) != op2(e21,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f334,plain,
op2(e20,e22) != op2(e20,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f335,plain,
op2(e20,e21) != op2(e20,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f336,plain,
op2(e20,e21) != op2(e20,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f337,plain,
op2(e20,e20) != op2(e20,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f338,plain,
op2(e20,e20) != op2(e20,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f339,plain,
op2(e20,e20) != op2(e20,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f340,plain,
op2(e22,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f341,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f342,plain,
op2(e21,e23) != op2(e22,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f343,plain,
op2(e20,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f344,plain,
op2(e20,e23) != op2(e22,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f345,plain,
op2(e20,e23) != op2(e21,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f349,plain,
op2(e20,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f350,plain,
op2(e20,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f351,plain,
op2(e20,e22) != op2(e21,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f352,plain,
op2(e22,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f353,plain,
op2(e21,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f354,plain,
op2(e21,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f355,plain,
op2(e20,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f356,plain,
op2(e20,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f357,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f359,plain,
op2(e21,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f18]) ).
fof(f360,plain,
op2(e21,e20) != op2(e22,e20),
inference(cnf_transformation,[],[f18]) ).
fof(f361,plain,
op2(e20,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f18]) ).
fof(f362,plain,
op2(e20,e20) != op2(e22,e20),
inference(cnf_transformation,[],[f18]) ).
fof(f364,plain,
op2(op2(e23,e23),e23) = op2(e23,op2(e23,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f365,plain,
op2(op2(e23,e23),e22) = op2(e23,op2(e23,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f366,plain,
op2(op2(e23,e23),e21) = op2(e23,op2(e23,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f385,plain,
op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f427,plain,
op2(op2(e20,e20),e20) = op2(e20,op2(e20,e20)),
inference(cnf_transformation,[],[f6]) ).
fof(f428,plain,
( e20 = op2(e23,e23)
| e21 = op2(e23,e23)
| e22 = op2(e23,e23)
| e23 = op2(e23,e23) ),
inference(cnf_transformation,[],[f5]) ).
fof(f430,plain,
( e20 = op2(e23,e21)
| e21 = op2(e23,e21)
| e22 = op2(e23,e21)
| e23 = op2(e23,e21) ),
inference(cnf_transformation,[],[f5]) ).
fof(f431,plain,
( e20 = op2(e23,e20)
| e21 = op2(e23,e20)
| e22 = op2(e23,e20)
| e23 = op2(e23,e20) ),
inference(cnf_transformation,[],[f5]) ).
fof(f434,plain,
( e20 = op2(e22,e21)
| e21 = op2(e22,e21)
| e22 = op2(e22,e21)
| e23 = op2(e22,e21) ),
inference(cnf_transformation,[],[f5]) ).
fof(f435,plain,
( e20 = op2(e22,e20)
| e21 = op2(e22,e20)
| e22 = op2(e22,e20)
| e23 = op2(e22,e20) ),
inference(cnf_transformation,[],[f5]) ).
fof(f436,plain,
( e20 = op2(e21,e23)
| e21 = op2(e21,e23)
| e22 = op2(e21,e23)
| e23 = op2(e21,e23) ),
inference(cnf_transformation,[],[f5]) ).
fof(f438,plain,
( e20 = op2(e21,e21)
| e21 = op2(e21,e21)
| e22 = op2(e21,e21)
| e23 = op2(e21,e21) ),
inference(cnf_transformation,[],[f5]) ).
fof(f439,plain,
( e20 = op2(e21,e20)
| e21 = op2(e21,e20)
| e22 = op2(e21,e20)
| e23 = op2(e21,e20) ),
inference(cnf_transformation,[],[f5]) ).
fof(f440,plain,
( e20 = op2(e20,e23)
| e21 = op2(e20,e23)
| e22 = op2(e20,e23)
| e23 = op2(e20,e23) ),
inference(cnf_transformation,[],[f5]) ).
fof(f441,plain,
( e20 = op2(e20,e22)
| e21 = op2(e20,e22)
| e22 = op2(e20,e22)
| e23 = op2(e20,e22) ),
inference(cnf_transformation,[],[f5]) ).
fof(f442,plain,
( e20 = op2(e20,e21)
| e21 = op2(e20,e21)
| e22 = op2(e20,e21)
| e23 = op2(e20,e21) ),
inference(cnf_transformation,[],[f5]) ).
fof(f443,plain,
( e20 = op2(e20,e20)
| op2(e20,e20) = e21
| op2(e20,e20) = e22
| op2(e20,e20) = e23 ),
inference(cnf_transformation,[],[f5]) ).
fof(f444,plain,
op2(e20,e20) = h1(e13),
inference(cnf_transformation,[],[f26]) ).
fof(f445,plain,
op2(e20,op2(e20,e20)) = h1(e11),
inference(cnf_transformation,[],[f26]) ).
fof(f448,plain,
op2(e21,e21) = h2(e13),
inference(cnf_transformation,[],[f27]) ).
fof(f452,plain,
op2(e22,e22) = h3(e13),
inference(cnf_transformation,[],[f28]) ).
fof(f453,plain,
op2(e22,op2(e22,e22)) = h3(e11),
inference(cnf_transformation,[],[f28]) ).
fof(f454,plain,
op2(op2(e22,op2(e22,e22)),e22) = h3(e10),
inference(cnf_transformation,[],[f28]) ).
fof(f455,plain,
e22 = h3(e12),
inference(cnf_transformation,[],[f28]) ).
fof(f456,plain,
op2(e23,e23) = h4(e13),
inference(cnf_transformation,[],[f29]) ).
fof(f457,plain,
op2(e23,op2(e23,e23)) = h4(e11),
inference(cnf_transformation,[],[f29]) ).
fof(f460,plain,
unit1 = inv1(unit1),
inference(cnf_transformation,[],[f9]) ).
fof(f469,plain,
( e13 = inv1(e11)
| e11 != inv1(e13) ),
inference(cnf_transformation,[],[f35]) ).
fof(f470,plain,
( e13 = inv1(e10)
| e10 != inv1(e13) ),
inference(cnf_transformation,[],[f35]) ).
fof(f471,plain,
( e12 = inv1(e13)
| e13 != inv1(e12) ),
inference(cnf_transformation,[],[f35]) ).
fof(f474,plain,
( e12 = inv1(e10)
| e10 != inv1(e12) ),
inference(cnf_transformation,[],[f35]) ).
fof(f484,plain,
e12 = inv1(inv1(e12)),
inference(cnf_transformation,[],[f10]) ).
fof(f488,definition,
( spl12_1
<=> e12 = inv1(e13) ),
introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition]) ).
fof(f489,plain,
( e12 = inv1(e13)
| ~ spl12_1 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f492,definition,
( spl12_2
<=> e13 = inv1(e12) ),
introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition]) ).
fof(f497,definition,
( spl12_3
<=> e11 = inv1(e13) ),
introduced(definition,[new_symbols(definition,[spl12_3])],[avatar_definition]) ).
fof(f501,definition,
( spl12_4
<=> e13 = inv1(e11) ),
introduced(definition,[new_symbols(definition,[spl12_4])],[avatar_definition]) ).
fof(f503,plain,
( e13 = inv1(e11)
| ~ spl12_4 ),
inference(avatar_component_clause,[],[f501]) ).
fof(f504,plain,
( ~ spl12_3
| spl12_4 ),
inference(avatar_split_clause,[],[f469,f501,f497]) ).
fof(f506,definition,
( spl12_5
<=> e10 = inv1(e13) ),
introduced(definition,[new_symbols(definition,[spl12_5])],[avatar_definition]) ).
fof(f510,definition,
( spl12_6
<=> e13 = inv1(e10) ),
introduced(definition,[new_symbols(definition,[spl12_6])],[avatar_definition]) ).
fof(f512,plain,
( e13 = inv1(e10)
| ~ spl12_6 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f513,plain,
( ~ spl12_5
| spl12_6 ),
inference(avatar_split_clause,[],[f470,f510,f506]) ).
fof(f514,plain,
( ~ spl12_2
| spl12_1 ),
inference(avatar_split_clause,[],[f471,f488,f492]) ).
fof(f516,definition,
( spl12_7
<=> e11 = inv1(e12) ),
introduced(definition,[new_symbols(definition,[spl12_7])],[avatar_definition]) ).
fof(f517,plain,
( e11 = inv1(e12)
| ~ spl12_7 ),
inference(avatar_component_clause,[],[f516]) ).
fof(f520,definition,
( spl12_8
<=> e12 = inv1(e11) ),
introduced(definition,[new_symbols(definition,[spl12_8])],[avatar_definition]) ).
fof(f522,plain,
( e12 = inv1(e11)
| ~ spl12_8 ),
inference(avatar_component_clause,[],[f520]) ).
fof(f525,definition,
( spl12_9
<=> e10 = inv1(e12) ),
introduced(definition,[new_symbols(definition,[spl12_9])],[avatar_definition]) ).
fof(f529,definition,
( spl12_10
<=> e12 = inv1(e10) ),
introduced(definition,[new_symbols(definition,[spl12_10])],[avatar_definition]) ).
fof(f531,plain,
( e12 = inv1(e10)
| ~ spl12_10 ),
inference(avatar_component_clause,[],[f529]) ).
fof(f532,plain,
( ~ spl12_9
| spl12_10 ),
inference(avatar_split_clause,[],[f474,f529,f525]) ).
fof(f547,plain,
h4(e11) = op2(e23,h4(e13)),
inference(forward_demodulation,[],[f457,f456]) ).
fof(f549,plain,
h3(e11) = op2(e22,h3(e13)),
inference(forward_demodulation,[],[f453,f452]) ).
fof(f550,plain,
h3(e10) = op2(op2(e22,h3(e13)),e22),
inference(forward_demodulation,[],[f454,f452]) ).
fof(f553,plain,
h1(e11) = op2(e20,h1(e13)),
inference(forward_demodulation,[],[f445,f444]) ).
fof(f555,plain,
( e20 = h4(e13)
| e21 = op2(e23,e23)
| e22 = op2(e23,e23)
| e23 = op2(e23,e23) ),
inference(forward_demodulation,[],[f428,f456]) ).
fof(f565,definition,
( spl12_15
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_15])],[avatar_definition]) ).
fof(f566,plain,
( e21 != op2(e23,e22)
| spl12_15 ),
inference(avatar_component_clause,[],[f565]) ).
fof(f567,plain,
( e21 = op2(e23,e22)
| ~ spl12_15 ),
inference(avatar_component_clause,[],[f565]) ).
fof(f574,definition,
( spl12_17
<=> e23 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_17])],[avatar_definition]) ).
fof(f576,plain,
( e23 = op2(e23,e21)
| ~ spl12_17 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f578,definition,
( spl12_18
<=> e22 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_18])],[avatar_definition]) ).
fof(f580,plain,
( e22 = op2(e23,e21)
| ~ spl12_18 ),
inference(avatar_component_clause,[],[f578]) ).
fof(f582,definition,
( spl12_19
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_19])],[avatar_definition]) ).
fof(f586,definition,
( spl12_20
<=> e20 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_20])],[avatar_definition]) ).
fof(f588,plain,
( e20 = op2(e23,e21)
| ~ spl12_20 ),
inference(avatar_component_clause,[],[f586]) ).
fof(f589,plain,
( spl12_17
| spl12_18
| spl12_19
| spl12_20 ),
inference(avatar_split_clause,[],[f430,f586,f582,f578,f574]) ).
fof(f591,definition,
( spl12_21
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_21])],[avatar_definition]) ).
fof(f592,plain,
( e23 != op2(e23,e20)
| spl12_21 ),
inference(avatar_component_clause,[],[f591]) ).
fof(f593,plain,
( e23 = op2(e23,e20)
| ~ spl12_21 ),
inference(avatar_component_clause,[],[f591]) ).
fof(f595,definition,
( spl12_22
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_22])],[avatar_definition]) ).
fof(f597,plain,
( e22 = op2(e23,e20)
| ~ spl12_22 ),
inference(avatar_component_clause,[],[f595]) ).
fof(f599,definition,
( spl12_23
<=> e21 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_23])],[avatar_definition]) ).
fof(f603,definition,
( spl12_24
<=> e20 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_24])],[avatar_definition]) ).
fof(f605,plain,
( e20 = op2(e23,e20)
| ~ spl12_24 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f606,plain,
( spl12_21
| spl12_22
| spl12_23
| spl12_24 ),
inference(avatar_split_clause,[],[f431,f603,f599,f595,f591]) ).
fof(f616,definition,
( spl12_27
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_27])],[avatar_definition]) ).
fof(f618,plain,
( e21 = op2(e22,e23)
| ~ spl12_27 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f626,definition,
( spl12_29
<=> e23 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_29])],[avatar_definition]) ).
fof(f628,plain,
( e23 = op2(e22,e21)
| ~ spl12_29 ),
inference(avatar_component_clause,[],[f626]) ).
fof(f630,definition,
( spl12_30
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_30])],[avatar_definition]) ).
fof(f631,plain,
( e22 != op2(e22,e21)
| spl12_30 ),
inference(avatar_component_clause,[],[f630]) ).
fof(f632,plain,
( e22 = op2(e22,e21)
| ~ spl12_30 ),
inference(avatar_component_clause,[],[f630]) ).
fof(f634,definition,
( spl12_31
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_31])],[avatar_definition]) ).
fof(f636,plain,
( e21 = op2(e22,e21)
| ~ spl12_31 ),
inference(avatar_component_clause,[],[f634]) ).
fof(f638,definition,
( spl12_32
<=> e20 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_32])],[avatar_definition]) ).
fof(f640,plain,
( e20 = op2(e22,e21)
| ~ spl12_32 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f641,plain,
( spl12_29
| spl12_30
| spl12_31
| spl12_32 ),
inference(avatar_split_clause,[],[f434,f638,f634,f630,f626]) ).
fof(f643,definition,
( spl12_33
<=> e23 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_33])],[avatar_definition]) ).
fof(f645,plain,
( e23 = op2(e22,e20)
| ~ spl12_33 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f647,definition,
( spl12_34
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_34])],[avatar_definition]) ).
fof(f649,plain,
( e22 = op2(e22,e20)
| ~ spl12_34 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f651,definition,
( spl12_35
<=> e21 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_35])],[avatar_definition]) ).
fof(f655,definition,
( spl12_36
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_36])],[avatar_definition]) ).
fof(f657,plain,
( e20 = op2(e22,e20)
| ~ spl12_36 ),
inference(avatar_component_clause,[],[f655]) ).
fof(f658,plain,
( spl12_33
| spl12_34
| spl12_35
| spl12_36 ),
inference(avatar_split_clause,[],[f435,f655,f651,f647,f643]) ).
fof(f660,definition,
( spl12_37
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_37])],[avatar_definition]) ).
fof(f662,plain,
( e23 = op2(e21,e23)
| ~ spl12_37 ),
inference(avatar_component_clause,[],[f660]) ).
fof(f664,definition,
( spl12_38
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_38])],[avatar_definition]) ).
fof(f666,plain,
( e22 = op2(e21,e23)
| ~ spl12_38 ),
inference(avatar_component_clause,[],[f664]) ).
fof(f668,definition,
( spl12_39
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_39])],[avatar_definition]) ).
fof(f670,plain,
( e21 = op2(e21,e23)
| ~ spl12_39 ),
inference(avatar_component_clause,[],[f668]) ).
fof(f672,definition,
( spl12_40
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_40])],[avatar_definition]) ).
fof(f674,plain,
( e20 = op2(e21,e23)
| ~ spl12_40 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f675,plain,
( spl12_37
| spl12_38
| spl12_39
| spl12_40 ),
inference(avatar_split_clause,[],[f436,f672,f668,f664,f660]) ).
fof(f689,definition,
( spl12_44
<=> e20 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_44])],[avatar_definition]) ).
fof(f691,plain,
( e20 = op2(e21,e22)
| ~ spl12_44 ),
inference(avatar_component_clause,[],[f689]) ).
fof(f693,plain,
( e20 = h2(e13)
| e21 = op2(e21,e21)
| e22 = op2(e21,e21)
| e23 = op2(e21,e21) ),
inference(forward_demodulation,[],[f438,f448]) ).
fof(f695,definition,
( spl12_45
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_45])],[avatar_definition]) ).
fof(f696,plain,
( e23 != op2(e21,e20)
| spl12_45 ),
inference(avatar_component_clause,[],[f695]) ).
fof(f699,definition,
( spl12_46
<=> e22 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_46])],[avatar_definition]) ).
fof(f703,definition,
( spl12_47
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_47])],[avatar_definition]) ).
fof(f705,plain,
( e21 = op2(e21,e20)
| ~ spl12_47 ),
inference(avatar_component_clause,[],[f703]) ).
fof(f707,definition,
( spl12_48
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_48])],[avatar_definition]) ).
fof(f709,plain,
( e20 = op2(e21,e20)
| ~ spl12_48 ),
inference(avatar_component_clause,[],[f707]) ).
fof(f710,plain,
( spl12_45
| spl12_46
| spl12_47
| spl12_48 ),
inference(avatar_split_clause,[],[f439,f707,f703,f699,f695]) ).
fof(f712,definition,
( spl12_49
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_49])],[avatar_definition]) ).
fof(f714,plain,
( e23 = op2(e20,e23)
| ~ spl12_49 ),
inference(avatar_component_clause,[],[f712]) ).
fof(f716,definition,
( spl12_50
<=> e22 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_50])],[avatar_definition]) ).
fof(f718,plain,
( e22 = op2(e20,e23)
| ~ spl12_50 ),
inference(avatar_component_clause,[],[f716]) ).
fof(f720,definition,
( spl12_51
<=> e21 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_51])],[avatar_definition]) ).
fof(f722,plain,
( e21 = op2(e20,e23)
| ~ spl12_51 ),
inference(avatar_component_clause,[],[f720]) ).
fof(f724,definition,
( spl12_52
<=> e20 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_52])],[avatar_definition]) ).
fof(f726,plain,
( e20 = op2(e20,e23)
| ~ spl12_52 ),
inference(avatar_component_clause,[],[f724]) ).
fof(f727,plain,
( spl12_49
| spl12_50
| spl12_51
| spl12_52 ),
inference(avatar_split_clause,[],[f440,f724,f720,f716,f712]) ).
fof(f729,definition,
( spl12_53
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_53])],[avatar_definition]) ).
fof(f731,plain,
( e23 = op2(e20,e22)
| ~ spl12_53 ),
inference(avatar_component_clause,[],[f729]) ).
fof(f733,definition,
( spl12_54
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_54])],[avatar_definition]) ).
fof(f735,plain,
( e22 = op2(e20,e22)
| ~ spl12_54 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f737,definition,
( spl12_55
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_55])],[avatar_definition]) ).
fof(f741,definition,
( spl12_56
<=> e20 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_56])],[avatar_definition]) ).
fof(f744,plain,
( spl12_53
| spl12_54
| spl12_55
| spl12_56 ),
inference(avatar_split_clause,[],[f441,f741,f737,f733,f729]) ).
fof(f746,definition,
( spl12_57
<=> e23 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_57])],[avatar_definition]) ).
fof(f748,plain,
( e23 = op2(e20,e21)
| ~ spl12_57 ),
inference(avatar_component_clause,[],[f746]) ).
fof(f750,definition,
( spl12_58
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_58])],[avatar_definition]) ).
fof(f754,definition,
( spl12_59
<=> e21 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_59])],[avatar_definition]) ).
fof(f756,plain,
( e21 = op2(e20,e21)
| ~ spl12_59 ),
inference(avatar_component_clause,[],[f754]) ).
fof(f758,definition,
( spl12_60
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_60])],[avatar_definition]) ).
fof(f761,plain,
( spl12_57
| spl12_58
| spl12_59
| spl12_60 ),
inference(avatar_split_clause,[],[f442,f758,f754,f750,f746]) ).
fof(f762,plain,
( e20 = h1(e13)
| op2(e20,e20) = e21
| op2(e20,e20) = e22
| op2(e20,e20) = e23 ),
inference(forward_demodulation,[],[f443,f444]) ).
fof(f763,plain,
op2(e23,h4(e13)) = op2(h4(e13),e23),
inference(forward_demodulation,[],[f364,f456]) ).
fof(f764,plain,
op2(e23,op2(e23,e22)) = op2(h4(e13),e22),
inference(forward_demodulation,[],[f365,f456]) ).
fof(f765,plain,
op2(e23,op2(e23,e21)) = op2(h4(e13),e21),
inference(forward_demodulation,[],[f366,f456]) ).
fof(f772,plain,
op2(e22,h3(e13)) = op2(h3(e13),e22),
inference(forward_demodulation,[],[f385,f452]) ).
fof(f790,plain,
op2(e20,h1(e13)) = op2(h1(e13),e20),
inference(forward_demodulation,[],[f427,f444]) ).
fof(f792,plain,
op2(e23,e21) != h4(e13),
inference(forward_demodulation,[],[f317,f456]) ).
fof(f793,plain,
op2(e23,e20) != h4(e13),
inference(forward_demodulation,[],[f319,f456]) ).
fof(f795,plain,
op2(e22,e21) != h3(e13),
inference(forward_demodulation,[],[f324,f452]) ).
fof(f796,plain,
op2(e22,e20) != h3(e13),
inference(forward_demodulation,[],[f326,f452]) ).
fof(f798,plain,
op2(e21,e22) != h2(e13),
inference(forward_demodulation,[],[f330,f448]) ).
fof(f800,plain,
op2(e20,e23) != h1(e13),
inference(forward_demodulation,[],[f337,f444]) ).
fof(f801,plain,
op2(e20,e22) != h1(e13),
inference(forward_demodulation,[],[f338,f444]) ).
fof(f802,plain,
op2(e20,e21) != h1(e13),
inference(forward_demodulation,[],[f339,f444]) ).
fof(f803,plain,
op2(e22,e23) != h4(e13),
inference(forward_demodulation,[],[f340,f456]) ).
fof(f804,plain,
op2(e21,e23) != h4(e13),
inference(forward_demodulation,[],[f341,f456]) ).
fof(f805,plain,
op2(e20,e23) != h4(e13),
inference(forward_demodulation,[],[f343,f456]) ).
fof(f808,plain,
op2(e20,e22) != h3(e13),
inference(forward_demodulation,[],[f350,f452]) ).
fof(f809,plain,
op2(e23,e21) != h2(e13),
inference(forward_demodulation,[],[f353,f448]) ).
fof(f810,plain,
op2(e22,e21) != h2(e13),
inference(forward_demodulation,[],[f354,f448]) ).
fof(f811,plain,
op2(e20,e21) != h2(e13),
inference(forward_demodulation,[],[f357,f448]) ).
fof(f812,plain,
op2(e23,e20) != h1(e13),
inference(forward_demodulation,[],[f361,f444]) ).
fof(f813,plain,
op2(e22,e20) != h1(e13),
inference(forward_demodulation,[],[f362,f444]) ).
fof(f819,plain,
e21 = op2(e22,h3(e13)),
inference(forward_demodulation,[],[f310,f452]) ).
fof(f820,plain,
e20 = op2(op2(e22,h3(e13)),e22),
inference(forward_demodulation,[],[f311,f452]) ).
fof(f834,definition,
( spl12_64
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_64])],[avatar_definition]) ).
fof(f836,plain,
( e10 = op1(e13,e13)
| ~ spl12_64 ),
inference(avatar_component_clause,[],[f834]) ).
fof(f839,definition,
( spl12_65
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_65])],[avatar_definition]) ).
fof(f841,plain,
( e13 = op1(e13,e12)
| ~ spl12_65 ),
inference(avatar_component_clause,[],[f839]) ).
fof(f843,definition,
( spl12_66
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_66])],[avatar_definition]) ).
fof(f845,plain,
( e12 = op1(e13,e12)
| ~ spl12_66 ),
inference(avatar_component_clause,[],[f843]) ).
fof(f847,definition,
( spl12_67
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_67])],[avatar_definition]) ).
fof(f849,plain,
( e11 = op1(e13,e12)
| ~ spl12_67 ),
inference(avatar_component_clause,[],[f847]) ).
fof(f851,definition,
( spl12_68
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_68])],[avatar_definition]) ).
fof(f854,plain,
( spl12_65
| spl12_66
| spl12_67
| spl12_68 ),
inference(avatar_split_clause,[],[f272,f851,f847,f843,f839]) ).
fof(f856,definition,
( spl12_69
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_69])],[avatar_definition]) ).
fof(f858,plain,
( e13 = op1(e13,e11)
| ~ spl12_69 ),
inference(avatar_component_clause,[],[f856]) ).
fof(f860,definition,
( spl12_70
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_70])],[avatar_definition]) ).
fof(f862,plain,
( e12 = op1(e13,e11)
| ~ spl12_70 ),
inference(avatar_component_clause,[],[f860]) ).
fof(f864,definition,
( spl12_71
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_71])],[avatar_definition]) ).
fof(f868,definition,
( spl12_72
<=> e10 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_72])],[avatar_definition]) ).
fof(f871,plain,
( spl12_69
| spl12_70
| spl12_71
| spl12_72 ),
inference(avatar_split_clause,[],[f273,f868,f864,f860,f856]) ).
fof(f873,definition,
( spl12_73
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_73])],[avatar_definition]) ).
fof(f874,plain,
( e13 != op1(e13,e10)
| spl12_73 ),
inference(avatar_component_clause,[],[f873]) ).
fof(f875,plain,
( e13 = op1(e13,e10)
| ~ spl12_73 ),
inference(avatar_component_clause,[],[f873]) ).
fof(f898,definition,
( spl12_79
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_79])],[avatar_definition]) ).
fof(f900,plain,
( e11 = op1(e12,e13)
| ~ spl12_79 ),
inference(avatar_component_clause,[],[f898]) ).
fof(f902,definition,
( spl12_80
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_80])],[avatar_definition]) ).
fof(f904,plain,
( e10 = op1(e12,e13)
| ~ spl12_80 ),
inference(avatar_component_clause,[],[f902]) ).
fof(f907,definition,
( spl12_81
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_81])],[avatar_definition]) ).
fof(f909,plain,
( e13 = op1(e12,e12)
| ~ spl12_81 ),
inference(avatar_component_clause,[],[f907]) ).
fof(f919,definition,
( spl12_84
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_84])],[avatar_definition]) ).
fof(f921,plain,
( e10 = op1(e12,e12)
| ~ spl12_84 ),
inference(avatar_component_clause,[],[f919]) ).
fof(f936,definition,
( spl12_88
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_88])],[avatar_definition]) ).
fof(f938,plain,
( e10 = op1(e12,e11)
| ~ spl12_88 ),
inference(avatar_component_clause,[],[f936]) ).
fof(f945,definition,
( spl12_90
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_90])],[avatar_definition]) ).
fof(f947,plain,
( e12 = op1(e12,e10)
| ~ spl12_90 ),
inference(avatar_component_clause,[],[f945]) ).
fof(f958,definition,
( spl12_93
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_93])],[avatar_definition]) ).
fof(f960,plain,
( e13 = op1(e11,e13)
| ~ spl12_93 ),
inference(avatar_component_clause,[],[f958]) ).
fof(f962,definition,
( spl12_94
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_94])],[avatar_definition]) ).
fof(f964,plain,
( e12 = op1(e11,e13)
| ~ spl12_94 ),
inference(avatar_component_clause,[],[f962]) ).
fof(f966,definition,
( spl12_95
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_95])],[avatar_definition]) ).
fof(f968,plain,
( e11 = op1(e11,e13)
| ~ spl12_95 ),
inference(avatar_component_clause,[],[f966]) ).
fof(f970,definition,
( spl12_96
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_96])],[avatar_definition]) ).
fof(f973,plain,
( spl12_93
| spl12_94
| spl12_95
| spl12_96 ),
inference(avatar_split_clause,[],[f279,f970,f966,f962,f958]) ).
fof(f987,definition,
( spl12_100
<=> e10 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_100])],[avatar_definition]) ).
fof(f989,plain,
( e10 = op1(e11,e12)
| ~ spl12_100 ),
inference(avatar_component_clause,[],[f987]) ).
fof(f992,definition,
( spl12_101
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_101])],[avatar_definition]) ).
fof(f994,plain,
( e13 = op1(e11,e11)
| ~ spl12_101 ),
inference(avatar_component_clause,[],[f992]) ).
fof(f996,definition,
( spl12_102
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_102])],[avatar_definition]) ).
fof(f1000,definition,
( spl12_103
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_103])],[avatar_definition]) ).
fof(f1002,plain,
( e11 = op1(e11,e11)
| ~ spl12_103 ),
inference(avatar_component_clause,[],[f1000]) ).
fof(f1004,definition,
( spl12_104
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_104])],[avatar_definition]) ).
fof(f1006,plain,
( e10 = op1(e11,e11)
| ~ spl12_104 ),
inference(avatar_component_clause,[],[f1004]) ).
fof(f1007,plain,
( spl12_101
| spl12_102
| spl12_103
| spl12_104 ),
inference(avatar_split_clause,[],[f281,f1004,f1000,f996,f992]) ).
fof(f1017,definition,
( spl12_107
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl12_107])],[avatar_definition]) ).
fof(f1019,plain,
( e11 = op1(e11,e10)
| ~ spl12_107 ),
inference(avatar_component_clause,[],[f1017]) ).
fof(f1026,definition,
( spl12_109
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_109])],[avatar_definition]) ).
fof(f1027,plain,
( e13 != op1(e10,e13)
| spl12_109 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1028,plain,
( e13 = op1(e10,e13)
| ~ spl12_109 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1047,definition,
( spl12_114
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_114])],[avatar_definition]) ).
fof(f1049,plain,
( e12 = op1(e10,e12)
| ~ spl12_114 ),
inference(avatar_component_clause,[],[f1047]) ).
fof(f1068,definition,
( spl12_119
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_119])],[avatar_definition]) ).
fof(f1070,plain,
( e11 = op1(e10,e11)
| ~ spl12_119 ),
inference(avatar_component_clause,[],[f1068]) ).
fof(f1089,definition,
( spl12_124
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl12_124])],[avatar_definition]) ).
fof(f1091,plain,
( e10 = op1(e10,e10)
| ~ spl12_124 ),
inference(avatar_component_clause,[],[f1089]) ).
fof(f1094,definition,
( spl12_125
<=> e13 = unit1 ),
introduced(definition,[new_symbols(definition,[spl12_125])],[avatar_definition]) ).
fof(f1096,plain,
( e13 = unit1
| ~ spl12_125 ),
inference(avatar_component_clause,[],[f1094]) ).
fof(f1098,definition,
( spl12_126
<=> e12 = unit1 ),
introduced(definition,[new_symbols(definition,[spl12_126])],[avatar_definition]) ).
fof(f1100,plain,
( e12 = unit1
| ~ spl12_126 ),
inference(avatar_component_clause,[],[f1098]) ).
fof(f1102,definition,
( spl12_127
<=> e11 = unit1 ),
introduced(definition,[new_symbols(definition,[spl12_127])],[avatar_definition]) ).
fof(f1104,plain,
( e11 = unit1
| ~ spl12_127 ),
inference(avatar_component_clause,[],[f1102]) ).
fof(f1106,definition,
( spl12_128
<=> e10 = unit1 ),
introduced(definition,[new_symbols(definition,[spl12_128])],[avatar_definition]) ).
fof(f1108,plain,
( e10 = unit1
| ~ spl12_128 ),
inference(avatar_component_clause,[],[f1106]) ).
fof(f1109,plain,
( spl12_125
| spl12_126
| spl12_127
| spl12_128 ),
inference(avatar_split_clause,[],[f198,f1106,f1102,f1098,f1094]) ).
fof(f1111,definition,
( spl12_129
<=> e13 = inv1(e13) ),
introduced(definition,[new_symbols(definition,[spl12_129])],[avatar_definition]) ).
fof(f1113,plain,
( e13 = inv1(e13)
| ~ spl12_129 ),
inference(avatar_component_clause,[],[f1111]) ).
fof(f1114,plain,
( spl12_129
| spl12_1
| spl12_3
| spl12_5 ),
inference(avatar_split_clause,[],[f186,f506,f497,f488,f1111]) ).
fof(f1116,definition,
( spl12_130
<=> e12 = inv1(e12) ),
introduced(definition,[new_symbols(definition,[spl12_130])],[avatar_definition]) ).
fof(f1118,plain,
( e12 = inv1(e12)
| ~ spl12_130 ),
inference(avatar_component_clause,[],[f1116]) ).
fof(f1119,plain,
( spl12_2
| spl12_130
| spl12_7
| spl12_9 ),
inference(avatar_split_clause,[],[f187,f525,f516,f1116,f492]) ).
fof(f1126,definition,
( spl12_132
<=> e10 = inv1(e10) ),
introduced(definition,[new_symbols(definition,[spl12_132])],[avatar_definition]) ).
fof(f1128,plain,
( e10 = inv1(e10)
| ~ spl12_132 ),
inference(avatar_component_clause,[],[f1126]) ).
fof(f1134,plain,
spl12_81,
inference(avatar_split_clause,[],[f131,f907]) ).
fof(f1135,plain,
e10 = op1(e11,e12),
inference(forward_demodulation,[],[f133,f132]) ).
fof(f1143,plain,
( h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f116,f455]) ).
fof(f1157,definition,
( spl12_134
<=> e23 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl12_134])],[avatar_definition]) ).
fof(f1158,plain,
( e23 = h4(e13)
| ~ spl12_134 ),
inference(avatar_component_clause,[],[f1157]) ).
fof(f1163,definition,
( spl12_135
<=> e23 = h4(e11) ),
introduced(definition,[new_symbols(definition,[spl12_135])],[avatar_definition]) ).
fof(f1164,plain,
( e23 = h4(e11)
| ~ spl12_135 ),
inference(avatar_component_clause,[],[f1163]) ).
fof(f1165,plain,
( e23 != h4(e11)
| spl12_135 ),
inference(avatar_component_clause,[],[f1163]) ).
fof(f1177,definition,
( spl12_138
<=> e22 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl12_138])],[avatar_definition]) ).
fof(f1178,plain,
( e22 = h4(e13)
| ~ spl12_138 ),
inference(avatar_component_clause,[],[f1177]) ).
fof(f1197,definition,
( spl12_142
<=> e21 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl12_142])],[avatar_definition]) ).
fof(f1198,plain,
( e21 = h4(e13)
| ~ spl12_142 ),
inference(avatar_component_clause,[],[f1197]) ).
fof(f1213,definition,
( spl12_145
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl12_145])],[avatar_definition]) ).
fof(f1217,definition,
( spl12_146
<=> e23 = h3(e13) ),
introduced(definition,[new_symbols(definition,[spl12_146])],[avatar_definition]) ).
fof(f1218,plain,
( e23 = h3(e13)
| ~ spl12_146 ),
inference(avatar_component_clause,[],[f1217]) ).
fof(f1220,plain,
( ~ spl12_145
| ~ spl12_146 ),
inference(avatar_split_clause,[],[f93,f1217,f1213]) ).
fof(f1233,definition,
( spl12_149
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl12_149])],[avatar_definition]) ).
fof(f1241,plain,
~ sP4,
inference(forward_subsumption_resolution,[],[f90,f455]) ).
fof(f1253,definition,
( spl12_153
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl12_153])],[avatar_definition]) ).
fof(f1263,definition,
( spl12_155
<=> e21 = h3(e11) ),
introduced(definition,[new_symbols(definition,[spl12_155])],[avatar_definition]) ).
fof(f1264,plain,
( e21 = h3(e11)
| ~ spl12_155 ),
inference(avatar_component_clause,[],[f1263]) ).
fof(f1266,plain,
( ~ spl12_153
| ~ spl12_155 ),
inference(avatar_split_clause,[],[f87,f1263,f1253]) ).
fof(f1277,definition,
( spl12_158
<=> e23 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl12_158])],[avatar_definition]) ).
fof(f1278,plain,
( e23 = h2(e13)
| ~ spl12_158 ),
inference(avatar_component_clause,[],[f1277]) ).
fof(f1297,definition,
( spl12_162
<=> e22 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl12_162])],[avatar_definition]) ).
fof(f1298,plain,
( e22 = h2(e13)
| ~ spl12_162 ),
inference(avatar_component_clause,[],[f1297]) ).
fof(f1317,definition,
( spl12_166
<=> e21 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl12_166])],[avatar_definition]) ).
fof(f1337,definition,
( spl12_170
<=> e23 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl12_170])],[avatar_definition]) ).
fof(f1343,definition,
( spl12_171
<=> e23 = h1(e11) ),
introduced(definition,[new_symbols(definition,[spl12_171])],[avatar_definition]) ).
fof(f1344,plain,
( e23 = h1(e11)
| ~ spl12_171 ),
inference(avatar_component_clause,[],[f1343]) ).
fof(f1357,definition,
( spl12_174
<=> e22 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl12_174])],[avatar_definition]) ).
fof(f1377,definition,
( spl12_178
<=> e21 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl12_178])],[avatar_definition]) ).
fof(f1378,plain,
( e21 = h1(e13)
| ~ spl12_178 ),
inference(avatar_component_clause,[],[f1377]) ).
fof(f1393,plain,
h3(e10) = op2(h3(e11),e22),
inference(forward_demodulation,[],[f550,f549]) ).
fof(f1396,plain,
( e21 = h4(e13)
| e20 = h4(e13)
| e22 = op2(e23,e23)
| e23 = op2(e23,e23) ),
inference(forward_demodulation,[],[f555,f456]) ).
fof(f1397,plain,
( e21 = h2(e13)
| e20 = h2(e13)
| e22 = op2(e21,e21)
| e23 = op2(e21,e21) ),
inference(forward_demodulation,[],[f693,f448]) ).
fof(f1398,plain,
( e21 = h1(e13)
| e20 = h1(e13)
| op2(e20,e20) = e22
| op2(e20,e20) = e23 ),
inference(forward_demodulation,[],[f762,f444]) ).
fof(f1399,plain,
h4(e11) = op2(h4(e13),e23),
inference(forward_demodulation,[],[f763,f547]) ).
fof(f1400,plain,
h3(e11) = op2(h3(e13),e22),
inference(forward_demodulation,[],[f772,f549]) ).
fof(f1402,plain,
h1(e11) = op2(h1(e13),e20),
inference(forward_demodulation,[],[f790,f553]) ).
fof(f1407,plain,
e20 = op2(h3(e11),e22),
inference(forward_demodulation,[],[f820,f549]) ).
fof(f1408,plain,
spl12_100,
inference(avatar_split_clause,[],[f1135,f987]) ).
fof(f1416,plain,
( h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,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,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1143,f455]) ).
fof(f1426,plain,
~ spl12_149,
inference(avatar_split_clause,[],[f1241,f1233]) ).
fof(f1428,plain,
( e22 = h4(e13)
| e21 = h4(e13)
| e20 = h4(e13)
| e23 = op2(e23,e23) ),
inference(forward_demodulation,[],[f1396,f456]) ).
fof(f1429,plain,
( e22 = h2(e13)
| e21 = h2(e13)
| e20 = h2(e13)
| e23 = op2(e21,e21) ),
inference(forward_demodulation,[],[f1397,f448]) ).
fof(f1430,plain,
( e22 = h1(e13)
| e21 = h1(e13)
| e20 = h1(e13)
| op2(e20,e20) = e23 ),
inference(forward_demodulation,[],[f1398,f444]) ).
fof(f1442,plain,
( h3(e10) != h3(op1(e11,e12))
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,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,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1416,f1393]) ).
fof(f1451,plain,
( e23 = h4(e13)
| e22 = h4(e13)
| e21 = h4(e13)
| e20 = h4(e13) ),
inference(forward_demodulation,[],[f1428,f456]) ).
fof(f1452,plain,
( e23 = h2(e13)
| e22 = h2(e13)
| e21 = h2(e13)
| e20 = h2(e13) ),
inference(forward_demodulation,[],[f1429,f448]) ).
fof(f1453,plain,
( e23 = h1(e13)
| e22 = h1(e13)
| e21 = h1(e13)
| e20 = h1(e13) ),
inference(forward_demodulation,[],[f1430,f444]) ).
fof(f1465,plain,
( h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(e10) != h3(op1(e11,e12))
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,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,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1442,f455]) ).
fof(f1475,definition,
( spl12_181
<=> e20 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl12_181])],[avatar_definition]) ).
fof(f1477,plain,
( e20 = h4(e13)
| ~ spl12_181 ),
inference(avatar_component_clause,[],[f1475]) ).
fof(f1478,plain,
( spl12_181
| spl12_142
| spl12_138
| spl12_134 ),
inference(avatar_split_clause,[],[f1451,f1157,f1177,f1197,f1475]) ).
fof(f1480,definition,
( spl12_182
<=> e20 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl12_182])],[avatar_definition]) ).
fof(f1482,plain,
( e20 = h2(e13)
| ~ spl12_182 ),
inference(avatar_component_clause,[],[f1480]) ).
fof(f1483,plain,
( spl12_182
| spl12_166
| spl12_162
| spl12_158 ),
inference(avatar_split_clause,[],[f1452,f1277,f1297,f1317,f1480]) ).
fof(f1485,definition,
( spl12_183
<=> e20 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl12_183])],[avatar_definition]) ).
fof(f1487,plain,
( e20 = h1(e13)
| ~ spl12_183 ),
inference(avatar_component_clause,[],[f1485]) ).
fof(f1488,plain,
( spl12_183
| spl12_178
| spl12_174
| spl12_170 ),
inference(avatar_split_clause,[],[f1453,f1337,f1357,f1377,f1485]) ).
fof(f1504,plain,
( h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(e10) != h3(op1(e11,e12))
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,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,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1465,f455]) ).
fof(f1520,plain,
( op2(e22,e22) != h3(op1(e12,e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(e10) != h3(op1(e11,e12))
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,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,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1504,f455]) ).
fof(f1536,plain,
( h3(e13) != h3(op1(e12,e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(e10) != h3(op1(e11,e12))
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,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,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1520,f452]) ).
fof(f1552,plain,
( h3(op1(e12,e13)) != op2(e22,h3(e13))
| h3(e13) != h3(op1(e12,e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(e10) != h3(op1(e11,e12))
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,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,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1536,f455]) ).
fof(f1568,plain,
( h3(e11) != h3(op1(e12,e13))
| h3(e13) != h3(op1(e12,e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(e10) != h3(op1(e11,e12))
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,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,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1552,f549]) ).
fof(f1584,plain,
( h3(op1(e13,e12)) != op2(h3(e13),e22)
| h3(e11) != h3(op1(e12,e13))
| h3(e13) != h3(op1(e12,e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(e10) != h3(op1(e11,e12))
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,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,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1568,f455]) ).
fof(f1600,plain,
( h3(e11) != h3(op1(e13,e12))
| h3(e11) != h3(op1(e12,e13))
| h3(e13) != h3(op1(e12,e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(e10) != h3(op1(e11,e12))
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,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,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| e20 != h3(e10)
| sP5
| sP4
| sP3 ),
inference(forward_demodulation,[],[f1584,f1400]) ).
fof(f1686,definition,
( spl12_203
<=> h3(op1(e13,e13)) = op2(h3(e13),h3(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_203])],[avatar_definition]) ).
fof(f1688,plain,
( h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| spl12_203 ),
inference(avatar_component_clause,[],[f1686]) ).
fof(f1690,definition,
( spl12_204
<=> h3(op1(e13,e11)) = op2(h3(e13),h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_204])],[avatar_definition]) ).
fof(f1692,plain,
( h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| spl12_204 ),
inference(avatar_component_clause,[],[f1690]) ).
fof(f1694,definition,
( spl12_205
<=> h3(op1(e13,e10)) = op2(h3(e13),h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_205])],[avatar_definition]) ).
fof(f1696,plain,
( h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| spl12_205 ),
inference(avatar_component_clause,[],[f1694]) ).
fof(f1698,definition,
( spl12_206
<=> h3(op1(e11,e13)) = op2(h3(e11),h3(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_206])],[avatar_definition]) ).
fof(f1700,plain,
( h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| spl12_206 ),
inference(avatar_component_clause,[],[f1698]) ).
fof(f1702,definition,
( spl12_207
<=> h3(op1(e11,e11)) = op2(h3(e11),h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_207])],[avatar_definition]) ).
fof(f1704,plain,
( h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| spl12_207 ),
inference(avatar_component_clause,[],[f1702]) ).
fof(f1706,definition,
( spl12_208
<=> h3(op1(e11,e10)) = op2(h3(e11),h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_208])],[avatar_definition]) ).
fof(f1708,plain,
( h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| spl12_208 ),
inference(avatar_component_clause,[],[f1706]) ).
fof(f1710,definition,
( spl12_209
<=> h3(op1(e10,e13)) = op2(h3(e10),h3(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_209])],[avatar_definition]) ).
fof(f1712,plain,
( h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| spl12_209 ),
inference(avatar_component_clause,[],[f1710]) ).
fof(f1714,definition,
( spl12_210
<=> h3(op1(e10,e11)) = op2(h3(e10),h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_210])],[avatar_definition]) ).
fof(f1716,plain,
( h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| spl12_210 ),
inference(avatar_component_clause,[],[f1714]) ).
fof(f1718,definition,
( spl12_211
<=> h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_211])],[avatar_definition]) ).
fof(f1720,plain,
( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| spl12_211 ),
inference(avatar_component_clause,[],[f1718]) ).
fof(f1722,definition,
( spl12_212
<=> h3(op1(e10,e12)) = op2(h3(e10),e22) ),
introduced(definition,[new_symbols(definition,[spl12_212])],[avatar_definition]) ).
fof(f1724,plain,
( h3(op1(e10,e12)) != op2(h3(e10),e22)
| spl12_212 ),
inference(avatar_component_clause,[],[f1722]) ).
fof(f1726,definition,
( spl12_213
<=> h3(e10) = h3(op1(e11,e12)) ),
introduced(definition,[new_symbols(definition,[spl12_213])],[avatar_definition]) ).
fof(f1728,plain,
( h3(e10) != h3(op1(e11,e12))
| spl12_213 ),
inference(avatar_component_clause,[],[f1726]) ).
fof(f1730,definition,
( spl12_214
<=> h3(op1(e12,e10)) = op2(e22,h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_214])],[avatar_definition]) ).
fof(f1732,plain,
( h3(op1(e12,e10)) != op2(e22,h3(e10))
| spl12_214 ),
inference(avatar_component_clause,[],[f1730]) ).
fof(f1734,definition,
( spl12_215
<=> h3(op1(e12,e11)) = op2(e22,h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_215])],[avatar_definition]) ).
fof(f1736,plain,
( h3(op1(e12,e11)) != op2(e22,h3(e11))
| spl12_215 ),
inference(avatar_component_clause,[],[f1734]) ).
fof(f1738,definition,
( spl12_216
<=> h3(e13) = h3(op1(e12,e12)) ),
introduced(definition,[new_symbols(definition,[spl12_216])],[avatar_definition]) ).
fof(f1740,plain,
( h3(e13) != h3(op1(e12,e12))
| spl12_216 ),
inference(avatar_component_clause,[],[f1738]) ).
fof(f1742,definition,
( spl12_217
<=> h3(e11) = h3(op1(e12,e13)) ),
introduced(definition,[new_symbols(definition,[spl12_217])],[avatar_definition]) ).
fof(f1744,plain,
( h3(e11) != h3(op1(e12,e13))
| spl12_217 ),
inference(avatar_component_clause,[],[f1742]) ).
fof(f1746,definition,
( spl12_218
<=> h3(e11) = h3(op1(e13,e12)) ),
introduced(definition,[new_symbols(definition,[spl12_218])],[avatar_definition]) ).
fof(f1748,plain,
( h3(e11) != h3(op1(e13,e12))
| spl12_218 ),
inference(avatar_component_clause,[],[f1746]) ).
fof(f1757,definition,
( spl12_220
<=> e20 = h3(e10) ),
introduced(definition,[new_symbols(definition,[spl12_220])],[avatar_definition]) ).
fof(f1758,plain,
( e20 = h3(e10)
| ~ spl12_220 ),
inference(avatar_component_clause,[],[f1757]) ).
fof(f1759,plain,
( e20 != h3(e10)
| spl12_220 ),
inference(avatar_component_clause,[],[f1757]) ).
fof(f1760,plain,
( spl12_145
| spl12_149
| spl12_153
| ~ spl12_220
| ~ spl12_203
| ~ spl12_204
| ~ spl12_205
| ~ spl12_206
| ~ spl12_207
| ~ spl12_208
| ~ spl12_209
| ~ spl12_210
| ~ spl12_211
| ~ spl12_212
| ~ spl12_213
| ~ spl12_214
| ~ spl12_215
| ~ spl12_216
| ~ spl12_217
| ~ spl12_218 ),
inference(avatar_split_clause,[],[f1600,f1746,f1742,f1738,f1734,f1730,f1726,f1722,f1718,f1714,f1710,f1706,f1702,f1698,f1694,f1690,f1686,f1757,f1253,f1233,f1213]) ).
fof(f1964,plain,
( e10 = inv1(e10)
| ~ spl12_128 ),
inference(superposition,[],[f460,f1108]) ).
fof(f1965,plain,
( spl12_132
| ~ spl12_128 ),
inference(avatar_split_clause,[],[f1964,f1106,f1126]) ).
fof(f1984,plain,
( e11 = op1(e11,e12)
| ~ spl12_126 ),
inference(superposition,[],[f203,f1100]) ).
fof(f1985,plain,
( e10 = e11
| ~ spl12_100
| ~ spl12_126 ),
inference(forward_demodulation,[],[f1984,f989]) ).
fof(f1986,plain,
( $false
| ~ spl12_100
| ~ spl12_126 ),
inference(forward_subsumption_resolution,[],[f1985,f130]) ).
fof(f1987,plain,
( ~ spl12_100
| ~ spl12_126 ),
inference(avatar_contradiction_clause,[],[f1986]) ).
fof(f1990,plain,
( e12 = op1(e12,e10)
| ~ spl12_128 ),
inference(superposition,[],[f201,f1108]) ).
fof(f1991,plain,
( e12 = op1(e10,e12)
| ~ spl12_128 ),
inference(superposition,[],[f202,f1108]) ).
fof(f1992,plain,
( e11 = op1(e11,e10)
| ~ spl12_128 ),
inference(superposition,[],[f203,f1108]) ).
fof(f1997,plain,
( spl12_107
| ~ spl12_128 ),
inference(avatar_split_clause,[],[f1992,f1106,f1017]) ).
fof(f1998,plain,
( spl12_114
| ~ spl12_128 ),
inference(avatar_split_clause,[],[f1991,f1106,f1047]) ).
fof(f1999,plain,
( spl12_90
| ~ spl12_128 ),
inference(avatar_split_clause,[],[f1990,f1106,f945]) ).
fof(f2000,plain,
( e10 = e13
| ~ spl12_6
| ~ spl12_132 ),
inference(superposition,[],[f1128,f512]) ).
fof(f2004,plain,
( $false
| ~ spl12_6
| ~ spl12_132 ),
inference(forward_subsumption_resolution,[],[f2000,f128]) ).
fof(f2005,plain,
( ~ spl12_6
| ~ spl12_132 ),
inference(avatar_contradiction_clause,[],[f2004]) ).
fof(f2012,plain,
( e11 = op1(e10,e11)
| ~ spl12_128 ),
inference(superposition,[],[f204,f1108]) ).
fof(f2013,plain,
( spl12_119
| ~ spl12_128 ),
inference(avatar_split_clause,[],[f2012,f1106,f1068]) ).
fof(f2014,plain,
( e10 = op1(e10,e10)
| ~ spl12_128 ),
inference(superposition,[],[f205,f1108]) ).
fof(f2015,plain,
( spl12_124
| ~ spl12_128 ),
inference(avatar_split_clause,[],[f2014,f1106,f1089]) ).
fof(f2074,plain,
( op1(e13,e13) = unit1
| ~ spl12_129 ),
inference(superposition,[],[f190,f1113]) ).
fof(f2075,plain,
( e10 = op1(e13,e13)
| ~ spl12_128
| ~ spl12_129 ),
inference(forward_demodulation,[],[f2074,f1108]) ).
fof(f2076,plain,
( spl12_64
| ~ spl12_128
| ~ spl12_129 ),
inference(avatar_split_clause,[],[f2075,f1111,f1106,f834]) ).
fof(f2098,plain,
( op1(e12,e12) = unit1
| ~ spl12_130 ),
inference(superposition,[],[f192,f1118]) ).
fof(f2099,plain,
( e10 = op1(e12,e12)
| ~ spl12_128
| ~ spl12_130 ),
inference(forward_demodulation,[],[f2098,f1108]) ).
fof(f2100,plain,
( spl12_84
| ~ spl12_128
| ~ spl12_130 ),
inference(avatar_split_clause,[],[f2099,f1116,f1106,f919]) ).
fof(f2102,plain,
( e10 = e13
| ~ spl12_81
| ~ spl12_84 ),
inference(superposition,[],[f921,f909]) ).
fof(f2106,plain,
( $false
| ~ spl12_81
| ~ spl12_84 ),
inference(forward_subsumption_resolution,[],[f2102,f128]) ).
fof(f2107,plain,
( ~ spl12_81
| ~ spl12_84 ),
inference(avatar_contradiction_clause,[],[f2106]) ).
fof(f2114,plain,
( e10 = e12
| ~ spl12_10
| ~ spl12_132 ),
inference(forward_demodulation,[],[f531,f1128]) ).
fof(f2116,plain,
( $false
| ~ spl12_10
| ~ spl12_132 ),
inference(forward_subsumption_resolution,[],[f2114,f129]) ).
fof(f2117,plain,
( ~ spl12_10
| ~ spl12_132 ),
inference(avatar_contradiction_clause,[],[f2116]) ).
fof(f2122,plain,
( op1(e12,e13) = unit1
| ~ spl12_1 ),
inference(superposition,[],[f190,f489]) ).
fof(f2133,plain,
( e10 = op1(e12,e13)
| ~ spl12_1
| ~ spl12_128 ),
inference(forward_demodulation,[],[f2122,f1108]) ).
fof(f2135,plain,
( spl12_80
| ~ spl12_1
| ~ spl12_128 ),
inference(avatar_split_clause,[],[f2133,f1106,f488,f902]) ).
fof(f2177,plain,
e23 = h3(e13),
inference(superposition,[],[f309,f452]) ).
fof(f2178,plain,
spl12_146,
inference(avatar_split_clause,[],[f2177,f1217]) ).
fof(f2189,plain,
( e23 != h3(e13)
| ~ spl12_29 ),
inference(superposition,[],[f795,f628]) ).
fof(f2190,plain,
( $false
| ~ spl12_29
| ~ spl12_146 ),
inference(forward_subsumption_resolution,[],[f2189,f1218]) ).
fof(f2191,plain,
( ~ spl12_29
| ~ spl12_146 ),
inference(avatar_contradiction_clause,[],[f2190]) ).
fof(f2195,plain,
( e23 != h3(e13)
| ~ spl12_33 ),
inference(superposition,[],[f796,f645]) ).
fof(f2196,plain,
( $false
| ~ spl12_33
| ~ spl12_146 ),
inference(forward_subsumption_resolution,[],[f2195,f1218]) ).
fof(f2197,plain,
( ~ spl12_33
| ~ spl12_146 ),
inference(avatar_contradiction_clause,[],[f2196]) ).
fof(f2222,plain,
( e23 != h1(e13)
| ~ spl12_49 ),
inference(superposition,[],[f800,f714]) ).
fof(f2232,plain,
( e22 != h1(e13)
| ~ spl12_54 ),
inference(superposition,[],[f801,f735]) ).
fof(f2290,plain,
( e23 != h1(e13)
| ~ spl12_21 ),
inference(superposition,[],[f812,f593]) ).
fof(f2294,plain,
( e21 = op2(e22,e23)
| ~ spl12_146 ),
inference(superposition,[],[f819,f1218]) ).
fof(f2300,plain,
( e21 != h4(e13)
| ~ spl12_27 ),
inference(superposition,[],[f803,f618]) ).
fof(f2304,plain,
( e11 = op1(e12,e13)
| ~ spl12_81 ),
inference(superposition,[],[f132,f909]) ).
fof(f2305,plain,
( e10 = e11
| ~ spl12_80
| ~ spl12_81 ),
inference(forward_demodulation,[],[f2304,f904]) ).
fof(f2306,plain,
( $false
| ~ spl12_80
| ~ spl12_81 ),
inference(forward_subsumption_resolution,[],[f2305,f130]) ).
fof(f2307,plain,
( ~ spl12_80
| ~ spl12_81 ),
inference(avatar_contradiction_clause,[],[f2306]) ).
fof(f2317,plain,
( spl12_79
| ~ spl12_81 ),
inference(avatar_split_clause,[],[f2304,f907,f898]) ).
fof(f2337,plain,
( e11 = op1(e11,e13)
| ~ spl12_125 ),
inference(superposition,[],[f203,f1096]) ).
fof(f2347,plain,
( spl12_95
| ~ spl12_125 ),
inference(avatar_split_clause,[],[f2337,f1094,f966]) ).
fof(f2418,plain,
( e12 = op1(e11,e12)
| ~ spl12_127 ),
inference(superposition,[],[f202,f1104]) ).
fof(f2428,plain,
( e10 = e12
| ~ spl12_100
| ~ spl12_127 ),
inference(forward_demodulation,[],[f2418,f989]) ).
fof(f2430,plain,
( $false
| ~ spl12_100
| ~ spl12_127 ),
inference(forward_subsumption_resolution,[],[f2428,f129]) ).
fof(f2431,plain,
( ~ spl12_100
| ~ spl12_127 ),
inference(avatar_contradiction_clause,[],[f2430]) ).
fof(f2452,plain,
( e13 = op1(e13,e10)
| ~ spl12_128 ),
inference(superposition,[],[f199,f1108]) ).
fof(f2453,plain,
( e13 = op1(e10,e13)
| ~ spl12_128 ),
inference(superposition,[],[f200,f1108]) ).
fof(f2465,plain,
( op1(e12,e11) = unit1
| ~ spl12_7 ),
inference(superposition,[],[f193,f517]) ).
fof(f2468,plain,
( e12 = inv1(e11)
| ~ spl12_7 ),
inference(superposition,[],[f484,f517]) ).
fof(f2471,plain,
( e10 = op1(e12,e11)
| ~ spl12_7
| ~ spl12_128 ),
inference(forward_demodulation,[],[f2465,f1108]) ).
fof(f2473,plain,
( spl12_88
| ~ spl12_7
| ~ spl12_128 ),
inference(avatar_split_clause,[],[f2471,f1106,f516,f936]) ).
fof(f2580,plain,
( e10 != op1(e13,e12)
| ~ spl12_64 ),
inference(superposition,[],[f138,f836]) ).
fof(f2582,plain,
( e10 != op1(e13,e11)
| ~ spl12_64 ),
inference(superposition,[],[f139,f836]) ).
fof(f2608,plain,
( e10 != op1(e11,e11)
| ~ spl12_100 ),
inference(superposition,[],[f152,f989]) ).
fof(f2609,plain,
( $false
| ~ spl12_100
| ~ spl12_104 ),
inference(forward_subsumption_resolution,[],[f2608,f1006]) ).
fof(f2610,plain,
( ~ spl12_100
| ~ spl12_104 ),
inference(avatar_contradiction_clause,[],[f2609]) ).
fof(f2622,plain,
( e12 != op1(e11,e11)
| ~ spl12_94 ),
inference(superposition,[],[f151,f964]) ).
fof(f2654,plain,
( e10 != op1(e11,e13)
| ~ spl12_64 ),
inference(superposition,[],[f163,f836]) ).
fof(f2656,plain,
( e11 != op1(e11,e13)
| ~ spl12_79 ),
inference(superposition,[],[f164,f900]) ).
fof(f2662,plain,
( e13 != op1(e10,e13)
| ~ spl12_93 ),
inference(superposition,[],[f167,f960]) ).
fof(f2663,plain,
( $false
| ~ spl12_93
| ~ spl12_109 ),
inference(forward_subsumption_resolution,[],[f2662,f1028]) ).
fof(f2664,plain,
( ~ spl12_93
| ~ spl12_109 ),
inference(avatar_contradiction_clause,[],[f2663]) ).
fof(f2667,plain,
( $false
| spl12_109
| ~ spl12_128 ),
inference(forward_subsumption_resolution,[],[f2453,f1027]) ).
fof(f2668,plain,
( spl12_109
| ~ spl12_128 ),
inference(avatar_contradiction_clause,[],[f2667]) ).
fof(f2687,plain,
( ~ spl12_102
| ~ spl12_94 ),
inference(avatar_split_clause,[],[f2622,f962,f996]) ).
fof(f2704,plain,
( e11 != op1(e11,e10)
| ~ spl12_103 ),
inference(superposition,[],[f155,f1002]) ).
fof(f2705,plain,
( $false
| ~ spl12_103
| ~ spl12_107 ),
inference(forward_subsumption_resolution,[],[f2704,f1019]) ).
fof(f2706,plain,
( ~ spl12_103
| ~ spl12_107 ),
inference(avatar_contradiction_clause,[],[f2705]) ).
fof(f2707,plain,
( e12 = e13
| ~ spl12_4
| ~ spl12_8 ),
inference(forward_demodulation,[],[f503,f522]) ).
fof(f2721,plain,
( $false
| ~ spl12_4
| ~ spl12_8 ),
inference(forward_subsumption_resolution,[],[f2707,f125]) ).
fof(f2722,plain,
( ~ spl12_4
| ~ spl12_8 ),
inference(avatar_contradiction_clause,[],[f2721]) ).
fof(f2735,plain,
( ~ spl12_96
| ~ spl12_64 ),
inference(avatar_split_clause,[],[f2654,f834,f970]) ).
fof(f2788,plain,
( e23 != h3(e13)
| ~ spl12_53 ),
inference(superposition,[],[f808,f731]) ).
fof(f2790,plain,
( $false
| ~ spl12_53
| ~ spl12_146 ),
inference(forward_subsumption_resolution,[],[f2788,f1218]) ).
fof(f2791,plain,
( ~ spl12_53
| ~ spl12_146 ),
inference(avatar_contradiction_clause,[],[f2790]) ).
fof(f2863,plain,
( e12 != op1(e10,e12)
| ~ spl12_66 ),
inference(superposition,[],[f171,f845]) ).
fof(f2876,plain,
( e13 != op1(e12,e12)
| ~ spl12_65 ),
inference(superposition,[],[f168,f841]) ).
fof(f2882,plain,
( $false
| ~ spl12_65
| ~ spl12_81 ),
inference(forward_subsumption_resolution,[],[f2876,f909]) ).
fof(f2883,plain,
( ~ spl12_65
| ~ spl12_81 ),
inference(avatar_contradiction_clause,[],[f2882]) ).
fof(f2888,plain,
( h3(e11) != h3(e11)
| ~ spl12_67
| spl12_218 ),
inference(forward_demodulation,[],[f1748,f849]) ).
fof(f2889,plain,
( $false
| ~ spl12_67
| spl12_218 ),
inference(trivial_inequality_removal,[],[f2888]) ).
fof(f2890,plain,
( ~ spl12_67
| spl12_218 ),
inference(avatar_contradiction_clause,[],[f2889]) ).
fof(f2893,plain,
( op2(e23,e23) != h3(op1(e13,e13))
| ~ spl12_146
| spl12_203 ),
inference(forward_demodulation,[],[f1688,f1218]) ).
fof(f2894,plain,
( op2(e23,e23) != h3(e10)
| ~ spl12_64
| ~ spl12_146
| spl12_203 ),
inference(forward_demodulation,[],[f2893,f836]) ).
fof(f2895,plain,
( h3(e10) != h4(e13)
| ~ spl12_64
| ~ spl12_146
| spl12_203 ),
inference(forward_demodulation,[],[f2894,f456]) ).
fof(f2898,plain,
( e11 != op1(e13,e11)
| ~ spl12_67 ),
inference(superposition,[],[f140,f849]) ).
fof(f2949,plain,
( e23 != op2(e23,e20)
| ~ spl12_17 ),
inference(superposition,[],[f321,f576]) ).
fof(f2963,plain,
( e21 != op2(e22,e20)
| ~ spl12_27 ),
inference(superposition,[],[f325,f618]) ).
fof(f2980,plain,
( spl12_27
| ~ spl12_146 ),
inference(avatar_split_clause,[],[f2294,f1217,f616]) ).
fof(f2988,plain,
( ~ spl12_35
| ~ spl12_27 ),
inference(avatar_split_clause,[],[f2963,f616,f651]) ).
fof(f3009,plain,
( e20 != h3(e10)
| ~ spl12_64
| ~ spl12_146
| ~ spl12_181
| spl12_203 ),
inference(forward_demodulation,[],[f2895,f1477]) ).
fof(f3014,plain,
( ~ spl12_220
| ~ spl12_64
| ~ spl12_146
| ~ spl12_181
| spl12_203 ),
inference(avatar_split_clause,[],[f3009,f1686,f1475,f1217,f834,f1757]) ).
fof(f3031,plain,
( $false
| ~ spl12_27
| ~ spl12_142 ),
inference(forward_subsumption_resolution,[],[f2300,f1198]) ).
fof(f3032,plain,
( ~ spl12_27
| ~ spl12_142 ),
inference(avatar_contradiction_clause,[],[f3031]) ).
fof(f3145,plain,
( e21 != op2(e23,e21)
| ~ spl12_15 ),
inference(superposition,[],[f318,f567]) ).
fof(f3146,plain,
( e21 != op2(e23,e20)
| ~ spl12_15 ),
inference(superposition,[],[f320,f567]) ).
fof(f3154,plain,
( e22 != op2(e23,e20)
| ~ spl12_18 ),
inference(superposition,[],[f321,f580]) ).
fof(f3155,plain,
( e22 != h2(e13)
| ~ spl12_18 ),
inference(superposition,[],[f809,f580]) ).
fof(f3156,plain,
( e22 != h4(e13)
| ~ spl12_18 ),
inference(superposition,[],[f792,f580]) ).
fof(f3158,plain,
( $false
| ~ spl12_18
| ~ spl12_162 ),
inference(forward_subsumption_resolution,[],[f3155,f1298]) ).
fof(f3159,plain,
( ~ spl12_18
| ~ spl12_162 ),
inference(avatar_contradiction_clause,[],[f3158]) ).
fof(f3175,plain,
( ~ spl12_19
| ~ spl12_15 ),
inference(avatar_split_clause,[],[f3145,f565,f582]) ).
fof(f3188,plain,
( e23 != h2(e13)
| ~ spl12_17 ),
inference(superposition,[],[f809,f576]) ).
fof(f3193,plain,
( e22 != h4(e13)
| ~ spl12_22 ),
inference(superposition,[],[f793,f597]) ).
fof(f3204,plain,
( e21 != op2(e22,e21)
| ~ spl12_27 ),
inference(superposition,[],[f323,f618]) ).
fof(f3219,plain,
( e20 != h1(e13)
| ~ spl12_36 ),
inference(superposition,[],[f813,f657]) ).
fof(f3244,plain,
( e20 != op2(e22,e20)
| ~ spl12_32 ),
inference(superposition,[],[f327,f640]) ).
fof(f3250,plain,
( $false
| ~ spl12_27
| ~ spl12_31 ),
inference(forward_subsumption_resolution,[],[f3204,f636]) ).
fof(f3251,plain,
( ~ spl12_27
| ~ spl12_31 ),
inference(avatar_contradiction_clause,[],[f3250]) ).
fof(f3256,plain,
( e22 != op2(e22,e20)
| ~ spl12_30 ),
inference(superposition,[],[f327,f632]) ).
fof(f3257,plain,
( e22 != h2(e13)
| ~ spl12_30 ),
inference(superposition,[],[f810,f632]) ).
fof(f3276,plain,
( $false
| ~ spl12_17
| ~ spl12_158 ),
inference(forward_subsumption_resolution,[],[f3188,f1278]) ).
fof(f3277,plain,
( ~ spl12_17
| ~ spl12_158 ),
inference(avatar_contradiction_clause,[],[f3276]) ).
fof(f3295,plain,
( e20 != op2(e23,e20)
| ~ spl12_20 ),
inference(superposition,[],[f321,f588]) ).
fof(f3297,plain,
( e20 != h4(e13)
| ~ spl12_20 ),
inference(superposition,[],[f792,f588]) ).
fof(f3303,plain,
( ~ spl12_22
| ~ spl12_18 ),
inference(avatar_split_clause,[],[f3154,f578,f595]) ).
fof(f3320,plain,
( e20 != h4(e13)
| ~ spl12_24 ),
inference(superposition,[],[f793,f605]) ).
fof(f3410,plain,
( e20 != h2(e13)
| ~ spl12_44 ),
inference(superposition,[],[f798,f691]) ).
fof(f3415,plain,
( e20 != op2(e21,e20)
| ~ spl12_44 ),
inference(superposition,[],[f332,f691]) ).
fof(f3417,plain,
( e22 != op2(e20,e22)
| ~ spl12_50 ),
inference(superposition,[],[f334,f718]) ).
fof(f3424,plain,
( e21 != h2(e13)
| ~ spl12_59 ),
inference(superposition,[],[f811,f756]) ).
fof(f3425,plain,
( e21 != h1(e13)
| ~ spl12_59 ),
inference(superposition,[],[f802,f756]) ).
fof(f3436,plain,
( e23 != op2(e20,e21)
| ~ spl12_49 ),
inference(superposition,[],[f335,f714]) ).
fof(f3447,plain,
( e21 != op2(e21,e23)
| ~ spl12_27 ),
inference(superposition,[],[f342,f618]) ).
fof(f3448,plain,
( $false
| ~ spl12_27
| ~ spl12_39 ),
inference(forward_subsumption_resolution,[],[f3447,f670]) ).
fof(f3449,plain,
( ~ spl12_27
| ~ spl12_39 ),
inference(avatar_contradiction_clause,[],[f3448]) ).
fof(f3457,plain,
( e22 != h4(e13)
| ~ spl12_38 ),
inference(superposition,[],[f804,f666]) ).
fof(f3464,plain,
( e20 != op2(e21,e22)
| ~ spl12_40 ),
inference(superposition,[],[f328,f674]) ).
fof(f3474,plain,
( $false
| ~ spl12_40
| ~ spl12_44 ),
inference(forward_subsumption_resolution,[],[f3464,f691]) ).
fof(f3475,plain,
( ~ spl12_40
| ~ spl12_44 ),
inference(avatar_contradiction_clause,[],[f3474]) ).
fof(f3507,plain,
( e21 != op2(e20,e23)
| ~ spl12_27 ),
inference(superposition,[],[f344,f618]) ).
fof(f3509,plain,
( e23 != op2(e20,e23)
| ~ spl12_37 ),
inference(superposition,[],[f345,f662]) ).
fof(f3536,plain,
( e21 != op2(e20,e22)
| ~ spl12_15 ),
inference(superposition,[],[f349,f567]) ).
fof(f3537,plain,
( e20 != op2(e20,e22)
| ~ spl12_44 ),
inference(superposition,[],[f351,f691]) ).
fof(f3543,plain,
( e22 != op2(e20,e21)
| ~ spl12_54 ),
inference(superposition,[],[f336,f735]) ).
fof(f3558,plain,
( e22 != op2(e22,e21)
| ~ spl12_18 ),
inference(superposition,[],[f352,f580]) ).
fof(f3562,plain,
( ~ spl12_36
| ~ spl12_32 ),
inference(avatar_split_clause,[],[f3244,f638,f655]) ).
fof(f3583,plain,
( e20 != op2(e20,e21)
| ~ spl12_32 ),
inference(superposition,[],[f356,f640]) ).
fof(f3602,plain,
( e20 != op2(e20,e21)
| ~ spl12_52 ),
inference(superposition,[],[f335,f726]) ).
fof(f3606,plain,
( e20 != h4(e13)
| ~ spl12_52 ),
inference(superposition,[],[f805,f726]) ).
fof(f3628,plain,
( $false
| ~ spl12_27
| ~ spl12_51 ),
inference(forward_subsumption_resolution,[],[f3507,f722]) ).
fof(f3629,plain,
( ~ spl12_27
| ~ spl12_51 ),
inference(avatar_contradiction_clause,[],[f3628]) ).
fof(f3640,plain,
( ~ spl12_57
| ~ spl12_49 ),
inference(avatar_split_clause,[],[f3436,f712,f746]) ).
fof(f3689,plain,
( ~ spl12_21
| ~ spl12_17 ),
inference(avatar_split_clause,[],[f2949,f574,f591]) ).
fof(f3835,plain,
( ~ spl12_60
| ~ spl12_32 ),
inference(avatar_split_clause,[],[f3583,f638,f758]) ).
fof(f3840,plain,
( ~ spl12_49
| ~ spl12_37 ),
inference(avatar_split_clause,[],[f3509,f660,f712]) ).
fof(f3891,plain,
( ~ spl12_162
| ~ spl12_30 ),
inference(avatar_split_clause,[],[f3257,f630,f1297]) ).
fof(f3892,plain,
( ~ spl12_34
| ~ spl12_30 ),
inference(avatar_split_clause,[],[f3256,f630,f647]) ).
fof(f3974,plain,
( e23 != op2(e21,e20)
| ~ spl12_21 ),
inference(superposition,[],[f359,f593]) ).
fof(f3977,plain,
( op2(e23,e20) = h4(e11)
| ~ spl12_181 ),
inference(superposition,[],[f547,f1477]) ).
fof(f3983,plain,
e21 = h3(e11),
inference(superposition,[],[f819,f549]) ).
fof(f3984,plain,
spl12_155,
inference(avatar_split_clause,[],[f3983,f1263]) ).
fof(f3989,plain,
( e20 = op2(e21,e22)
| ~ spl12_155 ),
inference(superposition,[],[f1407,f1264]) ).
fof(f3990,plain,
( spl12_44
| ~ spl12_155 ),
inference(avatar_split_clause,[],[f3989,f1263,f689]) ).
fof(f3991,plain,
( ~ spl12_56
| ~ spl12_44 ),
inference(avatar_split_clause,[],[f3537,f689,f741]) ).
fof(f3994,plain,
( $false
| ~ spl12_44
| ~ spl12_182 ),
inference(forward_subsumption_resolution,[],[f3410,f1482]) ).
fof(f3995,plain,
( ~ spl12_44
| ~ spl12_182 ),
inference(avatar_contradiction_clause,[],[f3994]) ).
fof(f3998,plain,
( ~ spl12_178
| ~ spl12_59 ),
inference(avatar_split_clause,[],[f3425,f754,f1377]) ).
fof(f4057,plain,
( e23 = op2(e23,e20)
| ~ spl12_135
| ~ spl12_181 ),
inference(forward_demodulation,[],[f3977,f1164]) ).
fof(f4063,plain,
( $false
| spl12_21
| ~ spl12_135
| ~ spl12_181 ),
inference(forward_subsumption_resolution,[],[f4057,f592]) ).
fof(f4064,plain,
( spl12_21
| ~ spl12_135
| ~ spl12_181 ),
inference(avatar_contradiction_clause,[],[f4063]) ).
fof(f4108,plain,
( e23 != op2(e20,e21)
| ~ spl12_17 ),
inference(superposition,[],[f355,f576]) ).
fof(f4120,plain,
( ~ spl12_23
| ~ spl12_15 ),
inference(avatar_split_clause,[],[f3146,f565,f599]) ).
fof(f4142,plain,
( $false
| ~ spl12_44
| ~ spl12_48 ),
inference(forward_subsumption_resolution,[],[f3415,f709]) ).
fof(f4143,plain,
( ~ spl12_44
| ~ spl12_48 ),
inference(avatar_contradiction_clause,[],[f4142]) ).
fof(f4254,plain,
e20 = h3(e10),
inference(superposition,[],[f1393,f1407]) ).
fof(f4258,plain,
( $false
| spl12_220 ),
inference(forward_subsumption_resolution,[],[f4254,f1759]) ).
fof(f4259,plain,
spl12_220,
inference(avatar_contradiction_clause,[],[f4258]) ).
fof(f4264,plain,
( h3(op1(e13,e11)) != op2(h3(e13),e21)
| ~ spl12_155
| spl12_204 ),
inference(forward_demodulation,[],[f1692,f1264]) ).
fof(f4266,plain,
( op2(e23,e21) != h3(op1(e13,e11))
| ~ spl12_146
| ~ spl12_155
| spl12_204 ),
inference(forward_demodulation,[],[f4264,f1218]) ).
fof(f4268,plain,
( op2(e23,e21) != h3(e12)
| ~ spl12_70
| ~ spl12_146
| ~ spl12_155
| spl12_204 ),
inference(forward_demodulation,[],[f4266,f862]) ).
fof(f4269,plain,
( e22 != op2(e23,e21)
| ~ spl12_70
| ~ spl12_146
| ~ spl12_155
| spl12_204 ),
inference(forward_demodulation,[],[f4268,f455]) ).
fof(f4312,plain,
( op2(e20,e23) = h4(e11)
| ~ spl12_181 ),
inference(superposition,[],[f1399,f1477]) ).
fof(f4319,plain,
( ~ spl12_170
| ~ spl12_21 ),
inference(avatar_split_clause,[],[f2290,f591,f1337]) ).
fof(f4321,plain,
( ~ spl12_45
| ~ spl12_21 ),
inference(avatar_split_clause,[],[f3974,f591,f695]) ).
fof(f4328,plain,
( ~ spl12_170
| ~ spl12_49 ),
inference(avatar_split_clause,[],[f2222,f712,f1337]) ).
fof(f4330,plain,
( ~ spl12_174
| ~ spl12_54 ),
inference(avatar_split_clause,[],[f2232,f733,f1357]) ).
fof(f4395,plain,
( e23 = h4(e11)
| ~ spl12_49
| ~ spl12_181 ),
inference(forward_demodulation,[],[f4312,f714]) ).
fof(f4404,plain,
( $false
| ~ spl12_49
| spl12_135
| ~ spl12_181 ),
inference(forward_subsumption_resolution,[],[f4395,f1165]) ).
fof(f4405,plain,
( ~ spl12_49
| spl12_135
| ~ spl12_181 ),
inference(avatar_contradiction_clause,[],[f4404]) ).
fof(f4407,plain,
( ~ spl12_181
| ~ spl12_24 ),
inference(avatar_split_clause,[],[f3320,f603,f1475]) ).
fof(f4495,plain,
( ~ spl12_30
| ~ spl12_18 ),
inference(avatar_split_clause,[],[f3558,f578,f630]) ).
fof(f4512,plain,
( $false
| ~ spl12_18
| ~ spl12_70
| ~ spl12_146
| ~ spl12_155
| spl12_204 ),
inference(forward_subsumption_resolution,[],[f4269,f580]) ).
fof(f4513,plain,
( ~ spl12_18
| ~ spl12_70
| ~ spl12_146
| ~ spl12_155
| spl12_204 ),
inference(avatar_contradiction_clause,[],[f4512]) ).
fof(f4514,plain,
( ~ spl12_24
| ~ spl12_20 ),
inference(avatar_split_clause,[],[f3295,f586,f603]) ).
fof(f4590,plain,
( op2(e20,e21) = h1(e11)
| ~ spl12_178 ),
inference(superposition,[],[f553,f1378]) ).
fof(f4591,plain,
( e23 = h1(e11)
| ~ spl12_57
| ~ spl12_178 ),
inference(forward_demodulation,[],[f4590,f748]) ).
fof(f4592,plain,
( spl12_171
| ~ spl12_57
| ~ spl12_178 ),
inference(avatar_split_clause,[],[f4591,f1377,f746,f1343]) ).
fof(f4617,plain,
( e20 != op2(e22,e21)
| ~ spl12_20 ),
inference(superposition,[],[f352,f588]) ).
fof(f4618,plain,
( e20 != op2(e20,e21)
| ~ spl12_20 ),
inference(superposition,[],[f355,f588]) ).
fof(f4714,plain,
( op2(e23,e22) = h3(e11)
| ~ spl12_146 ),
inference(superposition,[],[f1400,f1218]) ).
fof(f4715,plain,
( e21 = op2(e23,e22)
| ~ spl12_146
| ~ spl12_155 ),
inference(forward_demodulation,[],[f4714,f1264]) ).
fof(f4717,plain,
( op2(e21,e20) = h1(e11)
| ~ spl12_178 ),
inference(superposition,[],[f1402,f1378]) ).
fof(f4718,plain,
( e23 = op2(e21,e20)
| ~ spl12_171
| ~ spl12_178 ),
inference(forward_demodulation,[],[f4717,f1344]) ).
fof(f4719,plain,
( $false
| spl12_45
| ~ spl12_171
| ~ spl12_178 ),
inference(forward_subsumption_resolution,[],[f4718,f696]) ).
fof(f4720,plain,
( spl12_45
| ~ spl12_171
| ~ spl12_178 ),
inference(avatar_contradiction_clause,[],[f4719]) ).
fof(f4721,plain,
( ~ spl12_57
| ~ spl12_17 ),
inference(avatar_split_clause,[],[f4108,f574,f746]) ).
fof(f4730,plain,
( ~ spl12_166
| ~ spl12_59 ),
inference(avatar_split_clause,[],[f3424,f754,f1317]) ).
fof(f4933,plain,
( e22 != op2(e21,e20)
| ~ spl12_34 ),
inference(superposition,[],[f360,f649]) ).
fof(f4951,plain,
( e13 != op1(e13,e10)
| ~ spl12_69 ),
inference(superposition,[],[f143,f858]) ).
fof(f4952,plain,
( $false
| ~ spl12_69
| ~ spl12_73 ),
inference(forward_subsumption_resolution,[],[f4951,f875]) ).
fof(f4953,plain,
( ~ spl12_69
| ~ spl12_73 ),
inference(avatar_contradiction_clause,[],[f4952]) ).
fof(f4995,plain,
( op2(e23,e23) = op2(h4(e13),e21)
| ~ spl12_17 ),
inference(superposition,[],[f765,f576]) ).
fof(f4996,plain,
( op2(e22,e21) = op2(e23,e23)
| ~ spl12_17
| ~ spl12_138 ),
inference(forward_demodulation,[],[f4995,f1178]) ).
fof(f4997,plain,
( op2(e22,e21) = h4(e13)
| ~ spl12_17
| ~ spl12_138 ),
inference(forward_demodulation,[],[f4996,f456]) ).
fof(f4998,plain,
( e22 = op2(e22,e21)
| ~ spl12_17
| ~ spl12_138 ),
inference(forward_demodulation,[],[f4997,f1178]) ).
fof(f4999,plain,
( $false
| ~ spl12_17
| spl12_30
| ~ spl12_138 ),
inference(forward_subsumption_resolution,[],[f4998,f631]) ).
fof(f5000,plain,
( ~ spl12_17
| spl12_30
| ~ spl12_138 ),
inference(avatar_contradiction_clause,[],[f4999]) ).
fof(f5021,plain,
( ~ spl12_54
| ~ spl12_50 ),
inference(avatar_split_clause,[],[f3417,f716,f733]) ).
fof(f5062,plain,
( $false
| spl12_15
| ~ spl12_146
| ~ spl12_155 ),
inference(forward_subsumption_resolution,[],[f4715,f566]) ).
fof(f5063,plain,
( spl12_15
| ~ spl12_146
| ~ spl12_155 ),
inference(avatar_contradiction_clause,[],[f5062]) ).
fof(f5084,plain,
( ~ spl12_55
| ~ spl12_15 ),
inference(avatar_split_clause,[],[f3536,f565,f737]) ).
fof(f5087,plain,
( ~ spl12_138
| ~ spl12_18 ),
inference(avatar_split_clause,[],[f3156,f578,f1177]) ).
fof(f5094,plain,
( ~ spl12_46
| ~ spl12_34 ),
inference(avatar_split_clause,[],[f4933,f647,f699]) ).
fof(f5096,plain,
( ~ spl12_138
| ~ spl12_38 ),
inference(avatar_split_clause,[],[f3457,f664,f1177]) ).
fof(f5099,plain,
( ~ spl12_58
| ~ spl12_54 ),
inference(avatar_split_clause,[],[f3543,f733,f750]) ).
fof(f5179,plain,
( h3(e11) != h3(e11)
| ~ spl12_79
| spl12_217 ),
inference(forward_demodulation,[],[f1744,f900]) ).
fof(f5180,plain,
( $false
| ~ spl12_79
| spl12_217 ),
inference(trivial_inequality_removal,[],[f5179]) ).
fof(f5181,plain,
( ~ spl12_79
| spl12_217 ),
inference(avatar_contradiction_clause,[],[f5180]) ).
fof(f5197,plain,
( h3(op1(e13,e10)) != op2(h3(e13),e20)
| spl12_205
| ~ spl12_220 ),
inference(forward_demodulation,[],[f1696,f1758]) ).
fof(f5198,plain,
( op2(e23,e20) != h3(op1(e13,e10))
| ~ spl12_146
| spl12_205
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5197,f1218]) ).
fof(f5199,plain,
( op2(e23,e20) != h3(e13)
| ~ spl12_73
| ~ spl12_146
| spl12_205
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5198,f875]) ).
fof(f5200,plain,
( e23 != op2(e23,e20)
| ~ spl12_73
| ~ spl12_146
| spl12_205
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5199,f1218]) ).
fof(f5201,plain,
( $false
| ~ spl12_21
| ~ spl12_73
| ~ spl12_146
| spl12_205
| ~ spl12_220 ),
inference(forward_subsumption_resolution,[],[f5200,f593]) ).
fof(f5202,plain,
( ~ spl12_21
| ~ spl12_73
| ~ spl12_146
| spl12_205
| ~ spl12_220 ),
inference(avatar_contradiction_clause,[],[f5201]) ).
fof(f5204,plain,
( h3(op1(e11,e13)) != op2(h3(e11),e23)
| ~ spl12_146
| spl12_206 ),
inference(forward_demodulation,[],[f1700,f1218]) ).
fof(f5206,plain,
( op2(e21,e23) != h3(op1(e11,e13))
| ~ spl12_146
| ~ spl12_155
| spl12_206 ),
inference(forward_demodulation,[],[f5204,f1264]) ).
fof(f5208,plain,
( op2(e21,e23) != h3(e12)
| ~ spl12_94
| ~ spl12_146
| ~ spl12_155
| spl12_206 ),
inference(forward_demodulation,[],[f5206,f964]) ).
fof(f5210,plain,
( e22 != op2(e21,e23)
| ~ spl12_94
| ~ spl12_146
| ~ spl12_155
| spl12_206 ),
inference(forward_demodulation,[],[f5208,f455]) ).
fof(f5211,plain,
( $false
| ~ spl12_38
| ~ spl12_94
| ~ spl12_146
| ~ spl12_155
| spl12_206 ),
inference(forward_subsumption_resolution,[],[f5210,f666]) ).
fof(f5212,plain,
( ~ spl12_38
| ~ spl12_94
| ~ spl12_146
| ~ spl12_155
| spl12_206 ),
inference(avatar_contradiction_clause,[],[f5211]) ).
fof(f5214,plain,
( op2(e21,e21) != h3(op1(e11,e11))
| ~ spl12_155
| spl12_207 ),
inference(forward_demodulation,[],[f1704,f1264]) ).
fof(f5216,plain,
( op2(e21,e21) != h3(e13)
| ~ spl12_101
| ~ spl12_155
| spl12_207 ),
inference(forward_demodulation,[],[f5214,f994]) ).
fof(f5218,plain,
( e23 != op2(e21,e21)
| ~ spl12_101
| ~ spl12_146
| ~ spl12_155
| spl12_207 ),
inference(forward_demodulation,[],[f5216,f1218]) ).
fof(f5220,plain,
( e23 != h2(e13)
| ~ spl12_101
| ~ spl12_146
| ~ spl12_155
| spl12_207 ),
inference(forward_demodulation,[],[f5218,f448]) ).
fof(f5221,plain,
( $false
| ~ spl12_101
| ~ spl12_146
| ~ spl12_155
| ~ spl12_158
| spl12_207 ),
inference(forward_subsumption_resolution,[],[f5220,f1278]) ).
fof(f5222,plain,
( ~ spl12_101
| ~ spl12_146
| ~ spl12_155
| ~ spl12_158
| spl12_207 ),
inference(avatar_contradiction_clause,[],[f5221]) ).
fof(f5224,plain,
( h3(op1(e11,e10)) != op2(h3(e11),e20)
| spl12_208
| ~ spl12_220 ),
inference(forward_demodulation,[],[f1708,f1758]) ).
fof(f5226,plain,
( op2(e21,e20) != h3(op1(e11,e10))
| ~ spl12_155
| spl12_208
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5224,f1264]) ).
fof(f5228,plain,
( op2(e21,e20) != h3(e11)
| ~ spl12_107
| ~ spl12_155
| spl12_208
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5226,f1019]) ).
fof(f5229,plain,
( e21 != op2(e21,e20)
| ~ spl12_107
| ~ spl12_155
| spl12_208
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5228,f1264]) ).
fof(f5230,plain,
( $false
| ~ spl12_47
| ~ spl12_107
| ~ spl12_155
| spl12_208
| ~ spl12_220 ),
inference(forward_subsumption_resolution,[],[f5229,f705]) ).
fof(f5231,plain,
( ~ spl12_47
| ~ spl12_107
| ~ spl12_155
| spl12_208
| ~ spl12_220 ),
inference(avatar_contradiction_clause,[],[f5230]) ).
fof(f5233,plain,
( h3(op1(e10,e13)) != op2(h3(e10),e23)
| ~ spl12_146
| spl12_209 ),
inference(forward_demodulation,[],[f1712,f1218]) ).
fof(f5235,plain,
( op2(e20,e23) != h3(op1(e10,e13))
| ~ spl12_146
| spl12_209
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5233,f1758]) ).
fof(f5237,plain,
( op2(e20,e23) != h3(e13)
| ~ spl12_109
| ~ spl12_146
| spl12_209
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5235,f1028]) ).
fof(f5239,plain,
( e23 != op2(e20,e23)
| ~ spl12_109
| ~ spl12_146
| spl12_209
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5237,f1218]) ).
fof(f5240,plain,
( $false
| ~ spl12_49
| ~ spl12_109
| ~ spl12_146
| spl12_209
| ~ spl12_220 ),
inference(forward_subsumption_resolution,[],[f5239,f714]) ).
fof(f5241,plain,
( ~ spl12_49
| ~ spl12_109
| ~ spl12_146
| spl12_209
| ~ spl12_220 ),
inference(avatar_contradiction_clause,[],[f5240]) ).
fof(f5243,plain,
( h3(op1(e10,e11)) != op2(h3(e10),e21)
| ~ spl12_155
| spl12_210 ),
inference(forward_demodulation,[],[f1716,f1264]) ).
fof(f5245,plain,
( op2(e20,e21) != h3(op1(e10,e11))
| ~ spl12_155
| spl12_210
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5243,f1758]) ).
fof(f5247,plain,
( op2(e20,e21) != h3(e11)
| ~ spl12_119
| ~ spl12_155
| spl12_210
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5245,f1070]) ).
fof(f5249,plain,
( e21 != op2(e20,e21)
| ~ spl12_119
| ~ spl12_155
| spl12_210
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5247,f1264]) ).
fof(f5250,plain,
( $false
| ~ spl12_59
| ~ spl12_119
| ~ spl12_155
| spl12_210
| ~ spl12_220 ),
inference(forward_subsumption_resolution,[],[f5249,f756]) ).
fof(f5251,plain,
( ~ spl12_59
| ~ spl12_119
| ~ spl12_155
| spl12_210
| ~ spl12_220 ),
inference(avatar_contradiction_clause,[],[f5250]) ).
fof(f5253,plain,
( op2(e20,e20) != h3(op1(e10,e10))
| spl12_211
| ~ spl12_220 ),
inference(forward_demodulation,[],[f1720,f1758]) ).
fof(f5255,plain,
( op2(e20,e20) != h3(e10)
| ~ spl12_124
| spl12_211
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5253,f1091]) ).
fof(f5257,plain,
( e20 != op2(e20,e20)
| ~ spl12_124
| spl12_211
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5255,f1758]) ).
fof(f5259,plain,
( e20 != h1(e13)
| ~ spl12_124
| spl12_211
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5257,f444]) ).
fof(f5260,plain,
( $false
| ~ spl12_124
| ~ spl12_183
| spl12_211
| ~ spl12_220 ),
inference(forward_subsumption_resolution,[],[f5259,f1487]) ).
fof(f5261,plain,
( ~ spl12_124
| ~ spl12_183
| spl12_211
| ~ spl12_220 ),
inference(avatar_contradiction_clause,[],[f5260]) ).
fof(f5263,plain,
( op2(e20,e22) != h3(op1(e10,e12))
| spl12_212
| ~ spl12_220 ),
inference(forward_demodulation,[],[f1724,f1758]) ).
fof(f5265,plain,
( op2(e20,e22) != h3(e12)
| ~ spl12_114
| spl12_212
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5263,f1049]) ).
fof(f5267,plain,
( e22 != op2(e20,e22)
| ~ spl12_114
| spl12_212
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5265,f455]) ).
fof(f5268,plain,
( $false
| ~ spl12_54
| ~ spl12_114
| spl12_212
| ~ spl12_220 ),
inference(forward_subsumption_resolution,[],[f5267,f735]) ).
fof(f5269,plain,
( ~ spl12_54
| ~ spl12_114
| spl12_212
| ~ spl12_220 ),
inference(avatar_contradiction_clause,[],[f5268]) ).
fof(f5271,plain,
( h3(e10) != h3(e10)
| ~ spl12_100
| spl12_213 ),
inference(forward_demodulation,[],[f1728,f989]) ).
fof(f5272,plain,
( $false
| ~ spl12_100
| spl12_213 ),
inference(trivial_inequality_removal,[],[f5271]) ).
fof(f5273,plain,
( ~ spl12_100
| spl12_213 ),
inference(avatar_contradiction_clause,[],[f5272]) ).
fof(f5276,plain,
( op2(e22,e20) != h3(op1(e12,e10))
| spl12_214
| ~ spl12_220 ),
inference(forward_demodulation,[],[f1732,f1758]) ).
fof(f5277,plain,
( op2(e22,e20) != h3(e12)
| ~ spl12_90
| spl12_214
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5276,f947]) ).
fof(f5278,plain,
( e22 != op2(e22,e20)
| ~ spl12_90
| spl12_214
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5277,f455]) ).
fof(f5279,plain,
( $false
| ~ spl12_34
| ~ spl12_90
| spl12_214
| ~ spl12_220 ),
inference(forward_subsumption_resolution,[],[f5278,f649]) ).
fof(f5280,plain,
( ~ spl12_34
| ~ spl12_90
| spl12_214
| ~ spl12_220 ),
inference(avatar_contradiction_clause,[],[f5279]) ).
fof(f5282,plain,
( op2(e22,e21) != h3(op1(e12,e11))
| ~ spl12_155
| spl12_215 ),
inference(forward_demodulation,[],[f1736,f1264]) ).
fof(f5284,plain,
( op2(e22,e21) != h3(e10)
| ~ spl12_88
| ~ spl12_155
| spl12_215 ),
inference(forward_demodulation,[],[f5282,f938]) ).
fof(f5286,plain,
( e20 != op2(e22,e21)
| ~ spl12_88
| ~ spl12_155
| spl12_215
| ~ spl12_220 ),
inference(forward_demodulation,[],[f5284,f1758]) ).
fof(f5287,plain,
( $false
| ~ spl12_32
| ~ spl12_88
| ~ spl12_155
| spl12_215
| ~ spl12_220 ),
inference(forward_subsumption_resolution,[],[f5286,f640]) ).
fof(f5288,plain,
( ~ spl12_32
| ~ spl12_88
| ~ spl12_155
| spl12_215
| ~ spl12_220 ),
inference(avatar_contradiction_clause,[],[f5287]) ).
fof(f5290,plain,
( h3(e13) != h3(e13)
| ~ spl12_81
| spl12_216 ),
inference(forward_demodulation,[],[f1740,f909]) ).
fof(f5291,plain,
( $false
| ~ spl12_81
| spl12_216 ),
inference(trivial_inequality_removal,[],[f5290]) ).
fof(f5292,plain,
( ~ spl12_81
| spl12_216 ),
inference(avatar_contradiction_clause,[],[f5291]) ).
fof(f5317,plain,
( $false
| spl12_73
| ~ spl12_128 ),
inference(forward_subsumption_resolution,[],[f2452,f874]) ).
fof(f5318,plain,
( spl12_73
| ~ spl12_128 ),
inference(avatar_contradiction_clause,[],[f5317]) ).
fof(f5389,plain,
( ~ spl12_114
| ~ spl12_66 ),
inference(avatar_split_clause,[],[f2863,f843,f1047]) ).
fof(f5701,plain,
( $false
| ~ spl12_79
| ~ spl12_95 ),
inference(forward_subsumption_resolution,[],[f2656,f968]) ).
fof(f5702,plain,
( ~ spl12_79
| ~ spl12_95 ),
inference(avatar_contradiction_clause,[],[f5701]) ).
fof(f5732,plain,
( spl12_8
| ~ spl12_7 ),
inference(avatar_split_clause,[],[f2468,f516,f520]) ).
fof(f5736,plain,
( ~ spl12_181
| ~ spl12_20 ),
inference(avatar_split_clause,[],[f3297,f586,f1475]) ).
fof(f5737,plain,
( ~ spl12_60
| ~ spl12_20 ),
inference(avatar_split_clause,[],[f4618,f586,f758]) ).
fof(f5738,plain,
( ~ spl12_32
| ~ spl12_20 ),
inference(avatar_split_clause,[],[f4617,f586,f638]) ).
fof(f5739,plain,
( ~ spl12_138
| ~ spl12_22 ),
inference(avatar_split_clause,[],[f3193,f595,f1177]) ).
fof(f5743,plain,
( ~ spl12_183
| ~ spl12_36 ),
inference(avatar_split_clause,[],[f3219,f655,f1485]) ).
fof(f5750,plain,
( ~ spl12_60
| ~ spl12_52 ),
inference(avatar_split_clause,[],[f3602,f724,f758]) ).
fof(f5751,plain,
( ~ spl12_181
| ~ spl12_52 ),
inference(avatar_split_clause,[],[f3606,f724,f1475]) ).
fof(f5758,plain,
( ~ spl12_68
| ~ spl12_64 ),
inference(avatar_split_clause,[],[f2580,f834,f851]) ).
fof(f5760,plain,
( ~ spl12_72
| ~ spl12_64 ),
inference(avatar_split_clause,[],[f2582,f834,f868]) ).
fof(f5770,plain,
( ~ spl12_71
| ~ spl12_67 ),
inference(avatar_split_clause,[],[f2898,f847,f864]) ).
fof(f6163,plain,
( op2(e23,e21) = op2(h4(e13),e22)
| ~ spl12_15 ),
inference(superposition,[],[f764,f567]) ).
fof(f6166,plain,
( op2(e23,e21) = op2(e23,e22)
| ~ spl12_15
| ~ spl12_134 ),
inference(forward_demodulation,[],[f6163,f1158]) ).
fof(f6171,plain,
( $false
| ~ spl12_15
| ~ spl12_134 ),
inference(forward_subsumption_resolution,[],[f6166,f318]) ).
fof(f6172,plain,
( ~ spl12_15
| ~ spl12_134 ),
inference(avatar_contradiction_clause,[],[f6171]) ).
cnf(s2,plain,
( ~ spl12_3
| spl12_4 ),
inference(sat_conversion,[],[f504]) ).
cnf(s3,plain,
( ~ spl12_5
| spl12_6 ),
inference(sat_conversion,[],[f513]) ).
cnf(s4,plain,
( spl12_1
| ~ spl12_2 ),
inference(sat_conversion,[],[f514]) ).
cnf(s6,plain,
( ~ spl12_9
| spl12_10 ),
inference(sat_conversion,[],[f532]) ).
cnf(s14,plain,
( spl12_17
| spl12_18
| spl12_19
| spl12_20 ),
inference(sat_conversion,[],[f589]) ).
cnf(s15,plain,
( spl12_21
| spl12_22
| spl12_23
| spl12_24 ),
inference(sat_conversion,[],[f606]) ).
cnf(s17,plain,
( spl12_29
| spl12_30
| spl12_31
| spl12_32 ),
inference(sat_conversion,[],[f641]) ).
cnf(s18,plain,
( spl12_33
| spl12_34
| spl12_35
| spl12_36 ),
inference(sat_conversion,[],[f658]) ).
cnf(s19,plain,
( spl12_37
| spl12_38
| spl12_39
| spl12_40 ),
inference(sat_conversion,[],[f675]) ).
cnf(s21,plain,
( spl12_45
| spl12_46
| spl12_47
| spl12_48 ),
inference(sat_conversion,[],[f710]) ).
cnf(s22,plain,
( spl12_49
| spl12_50
| spl12_51
| spl12_52 ),
inference(sat_conversion,[],[f727]) ).
cnf(s23,plain,
( spl12_53
| spl12_54
| spl12_55
| spl12_56 ),
inference(sat_conversion,[],[f744]) ).
cnf(s24,plain,
( spl12_57
| spl12_58
| spl12_59
| spl12_60 ),
inference(sat_conversion,[],[f761]) ).
cnf(s26,plain,
( spl12_65
| spl12_66
| spl12_67
| spl12_68 ),
inference(sat_conversion,[],[f854]) ).
cnf(s27,plain,
( spl12_69
| spl12_70
| spl12_71
| spl12_72 ),
inference(sat_conversion,[],[f871]) ).
cnf(s33,plain,
( spl12_93
| spl12_94
| spl12_95
| spl12_96 ),
inference(sat_conversion,[],[f973]) ).
cnf(s35,plain,
( spl12_101
| spl12_102
| spl12_103
| spl12_104 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s41,plain,
( spl12_125
| spl12_126
| spl12_127
| spl12_128 ),
inference(sat_conversion,[],[f1109]) ).
cnf(s42,plain,
( spl12_1
| spl12_3
| spl12_5
| spl12_129 ),
inference(sat_conversion,[],[f1114]) ).
cnf(s43,plain,
( spl12_2
| spl12_7
| spl12_9
| spl12_130 ),
inference(sat_conversion,[],[f1119]) ).
cnf(s50,plain,
spl12_81,
inference(sat_conversion,[],[f1134]) ).
cnf(s60,plain,
( ~ spl12_145
| ~ spl12_146 ),
inference(sat_conversion,[],[f1220]) ).
cnf(s67,plain,
( ~ spl12_153
| ~ spl12_155 ),
inference(sat_conversion,[],[f1266]) ).
cnf(s87,plain,
spl12_100,
inference(sat_conversion,[],[f1408]) ).
cnf(s89,plain,
~ spl12_149,
inference(sat_conversion,[],[f1426]) ).
cnf(s91,plain,
( spl12_134
| spl12_138
| spl12_142
| spl12_181 ),
inference(sat_conversion,[],[f1478]) ).
cnf(s92,plain,
( spl12_158
| spl12_162
| spl12_166
| spl12_182 ),
inference(sat_conversion,[],[f1483]) ).
cnf(s93,plain,
( spl12_170
| spl12_174
| spl12_178
| spl12_183 ),
inference(sat_conversion,[],[f1488]) ).
cnf(s103,plain,
( spl12_145
| spl12_149
| spl12_153
| ~ spl12_203
| ~ spl12_204
| ~ spl12_205
| ~ spl12_206
| ~ spl12_207
| ~ spl12_208
| ~ spl12_209
| ~ spl12_210
| ~ spl12_211
| ~ spl12_212
| ~ spl12_213
| ~ spl12_214
| ~ spl12_215
| ~ spl12_216
| ~ spl12_217
| ~ spl12_218
| ~ spl12_220 ),
inference(sat_conversion,[],[f1760]) ).
cnf(s117,plain,
( ~ spl12_128
| spl12_132 ),
inference(sat_conversion,[],[f1965]) ).
cnf(s119,plain,
( ~ spl12_100
| ~ spl12_126 ),
inference(sat_conversion,[],[f1987]) ).
cnf(s120,plain,
( spl12_107
| ~ spl12_128 ),
inference(sat_conversion,[],[f1997]) ).
cnf(s121,plain,
( spl12_114
| ~ spl12_128 ),
inference(sat_conversion,[],[f1998]) ).
cnf(s122,plain,
( spl12_90
| ~ spl12_128 ),
inference(sat_conversion,[],[f1999]) ).
cnf(s124,plain,
( ~ spl12_6
| ~ spl12_132 ),
inference(sat_conversion,[],[f2005]) ).
cnf(s125,plain,
( spl12_119
| ~ spl12_128 ),
inference(sat_conversion,[],[f2013]) ).
cnf(s126,plain,
( spl12_124
| ~ spl12_128 ),
inference(sat_conversion,[],[f2015]) ).
cnf(s139,plain,
( spl12_64
| ~ spl12_128
| ~ spl12_129 ),
inference(sat_conversion,[],[f2076]) ).
cnf(s144,plain,
( spl12_84
| ~ spl12_128
| ~ spl12_130 ),
inference(sat_conversion,[],[f2100]) ).
cnf(s146,plain,
( ~ spl12_81
| ~ spl12_84 ),
inference(sat_conversion,[],[f2107]) ).
cnf(s148,plain,
( ~ spl12_10
| ~ spl12_132 ),
inference(sat_conversion,[],[f2117]) ).
cnf(s150,plain,
( ~ spl12_1
| spl12_80
| ~ spl12_128 ),
inference(sat_conversion,[],[f2135]) ).
cnf(s158,plain,
spl12_146,
inference(sat_conversion,[],[f2178]) ).
cnf(s161,plain,
( ~ spl12_29
| ~ spl12_146 ),
inference(sat_conversion,[],[f2191]) ).
cnf(s162,plain,
( ~ spl12_33
| ~ spl12_146 ),
inference(sat_conversion,[],[f2197]) ).
cnf(s177,plain,
( ~ spl12_80
| ~ spl12_81 ),
inference(sat_conversion,[],[f2307]) ).
cnf(s178,plain,
( spl12_79
| ~ spl12_81 ),
inference(sat_conversion,[],[f2317]) ).
cnf(s186,plain,
( spl12_95
| ~ spl12_125 ),
inference(sat_conversion,[],[f2347]) ).
cnf(s213,plain,
( ~ spl12_100
| ~ spl12_127 ),
inference(sat_conversion,[],[f2431]) ).
cnf(s217,plain,
( ~ spl12_7
| spl12_88
| ~ spl12_128 ),
inference(sat_conversion,[],[f2473]) ).
cnf(s238,plain,
( ~ spl12_100
| ~ spl12_104 ),
inference(sat_conversion,[],[f2610]) ).
cnf(s241,plain,
( ~ spl12_93
| ~ spl12_109 ),
inference(sat_conversion,[],[f2664]) ).
cnf(s242,plain,
( spl12_109
| ~ spl12_128 ),
inference(sat_conversion,[],[f2668]) ).
cnf(s245,plain,
( ~ spl12_94
| ~ spl12_102 ),
inference(sat_conversion,[],[f2687]) ).
cnf(s246,plain,
( ~ spl12_103
| ~ spl12_107 ),
inference(sat_conversion,[],[f2706]) ).
cnf(s247,plain,
( ~ spl12_4
| ~ spl12_8 ),
inference(sat_conversion,[],[f2722]) ).
cnf(s249,plain,
( ~ spl12_64
| ~ spl12_96 ),
inference(sat_conversion,[],[f2735]) ).
cnf(s254,plain,
( ~ spl12_53
| ~ spl12_146 ),
inference(sat_conversion,[],[f2791]) ).
cnf(s263,plain,
( ~ spl12_65
| ~ spl12_81 ),
inference(sat_conversion,[],[f2883]) ).
cnf(s264,plain,
( ~ spl12_67
| spl12_218 ),
inference(sat_conversion,[],[f2890]) ).
cnf(s272,plain,
( spl12_27
| ~ spl12_146 ),
inference(sat_conversion,[],[f2980]) ).
cnf(s275,plain,
( ~ spl12_27
| ~ spl12_35 ),
inference(sat_conversion,[],[f2988]) ).
cnf(s279,plain,
( ~ spl12_64
| ~ spl12_146
| ~ spl12_181
| spl12_203
| ~ spl12_220 ),
inference(sat_conversion,[],[f3014]) ).
cnf(s284,plain,
( ~ spl12_27
| ~ spl12_142 ),
inference(sat_conversion,[],[f3032]) ).
cnf(s304,plain,
( ~ spl12_18
| ~ spl12_162 ),
inference(sat_conversion,[],[f3159]) ).
cnf(s308,plain,
( ~ spl12_15
| ~ spl12_19 ),
inference(sat_conversion,[],[f3175]) ).
cnf(s314,plain,
( ~ spl12_27
| ~ spl12_31 ),
inference(sat_conversion,[],[f3251]) ).
cnf(s318,plain,
( ~ spl12_17
| ~ spl12_158 ),
inference(sat_conversion,[],[f3277]) ).
cnf(s325,plain,
( ~ spl12_18
| ~ spl12_22 ),
inference(sat_conversion,[],[f3303]) ).
cnf(s341,plain,
( ~ spl12_27
| ~ spl12_39 ),
inference(sat_conversion,[],[f3449]) ).
cnf(s344,plain,
( ~ spl12_40
| ~ spl12_44 ),
inference(sat_conversion,[],[f3475]) ).
cnf(s358,plain,
( ~ spl12_32
| ~ spl12_36 ),
inference(sat_conversion,[],[f3562]) ).
cnf(s369,plain,
( ~ spl12_27
| ~ spl12_51 ),
inference(sat_conversion,[],[f3629]) ).
cnf(s370,plain,
( ~ spl12_49
| ~ spl12_57 ),
inference(sat_conversion,[],[f3640]) ).
cnf(s382,plain,
( ~ spl12_17
| ~ spl12_21 ),
inference(sat_conversion,[],[f3689]) ).
cnf(s398,plain,
( ~ spl12_32
| ~ spl12_60 ),
inference(sat_conversion,[],[f3835]) ).
cnf(s400,plain,
( ~ spl12_37
| ~ spl12_49 ),
inference(sat_conversion,[],[f3840]) ).
cnf(s404,plain,
( ~ spl12_30
| ~ spl12_162 ),
inference(sat_conversion,[],[f3891]) ).
cnf(s405,plain,
( ~ spl12_30
| ~ spl12_34 ),
inference(sat_conversion,[],[f3892]) ).
cnf(s409,plain,
spl12_155,
inference(sat_conversion,[],[f3984]) ).
cnf(s412,plain,
( spl12_44
| ~ spl12_155 ),
inference(sat_conversion,[],[f3990]) ).
cnf(s413,plain,
( ~ spl12_44
| ~ spl12_56 ),
inference(sat_conversion,[],[f3991]) ).
cnf(s414,plain,
( ~ spl12_44
| ~ spl12_182 ),
inference(sat_conversion,[],[f3995]) ).
cnf(s416,plain,
( ~ spl12_59
| ~ spl12_178 ),
inference(sat_conversion,[],[f3998]) ).
cnf(s425,plain,
( spl12_21
| ~ spl12_135
| ~ spl12_181 ),
inference(sat_conversion,[],[f4064]) ).
cnf(s433,plain,
( ~ spl12_15
| ~ spl12_23 ),
inference(sat_conversion,[],[f4120]) ).
cnf(s440,plain,
( ~ spl12_44
| ~ spl12_48 ),
inference(sat_conversion,[],[f4143]) ).
cnf(s457,plain,
spl12_220,
inference(sat_conversion,[],[f4259]) ).
cnf(s473,plain,
( ~ spl12_21
| ~ spl12_170 ),
inference(sat_conversion,[],[f4319]) ).
cnf(s477,plain,
( ~ spl12_21
| ~ spl12_45 ),
inference(sat_conversion,[],[f4321]) ).
cnf(s483,plain,
( ~ spl12_49
| ~ spl12_170 ),
inference(sat_conversion,[],[f4328]) ).
cnf(s485,plain,
( ~ spl12_54
| ~ spl12_174 ),
inference(sat_conversion,[],[f4330]) ).
cnf(s507,plain,
( ~ spl12_49
| spl12_135
| ~ spl12_181 ),
inference(sat_conversion,[],[f4405]) ).
cnf(s508,plain,
( ~ spl12_24
| ~ spl12_181 ),
inference(sat_conversion,[],[f4407]) ).
cnf(s525,plain,
( ~ spl12_18
| ~ spl12_30 ),
inference(sat_conversion,[],[f4495]) ).
cnf(s528,plain,
( ~ spl12_18
| ~ spl12_70
| ~ spl12_146
| ~ spl12_155
| spl12_204 ),
inference(sat_conversion,[],[f4513]) ).
cnf(s529,plain,
( ~ spl12_20
| ~ spl12_24 ),
inference(sat_conversion,[],[f4514]) ).
cnf(s541,plain,
( ~ spl12_57
| spl12_171
| ~ spl12_178 ),
inference(sat_conversion,[],[f4592]) ).
cnf(s552,plain,
( spl12_45
| ~ spl12_171
| ~ spl12_178 ),
inference(sat_conversion,[],[f4720]) ).
cnf(s555,plain,
( ~ spl12_17
| ~ spl12_57 ),
inference(sat_conversion,[],[f4721]) ).
cnf(s568,plain,
( ~ spl12_59
| ~ spl12_166 ),
inference(sat_conversion,[],[f4730]) ).
cnf(s588,plain,
( ~ spl12_69
| ~ spl12_73 ),
inference(sat_conversion,[],[f4953]) ).
cnf(s591,plain,
( ~ spl12_17
| spl12_30
| ~ spl12_138 ),
inference(sat_conversion,[],[f5000]) ).
cnf(s617,plain,
( ~ spl12_50
| ~ spl12_54 ),
inference(sat_conversion,[],[f5021]) ).
cnf(s627,plain,
( spl12_15
| ~ spl12_146
| ~ spl12_155 ),
inference(sat_conversion,[],[f5063]) ).
cnf(s639,plain,
( ~ spl12_15
| ~ spl12_55 ),
inference(sat_conversion,[],[f5084]) ).
cnf(s645,plain,
( ~ spl12_18
| ~ spl12_138 ),
inference(sat_conversion,[],[f5087]) ).
cnf(s669,plain,
( ~ spl12_34
| ~ spl12_46 ),
inference(sat_conversion,[],[f5094]) ).
cnf(s671,plain,
( ~ spl12_38
| ~ spl12_138 ),
inference(sat_conversion,[],[f5096]) ).
cnf(s683,plain,
( ~ spl12_54
| ~ spl12_58 ),
inference(sat_conversion,[],[f5099]) ).
cnf(s692,plain,
( ~ spl12_79
| spl12_217 ),
inference(sat_conversion,[],[f5181]) ).
cnf(s693,plain,
( ~ spl12_21
| ~ spl12_73
| ~ spl12_146
| spl12_205
| ~ spl12_220 ),
inference(sat_conversion,[],[f5202]) ).
cnf(s694,plain,
( ~ spl12_38
| ~ spl12_94
| ~ spl12_146
| ~ spl12_155
| spl12_206 ),
inference(sat_conversion,[],[f5212]) ).
cnf(s695,plain,
( ~ spl12_101
| ~ spl12_146
| ~ spl12_155
| ~ spl12_158
| spl12_207 ),
inference(sat_conversion,[],[f5222]) ).
cnf(s696,plain,
( ~ spl12_47
| ~ spl12_107
| ~ spl12_155
| spl12_208
| ~ spl12_220 ),
inference(sat_conversion,[],[f5231]) ).
cnf(s697,plain,
( ~ spl12_49
| ~ spl12_109
| ~ spl12_146
| spl12_209
| ~ spl12_220 ),
inference(sat_conversion,[],[f5241]) ).
cnf(s698,plain,
( ~ spl12_59
| ~ spl12_119
| ~ spl12_155
| spl12_210
| ~ spl12_220 ),
inference(sat_conversion,[],[f5251]) ).
cnf(s699,plain,
( ~ spl12_124
| ~ spl12_183
| spl12_211
| ~ spl12_220 ),
inference(sat_conversion,[],[f5261]) ).
cnf(s700,plain,
( ~ spl12_54
| ~ spl12_114
| spl12_212
| ~ spl12_220 ),
inference(sat_conversion,[],[f5269]) ).
cnf(s701,plain,
( ~ spl12_100
| spl12_213 ),
inference(sat_conversion,[],[f5273]) ).
cnf(s702,plain,
( ~ spl12_34
| ~ spl12_90
| spl12_214
| ~ spl12_220 ),
inference(sat_conversion,[],[f5280]) ).
cnf(s703,plain,
( ~ spl12_32
| ~ spl12_88
| ~ spl12_155
| spl12_215
| ~ spl12_220 ),
inference(sat_conversion,[],[f5288]) ).
cnf(s704,plain,
( ~ spl12_81
| spl12_216 ),
inference(sat_conversion,[],[f5292]) ).
cnf(s709,plain,
( spl12_73
| ~ spl12_128 ),
inference(sat_conversion,[],[f5318]) ).
cnf(s715,plain,
( ~ spl12_66
| ~ spl12_114 ),
inference(sat_conversion,[],[f5389]) ).
cnf(s761,plain,
( ~ spl12_79
| ~ spl12_95 ),
inference(sat_conversion,[],[f5702]) ).
cnf(s767,plain,
( ~ spl12_7
| spl12_8 ),
inference(sat_conversion,[],[f5732]) ).
cnf(s771,plain,
( ~ spl12_20
| ~ spl12_181 ),
inference(sat_conversion,[],[f5736]) ).
cnf(s772,plain,
( ~ spl12_20
| ~ spl12_60 ),
inference(sat_conversion,[],[f5737]) ).
cnf(s776,plain,
( ~ spl12_20
| ~ spl12_32 ),
inference(sat_conversion,[],[f5738]) ).
cnf(s777,plain,
( ~ spl12_22
| ~ spl12_138 ),
inference(sat_conversion,[],[f5739]) ).
cnf(s788,plain,
( ~ spl12_36
| ~ spl12_183 ),
inference(sat_conversion,[],[f5743]) ).
cnf(s798,plain,
( ~ spl12_52
| ~ spl12_60 ),
inference(sat_conversion,[],[f5750]) ).
cnf(s799,plain,
( ~ spl12_52
| ~ spl12_181 ),
inference(sat_conversion,[],[f5751]) ).
cnf(s809,plain,
( ~ spl12_64
| ~ spl12_68 ),
inference(sat_conversion,[],[f5758]) ).
cnf(s811,plain,
( ~ spl12_64
| ~ spl12_72 ),
inference(sat_conversion,[],[f5760]) ).
cnf(s822,plain,
( ~ spl12_67
| ~ spl12_71 ),
inference(sat_conversion,[],[f5770]) ).
cnf(s857,plain,
( ~ spl12_15
| ~ spl12_134 ),
inference(sat_conversion,[],[f6172]) ).
cnf(s858,plain,
spl12_44,
inference(rat,[],[s412,s409]) ).
cnf(s859,plain,
~ spl12_48,
inference(rat,[],[s440,s858]) ).
cnf(s860,plain,
~ spl12_182,
inference(rat,[],[s414,s858]) ).
cnf(s861,plain,
~ spl12_56,
inference(rat,[],[s413,s858]) ).
cnf(s862,plain,
~ spl12_40,
inference(rat,[],[s344,s858]) ).
cnf(s863,plain,
( ~ spl12_64
| ~ spl12_146
| ~ spl12_181
| spl12_203 ),
inference(rat,[],[s279,s457]) ).
cnf(s865,plain,
spl12_15,
inference(rat,[],[s627,s409,s158]) ).
cnf(s866,plain,
spl12_27,
inference(rat,[],[s272,s158]) ).
cnf(s867,plain,
~ spl12_53,
inference(rat,[],[s254,s158]) ).
cnf(s871,plain,
~ spl12_33,
inference(rat,[],[s162,s158]) ).
cnf(s872,plain,
~ spl12_29,
inference(rat,[],[s161,s158]) ).
cnf(s874,plain,
~ spl12_134,
inference(rat,[],[s857,s865]) ).
cnf(s875,plain,
~ spl12_55,
inference(rat,[],[s639,s865]) ).
cnf(s876,plain,
~ spl12_23,
inference(rat,[],[s433,s865]) ).
cnf(s878,plain,
~ spl12_19,
inference(rat,[],[s308,s865]) ).
cnf(s879,plain,
~ spl12_51,
inference(rat,[],[s369,s866]) ).
cnf(s880,plain,
~ spl12_39,
inference(rat,[],[s341,s866]) ).
cnf(s881,plain,
~ spl12_31,
inference(rat,[],[s314,s866]) ).
cnf(s883,plain,
~ spl12_142,
inference(rat,[],[s284,s866]) ).
cnf(s884,plain,
~ spl12_35,
inference(rat,[],[s275,s866]) ).
cnf(s885,plain,
( spl12_145
| spl12_149
| spl12_153
| ~ spl12_203
| ~ spl12_204
| ~ spl12_205
| ~ spl12_206
| ~ spl12_207
| ~ spl12_208
| ~ spl12_209
| ~ spl12_210
| ~ spl12_211
| ~ spl12_212
| ~ spl12_213
| ~ spl12_214
| ~ spl12_215
| ~ spl12_216
| ~ spl12_217
| ~ spl12_218 ),
inference(rat,[],[s103,s457]) ).
cnf(s886,plain,
( spl12_158
| spl12_162
| spl12_166 ),
inference(rat,[],[s92,s860]) ).
cnf(s887,plain,
( spl12_138
| spl12_181 ),
inference(rat,[],[s91,s883,s874]) ).
cnf(s890,plain,
spl12_213,
inference(rat,[],[s701,s87]) ).
cnf(s892,plain,
~ spl12_104,
inference(rat,[],[s238,s87]) ).
cnf(s893,plain,
~ spl12_127,
inference(rat,[],[s213,s87]) ).
cnf(s894,plain,
~ spl12_126,
inference(rat,[],[s119,s87]) ).
cnf(s895,plain,
~ spl12_153,
inference(rat,[],[s67,s409]) ).
cnf(s896,plain,
~ spl12_145,
inference(rat,[],[s60,s158]) ).
cnf(s899,plain,
spl12_216,
inference(rat,[],[s704,s50]) ).
cnf(s900,plain,
~ spl12_65,
inference(rat,[],[s263,s50]) ).
cnf(s901,plain,
spl12_79,
inference(rat,[],[s178,s50]) ).
cnf(s902,plain,
~ spl12_80,
inference(rat,[],[s177,s50]) ).
cnf(s903,plain,
~ spl12_84,
inference(rat,[],[s146,s50]) ).
cnf(s906,plain,
~ spl12_95,
inference(rat,[],[s761,s901]) ).
cnf(s907,plain,
spl12_217,
inference(rat,[],[s692,s901]) ).
cnf(s910,plain,
~ spl12_125,
inference(rat,[],[s186,s906]) ).
cnf(s912,plain,
spl12_128,
inference(rat,[],[s41,s893,s894,s910]) ).
cnf(s913,plain,
spl12_73,
inference(rat,[],[s709,s912]) ).
cnf(s914,plain,
spl12_109,
inference(rat,[],[s242,s912]) ).
cnf(s918,plain,
~ spl12_130,
inference(rat,[],[s144,s903,s912]) ).
cnf(s919,plain,
spl12_124,
inference(rat,[],[s126,s912]) ).
cnf(s920,plain,
spl12_119,
inference(rat,[],[s125,s912]) ).
cnf(s921,plain,
spl12_90,
inference(rat,[],[s122,s912]) ).
cnf(s922,plain,
spl12_114,
inference(rat,[],[s121,s912]) ).
cnf(s923,plain,
spl12_107,
inference(rat,[],[s120,s912]) ).
cnf(s924,plain,
spl12_132,
inference(rat,[],[s117,s912]) ).
cnf(s925,plain,
~ spl12_1,
inference(rat,[],[s150,s902,s912]) ).
cnf(s928,plain,
~ spl12_69,
inference(rat,[],[s588,s913]) ).
cnf(s930,plain,
~ spl12_93,
inference(rat,[],[s241,s914]) ).
cnf(s935,plain,
~ spl12_66,
inference(rat,[],[s715,s922]) ).
cnf(s936,plain,
~ spl12_103,
inference(rat,[],[s246,s923]) ).
cnf(s938,plain,
~ spl12_10,
inference(rat,[],[s148,s924]) ).
cnf(s939,plain,
~ spl12_6,
inference(rat,[],[s124,s924]) ).
cnf(s940,plain,
( spl12_101
| spl12_102 ),
inference(rat,[],[s35,s892,s936]) ).
cnf(s941,plain,
( spl12_94
| spl12_96 ),
inference(rat,[],[s33,s906,s930]) ).
cnf(s942,plain,
( spl12_70
| spl12_71
| spl12_72 ),
inference(rat,[],[s27,s928]) ).
cnf(s943,plain,
( spl12_67
| spl12_68 ),
inference(rat,[],[s26,s935,s900]) ).
cnf(s944,plain,
spl12_54,
inference(rat,[],[s23,s861,s875,s867]) ).
cnf(s945,plain,
spl12_212,
inference(rat,[],[s700,s457,s922,s944]) ).
cnf(s946,plain,
~ spl12_58,
inference(rat,[],[s683,s944]) ).
cnf(s947,plain,
~ spl12_50,
inference(rat,[],[s617,s944]) ).
cnf(s949,plain,
~ spl12_174,
inference(rat,[],[s485,s944]) ).
cnf(s951,plain,
( spl12_49
| spl12_52 ),
inference(rat,[],[s22,s879,s947]) ).
cnf(s952,plain,
( spl12_45
| spl12_46
| spl12_47 ),
inference(rat,[],[s21,s859]) ).
cnf(s953,plain,
( spl12_37
| spl12_38 ),
inference(rat,[],[s19,s862,s880]) ).
cnf(s954,plain,
( spl12_34
| spl12_36 ),
inference(rat,[],[s18,s884,s871]) ).
cnf(s955,plain,
( spl12_30
| spl12_32 ),
inference(rat,[],[s17,s881,s872]) ).
cnf(s956,plain,
( spl12_21
| spl12_22
| spl12_24 ),
inference(rat,[],[s15,s876]) ).
cnf(s957,plain,
( spl12_17
| spl12_18
| spl12_20 ),
inference(rat,[],[s14,s878]) ).
cnf(s958,plain,
~ spl12_9,
inference(rat,[],[s6,s938]) ).
cnf(s959,plain,
~ spl12_2,
inference(rat,[],[s4,s925]) ).
cnf(s960,plain,
spl12_7,
inference(rat,[],[s43,s918,s958,s959]) ).
cnf(s961,plain,
spl12_8,
inference(rat,[],[s767,s960]) ).
cnf(s963,plain,
spl12_88,
inference(rat,[],[s217,s912,s960]) ).
cnf(s964,plain,
~ spl12_4,
inference(rat,[],[s247,s961]) ).
cnf(s967,plain,
~ spl12_5,
inference(rat,[],[s3,s939]) ).
cnf(s968,plain,
~ spl12_3,
inference(rat,[],[s2,s964]) ).
cnf(s969,plain,
spl12_129,
inference(rat,[],[s42,s967,s925,s968]) ).
cnf(s970,plain,
spl12_64,
inference(rat,[],[s139,s912,s969]) ).
cnf(s971,plain,
~ spl12_72,
inference(rat,[],[s811,s970]) ).
cnf(s972,plain,
~ spl12_68,
inference(rat,[],[s809,s970]) ).
cnf(s973,plain,
~ spl12_96,
inference(rat,[],[s249,s970]) ).
cnf(s976,plain,
spl12_67,
inference(rat,[],[s943,s972]) ).
cnf(s977,plain,
spl12_94,
inference(rat,[],[s941,s973]) ).
cnf(s978,plain,
~ spl12_71,
inference(rat,[],[s822,s976]) ).
cnf(s981,plain,
spl12_218,
inference(rat,[],[s264,s976]) ).
cnf(s983,plain,
~ spl12_102,
inference(rat,[],[s245,s977]) ).
cnf(s984,plain,
spl12_70,
inference(rat,[],[s942,s971,s978]) ).
cnf(s985,plain,
spl12_101,
inference(rat,[],[s940,s983]) ).
cnf(s987,plain,
~ spl12_20,
inference(rat,[],[s541,s24,s552,s416,s93,s473,s477,s788,s956,s954,s777,s405,s887,s955,s529,s771,s772,s776,s946,s949]) ).
cnf(s988,plain,
~ spl12_18,
inference(rat,[],[s885,s699,s695,s93,s886,s696,s416,s568,s698,s694,s952,s24,s953,s669,s702,s477,s693,s370,s400,s483,s697,s954,s956,s951,s358,s398,s703,s863,s508,s799,s955,s887,s304,s325,s525,s528,s645,s89,s895,s896,s945,s890,s899,s907,s981,s919,s457,s409,s158,s985,s949,s923,s920,s977,s946,s921,s913,s914,s963,s970,s984]) ).
cnf(s990,plain,
spl12_17,
inference(rat,[],[s957,s987,s988]) ).
cnf(s991,plain,
~ spl12_57,
inference(rat,[],[s555,s990]) ).
cnf(s992,plain,
~ spl12_21,
inference(rat,[],[s382,s990]) ).
cnf(s993,plain,
~ spl12_158,
inference(rat,[],[s318,s990]) ).
cnf(s995,plain,
~ spl12_138,
inference(rat,[],[s24,s798,s568,s951,s886,s400,s404,s953,s591,s671,s946,s991,s993,s990]) ).
cnf(s996,plain,
spl12_181,
inference(rat,[],[s887,s995]) ).
cnf(s997,plain,
~ spl12_52,
inference(rat,[],[s799,s996]) ).
cnf(s1001,plain,
~ spl12_135,
inference(rat,[],[s425,s992,s996]) ).
cnf(s1002,plain,
spl12_49,
inference(rat,[],[s951,s997]) ).
cnf(s1004,plain,
$false,
inference(rat,[],[s507,s996,s1002,s1001]) ).
fof(f6173,plain,
$false,
inference(avatar_sat_refutation,[],[s1004]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG016+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n011.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 19:18:01 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.90/1.42 % (3682534)Detected formulas, will run a generic FOF schedule.
% 4.90/1.42 % (3682545)dis-21_1_sil=8000:lcm=predicate:random_seed=326757797:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.90/1.42 % (3682545)Refutation not found, incomplete strategy
% 4.90/1.42 % (3682545)------------------------------
% 4.90/1.42 % (3682545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.42 % (3682545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.42 % (3682545)CaDiCaL version: 2.1.3
% 4.90/1.42 % (3682545)Termination reason: Refutation not found, incomplete strategy
% 4.90/1.42 % (3682545)Time elapsed: 0.010 s
% 4.90/1.42 % (3682545)Peak memory usage: 89 MB
% 4.90/1.42 % (3682545)Instructions burned: 38 (million)
% 4.90/1.42 % (3682542)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4103513004:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.90/1.42 % (3682544)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=714537581:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.90/1.42 % (3682543)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2484473269:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.90/1.42 % (3682539)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1690099452:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.90/1.42 % (3682541)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=464418059:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.90/1.42 % (3682540)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=465901292:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.90/1.42 % (3682543)Instruction limit reached!
% 4.90/1.42 % (3682543)------------------------------
% 4.90/1.42 % (3682543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.42 % (3682543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.42 % (3682543)CaDiCaL version: 2.1.3
% 4.90/1.42 % (3682543)Termination reason: Instruction limit
% 4.90/1.42 % (3682543)Termination phase: Saturation
% 4.90/1.42 % (3682543)Time elapsed: 0.050 s
% 4.90/1.42 % (3682543)Peak memory usage: 88 MB
% 4.90/1.42 % (3682543)Instructions burned: 121 (million)
% 4.90/1.42 % (3682542)Instruction limit reached!
% 4.90/1.42 % (3682542)------------------------------
% 4.90/1.42 % (3682542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.42 % (3682542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.42 % (3682542)CaDiCaL version: 2.1.3
% 4.90/1.42 % (3682542)Termination reason: Instruction limit
% 4.90/1.42 % (3682542)Termination phase: Saturation
% 4.90/1.42 % (3682542)Time elapsed: 0.050 s
% 4.90/1.42 % (3682542)Peak memory usage: 90 MB
% 4.90/1.42 % (3682542)Instructions burned: 110 (million)
% 4.90/1.42 % (3682544)Instruction limit reached!
% 4.90/1.42 % (3682544)------------------------------
% 4.90/1.42 % (3682544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.42 % (3682544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.42 % (3682544)CaDiCaL version: 2.1.3
% 4.90/1.42 % (3682544)Termination reason: Instruction limit
% 4.90/1.42 % (3682544)Termination phase: Saturation
% 4.90/1.42 % (3682544)Time elapsed: 0.072 s
% 4.90/1.42 % (3682544)Peak memory usage: 89 MB
% 4.90/1.42 % (3682544)Instructions burned: 140 (million)
% 4.90/1.42 % (3682545)------------------------------
% 4.90/1.42 % (3682545)------------------------------
% 4.90/1.42 % (3682554)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1504281913:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.90/1.42 % (3682553)lrs+10_1_sil=8000:sp=occurrence:random_seed=3925448662:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 4.90/1.42 % (3682555)lrs+1011_1_sil=32000:sp=occurrence:random_seed=539397827:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 4.90/1.42 % (3682556)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=606367481:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 4.90/1.42 % (3682554)Instruction limit reached!
% 4.90/1.42 % (3682554)------------------------------
% 4.90/1.42 % (3682554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.42 % (3682554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.42 % (3682554)CaDiCaL version: 2.1.3
% 4.90/1.42 % (3682554)Termination reason: Instruction limit
% 4.90/1.42 % (3682554)Termination phase: Saturation
% 4.90/1.42 % (3682554)Time elapsed: 0.079 s
% 4.90/1.42 % (3682554)Peak memory usage: 89 MB
% 4.90/1.42 % (3682554)Instructions burned: 158 (million)
% 4.90/1.42 % (3682553)First to succeed.
% 4.90/1.42 % (3682555)Also succeeded, but the first one will report.
% 4.90/1.42 % (3682556)Instruction limit reached!
% 4.90/1.42 % (3682556)------------------------------
% 4.90/1.42 % (3682556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.42 % (3682556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.42 % (3682556)CaDiCaL version: 2.1.3
% 4.90/1.42 % (3682556)Termination reason: Instruction limit
% 4.90/1.42 % (3682556)Termination phase: Saturation
% 4.90/1.42 % (3682556)Time elapsed: 0.077 s
% 4.90/1.42 % (3682556)Peak memory usage: 91 MB
% 4.90/1.42 % (3682556)Instructions burned: 250 (million)
% 4.90/1.42 % (3682553)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3682534"
% 4.90/1.42 [W928 19:18:02.742202087 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742238014 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742274384 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742267667 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742288417 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742292157 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742316424 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742326074 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742328958 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742339144 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742367591 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742378241 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742417571 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742442254 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742480781 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742493211 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742521094 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 [W928 19:18:02.742536464 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.90/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.90/1.42 % (3682562)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3407971810:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 4.90/1.42 % (3682561)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=103519595:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 4.90/1.42 % (3682561)Instruction limit reached!
% 4.90/1.42 % (3682561)------------------------------
% 4.90/1.42 % (3682561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.42 % (3682561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.42 % (3682561)CaDiCaL version: 2.1.3
% 4.90/1.42 % (3682561)Termination reason: Instruction limit
% 4.90/1.42 % (3682561)Termination phase: Saturation
% 4.90/1.42 % (3682561)Time elapsed: 0.106 s
% 4.90/1.42 % (3682561)Peak memory usage: 89 MB
% 4.90/1.42 % (3682561)Instructions burned: 294 (million)
% 4.90/1.42 % (3682553)Refutation found. Thanks to Tanya!
% 4.90/1.42 % SZS status Theorem for theBenchmark
% 4.90/1.42 % SZS output start Proof for theBenchmark
% See solution above
% 5.94/1.61 % (3682553)------------------------------
% 5.94/1.61 % (3682553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.94/1.61 % (3682553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.61 % (3682553)CaDiCaL version: 2.1.3
% 5.94/1.61 % (3682553)Termination reason: Refutation
% 5.94/1.61 % (3682553)Time elapsed: 0.112 s
% 5.94/1.61 % (3682553)Peak memory usage: 91 MB
% 5.94/1.61 % (3682553)Instructions burned: 224 (million)
% 5.94/1.61 % (3682553)------------------------------
% 5.94/1.61 % (3682553)------------------------------
% 5.94/1.61 % (3682534)Success in time 0.752 s
% 5.94/1.61 % Vampire exiting
%------------------------------------------------------------------------------