%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG121+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:23:04 AM UTC 2026
% Result : Theorem 0.76s 0.40s
% Output : Refutation 0.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 130
% Syntax : Number of formulae : 863 ( 163 unt; 115 def)
% Number of atoms : 3234 (1535 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 3879 (1508 ~;1761 |; 495 &)
% ( 115 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 119 ( 117 usr; 118 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(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(f2,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e11) = e10
| op1(e10,e12) = e10
| op1(e10,e13) = e10 )
& ( op1(e10,e10) = e10
| op1(e11,e10) = e10
| op1(e12,e10) = e10
| op1(e13,e10) = e10 )
& ( op1(e10,e10) = e11
| op1(e10,e11) = e11
| op1(e10,e12) = e11
| op1(e10,e13) = e11 )
& ( op1(e10,e10) = e11
| op1(e11,e10) = e11
| op1(e12,e10) = e11
| op1(e13,e10) = e11 )
& ( op1(e10,e10) = e12
| op1(e10,e11) = e12
| op1(e10,e12) = e12
| op1(e10,e13) = e12 )
& ( op1(e10,e10) = e12
| op1(e11,e10) = e12
| op1(e12,e10) = e12
| op1(e13,e10) = e12 )
& ( op1(e10,e10) = e13
| op1(e10,e11) = e13
| op1(e10,e12) = e13
| op1(e10,e13) = e13 )
& ( op1(e10,e10) = e13
| op1(e11,e10) = e13
| op1(e12,e10) = e13
| op1(e13,e10) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e11) = e10
| op1(e11,e12) = e10
| op1(e11,e13) = e10 )
& ( op1(e10,e11) = e10
| op1(e11,e11) = e10
| op1(e12,e11) = e10
| op1(e13,e11) = e10 )
& ( op1(e11,e10) = e11
| op1(e11,e11) = e11
| op1(e11,e12) = e11
| op1(e11,e13) = e11 )
& ( op1(e10,e11) = e11
| op1(e11,e11) = e11
| op1(e12,e11) = e11
| op1(e13,e11) = e11 )
& ( op1(e11,e10) = e12
| op1(e11,e11) = e12
| op1(e11,e12) = e12
| op1(e11,e13) = e12 )
& ( op1(e10,e11) = e12
| op1(e11,e11) = e12
| op1(e12,e11) = e12
| op1(e13,e11) = e12 )
& ( op1(e11,e10) = e13
| op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e11,e13) = e13 )
& ( op1(e10,e11) = e13
| op1(e11,e11) = e13
| op1(e12,e11) = e13
| op1(e13,e11) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e11) = e10
| op1(e12,e12) = e10
| op1(e12,e13) = e10 )
& ( op1(e10,e12) = e10
| op1(e11,e12) = e10
| op1(e12,e12) = e10
| op1(e13,e12) = e10 )
& ( op1(e12,e10) = e11
| op1(e12,e11) = e11
| op1(e12,e12) = e11
| op1(e12,e13) = e11 )
& ( op1(e10,e12) = e11
| op1(e11,e12) = e11
| op1(e12,e12) = e11
| op1(e13,e12) = e11 )
& ( op1(e12,e10) = e12
| op1(e12,e11) = e12
| op1(e12,e12) = e12
| op1(e12,e13) = e12 )
& ( op1(e10,e12) = e12
| op1(e11,e12) = e12
| op1(e12,e12) = e12
| op1(e13,e12) = e12 )
& ( op1(e12,e10) = e13
| op1(e12,e11) = e13
| op1(e12,e12) = e13
| op1(e12,e13) = e13 )
& ( op1(e10,e12) = e13
| op1(e11,e12) = e13
| op1(e12,e12) = e13
| op1(e13,e12) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10 )
& ( op1(e10,e13) = e10
| op1(e11,e13) = e10
| op1(e12,e13) = e10
| op1(e13,e13) = e10 )
& ( op1(e13,e10) = e11
| op1(e13,e11) = e11
| op1(e13,e12) = e11
| op1(e13,e13) = e11 )
& ( op1(e10,e13) = e11
| op1(e11,e13) = e11
| op1(e12,e13) = e11
| op1(e13,e13) = e11 )
& ( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12
| op1(e13,e13) = e12 )
& ( op1(e10,e13) = e12
| op1(e11,e13) = e12
| op1(e12,e13) = e12
| op1(e13,e13) = e12 )
& ( op1(e13,e10) = e13
| op1(e13,e11) = e13
| op1(e13,e12) = e13
| op1(e13,e13) = e13 )
& ( op1(e10,e13) = e13
| op1(e11,e13) = e13
| op1(e12,e13) = e13
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f4,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e22) = e20
| op2(e20,e23) = e20 )
& ( op2(e20,e20) = e20
| op2(e21,e20) = e20
| op2(e22,e20) = e20
| op2(e23,e20) = e20 )
& ( op2(e20,e20) = e21
| op2(e20,e21) = e21
| op2(e20,e22) = e21
| op2(e20,e23) = e21 )
& ( op2(e20,e20) = e21
| op2(e21,e20) = e21
| op2(e22,e20) = e21
| op2(e23,e20) = e21 )
& ( op2(e20,e20) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 )
& ( op2(e20,e20) = e22
| op2(e21,e20) = e22
| op2(e22,e20) = e22
| op2(e23,e20) = e22 )
& ( op2(e20,e20) = e23
| op2(e20,e21) = e23
| op2(e20,e22) = e23
| op2(e20,e23) = e23 )
& ( op2(e20,e20) = e23
| op2(e21,e20) = e23
| op2(e22,e20) = e23
| op2(e23,e20) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e21) = e20
| op2(e21,e22) = e20
| op2(e21,e23) = e20 )
& ( op2(e20,e21) = e20
| op2(e21,e21) = e20
| op2(e22,e21) = e20
| op2(e23,e21) = e20 )
& ( op2(e21,e20) = e21
| op2(e21,e21) = e21
| op2(e21,e22) = e21
| op2(e21,e23) = e21 )
& ( op2(e20,e21) = e21
| op2(e21,e21) = e21
| op2(e22,e21) = e21
| op2(e23,e21) = e21 )
& ( op2(e21,e20) = e22
| op2(e21,e21) = e22
| op2(e21,e22) = e22
| op2(e21,e23) = e22 )
& ( op2(e20,e21) = e22
| op2(e21,e21) = e22
| op2(e22,e21) = e22
| op2(e23,e21) = e22 )
& ( op2(e21,e20) = e23
| op2(e21,e21) = e23
| op2(e21,e22) = e23
| op2(e21,e23) = e23 )
& ( op2(e20,e21) = e23
| op2(e21,e21) = e23
| op2(e22,e21) = e23
| op2(e23,e21) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e21) = e20
| op2(e22,e22) = e20
| op2(e22,e23) = e20 )
& ( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e22,e22) = e20
| op2(e23,e22) = e20 )
& ( op2(e22,e20) = e21
| op2(e22,e21) = e21
| op2(e22,e22) = e21
| op2(e22,e23) = e21 )
& ( op2(e20,e22) = e21
| op2(e21,e22) = e21
| op2(e22,e22) = e21
| op2(e23,e22) = e21 )
& ( op2(e22,e20) = e22
| op2(e22,e21) = e22
| op2(e22,e22) = e22
| op2(e22,e23) = e22 )
& ( op2(e20,e22) = e22
| op2(e21,e22) = e22
| op2(e22,e22) = e22
| op2(e23,e22) = e22 )
& ( op2(e22,e20) = e23
| op2(e22,e21) = e23
| op2(e22,e22) = e23
| op2(e22,e23) = e23 )
& ( op2(e20,e22) = e23
| op2(e21,e22) = e23
| op2(e22,e22) = e23
| op2(e23,e22) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e23) = e20 )
& ( op2(e20,e23) = e20
| op2(e21,e23) = e20
| op2(e22,e23) = e20
| op2(e23,e23) = e20 )
& ( op2(e23,e20) = e21
| op2(e23,e21) = e21
| op2(e23,e22) = e21
| op2(e23,e23) = e21 )
& ( op2(e20,e23) = e21
| op2(e21,e23) = e21
| op2(e22,e23) = e21
| op2(e23,e23) = e21 )
& ( op2(e23,e20) = e22
| op2(e23,e21) = e22
| op2(e23,e22) = e22
| op2(e23,e23) = e22 )
& ( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22
| op2(e23,e23) = e22 )
& ( op2(e23,e20) = e23
| op2(e23,e21) = e23
| op2(e23,e22) = e23
| op2(e23,e23) = e23 )
& ( op2(e20,e23) = e23
| op2(e21,e23) = e23
| op2(e22,e23) = e23
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op1(e10,e10) != op1(e11,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e12,e10) != op1(e13,e10)
& op1(e10,e11) != op1(e11,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e12,e11) != op1(e13,e11)
& op1(e10,e12) != op1(e11,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e12,e12) != op1(e13,e12)
& op1(e10,e13) != op1(e11,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e12,e13) != op1(e13,e13)
& op1(e10,e10) != op1(e10,e11)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e12) != op1(e10,e13)
& op1(e11,e10) != op1(e11,e11)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e12) != op1(e11,e13)
& op1(e12,e10) != op1(e12,e11)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e12) != op1(e12,e13)
& op1(e13,e10) != op1(e13,e11)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e12) != op1(e13,e13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( op2(e20,e20) != op2(e21,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e22,e20) != op2(e23,e20)
& op2(e20,e21) != op2(e21,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e22,e21) != op2(e23,e21)
& op2(e20,e22) != op2(e21,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e22,e22) != op2(e23,e22)
& op2(e20,e23) != op2(e21,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e22,e23) != op2(e23,e23)
& op2(e20,e20) != op2(e20,e21)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e22) != op2(e20,e23)
& op2(e21,e20) != op2(e21,e21)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e22) != op2(e21,e23)
& op2(e22,e20) != op2(e22,e21)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e22) != op2(e22,e23)
& op2(e23,e20) != op2(e23,e21)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e22) != op2(e23,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f10,axiom,
( ( op1(e10,e10) = e10
| op1(e11,e11) = e11
| op1(e12,e12) = e12
| op1(e13,e13) = e13 )
& ( op1(e10,e10) != e10
| op1(e10,e10) = e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) = e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) = e10 )
& ( op1(e10,e10) != e13
| op1(e10,e13) = e10 )
& ( op1(e11,e11) != e10
| op1(e11,e10) = e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) = e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) = e11 )
& ( op1(e11,e11) != e13
| op1(e11,e13) = e11 )
& ( op1(e12,e12) != e10
| op1(e12,e10) = e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) = e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) = e12 )
& ( op1(e12,e12) != e13
| op1(e12,e13) = e12 )
& ( op1(e13,e13) != e10
| op1(e13,e10) = e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) = e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) = e13 )
& ( op1(e13,e13) != e13
| op1(e13,e13) = e13 )
& ( ( op1(e10,e10) = e10
& op1(e10,e10) = e10
& op1(e10,e10) != e10 )
| ( op1(e10,e11) = e10
& op1(e11,e10) = e10
& op1(e11,e11) != e11 )
| ( op1(e10,e12) = e10
& op1(e12,e10) = e10
& op1(e12,e12) != e12 )
| ( op1(e10,e13) = e10
& op1(e13,e10) = e10
& op1(e13,e13) != e13 )
| ( op1(e11,e10) = e11
& op1(e10,e11) = e11
& op1(e10,e10) != e10 )
| ( op1(e11,e11) = e11
& op1(e11,e11) = e11
& op1(e11,e11) != e11 )
| ( op1(e11,e12) = e11
& op1(e12,e11) = e11
& op1(e12,e12) != e12 )
| ( op1(e11,e13) = e11
& op1(e13,e11) = e11
& op1(e13,e13) != e13 )
| ( op1(e12,e10) = e12
& op1(e10,e12) = e12
& op1(e10,e10) != e10 )
| ( op1(e12,e11) = e12
& op1(e11,e12) = e12
& op1(e11,e11) != e11 )
| ( op1(e12,e12) = e12
& op1(e12,e12) = e12
& op1(e12,e12) != e12 )
| ( op1(e12,e13) = e12
& op1(e13,e12) = e12
& op1(e13,e13) != e13 )
| ( op1(e13,e10) = e13
& op1(e10,e13) = e13
& op1(e10,e10) != e10 )
| ( op1(e13,e11) = e13
& op1(e11,e13) = e13
& op1(e11,e11) != e11 )
| ( op1(e13,e12) = e13
& op1(e12,e13) = e13
& op1(e12,e12) != e12 )
| ( op1(e13,e13) = e13
& op1(e13,e13) = e13
& op1(e13,e13) != e13 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( ( op2(e20,e20) = e20
| op2(e21,e21) = e21
| op2(e22,e22) = e22
| op2(e23,e23) = e23 )
& ( op2(e20,e20) != e20
| op2(e20,e20) = e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) = e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) = e20 )
& ( op2(e20,e20) != e23
| op2(e20,e23) = e20 )
& ( op2(e21,e21) != e20
| op2(e21,e20) = e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) = e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) = e21 )
& ( op2(e21,e21) != e23
| op2(e21,e23) = e21 )
& ( op2(e22,e22) != e20
| op2(e22,e20) = e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) = e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) = e22 )
& ( op2(e22,e22) != e23
| op2(e22,e23) = e22 )
& ( op2(e23,e23) != e20
| op2(e23,e20) = e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) = e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) = e23 )
& ( op2(e23,e23) != e23
| op2(e23,e23) = e23 )
& ( ( op2(e20,e20) = e20
& op2(e20,e20) = e20
& op2(e20,e20) != e20 )
| ( op2(e20,e21) = e20
& op2(e21,e20) = e20
& op2(e21,e21) != e21 )
| ( op2(e20,e22) = e20
& op2(e22,e20) = e20
& op2(e22,e22) != e22 )
| ( op2(e20,e23) = e20
& op2(e23,e20) = e20
& op2(e23,e23) != e23 )
| ( op2(e21,e20) = e21
& op2(e20,e21) = e21
& op2(e20,e20) != e20 )
| ( op2(e21,e21) = e21
& op2(e21,e21) = e21
& op2(e21,e21) != e21 )
| ( op2(e21,e22) = e21
& op2(e22,e21) = e21
& op2(e22,e22) != e22 )
| ( op2(e21,e23) = e21
& op2(e23,e21) = e21
& op2(e23,e23) != e23 )
| ( op2(e22,e20) = e22
& op2(e20,e22) = e22
& op2(e20,e20) != e20 )
| ( op2(e22,e21) = e22
& op2(e21,e22) = e22
& op2(e21,e21) != e21 )
| ( op2(e22,e22) = e22
& op2(e22,e22) = e22
& op2(e22,e22) != e22 )
| ( op2(e22,e23) = e22
& op2(e23,e22) = e22
& op2(e23,e23) != e23 )
| ( op2(e23,e20) = e23
& op2(e20,e23) = e23
& op2(e20,e20) != e20 )
| ( op2(e23,e21) = e23
& op2(e21,e23) = e23
& op2(e21,e21) != e21 )
| ( op2(e23,e22) = e23
& op2(e22,e23) = e23
& op2(e22,e22) != e22 )
| ( op2(e23,e23) = e23
& op2(e23,e23) = e23
& op2(e23,e23) != e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e10 = op1(e13,e13)
& e11 = op1(op1(e13,e13),op1(e13,e13))
& e12 = op1(op1(op1(e13,e13),op1(e13,e13)),e13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e20 = op2(e23,e23)
& e21 = op2(op2(e23,e23),op2(e23,e23))
& e22 = op2(op2(op2(e23,e23),op2(e23,e23)),e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( h1(e13) = e20
& h1(e10) = op2(e20,e20)
& h1(e11) = op2(op2(e20,e20),op2(e20,e20))
& h1(e12) = op2(op2(op2(e20,e20),op2(e20,e20)),e20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f16,axiom,
( h3(e13) = e22
& h3(e10) = op2(e22,e22)
& h3(e11) = op2(op2(e22,e22),op2(e22,e22))
& h3(e12) = op2(op2(op2(e22,e22),op2(e22,e22)),e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
( h4(e13) = e23
& h4(e10) = op2(e23,e23)
& h4(e11) = op2(op2(e23,e23),op2(e23,e23))
& h4(e12) = op2(op2(op2(e23,e23),op2(e23,e23)),e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f18,conjecture,
( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f19,negated_conjecture,
~ ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f20,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) ) )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) ) )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) ) )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) ) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f23,plain,
( e13 = op1(e10,e12)
| e12 = op1(e10,e12)
| e11 = op1(e10,e12)
| e10 = op1(e10,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f24,plain,
( e13 = op1(e10,e13)
| e12 = op1(e10,e13)
| e11 = op1(e10,e13)
| e10 = op1(e10,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f37,plain,
( e10 = op1(e10,e13)
| e10 = op1(e10,e12)
| e10 = op1(e10,e11)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f38,plain,
( e10 = op1(e13,e10)
| e10 = op1(e12,e10)
| e10 = op1(e11,e10)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f42,plain,
( e12 = op1(e13,e10)
| e12 = op1(e12,e10)
| e12 = op1(e11,e10)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f2]) ).
fof(f47,plain,
( e11 = op1(e11,e13)
| e11 = op1(e11,e12)
| e11 = op1(e11,e11)
| e11 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f53,plain,
( e10 = op1(e12,e13)
| e10 = op1(e12,e12)
| e10 = op1(e12,e11)
| e10 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f56,plain,
( e11 = op1(e13,e12)
| e11 = op1(e12,e12)
| e11 = op1(e11,e12)
| e11 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f59,plain,
( e13 = op1(e12,e13)
| e13 = op1(e12,e12)
| e13 = op1(e12,e11)
| e13 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f60,plain,
( e13 = op1(e13,e12)
| e13 = op1(e12,e12)
| e13 = op1(e11,e12)
| e13 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f64,plain,
( e11 = op1(e13,e13)
| e11 = op1(e12,e13)
| e11 = op1(e11,e13)
| e11 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f65,plain,
( e12 = op1(e13,e13)
| e12 = op1(e13,e12)
| e12 = op1(e13,e11)
| e12 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f89,plain,
( e22 = op2(e20,e23)
| e22 = op2(e20,e22)
| e22 = op2(e20,e21)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f4]) ).
fof(f90,plain,
( e22 = op2(e23,e20)
| e22 = op2(e22,e20)
| e22 = op2(e21,e20)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f4]) ).
fof(f91,plain,
( e23 = op2(e20,e23)
| e23 = op2(e20,e22)
| e23 = op2(e20,e21)
| op2(e20,e20) = e23 ),
inference(cnf_transformation,[],[f4]) ).
fof(f93,plain,
( e20 = op2(e21,e23)
| e20 = op2(e21,e22)
| e20 = op2(e21,e21)
| e20 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f99,plain,
( e23 = op2(e21,e23)
| e23 = op2(e21,e22)
| e23 = op2(e21,e21)
| e23 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f100,plain,
( e23 = op2(e23,e21)
| e23 = op2(e22,e21)
| e23 = op2(e21,e21)
| e23 = op2(e20,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f102,plain,
( e20 = op2(e23,e22)
| e20 = op2(e22,e22)
| e20 = op2(e21,e22)
| e20 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f104,plain,
( e21 = op2(e23,e22)
| e21 = op2(e22,e22)
| e21 = op2(e21,e22)
| e21 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f106,plain,
( e22 = op2(e23,e22)
| e22 = op2(e22,e22)
| e22 = op2(e21,e22)
| e22 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f112,plain,
( e21 = op2(e23,e23)
| e21 = op2(e22,e23)
| e21 = op2(e21,e23)
| e21 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f113,plain,
( e22 = op2(e23,e23)
| e22 = op2(e23,e22)
| e22 = op2(e23,e21)
| e22 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f116,plain,
( e23 = op2(e23,e23)
| e23 = op2(e22,e23)
| e23 = op2(e21,e23)
| e23 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f121,plain,
op1(e13,e10) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f123,plain,
op1(e12,e12) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f126,plain,
op1(e12,e10) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f132,plain,
op1(e11,e10) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f135,plain,
op1(e10,e12) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f138,plain,
op1(e10,e10) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f139,plain,
op1(e10,e10) != op1(e10,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f141,plain,
op1(e12,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f144,plain,
op1(e10,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f145,plain,
op1(e10,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f146,plain,
op1(e10,e13) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f151,plain,
op1(e10,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f159,plain,
op1(e12,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f165,plain,
op2(e23,e22) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f172,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f186,plain,
op2(e20,e20) != op2(e20,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f187,plain,
op2(e20,e20) != op2(e20,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f195,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f208,plain,
op2(e21,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f213,plain,
e12 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f214,plain,
e11 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f215,plain,
e11 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f216,plain,
e10 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f217,plain,
e10 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f218,plain,
e10 != e11,
inference(cnf_transformation,[],[f7]) ).
fof(f219,plain,
e22 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f221,plain,
e21 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f222,plain,
e20 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f223,plain,
e20 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f224,plain,
e20 != e21,
inference(cnf_transformation,[],[f8]) ).
fof(f301,plain,
( e12 = op1(e12,e13)
| e13 != op1(e12,e12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f302,plain,
( e13 = op1(e13,e10)
| e10 != op1(e13,e13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f356,plain,
( e23 = op2(e23,e23)
| e22 = op2(e22,e22)
| e21 = op2(e21,e21)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f11]) ).
fof(f357,plain,
( e20 = op2(e20,e21)
| op2(e20,e20) != e21 ),
inference(cnf_transformation,[],[f11]) ).
fof(f362,plain,
( e21 = op2(e21,e23)
| e23 != op2(e21,e21) ),
inference(cnf_transformation,[],[f11]) ).
fof(f366,plain,
( e23 = op2(e23,e20)
| e20 != op2(e23,e23) ),
inference(cnf_transformation,[],[f11]) ).
fof(f367,plain,
( e23 = op2(e23,e21)
| e21 != op2(e23,e23) ),
inference(cnf_transformation,[],[f11]) ).
fof(f369,plain,
e12 = op1(op1(op1(e13,e13),op1(e13,e13)),e13),
inference(cnf_transformation,[],[f12]) ).
fof(f370,plain,
e11 = op1(op1(e13,e13),op1(e13,e13)),
inference(cnf_transformation,[],[f12]) ).
fof(f371,plain,
e10 = op1(e13,e13),
inference(cnf_transformation,[],[f12]) ).
fof(f372,plain,
e22 = op2(op2(op2(e23,e23),op2(e23,e23)),e23),
inference(cnf_transformation,[],[f13]) ).
fof(f373,plain,
e21 = op2(op2(e23,e23),op2(e23,e23)),
inference(cnf_transformation,[],[f13]) ).
fof(f374,plain,
e20 = op2(e23,e23),
inference(cnf_transformation,[],[f13]) ).
fof(f378,plain,
e20 = h1(e13),
inference(cnf_transformation,[],[f14]) ).
fof(f383,plain,
h3(e12) = op2(op2(op2(e22,e22),op2(e22,e22)),e22),
inference(cnf_transformation,[],[f16]) ).
fof(f384,plain,
h3(e11) = op2(op2(e22,e22),op2(e22,e22)),
inference(cnf_transformation,[],[f16]) ).
fof(f385,plain,
op2(e22,e22) = h3(e10),
inference(cnf_transformation,[],[f16]) ).
fof(f386,plain,
e22 = h3(e13),
inference(cnf_transformation,[],[f16]) ).
fof(f390,plain,
e23 = h4(e13),
inference(cnf_transformation,[],[f17]) ).
fof(f410,plain,
( e20 != h3(e10)
| ~ sP31 ),
inference(cnf_transformation,[],[f20]) ).
fof(f413,plain,
( e21 != h3(e11)
| ~ sP30 ),
inference(cnf_transformation,[],[f20]) ).
fof(f463,plain,
( e23 != h3(e12)
| e22 != h3(e13)
| sP30
| sP31
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(cnf_transformation,[],[f20]) ).
fof(f567,plain,
( e23 != h3(e12)
| e22 != h3(e13)
| ~ sP30
| sP31
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(consistent_polarity_flipping,[],[f463]) ).
fof(f613,plain,
( e21 != h3(e11)
| sP30 ),
inference(consistent_polarity_flipping,[],[f413]) ).
fof(f629,definition,
( spl36_2
<=> e20 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl36_2])],[avatar_definition]) ).
fof(f630,plain,
( e20 = h1(e13)
| ~ spl36_2 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f653,definition,
( spl36_7
<=> e21 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl36_7])],[avatar_definition]) ).
fof(f654,plain,
( e21 = h1(e13)
| ~ spl36_7 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f655,plain,
( e21 != h1(e13)
| spl36_7 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f721,definition,
( spl36_21
<=> sP31 ),
introduced(definition,[new_symbols(definition,[spl36_21])],[avatar_definition]) ).
fof(f740,definition,
( spl36_25
<=> e20 = h3(e10) ),
introduced(definition,[new_symbols(definition,[spl36_25])],[avatar_definition]) ).
fof(f741,plain,
( e20 = h3(e10)
| ~ spl36_25 ),
inference(avatar_component_clause,[],[f740]) ).
fof(f743,plain,
( ~ spl36_21
| ~ spl36_25 ),
inference(avatar_split_clause,[],[f410,f740,f721]) ).
fof(f745,definition,
( spl36_26
<=> sP30 ),
introduced(definition,[new_symbols(definition,[spl36_26])],[avatar_definition]) ).
fof(f749,definition,
( spl36_27
<=> e21 = h3(e13) ),
introduced(definition,[new_symbols(definition,[spl36_27])],[avatar_definition]) ).
fof(f750,plain,
( e21 = h3(e13)
| ~ spl36_27 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f751,plain,
( e21 != h3(e13)
| spl36_27 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f759,definition,
( spl36_29
<=> e21 = h3(e11) ),
introduced(definition,[new_symbols(definition,[spl36_29])],[avatar_definition]) ).
fof(f760,plain,
( e21 = h3(e11)
| ~ spl36_29 ),
inference(avatar_component_clause,[],[f759]) ).
fof(f762,plain,
( spl36_26
| ~ spl36_29 ),
inference(avatar_split_clause,[],[f613,f759,f745]) ).
fof(f797,definition,
( spl36_37
<=> e21 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl36_37])],[avatar_definition]) ).
fof(f798,plain,
( e21 = h4(e13)
| ~ spl36_37 ),
inference(avatar_component_clause,[],[f797]) ).
fof(f799,plain,
( e21 != h4(e13)
| spl36_37 ),
inference(avatar_component_clause,[],[f797]) ).
fof(f1041,definition,
( spl36_89
<=> h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl36_89])],[avatar_definition]) ).
fof(f1043,plain,
( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| spl36_89 ),
inference(avatar_component_clause,[],[f1041]) ).
fof(f1045,definition,
( spl36_90
<=> h3(op1(e10,e11)) = op2(h3(e10),h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl36_90])],[avatar_definition]) ).
fof(f1047,plain,
( h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| spl36_90 ),
inference(avatar_component_clause,[],[f1045]) ).
fof(f1049,definition,
( spl36_91
<=> h3(op1(e10,e12)) = op2(h3(e10),h3(e12)) ),
introduced(definition,[new_symbols(definition,[spl36_91])],[avatar_definition]) ).
fof(f1051,plain,
( h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| spl36_91 ),
inference(avatar_component_clause,[],[f1049]) ).
fof(f1053,definition,
( spl36_92
<=> h3(op1(e10,e13)) = op2(h3(e10),h3(e13)) ),
introduced(definition,[new_symbols(definition,[spl36_92])],[avatar_definition]) ).
fof(f1055,plain,
( h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| spl36_92 ),
inference(avatar_component_clause,[],[f1053]) ).
fof(f1057,definition,
( spl36_93
<=> h3(op1(e11,e10)) = op2(h3(e11),h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl36_93])],[avatar_definition]) ).
fof(f1059,plain,
( h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| spl36_93 ),
inference(avatar_component_clause,[],[f1057]) ).
fof(f1061,definition,
( spl36_94
<=> h3(op1(e11,e11)) = op2(h3(e11),h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl36_94])],[avatar_definition]) ).
fof(f1063,plain,
( h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| spl36_94 ),
inference(avatar_component_clause,[],[f1061]) ).
fof(f1065,definition,
( spl36_95
<=> h3(op1(e11,e12)) = op2(h3(e11),h3(e12)) ),
introduced(definition,[new_symbols(definition,[spl36_95])],[avatar_definition]) ).
fof(f1067,plain,
( h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| spl36_95 ),
inference(avatar_component_clause,[],[f1065]) ).
fof(f1069,definition,
( spl36_96
<=> h3(op1(e11,e13)) = op2(h3(e11),h3(e13)) ),
introduced(definition,[new_symbols(definition,[spl36_96])],[avatar_definition]) ).
fof(f1071,plain,
( h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| spl36_96 ),
inference(avatar_component_clause,[],[f1069]) ).
fof(f1073,definition,
( spl36_97
<=> h3(op1(e12,e10)) = op2(h3(e12),h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl36_97])],[avatar_definition]) ).
fof(f1075,plain,
( h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| spl36_97 ),
inference(avatar_component_clause,[],[f1073]) ).
fof(f1077,definition,
( spl36_98
<=> h3(op1(e12,e11)) = op2(h3(e12),h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl36_98])],[avatar_definition]) ).
fof(f1079,plain,
( h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| spl36_98 ),
inference(avatar_component_clause,[],[f1077]) ).
fof(f1081,definition,
( spl36_99
<=> h3(op1(e12,e12)) = op2(h3(e12),h3(e12)) ),
introduced(definition,[new_symbols(definition,[spl36_99])],[avatar_definition]) ).
fof(f1083,plain,
( h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| spl36_99 ),
inference(avatar_component_clause,[],[f1081]) ).
fof(f1085,definition,
( spl36_100
<=> h3(op1(e12,e13)) = op2(h3(e12),h3(e13)) ),
introduced(definition,[new_symbols(definition,[spl36_100])],[avatar_definition]) ).
fof(f1087,plain,
( h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| spl36_100 ),
inference(avatar_component_clause,[],[f1085]) ).
fof(f1089,definition,
( spl36_101
<=> h3(op1(e13,e10)) = op2(h3(e13),h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl36_101])],[avatar_definition]) ).
fof(f1091,plain,
( h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| spl36_101 ),
inference(avatar_component_clause,[],[f1089]) ).
fof(f1093,definition,
( spl36_102
<=> h3(op1(e13,e11)) = op2(h3(e13),h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl36_102])],[avatar_definition]) ).
fof(f1095,plain,
( h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| spl36_102 ),
inference(avatar_component_clause,[],[f1093]) ).
fof(f1097,definition,
( spl36_103
<=> h3(op1(e13,e12)) = op2(h3(e13),h3(e12)) ),
introduced(definition,[new_symbols(definition,[spl36_103])],[avatar_definition]) ).
fof(f1099,plain,
( h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| spl36_103 ),
inference(avatar_component_clause,[],[f1097]) ).
fof(f1101,definition,
( spl36_104
<=> h3(op1(e13,e13)) = op2(h3(e13),h3(e13)) ),
introduced(definition,[new_symbols(definition,[spl36_104])],[avatar_definition]) ).
fof(f1103,plain,
( h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| spl36_104 ),
inference(avatar_component_clause,[],[f1101]) ).
fof(f1105,definition,
( spl36_105
<=> e22 = h3(e13) ),
introduced(definition,[new_symbols(definition,[spl36_105])],[avatar_definition]) ).
fof(f1106,plain,
( e22 = h3(e13)
| ~ spl36_105 ),
inference(avatar_component_clause,[],[f1105]) ).
fof(f1137,definition,
( spl36_111
<=> e23 = h3(e12) ),
introduced(definition,[new_symbols(definition,[spl36_111])],[avatar_definition]) ).
fof(f1138,plain,
( e23 = h3(e12)
| ~ spl36_111 ),
inference(avatar_component_clause,[],[f1137]) ).
fof(f1140,plain,
( ~ spl36_89
| ~ spl36_90
| ~ spl36_91
| ~ spl36_92
| ~ spl36_93
| ~ spl36_94
| ~ spl36_95
| ~ spl36_96
| ~ spl36_97
| ~ spl36_98
| ~ spl36_99
| ~ spl36_100
| ~ spl36_101
| ~ spl36_102
| ~ spl36_103
| ~ spl36_104
| spl36_21
| ~ spl36_26
| ~ spl36_105
| ~ spl36_111 ),
inference(avatar_split_clause,[],[f567,f1137,f1105,f745,f721,f1101,f1097,f1093,f1089,f1085,f1081,f1077,f1073,f1069,f1065,f1061,f1057,f1053,f1049,f1045,f1041]) ).
fof(f1257,definition,
( spl36_136
<=> e23 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl36_136])],[avatar_definition]) ).
fof(f1258,plain,
( e23 = h4(e13)
| ~ spl36_136 ),
inference(avatar_component_clause,[],[f1257]) ).
fof(f1264,plain,
spl36_136,
inference(avatar_split_clause,[],[f390,f1257]) ).
fof(f1265,plain,
spl36_105,
inference(avatar_split_clause,[],[f386,f1105]) ).
fof(f1267,plain,
spl36_2,
inference(avatar_split_clause,[],[f378,f629]) ).
fof(f1273,definition,
( spl36_138
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl36_138])],[avatar_definition]) ).
fof(f1274,plain,
( e20 = op2(e20,e20)
| ~ spl36_138 ),
inference(avatar_component_clause,[],[f1273]) ).
fof(f1284,definition,
( spl36_140
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl36_140])],[avatar_definition]) ).
fof(f1285,plain,
( e21 = op2(e21,e21)
| ~ spl36_140 ),
inference(avatar_component_clause,[],[f1284]) ).
fof(f1289,definition,
( spl36_141
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl36_141])],[avatar_definition]) ).
fof(f1291,plain,
( e20 = op2(e21,e20)
| ~ spl36_141 ),
inference(avatar_component_clause,[],[f1289]) ).
fof(f1294,definition,
( spl36_142
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl36_142])],[avatar_definition]) ).
fof(f1296,plain,
( e20 = op2(e20,e21)
| ~ spl36_142 ),
inference(avatar_component_clause,[],[f1294]) ).
fof(f1303,definition,
( spl36_144
<=> e22 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl36_144])],[avatar_definition]) ).
fof(f1304,plain,
( e22 = op2(e22,e22)
| ~ spl36_144 ),
inference(avatar_component_clause,[],[f1303]) ).
fof(f1313,definition,
( spl36_146
<=> e20 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl36_146])],[avatar_definition]) ).
fof(f1315,plain,
( e20 = op2(e20,e22)
| ~ spl36_146 ),
inference(avatar_component_clause,[],[f1313]) ).
fof(f1322,definition,
( spl36_148
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl36_148])],[avatar_definition]) ).
fof(f1323,plain,
( e23 = op2(e23,e23)
| ~ spl36_148 ),
inference(avatar_component_clause,[],[f1322]) ).
fof(f1369,definition,
( spl36_157
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl36_157])],[avatar_definition]) ).
fof(f1371,plain,
( e21 = op2(e21,e22)
| ~ spl36_157 ),
inference(avatar_component_clause,[],[f1369]) ).
fof(f1384,definition,
( spl36_160
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl36_160])],[avatar_definition]) ).
fof(f1386,plain,
( e21 = op2(e21,e23)
| ~ spl36_160 ),
inference(avatar_component_clause,[],[f1384]) ).
fof(f1394,definition,
( spl36_162
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl36_162])],[avatar_definition]) ).
fof(f1396,plain,
( e22 = op2(e20,e22)
| ~ spl36_162 ),
inference(avatar_component_clause,[],[f1394]) ).
fof(f1399,definition,
( spl36_163
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl36_163])],[avatar_definition]) ).
fof(f1401,plain,
( e22 = op2(e22,e20)
| ~ spl36_163 ),
inference(avatar_component_clause,[],[f1399]) ).
fof(f1409,definition,
( spl36_165
<=> e22 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl36_165])],[avatar_definition]) ).
fof(f1411,plain,
( e22 = op2(e21,e22)
| ~ spl36_165 ),
inference(avatar_component_clause,[],[f1409]) ).
fof(f1431,definition,
( spl36_169
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl36_169])],[avatar_definition]) ).
fof(f1433,plain,
( e22 = op2(e23,e22)
| ~ spl36_169 ),
inference(avatar_component_clause,[],[f1431]) ).
fof(f1446,definition,
( spl36_172
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl36_172])],[avatar_definition]) ).
fof(f1448,plain,
( e23 = op2(e20,e23)
| ~ spl36_172 ),
inference(avatar_component_clause,[],[f1446]) ).
fof(f1451,definition,
( spl36_173
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl36_173])],[avatar_definition]) ).
fof(f1453,plain,
( e23 = op2(e23,e20)
| ~ spl36_173 ),
inference(avatar_component_clause,[],[f1451]) ).
fof(f1461,definition,
( spl36_175
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl36_175])],[avatar_definition]) ).
fof(f1463,plain,
( e23 = op2(e21,e23)
| ~ spl36_175 ),
inference(avatar_component_clause,[],[f1461]) ).
fof(f1466,definition,
( spl36_176
<=> e23 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl36_176])],[avatar_definition]) ).
fof(f1468,plain,
( e23 = op2(e23,e21)
| ~ spl36_176 ),
inference(avatar_component_clause,[],[f1466]) ).
fof(f1472,definition,
( spl36_177
<=> e23 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl36_177])],[avatar_definition]) ).
fof(f1487,plain,
( spl36_138
| spl36_140
| spl36_144
| spl36_148 ),
inference(avatar_split_clause,[],[f356,f1322,f1303,f1284,f1273]) ).
fof(f1489,definition,
( spl36_179
<=> op2(e20,e20) = e21 ),
introduced(definition,[new_symbols(definition,[spl36_179])],[avatar_definition]) ).
fof(f1490,plain,
( op2(e20,e20) = e21
| ~ spl36_179 ),
inference(avatar_component_clause,[],[f1489]) ).
fof(f1492,plain,
( ~ spl36_179
| spl36_142 ),
inference(avatar_split_clause,[],[f357,f1294,f1489]) ).
fof(f1494,definition,
( spl36_180
<=> op2(e20,e20) = e22 ),
introduced(definition,[new_symbols(definition,[spl36_180])],[avatar_definition]) ).
fof(f1495,plain,
( op2(e20,e20) = e22
| ~ spl36_180 ),
inference(avatar_component_clause,[],[f1494]) ).
fof(f1499,definition,
( spl36_181
<=> op2(e20,e20) = e23 ),
introduced(definition,[new_symbols(definition,[spl36_181])],[avatar_definition]) ).
fof(f1500,plain,
( op2(e20,e20) = e23
| ~ spl36_181 ),
inference(avatar_component_clause,[],[f1499]) ).
fof(f1504,definition,
( spl36_182
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl36_182])],[avatar_definition]) ).
fof(f1505,plain,
( e20 = op2(e21,e21)
| ~ spl36_182 ),
inference(avatar_component_clause,[],[f1504]) ).
fof(f1506,plain,
( e20 != op2(e21,e21)
| spl36_182 ),
inference(avatar_component_clause,[],[f1504]) ).
fof(f1514,definition,
( spl36_184
<=> e23 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl36_184])],[avatar_definition]) ).
fof(f1517,plain,
( ~ spl36_184
| spl36_160 ),
inference(avatar_split_clause,[],[f362,f1384,f1514]) ).
fof(f1519,definition,
( spl36_185
<=> e20 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl36_185])],[avatar_definition]) ).
fof(f1520,plain,
( e20 = op2(e22,e22)
| ~ spl36_185 ),
inference(avatar_component_clause,[],[f1519]) ).
fof(f1524,definition,
( spl36_186
<=> e21 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl36_186])],[avatar_definition]) ).
fof(f1525,plain,
( e21 = op2(e22,e22)
| ~ spl36_186 ),
inference(avatar_component_clause,[],[f1524]) ).
fof(f1534,definition,
( spl36_188
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl36_188])],[avatar_definition]) ).
fof(f1535,plain,
( e20 = op2(e23,e23)
| ~ spl36_188 ),
inference(avatar_component_clause,[],[f1534]) ).
fof(f1537,plain,
( ~ spl36_188
| spl36_173 ),
inference(avatar_split_clause,[],[f366,f1451,f1534]) ).
fof(f1539,definition,
( spl36_189
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl36_189])],[avatar_definition]) ).
fof(f1542,plain,
( ~ spl36_189
| spl36_176 ),
inference(avatar_split_clause,[],[f367,f1466,f1539]) ).
fof(f1544,definition,
( spl36_190
<=> e22 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl36_190])],[avatar_definition]) ).
fof(f1545,plain,
( e22 = op2(e23,e23)
| ~ spl36_190 ),
inference(avatar_component_clause,[],[f1544]) ).
fof(f1553,definition,
( spl36_192
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl36_192])],[avatar_definition]) ).
fof(f1554,plain,
( e10 = op1(e10,e10)
| ~ spl36_192 ),
inference(avatar_component_clause,[],[f1553]) ).
fof(f1564,definition,
( spl36_194
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl36_194])],[avatar_definition]) ).
fof(f1565,plain,
( e11 = op1(e11,e11)
| ~ spl36_194 ),
inference(avatar_component_clause,[],[f1564]) ).
fof(f1569,definition,
( spl36_195
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl36_195])],[avatar_definition]) ).
fof(f1571,plain,
( e10 = op1(e11,e10)
| ~ spl36_195 ),
inference(avatar_component_clause,[],[f1569]) ).
fof(f1574,definition,
( spl36_196
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl36_196])],[avatar_definition]) ).
fof(f1576,plain,
( e10 = op1(e10,e11)
| ~ spl36_196 ),
inference(avatar_component_clause,[],[f1574]) ).
fof(f1588,definition,
( spl36_199
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl36_199])],[avatar_definition]) ).
fof(f1590,plain,
( e10 = op1(e12,e10)
| ~ spl36_199 ),
inference(avatar_component_clause,[],[f1588]) ).
fof(f1593,definition,
( spl36_200
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl36_200])],[avatar_definition]) ).
fof(f1607,definition,
( spl36_203
<=> e10 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl36_203])],[avatar_definition]) ).
fof(f1609,plain,
( e10 = op1(e13,e10)
| ~ spl36_203 ),
inference(avatar_component_clause,[],[f1607]) ).
fof(f1612,definition,
( spl36_204
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl36_204])],[avatar_definition]) ).
fof(f1627,definition,
( spl36_207
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl36_207])],[avatar_definition]) ).
fof(f1649,definition,
( spl36_211
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl36_211])],[avatar_definition]) ).
fof(f1651,plain,
( e11 = op1(e11,e12)
| ~ spl36_211 ),
inference(avatar_component_clause,[],[f1649]) ).
fof(f1664,definition,
( spl36_214
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl36_214])],[avatar_definition]) ).
fof(f1666,plain,
( e11 = op1(e11,e13)
| ~ spl36_214 ),
inference(avatar_component_clause,[],[f1664]) ).
fof(f1674,definition,
( spl36_216
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl36_216])],[avatar_definition]) ).
fof(f1676,plain,
( e12 = op1(e10,e12)
| ~ spl36_216 ),
inference(avatar_component_clause,[],[f1674]) ).
fof(f1679,definition,
( spl36_217
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl36_217])],[avatar_definition]) ).
fof(f1681,plain,
( e12 = op1(e12,e10)
| ~ spl36_217 ),
inference(avatar_component_clause,[],[f1679]) ).
fof(f1711,definition,
( spl36_223
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl36_223])],[avatar_definition]) ).
fof(f1713,plain,
( e12 = op1(e13,e12)
| ~ spl36_223 ),
inference(avatar_component_clause,[],[f1711]) ).
fof(f1716,definition,
( spl36_224
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl36_224])],[avatar_definition]) ).
fof(f1718,plain,
( e12 = op1(e12,e13)
| ~ spl36_224 ),
inference(avatar_component_clause,[],[f1716]) ).
fof(f1726,definition,
( spl36_226
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl36_226])],[avatar_definition]) ).
fof(f1728,plain,
( e13 = op1(e10,e13)
| ~ spl36_226 ),
inference(avatar_component_clause,[],[f1726]) ).
fof(f1731,definition,
( spl36_227
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl36_227])],[avatar_definition]) ).
fof(f1733,plain,
( e13 = op1(e13,e10)
| ~ spl36_227 ),
inference(avatar_component_clause,[],[f1731]) ).
fof(f1752,definition,
( spl36_231
<=> e13 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl36_231])],[avatar_definition]) ).
fof(f1757,definition,
( spl36_232
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl36_232])],[avatar_definition]) ).
fof(f1769,definition,
( spl36_233
<=> op1(e10,e10) = e11 ),
introduced(definition,[new_symbols(definition,[spl36_233])],[avatar_definition]) ).
fof(f1770,plain,
( op1(e10,e10) = e11
| ~ spl36_233 ),
inference(avatar_component_clause,[],[f1769]) ).
fof(f1774,definition,
( spl36_234
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[spl36_234])],[avatar_definition]) ).
fof(f1775,plain,
( op1(e10,e10) = e12
| ~ spl36_234 ),
inference(avatar_component_clause,[],[f1774]) ).
fof(f1799,definition,
( spl36_239
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl36_239])],[avatar_definition]) ).
fof(f1800,plain,
( e10 = op1(e12,e12)
| ~ spl36_239 ),
inference(avatar_component_clause,[],[f1799]) ).
fof(f1804,definition,
( spl36_240
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl36_240])],[avatar_definition]) ).
fof(f1809,definition,
( spl36_241
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl36_241])],[avatar_definition]) ).
fof(f1812,plain,
( ~ spl36_241
| spl36_224 ),
inference(avatar_split_clause,[],[f301,f1716,f1809]) ).
fof(f1814,definition,
( spl36_242
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl36_242])],[avatar_definition]) ).
fof(f1815,plain,
( e10 = op1(e13,e13)
| ~ spl36_242 ),
inference(avatar_component_clause,[],[f1814]) ).
fof(f1817,plain,
( ~ spl36_242
| spl36_227 ),
inference(avatar_split_clause,[],[f302,f1731,f1814]) ).
fof(f1819,definition,
( spl36_243
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl36_243])],[avatar_definition]) ).
fof(f1820,plain,
( e11 = op1(e13,e13)
| ~ spl36_243 ),
inference(avatar_component_clause,[],[f1819]) ).
fof(f1824,definition,
( spl36_244
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl36_244])],[avatar_definition]) ).
fof(f1825,plain,
( e12 = op1(e13,e13)
| ~ spl36_244 ),
inference(avatar_component_clause,[],[f1824]) ).
fof(f1831,definition,
( spl36_245
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl36_245])],[avatar_definition]) ).
fof(f1835,definition,
( spl36_246
<=> e21 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl36_246])],[avatar_definition]) ).
fof(f1849,definition,
( spl36_249
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl36_249])],[avatar_definition]) ).
fof(f1851,plain,
( e22 = op2(e20,e21)
| ~ spl36_249 ),
inference(avatar_component_clause,[],[f1849]) ).
fof(f1853,definition,
( spl36_250
<=> e22 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl36_250])],[avatar_definition]) ).
fof(f1855,plain,
( e22 = op2(e20,e23)
| ~ spl36_250 ),
inference(avatar_component_clause,[],[f1853]) ).
fof(f1856,plain,
( spl36_180
| spl36_249
| spl36_162
| spl36_250 ),
inference(avatar_split_clause,[],[f89,f1853,f1394,f1849,f1494]) ).
fof(f1858,definition,
( spl36_251
<=> e22 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl36_251])],[avatar_definition]) ).
fof(f1860,plain,
( e22 = op2(e21,e20)
| ~ spl36_251 ),
inference(avatar_component_clause,[],[f1858]) ).
fof(f1862,definition,
( spl36_252
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl36_252])],[avatar_definition]) ).
fof(f1864,plain,
( e22 = op2(e23,e20)
| ~ spl36_252 ),
inference(avatar_component_clause,[],[f1862]) ).
fof(f1865,plain,
( spl36_180
| spl36_251
| spl36_163
| spl36_252 ),
inference(avatar_split_clause,[],[f90,f1862,f1399,f1858,f1494]) ).
fof(f1867,definition,
( spl36_253
<=> e23 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl36_253])],[avatar_definition]) ).
fof(f1869,plain,
( e23 = op2(e20,e21)
| ~ spl36_253 ),
inference(avatar_component_clause,[],[f1867]) ).
fof(f1871,definition,
( spl36_254
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl36_254])],[avatar_definition]) ).
fof(f1873,plain,
( e23 = op2(e20,e22)
| ~ spl36_254 ),
inference(avatar_component_clause,[],[f1871]) ).
fof(f1874,plain,
( spl36_181
| spl36_253
| spl36_254
| spl36_172 ),
inference(avatar_split_clause,[],[f91,f1446,f1871,f1867,f1499]) ).
fof(f1876,definition,
( spl36_255
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl36_255])],[avatar_definition]) ).
fof(f1885,definition,
( spl36_257
<=> e20 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl36_257])],[avatar_definition]) ).
fof(f1887,plain,
( e20 = op2(e21,e22)
| ~ spl36_257 ),
inference(avatar_component_clause,[],[f1885]) ).
fof(f1889,definition,
( spl36_258
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl36_258])],[avatar_definition]) ).
fof(f1891,plain,
( e20 = op2(e21,e23)
| ~ spl36_258 ),
inference(avatar_component_clause,[],[f1889]) ).
fof(f1892,plain,
( spl36_141
| spl36_182
| spl36_257
| spl36_258 ),
inference(avatar_split_clause,[],[f93,f1889,f1885,f1504,f1289]) ).
fof(f1905,definition,
( spl36_261
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl36_261])],[avatar_definition]) ).
fof(f1907,plain,
( e22 = op2(e21,e23)
| ~ spl36_261 ),
inference(avatar_component_clause,[],[f1905]) ).
fof(f1910,definition,
( spl36_262
<=> e22 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl36_262])],[avatar_definition]) ).
fof(f1912,plain,
( e22 = op2(e23,e21)
| ~ spl36_262 ),
inference(avatar_component_clause,[],[f1910]) ).
fof(f1915,definition,
( spl36_263
<=> e23 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl36_263])],[avatar_definition]) ).
fof(f1917,plain,
( e23 = op2(e21,e22)
| ~ spl36_263 ),
inference(avatar_component_clause,[],[f1915]) ).
fof(f1918,plain,
( spl36_255
| spl36_184
| spl36_263
| spl36_175 ),
inference(avatar_split_clause,[],[f99,f1461,f1915,f1514,f1876]) ).
fof(f1920,definition,
( spl36_264
<=> e23 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl36_264])],[avatar_definition]) ).
fof(f1922,plain,
( e23 = op2(e22,e21)
| ~ spl36_264 ),
inference(avatar_component_clause,[],[f1920]) ).
fof(f1923,plain,
( spl36_253
| spl36_184
| spl36_264
| spl36_176 ),
inference(avatar_split_clause,[],[f100,f1466,f1920,f1514,f1867]) ).
fof(f1930,definition,
( spl36_266
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl36_266])],[avatar_definition]) ).
fof(f1933,plain,
( spl36_146
| spl36_257
| spl36_185
| spl36_266 ),
inference(avatar_split_clause,[],[f102,f1930,f1519,f1885,f1313]) ).
fof(f1935,definition,
( spl36_267
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl36_267])],[avatar_definition]) ).
fof(f1937,plain,
( e21 = op2(e22,e23)
| ~ spl36_267 ),
inference(avatar_component_clause,[],[f1935]) ).
fof(f1940,definition,
( spl36_268
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl36_268])],[avatar_definition]) ).
fof(f1942,plain,
( e21 = op2(e23,e22)
| ~ spl36_268 ),
inference(avatar_component_clause,[],[f1940]) ).
fof(f1943,plain,
( spl36_245
| spl36_157
| spl36_186
| spl36_268 ),
inference(avatar_split_clause,[],[f104,f1940,f1524,f1369,f1831]) ).
fof(f1945,plain,
( spl36_162
| spl36_165
| spl36_144
| spl36_169 ),
inference(avatar_split_clause,[],[f106,f1431,f1303,f1409,f1394]) ).
fof(f1951,plain,
( spl36_246
| spl36_160
| spl36_267
| spl36_189 ),
inference(avatar_split_clause,[],[f112,f1539,f1935,f1384,f1835]) ).
fof(f1952,plain,
( spl36_252
| spl36_262
| spl36_169
| spl36_190 ),
inference(avatar_split_clause,[],[f113,f1544,f1431,f1910,f1862]) ).
fof(f1955,plain,
( spl36_172
| spl36_175
| spl36_177
| spl36_148 ),
inference(avatar_split_clause,[],[f116,f1322,f1472,f1461,f1446]) ).
fof(f1972,plain,
( spl36_192
| spl36_196
| spl36_200
| spl36_204 ),
inference(avatar_split_clause,[],[f37,f1612,f1593,f1574,f1553]) ).
fof(f1973,plain,
( spl36_192
| spl36_195
| spl36_199
| spl36_203 ),
inference(avatar_split_clause,[],[f38,f1607,f1588,f1569,f1553]) ).
fof(f1975,definition,
( spl36_269
<=> e11 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl36_269])],[avatar_definition]) ).
fof(f1977,plain,
( e11 = op1(e10,e12)
| ~ spl36_269 ),
inference(avatar_component_clause,[],[f1975]) ).
fof(f1979,definition,
( spl36_270
<=> e11 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl36_270])],[avatar_definition]) ).
fof(f1997,definition,
( spl36_274
<=> e12 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl36_274])],[avatar_definition]) ).
fof(f2002,definition,
( spl36_275
<=> e12 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl36_275])],[avatar_definition]) ).
fof(f2006,definition,
( spl36_276
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl36_276])],[avatar_definition]) ).
fof(f2008,plain,
( e12 = op1(e13,e10)
| ~ spl36_276 ),
inference(avatar_component_clause,[],[f2006]) ).
fof(f2009,plain,
( spl36_234
| spl36_275
| spl36_217
| spl36_276 ),
inference(avatar_split_clause,[],[f42,f2006,f1679,f2002,f1774]) ).
fof(f2015,definition,
( spl36_278
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl36_278])],[avatar_definition]) ).
fof(f2024,definition,
( spl36_280
<=> e13 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl36_280])],[avatar_definition]) ).
fof(f2038,definition,
( spl36_283
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl36_283])],[avatar_definition]) ).
fof(f2040,plain,
( e10 = op1(e12,e11)
| ~ spl36_283 ),
inference(avatar_component_clause,[],[f2038]) ).
fof(f2046,plain,
( spl36_207
| spl36_194
| spl36_211
| spl36_214 ),
inference(avatar_split_clause,[],[f47,f1664,f1649,f1564,f1627]) ).
fof(f2049,definition,
( spl36_285
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl36_285])],[avatar_definition]) ).
fof(f2051,plain,
( e12 = op1(e11,e13)
| ~ spl36_285 ),
inference(avatar_component_clause,[],[f2049]) ).
fof(f2054,definition,
( spl36_286
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl36_286])],[avatar_definition]) ).
fof(f2056,plain,
( e12 = op1(e13,e11)
| ~ spl36_286 ),
inference(avatar_component_clause,[],[f2054]) ).
fof(f2059,definition,
( spl36_287
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl36_287])],[avatar_definition]) ).
fof(f2061,plain,
( e13 = op1(e11,e12)
| ~ spl36_287 ),
inference(avatar_component_clause,[],[f2059]) ).
fof(f2064,definition,
( spl36_288
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl36_288])],[avatar_definition]) ).
fof(f2066,plain,
( e13 = op1(e12,e11)
| ~ spl36_288 ),
inference(avatar_component_clause,[],[f2064]) ).
fof(f2069,definition,
( spl36_289
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl36_289])],[avatar_definition]) ).
fof(f2072,plain,
( spl36_199
| spl36_283
| spl36_239
| spl36_289 ),
inference(avatar_split_clause,[],[f53,f2069,f1799,f2038,f1588]) ).
fof(f2079,definition,
( spl36_291
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl36_291])],[avatar_definition]) ).
fof(f2081,plain,
( e11 = op1(e12,e13)
| ~ spl36_291 ),
inference(avatar_component_clause,[],[f2079]) ).
fof(f2084,definition,
( spl36_292
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl36_292])],[avatar_definition]) ).
fof(f2086,plain,
( e11 = op1(e13,e12)
| ~ spl36_292 ),
inference(avatar_component_clause,[],[f2084]) ).
fof(f2087,plain,
( spl36_269
| spl36_211
| spl36_240
| spl36_292 ),
inference(avatar_split_clause,[],[f56,f2084,f1804,f1649,f1975]) ).
fof(f2090,plain,
( spl36_280
| spl36_288
| spl36_241
| spl36_231 ),
inference(avatar_split_clause,[],[f59,f1752,f1809,f2064,f2024]) ).
fof(f2091,plain,
( spl36_278
| spl36_287
| spl36_241
| spl36_232 ),
inference(avatar_split_clause,[],[f60,f1757,f1809,f2059,f2015]) ).
fof(f2095,plain,
( spl36_270
| spl36_214
| spl36_291
| spl36_243 ),
inference(avatar_split_clause,[],[f64,f1819,f2079,f1664,f1979]) ).
fof(f2096,plain,
( spl36_276
| spl36_286
| spl36_223
| spl36_244 ),
inference(avatar_split_clause,[],[f65,f1824,f1711,f2054,f2006]) ).
fof(f2102,plain,
( spl36_200
| spl36_269
| spl36_216
| spl36_278 ),
inference(avatar_split_clause,[],[f23,f2015,f1674,f1975,f1593]) ).
fof(f2103,plain,
( spl36_204
| spl36_270
| spl36_274
| spl36_226 ),
inference(avatar_split_clause,[],[f24,f1726,f1997,f1979,f1612]) ).
fof(f2116,plain,
( e20 != e21
| ~ spl36_2
| spl36_7 ),
inference(forward_demodulation,[],[f655,f630]) ).
fof(f2120,plain,
spl36_242,
inference(avatar_split_clause,[],[f371,f1814]) ).
fof(f2121,plain,
spl36_188,
inference(avatar_split_clause,[],[f374,f1534]) ).
fof(f2130,plain,
( e20 = e22
| ~ spl36_146
| ~ spl36_162 ),
inference(superposition,[],[f1396,f1315]) ).
fof(f2134,plain,
( $false
| ~ spl36_146
| ~ spl36_162 ),
inference(forward_subsumption_resolution,[],[f2130,f223]) ).
fof(f2135,plain,
( ~ spl36_146
| ~ spl36_162 ),
inference(avatar_contradiction_clause,[],[f2134]) ).
fof(f2144,plain,
( e20 = e22
| ~ spl36_144
| ~ spl36_185 ),
inference(forward_demodulation,[],[f1520,f1304]) ).
fof(f2145,plain,
( $false
| ~ spl36_144
| ~ spl36_185 ),
inference(forward_subsumption_resolution,[],[f2144,f223]) ).
fof(f2146,plain,
( ~ spl36_144
| ~ spl36_185 ),
inference(avatar_contradiction_clause,[],[f2145]) ).
fof(f2155,plain,
( e21 = e22
| ~ spl36_27
| ~ spl36_105 ),
inference(forward_demodulation,[],[f750,f1106]) ).
fof(f2182,plain,
( e21 != e22
| spl36_27
| ~ spl36_105 ),
inference(forward_demodulation,[],[f751,f1106]) ).
fof(f2218,plain,
( e21 = e23
| ~ spl36_37
| ~ spl36_136 ),
inference(forward_demodulation,[],[f798,f1258]) ).
fof(f2240,plain,
( e21 != e23
| spl36_37
| ~ spl36_136 ),
inference(forward_demodulation,[],[f799,f1258]) ).
fof(f2260,plain,
( e20 = e21
| ~ spl36_140
| ~ spl36_182 ),
inference(superposition,[],[f1505,f1285]) ).
fof(f2264,plain,
( $false
| ~ spl36_2
| spl36_7
| ~ spl36_140
| ~ spl36_182 ),
inference(forward_subsumption_resolution,[],[f2260,f2116]) ).
fof(f2265,plain,
( ~ spl36_2
| spl36_7
| ~ spl36_140
| ~ spl36_182 ),
inference(avatar_contradiction_clause,[],[f2264]) ).
fof(f2269,plain,
( e20 = e23
| ~ spl36_148
| ~ spl36_188 ),
inference(forward_demodulation,[],[f1535,f1323]) ).
fof(f2270,plain,
( $false
| ~ spl36_148
| ~ spl36_188 ),
inference(forward_subsumption_resolution,[],[f2269,f222]) ).
fof(f2271,plain,
( ~ spl36_148
| ~ spl36_188 ),
inference(avatar_contradiction_clause,[],[f2270]) ).
fof(f2314,plain,
( e10 = e13
| ~ spl36_203
| ~ spl36_227 ),
inference(superposition,[],[f1733,f1609]) ).
fof(f2318,plain,
( $false
| ~ spl36_203
| ~ spl36_227 ),
inference(forward_subsumption_resolution,[],[f2314,f216]) ).
fof(f2319,plain,
( ~ spl36_203
| ~ spl36_227 ),
inference(avatar_contradiction_clause,[],[f2318]) ).
fof(f2358,plain,
( e12 = e13
| ~ spl36_227
| ~ spl36_276 ),
inference(forward_demodulation,[],[f2008,f1733]) ).
fof(f2359,plain,
( $false
| ~ spl36_227
| ~ spl36_276 ),
inference(forward_subsumption_resolution,[],[f2358,f213]) ).
fof(f2360,plain,
( ~ spl36_227
| ~ spl36_276 ),
inference(avatar_contradiction_clause,[],[f2359]) ).
fof(f2378,plain,
( e21 = e22
| ~ spl36_160
| ~ spl36_261 ),
inference(superposition,[],[f1907,f1386]) ).
fof(f2383,plain,
( $false
| spl36_27
| ~ spl36_105
| ~ spl36_160
| ~ spl36_261 ),
inference(forward_subsumption_resolution,[],[f2378,f2182]) ).
fof(f2384,plain,
( spl36_27
| ~ spl36_105
| ~ spl36_160
| ~ spl36_261 ),
inference(avatar_contradiction_clause,[],[f2383]) ).
fof(f2385,plain,
( e20 = e21
| ~ spl36_2
| ~ spl36_7 ),
inference(forward_demodulation,[],[f654,f630]) ).
fof(f2389,plain,
( e21 = e22
| ~ spl36_179
| ~ spl36_180 ),
inference(forward_demodulation,[],[f1490,f1495]) ).
fof(f2449,plain,
( $false
| spl36_27
| ~ spl36_105
| ~ spl36_179
| ~ spl36_180 ),
inference(forward_subsumption_resolution,[],[f2389,f2182]) ).
fof(f2450,plain,
( spl36_27
| ~ spl36_105
| ~ spl36_179
| ~ spl36_180 ),
inference(avatar_contradiction_clause,[],[f2449]) ).
fof(f2479,plain,
( $false
| ~ spl36_2
| ~ spl36_7 ),
inference(forward_subsumption_resolution,[],[f224,f2385]) ).
fof(f2480,plain,
( ~ spl36_2
| ~ spl36_7 ),
inference(avatar_contradiction_clause,[],[f2479]) ).
fof(f2491,plain,
( $false
| ~ spl36_27
| ~ spl36_105 ),
inference(forward_subsumption_resolution,[],[f221,f2155]) ).
fof(f2492,plain,
( ~ spl36_27
| ~ spl36_105 ),
inference(avatar_contradiction_clause,[],[f2491]) ).
fof(f2546,plain,
( e20 != op2(e23,e23)
| ~ spl36_37
| ~ spl36_136
| spl36_182 ),
inference(superposition,[],[f1506,f2218]) ).
fof(f2553,plain,
( $false
| ~ spl36_37
| ~ spl36_136
| spl36_182
| ~ spl36_188 ),
inference(forward_subsumption_resolution,[],[f2546,f1535]) ).
fof(f2554,plain,
( ~ spl36_37
| ~ spl36_136
| spl36_182
| ~ spl36_188 ),
inference(avatar_contradiction_clause,[],[f2553]) ).
fof(f2574,plain,
( e20 = e22
| ~ spl36_142
| ~ spl36_249 ),
inference(superposition,[],[f1851,f1296]) ).
fof(f2578,plain,
( $false
| ~ spl36_142
| ~ spl36_249 ),
inference(forward_subsumption_resolution,[],[f2574,f223]) ).
fof(f2579,plain,
( ~ spl36_142
| ~ spl36_249 ),
inference(avatar_contradiction_clause,[],[f2578]) ).
fof(f2580,plain,
( e22 = e23
| ~ spl36_172
| ~ spl36_250 ),
inference(forward_demodulation,[],[f1855,f1448]) ).
fof(f2581,plain,
( $false
| ~ spl36_172
| ~ spl36_250 ),
inference(forward_subsumption_resolution,[],[f2580,f219]) ).
fof(f2582,plain,
( ~ spl36_172
| ~ spl36_250 ),
inference(avatar_contradiction_clause,[],[f2581]) ).
fof(f2584,plain,
( e21 = e23
| ~ spl36_179
| ~ spl36_181 ),
inference(superposition,[],[f1500,f1490]) ).
fof(f2590,plain,
( $false
| spl36_37
| ~ spl36_136
| ~ spl36_179
| ~ spl36_181 ),
inference(forward_subsumption_resolution,[],[f2584,f2240]) ).
fof(f2591,plain,
( spl36_37
| ~ spl36_136
| ~ spl36_179
| ~ spl36_181 ),
inference(avatar_contradiction_clause,[],[f2590]) ).
fof(f2604,plain,
( e20 = e22
| ~ spl36_141
| ~ spl36_251 ),
inference(superposition,[],[f1860,f1291]) ).
fof(f2608,plain,
( $false
| ~ spl36_141
| ~ spl36_251 ),
inference(forward_subsumption_resolution,[],[f2604,f223]) ).
fof(f2609,plain,
( ~ spl36_141
| ~ spl36_251 ),
inference(avatar_contradiction_clause,[],[f2608]) ).
fof(f2613,plain,
( e20 = e23
| ~ spl36_146
| ~ spl36_254 ),
inference(superposition,[],[f1873,f1315]) ).
fof(f2618,plain,
( $false
| ~ spl36_146
| ~ spl36_254 ),
inference(forward_subsumption_resolution,[],[f2613,f222]) ).
fof(f2619,plain,
( ~ spl36_146
| ~ spl36_254 ),
inference(avatar_contradiction_clause,[],[f2618]) ).
fof(f2620,plain,
( e20 = e23
| ~ spl36_142
| ~ spl36_253 ),
inference(superposition,[],[f1869,f1296]) ).
fof(f2625,plain,
( $false
| ~ spl36_142
| ~ spl36_253 ),
inference(forward_subsumption_resolution,[],[f2620,f222]) ).
fof(f2626,plain,
( ~ spl36_142
| ~ spl36_253 ),
inference(avatar_contradiction_clause,[],[f2625]) ).
fof(f2630,plain,
( e22 = e23
| ~ spl36_173
| ~ spl36_252 ),
inference(forward_demodulation,[],[f1864,f1453]) ).
fof(f2631,plain,
( $false
| ~ spl36_173
| ~ spl36_252 ),
inference(forward_subsumption_resolution,[],[f2630,f219]) ).
fof(f2632,plain,
( ~ spl36_173
| ~ spl36_252 ),
inference(avatar_contradiction_clause,[],[f2631]) ).
fof(f2688,plain,
( e22 = e23
| ~ spl36_162
| ~ spl36_254 ),
inference(forward_demodulation,[],[f1396,f1873]) ).
fof(f2690,plain,
( $false
| ~ spl36_162
| ~ spl36_254 ),
inference(forward_subsumption_resolution,[],[f2688,f219]) ).
fof(f2691,plain,
( ~ spl36_162
| ~ spl36_254 ),
inference(avatar_contradiction_clause,[],[f2690]) ).
fof(f2729,plain,
( e22 = e23
| ~ spl36_175
| ~ spl36_261 ),
inference(forward_demodulation,[],[f1907,f1463]) ).
fof(f2730,plain,
( $false
| ~ spl36_175
| ~ spl36_261 ),
inference(forward_subsumption_resolution,[],[f2729,f219]) ).
fof(f2731,plain,
( ~ spl36_175
| ~ spl36_261 ),
inference(avatar_contradiction_clause,[],[f2730]) ).
fof(f2756,plain,
( e22 = e23
| ~ spl36_176
| ~ spl36_262 ),
inference(forward_demodulation,[],[f1912,f1468]) ).
fof(f2757,plain,
( $false
| ~ spl36_176
| ~ spl36_262 ),
inference(forward_subsumption_resolution,[],[f2756,f219]) ).
fof(f2758,plain,
( ~ spl36_176
| ~ spl36_262 ),
inference(avatar_contradiction_clause,[],[f2757]) ).
fof(f2762,plain,
( e20 = e23
| ~ spl36_257
| ~ spl36_263 ),
inference(superposition,[],[f1917,f1887]) ).
fof(f2767,plain,
( $false
| ~ spl36_257
| ~ spl36_263 ),
inference(forward_subsumption_resolution,[],[f2762,f222]) ).
fof(f2768,plain,
( ~ spl36_257
| ~ spl36_263 ),
inference(avatar_contradiction_clause,[],[f2767]) ).
fof(f2777,plain,
( e20 = e22
| ~ spl36_258
| ~ spl36_261 ),
inference(forward_demodulation,[],[f1891,f1907]) ).
fof(f2778,plain,
( $false
| ~ spl36_258
| ~ spl36_261 ),
inference(forward_subsumption_resolution,[],[f2777,f223]) ).
fof(f2779,plain,
( ~ spl36_258
| ~ spl36_261 ),
inference(avatar_contradiction_clause,[],[f2778]) ).
fof(f2781,plain,
( e20 = e22
| ~ spl36_188
| ~ spl36_190 ),
inference(superposition,[],[f1545,f1535]) ).
fof(f2786,plain,
( $false
| ~ spl36_188
| ~ spl36_190 ),
inference(forward_subsumption_resolution,[],[f2781,f223]) ).
fof(f2787,plain,
( ~ spl36_188
| ~ spl36_190 ),
inference(avatar_contradiction_clause,[],[f2786]) ).
fof(f2806,plain,
( e22 = e23
| ~ spl36_165
| ~ spl36_263 ),
inference(superposition,[],[f1917,f1411]) ).
fof(f2811,plain,
( $false
| ~ spl36_165
| ~ spl36_263 ),
inference(forward_subsumption_resolution,[],[f2806,f219]) ).
fof(f2812,plain,
( ~ spl36_165
| ~ spl36_263 ),
inference(avatar_contradiction_clause,[],[f2811]) ).
fof(f2835,plain,
( e20 = e21
| ~ spl36_185
| ~ spl36_186 ),
inference(forward_demodulation,[],[f1525,f1520]) ).
fof(f2836,plain,
( $false
| ~ spl36_2
| spl36_7
| ~ spl36_185
| ~ spl36_186 ),
inference(forward_subsumption_resolution,[],[f2835,f2116]) ).
fof(f2837,plain,
( ~ spl36_2
| spl36_7
| ~ spl36_185
| ~ spl36_186 ),
inference(avatar_contradiction_clause,[],[f2836]) ).
fof(f2865,plain,
( e21 = e23
| ~ spl36_157
| ~ spl36_263 ),
inference(superposition,[],[f1917,f1371]) ).
fof(f2871,plain,
( $false
| spl36_37
| ~ spl36_136
| ~ spl36_157
| ~ spl36_263 ),
inference(forward_subsumption_resolution,[],[f2865,f2240]) ).
fof(f2872,plain,
( spl36_37
| ~ spl36_136
| ~ spl36_157
| ~ spl36_263 ),
inference(avatar_contradiction_clause,[],[f2871]) ).
fof(f2982,plain,
( e21 = e22
| ~ spl36_169
| ~ spl36_268 ),
inference(forward_demodulation,[],[f1942,f1433]) ).
fof(f2983,plain,
( $false
| spl36_27
| ~ spl36_105
| ~ spl36_169
| ~ spl36_268 ),
inference(forward_subsumption_resolution,[],[f2982,f2182]) ).
fof(f2984,plain,
( spl36_27
| ~ spl36_105
| ~ spl36_169
| ~ spl36_268 ),
inference(avatar_contradiction_clause,[],[f2983]) ).
fof(f3022,plain,
( e11 = e12
| ~ spl36_214
| ~ spl36_285 ),
inference(superposition,[],[f2051,f1666]) ).
fof(f3027,plain,
( $false
| ~ spl36_214
| ~ spl36_285 ),
inference(forward_subsumption_resolution,[],[f3022,f215]) ).
fof(f3028,plain,
( ~ spl36_214
| ~ spl36_285 ),
inference(avatar_contradiction_clause,[],[f3027]) ).
fof(f3030,plain,
( e11 = e12
| ~ spl36_233
| ~ spl36_234 ),
inference(forward_demodulation,[],[f1770,f1775]) ).
fof(f3033,plain,
( $false
| ~ spl36_233
| ~ spl36_234 ),
inference(forward_subsumption_resolution,[],[f3030,f215]) ).
fof(f3034,plain,
( ~ spl36_233
| ~ spl36_234 ),
inference(avatar_contradiction_clause,[],[f3033]) ).
fof(f3040,plain,
( e10 = e11
| ~ spl36_242
| ~ spl36_243 ),
inference(forward_demodulation,[],[f1820,f1815]) ).
fof(f3045,plain,
( $false
| ~ spl36_242
| ~ spl36_243 ),
inference(forward_subsumption_resolution,[],[f3040,f218]) ).
fof(f3046,plain,
( ~ spl36_242
| ~ spl36_243 ),
inference(avatar_contradiction_clause,[],[f3045]) ).
fof(f3061,plain,
( e10 = e12
| ~ spl36_242
| ~ spl36_244 ),
inference(superposition,[],[f1825,f1815]) ).
fof(f3066,plain,
( $false
| ~ spl36_242
| ~ spl36_244 ),
inference(forward_subsumption_resolution,[],[f3061,f217]) ).
fof(f3067,plain,
( ~ spl36_242
| ~ spl36_244 ),
inference(avatar_contradiction_clause,[],[f3066]) ).
fof(f3082,plain,
( e10 = e12
| ~ spl36_199
| ~ spl36_217 ),
inference(superposition,[],[f1681,f1590]) ).
fof(f3086,plain,
( $false
| ~ spl36_199
| ~ spl36_217 ),
inference(forward_subsumption_resolution,[],[f3082,f217]) ).
fof(f3087,plain,
( ~ spl36_199
| ~ spl36_217 ),
inference(avatar_contradiction_clause,[],[f3086]) ).
fof(f3127,plain,
( e11 = e13
| ~ spl36_211
| ~ spl36_287 ),
inference(forward_demodulation,[],[f1651,f2061]) ).
fof(f3131,plain,
( $false
| ~ spl36_211
| ~ spl36_287 ),
inference(forward_subsumption_resolution,[],[f3127,f214]) ).
fof(f3132,plain,
( ~ spl36_211
| ~ spl36_287 ),
inference(avatar_contradiction_clause,[],[f3131]) ).
fof(f3239,plain,
( e10 = e13
| ~ spl36_283
| ~ spl36_288 ),
inference(superposition,[],[f2066,f2040]) ).
fof(f3245,plain,
( $false
| ~ spl36_283
| ~ spl36_288 ),
inference(forward_subsumption_resolution,[],[f3239,f216]) ).
fof(f3246,plain,
( ~ spl36_283
| ~ spl36_288 ),
inference(avatar_contradiction_clause,[],[f3245]) ).
fof(f3361,plain,
( e11 = e12
| ~ spl36_223
| ~ spl36_292 ),
inference(forward_demodulation,[],[f2086,f1713]) ).
fof(f3362,plain,
( $false
| ~ spl36_223
| ~ spl36_292 ),
inference(forward_subsumption_resolution,[],[f3361,f215]) ).
fof(f3363,plain,
( ~ spl36_223
| ~ spl36_292 ),
inference(avatar_contradiction_clause,[],[f3362]) ).
fof(f3412,plain,
( e12 != op1(e12,e10)
| ~ spl36_224 ),
inference(forward_demodulation,[],[f126,f1718]) ).
fof(f3421,plain,
( e13 != op1(e10,e12)
| ~ spl36_226 ),
inference(forward_demodulation,[],[f135,f1728]) ).
fof(f3427,plain,
( op1(e10,e10) != e11
| ~ spl36_269 ),
inference(forward_demodulation,[],[f139,f1977]) ).
fof(f3430,plain,
( e10 != op1(e12,e13)
| ~ spl36_242 ),
inference(forward_demodulation,[],[f141,f1815]) ).
fof(f3434,plain,
( e10 != op1(e10,e13)
| ~ spl36_242 ),
inference(forward_demodulation,[],[f144,f1815]) ).
fof(f3451,plain,
( e13 != op1(e12,e10)
| ~ spl36_227 ),
inference(forward_demodulation,[],[f159,f1733]) ).
fof(f3458,plain,
( e20 != op2(e23,e22)
| ~ spl36_188 ),
inference(forward_demodulation,[],[f165,f1535]) ).
fof(f3501,plain,
( e22 != op2(e22,e22)
| ~ spl36_169 ),
inference(forward_demodulation,[],[f195,f1433]) ).
fof(f3517,plain,
( e23 != op2(e21,e20)
| ~ spl36_173 ),
inference(forward_demodulation,[],[f208,f1453]) ).
fof(f3523,plain,
( op1(e10,e10) = e11
| ~ spl36_242 ),
inference(forward_demodulation,[],[f370,f1815]) ).
fof(f3524,plain,
( e10 = e11
| ~ spl36_192
| ~ spl36_242 ),
inference(forward_demodulation,[],[f3523,f1554]) ).
fof(f3525,plain,
( $false
| ~ spl36_192
| ~ spl36_242 ),
inference(forward_subsumption_resolution,[],[f3524,f218]) ).
fof(f3526,plain,
( ~ spl36_192
| ~ spl36_242 ),
inference(avatar_contradiction_clause,[],[f3525]) ).
fof(f3532,plain,
( ~ spl36_280
| ~ spl36_227 ),
inference(avatar_split_clause,[],[f3451,f1731,f2024]) ).
fof(f3533,plain,
( ~ spl36_278
| ~ spl36_226 ),
inference(avatar_split_clause,[],[f3421,f1726,f2015]) ).
fof(f3536,plain,
( ~ spl36_217
| ~ spl36_224 ),
inference(avatar_split_clause,[],[f3412,f1716,f1679]) ).
fof(f3542,plain,
( ~ spl36_233
| ~ spl36_269 ),
inference(avatar_split_clause,[],[f3427,f1975,f1769]) ).
fof(f3543,plain,
( spl36_233
| ~ spl36_242 ),
inference(avatar_split_clause,[],[f3523,f1814,f1769]) ).
fof(f3546,plain,
( ~ spl36_289
| ~ spl36_242 ),
inference(avatar_split_clause,[],[f3430,f1814,f2069]) ).
fof(f3547,plain,
( e13 != op1(e12,e13)
| ~ spl36_226 ),
inference(forward_demodulation,[],[f145,f1728]) ).
fof(f3549,plain,
( e13 != op1(e13,e12)
| ~ spl36_227 ),
inference(forward_demodulation,[],[f121,f1733]) ).
fof(f3626,plain,
( e11 != op1(e12,e12)
| ~ spl36_291 ),
inference(forward_demodulation,[],[f123,f2081]) ).
fof(f3636,plain,
( e12 != op1(e11,e10)
| ~ spl36_285 ),
inference(forward_demodulation,[],[f132,f2051]) ).
fof(f3648,plain,
( e10 != op1(e10,e12)
| ~ spl36_239 ),
inference(forward_demodulation,[],[f151,f1800]) ).
fof(f3659,plain,
( op2(e20,e20) = e21
| ~ spl36_188 ),
inference(forward_demodulation,[],[f373,f1535]) ).
fof(f3660,plain,
( e20 = e21
| ~ spl36_138
| ~ spl36_188 ),
inference(forward_demodulation,[],[f3659,f1274]) ).
fof(f3661,plain,
( $false
| ~ spl36_2
| spl36_7
| ~ spl36_138
| ~ spl36_188 ),
inference(forward_subsumption_resolution,[],[f3660,f2116]) ).
fof(f3662,plain,
( ~ spl36_2
| spl36_7
| ~ spl36_138
| ~ spl36_188 ),
inference(avatar_contradiction_clause,[],[f3661]) ).
fof(f3669,plain,
( ~ spl36_266
| ~ spl36_188 ),
inference(avatar_split_clause,[],[f3458,f1534,f1930]) ).
fof(f3680,plain,
( spl36_179
| ~ spl36_188 ),
inference(avatar_split_clause,[],[f3659,f1534,f1489]) ).
fof(f3781,plain,
( e20 = h3(e10)
| ~ spl36_185 ),
inference(forward_demodulation,[],[f385,f1520]) ).
fof(f3782,plain,
( spl36_25
| ~ spl36_185 ),
inference(avatar_split_clause,[],[f3781,f1519,f740]) ).
fof(f3834,plain,
( op2(e20,e20) = h3(e11)
| ~ spl36_185 ),
inference(forward_demodulation,[],[f384,f1520]) ).
fof(f3835,plain,
( e21 = h3(e11)
| ~ spl36_179
| ~ spl36_185 ),
inference(forward_demodulation,[],[f3834,f1490]) ).
fof(f3838,plain,
( spl36_29
| ~ spl36_179
| ~ spl36_185 ),
inference(avatar_split_clause,[],[f3835,f1519,f1489,f759]) ).
fof(f3840,plain,
( h3(op1(e10,e11)) != op2(h3(e10),e21)
| ~ spl36_29
| spl36_90 ),
inference(superposition,[],[f1047,f760]) ).
fof(f3841,plain,
( op2(e20,e21) != h3(op1(e10,e11))
| ~ spl36_25
| ~ spl36_29
| spl36_90 ),
inference(forward_demodulation,[],[f3840,f741]) ).
fof(f3844,plain,
( op2(e20,e21) != h3(e10)
| ~ spl36_25
| ~ spl36_29
| spl36_90
| ~ spl36_196 ),
inference(forward_demodulation,[],[f3841,f1576]) ).
fof(f3845,plain,
( e20 != op2(e20,e21)
| ~ spl36_25
| ~ spl36_29
| spl36_90
| ~ spl36_196 ),
inference(forward_demodulation,[],[f3844,f741]) ).
fof(f3846,plain,
( $false
| ~ spl36_25
| ~ spl36_29
| spl36_90
| ~ spl36_142
| ~ spl36_196 ),
inference(forward_subsumption_resolution,[],[f3845,f1296]) ).
fof(f3847,plain,
( ~ spl36_25
| ~ spl36_29
| spl36_90
| ~ spl36_142
| ~ spl36_196 ),
inference(avatar_contradiction_clause,[],[f3846]) ).
fof(f3848,plain,
( op2(e20,e20) != h3(op1(e10,e10))
| ~ spl36_25
| spl36_89 ),
inference(forward_demodulation,[],[f1043,f741]) ).
fof(f3850,plain,
( op2(e20,e20) != h3(e11)
| ~ spl36_25
| spl36_89
| ~ spl36_233 ),
inference(forward_demodulation,[],[f3848,f1770]) ).
fof(f3852,plain,
( op2(e20,e20) != e21
| ~ spl36_25
| ~ spl36_29
| spl36_89
| ~ spl36_233 ),
inference(forward_demodulation,[],[f3850,f760]) ).
fof(f3854,plain,
( $false
| ~ spl36_25
| ~ spl36_29
| spl36_89
| ~ spl36_179
| ~ spl36_233 ),
inference(forward_subsumption_resolution,[],[f3852,f1490]) ).
fof(f3855,plain,
( ~ spl36_25
| ~ spl36_29
| spl36_89
| ~ spl36_179
| ~ spl36_233 ),
inference(avatar_contradiction_clause,[],[f3854]) ).
fof(f3858,plain,
( h3(op1(e10,e12)) != op2(e20,h3(e12))
| ~ spl36_25
| spl36_91 ),
inference(forward_demodulation,[],[f1051,f741]) ).
fof(f3860,plain,
( h3(e12) != op2(e20,h3(e12))
| ~ spl36_25
| spl36_91
| ~ spl36_216 ),
inference(forward_demodulation,[],[f3858,f1676]) ).
fof(f3878,plain,
( e12 = op1(op1(e10,e10),e13)
| ~ spl36_242 ),
inference(forward_demodulation,[],[f369,f1815]) ).
fof(f3879,plain,
( e12 = op1(e11,e13)
| ~ spl36_233
| ~ spl36_242 ),
inference(forward_demodulation,[],[f3878,f1770]) ).
fof(f3880,plain,
( e22 = op2(op2(e20,e20),e23)
| ~ spl36_188 ),
inference(forward_demodulation,[],[f372,f1535]) ).
fof(f3881,plain,
( e22 = op2(e21,e23)
| ~ spl36_179
| ~ spl36_188 ),
inference(forward_demodulation,[],[f3880,f1490]) ).
fof(f4204,plain,
( h3(e12) = op2(op2(e20,e20),e22)
| ~ spl36_185 ),
inference(forward_demodulation,[],[f383,f1520]) ).
fof(f4205,plain,
( op2(e21,e22) = h3(e12)
| ~ spl36_179
| ~ spl36_185 ),
inference(forward_demodulation,[],[f4204,f1490]) ).
fof(f4206,plain,
( e23 = h3(e12)
| ~ spl36_179
| ~ spl36_185
| ~ spl36_263 ),
inference(forward_demodulation,[],[f4205,f1917]) ).
fof(f4207,plain,
( spl36_111
| ~ spl36_179
| ~ spl36_185
| ~ spl36_263 ),
inference(avatar_split_clause,[],[f4206,f1915,f1519,f1489,f1137]) ).
fof(f4208,plain,
( e23 != op2(e20,e23)
| ~ spl36_25
| spl36_91
| ~ spl36_111
| ~ spl36_216 ),
inference(superposition,[],[f3860,f1138]) ).
fof(f4210,plain,
( $false
| ~ spl36_25
| spl36_91
| ~ spl36_111
| ~ spl36_172
| ~ spl36_216 ),
inference(forward_subsumption_resolution,[],[f4208,f1448]) ).
fof(f4211,plain,
( ~ spl36_25
| spl36_91
| ~ spl36_111
| ~ spl36_172
| ~ spl36_216 ),
inference(avatar_contradiction_clause,[],[f4210]) ).
fof(f4213,plain,
( h3(op1(e10,e13)) != op2(h3(e10),e22)
| spl36_92
| ~ spl36_105 ),
inference(forward_demodulation,[],[f1055,f1106]) ).
fof(f4215,plain,
( op2(e20,e22) != h3(op1(e10,e13))
| ~ spl36_25
| spl36_92
| ~ spl36_105 ),
inference(forward_demodulation,[],[f4213,f741]) ).
fof(f4217,plain,
( op2(e20,e22) != h3(e13)
| ~ spl36_25
| spl36_92
| ~ spl36_105
| ~ spl36_226 ),
inference(forward_demodulation,[],[f4215,f1728]) ).
fof(f4219,plain,
( e22 != op2(e20,e22)
| ~ spl36_25
| spl36_92
| ~ spl36_105
| ~ spl36_226 ),
inference(forward_demodulation,[],[f4217,f1106]) ).
fof(f4220,plain,
( $false
| ~ spl36_25
| spl36_92
| ~ spl36_105
| ~ spl36_162
| ~ spl36_226 ),
inference(forward_subsumption_resolution,[],[f4219,f1396]) ).
fof(f4221,plain,
( ~ spl36_25
| spl36_92
| ~ spl36_105
| ~ spl36_162
| ~ spl36_226 ),
inference(avatar_contradiction_clause,[],[f4220]) ).
fof(f4223,plain,
( h3(op1(e11,e10)) != op2(h3(e11),e20)
| ~ spl36_25
| spl36_93 ),
inference(forward_demodulation,[],[f1059,f741]) ).
fof(f4225,plain,
( op2(e21,e20) != h3(op1(e11,e10))
| ~ spl36_25
| ~ spl36_29
| spl36_93 ),
inference(forward_demodulation,[],[f4223,f760]) ).
fof(f4227,plain,
( op2(e21,e20) != h3(e10)
| ~ spl36_25
| ~ spl36_29
| spl36_93
| ~ spl36_195 ),
inference(forward_demodulation,[],[f4225,f1571]) ).
fof(f4229,plain,
( e20 != op2(e21,e20)
| ~ spl36_25
| ~ spl36_29
| spl36_93
| ~ spl36_195 ),
inference(forward_demodulation,[],[f4227,f741]) ).
fof(f4230,plain,
( $false
| ~ spl36_25
| ~ spl36_29
| spl36_93
| ~ spl36_141
| ~ spl36_195 ),
inference(forward_subsumption_resolution,[],[f4229,f1291]) ).
fof(f4231,plain,
( ~ spl36_25
| ~ spl36_29
| spl36_93
| ~ spl36_141
| ~ spl36_195 ),
inference(avatar_contradiction_clause,[],[f4230]) ).
fof(f4233,plain,
( op2(e21,e21) != h3(op1(e11,e11))
| ~ spl36_29
| spl36_94 ),
inference(forward_demodulation,[],[f1063,f760]) ).
fof(f4235,plain,
( op2(e21,e21) != h3(e11)
| ~ spl36_29
| spl36_94
| ~ spl36_194 ),
inference(forward_demodulation,[],[f4233,f1565]) ).
fof(f4237,plain,
( e21 != op2(e21,e21)
| ~ spl36_29
| spl36_94
| ~ spl36_194 ),
inference(forward_demodulation,[],[f4235,f760]) ).
fof(f4239,plain,
( $false
| ~ spl36_29
| spl36_94
| ~ spl36_140
| ~ spl36_194 ),
inference(forward_subsumption_resolution,[],[f4237,f1285]) ).
fof(f4240,plain,
( ~ spl36_29
| spl36_94
| ~ spl36_140
| ~ spl36_194 ),
inference(avatar_contradiction_clause,[],[f4239]) ).
fof(f4242,plain,
( h3(op1(e11,e12)) != op2(h3(e11),e23)
| spl36_95
| ~ spl36_111 ),
inference(forward_demodulation,[],[f1067,f1138]) ).
fof(f4244,plain,
( op2(e21,e23) != h3(op1(e11,e12))
| ~ spl36_29
| spl36_95
| ~ spl36_111 ),
inference(forward_demodulation,[],[f4242,f760]) ).
fof(f4246,plain,
( op2(e21,e23) != h3(e13)
| ~ spl36_29
| spl36_95
| ~ spl36_111
| ~ spl36_287 ),
inference(forward_demodulation,[],[f4244,f2061]) ).
fof(f4247,plain,
( e22 != op2(e21,e23)
| ~ spl36_29
| spl36_95
| ~ spl36_105
| ~ spl36_111
| ~ spl36_287 ),
inference(forward_demodulation,[],[f4246,f1106]) ).
fof(f4248,plain,
( $false
| ~ spl36_29
| spl36_95
| ~ spl36_105
| ~ spl36_111
| ~ spl36_261
| ~ spl36_287 ),
inference(forward_subsumption_resolution,[],[f4247,f1907]) ).
fof(f4249,plain,
( ~ spl36_29
| spl36_95
| ~ spl36_105
| ~ spl36_111
| ~ spl36_261
| ~ spl36_287 ),
inference(avatar_contradiction_clause,[],[f4248]) ).
fof(f4251,plain,
( h3(op1(e11,e13)) != op2(h3(e11),e22)
| spl36_96
| ~ spl36_105 ),
inference(forward_demodulation,[],[f1071,f1106]) ).
fof(f4253,plain,
( op2(e21,e22) != h3(op1(e11,e13))
| ~ spl36_29
| spl36_96
| ~ spl36_105 ),
inference(forward_demodulation,[],[f4251,f760]) ).
fof(f4255,plain,
( op2(e21,e22) != h3(e12)
| ~ spl36_29
| spl36_96
| ~ spl36_105
| ~ spl36_285 ),
inference(forward_demodulation,[],[f4253,f2051]) ).
fof(f4257,plain,
( e23 != op2(e21,e22)
| ~ spl36_29
| spl36_96
| ~ spl36_105
| ~ spl36_111
| ~ spl36_285 ),
inference(forward_demodulation,[],[f4255,f1138]) ).
fof(f4258,plain,
( $false
| ~ spl36_29
| spl36_96
| ~ spl36_105
| ~ spl36_111
| ~ spl36_263
| ~ spl36_285 ),
inference(forward_subsumption_resolution,[],[f4257,f1917]) ).
fof(f4259,plain,
( ~ spl36_29
| spl36_96
| ~ spl36_105
| ~ spl36_111
| ~ spl36_263
| ~ spl36_285 ),
inference(avatar_contradiction_clause,[],[f4258]) ).
fof(f4261,plain,
( h3(op1(e12,e10)) != op2(h3(e12),e20)
| ~ spl36_25
| spl36_97 ),
inference(forward_demodulation,[],[f1075,f741]) ).
fof(f4263,plain,
( op2(e23,e20) != h3(op1(e12,e10))
| ~ spl36_25
| spl36_97
| ~ spl36_111 ),
inference(forward_demodulation,[],[f4261,f1138]) ).
fof(f4265,plain,
( op2(e23,e20) != h3(e12)
| ~ spl36_25
| spl36_97
| ~ spl36_111
| ~ spl36_217 ),
inference(forward_demodulation,[],[f4263,f1681]) ).
fof(f4267,plain,
( e23 != op2(e23,e20)
| ~ spl36_25
| spl36_97
| ~ spl36_111
| ~ spl36_217 ),
inference(forward_demodulation,[],[f4265,f1138]) ).
fof(f4268,plain,
( $false
| ~ spl36_25
| spl36_97
| ~ spl36_111
| ~ spl36_173
| ~ spl36_217 ),
inference(forward_subsumption_resolution,[],[f4267,f1453]) ).
fof(f4269,plain,
( ~ spl36_25
| spl36_97
| ~ spl36_111
| ~ spl36_173
| ~ spl36_217 ),
inference(avatar_contradiction_clause,[],[f4268]) ).
fof(f4271,plain,
( h3(op1(e12,e11)) != op2(h3(e12),e21)
| ~ spl36_29
| spl36_98 ),
inference(forward_demodulation,[],[f1079,f760]) ).
fof(f4273,plain,
( op2(e23,e21) != h3(op1(e12,e11))
| ~ spl36_29
| spl36_98
| ~ spl36_111 ),
inference(forward_demodulation,[],[f4271,f1138]) ).
fof(f4275,plain,
( op2(e23,e21) != h3(e13)
| ~ spl36_29
| spl36_98
| ~ spl36_111
| ~ spl36_288 ),
inference(forward_demodulation,[],[f4273,f2066]) ).
fof(f4277,plain,
( e22 != op2(e23,e21)
| ~ spl36_29
| spl36_98
| ~ spl36_105
| ~ spl36_111
| ~ spl36_288 ),
inference(forward_demodulation,[],[f4275,f1106]) ).
fof(f4278,plain,
( $false
| ~ spl36_29
| spl36_98
| ~ spl36_105
| ~ spl36_111
| ~ spl36_262
| ~ spl36_288 ),
inference(forward_subsumption_resolution,[],[f4277,f1912]) ).
fof(f4279,plain,
( ~ spl36_29
| spl36_98
| ~ spl36_105
| ~ spl36_111
| ~ spl36_262
| ~ spl36_288 ),
inference(avatar_contradiction_clause,[],[f4278]) ).
fof(f4281,plain,
( op2(e23,e23) != h3(op1(e12,e12))
| spl36_99
| ~ spl36_111 ),
inference(forward_demodulation,[],[f1083,f1138]) ).
fof(f4283,plain,
( op2(e23,e23) != h3(e10)
| spl36_99
| ~ spl36_111
| ~ spl36_239 ),
inference(forward_demodulation,[],[f4281,f1800]) ).
fof(f4285,plain,
( e20 != op2(e23,e23)
| ~ spl36_25
| spl36_99
| ~ spl36_111
| ~ spl36_239 ),
inference(forward_demodulation,[],[f4283,f741]) ).
fof(f4287,plain,
( $false
| ~ spl36_25
| spl36_99
| ~ spl36_111
| ~ spl36_188
| ~ spl36_239 ),
inference(forward_subsumption_resolution,[],[f4285,f1535]) ).
fof(f4288,plain,
( ~ spl36_25
| spl36_99
| ~ spl36_111
| ~ spl36_188
| ~ spl36_239 ),
inference(avatar_contradiction_clause,[],[f4287]) ).
fof(f4290,plain,
( h3(op1(e12,e13)) != op2(h3(e12),e22)
| spl36_100
| ~ spl36_105 ),
inference(forward_demodulation,[],[f1087,f1106]) ).
fof(f4292,plain,
( op2(e23,e22) != h3(op1(e12,e13))
| spl36_100
| ~ spl36_105
| ~ spl36_111 ),
inference(forward_demodulation,[],[f4290,f1138]) ).
fof(f4294,plain,
( op2(e23,e22) != h3(e11)
| spl36_100
| ~ spl36_105
| ~ spl36_111
| ~ spl36_291 ),
inference(forward_demodulation,[],[f4292,f2081]) ).
fof(f4295,plain,
( e21 != op2(e23,e22)
| ~ spl36_29
| spl36_100
| ~ spl36_105
| ~ spl36_111
| ~ spl36_291 ),
inference(forward_demodulation,[],[f4294,f760]) ).
fof(f4296,plain,
( $false
| ~ spl36_29
| spl36_100
| ~ spl36_105
| ~ spl36_111
| ~ spl36_268
| ~ spl36_291 ),
inference(forward_subsumption_resolution,[],[f4295,f1942]) ).
fof(f4297,plain,
( ~ spl36_29
| spl36_100
| ~ spl36_105
| ~ spl36_111
| ~ spl36_268
| ~ spl36_291 ),
inference(avatar_contradiction_clause,[],[f4296]) ).
fof(f4299,plain,
( h3(op1(e13,e10)) != op2(h3(e13),e20)
| ~ spl36_25
| spl36_101 ),
inference(forward_demodulation,[],[f1091,f741]) ).
fof(f4301,plain,
( op2(e22,e20) != h3(op1(e13,e10))
| ~ spl36_25
| spl36_101
| ~ spl36_105 ),
inference(forward_demodulation,[],[f4299,f1106]) ).
fof(f4303,plain,
( op2(e22,e20) != h3(e13)
| ~ spl36_25
| spl36_101
| ~ spl36_105
| ~ spl36_227 ),
inference(forward_demodulation,[],[f4301,f1733]) ).
fof(f4305,plain,
( e22 != op2(e22,e20)
| ~ spl36_25
| spl36_101
| ~ spl36_105
| ~ spl36_227 ),
inference(forward_demodulation,[],[f4303,f1106]) ).
fof(f4306,plain,
( $false
| ~ spl36_25
| spl36_101
| ~ spl36_105
| ~ spl36_163
| ~ spl36_227 ),
inference(forward_subsumption_resolution,[],[f4305,f1401]) ).
fof(f4307,plain,
( ~ spl36_25
| spl36_101
| ~ spl36_105
| ~ spl36_163
| ~ spl36_227 ),
inference(avatar_contradiction_clause,[],[f4306]) ).
fof(f4309,plain,
( h3(op1(e13,e11)) != op2(h3(e13),e21)
| ~ spl36_29
| spl36_102 ),
inference(forward_demodulation,[],[f1095,f760]) ).
fof(f4311,plain,
( op2(e22,e21) != h3(op1(e13,e11))
| ~ spl36_29
| spl36_102
| ~ spl36_105 ),
inference(forward_demodulation,[],[f4309,f1106]) ).
fof(f4313,plain,
( op2(e22,e21) != h3(e12)
| ~ spl36_29
| spl36_102
| ~ spl36_105
| ~ spl36_286 ),
inference(forward_demodulation,[],[f4311,f2056]) ).
fof(f4315,plain,
( e23 != op2(e22,e21)
| ~ spl36_29
| spl36_102
| ~ spl36_105
| ~ spl36_111
| ~ spl36_286 ),
inference(forward_demodulation,[],[f4313,f1138]) ).
fof(f4316,plain,
( $false
| ~ spl36_29
| spl36_102
| ~ spl36_105
| ~ spl36_111
| ~ spl36_264
| ~ spl36_286 ),
inference(forward_subsumption_resolution,[],[f4315,f1922]) ).
fof(f4317,plain,
( ~ spl36_29
| spl36_102
| ~ spl36_105
| ~ spl36_111
| ~ spl36_264
| ~ spl36_286 ),
inference(avatar_contradiction_clause,[],[f4316]) ).
fof(f4319,plain,
( h3(op1(e13,e12)) != op2(h3(e13),e23)
| spl36_103
| ~ spl36_111 ),
inference(forward_demodulation,[],[f1099,f1138]) ).
fof(f4321,plain,
( op2(e22,e23) != h3(op1(e13,e12))
| spl36_103
| ~ spl36_105
| ~ spl36_111 ),
inference(forward_demodulation,[],[f4319,f1106]) ).
fof(f4323,plain,
( op2(e22,e23) != h3(e11)
| spl36_103
| ~ spl36_105
| ~ spl36_111
| ~ spl36_292 ),
inference(forward_demodulation,[],[f4321,f2086]) ).
fof(f4325,plain,
( e21 != op2(e22,e23)
| ~ spl36_29
| spl36_103
| ~ spl36_105
| ~ spl36_111
| ~ spl36_292 ),
inference(forward_demodulation,[],[f4323,f760]) ).
fof(f4326,plain,
( $false
| ~ spl36_29
| spl36_103
| ~ spl36_105
| ~ spl36_111
| ~ spl36_267
| ~ spl36_292 ),
inference(forward_subsumption_resolution,[],[f4325,f1937]) ).
fof(f4327,plain,
( ~ spl36_29
| spl36_103
| ~ spl36_105
| ~ spl36_111
| ~ spl36_267
| ~ spl36_292 ),
inference(avatar_contradiction_clause,[],[f4326]) ).
fof(f4329,plain,
( op2(e22,e22) != h3(op1(e13,e13))
| spl36_104
| ~ spl36_105 ),
inference(forward_demodulation,[],[f1103,f1106]) ).
fof(f4331,plain,
( op2(e22,e22) != h3(e10)
| spl36_104
| ~ spl36_105
| ~ spl36_242 ),
inference(forward_demodulation,[],[f4329,f1815]) ).
fof(f4333,plain,
( e20 != op2(e22,e22)
| ~ spl36_25
| spl36_104
| ~ spl36_105
| ~ spl36_242 ),
inference(forward_demodulation,[],[f4331,f741]) ).
fof(f4344,plain,
( e11 != op1(e10,e13)
| ~ spl36_233 ),
inference(forward_demodulation,[],[f138,f1770]) ).
fof(f4346,plain,
( e12 != op1(e10,e13)
| ~ spl36_285 ),
inference(forward_demodulation,[],[f146,f2051]) ).
fof(f4349,plain,
( ~ spl36_204
| ~ spl36_242 ),
inference(avatar_split_clause,[],[f3434,f1814,f1612]) ).
fof(f4355,plain,
( ~ spl36_270
| ~ spl36_233 ),
inference(avatar_split_clause,[],[f4344,f1769,f1979]) ).
fof(f4357,plain,
( ~ spl36_274
| ~ spl36_285 ),
inference(avatar_split_clause,[],[f4346,f2049,f1997]) ).
fof(f4373,plain,
( ~ spl36_232
| ~ spl36_227 ),
inference(avatar_split_clause,[],[f3549,f1731,f1757]) ).
fof(f4417,plain,
( spl36_285
| ~ spl36_233
| ~ spl36_242 ),
inference(avatar_split_clause,[],[f3879,f1814,f1769,f2049]) ).
fof(f4433,plain,
( e11 != op1(e11,e10)
| ~ spl36_233 ),
inference(forward_demodulation,[],[f164,f1770]) ).
fof(f4444,plain,
( ~ spl36_207
| ~ spl36_233 ),
inference(avatar_split_clause,[],[f4433,f1769,f1627]) ).
fof(f4453,plain,
( ~ spl36_185
| ~ spl36_25
| spl36_104
| ~ spl36_105
| ~ spl36_242 ),
inference(avatar_split_clause,[],[f4333,f1814,f1105,f1101,f740,f1519]) ).
fof(f4463,plain,
( ~ spl36_144
| ~ spl36_169 ),
inference(avatar_split_clause,[],[f3501,f1431,f1303]) ).
fof(f4472,plain,
( ~ spl36_231
| ~ spl36_226 ),
inference(avatar_split_clause,[],[f3547,f1726,f1752]) ).
fof(f4475,plain,
( ~ spl36_200
| ~ spl36_239 ),
inference(avatar_split_clause,[],[f3648,f1799,f1593]) ).
fof(f4481,plain,
( ~ spl36_275
| ~ spl36_285 ),
inference(avatar_split_clause,[],[f3636,f2049,f2002]) ).
fof(f4496,plain,
( ~ spl36_240
| ~ spl36_291 ),
inference(avatar_split_clause,[],[f3626,f2079,f1804]) ).
fof(f4508,plain,
( e23 != op2(e22,e23)
| ~ spl36_264 ),
inference(forward_demodulation,[],[f172,f1922]) ).
fof(f4514,plain,
( spl36_261
| ~ spl36_179
| ~ spl36_188 ),
inference(avatar_split_clause,[],[f3881,f1534,f1489,f1905]) ).
fof(f4516,plain,
( ~ spl36_255
| ~ spl36_173 ),
inference(avatar_split_clause,[],[f3517,f1451,f1876]) ).
fof(f4522,plain,
( e21 != op2(e20,e23)
| ~ spl36_179 ),
inference(forward_demodulation,[],[f186,f1490]) ).
fof(f4526,plain,
( e21 != op2(e20,e22)
| ~ spl36_179 ),
inference(forward_demodulation,[],[f187,f1490]) ).
fof(f4535,plain,
( ~ spl36_177
| ~ spl36_264 ),
inference(avatar_split_clause,[],[f4508,f1920,f1472]) ).
fof(f4539,plain,
( ~ spl36_246
| ~ spl36_179 ),
inference(avatar_split_clause,[],[f4522,f1489,f1835]) ).
fof(f4540,plain,
( ~ spl36_245
| ~ spl36_179 ),
inference(avatar_split_clause,[],[f4526,f1489,f1831]) ).
cnf(s20,plain,
( ~ spl36_21
| ~ spl36_25 ),
inference(sat_conversion,[],[f743]) ).
cnf(s23,plain,
( spl36_26
| ~ spl36_29 ),
inference(sat_conversion,[],[f762]) ).
cnf(s73,plain,
( spl36_21
| ~ spl36_26
| ~ spl36_89
| ~ spl36_90
| ~ spl36_91
| ~ spl36_92
| ~ spl36_93
| ~ spl36_94
| ~ spl36_95
| ~ spl36_96
| ~ spl36_97
| ~ spl36_98
| ~ spl36_99
| ~ spl36_100
| ~ spl36_101
| ~ spl36_102
| ~ spl36_103
| ~ spl36_104
| ~ spl36_105
| ~ spl36_111 ),
inference(sat_conversion,[],[f1140]) ).
cnf(s97,plain,
spl36_136,
inference(sat_conversion,[],[f1264]) ).
cnf(s98,plain,
spl36_105,
inference(sat_conversion,[],[f1265]) ).
cnf(s100,plain,
spl36_2,
inference(sat_conversion,[],[f1267]) ).
cnf(s152,plain,
( spl36_138
| spl36_140
| spl36_144
| spl36_148 ),
inference(sat_conversion,[],[f1487]) ).
cnf(s153,plain,
( spl36_142
| ~ spl36_179 ),
inference(sat_conversion,[],[f1492]) ).
cnf(s158,plain,
( spl36_160
| ~ spl36_184 ),
inference(sat_conversion,[],[f1517]) ).
cnf(s162,plain,
( spl36_173
| ~ spl36_188 ),
inference(sat_conversion,[],[f1537]) ).
cnf(s163,plain,
( spl36_176
| ~ spl36_189 ),
inference(sat_conversion,[],[f1542]) ).
cnf(s225,plain,
( spl36_224
| ~ spl36_241 ),
inference(sat_conversion,[],[f1812]) ).
cnf(s226,plain,
( spl36_227
| ~ spl36_242 ),
inference(sat_conversion,[],[f1817]) ).
cnf(s233,plain,
( spl36_162
| spl36_180
| spl36_249
| spl36_250 ),
inference(sat_conversion,[],[f1856]) ).
cnf(s234,plain,
( spl36_163
| spl36_180
| spl36_251
| spl36_252 ),
inference(sat_conversion,[],[f1865]) ).
cnf(s235,plain,
( spl36_172
| spl36_181
| spl36_253
| spl36_254 ),
inference(sat_conversion,[],[f1874]) ).
cnf(s237,plain,
( spl36_141
| spl36_182
| spl36_257
| spl36_258 ),
inference(sat_conversion,[],[f1892]) ).
cnf(s243,plain,
( spl36_175
| spl36_184
| spl36_255
| spl36_263 ),
inference(sat_conversion,[],[f1918]) ).
cnf(s244,plain,
( spl36_176
| spl36_184
| spl36_253
| spl36_264 ),
inference(sat_conversion,[],[f1923]) ).
cnf(s246,plain,
( spl36_146
| spl36_185
| spl36_257
| spl36_266 ),
inference(sat_conversion,[],[f1933]) ).
cnf(s248,plain,
( spl36_157
| spl36_186
| spl36_245
| spl36_268 ),
inference(sat_conversion,[],[f1943]) ).
cnf(s250,plain,
( spl36_144
| spl36_162
| spl36_165
| spl36_169 ),
inference(sat_conversion,[],[f1945]) ).
cnf(s256,plain,
( spl36_160
| spl36_189
| spl36_246
| spl36_267 ),
inference(sat_conversion,[],[f1951]) ).
cnf(s257,plain,
( spl36_169
| spl36_190
| spl36_252
| spl36_262 ),
inference(sat_conversion,[],[f1952]) ).
cnf(s260,plain,
( spl36_148
| spl36_172
| spl36_175
| spl36_177 ),
inference(sat_conversion,[],[f1955]) ).
cnf(s277,plain,
( spl36_192
| spl36_196
| spl36_200
| spl36_204 ),
inference(sat_conversion,[],[f1972]) ).
cnf(s278,plain,
( spl36_192
| spl36_195
| spl36_199
| spl36_203 ),
inference(sat_conversion,[],[f1973]) ).
cnf(s282,plain,
( spl36_217
| spl36_234
| spl36_275
| spl36_276 ),
inference(sat_conversion,[],[f2009]) ).
cnf(s287,plain,
( spl36_194
| spl36_207
| spl36_211
| spl36_214 ),
inference(sat_conversion,[],[f2046]) ).
cnf(s293,plain,
( spl36_199
| spl36_239
| spl36_283
| spl36_289 ),
inference(sat_conversion,[],[f2072]) ).
cnf(s296,plain,
( spl36_211
| spl36_240
| spl36_269
| spl36_292 ),
inference(sat_conversion,[],[f2087]) ).
cnf(s299,plain,
( spl36_231
| spl36_241
| spl36_280
| spl36_288 ),
inference(sat_conversion,[],[f2090]) ).
cnf(s300,plain,
( spl36_232
| spl36_241
| spl36_278
| spl36_287 ),
inference(sat_conversion,[],[f2091]) ).
cnf(s304,plain,
( spl36_214
| spl36_243
| spl36_270
| spl36_291 ),
inference(sat_conversion,[],[f2095]) ).
cnf(s305,plain,
( spl36_223
| spl36_244
| spl36_276
| spl36_286 ),
inference(sat_conversion,[],[f2096]) ).
cnf(s311,plain,
( spl36_200
| spl36_216
| spl36_269
| spl36_278 ),
inference(sat_conversion,[],[f2102]) ).
cnf(s312,plain,
( spl36_204
| spl36_226
| spl36_270
| spl36_274 ),
inference(sat_conversion,[],[f2103]) ).
cnf(s325,plain,
spl36_242,
inference(sat_conversion,[],[f2120]) ).
cnf(s326,plain,
spl36_188,
inference(sat_conversion,[],[f2121]) ).
cnf(s330,plain,
( ~ spl36_146
| ~ spl36_162 ),
inference(sat_conversion,[],[f2135]) ).
cnf(s333,plain,
( ~ spl36_144
| ~ spl36_185 ),
inference(sat_conversion,[],[f2146]) ).
cnf(s358,plain,
( ~ spl36_2
| spl36_7
| ~ spl36_140
| ~ spl36_182 ),
inference(sat_conversion,[],[f2265]) ).
cnf(s359,plain,
( ~ spl36_148
| ~ spl36_188 ),
inference(sat_conversion,[],[f2271]) ).
cnf(s372,plain,
( ~ spl36_203
| ~ spl36_227 ),
inference(sat_conversion,[],[f2319]) ).
cnf(s383,plain,
( ~ spl36_227
| ~ spl36_276 ),
inference(sat_conversion,[],[f2360]) ).
cnf(s387,plain,
( spl36_27
| ~ spl36_105
| ~ spl36_160
| ~ spl36_261 ),
inference(sat_conversion,[],[f2384]) ).
cnf(s408,plain,
( spl36_27
| ~ spl36_105
| ~ spl36_179
| ~ spl36_180 ),
inference(sat_conversion,[],[f2450]) ).
cnf(s412,plain,
( ~ spl36_2
| ~ spl36_7 ),
inference(sat_conversion,[],[f2480]) ).
cnf(s413,plain,
( ~ spl36_27
| ~ spl36_105 ),
inference(sat_conversion,[],[f2492]) ).
cnf(s422,plain,
( ~ spl36_37
| ~ spl36_136
| spl36_182
| ~ spl36_188 ),
inference(sat_conversion,[],[f2554]) ).
cnf(s429,plain,
( ~ spl36_142
| ~ spl36_249 ),
inference(sat_conversion,[],[f2579]) ).
cnf(s430,plain,
( ~ spl36_172
| ~ spl36_250 ),
inference(sat_conversion,[],[f2582]) ).
cnf(s432,plain,
( spl36_37
| ~ spl36_136
| ~ spl36_179
| ~ spl36_181 ),
inference(sat_conversion,[],[f2591]) ).
cnf(s436,plain,
( ~ spl36_141
| ~ spl36_251 ),
inference(sat_conversion,[],[f2609]) ).
cnf(s438,plain,
( ~ spl36_146
| ~ spl36_254 ),
inference(sat_conversion,[],[f2619]) ).
cnf(s440,plain,
( ~ spl36_142
| ~ spl36_253 ),
inference(sat_conversion,[],[f2626]) ).
cnf(s442,plain,
( ~ spl36_173
| ~ spl36_252 ),
inference(sat_conversion,[],[f2632]) ).
cnf(s452,plain,
( ~ spl36_162
| ~ spl36_254 ),
inference(sat_conversion,[],[f2691]) ).
cnf(s460,plain,
( ~ spl36_175
| ~ spl36_261 ),
inference(sat_conversion,[],[f2731]) ).
cnf(s463,plain,
( ~ spl36_176
| ~ spl36_262 ),
inference(sat_conversion,[],[f2758]) ).
cnf(s465,plain,
( ~ spl36_257
| ~ spl36_263 ),
inference(sat_conversion,[],[f2768]) ).
cnf(s468,plain,
( ~ spl36_258
| ~ spl36_261 ),
inference(sat_conversion,[],[f2779]) ).
cnf(s470,plain,
( ~ spl36_188
| ~ spl36_190 ),
inference(sat_conversion,[],[f2787]) ).
cnf(s474,plain,
( ~ spl36_165
| ~ spl36_263 ),
inference(sat_conversion,[],[f2812]) ).
cnf(s478,plain,
( ~ spl36_2
| spl36_7
| ~ spl36_185
| ~ spl36_186 ),
inference(sat_conversion,[],[f2837]) ).
cnf(s483,plain,
( spl36_37
| ~ spl36_136
| ~ spl36_157
| ~ spl36_263 ),
inference(sat_conversion,[],[f2872]) ).
cnf(s500,plain,
( spl36_27
| ~ spl36_105
| ~ spl36_169
| ~ spl36_268 ),
inference(sat_conversion,[],[f2984]) ).
cnf(s510,plain,
( ~ spl36_214
| ~ spl36_285 ),
inference(sat_conversion,[],[f3028]) ).
cnf(s511,plain,
( ~ spl36_233
| ~ spl36_234 ),
inference(sat_conversion,[],[f3034]) ).
cnf(s515,plain,
( ~ spl36_242
| ~ spl36_243 ),
inference(sat_conversion,[],[f3046]) ).
cnf(s517,plain,
( ~ spl36_242
| ~ spl36_244 ),
inference(sat_conversion,[],[f3067]) ).
cnf(s521,plain,
( ~ spl36_199
| ~ spl36_217 ),
inference(sat_conversion,[],[f3087]) ).
cnf(s528,plain,
( ~ spl36_211
| ~ spl36_287 ),
inference(sat_conversion,[],[f3132]) ).
cnf(s547,plain,
( ~ spl36_283
| ~ spl36_288 ),
inference(sat_conversion,[],[f3246]) ).
cnf(s562,plain,
( ~ spl36_223
| ~ spl36_292 ),
inference(sat_conversion,[],[f3363]) ).
cnf(s571,plain,
( ~ spl36_192
| ~ spl36_242 ),
inference(sat_conversion,[],[f3526]) ).
cnf(s572,plain,
( ~ spl36_227
| ~ spl36_280 ),
inference(sat_conversion,[],[f3532]) ).
cnf(s573,plain,
( ~ spl36_226
| ~ spl36_278 ),
inference(sat_conversion,[],[f3533]) ).
cnf(s575,plain,
( ~ spl36_217
| ~ spl36_224 ),
inference(sat_conversion,[],[f3536]) ).
cnf(s579,plain,
( ~ spl36_233
| ~ spl36_269 ),
inference(sat_conversion,[],[f3542]) ).
cnf(s580,plain,
( spl36_233
| ~ spl36_242 ),
inference(sat_conversion,[],[f3543]) ).
cnf(s582,plain,
( ~ spl36_242
| ~ spl36_289 ),
inference(sat_conversion,[],[f3546]) ).
cnf(s589,plain,
( ~ spl36_2
| spl36_7
| ~ spl36_138
| ~ spl36_188 ),
inference(sat_conversion,[],[f3662]) ).
cnf(s592,plain,
( ~ spl36_188
| ~ spl36_266 ),
inference(sat_conversion,[],[f3669]) ).
cnf(s596,plain,
( spl36_179
| ~ spl36_188 ),
inference(sat_conversion,[],[f3680]) ).
cnf(s616,plain,
( spl36_25
| ~ spl36_185 ),
inference(sat_conversion,[],[f3782]) ).
cnf(s619,plain,
( spl36_29
| ~ spl36_179
| ~ spl36_185 ),
inference(sat_conversion,[],[f3838]) ).
cnf(s621,plain,
( ~ spl36_25
| ~ spl36_29
| spl36_90
| ~ spl36_142
| ~ spl36_196 ),
inference(sat_conversion,[],[f3847]) ).
cnf(s622,plain,
( ~ spl36_25
| ~ spl36_29
| spl36_89
| ~ spl36_179
| ~ spl36_233 ),
inference(sat_conversion,[],[f3855]) ).
cnf(s672,plain,
( spl36_111
| ~ spl36_179
| ~ spl36_185
| ~ spl36_263 ),
inference(sat_conversion,[],[f4207]) ).
cnf(s673,plain,
( ~ spl36_25
| spl36_91
| ~ spl36_111
| ~ spl36_172
| ~ spl36_216 ),
inference(sat_conversion,[],[f4211]) ).
cnf(s674,plain,
( ~ spl36_25
| spl36_92
| ~ spl36_105
| ~ spl36_162
| ~ spl36_226 ),
inference(sat_conversion,[],[f4221]) ).
cnf(s675,plain,
( ~ spl36_25
| ~ spl36_29
| spl36_93
| ~ spl36_141
| ~ spl36_195 ),
inference(sat_conversion,[],[f4231]) ).
cnf(s676,plain,
( ~ spl36_29
| spl36_94
| ~ spl36_140
| ~ spl36_194 ),
inference(sat_conversion,[],[f4240]) ).
cnf(s677,plain,
( ~ spl36_29
| spl36_95
| ~ spl36_105
| ~ spl36_111
| ~ spl36_261
| ~ spl36_287 ),
inference(sat_conversion,[],[f4249]) ).
cnf(s678,plain,
( ~ spl36_29
| spl36_96
| ~ spl36_105
| ~ spl36_111
| ~ spl36_263
| ~ spl36_285 ),
inference(sat_conversion,[],[f4259]) ).
cnf(s679,plain,
( ~ spl36_25
| spl36_97
| ~ spl36_111
| ~ spl36_173
| ~ spl36_217 ),
inference(sat_conversion,[],[f4269]) ).
cnf(s680,plain,
( ~ spl36_29
| spl36_98
| ~ spl36_105
| ~ spl36_111
| ~ spl36_262
| ~ spl36_288 ),
inference(sat_conversion,[],[f4279]) ).
cnf(s681,plain,
( ~ spl36_25
| spl36_99
| ~ spl36_111
| ~ spl36_188
| ~ spl36_239 ),
inference(sat_conversion,[],[f4288]) ).
cnf(s682,plain,
( ~ spl36_29
| spl36_100
| ~ spl36_105
| ~ spl36_111
| ~ spl36_268
| ~ spl36_291 ),
inference(sat_conversion,[],[f4297]) ).
cnf(s683,plain,
( ~ spl36_25
| spl36_101
| ~ spl36_105
| ~ spl36_163
| ~ spl36_227 ),
inference(sat_conversion,[],[f4307]) ).
cnf(s684,plain,
( ~ spl36_29
| spl36_102
| ~ spl36_105
| ~ spl36_111
| ~ spl36_264
| ~ spl36_286 ),
inference(sat_conversion,[],[f4317]) ).
cnf(s685,plain,
( ~ spl36_29
| spl36_103
| ~ spl36_105
| ~ spl36_111
| ~ spl36_267
| ~ spl36_292 ),
inference(sat_conversion,[],[f4327]) ).
cnf(s688,plain,
( ~ spl36_204
| ~ spl36_242 ),
inference(sat_conversion,[],[f4349]) ).
cnf(s691,plain,
( ~ spl36_233
| ~ spl36_270 ),
inference(sat_conversion,[],[f4355]) ).
cnf(s693,plain,
( ~ spl36_274
| ~ spl36_285 ),
inference(sat_conversion,[],[f4357]) ).
cnf(s696,plain,
( ~ spl36_227
| ~ spl36_232 ),
inference(sat_conversion,[],[f4373]) ).
cnf(s706,plain,
( ~ spl36_233
| ~ spl36_242
| spl36_285 ),
inference(sat_conversion,[],[f4417]) ).
cnf(s713,plain,
( ~ spl36_207
| ~ spl36_233 ),
inference(sat_conversion,[],[f4444]) ).
cnf(s714,plain,
( ~ spl36_25
| spl36_104
| ~ spl36_105
| ~ spl36_185
| ~ spl36_242 ),
inference(sat_conversion,[],[f4453]) ).
cnf(s718,plain,
( ~ spl36_144
| ~ spl36_169 ),
inference(sat_conversion,[],[f4463]) ).
cnf(s730,plain,
( ~ spl36_226
| ~ spl36_231 ),
inference(sat_conversion,[],[f4472]) ).
cnf(s734,plain,
( ~ spl36_200
| ~ spl36_239 ),
inference(sat_conversion,[],[f4475]) ).
cnf(s739,plain,
( ~ spl36_275
| ~ spl36_285 ),
inference(sat_conversion,[],[f4481]) ).
cnf(s745,plain,
( ~ spl36_240
| ~ spl36_291 ),
inference(sat_conversion,[],[f4496]) ).
cnf(s753,plain,
( ~ spl36_179
| ~ spl36_188
| spl36_261 ),
inference(sat_conversion,[],[f4514]) ).
cnf(s756,plain,
( ~ spl36_173
| ~ spl36_255 ),
inference(sat_conversion,[],[f4516]) ).
cnf(s767,plain,
( ~ spl36_177
| ~ spl36_264 ),
inference(sat_conversion,[],[f4535]) ).
cnf(s771,plain,
( ~ spl36_179
| ~ spl36_246 ),
inference(sat_conversion,[],[f4539]) ).
cnf(s773,plain,
( ~ spl36_179
| ~ spl36_245 ),
inference(sat_conversion,[],[f4540]) ).
cnf(s778,plain,
spl36_179,
inference(rat,[],[s596,s326]) ).
cnf(s779,plain,
~ spl36_266,
inference(rat,[],[s592,s326]) ).
cnf(s781,plain,
~ spl36_190,
inference(rat,[],[s470,s326]) ).
cnf(s782,plain,
~ spl36_148,
inference(rat,[],[s359,s326]) ).
cnf(s783,plain,
~ spl36_245,
inference(rat,[],[s773,s778]) ).
cnf(s784,plain,
~ spl36_246,
inference(rat,[],[s771,s778]) ).
cnf(s785,plain,
spl36_261,
inference(rat,[],[s753,s326,s778]) ).
cnf(s789,plain,
~ spl36_258,
inference(rat,[],[s468,s785]) ).
cnf(s790,plain,
~ spl36_175,
inference(rat,[],[s460,s785]) ).
cnf(s791,plain,
~ spl36_204,
inference(rat,[],[s688,s325]) ).
cnf(s793,plain,
~ spl36_289,
inference(rat,[],[s582,s325]) ).
cnf(s794,plain,
spl36_233,
inference(rat,[],[s580,s325]) ).
cnf(s795,plain,
~ spl36_192,
inference(rat,[],[s571,s325]) ).
cnf(s796,plain,
~ spl36_244,
inference(rat,[],[s517,s325]) ).
cnf(s797,plain,
~ spl36_243,
inference(rat,[],[s515,s325]) ).
cnf(s799,plain,
~ spl36_207,
inference(rat,[],[s713,s794]) ).
cnf(s801,plain,
spl36_285,
inference(rat,[],[s706,s325,s794]) ).
cnf(s802,plain,
~ spl36_270,
inference(rat,[],[s691,s794]) ).
cnf(s803,plain,
~ spl36_269,
inference(rat,[],[s579,s794]) ).
cnf(s804,plain,
~ spl36_234,
inference(rat,[],[s511,s794]) ).
cnf(s806,plain,
~ spl36_275,
inference(rat,[],[s739,s801]) ).
cnf(s808,plain,
~ spl36_274,
inference(rat,[],[s693,s801]) ).
cnf(s810,plain,
~ spl36_214,
inference(rat,[],[s510,s801]) ).
cnf(s816,plain,
spl36_226,
inference(rat,[],[s312,s808,s802,s791]) ).
cnf(s817,plain,
~ spl36_231,
inference(rat,[],[s730,s816]) ).
cnf(s820,plain,
~ spl36_278,
inference(rat,[],[s573,s816]) ).
cnf(s822,plain,
( spl36_200
| spl36_216 ),
inference(rat,[],[s311,s820,s803]) ).
cnf(s825,plain,
( spl36_223
| spl36_276
| spl36_286 ),
inference(rat,[],[s305,s796]) ).
cnf(s826,plain,
spl36_291,
inference(rat,[],[s304,s802,s797,s810]) ).
cnf(s827,plain,
~ spl36_240,
inference(rat,[],[s745,s826]) ).
cnf(s829,plain,
( spl36_232
| spl36_241
| spl36_287 ),
inference(rat,[],[s300,s820]) ).
cnf(s830,plain,
( spl36_241
| spl36_280
| spl36_288 ),
inference(rat,[],[s299,s817]) ).
cnf(s832,plain,
( spl36_211
| spl36_292 ),
inference(rat,[],[s296,s803,s827]) ).
cnf(s834,plain,
( spl36_199
| spl36_239
| spl36_283 ),
inference(rat,[],[s293,s793]) ).
cnf(s837,plain,
( spl36_194
| spl36_211 ),
inference(rat,[],[s287,s810,s799]) ).
cnf(s840,plain,
( spl36_217
| spl36_276 ),
inference(rat,[],[s282,s806,s804]) ).
cnf(s842,plain,
( spl36_195
| spl36_199
| spl36_203 ),
inference(rat,[],[s278,s795]) ).
cnf(s843,plain,
( spl36_196
| spl36_200 ),
inference(rat,[],[s277,s791,s795]) ).
cnf(s849,plain,
( spl36_172
| spl36_177 ),
inference(rat,[],[s260,s790,s782]) ).
cnf(s851,plain,
( spl36_169
| spl36_252
| spl36_262 ),
inference(rat,[],[s257,s781]) ).
cnf(s852,plain,
( spl36_160
| spl36_189
| spl36_267 ),
inference(rat,[],[s256,s784]) ).
cnf(s853,plain,
( spl36_157
| spl36_186
| spl36_268 ),
inference(rat,[],[s248,s783]) ).
cnf(s855,plain,
( spl36_146
| spl36_185
| spl36_257 ),
inference(rat,[],[s246,s779]) ).
cnf(s857,plain,
( spl36_184
| spl36_255
| spl36_263 ),
inference(rat,[],[s243,s790]) ).
cnf(s858,plain,
( spl36_141
| spl36_182
| spl36_257 ),
inference(rat,[],[s237,s789]) ).
cnf(s859,plain,
spl36_227,
inference(rat,[],[s226,s325]) ).
cnf(s860,plain,
~ spl36_232,
inference(rat,[],[s696,s859]) ).
cnf(s861,plain,
~ spl36_280,
inference(rat,[],[s572,s859]) ).
cnf(s863,plain,
~ spl36_276,
inference(rat,[],[s383,s859]) ).
cnf(s864,plain,
~ spl36_203,
inference(rat,[],[s372,s859]) ).
cnf(s865,plain,
spl36_217,
inference(rat,[],[s840,s863]) ).
cnf(s866,plain,
~ spl36_224,
inference(rat,[],[s575,s865]) ).
cnf(s867,plain,
~ spl36_199,
inference(rat,[],[s521,s865]) ).
cnf(s868,plain,
spl36_195,
inference(rat,[],[s842,s864,s867]) ).
cnf(s870,plain,
~ spl36_241,
inference(rat,[],[s225,s866]) ).
cnf(s871,plain,
spl36_287,
inference(rat,[],[s829,s860,s870]) ).
cnf(s872,plain,
spl36_288,
inference(rat,[],[s830,s861,s870]) ).
cnf(s874,plain,
~ spl36_211,
inference(rat,[],[s528,s871]) ).
cnf(s876,plain,
~ spl36_283,
inference(rat,[],[s547,s872]) ).
cnf(s878,plain,
spl36_292,
inference(rat,[],[s832,s874]) ).
cnf(s879,plain,
spl36_194,
inference(rat,[],[s837,s874]) ).
cnf(s880,plain,
spl36_239,
inference(rat,[],[s834,s867,s876]) ).
cnf(s882,plain,
~ spl36_223,
inference(rat,[],[s562,s878]) ).
cnf(s884,plain,
~ spl36_200,
inference(rat,[],[s734,s880]) ).
cnf(s886,plain,
spl36_286,
inference(rat,[],[s825,s863,s882]) ).
cnf(s887,plain,
spl36_216,
inference(rat,[],[s822,s884]) ).
cnf(s888,plain,
spl36_196,
inference(rat,[],[s843,s884]) ).
cnf(s911,plain,
spl36_173,
inference(rat,[],[s162,s326]) ).
cnf(s912,plain,
~ spl36_255,
inference(rat,[],[s756,s911]) ).
cnf(s915,plain,
~ spl36_252,
inference(rat,[],[s442,s911]) ).
cnf(s917,plain,
spl36_142,
inference(rat,[],[s153,s778]) ).
cnf(s918,plain,
~ spl36_253,
inference(rat,[],[s440,s917]) ).
cnf(s919,plain,
~ spl36_249,
inference(rat,[],[s429,s917]) ).
cnf(s920,plain,
( spl36_138
| spl36_140
| spl36_144 ),
inference(rat,[],[s152,s782]) ).
cnf(s931,plain,
~ spl36_7,
inference(rat,[],[s412,s100]) ).
cnf(s932,plain,
~ spl36_138,
inference(rat,[],[s589,s326,s100,s931]) ).
cnf(s939,plain,
~ spl36_27,
inference(rat,[],[s413,s98]) ).
cnf(s940,plain,
~ spl36_180,
inference(rat,[],[s408,s98,s778,s939]) ).
cnf(s941,plain,
~ spl36_160,
inference(rat,[],[s387,s785,s98,s939]) ).
cnf(s942,plain,
~ spl36_184,
inference(rat,[],[s158,s941]) ).
cnf(s945,plain,
spl36_263,
inference(rat,[],[s857,s912,s942]) ).
cnf(s946,plain,
~ spl36_165,
inference(rat,[],[s474,s945]) ).
cnf(s947,plain,
~ spl36_257,
inference(rat,[],[s465,s945]) ).
cnf(s966,plain,
( spl36_21
| ~ spl36_26
| ~ spl36_89
| ~ spl36_90
| ~ spl36_91
| ~ spl36_92
| ~ spl36_93
| ~ spl36_94
| ~ spl36_95
| ~ spl36_96
| ~ spl36_97
| ~ spl36_98
| ~ spl36_99
| ~ spl36_100
| ~ spl36_101
| ~ spl36_102
| ~ spl36_103
| ~ spl36_104
| ~ spl36_111 ),
inference(rat,[],[s73,s98]) ).
cnf(s990,plain,
~ spl36_144,
inference(rat,[],[s849,s430,s767,s233,s244,s330,s463,s855,s851,s333,s718,s919,s940,s918,s942,s947,s915]) ).
cnf(s992,plain,
spl36_140,
inference(rat,[],[s920,s932,s990]) ).
cnf(s1000,plain,
~ spl36_182,
inference(rat,[],[s358,s931,s100,s992]) ).
cnf(s1021,plain,
spl36_141,
inference(rat,[],[s858,s947,s1000]) ).
cnf(s1022,plain,
~ spl36_37,
inference(rat,[],[s422,s326,s97,s1000]) ).
cnf(s1024,plain,
~ spl36_251,
inference(rat,[],[s436,s1021]) ).
cnf(s1028,plain,
~ spl36_157,
inference(rat,[],[s483,s945,s97,s1022]) ).
cnf(s1029,plain,
~ spl36_181,
inference(rat,[],[s432,s97,s778,s1022]) ).
cnf(s1031,plain,
spl36_163,
inference(rat,[],[s234,s915,s940,s1024]) ).
cnf(s1045,plain,
~ spl36_146,
inference(rat,[],[s430,s233,s235,s330,s438,s919,s940,s918,s1029]) ).
cnf(s1046,plain,
spl36_185,
inference(rat,[],[s855,s947,s1045]) ).
cnf(s1047,plain,
spl36_25,
inference(rat,[],[s616,s1046]) ).
cnf(s1049,plain,
spl36_111,
inference(rat,[],[s672,s945,s778,s1046]) ).
cnf(s1050,plain,
spl36_29,
inference(rat,[],[s619,s778,s1046]) ).
cnf(s1051,plain,
~ spl36_186,
inference(rat,[],[s478,s931,s100,s1046]) ).
cnf(s1052,plain,
spl36_104,
inference(rat,[],[s714,s325,s1046,s98,s1047]) ).
cnf(s1053,plain,
spl36_101,
inference(rat,[],[s683,s859,s1031,s98,s1047]) ).
cnf(s1054,plain,
spl36_99,
inference(rat,[],[s681,s880,s326,s1049,s1047]) ).
cnf(s1055,plain,
spl36_97,
inference(rat,[],[s679,s865,s911,s1049,s1047]) ).
cnf(s1056,plain,
~ spl36_21,
inference(rat,[],[s20,s1047]) ).
cnf(s1057,plain,
spl36_96,
inference(rat,[],[s678,s801,s945,s1049,s98,s1050]) ).
cnf(s1058,plain,
spl36_95,
inference(rat,[],[s677,s871,s785,s1049,s98,s1050]) ).
cnf(s1059,plain,
spl36_94,
inference(rat,[],[s676,s879,s992,s1050]) ).
cnf(s1060,plain,
spl36_89,
inference(rat,[],[s622,s794,s778,s1047,s1050]) ).
cnf(s1061,plain,
spl36_90,
inference(rat,[],[s621,s888,s917,s1047,s1050]) ).
cnf(s1062,plain,
spl36_26,
inference(rat,[],[s23,s1050]) ).
cnf(s1063,plain,
spl36_93,
inference(rat,[],[s675,s868,s1021,s1047,s1050]) ).
cnf(s1064,plain,
spl36_268,
inference(rat,[],[s853,s1028,s1051]) ).
cnf(s1065,plain,
~ spl36_169,
inference(rat,[],[s500,s939,s98,s1064]) ).
cnf(s1066,plain,
spl36_100,
inference(rat,[],[s682,s826,s1050,s1049,s98,s1064]) ).
cnf(s1067,plain,
spl36_262,
inference(rat,[],[s851,s915,s1065]) ).
cnf(s1069,plain,
spl36_162,
inference(rat,[],[s250,s990,s946,s1065]) ).
cnf(s1070,plain,
~ spl36_176,
inference(rat,[],[s463,s1067]) ).
cnf(s1071,plain,
spl36_98,
inference(rat,[],[s680,s872,s1050,s1049,s98,s1067]) ).
cnf(s1072,plain,
~ spl36_254,
inference(rat,[],[s452,s1069]) ).
cnf(s1073,plain,
spl36_92,
inference(rat,[],[s674,s816,s1047,s98,s1069]) ).
cnf(s1074,plain,
spl36_264,
inference(rat,[],[s244,s942,s918,s1070]) ).
cnf(s1075,plain,
~ spl36_189,
inference(rat,[],[s163,s1070]) ).
cnf(s1076,plain,
spl36_172,
inference(rat,[],[s235,s1029,s918,s1072]) ).
cnf(s1080,plain,
spl36_102,
inference(rat,[],[s684,s886,s1050,s1049,s98,s1074]) ).
cnf(s1081,plain,
spl36_267,
inference(rat,[],[s852,s941,s1075]) ).
cnf(s1084,plain,
spl36_91,
inference(rat,[],[s673,s887,s1047,s1049,s1076]) ).
cnf(s1085,plain,
~ spl36_103,
inference(rat,[],[s966,s1049,s1052,s1071,s1066,s1053,s1063,s1054,s1062,s1055,s1057,s1058,s1059,s1056,s1073,s1084,s1061,s1060,s1080]) ).
cnf(s1087,plain,
$false,
inference(rat,[],[s685,s878,s1050,s1049,s98,s1081,s1085]) ).
fof(f4543,plain,
$false,
inference(avatar_sat_refutation,[],[s1087]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG121+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 % Computer : n009.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Mon Sep 28 19:31:00 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24 Running first-order model finding
% 0.09/0.24 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.76/0.40 % (3371949)Will run a generic schedule for satisfiability detection.
% 0.76/0.40 % (3371958)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=490330788:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.76/0.40 % (3371955)% WARNING: option uhcvi not known.
% 0.76/0.40 % (3371954)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2563274803_2999 on theBenchmark for (2999ds/0Mi)
% 0.76/0.40 % (3371956)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3976705906:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.76/0.40 % (3371955)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3268119532:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.76/0.40 % (3371957)dis+10_1_sil=32000:sp=arity:random_seed=3162104598:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.76/0.40 % (3371959)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4289091660:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.76/0.40 % (3371960)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1160537798:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.76/0.40 % (3371958)Instruction limit reached!
% 0.76/0.40 % (3371958)------------------------------
% 0.76/0.40 % (3371958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.40 % (3371958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.40 % (3371958)CaDiCaL version: 2.1.3
% 0.76/0.40 % (3371958)Termination reason: Instruction limit
% 0.76/0.40 % (3371958)Termination phase: Saturation
% 0.76/0.40 % (3371958)Time elapsed: 0.032 s
% 0.76/0.40 % (3371958)Peak memory usage: 13 MB
% 0.76/0.40 % (3371958)Instructions burned: 118 (million)
% 0.76/0.40 % (3371968)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3340464012:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.76/0.40 % Detected minimum model sizes of [8]
% 0.76/0.40 % Detected maximum model sizes of [max]
% 0.76/0.40 % TRYING [8]
% 0.76/0.40 % Detected minimum model sizes of [8]
% 0.76/0.40 % Detected maximum model sizes of [max]
% 0.76/0.40 % TRYING [8]
% 0.76/0.40 % (3371957)Instruction limit reached!
% 0.76/0.40 % (3371957)------------------------------
% 0.76/0.40 % (3371957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.40 % (3371957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.40 % (3371957)CaDiCaL version: 2.1.3
% 0.76/0.40 % (3371957)Termination reason: Instruction limit
% 0.76/0.40 % (3371957)Termination phase: Saturation
% 0.76/0.40 % (3371957)Time elapsed: 0.053 s
% 0.76/0.40 % (3371957)Peak memory usage: 12 MB
% 0.76/0.40 % (3371957)Instructions burned: 103 (million)
% 0.76/0.40 % (3371959)Instruction limit reached!
% 0.76/0.40 % (3371959)------------------------------
% 0.76/0.40 % (3371959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.40 % (3371959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.40 % (3371959)CaDiCaL version: 2.1.3
% 0.76/0.40 % (3371959)Termination reason: Instruction limit
% 0.76/0.40 % (3371959)Termination phase: Saturation
% 0.76/0.40 % (3371959)Time elapsed: 0.068 s
% 0.76/0.40 % (3371959)Peak memory usage: 13 MB
% 0.76/0.40 % (3371959)Instructions burned: 133 (million)
% 0.76/0.40 % (3371970)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1742901285:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.76/0.40 % (3371960)Instruction limit reached!
% 0.76/0.40 % (3371960)------------------------------
% 0.76/0.40 % (3371960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.40 % (3371960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.40 % (3371960)CaDiCaL version: 2.1.3
% 0.76/0.40 % (3371960)Termination reason: Instruction limit
% 0.76/0.40 % (3371960)Termination phase: Saturation
% 0.76/0.40 % (3371960)Time elapsed: 0.088 s
% 0.76/0.40 % (3371960)Peak memory usage: 14 MB
% 0.76/0.40 % (3371960)Instructions burned: 160 (million)
% 0.76/0.40 % (3371971)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1829375248:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.76/0.40 % (3371955) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3371949-3371955"...
% 0.76/0.40 % (3371955)...printing done.
% 0.76/0.40 % (3371974)ott-21_1_sil=16000:fs=off:random_seed=745257040:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.76/0.40 % (3371955)Refutation found. Thanks to Tanya!
% 0.76/0.40 % SZS status Theorem for theBenchmark
% 0.76/0.40 % SZS output start Proof for theBenchmark
% See solution above
% 0.76/0.41 % (3371955)------------------------------
% 0.76/0.41 % (3371955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.41 % (3371955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.41 % (3371955)CaDiCaL version: 2.1.3
% 0.76/0.41 % (3371955)Termination reason: Refutation
% 0.76/0.41 % (3371955)Time elapsed: 0.106 s
% 0.76/0.41 % (3371955)Peak memory usage: 14 MB
% 0.76/0.41 % (3371955)Instructions burned: 203 (million)
% 0.76/0.41 % (3371949)Success in time 0.153 s
% 0.76/0.41 % Vampire exiting
%------------------------------------------------------------------------------