%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG116+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:22:48 AM UTC 2026
% Result : Theorem 1.05s 0.38s
% Output : Refutation 1.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 181
% Syntax : Number of formulae : 1386 ( 185 unt; 165 def)
% Number of atoms : 4528 (1763 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 5275 (2133 ~;2541 |; 436 &)
% ( 165 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 173 ( 171 usr; 172 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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e20) = e21
| op2(e20,e20) = e22
| op2(e20,e20) = e23 )
& ( op2(e20,e21) = e20
| op2(e20,e21) = e21
| op2(e20,e21) = e22
| op2(e20,e21) = e23 )
& ( op2(e20,e22) = e20
| op2(e20,e22) = e21
| op2(e20,e22) = e22
| op2(e20,e22) = e23 )
& ( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22
| op2(e20,e23) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e20) = e21
| op2(e21,e20) = e22
| op2(e21,e20) = e23 )
& ( op2(e21,e21) = e20
| op2(e21,e21) = e21
| op2(e21,e21) = e22
| op2(e21,e21) = e23 )
& ( op2(e21,e22) = e20
| op2(e21,e22) = e21
| op2(e21,e22) = e22
| op2(e21,e22) = e23 )
& ( op2(e21,e23) = e20
| op2(e21,e23) = e21
| op2(e21,e23) = e22
| op2(e21,e23) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e20) = e21
| op2(e22,e20) = e22
| op2(e22,e20) = e23 )
& ( op2(e22,e21) = e20
| op2(e22,e21) = e21
| op2(e22,e21) = e22
| op2(e22,e21) = e23 )
& ( op2(e22,e22) = e20
| op2(e22,e22) = e21
| op2(e22,e22) = e22
| op2(e22,e22) = e23 )
& ( op2(e22,e23) = e20
| op2(e22,e23) = e21
| op2(e22,e23) = e22
| op2(e22,e23) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e20) = e21
| op2(e23,e20) = e22
| op2(e23,e20) = e23 )
& ( op2(e23,e21) = e20
| op2(e23,e21) = e21
| op2(e23,e21) = e22
| op2(e23,e21) = e23 )
& ( op2(e23,e22) = e20
| op2(e23,e22) = e21
| op2(e23,e22) = e22
| op2(e23,e22) = e23 )
& ( op2(e23,e23) = e20
| op2(e23,e23) = e21
| op2(e23,e23) = e22
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e22) = e20
| op2(e20,e23) = e20 )
& ( op2(e20,e20) = e20
| op2(e21,e20) = e20
| op2(e22,e20) = e20
| op2(e23,e20) = e20 )
& ( op2(e20,e20) = e21
| op2(e20,e21) = e21
| op2(e20,e22) = e21
| op2(e20,e23) = e21 )
& ( op2(e20,e20) = e21
| op2(e21,e20) = e21
| op2(e22,e20) = e21
| op2(e23,e20) = e21 )
& ( op2(e20,e20) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 )
& ( op2(e20,e20) = e22
| op2(e21,e20) = e22
| op2(e22,e20) = e22
| op2(e23,e20) = e22 )
& ( op2(e20,e20) = e23
| op2(e20,e21) = e23
| op2(e20,e22) = e23
| op2(e20,e23) = e23 )
& ( op2(e20,e20) = e23
| op2(e21,e20) = e23
| op2(e22,e20) = e23
| op2(e23,e20) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e21) = e20
| op2(e21,e22) = e20
| op2(e21,e23) = e20 )
& ( op2(e20,e21) = e20
| op2(e21,e21) = e20
| op2(e22,e21) = e20
| op2(e23,e21) = e20 )
& ( op2(e21,e20) = e21
| op2(e21,e21) = e21
| op2(e21,e22) = e21
| op2(e21,e23) = e21 )
& ( op2(e20,e21) = e21
| op2(e21,e21) = e21
| op2(e22,e21) = e21
| op2(e23,e21) = e21 )
& ( op2(e21,e20) = e22
| op2(e21,e21) = e22
| op2(e21,e22) = e22
| op2(e21,e23) = e22 )
& ( op2(e20,e21) = e22
| op2(e21,e21) = e22
| op2(e22,e21) = e22
| op2(e23,e21) = e22 )
& ( op2(e21,e20) = e23
| op2(e21,e21) = e23
| op2(e21,e22) = e23
| op2(e21,e23) = e23 )
& ( op2(e20,e21) = e23
| op2(e21,e21) = e23
| op2(e22,e21) = e23
| op2(e23,e21) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e21) = e20
| op2(e22,e22) = e20
| op2(e22,e23) = e20 )
& ( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e22,e22) = e20
| op2(e23,e22) = e20 )
& ( op2(e22,e20) = e21
| op2(e22,e21) = e21
| op2(e22,e22) = e21
| op2(e22,e23) = e21 )
& ( op2(e20,e22) = e21
| op2(e21,e22) = e21
| op2(e22,e22) = e21
| op2(e23,e22) = e21 )
& ( op2(e22,e20) = e22
| op2(e22,e21) = e22
| op2(e22,e22) = e22
| op2(e22,e23) = e22 )
& ( op2(e20,e22) = e22
| op2(e21,e22) = e22
| op2(e22,e22) = e22
| op2(e23,e22) = e22 )
& ( op2(e22,e20) = e23
| op2(e22,e21) = e23
| op2(e22,e22) = e23
| op2(e22,e23) = e23 )
& ( op2(e20,e22) = e23
| op2(e21,e22) = e23
| op2(e22,e22) = e23
| op2(e23,e22) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e23) = e20 )
& ( op2(e20,e23) = e20
| op2(e21,e23) = e20
| op2(e22,e23) = e20
| op2(e23,e23) = e20 )
& ( op2(e23,e20) = e21
| op2(e23,e21) = e21
| op2(e23,e22) = e21
| op2(e23,e23) = e21 )
& ( op2(e20,e23) = e21
| op2(e21,e23) = e21
| op2(e22,e23) = e21
| op2(e23,e23) = e21 )
& ( op2(e23,e20) = e22
| op2(e23,e21) = e22
| op2(e23,e22) = e22
| op2(e23,e23) = e22 )
& ( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22
| op2(e23,e23) = e22 )
& ( op2(e23,e20) = e23
| op2(e23,e21) = e23
| op2(e23,e22) = e23
| op2(e23,e23) = e23 )
& ( op2(e20,e23) = e23
| op2(e21,e23) = e23
| op2(e22,e23) = e23
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
fof(f10,axiom,
( ( op1(op1(e10,e10),op1(e10,e10)) = e10
& op1(op1(e10,e11),op1(e10,e11)) = e11
& op1(op1(e10,e12),op1(e10,e12)) = e12
& op1(op1(e10,e13),op1(e10,e13)) = e13 )
| ( op1(op1(e11,e10),op1(e11,e10)) = e10
& op1(op1(e11,e11),op1(e11,e11)) = e11
& op1(op1(e11,e12),op1(e11,e12)) = e12
& op1(op1(e11,e13),op1(e11,e13)) = e13 )
| ( op1(op1(e12,e10),op1(e12,e10)) = e10
& op1(op1(e12,e11),op1(e12,e11)) = e11
& op1(op1(e12,e12),op1(e12,e12)) = e12
& op1(op1(e12,e13),op1(e12,e13)) = e13 )
| ( op1(op1(e13,e10),op1(e13,e10)) = e10
& op1(op1(e13,e11),op1(e13,e11)) = e11
& op1(op1(e13,e12),op1(e13,e12)) = e12
& op1(op1(e13,e13),op1(e13,e13)) = e13 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( ( op2(op2(e20,e20),op2(e20,e20)) = e20
& op2(op2(e20,e21),op2(e20,e21)) = e21
& op2(op2(e20,e22),op2(e20,e22)) = e22
& op2(op2(e20,e23),op2(e20,e23)) = e23 )
| ( op2(op2(e21,e20),op2(e21,e20)) = e20
& op2(op2(e21,e21),op2(e21,e21)) = e21
& op2(op2(e21,e22),op2(e21,e22)) = e22
& op2(op2(e21,e23),op2(e21,e23)) = e23 )
| ( op2(op2(e22,e20),op2(e22,e20)) = e20
& op2(op2(e22,e21),op2(e22,e21)) = e21
& op2(op2(e22,e22),op2(e22,e22)) = e22
& op2(op2(e22,e23),op2(e22,e23)) = e23 )
| ( op2(op2(e23,e20),op2(e23,e20)) = e20
& op2(op2(e23,e21),op2(e23,e21)) = e21
& op2(op2(e23,e22),op2(e23,e22)) = e22
& op2(op2(e23,e23),op2(e23,e23)) = e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e10 = op1(e13,op1(e13,e13))
& e11 = op1(e13,e13)
& e12 = op1(op1(e13,op1(e13,e13)),e13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e20 = op2(e23,op2(e23,e23))
& e21 = op2(e23,e23)
& e22 = op2(op2(e23,op2(e23,e23)),e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( h1(e13) = e20
& h1(e10) = op2(e20,op2(e20,e20))
& h1(e11) = op2(e20,e20)
& h1(e12) = op2(op2(e20,op2(e20,e20)),e20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
( h2(e13) = e21
& h2(e10) = op2(e21,op2(e21,e21))
& h2(e11) = op2(e21,e21)
& h2(e12) = op2(op2(e21,op2(e21,e21)),e21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
( h3(e13) = e22
& h3(e10) = op2(e22,op2(e22,e22))
& h3(e11) = op2(e22,e22)
& h3(e12) = op2(op2(e22,op2(e22,e22)),e22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
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/sandbox2/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(f22,plain,
( e13 = op1(e10,e11)
| e12 = op1(e10,e11)
| e11 = op1(e10,e11)
| e10 = op1(e10,e11) ),
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(f40,plain,
( e11 = op1(e13,e10)
| e11 = op1(e12,e10)
| e11 = op1(e11,e10)
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[],[f2]) ).
fof(f43,plain,
( e13 = op1(e10,e13)
| e13 = op1(e10,e12)
| e13 = op1(e10,e11)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f2]) ).
fof(f45,plain,
( e10 = op1(e11,e13)
| e10 = op1(e11,e12)
| e10 = op1(e11,e11)
| e10 = 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(f55,plain,
( e11 = op1(e12,e13)
| e11 = op1(e12,e12)
| e11 = op1(e12,e11)
| e11 = 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(f57,plain,
( e12 = op1(e12,e13)
| e12 = op1(e12,e12)
| e12 = op1(e12,e11)
| e12 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f58,plain,
( e12 = op1(e13,e12)
| e12 = op1(e12,e12)
| e12 = op1(e11,e12)
| e12 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f62,plain,
( e10 = op1(e13,e13)
| e10 = op1(e12,e13)
| e10 = op1(e11,e13)
| e10 = 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(f67,plain,
( e13 = op1(e13,e13)
| e13 = op1(e13,e12)
| e13 = op1(e13,e11)
| e13 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f68,plain,
( e13 = op1(e13,e13)
| e13 = op1(e12,e13)
| e13 = op1(e11,e13)
| e13 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f69,plain,
( op2(e20,e20) = e23
| op2(e20,e20) = e22
| op2(e20,e20) = e21
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f70,plain,
( e23 = op2(e20,e21)
| e22 = op2(e20,e21)
| e21 = op2(e20,e21)
| e20 = op2(e20,e21) ),
inference(cnf_transformation,[],[f3]) ).
fof(f76,plain,
( e23 = op2(e21,e23)
| e22 = op2(e21,e23)
| e21 = op2(e21,e23)
| e20 = op2(e21,e23) ),
inference(cnf_transformation,[],[f3]) ).
fof(f80,plain,
( e23 = op2(e22,e23)
| e22 = op2(e22,e23)
| e21 = op2(e22,e23)
| e20 = op2(e22,e23) ),
inference(cnf_transformation,[],[f3]) ).
fof(f81,plain,
( e23 = op2(e23,e20)
| e22 = op2(e23,e20)
| e21 = op2(e23,e20)
| e20 = op2(e23,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f83,plain,
( e23 = op2(e23,e22)
| e22 = op2(e23,e22)
| e21 = op2(e23,e22)
| e20 = op2(e23,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f85,plain,
( e20 = op2(e20,e23)
| e20 = op2(e20,e22)
| e20 = op2(e20,e21)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f86,plain,
( e20 = op2(e23,e20)
| e20 = op2(e22,e20)
| e20 = op2(e21,e20)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f87,plain,
( e21 = op2(e20,e23)
| e21 = op2(e20,e22)
| e21 = op2(e20,e21)
| op2(e20,e20) = e21 ),
inference(cnf_transformation,[],[f4]) ).
fof(f88,plain,
( e21 = op2(e23,e20)
| e21 = op2(e22,e20)
| e21 = op2(e21,e20)
| op2(e20,e20) = e21 ),
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(f95,plain,
( e21 = op2(e21,e23)
| e21 = op2(e21,e22)
| e21 = op2(e21,e21)
| e21 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f96,plain,
( e21 = op2(e23,e21)
| e21 = op2(e22,e21)
| e21 = op2(e21,e21)
| e21 = op2(e20,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f97,plain,
( e22 = op2(e21,e23)
| e22 = op2(e21,e22)
| e22 = op2(e21,e21)
| e22 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f98,plain,
( e22 = op2(e23,e21)
| e22 = op2(e22,e21)
| e22 = op2(e21,e21)
| e22 = 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(f105,plain,
( e22 = op2(e22,e23)
| e22 = op2(e22,e22)
| e22 = op2(e22,e21)
| e22 = op2(e22,e20) ),
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(f110,plain,
( e20 = op2(e23,e23)
| e20 = op2(e22,e23)
| e20 = op2(e21,e23)
| e20 = op2(e20,e23) ),
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(f117,plain,
op1(e13,e12) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f122,plain,
op1(e13,e10) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f123,plain,
op1(e12,e12) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f132,plain,
op1(e11,e10) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f136,plain,
op1(e10,e11) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f138,plain,
op1(e10,e10) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f140,plain,
op1(e10,e10) != op1(e10,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f141,plain,
op1(e12,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f143,plain,
op1(e11,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f151,plain,
op1(e10,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f152,plain,
op1(e10,e12) != op1(e11,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f153,plain,
op1(e12,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f154,plain,
op1(e11,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f155,plain,
op1(e11,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f156,plain,
op1(e10,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f158,plain,
op1(e10,e11) != op1(e11,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
op1(e10,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f163,plain,
op1(e10,e10) != op1(e12,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(f166,plain,
op2(e23,e21) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f167,plain,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f168,plain,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f169,plain,
op2(e23,e20) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f170,plain,
op2(e23,e20) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f171,plain,
op2(e22,e22) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f173,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f175,plain,
op2(e22,e20) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f176,plain,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f179,plain,
op2(e21,e21) != op2(e21,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f181,plain,
op2(e21,e20) != op2(e21,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f184,plain,
op2(e20,e21) != op2(e20,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f185,plain,
op2(e20,e21) != op2(e20,e22),
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(f188,plain,
op2(e20,e20) != op2(e20,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f189,plain,
op2(e22,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f190,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f192,plain,
op2(e20,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f193,plain,
op2(e20,e23) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f194,plain,
op2(e20,e23) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f195,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f203,plain,
op2(e21,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f204,plain,
op2(e20,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f206,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f208,plain,
op2(e21,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f210,plain,
op2(e20,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f212,plain,
op2(e20,e20) != op2(e21,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(f220,plain,
e21 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f221,plain,
e21 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f222,plain,
e20 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f224,plain,
e20 != e21,
inference(cnf_transformation,[],[f8]) ).
fof(f241,plain,
( e13 = op1(op1(e10,e13),op1(e10,e13))
| ~ sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f242,plain,
( e12 = op1(op1(e10,e12),op1(e10,e12))
| ~ sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f245,plain,
( e13 = op1(op1(e11,e13),op1(e11,e13))
| ~ sP0 ),
inference(cnf_transformation,[],[f10]) ).
fof(f246,plain,
( e12 = op1(op1(e11,e12),op1(e11,e12))
| ~ sP0 ),
inference(cnf_transformation,[],[f10]) ).
fof(f248,plain,
( e10 = op1(op1(e11,e10),op1(e11,e10))
| ~ sP0 ),
inference(cnf_transformation,[],[f10]) ).
fof(f253,plain,
( e11 = op1(op1(e13,e11),op1(e13,e11))
| e13 = op1(op1(e12,e13),op1(e12,e13))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f254,plain,
( e11 = op1(op1(e13,e11),op1(e13,e11))
| e12 = op1(op1(e12,e12),op1(e12,e12))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f256,plain,
( e11 = op1(op1(e13,e11),op1(e13,e11))
| e10 = op1(op1(e12,e10),op1(e12,e10))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f261,plain,
( e13 = op1(op1(e13,e13),op1(e13,e13))
| e13 = op1(op1(e12,e13),op1(e12,e13))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f265,plain,
( e23 = op2(op2(e20,e23),op2(e20,e23))
| ~ sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f266,plain,
( e22 = op2(op2(e20,e22),op2(e20,e22))
| ~ sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f267,plain,
( e21 = op2(op2(e20,e21),op2(e20,e21))
| ~ sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f269,plain,
( e23 = op2(op2(e21,e23),op2(e21,e23))
| ~ sP2 ),
inference(cnf_transformation,[],[f11]) ).
fof(f270,plain,
( e22 = op2(op2(e21,e22),op2(e21,e22))
| ~ sP2 ),
inference(cnf_transformation,[],[f11]) ).
fof(f271,plain,
( e21 = op2(op2(e21,e21),op2(e21,e21))
| ~ sP2 ),
inference(cnf_transformation,[],[f11]) ).
fof(f272,plain,
( e20 = op2(op2(e21,e20),op2(e21,e20))
| ~ sP2 ),
inference(cnf_transformation,[],[f11]) ).
fof(f276,plain,
( e20 = op2(op2(e23,e20),op2(e23,e20))
| e20 = op2(op2(e22,e20),op2(e22,e20))
| sP2
| sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f277,plain,
( e21 = op2(op2(e23,e21),op2(e23,e21))
| e23 = op2(op2(e22,e23),op2(e22,e23))
| sP2
| sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f278,plain,
( e21 = op2(op2(e23,e21),op2(e23,e21))
| e22 = op2(op2(e22,e22),op2(e22,e22))
| sP2
| sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f279,plain,
( e21 = op2(op2(e23,e21),op2(e23,e21))
| e21 = op2(op2(e22,e21),op2(e22,e21))
| sP2
| sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f280,plain,
( e21 = op2(op2(e23,e21),op2(e23,e21))
| e20 = op2(op2(e22,e20),op2(e22,e20))
| sP2
| sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f286,plain,
( e23 = op2(op2(e23,e23),op2(e23,e23))
| e22 = op2(op2(e22,e22),op2(e22,e22))
| sP2
| sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f287,plain,
( e23 = op2(op2(e23,e23),op2(e23,e23))
| e21 = op2(op2(e22,e21),op2(e22,e21))
| sP2
| sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f288,plain,
( e23 = op2(op2(e23,e23),op2(e23,e23))
| e20 = op2(op2(e22,e20),op2(e22,e20))
| sP2
| sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f289,plain,
e12 = op1(op1(e13,op1(e13,e13)),e13),
inference(cnf_transformation,[],[f12]) ).
fof(f290,plain,
e11 = op1(e13,e13),
inference(cnf_transformation,[],[f12]) ).
fof(f291,plain,
e10 = op1(e13,op1(e13,e13)),
inference(cnf_transformation,[],[f12]) ).
fof(f292,plain,
e22 = op2(op2(e23,op2(e23,e23)),e23),
inference(cnf_transformation,[],[f13]) ).
fof(f293,plain,
e21 = op2(e23,e23),
inference(cnf_transformation,[],[f13]) ).
fof(f294,plain,
e20 = op2(e23,op2(e23,e23)),
inference(cnf_transformation,[],[f13]) ).
fof(f298,plain,
e20 = h1(e13),
inference(cnf_transformation,[],[f14]) ).
fof(f299,plain,
h2(e12) = op2(op2(e21,op2(e21,e21)),e21),
inference(cnf_transformation,[],[f15]) ).
fof(f300,plain,
op2(e21,e21) = h2(e11),
inference(cnf_transformation,[],[f15]) ).
fof(f301,plain,
h2(e10) = op2(e21,op2(e21,e21)),
inference(cnf_transformation,[],[f15]) ).
fof(f302,plain,
e21 = h2(e13),
inference(cnf_transformation,[],[f15]) ).
fof(f305,plain,
h3(e10) = op2(e22,op2(e22,e22)),
inference(cnf_transformation,[],[f16]) ).
fof(f306,plain,
e22 = h3(e13),
inference(cnf_transformation,[],[f16]) ).
fof(f322,plain,
( e20 != h2(e10)
| ~ sP9 ),
inference(cnf_transformation,[],[f20]) ).
fof(f323,plain,
( e21 != h2(e13)
| ~ sP8 ),
inference(cnf_transformation,[],[f20]) ).
fof(f369,plain,
( e23 != h2(e12)
| e22 != h2(e11)
| sP8
| sP9
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(cnf_transformation,[],[f20]) ).
fof(f410,plain,
( e13 = op1(op1(e13,e13),op1(e13,e13))
| e13 = op1(op1(e12,e13),op1(e12,e13))
| sP0
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f261]) ).
fof(f415,plain,
( e11 = op1(op1(e13,e11),op1(e13,e11))
| e10 = op1(op1(e12,e10),op1(e12,e10))
| sP0
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f256]) ).
fof(f417,plain,
( e11 = op1(op1(e13,e11),op1(e13,e11))
| e12 = op1(op1(e12,e12),op1(e12,e12))
| sP0
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f254]) ).
fof(f418,plain,
( e11 = op1(op1(e13,e11),op1(e13,e11))
| e13 = op1(op1(e12,e13),op1(e12,e13))
| sP0
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f253]) ).
fof(f425,plain,
( e12 = op1(op1(e10,e12),op1(e10,e12))
| sP1 ),
inference(consistent_polarity_flipping,[],[f242]) ).
fof(f426,plain,
( e13 = op1(op1(e10,e13),op1(e10,e13))
| sP1 ),
inference(consistent_polarity_flipping,[],[f241]) ).
fof(f464,plain,
( e23 != h2(e12)
| e22 != h2(e11)
| ~ sP8
| ~ sP9
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(consistent_polarity_flipping,[],[f369]) ).
fof(f502,plain,
( e21 != h2(e13)
| sP8 ),
inference(consistent_polarity_flipping,[],[f323]) ).
fof(f503,plain,
( e20 != h2(e10)
| sP9 ),
inference(consistent_polarity_flipping,[],[f322]) ).
fof(f516,definition,
( spl12_2
<=> e20 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition]) ).
fof(f517,plain,
( e20 = h1(e13)
| ~ spl12_2 ),
inference(avatar_component_clause,[],[f516]) ).
fof(f540,definition,
( spl12_7
<=> e21 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl12_7])],[avatar_definition]) ).
fof(f541,plain,
( e21 = h1(e13)
| ~ spl12_7 ),
inference(avatar_component_clause,[],[f540]) ).
fof(f542,plain,
( e21 != h1(e13)
| spl12_7 ),
inference(avatar_component_clause,[],[f540]) ).
fof(f560,definition,
( spl12_11
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl12_11])],[avatar_definition]) ).
fof(f579,definition,
( spl12_15
<=> e20 = h2(e10) ),
introduced(definition,[new_symbols(definition,[spl12_15])],[avatar_definition]) ).
fof(f580,plain,
( e20 = h2(e10)
| ~ spl12_15 ),
inference(avatar_component_clause,[],[f579]) ).
fof(f582,plain,
( spl12_11
| ~ spl12_15 ),
inference(avatar_split_clause,[],[f503,f579,f560]) ).
fof(f584,definition,
( spl12_16
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl12_16])],[avatar_definition]) ).
fof(f588,definition,
( spl12_17
<=> e21 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl12_17])],[avatar_definition]) ).
fof(f589,plain,
( e21 = h2(e13)
| ~ spl12_17 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f591,plain,
( spl12_16
| ~ spl12_17 ),
inference(avatar_split_clause,[],[f502,f588,f584]) ).
fof(f603,definition,
( spl12_20
<=> e21 = h2(e10) ),
introduced(definition,[new_symbols(definition,[spl12_20])],[avatar_definition]) ).
fof(f604,plain,
( e21 = h2(e10)
| ~ spl12_20 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f612,definition,
( spl12_22
<=> e20 = h3(e13) ),
introduced(definition,[new_symbols(definition,[spl12_22])],[avatar_definition]) ).
fof(f613,plain,
( e20 = h3(e13)
| ~ spl12_22 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f614,plain,
( e20 != h3(e13)
| spl12_22 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f816,definition,
( spl12_65
<=> h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_65])],[avatar_definition]) ).
fof(f818,plain,
( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| spl12_65 ),
inference(avatar_component_clause,[],[f816]) ).
fof(f820,definition,
( spl12_66
<=> h2(op1(e10,e11)) = op2(h2(e10),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_66])],[avatar_definition]) ).
fof(f822,plain,
( h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| spl12_66 ),
inference(avatar_component_clause,[],[f820]) ).
fof(f824,definition,
( spl12_67
<=> h2(op1(e10,e12)) = op2(h2(e10),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_67])],[avatar_definition]) ).
fof(f826,plain,
( h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| spl12_67 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f828,definition,
( spl12_68
<=> h2(op1(e10,e13)) = op2(h2(e10),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_68])],[avatar_definition]) ).
fof(f830,plain,
( h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| spl12_68 ),
inference(avatar_component_clause,[],[f828]) ).
fof(f832,definition,
( spl12_69
<=> h2(op1(e11,e10)) = op2(h2(e11),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_69])],[avatar_definition]) ).
fof(f834,plain,
( h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| spl12_69 ),
inference(avatar_component_clause,[],[f832]) ).
fof(f836,definition,
( spl12_70
<=> h2(op1(e11,e11)) = op2(h2(e11),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_70])],[avatar_definition]) ).
fof(f838,plain,
( h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| spl12_70 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f840,definition,
( spl12_71
<=> h2(op1(e11,e12)) = op2(h2(e11),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_71])],[avatar_definition]) ).
fof(f842,plain,
( h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| spl12_71 ),
inference(avatar_component_clause,[],[f840]) ).
fof(f844,definition,
( spl12_72
<=> h2(op1(e11,e13)) = op2(h2(e11),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_72])],[avatar_definition]) ).
fof(f846,plain,
( h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| spl12_72 ),
inference(avatar_component_clause,[],[f844]) ).
fof(f848,definition,
( spl12_73
<=> h2(op1(e12,e10)) = op2(h2(e12),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_73])],[avatar_definition]) ).
fof(f850,plain,
( h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| spl12_73 ),
inference(avatar_component_clause,[],[f848]) ).
fof(f852,definition,
( spl12_74
<=> h2(op1(e12,e11)) = op2(h2(e12),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_74])],[avatar_definition]) ).
fof(f854,plain,
( h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| spl12_74 ),
inference(avatar_component_clause,[],[f852]) ).
fof(f856,definition,
( spl12_75
<=> h2(op1(e12,e12)) = op2(h2(e12),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_75])],[avatar_definition]) ).
fof(f858,plain,
( h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| spl12_75 ),
inference(avatar_component_clause,[],[f856]) ).
fof(f860,definition,
( spl12_76
<=> h2(op1(e12,e13)) = op2(h2(e12),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_76])],[avatar_definition]) ).
fof(f862,plain,
( h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| spl12_76 ),
inference(avatar_component_clause,[],[f860]) ).
fof(f864,definition,
( spl12_77
<=> h2(op1(e13,e10)) = op2(h2(e13),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_77])],[avatar_definition]) ).
fof(f866,plain,
( h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| spl12_77 ),
inference(avatar_component_clause,[],[f864]) ).
fof(f868,definition,
( spl12_78
<=> h2(op1(e13,e11)) = op2(h2(e13),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_78])],[avatar_definition]) ).
fof(f870,plain,
( h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| spl12_78 ),
inference(avatar_component_clause,[],[f868]) ).
fof(f872,definition,
( spl12_79
<=> h2(op1(e13,e12)) = op2(h2(e13),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_79])],[avatar_definition]) ).
fof(f874,plain,
( h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| spl12_79 ),
inference(avatar_component_clause,[],[f872]) ).
fof(f876,definition,
( spl12_80
<=> h2(op1(e13,e13)) = op2(h2(e13),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_80])],[avatar_definition]) ).
fof(f878,plain,
( h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| spl12_80 ),
inference(avatar_component_clause,[],[f876]) ).
fof(f894,definition,
( spl12_84
<=> e22 = h2(e11) ),
introduced(definition,[new_symbols(definition,[spl12_84])],[avatar_definition]) ).
fof(f895,plain,
( e22 = h2(e11)
| ~ spl12_84 ),
inference(avatar_component_clause,[],[f894]) ).
fof(f912,definition,
( spl12_87
<=> e23 = h2(e12) ),
introduced(definition,[new_symbols(definition,[spl12_87])],[avatar_definition]) ).
fof(f913,plain,
( e23 = h2(e12)
| ~ spl12_87 ),
inference(avatar_component_clause,[],[f912]) ).
fof(f917,plain,
( ~ spl12_65
| ~ spl12_66
| ~ spl12_67
| ~ spl12_68
| ~ spl12_69
| ~ spl12_70
| ~ spl12_71
| ~ spl12_72
| ~ spl12_73
| ~ spl12_74
| ~ spl12_75
| ~ spl12_76
| ~ spl12_77
| ~ spl12_78
| ~ spl12_79
| ~ spl12_80
| ~ spl12_11
| ~ spl12_16
| ~ spl12_84
| ~ spl12_87 ),
inference(avatar_split_clause,[],[f464,f912,f894,f584,f560,f876,f872,f868,f864,f860,f856,f852,f848,f844,f840,f836,f832,f828,f824,f820,f816]) ).
fof(f992,definition,
( spl12_105
<=> e22 = h3(e13) ),
introduced(definition,[new_symbols(definition,[spl12_105])],[avatar_definition]) ).
fof(f993,plain,
( e22 = h3(e13)
| ~ spl12_105 ),
inference(avatar_component_clause,[],[f992]) ).
fof(f1011,definition,
( spl12_109
<=> e22 = h3(e10) ),
introduced(definition,[new_symbols(definition,[spl12_109])],[avatar_definition]) ).
fof(f1012,plain,
( e22 = h3(e10)
| ~ spl12_109 ),
inference(avatar_component_clause,[],[f1011]) ).
fof(f1152,plain,
spl12_105,
inference(avatar_split_clause,[],[f306,f992]) ).
fof(f1153,plain,
spl12_17,
inference(avatar_split_clause,[],[f302,f588]) ).
fof(f1154,plain,
spl12_2,
inference(avatar_split_clause,[],[f298,f516]) ).
fof(f1156,definition,
( spl12_137
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl12_137])],[avatar_definition]) ).
fof(f1160,definition,
( spl12_138
<=> e23 = op2(op2(e20,e23),op2(e20,e23)) ),
introduced(definition,[new_symbols(definition,[spl12_138])],[avatar_definition]) ).
fof(f1162,plain,
( e23 = op2(op2(e20,e23),op2(e20,e23))
| ~ spl12_138 ),
inference(avatar_component_clause,[],[f1160]) ).
fof(f1163,plain,
( ~ spl12_137
| spl12_138 ),
inference(avatar_split_clause,[],[f265,f1160,f1156]) ).
fof(f1165,definition,
( spl12_139
<=> e22 = op2(op2(e20,e22),op2(e20,e22)) ),
introduced(definition,[new_symbols(definition,[spl12_139])],[avatar_definition]) ).
fof(f1167,plain,
( e22 = op2(op2(e20,e22),op2(e20,e22))
| ~ spl12_139 ),
inference(avatar_component_clause,[],[f1165]) ).
fof(f1168,plain,
( ~ spl12_137
| spl12_139 ),
inference(avatar_split_clause,[],[f266,f1165,f1156]) ).
fof(f1170,definition,
( spl12_140
<=> e21 = op2(op2(e20,e21),op2(e20,e21)) ),
introduced(definition,[new_symbols(definition,[spl12_140])],[avatar_definition]) ).
fof(f1172,plain,
( e21 = op2(op2(e20,e21),op2(e20,e21))
| ~ spl12_140 ),
inference(avatar_component_clause,[],[f1170]) ).
fof(f1173,plain,
( ~ spl12_137
| spl12_140 ),
inference(avatar_split_clause,[],[f267,f1170,f1156]) ).
fof(f1180,definition,
( spl12_142
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl12_142])],[avatar_definition]) ).
fof(f1184,definition,
( spl12_143
<=> e23 = op2(op2(e21,e23),op2(e21,e23)) ),
introduced(definition,[new_symbols(definition,[spl12_143])],[avatar_definition]) ).
fof(f1186,plain,
( e23 = op2(op2(e21,e23),op2(e21,e23))
| ~ spl12_143 ),
inference(avatar_component_clause,[],[f1184]) ).
fof(f1187,plain,
( ~ spl12_142
| spl12_143 ),
inference(avatar_split_clause,[],[f269,f1184,f1180]) ).
fof(f1189,definition,
( spl12_144
<=> e22 = op2(op2(e21,e22),op2(e21,e22)) ),
introduced(definition,[new_symbols(definition,[spl12_144])],[avatar_definition]) ).
fof(f1191,plain,
( e22 = op2(op2(e21,e22),op2(e21,e22))
| ~ spl12_144 ),
inference(avatar_component_clause,[],[f1189]) ).
fof(f1192,plain,
( ~ spl12_142
| spl12_144 ),
inference(avatar_split_clause,[],[f270,f1189,f1180]) ).
fof(f1194,definition,
( spl12_145
<=> e21 = op2(op2(e21,e21),op2(e21,e21)) ),
introduced(definition,[new_symbols(definition,[spl12_145])],[avatar_definition]) ).
fof(f1196,plain,
( e21 = op2(op2(e21,e21),op2(e21,e21))
| ~ spl12_145 ),
inference(avatar_component_clause,[],[f1194]) ).
fof(f1197,plain,
( ~ spl12_142
| spl12_145 ),
inference(avatar_split_clause,[],[f271,f1194,f1180]) ).
fof(f1199,definition,
( spl12_146
<=> e20 = op2(op2(e21,e20),op2(e21,e20)) ),
introduced(definition,[new_symbols(definition,[spl12_146])],[avatar_definition]) ).
fof(f1201,plain,
( e20 = op2(op2(e21,e20),op2(e21,e20))
| ~ spl12_146 ),
inference(avatar_component_clause,[],[f1199]) ).
fof(f1202,plain,
( ~ spl12_142
| spl12_146 ),
inference(avatar_split_clause,[],[f272,f1199,f1180]) ).
fof(f1204,definition,
( spl12_147
<=> e23 = op2(op2(e22,e23),op2(e22,e23)) ),
introduced(definition,[new_symbols(definition,[spl12_147])],[avatar_definition]) ).
fof(f1206,plain,
( e23 = op2(op2(e22,e23),op2(e22,e23))
| ~ spl12_147 ),
inference(avatar_component_clause,[],[f1204]) ).
fof(f1208,definition,
( spl12_148
<=> e20 = op2(op2(e23,e20),op2(e23,e20)) ),
introduced(definition,[new_symbols(definition,[spl12_148])],[avatar_definition]) ).
fof(f1210,plain,
( e20 = op2(op2(e23,e20),op2(e23,e20))
| ~ spl12_148 ),
inference(avatar_component_clause,[],[f1208]) ).
fof(f1213,definition,
( spl12_149
<=> e22 = op2(op2(e22,e22),op2(e22,e22)) ),
introduced(definition,[new_symbols(definition,[spl12_149])],[avatar_definition]) ).
fof(f1215,plain,
( e22 = op2(op2(e22,e22),op2(e22,e22))
| ~ spl12_149 ),
inference(avatar_component_clause,[],[f1213]) ).
fof(f1218,definition,
( spl12_150
<=> e21 = op2(op2(e22,e21),op2(e22,e21)) ),
introduced(definition,[new_symbols(definition,[spl12_150])],[avatar_definition]) ).
fof(f1220,plain,
( e21 = op2(op2(e22,e21),op2(e22,e21))
| ~ spl12_150 ),
inference(avatar_component_clause,[],[f1218]) ).
fof(f1223,definition,
( spl12_151
<=> e20 = op2(op2(e22,e20),op2(e22,e20)) ),
introduced(definition,[new_symbols(definition,[spl12_151])],[avatar_definition]) ).
fof(f1225,plain,
( e20 = op2(op2(e22,e20),op2(e22,e20))
| ~ spl12_151 ),
inference(avatar_component_clause,[],[f1223]) ).
fof(f1226,plain,
( spl12_137
| spl12_142
| spl12_151
| spl12_148 ),
inference(avatar_split_clause,[],[f276,f1208,f1223,f1180,f1156]) ).
fof(f1228,definition,
( spl12_152
<=> e21 = op2(op2(e23,e21),op2(e23,e21)) ),
introduced(definition,[new_symbols(definition,[spl12_152])],[avatar_definition]) ).
fof(f1229,plain,
( e21 != op2(op2(e23,e21),op2(e23,e21))
| spl12_152 ),
inference(avatar_component_clause,[],[f1228]) ).
fof(f1230,plain,
( e21 = op2(op2(e23,e21),op2(e23,e21))
| ~ spl12_152 ),
inference(avatar_component_clause,[],[f1228]) ).
fof(f1231,plain,
( spl12_137
| spl12_142
| spl12_147
| spl12_152 ),
inference(avatar_split_clause,[],[f277,f1228,f1204,f1180,f1156]) ).
fof(f1232,plain,
( spl12_137
| spl12_142
| spl12_149
| spl12_152 ),
inference(avatar_split_clause,[],[f278,f1228,f1213,f1180,f1156]) ).
fof(f1233,plain,
( spl12_137
| spl12_142
| spl12_150
| spl12_152 ),
inference(avatar_split_clause,[],[f279,f1228,f1218,f1180,f1156]) ).
fof(f1234,plain,
( spl12_137
| spl12_142
| spl12_151
| spl12_152 ),
inference(avatar_split_clause,[],[f280,f1228,f1223,f1180,f1156]) ).
fof(f1244,definition,
( spl12_154
<=> e23 = op2(op2(e23,e23),op2(e23,e23)) ),
introduced(definition,[new_symbols(definition,[spl12_154])],[avatar_definition]) ).
fof(f1246,plain,
( e23 = op2(op2(e23,e23),op2(e23,e23))
| ~ spl12_154 ),
inference(avatar_component_clause,[],[f1244]) ).
fof(f1248,plain,
( spl12_137
| spl12_142
| spl12_149
| spl12_154 ),
inference(avatar_split_clause,[],[f286,f1244,f1213,f1180,f1156]) ).
fof(f1249,plain,
( spl12_137
| spl12_142
| spl12_150
| spl12_154 ),
inference(avatar_split_clause,[],[f287,f1244,f1218,f1180,f1156]) ).
fof(f1250,plain,
( spl12_137
| spl12_142
| spl12_151
| spl12_154 ),
inference(avatar_split_clause,[],[f288,f1244,f1223,f1180,f1156]) ).
fof(f1252,definition,
( spl12_155
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl12_155])],[avatar_definition]) ).
fof(f1256,definition,
( spl12_156
<=> e13 = op1(op1(e10,e13),op1(e10,e13)) ),
introduced(definition,[new_symbols(definition,[spl12_156])],[avatar_definition]) ).
fof(f1258,plain,
( e13 = op1(op1(e10,e13),op1(e10,e13))
| ~ spl12_156 ),
inference(avatar_component_clause,[],[f1256]) ).
fof(f1259,plain,
( spl12_155
| spl12_156 ),
inference(avatar_split_clause,[],[f426,f1256,f1252]) ).
fof(f1261,definition,
( spl12_157
<=> e12 = op1(op1(e10,e12),op1(e10,e12)) ),
introduced(definition,[new_symbols(definition,[spl12_157])],[avatar_definition]) ).
fof(f1263,plain,
( e12 = op1(op1(e10,e12),op1(e10,e12))
| ~ spl12_157 ),
inference(avatar_component_clause,[],[f1261]) ).
fof(f1264,plain,
( spl12_155
| spl12_157 ),
inference(avatar_split_clause,[],[f425,f1261,f1252]) ).
fof(f1276,definition,
( spl12_160
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl12_160])],[avatar_definition]) ).
fof(f1280,definition,
( spl12_161
<=> e13 = op1(op1(e11,e13),op1(e11,e13)) ),
introduced(definition,[new_symbols(definition,[spl12_161])],[avatar_definition]) ).
fof(f1282,plain,
( e13 = op1(op1(e11,e13),op1(e11,e13))
| ~ spl12_161 ),
inference(avatar_component_clause,[],[f1280]) ).
fof(f1283,plain,
( ~ spl12_160
| spl12_161 ),
inference(avatar_split_clause,[],[f245,f1280,f1276]) ).
fof(f1285,definition,
( spl12_162
<=> e12 = op1(op1(e11,e12),op1(e11,e12)) ),
introduced(definition,[new_symbols(definition,[spl12_162])],[avatar_definition]) ).
fof(f1287,plain,
( e12 = op1(op1(e11,e12),op1(e11,e12))
| ~ spl12_162 ),
inference(avatar_component_clause,[],[f1285]) ).
fof(f1288,plain,
( ~ spl12_160
| spl12_162 ),
inference(avatar_split_clause,[],[f246,f1285,f1276]) ).
fof(f1295,definition,
( spl12_164
<=> e10 = op1(op1(e11,e10),op1(e11,e10)) ),
introduced(definition,[new_symbols(definition,[spl12_164])],[avatar_definition]) ).
fof(f1297,plain,
( e10 = op1(op1(e11,e10),op1(e11,e10))
| ~ spl12_164 ),
inference(avatar_component_clause,[],[f1295]) ).
fof(f1298,plain,
( ~ spl12_160
| spl12_164 ),
inference(avatar_split_clause,[],[f248,f1295,f1276]) ).
fof(f1300,definition,
( spl12_165
<=> e13 = op1(op1(e12,e13),op1(e12,e13)) ),
introduced(definition,[new_symbols(definition,[spl12_165])],[avatar_definition]) ).
fof(f1302,plain,
( e13 = op1(op1(e12,e13),op1(e12,e13))
| ~ spl12_165 ),
inference(avatar_component_clause,[],[f1300]) ).
fof(f1309,definition,
( spl12_167
<=> e12 = op1(op1(e12,e12),op1(e12,e12)) ),
introduced(definition,[new_symbols(definition,[spl12_167])],[avatar_definition]) ).
fof(f1311,plain,
( e12 = op1(op1(e12,e12),op1(e12,e12))
| ~ spl12_167 ),
inference(avatar_component_clause,[],[f1309]) ).
fof(f1319,definition,
( spl12_169
<=> e10 = op1(op1(e12,e10),op1(e12,e10)) ),
introduced(definition,[new_symbols(definition,[spl12_169])],[avatar_definition]) ).
fof(f1321,plain,
( e10 = op1(op1(e12,e10),op1(e12,e10))
| ~ spl12_169 ),
inference(avatar_component_clause,[],[f1319]) ).
fof(f1324,definition,
( spl12_170
<=> e11 = op1(op1(e13,e11),op1(e13,e11)) ),
introduced(definition,[new_symbols(definition,[spl12_170])],[avatar_definition]) ).
fof(f1326,plain,
( e11 = op1(op1(e13,e11),op1(e13,e11))
| ~ spl12_170 ),
inference(avatar_component_clause,[],[f1324]) ).
fof(f1327,plain,
( ~ spl12_155
| spl12_160
| spl12_165
| spl12_170 ),
inference(avatar_split_clause,[],[f418,f1324,f1300,f1276,f1252]) ).
fof(f1328,plain,
( ~ spl12_155
| spl12_160
| spl12_167
| spl12_170 ),
inference(avatar_split_clause,[],[f417,f1324,f1309,f1276,f1252]) ).
fof(f1330,plain,
( ~ spl12_155
| spl12_160
| spl12_169
| spl12_170 ),
inference(avatar_split_clause,[],[f415,f1324,f1319,f1276,f1252]) ).
fof(f1340,definition,
( spl12_172
<=> e13 = op1(op1(e13,e13),op1(e13,e13)) ),
introduced(definition,[new_symbols(definition,[spl12_172])],[avatar_definition]) ).
fof(f1342,plain,
( e13 = op1(op1(e13,e13),op1(e13,e13))
| ~ spl12_172 ),
inference(avatar_component_clause,[],[f1340]) ).
fof(f1343,plain,
( ~ spl12_155
| spl12_160
| spl12_165
| spl12_172 ),
inference(avatar_split_clause,[],[f410,f1340,f1300,f1276,f1252]) ).
fof(f1348,definition,
( spl12_173
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl12_173])],[avatar_definition]) ).
fof(f1350,plain,
( e20 = op2(e20,e20)
| ~ spl12_173 ),
inference(avatar_component_clause,[],[f1348]) ).
fof(f1352,definition,
( spl12_174
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_174])],[avatar_definition]) ).
fof(f1356,definition,
( spl12_175
<=> e20 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_175])],[avatar_definition]) ).
fof(f1358,plain,
( e20 = op2(e20,e22)
| ~ spl12_175 ),
inference(avatar_component_clause,[],[f1356]) ).
fof(f1360,definition,
( spl12_176
<=> e20 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_176])],[avatar_definition]) ).
fof(f1362,plain,
( e20 = op2(e20,e23)
| ~ spl12_176 ),
inference(avatar_component_clause,[],[f1360]) ).
fof(f1363,plain,
( spl12_173
| spl12_174
| spl12_175
| spl12_176 ),
inference(avatar_split_clause,[],[f85,f1360,f1356,f1352,f1348]) ).
fof(f1365,definition,
( spl12_177
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_177])],[avatar_definition]) ).
fof(f1367,plain,
( e20 = op2(e21,e20)
| ~ spl12_177 ),
inference(avatar_component_clause,[],[f1365]) ).
fof(f1369,definition,
( spl12_178
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_178])],[avatar_definition]) ).
fof(f1371,plain,
( e20 = op2(e22,e20)
| ~ spl12_178 ),
inference(avatar_component_clause,[],[f1369]) ).
fof(f1373,definition,
( spl12_179
<=> e20 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_179])],[avatar_definition]) ).
fof(f1375,plain,
( e20 = op2(e23,e20)
| ~ spl12_179 ),
inference(avatar_component_clause,[],[f1373]) ).
fof(f1376,plain,
( spl12_173
| spl12_177
| spl12_178
| spl12_179 ),
inference(avatar_split_clause,[],[f86,f1373,f1369,f1365,f1348]) ).
fof(f1378,definition,
( spl12_180
<=> op2(e20,e20) = e21 ),
introduced(definition,[new_symbols(definition,[spl12_180])],[avatar_definition]) ).
fof(f1380,plain,
( op2(e20,e20) = e21
| ~ spl12_180 ),
inference(avatar_component_clause,[],[f1378]) ).
fof(f1382,definition,
( spl12_181
<=> e21 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_181])],[avatar_definition]) ).
fof(f1384,plain,
( e21 = op2(e20,e21)
| ~ spl12_181 ),
inference(avatar_component_clause,[],[f1382]) ).
fof(f1386,definition,
( spl12_182
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_182])],[avatar_definition]) ).
fof(f1388,plain,
( e21 = op2(e20,e22)
| ~ spl12_182 ),
inference(avatar_component_clause,[],[f1386]) ).
fof(f1390,definition,
( spl12_183
<=> e21 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_183])],[avatar_definition]) ).
fof(f1393,plain,
( spl12_180
| spl12_181
| spl12_182
| spl12_183 ),
inference(avatar_split_clause,[],[f87,f1390,f1386,f1382,f1378]) ).
fof(f1395,definition,
( spl12_184
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_184])],[avatar_definition]) ).
fof(f1397,plain,
( e21 = op2(e21,e20)
| ~ spl12_184 ),
inference(avatar_component_clause,[],[f1395]) ).
fof(f1399,definition,
( spl12_185
<=> e21 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_185])],[avatar_definition]) ).
fof(f1401,plain,
( e21 = op2(e22,e20)
| ~ spl12_185 ),
inference(avatar_component_clause,[],[f1399]) ).
fof(f1403,definition,
( spl12_186
<=> e21 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_186])],[avatar_definition]) ).
fof(f1406,plain,
( spl12_180
| spl12_184
| spl12_185
| spl12_186 ),
inference(avatar_split_clause,[],[f88,f1403,f1399,f1395,f1378]) ).
fof(f1408,definition,
( spl12_187
<=> op2(e20,e20) = e22 ),
introduced(definition,[new_symbols(definition,[spl12_187])],[avatar_definition]) ).
fof(f1409,plain,
( op2(e20,e20) != e22
| spl12_187 ),
inference(avatar_component_clause,[],[f1408]) ).
fof(f1412,definition,
( spl12_188
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_188])],[avatar_definition]) ).
fof(f1416,definition,
( spl12_189
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_189])],[avatar_definition]) ).
fof(f1418,plain,
( e22 = op2(e20,e22)
| ~ spl12_189 ),
inference(avatar_component_clause,[],[f1416]) ).
fof(f1420,definition,
( spl12_190
<=> e22 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_190])],[avatar_definition]) ).
fof(f1422,plain,
( e22 = op2(e20,e23)
| ~ spl12_190 ),
inference(avatar_component_clause,[],[f1420]) ).
fof(f1425,definition,
( spl12_191
<=> e22 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_191])],[avatar_definition]) ).
fof(f1427,plain,
( e22 = op2(e21,e20)
| ~ spl12_191 ),
inference(avatar_component_clause,[],[f1425]) ).
fof(f1429,definition,
( spl12_192
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_192])],[avatar_definition]) ).
fof(f1431,plain,
( e22 = op2(e22,e20)
| ~ spl12_192 ),
inference(avatar_component_clause,[],[f1429]) ).
fof(f1433,definition,
( spl12_193
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_193])],[avatar_definition]) ).
fof(f1435,plain,
( e22 = op2(e23,e20)
| ~ spl12_193 ),
inference(avatar_component_clause,[],[f1433]) ).
fof(f1438,definition,
( spl12_194
<=> op2(e20,e20) = e23 ),
introduced(definition,[new_symbols(definition,[spl12_194])],[avatar_definition]) ).
fof(f1440,plain,
( op2(e20,e20) = e23
| ~ spl12_194 ),
inference(avatar_component_clause,[],[f1438]) ).
fof(f1442,definition,
( spl12_195
<=> e23 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_195])],[avatar_definition]) ).
fof(f1444,plain,
( e23 = op2(e20,e21)
| ~ spl12_195 ),
inference(avatar_component_clause,[],[f1442]) ).
fof(f1450,definition,
( spl12_197
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_197])],[avatar_definition]) ).
fof(f1452,plain,
( e23 = op2(e20,e23)
| ~ spl12_197 ),
inference(avatar_component_clause,[],[f1450]) ).
fof(f1463,definition,
( spl12_200
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_200])],[avatar_definition]) ).
fof(f1465,plain,
( e23 = op2(e23,e20)
| ~ spl12_200 ),
inference(avatar_component_clause,[],[f1463]) ).
fof(f1468,definition,
( spl12_201
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_201])],[avatar_definition]) ).
fof(f1469,plain,
( e20 != op2(e21,e21)
| spl12_201 ),
inference(avatar_component_clause,[],[f1468]) ).
fof(f1470,plain,
( e20 = op2(e21,e21)
| ~ spl12_201 ),
inference(avatar_component_clause,[],[f1468]) ).
fof(f1472,definition,
( spl12_202
<=> e20 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_202])],[avatar_definition]) ).
fof(f1474,plain,
( e20 = op2(e21,e22)
| ~ spl12_202 ),
inference(avatar_component_clause,[],[f1472]) ).
fof(f1476,definition,
( spl12_203
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_203])],[avatar_definition]) ).
fof(f1478,plain,
( e20 = op2(e21,e23)
| ~ spl12_203 ),
inference(avatar_component_clause,[],[f1476]) ).
fof(f1479,plain,
( spl12_177
| spl12_201
| spl12_202
| spl12_203 ),
inference(avatar_split_clause,[],[f93,f1476,f1472,f1468,f1365]) ).
fof(f1485,definition,
( spl12_205
<=> e20 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_205])],[avatar_definition]) ).
fof(f1487,plain,
( e20 = op2(e23,e21)
| ~ spl12_205 ),
inference(avatar_component_clause,[],[f1485]) ).
fof(f1490,definition,
( spl12_206
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_206])],[avatar_definition]) ).
fof(f1491,plain,
( e21 != op2(e21,e21)
| spl12_206 ),
inference(avatar_component_clause,[],[f1490]) ).
fof(f1492,plain,
( e21 = op2(e21,e21)
| ~ spl12_206 ),
inference(avatar_component_clause,[],[f1490]) ).
fof(f1494,definition,
( spl12_207
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_207])],[avatar_definition]) ).
fof(f1496,plain,
( e21 = op2(e21,e22)
| ~ spl12_207 ),
inference(avatar_component_clause,[],[f1494]) ).
fof(f1498,definition,
( spl12_208
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_208])],[avatar_definition]) ).
fof(f1499,plain,
( e21 != op2(e21,e23)
| spl12_208 ),
inference(avatar_component_clause,[],[f1498]) ).
fof(f1501,plain,
( spl12_184
| spl12_206
| spl12_207
| spl12_208 ),
inference(avatar_split_clause,[],[f95,f1498,f1494,f1490,f1395]) ).
fof(f1503,definition,
( spl12_209
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_209])],[avatar_definition]) ).
fof(f1505,plain,
( e21 = op2(e22,e21)
| ~ spl12_209 ),
inference(avatar_component_clause,[],[f1503]) ).
fof(f1507,definition,
( spl12_210
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_210])],[avatar_definition]) ).
fof(f1510,plain,
( spl12_181
| spl12_206
| spl12_209
| spl12_210 ),
inference(avatar_split_clause,[],[f96,f1507,f1503,f1490,f1382]) ).
fof(f1512,definition,
( spl12_211
<=> e22 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_211])],[avatar_definition]) ).
fof(f1513,plain,
( e22 != op2(e21,e21)
| spl12_211 ),
inference(avatar_component_clause,[],[f1512]) ).
fof(f1514,plain,
( e22 = op2(e21,e21)
| ~ spl12_211 ),
inference(avatar_component_clause,[],[f1512]) ).
fof(f1516,definition,
( spl12_212
<=> e22 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_212])],[avatar_definition]) ).
fof(f1518,plain,
( e22 = op2(e21,e22)
| ~ spl12_212 ),
inference(avatar_component_clause,[],[f1516]) ).
fof(f1520,definition,
( spl12_213
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_213])],[avatar_definition]) ).
fof(f1522,plain,
( e22 = op2(e21,e23)
| ~ spl12_213 ),
inference(avatar_component_clause,[],[f1520]) ).
fof(f1523,plain,
( spl12_191
| spl12_211
| spl12_212
| spl12_213 ),
inference(avatar_split_clause,[],[f97,f1520,f1516,f1512,f1425]) ).
fof(f1525,definition,
( spl12_214
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_214])],[avatar_definition]) ).
fof(f1527,plain,
( e22 = op2(e22,e21)
| ~ spl12_214 ),
inference(avatar_component_clause,[],[f1525]) ).
fof(f1529,definition,
( spl12_215
<=> e22 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_215])],[avatar_definition]) ).
fof(f1531,plain,
( e22 = op2(e23,e21)
| ~ spl12_215 ),
inference(avatar_component_clause,[],[f1529]) ).
fof(f1532,plain,
( spl12_188
| spl12_211
| spl12_214
| spl12_215 ),
inference(avatar_split_clause,[],[f98,f1529,f1525,f1512,f1412]) ).
fof(f1534,definition,
( spl12_216
<=> e23 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_216])],[avatar_definition]) ).
fof(f1536,plain,
( e23 = op2(e21,e21)
| ~ spl12_216 ),
inference(avatar_component_clause,[],[f1534]) ).
fof(f1542,definition,
( spl12_218
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_218])],[avatar_definition]) ).
fof(f1544,plain,
( e23 = op2(e21,e23)
| ~ spl12_218 ),
inference(avatar_component_clause,[],[f1542]) ).
fof(f1556,definition,
( spl12_221
<=> e20 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_221])],[avatar_definition]) ).
fof(f1557,plain,
( e20 != op2(e22,e22)
| spl12_221 ),
inference(avatar_component_clause,[],[f1556]) ).
fof(f1558,plain,
( e20 = op2(e22,e22)
| ~ spl12_221 ),
inference(avatar_component_clause,[],[f1556]) ).
fof(f1560,definition,
( spl12_222
<=> e20 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_222])],[avatar_definition]) ).
fof(f1562,plain,
( e20 = op2(e22,e23)
| ~ spl12_222 ),
inference(avatar_component_clause,[],[f1560]) ).
fof(f1565,definition,
( spl12_223
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_223])],[avatar_definition]) ).
fof(f1568,plain,
( spl12_175
| spl12_202
| spl12_221
| spl12_223 ),
inference(avatar_split_clause,[],[f102,f1565,f1556,f1472,f1356]) ).
fof(f1570,definition,
( spl12_224
<=> e21 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_224])],[avatar_definition]) ).
fof(f1571,plain,
( e21 != op2(e22,e22)
| spl12_224 ),
inference(avatar_component_clause,[],[f1570]) ).
fof(f1572,plain,
( e21 = op2(e22,e22)
| ~ spl12_224 ),
inference(avatar_component_clause,[],[f1570]) ).
fof(f1574,definition,
( spl12_225
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_225])],[avatar_definition]) ).
fof(f1579,definition,
( spl12_226
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_226])],[avatar_definition]) ).
fof(f1582,plain,
( spl12_182
| spl12_207
| spl12_224
| spl12_226 ),
inference(avatar_split_clause,[],[f104,f1579,f1570,f1494,f1386]) ).
fof(f1584,definition,
( spl12_227
<=> e22 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_227])],[avatar_definition]) ).
fof(f1585,plain,
( e22 != op2(e22,e22)
| spl12_227 ),
inference(avatar_component_clause,[],[f1584]) ).
fof(f1586,plain,
( e22 = op2(e22,e22)
| ~ spl12_227 ),
inference(avatar_component_clause,[],[f1584]) ).
fof(f1588,definition,
( spl12_228
<=> e22 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_228])],[avatar_definition]) ).
fof(f1589,plain,
( e22 != op2(e22,e23)
| spl12_228 ),
inference(avatar_component_clause,[],[f1588]) ).
fof(f1591,plain,
( spl12_192
| spl12_214
| spl12_227
| spl12_228 ),
inference(avatar_split_clause,[],[f105,f1588,f1584,f1525,f1429]) ).
fof(f1593,definition,
( spl12_229
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_229])],[avatar_definition]) ).
fof(f1595,plain,
( e22 = op2(e23,e22)
| ~ spl12_229 ),
inference(avatar_component_clause,[],[f1593]) ).
fof(f1596,plain,
( spl12_189
| spl12_212
| spl12_227
| spl12_229 ),
inference(avatar_split_clause,[],[f106,f1593,f1584,f1516,f1416]) ).
fof(f1598,definition,
( spl12_230
<=> e23 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_230])],[avatar_definition]) ).
fof(f1600,plain,
( e23 = op2(e22,e22)
| ~ spl12_230 ),
inference(avatar_component_clause,[],[f1598]) ).
fof(f1602,definition,
( spl12_231
<=> e23 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_231])],[avatar_definition]) ).
fof(f1604,plain,
( e23 = op2(e22,e23)
| ~ spl12_231 ),
inference(avatar_component_clause,[],[f1602]) ).
fof(f1607,definition,
( spl12_232
<=> e23 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_232])],[avatar_definition]) ).
fof(f1609,plain,
( e23 = op2(e23,e22)
| ~ spl12_232 ),
inference(avatar_component_clause,[],[f1607]) ).
fof(f1612,definition,
( spl12_233
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_233])],[avatar_definition]) ).
fof(f1614,plain,
( e20 = op2(e23,e23)
| ~ spl12_233 ),
inference(avatar_component_clause,[],[f1612]) ).
fof(f1616,plain,
( spl12_176
| spl12_203
| spl12_222
| spl12_233 ),
inference(avatar_split_clause,[],[f110,f1612,f1560,f1476,f1360]) ).
fof(f1618,definition,
( spl12_234
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_234])],[avatar_definition]) ).
fof(f1620,plain,
( e21 = op2(e23,e23)
| ~ spl12_234 ),
inference(avatar_component_clause,[],[f1618]) ).
fof(f1630,definition,
( spl12_236
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_236])],[avatar_definition]) ).
fof(f1631,plain,
( e23 != op2(e23,e23)
| spl12_236 ),
inference(avatar_component_clause,[],[f1630]) ).
fof(f1632,plain,
( e23 = op2(e23,e23)
| ~ spl12_236 ),
inference(avatar_component_clause,[],[f1630]) ).
fof(f1634,plain,
( spl12_197
| spl12_218
| spl12_231
| spl12_236 ),
inference(avatar_split_clause,[],[f116,f1630,f1602,f1542,f1450]) ).
fof(f1635,plain,
( spl12_173
| spl12_180
| spl12_187
| spl12_194 ),
inference(avatar_split_clause,[],[f69,f1438,f1408,f1378,f1348]) ).
fof(f1636,plain,
( spl12_174
| spl12_181
| spl12_188
| spl12_195 ),
inference(avatar_split_clause,[],[f70,f1442,f1412,f1382,f1352]) ).
fof(f1642,plain,
( spl12_203
| spl12_208
| spl12_213
| spl12_218 ),
inference(avatar_split_clause,[],[f76,f1542,f1520,f1498,f1476]) ).
fof(f1646,plain,
( spl12_222
| spl12_225
| spl12_228
| spl12_231 ),
inference(avatar_split_clause,[],[f80,f1602,f1588,f1574,f1560]) ).
fof(f1647,plain,
( spl12_179
| spl12_186
| spl12_193
| spl12_200 ),
inference(avatar_split_clause,[],[f81,f1463,f1433,f1403,f1373]) ).
fof(f1649,plain,
( spl12_223
| spl12_226
| spl12_229
| spl12_232 ),
inference(avatar_split_clause,[],[f83,f1607,f1593,f1579,f1565]) ).
fof(f1652,definition,
( spl12_237
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl12_237])],[avatar_definition]) ).
fof(f1654,plain,
( e10 = op1(e10,e10)
| ~ spl12_237 ),
inference(avatar_component_clause,[],[f1652]) ).
fof(f1656,definition,
( spl12_238
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_238])],[avatar_definition]) ).
fof(f1660,definition,
( spl12_239
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_239])],[avatar_definition]) ).
fof(f1662,plain,
( e10 = op1(e10,e12)
| ~ spl12_239 ),
inference(avatar_component_clause,[],[f1660]) ).
fof(f1664,definition,
( spl12_240
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_240])],[avatar_definition]) ).
fof(f1666,plain,
( e10 = op1(e10,e13)
| ~ spl12_240 ),
inference(avatar_component_clause,[],[f1664]) ).
fof(f1667,plain,
( spl12_237
| spl12_238
| spl12_239
| spl12_240 ),
inference(avatar_split_clause,[],[f37,f1664,f1660,f1656,f1652]) ).
fof(f1669,definition,
( spl12_241
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl12_241])],[avatar_definition]) ).
fof(f1671,plain,
( e10 = op1(e11,e10)
| ~ spl12_241 ),
inference(avatar_component_clause,[],[f1669]) ).
fof(f1673,definition,
( spl12_242
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_242])],[avatar_definition]) ).
fof(f1675,plain,
( e10 = op1(e12,e10)
| ~ spl12_242 ),
inference(avatar_component_clause,[],[f1673]) ).
fof(f1677,definition,
( spl12_243
<=> e10 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_243])],[avatar_definition]) ).
fof(f1680,plain,
( spl12_237
| spl12_241
| spl12_242
| spl12_243 ),
inference(avatar_split_clause,[],[f38,f1677,f1673,f1669,f1652]) ).
fof(f1682,definition,
( spl12_244
<=> op1(e10,e10) = e11 ),
introduced(definition,[new_symbols(definition,[spl12_244])],[avatar_definition]) ).
fof(f1683,plain,
( op1(e10,e10) != e11
| spl12_244 ),
inference(avatar_component_clause,[],[f1682]) ).
fof(f1684,plain,
( op1(e10,e10) = e11
| ~ spl12_244 ),
inference(avatar_component_clause,[],[f1682]) ).
fof(f1686,definition,
( spl12_245
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_245])],[avatar_definition]) ).
fof(f1688,plain,
( e11 = op1(e10,e11)
| ~ spl12_245 ),
inference(avatar_component_clause,[],[f1686]) ).
fof(f1690,definition,
( spl12_246
<=> e11 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_246])],[avatar_definition]) ).
fof(f1692,plain,
( e11 = op1(e10,e12)
| ~ spl12_246 ),
inference(avatar_component_clause,[],[f1690]) ).
fof(f1699,definition,
( spl12_248
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl12_248])],[avatar_definition]) ).
fof(f1701,plain,
( e11 = op1(e11,e10)
| ~ spl12_248 ),
inference(avatar_component_clause,[],[f1699]) ).
fof(f1703,definition,
( spl12_249
<=> e11 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_249])],[avatar_definition]) ).
fof(f1705,plain,
( e11 = op1(e12,e10)
| ~ spl12_249 ),
inference(avatar_component_clause,[],[f1703]) ).
fof(f1707,definition,
( spl12_250
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_250])],[avatar_definition]) ).
fof(f1709,plain,
( e11 = op1(e13,e10)
| ~ spl12_250 ),
inference(avatar_component_clause,[],[f1707]) ).
fof(f1710,plain,
( spl12_244
| spl12_248
| spl12_249
| spl12_250 ),
inference(avatar_split_clause,[],[f40,f1707,f1703,f1699,f1682]) ).
fof(f1712,definition,
( spl12_251
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[spl12_251])],[avatar_definition]) ).
fof(f1713,plain,
( op1(e10,e10) != e12
| spl12_251 ),
inference(avatar_component_clause,[],[f1712]) ).
fof(f1714,plain,
( op1(e10,e10) = e12
| ~ spl12_251 ),
inference(avatar_component_clause,[],[f1712]) ).
fof(f1716,definition,
( spl12_252
<=> e12 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_252])],[avatar_definition]) ).
fof(f1720,definition,
( spl12_253
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_253])],[avatar_definition]) ).
fof(f1722,plain,
( e12 = op1(e10,e12)
| ~ spl12_253 ),
inference(avatar_component_clause,[],[f1720]) ).
fof(f1724,definition,
( spl12_254
<=> e12 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_254])],[avatar_definition]) ).
fof(f1726,plain,
( e12 = op1(e10,e13)
| ~ spl12_254 ),
inference(avatar_component_clause,[],[f1724]) ).
fof(f1733,definition,
( spl12_256
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_256])],[avatar_definition]) ).
fof(f1735,plain,
( e12 = op1(e12,e10)
| ~ spl12_256 ),
inference(avatar_component_clause,[],[f1733]) ).
fof(f1737,definition,
( spl12_257
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_257])],[avatar_definition]) ).
fof(f1739,plain,
( e12 = op1(e13,e10)
| ~ spl12_257 ),
inference(avatar_component_clause,[],[f1737]) ).
fof(f1742,definition,
( spl12_258
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl12_258])],[avatar_definition]) ).
fof(f1743,plain,
( op1(e10,e10) != e13
| spl12_258 ),
inference(avatar_component_clause,[],[f1742]) ).
fof(f1744,plain,
( op1(e10,e10) = e13
| ~ spl12_258 ),
inference(avatar_component_clause,[],[f1742]) ).
fof(f1746,definition,
( spl12_259
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_259])],[avatar_definition]) ).
fof(f1748,plain,
( e13 = op1(e10,e11)
| ~ spl12_259 ),
inference(avatar_component_clause,[],[f1746]) ).
fof(f1750,definition,
( spl12_260
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_260])],[avatar_definition]) ).
fof(f1752,plain,
( e13 = op1(e10,e12)
| ~ spl12_260 ),
inference(avatar_component_clause,[],[f1750]) ).
fof(f1754,definition,
( spl12_261
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_261])],[avatar_definition]) ).
fof(f1756,plain,
( e13 = op1(e10,e13)
| ~ spl12_261 ),
inference(avatar_component_clause,[],[f1754]) ).
fof(f1757,plain,
( spl12_258
| spl12_259
| spl12_260
| spl12_261 ),
inference(avatar_split_clause,[],[f43,f1754,f1750,f1746,f1742]) ).
fof(f1767,definition,
( spl12_264
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_264])],[avatar_definition]) ).
fof(f1769,plain,
( e13 = op1(e13,e10)
| ~ spl12_264 ),
inference(avatar_component_clause,[],[f1767]) ).
fof(f1772,definition,
( spl12_265
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_265])],[avatar_definition]) ).
fof(f1773,plain,
( e10 != op1(e11,e11)
| spl12_265 ),
inference(avatar_component_clause,[],[f1772]) ).
fof(f1776,definition,
( spl12_266
<=> e10 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_266])],[avatar_definition]) ).
fof(f1778,plain,
( e10 = op1(e11,e12)
| ~ spl12_266 ),
inference(avatar_component_clause,[],[f1776]) ).
fof(f1780,definition,
( spl12_267
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_267])],[avatar_definition]) ).
fof(f1782,plain,
( e10 = op1(e11,e13)
| ~ spl12_267 ),
inference(avatar_component_clause,[],[f1780]) ).
fof(f1783,plain,
( spl12_241
| spl12_265
| spl12_266
| spl12_267 ),
inference(avatar_split_clause,[],[f45,f1780,f1776,f1772,f1669]) ).
fof(f1785,definition,
( spl12_268
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_268])],[avatar_definition]) ).
fof(f1789,definition,
( spl12_269
<=> e10 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_269])],[avatar_definition]) ).
fof(f1791,plain,
( e10 = op1(e13,e11)
| ~ spl12_269 ),
inference(avatar_component_clause,[],[f1789]) ).
fof(f1798,definition,
( spl12_271
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_271])],[avatar_definition]) ).
fof(f1800,plain,
( e11 = op1(e11,e12)
| ~ spl12_271 ),
inference(avatar_component_clause,[],[f1798]) ).
fof(f1807,definition,
( spl12_273
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_273])],[avatar_definition]) ).
fof(f1809,plain,
( e11 = op1(e12,e11)
| ~ spl12_273 ),
inference(avatar_component_clause,[],[f1807]) ).
fof(f1816,definition,
( spl12_275
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_275])],[avatar_definition]) ).
fof(f1818,plain,
( e12 = op1(e11,e11)
| ~ spl12_275 ),
inference(avatar_component_clause,[],[f1816]) ).
fof(f1820,definition,
( spl12_276
<=> e12 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_276])],[avatar_definition]) ).
fof(f1822,plain,
( e12 = op1(e11,e12)
| ~ spl12_276 ),
inference(avatar_component_clause,[],[f1820]) ).
fof(f1829,definition,
( spl12_278
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_278])],[avatar_definition]) ).
fof(f1831,plain,
( e12 = op1(e12,e11)
| ~ spl12_278 ),
inference(avatar_component_clause,[],[f1829]) ).
fof(f1833,definition,
( spl12_279
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_279])],[avatar_definition]) ).
fof(f1835,plain,
( e12 = op1(e13,e11)
| ~ spl12_279 ),
inference(avatar_component_clause,[],[f1833]) ).
fof(f1838,definition,
( spl12_280
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_280])],[avatar_definition]) ).
fof(f1840,plain,
( e13 = op1(e11,e11)
| ~ spl12_280 ),
inference(avatar_component_clause,[],[f1838]) ).
fof(f1846,definition,
( spl12_282
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_282])],[avatar_definition]) ).
fof(f1848,plain,
( e13 = op1(e11,e13)
| ~ spl12_282 ),
inference(avatar_component_clause,[],[f1846]) ).
fof(f1855,definition,
( spl12_284
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_284])],[avatar_definition]) ).
fof(f1857,plain,
( e13 = op1(e13,e11)
| ~ spl12_284 ),
inference(avatar_component_clause,[],[f1855]) ).
fof(f1860,definition,
( spl12_285
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_285])],[avatar_definition]) ).
fof(f1862,plain,
( e10 = op1(e12,e12)
| ~ spl12_285 ),
inference(avatar_component_clause,[],[f1860]) ).
fof(f1864,definition,
( spl12_286
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_286])],[avatar_definition]) ).
fof(f1866,plain,
( e10 = op1(e12,e13)
| ~ spl12_286 ),
inference(avatar_component_clause,[],[f1864]) ).
fof(f1867,plain,
( spl12_242
| spl12_268
| spl12_285
| spl12_286 ),
inference(avatar_split_clause,[],[f53,f1864,f1860,f1785,f1673]) ).
fof(f1874,definition,
( spl12_288
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_288])],[avatar_definition]) ).
fof(f1876,plain,
( e11 = op1(e12,e12)
| ~ spl12_288 ),
inference(avatar_component_clause,[],[f1874]) ).
fof(f1878,definition,
( spl12_289
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_289])],[avatar_definition]) ).
fof(f1881,plain,
( spl12_249
| spl12_273
| spl12_288
| spl12_289 ),
inference(avatar_split_clause,[],[f55,f1878,f1874,f1807,f1703]) ).
fof(f1883,definition,
( spl12_290
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_290])],[avatar_definition]) ).
fof(f1886,plain,
( spl12_246
| spl12_271
| spl12_288
| spl12_290 ),
inference(avatar_split_clause,[],[f56,f1883,f1874,f1798,f1690]) ).
fof(f1888,definition,
( spl12_291
<=> e12 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_291])],[avatar_definition]) ).
fof(f1890,plain,
( e12 = op1(e12,e12)
| ~ spl12_291 ),
inference(avatar_component_clause,[],[f1888]) ).
fof(f1892,definition,
( spl12_292
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_292])],[avatar_definition]) ).
fof(f1894,plain,
( e12 = op1(e12,e13)
| ~ spl12_292 ),
inference(avatar_component_clause,[],[f1892]) ).
fof(f1895,plain,
( spl12_256
| spl12_278
| spl12_291
| spl12_292 ),
inference(avatar_split_clause,[],[f57,f1892,f1888,f1829,f1733]) ).
fof(f1897,definition,
( spl12_293
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_293])],[avatar_definition]) ).
fof(f1899,plain,
( e12 = op1(e13,e12)
| ~ spl12_293 ),
inference(avatar_component_clause,[],[f1897]) ).
fof(f1900,plain,
( spl12_253
| spl12_276
| spl12_291
| spl12_293 ),
inference(avatar_split_clause,[],[f58,f1897,f1888,f1820,f1720]) ).
fof(f1902,definition,
( spl12_294
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_294])],[avatar_definition]) ).
fof(f1904,plain,
( e13 = op1(e12,e12)
| ~ spl12_294 ),
inference(avatar_component_clause,[],[f1902]) ).
fof(f1906,definition,
( spl12_295
<=> e13 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_295])],[avatar_definition]) ).
fof(f1908,plain,
( e13 = op1(e12,e13)
| ~ spl12_295 ),
inference(avatar_component_clause,[],[f1906]) ).
fof(f1911,definition,
( spl12_296
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_296])],[avatar_definition]) ).
fof(f1913,plain,
( e13 = op1(e13,e12)
| ~ spl12_296 ),
inference(avatar_component_clause,[],[f1911]) ).
fof(f1916,definition,
( spl12_297
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_297])],[avatar_definition]) ).
fof(f1918,plain,
( e10 = op1(e13,e13)
| ~ spl12_297 ),
inference(avatar_component_clause,[],[f1916]) ).
fof(f1920,plain,
( spl12_240
| spl12_267
| spl12_286
| spl12_297 ),
inference(avatar_split_clause,[],[f62,f1916,f1864,f1780,f1664]) ).
fof(f1922,definition,
( spl12_298
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_298])],[avatar_definition]) ).
fof(f1924,plain,
( e11 = op1(e13,e13)
| ~ spl12_298 ),
inference(avatar_component_clause,[],[f1922]) ).
fof(f1928,definition,
( spl12_299
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_299])],[avatar_definition]) ).
fof(f1930,plain,
( e12 = op1(e13,e13)
| ~ spl12_299 ),
inference(avatar_component_clause,[],[f1928]) ).
fof(f1931,plain,
( spl12_257
| spl12_279
| spl12_293
| spl12_299 ),
inference(avatar_split_clause,[],[f65,f1928,f1897,f1833,f1737]) ).
fof(f1934,definition,
( spl12_300
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_300])],[avatar_definition]) ).
fof(f1935,plain,
( e13 != op1(e13,e13)
| spl12_300 ),
inference(avatar_component_clause,[],[f1934]) ).
fof(f1936,plain,
( e13 = op1(e13,e13)
| ~ spl12_300 ),
inference(avatar_component_clause,[],[f1934]) ).
fof(f1937,plain,
( spl12_264
| spl12_284
| spl12_296
| spl12_300 ),
inference(avatar_split_clause,[],[f67,f1934,f1911,f1855,f1767]) ).
fof(f1938,plain,
( spl12_261
| spl12_282
| spl12_295
| spl12_300 ),
inference(avatar_split_clause,[],[f68,f1934,f1906,f1846,f1754]) ).
fof(f1940,plain,
( spl12_238
| spl12_245
| spl12_252
| spl12_259 ),
inference(avatar_split_clause,[],[f22,f1746,f1716,f1686,f1656]) ).
fof(f1955,plain,
( e20 != e21
| ~ spl12_2
| spl12_7 ),
inference(forward_demodulation,[],[f542,f517]) ).
fof(f1959,plain,
spl12_298,
inference(avatar_split_clause,[],[f290,f1922]) ).
fof(f1960,plain,
spl12_234,
inference(avatar_split_clause,[],[f293,f1618]) ).
fof(f1981,plain,
( e20 = e21
| ~ spl12_173
| ~ spl12_180 ),
inference(forward_demodulation,[],[f1380,f1350]) ).
fof(f1983,plain,
( $false
| ~ spl12_2
| spl12_7
| ~ spl12_173
| ~ spl12_180 ),
inference(forward_subsumption_resolution,[],[f1981,f1955]) ).
fof(f1984,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_173
| ~ spl12_180 ),
inference(avatar_contradiction_clause,[],[f1983]) ).
fof(f1988,plain,
( e20 = e22
| ~ spl12_22
| ~ spl12_105 ),
inference(forward_demodulation,[],[f613,f993]) ).
fof(f1999,plain,
( e22 = op2(e22,e23)
| ~ spl12_22
| ~ spl12_105
| ~ spl12_190 ),
inference(superposition,[],[f1422,f1988]) ).
fof(f2000,plain,
( spl12_228
| ~ spl12_22
| ~ spl12_105
| ~ spl12_190 ),
inference(avatar_split_clause,[],[f1999,f1420,f992,f612,f1588]) ).
fof(f2006,plain,
( e20 = e21
| ~ spl12_2
| ~ spl12_7 ),
inference(forward_demodulation,[],[f541,f517]) ).
fof(f2007,plain,
( e20 != e22
| spl12_22
| ~ spl12_105 ),
inference(forward_demodulation,[],[f614,f993]) ).
fof(f2020,plain,
( e20 = e22
| ~ spl12_175
| ~ spl12_189 ),
inference(forward_demodulation,[],[f1358,f1418]) ).
fof(f2021,plain,
( $false
| spl12_22
| ~ spl12_105
| ~ spl12_175
| ~ spl12_189 ),
inference(forward_subsumption_resolution,[],[f2020,f2007]) ).
fof(f2022,plain,
( spl12_22
| ~ spl12_105
| ~ spl12_175
| ~ spl12_189 ),
inference(avatar_contradiction_clause,[],[f2021]) ).
fof(f2024,plain,
( e20 = e22
| ~ spl12_176
| ~ spl12_190 ),
inference(forward_demodulation,[],[f1362,f1422]) ).
fof(f2025,plain,
( $false
| spl12_22
| ~ spl12_105
| ~ spl12_176
| ~ spl12_190 ),
inference(forward_subsumption_resolution,[],[f2024,f2007]) ).
fof(f2026,plain,
( spl12_22
| ~ spl12_105
| ~ spl12_176
| ~ spl12_190 ),
inference(avatar_contradiction_clause,[],[f2025]) ).
fof(f2041,plain,
( $false
| ~ spl12_2
| ~ spl12_7 ),
inference(forward_subsumption_resolution,[],[f224,f2006]) ).
fof(f2042,plain,
( ~ spl12_2
| ~ spl12_7 ),
inference(avatar_contradiction_clause,[],[f2041]) ).
fof(f2047,plain,
( e20 = e21
| ~ spl12_177
| ~ spl12_184 ),
inference(superposition,[],[f1367,f1397]) ).
fof(f2051,plain,
( $false
| ~ spl12_2
| spl12_7
| ~ spl12_177
| ~ spl12_184 ),
inference(forward_subsumption_resolution,[],[f2047,f1955]) ).
fof(f2052,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_177
| ~ spl12_184 ),
inference(avatar_contradiction_clause,[],[f2051]) ).
fof(f2106,plain,
( e22 = e23
| ~ spl12_190
| ~ spl12_197 ),
inference(superposition,[],[f1452,f1422]) ).
fof(f2110,plain,
( $false
| ~ spl12_190
| ~ spl12_197 ),
inference(forward_subsumption_resolution,[],[f2106,f219]) ).
fof(f2111,plain,
( ~ spl12_190
| ~ spl12_197 ),
inference(avatar_contradiction_clause,[],[f2110]) ).
fof(f2156,plain,
( e20 = e21
| ~ spl12_201
| ~ spl12_206 ),
inference(forward_demodulation,[],[f1492,f1470]) ).
fof(f2157,plain,
( $false
| ~ spl12_2
| spl12_7
| ~ spl12_201
| ~ spl12_206 ),
inference(forward_subsumption_resolution,[],[f2156,f1955]) ).
fof(f2158,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_201
| ~ spl12_206 ),
inference(avatar_contradiction_clause,[],[f2157]) ).
fof(f2160,plain,
( e20 = e21
| ~ spl12_202
| ~ spl12_207 ),
inference(forward_demodulation,[],[f1496,f1474]) ).
fof(f2161,plain,
( $false
| ~ spl12_2
| spl12_7
| ~ spl12_202
| ~ spl12_207 ),
inference(forward_subsumption_resolution,[],[f2160,f1955]) ).
fof(f2162,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_202
| ~ spl12_207 ),
inference(avatar_contradiction_clause,[],[f2161]) ).
fof(f2168,plain,
( e21 = e22
| ~ spl12_206
| ~ spl12_211 ),
inference(superposition,[],[f1514,f1492]) ).
fof(f2173,plain,
( $false
| ~ spl12_206
| ~ spl12_211 ),
inference(forward_subsumption_resolution,[],[f2168,f221]) ).
fof(f2174,plain,
( ~ spl12_206
| ~ spl12_211 ),
inference(avatar_contradiction_clause,[],[f2173]) ).
fof(f2176,plain,
( e21 = e22
| ~ spl12_207
| ~ spl12_212 ),
inference(superposition,[],[f1518,f1496]) ).
fof(f2181,plain,
( $false
| ~ spl12_207
| ~ spl12_212 ),
inference(forward_subsumption_resolution,[],[f2176,f221]) ).
fof(f2182,plain,
( ~ spl12_207
| ~ spl12_212 ),
inference(avatar_contradiction_clause,[],[f2181]) ).
fof(f2190,plain,
( e20 = e22
| ~ spl12_201
| ~ spl12_211 ),
inference(forward_demodulation,[],[f1470,f1514]) ).
fof(f2192,plain,
( $false
| spl12_22
| ~ spl12_105
| ~ spl12_201
| ~ spl12_211 ),
inference(forward_subsumption_resolution,[],[f2190,f2007]) ).
fof(f2193,plain,
( spl12_22
| ~ spl12_105
| ~ spl12_201
| ~ spl12_211 ),
inference(avatar_contradiction_clause,[],[f2192]) ).
fof(f2196,plain,
( e21 = e22
| ~ spl12_209
| ~ spl12_214 ),
inference(superposition,[],[f1527,f1505]) ).
fof(f2201,plain,
( $false
| ~ spl12_209
| ~ spl12_214 ),
inference(forward_subsumption_resolution,[],[f2196,f221]) ).
fof(f2202,plain,
( ~ spl12_209
| ~ spl12_214 ),
inference(avatar_contradiction_clause,[],[f2201]) ).
fof(f2255,plain,
( e20 = e21
| ~ spl12_221
| ~ spl12_224 ),
inference(forward_demodulation,[],[f1572,f1558]) ).
fof(f2256,plain,
( $false
| ~ spl12_2
| spl12_7
| ~ spl12_221
| ~ spl12_224 ),
inference(forward_subsumption_resolution,[],[f2255,f1955]) ).
fof(f2257,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_221
| ~ spl12_224 ),
inference(avatar_contradiction_clause,[],[f2256]) ).
fof(f2259,plain,
( e21 = e22
| ~ spl12_224
| ~ spl12_227 ),
inference(superposition,[],[f1586,f1572]) ).
fof(f2264,plain,
( $false
| ~ spl12_224
| ~ spl12_227 ),
inference(forward_subsumption_resolution,[],[f2259,f221]) ).
fof(f2265,plain,
( ~ spl12_224
| ~ spl12_227 ),
inference(avatar_contradiction_clause,[],[f2264]) ).
fof(f2286,plain,
( e22 = e23
| ~ spl12_227
| ~ spl12_230 ),
inference(superposition,[],[f1600,f1586]) ).
fof(f2291,plain,
( $false
| ~ spl12_227
| ~ spl12_230 ),
inference(forward_subsumption_resolution,[],[f2286,f219]) ).
fof(f2292,plain,
( ~ spl12_227
| ~ spl12_230 ),
inference(avatar_contradiction_clause,[],[f2291]) ).
fof(f2317,plain,
( e20 = e21
| ~ spl12_233
| ~ spl12_234 ),
inference(forward_demodulation,[],[f1620,f1614]) ).
fof(f2318,plain,
( $false
| ~ spl12_2
| spl12_7
| ~ spl12_233
| ~ spl12_234 ),
inference(forward_subsumption_resolution,[],[f2317,f1955]) ).
fof(f2319,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_233
| ~ spl12_234 ),
inference(avatar_contradiction_clause,[],[f2318]) ).
fof(f2343,plain,
( e20 = e23
| ~ spl12_173
| ~ spl12_194 ),
inference(superposition,[],[f1440,f1350]) ).
fof(f2348,plain,
( $false
| ~ spl12_173
| ~ spl12_194 ),
inference(forward_subsumption_resolution,[],[f2343,f222]) ).
fof(f2349,plain,
( ~ spl12_173
| ~ spl12_194 ),
inference(avatar_contradiction_clause,[],[f2348]) ).
fof(f2378,plain,
( e21 = e23
| ~ spl12_234
| ~ spl12_236 ),
inference(superposition,[],[f1632,f1620]) ).
fof(f2383,plain,
( $false
| ~ spl12_234
| ~ spl12_236 ),
inference(forward_subsumption_resolution,[],[f2378,f220]) ).
fof(f2384,plain,
( ~ spl12_234
| ~ spl12_236 ),
inference(avatar_contradiction_clause,[],[f2383]) ).
fof(f2393,plain,
( e11 = e12
| ~ spl12_246
| ~ spl12_253 ),
inference(superposition,[],[f1722,f1692]) ).
fof(f2397,plain,
( $false
| ~ spl12_246
| ~ spl12_253 ),
inference(forward_subsumption_resolution,[],[f2393,f215]) ).
fof(f2398,plain,
( ~ spl12_246
| ~ spl12_253 ),
inference(avatar_contradiction_clause,[],[f2397]) ).
fof(f2406,plain,
( e10 = e11
| ~ spl12_237
| ~ spl12_244 ),
inference(forward_demodulation,[],[f1684,f1654]) ).
fof(f2408,plain,
( $false
| ~ spl12_237
| ~ spl12_244 ),
inference(forward_subsumption_resolution,[],[f2406,f218]) ).
fof(f2409,plain,
( ~ spl12_237
| ~ spl12_244 ),
inference(avatar_contradiction_clause,[],[f2408]) ).
fof(f2418,plain,
( e10 = e12
| ~ spl12_240
| ~ spl12_254 ),
inference(forward_demodulation,[],[f1666,f1726]) ).
fof(f2419,plain,
( $false
| ~ spl12_240
| ~ spl12_254 ),
inference(forward_subsumption_resolution,[],[f2418,f217]) ).
fof(f2420,plain,
( ~ spl12_240
| ~ spl12_254 ),
inference(avatar_contradiction_clause,[],[f2419]) ).
fof(f2422,plain,
( e10 = e11
| ~ spl12_241
| ~ spl12_248 ),
inference(superposition,[],[f1671,f1701]) ).
fof(f2426,plain,
( $false
| ~ spl12_241
| ~ spl12_248 ),
inference(forward_subsumption_resolution,[],[f2422,f218]) ).
fof(f2427,plain,
( ~ spl12_241
| ~ spl12_248 ),
inference(avatar_contradiction_clause,[],[f2426]) ).
fof(f2440,plain,
( e11 = e12
| ~ spl12_249
| ~ spl12_256 ),
inference(superposition,[],[f1735,f1705]) ).
fof(f2444,plain,
( $false
| ~ spl12_249
| ~ spl12_256 ),
inference(forward_subsumption_resolution,[],[f2440,f215]) ).
fof(f2445,plain,
( ~ spl12_249
| ~ spl12_256 ),
inference(avatar_contradiction_clause,[],[f2444]) ).
fof(f2447,plain,
( e11 = e12
| ~ spl12_250
| ~ spl12_257 ),
inference(superposition,[],[f1739,f1709]) ).
fof(f2451,plain,
( $false
| ~ spl12_250
| ~ spl12_257 ),
inference(forward_subsumption_resolution,[],[f2447,f215]) ).
fof(f2452,plain,
( ~ spl12_250
| ~ spl12_257 ),
inference(avatar_contradiction_clause,[],[f2451]) ).
fof(f2472,plain,
( e12 = e13
| ~ spl12_254
| ~ spl12_261 ),
inference(superposition,[],[f1756,f1726]) ).
fof(f2476,plain,
( $false
| ~ spl12_254
| ~ spl12_261 ),
inference(forward_subsumption_resolution,[],[f2472,f213]) ).
fof(f2477,plain,
( ~ spl12_254
| ~ spl12_261 ),
inference(avatar_contradiction_clause,[],[f2476]) ).
fof(f2505,plain,
( e10 = e11
| ~ spl12_266
| ~ spl12_271 ),
inference(forward_demodulation,[],[f1800,f1778]) ).
fof(f2506,plain,
( $false
| ~ spl12_266
| ~ spl12_271 ),
inference(forward_subsumption_resolution,[],[f2505,f218]) ).
fof(f2507,plain,
( ~ spl12_266
| ~ spl12_271 ),
inference(avatar_contradiction_clause,[],[f2506]) ).
fof(f2547,plain,
( e10 = e13
| ~ spl12_269
| ~ spl12_284 ),
inference(superposition,[],[f1857,f1791]) ).
fof(f2551,plain,
( $false
| ~ spl12_269
| ~ spl12_284 ),
inference(forward_subsumption_resolution,[],[f2547,f216]) ).
fof(f2552,plain,
( ~ spl12_269
| ~ spl12_284 ),
inference(avatar_contradiction_clause,[],[f2551]) ).
fof(f2574,plain,
( e10 = e13
| ~ spl12_237
| ~ spl12_258 ),
inference(superposition,[],[f1744,f1654]) ).
fof(f2578,plain,
( $false
| ~ spl12_237
| ~ spl12_258 ),
inference(forward_subsumption_resolution,[],[f2574,f216]) ).
fof(f2579,plain,
( ~ spl12_237
| ~ spl12_258 ),
inference(avatar_contradiction_clause,[],[f2578]) ).
fof(f2601,plain,
( e10 = e12
| ~ spl12_269
| ~ spl12_279 ),
inference(superposition,[],[f1835,f1791]) ).
fof(f2606,plain,
( $false
| ~ spl12_269
| ~ spl12_279 ),
inference(forward_subsumption_resolution,[],[f2601,f217]) ).
fof(f2607,plain,
( ~ spl12_269
| ~ spl12_279 ),
inference(avatar_contradiction_clause,[],[f2606]) ).
fof(f2613,plain,
( e10 = e13
| ~ spl12_267
| ~ spl12_282 ),
inference(superposition,[],[f1848,f1782]) ).
fof(f2617,plain,
( $false
| ~ spl12_267
| ~ spl12_282 ),
inference(forward_subsumption_resolution,[],[f2613,f216]) ).
fof(f2618,plain,
( ~ spl12_267
| ~ spl12_282 ),
inference(avatar_contradiction_clause,[],[f2617]) ).
fof(f2670,plain,
( e10 = e12
| ~ spl12_286
| ~ spl12_292 ),
inference(superposition,[],[f1894,f1866]) ).
fof(f2674,plain,
( $false
| ~ spl12_286
| ~ spl12_292 ),
inference(forward_subsumption_resolution,[],[f2670,f217]) ).
fof(f2675,plain,
( ~ spl12_286
| ~ spl12_292 ),
inference(avatar_contradiction_clause,[],[f2674]) ).
fof(f2676,plain,
( e10 = e13
| ~ spl12_239
| ~ spl12_260 ),
inference(forward_demodulation,[],[f1662,f1752]) ).
fof(f2679,plain,
( $false
| ~ spl12_239
| ~ spl12_260 ),
inference(forward_subsumption_resolution,[],[f2676,f216]) ).
fof(f2680,plain,
( ~ spl12_239
| ~ spl12_260 ),
inference(avatar_contradiction_clause,[],[f2679]) ).
fof(f2723,plain,
( e12 = e13
| ~ spl12_293
| ~ spl12_296 ),
inference(superposition,[],[f1913,f1899]) ).
fof(f2729,plain,
( $false
| ~ spl12_293
| ~ spl12_296 ),
inference(forward_subsumption_resolution,[],[f2723,f213]) ).
fof(f2730,plain,
( ~ spl12_293
| ~ spl12_296 ),
inference(avatar_contradiction_clause,[],[f2729]) ).
fof(f2731,plain,
( e11 = e13
| ~ spl12_288
| ~ spl12_294 ),
inference(superposition,[],[f1904,f1876]) ).
fof(f2737,plain,
( $false
| ~ spl12_288
| ~ spl12_294 ),
inference(forward_subsumption_resolution,[],[f2731,f214]) ).
fof(f2738,plain,
( ~ spl12_288
| ~ spl12_294 ),
inference(avatar_contradiction_clause,[],[f2737]) ).
fof(f2786,plain,
( e10 = e11
| ~ spl12_297
| ~ spl12_298 ),
inference(forward_demodulation,[],[f1924,f1918]) ).
fof(f2787,plain,
( $false
| ~ spl12_297
| ~ spl12_298 ),
inference(forward_subsumption_resolution,[],[f2786,f218]) ).
fof(f2788,plain,
( ~ spl12_297
| ~ spl12_298 ),
inference(avatar_contradiction_clause,[],[f2787]) ).
fof(f2792,plain,
( e11 = e13
| ~ spl12_250
| ~ spl12_264 ),
inference(superposition,[],[f1769,f1709]) ).
fof(f2798,plain,
( $false
| ~ spl12_250
| ~ spl12_264 ),
inference(forward_subsumption_resolution,[],[f2792,f214]) ).
fof(f2799,plain,
( ~ spl12_250
| ~ spl12_264 ),
inference(avatar_contradiction_clause,[],[f2798]) ).
fof(f2842,plain,
( e11 = e12
| ~ spl12_298
| ~ spl12_299 ),
inference(superposition,[],[f1930,f1924]) ).
fof(f2847,plain,
( $false
| ~ spl12_298
| ~ spl12_299 ),
inference(forward_subsumption_resolution,[],[f2842,f215]) ).
fof(f2848,plain,
( ~ spl12_298
| ~ spl12_299 ),
inference(avatar_contradiction_clause,[],[f2847]) ).
fof(f2898,plain,
( e10 = e11
| ~ spl12_242
| ~ spl12_249 ),
inference(superposition,[],[f1675,f1705]) ).
fof(f2904,plain,
( $false
| ~ spl12_242
| ~ spl12_249 ),
inference(forward_subsumption_resolution,[],[f2898,f218]) ).
fof(f2905,plain,
( ~ spl12_242
| ~ spl12_249 ),
inference(avatar_contradiction_clause,[],[f2904]) ).
fof(f2977,plain,
( e12 = e13
| ~ spl12_291
| ~ spl12_294 ),
inference(superposition,[],[f1904,f1890]) ).
fof(f2983,plain,
( $false
| ~ spl12_291
| ~ spl12_294 ),
inference(forward_subsumption_resolution,[],[f2977,f213]) ).
fof(f2984,plain,
( ~ spl12_291
| ~ spl12_294 ),
inference(avatar_contradiction_clause,[],[f2983]) ).
fof(f3009,plain,
( e11 = e13
| ~ spl12_298
| ~ spl12_300 ),
inference(superposition,[],[f1936,f1924]) ).
fof(f3015,plain,
( $false
| ~ spl12_298
| ~ spl12_300 ),
inference(forward_subsumption_resolution,[],[f3009,f214]) ).
fof(f3016,plain,
( ~ spl12_298
| ~ spl12_300 ),
inference(avatar_contradiction_clause,[],[f3015]) ).
fof(f3137,plain,
( e10 = e13
| ~ spl12_286
| ~ spl12_295 ),
inference(superposition,[],[f1908,f1866]) ).
fof(f3142,plain,
( $false
| ~ spl12_286
| ~ spl12_295 ),
inference(forward_subsumption_resolution,[],[f3137,f216]) ).
fof(f3143,plain,
( ~ spl12_286
| ~ spl12_295 ),
inference(avatar_contradiction_clause,[],[f3142]) ).
fof(f3161,plain,
( e11 != op1(e13,e12)
| ~ spl12_298 ),
inference(forward_demodulation,[],[f117,f1924]) ).
fof(f3168,plain,
( e10 != op1(e13,e10)
| ~ spl12_269 ),
inference(forward_demodulation,[],[f122,f1791]) ).
fof(f3169,plain,
( e13 != op1(e12,e12)
| ~ spl12_295 ),
inference(forward_demodulation,[],[f123,f1908]) ).
fof(f3186,plain,
( op1(e10,e10) != e11
| ~ spl12_245 ),
inference(forward_demodulation,[],[f140,f1688]) ).
fof(f3188,plain,
( e11 != op1(e12,e13)
| ~ spl12_298 ),
inference(forward_demodulation,[],[f141,f1924]) ).
fof(f3201,plain,
( e10 != op1(e10,e12)
| ~ spl12_266 ),
inference(forward_demodulation,[],[f152,f1778]) ).
fof(f3202,plain,
( e10 != op1(e12,e11)
| ~ spl12_269 ),
inference(forward_demodulation,[],[f153,f1791]) ).
fof(f3203,plain,
( e10 != op1(e11,e11)
| ~ spl12_269 ),
inference(forward_demodulation,[],[f154,f1791]) ).
fof(f3204,plain,
( e12 != op1(e11,e11)
| ~ spl12_278 ),
inference(forward_demodulation,[],[f155,f1831]) ).
fof(f3205,plain,
( e10 != op1(e10,e11)
| ~ spl12_269 ),
inference(forward_demodulation,[],[f156,f1791]) ).
fof(f3207,plain,
( e13 != op1(e10,e11)
| ~ spl12_280 ),
inference(forward_demodulation,[],[f158,f1840]) ).
fof(f3211,plain,
( op1(e10,e10) != e13
| ~ spl12_264 ),
inference(forward_demodulation,[],[f162,f1769]) ).
fof(f3212,plain,
( e10 != op1(e10,e10)
| ~ spl12_242 ),
inference(forward_demodulation,[],[f163,f1675]) ).
fof(f3215,plain,
( e21 != op2(e23,e22)
| ~ spl12_234 ),
inference(forward_demodulation,[],[f165,f1620]) ).
fof(f3217,plain,
( e21 != op2(e23,e21)
| ~ spl12_234 ),
inference(forward_demodulation,[],[f166,f1620]) ).
fof(f3220,plain,
( e21 != op2(e23,e20)
| ~ spl12_234 ),
inference(forward_demodulation,[],[f168,f1620]) ).
fof(f3223,plain,
( e23 != op2(e22,e22)
| ~ spl12_231 ),
inference(forward_demodulation,[],[f171,f1604]) ).
fof(f3227,plain,
( e21 != op2(e22,e21)
| ~ spl12_224 ),
inference(forward_demodulation,[],[f173,f1572]) ).
fof(f3230,plain,
( e21 != op2(e22,e20)
| ~ spl12_224 ),
inference(forward_demodulation,[],[f175,f1572]) ).
fof(f3245,plain,
( op2(e20,e20) != e21
| ~ spl12_181 ),
inference(forward_demodulation,[],[f188,f1384]) ).
fof(f3247,plain,
( e21 != op2(e22,e23)
| ~ spl12_234 ),
inference(forward_demodulation,[],[f189,f1620]) ).
fof(f3248,plain,
( e21 != op2(e21,e23)
| ~ spl12_234 ),
inference(forward_demodulation,[],[f190,f1620]) ).
fof(f3253,plain,
( e21 != op2(e20,e23)
| ~ spl12_234 ),
inference(forward_demodulation,[],[f192,f1620]) ).
fof(f3256,plain,
( e22 != op2(e20,e23)
| ~ spl12_213 ),
inference(forward_demodulation,[],[f194,f1522]) ).
fof(f3257,plain,
( e23 != op2(e22,e22)
| ~ spl12_232 ),
inference(forward_demodulation,[],[f195,f1609]) ).
fof(f3268,plain,
( e23 != op2(e20,e21)
| ~ spl12_216 ),
inference(forward_demodulation,[],[f206,f1536]) ).
fof(f3278,plain,
( e10 = op1(e13,e11)
| ~ spl12_298 ),
inference(forward_demodulation,[],[f291,f1924]) ).
fof(f3279,plain,
( e20 = op2(e23,e21)
| ~ spl12_234 ),
inference(forward_demodulation,[],[f294,f1620]) ).
fof(f3280,plain,
( e20 = e22
| ~ spl12_215
| ~ spl12_234 ),
inference(forward_demodulation,[],[f3279,f1531]) ).
fof(f3281,plain,
( $false
| spl12_22
| ~ spl12_105
| ~ spl12_215
| ~ spl12_234 ),
inference(forward_subsumption_resolution,[],[f3280,f2007]) ).
fof(f3282,plain,
( spl12_22
| ~ spl12_105
| ~ spl12_215
| ~ spl12_234 ),
inference(avatar_contradiction_clause,[],[f3281]) ).
fof(f3285,plain,
( ~ spl12_210
| ~ spl12_234 ),
inference(avatar_split_clause,[],[f3217,f1618,f1507]) ).
fof(f3286,plain,
( e20 != op2(e23,e21)
| ~ spl12_179 ),
inference(forward_demodulation,[],[f170,f1375]) ).
fof(f3289,plain,
( spl12_205
| ~ spl12_234 ),
inference(avatar_split_clause,[],[f3279,f1618,f1485]) ).
fof(f3291,plain,
( e23 != op2(e20,e21)
| ~ spl12_194 ),
inference(forward_demodulation,[],[f188,f1440]) ).
fof(f3296,plain,
( ~ spl12_205
| ~ spl12_179 ),
inference(avatar_split_clause,[],[f3286,f1373,f1485]) ).
fof(f3302,plain,
( ~ spl12_209
| ~ spl12_224 ),
inference(avatar_split_clause,[],[f3227,f1570,f1503]) ).
fof(f3308,plain,
( e23 != op2(e23,e20)
| ~ spl12_194 ),
inference(forward_demodulation,[],[f210,f1440]) ).
fof(f3312,plain,
( ~ spl12_200
| ~ spl12_194 ),
inference(avatar_split_clause,[],[f3308,f1438,f1463]) ).
fof(f3342,plain,
( e20 != op2(e20,e21)
| ~ spl12_205 ),
inference(forward_demodulation,[],[f204,f1487]) ).
fof(f3353,plain,
( op2(e21,e23) = h2(e10)
| ~ spl12_216 ),
inference(forward_demodulation,[],[f301,f1536]) ).
fof(f3357,plain,
( op2(e22,e21) = h3(e10)
| ~ spl12_224 ),
inference(forward_demodulation,[],[f305,f1572]) ).
fof(f3358,plain,
( e22 = h3(e10)
| ~ spl12_214
| ~ spl12_224 ),
inference(forward_demodulation,[],[f3357,f1527]) ).
fof(f3359,plain,
( spl12_109
| ~ spl12_214
| ~ spl12_224 ),
inference(avatar_split_clause,[],[f3358,f1570,f1525,f1011]) ).
fof(f3374,plain,
( e12 = op1(op1(e13,e11),e13)
| ~ spl12_298 ),
inference(forward_demodulation,[],[f289,f1924]) ).
fof(f3375,plain,
( e12 = op1(e10,e13)
| ~ spl12_269
| ~ spl12_298 ),
inference(forward_demodulation,[],[f3374,f1791]) ).
fof(f3380,plain,
( e13 != op1(e12,e12)
| ~ spl12_260 ),
inference(forward_demodulation,[],[f151,f1752]) ).
fof(f3384,plain,
( spl12_254
| ~ spl12_269
| ~ spl12_298 ),
inference(avatar_split_clause,[],[f3375,f1922,f1789,f1724]) ).
fof(f3389,plain,
( e12 != op1(e10,e13)
| ~ spl12_251 ),
inference(forward_demodulation,[],[f138,f1714]) ).
fof(f3395,plain,
( ~ spl12_254
| ~ spl12_251 ),
inference(avatar_split_clause,[],[f3389,f1712,f1724]) ).
fof(f3396,plain,
( ~ spl12_244
| ~ spl12_245 ),
inference(avatar_split_clause,[],[f3186,f1686,f1682]) ).
fof(f3432,plain,
( e10 != op1(e11,e10)
| ~ spl12_267 ),
inference(forward_demodulation,[],[f132,f1782]) ).
fof(f3441,plain,
( e22 = op2(op2(e23,e21),e23)
| ~ spl12_234 ),
inference(forward_demodulation,[],[f292,f1620]) ).
fof(f3442,plain,
( e22 = op2(e20,e23)
| ~ spl12_205
| ~ spl12_234 ),
inference(forward_demodulation,[],[f3441,f1487]) ).
fof(f3451,plain,
( ~ spl12_190
| ~ spl12_213 ),
inference(avatar_split_clause,[],[f3256,f1520,f1420]) ).
fof(f3452,plain,
( spl12_190
| ~ spl12_205
| ~ spl12_234 ),
inference(avatar_split_clause,[],[f3442,f1618,f1485,f1420]) ).
fof(f3453,plain,
( e21 != op2(e20,e22)
| ~ spl12_181 ),
inference(forward_demodulation,[],[f185,f1384]) ).
fof(f3457,plain,
( ~ spl12_183
| ~ spl12_234 ),
inference(avatar_split_clause,[],[f3253,f1618,f1390]) ).
fof(f3466,plain,
( ~ spl12_208
| ~ spl12_234 ),
inference(avatar_split_clause,[],[f3248,f1618,f1498]) ).
fof(f3469,plain,
( e21 != op2(e21,e22)
| ~ spl12_184 ),
inference(forward_demodulation,[],[f181,f1397]) ).
fof(f3508,plain,
( e23 = op2(e22,e22)
| ~ spl12_138
| ~ spl12_190 ),
inference(forward_demodulation,[],[f1162,f1422]) ).
fof(f3512,plain,
( op2(e20,e20) = e23
| ~ spl12_143
| ~ spl12_203 ),
inference(forward_demodulation,[],[f1186,f1478]) ).
fof(f3513,plain,
( e22 = op2(e22,e22)
| ~ spl12_144
| ~ spl12_212 ),
inference(forward_demodulation,[],[f1191,f1518]) ).
fof(f3515,plain,
( e20 = op2(e21,e21)
| ~ spl12_146
| ~ spl12_184 ),
inference(forward_demodulation,[],[f1201,f1397]) ).
fof(f3516,plain,
( $false
| ~ spl12_144
| ~ spl12_212
| spl12_227 ),
inference(forward_subsumption_resolution,[],[f3513,f1585]) ).
fof(f3517,plain,
( ~ spl12_144
| ~ spl12_212
| spl12_227 ),
inference(avatar_contradiction_clause,[],[f3516]) ).
fof(f3518,plain,
( $false
| ~ spl12_146
| ~ spl12_184
| spl12_201 ),
inference(forward_subsumption_resolution,[],[f3515,f1469]) ).
fof(f3519,plain,
( ~ spl12_146
| ~ spl12_184
| spl12_201 ),
inference(avatar_contradiction_clause,[],[f3518]) ).
fof(f3522,plain,
( e23 = op2(e23,e23)
| ~ spl12_147
| ~ spl12_231 ),
inference(forward_demodulation,[],[f1206,f1604]) ).
fof(f3523,plain,
( e22 = op2(e21,e21)
| ~ spl12_149
| ~ spl12_224 ),
inference(forward_demodulation,[],[f1215,f1572]) ).
fof(f3524,plain,
( e21 = op2(e22,e22)
| ~ spl12_150
| ~ spl12_214 ),
inference(forward_demodulation,[],[f1220,f1527]) ).
fof(f3525,plain,
( e20 = op2(e20,e20)
| ~ spl12_151
| ~ spl12_178 ),
inference(forward_demodulation,[],[f1225,f1371]) ).
fof(f3526,plain,
( $false
| ~ spl12_147
| ~ spl12_231
| spl12_236 ),
inference(forward_subsumption_resolution,[],[f3522,f1631]) ).
fof(f3527,plain,
( ~ spl12_147
| ~ spl12_231
| spl12_236 ),
inference(avatar_contradiction_clause,[],[f3526]) ).
fof(f3530,plain,
( e20 = e23
| ~ spl12_151
| ~ spl12_178
| ~ spl12_194 ),
inference(forward_demodulation,[],[f3525,f1440]) ).
fof(f3531,plain,
( $false
| ~ spl12_151
| ~ spl12_178
| ~ spl12_194 ),
inference(forward_subsumption_resolution,[],[f3530,f222]) ).
fof(f3532,plain,
( ~ spl12_151
| ~ spl12_178
| ~ spl12_194 ),
inference(avatar_contradiction_clause,[],[f3531]) ).
fof(f3534,plain,
( e20 = op2(e22,e22)
| ~ spl12_148
| ~ spl12_193 ),
inference(forward_demodulation,[],[f1210,f1435]) ).
fof(f3537,plain,
( op2(e20,e20) = e21
| ~ spl12_152
| ~ spl12_205 ),
inference(forward_demodulation,[],[f1230,f1487]) ).
fof(f3539,plain,
( e23 = op2(e21,e21)
| ~ spl12_154
| ~ spl12_234 ),
inference(forward_demodulation,[],[f1246,f1620]) ).
fof(f3540,plain,
( $false
| ~ spl12_148
| ~ spl12_193
| spl12_221 ),
inference(forward_subsumption_resolution,[],[f3534,f1557]) ).
fof(f3541,plain,
( ~ spl12_148
| ~ spl12_193
| spl12_221 ),
inference(avatar_contradiction_clause,[],[f3540]) ).
fof(f3543,plain,
( e21 = e23
| ~ spl12_152
| ~ spl12_194
| ~ spl12_205 ),
inference(forward_demodulation,[],[f3537,f1440]) ).
fof(f3546,plain,
( $false
| ~ spl12_152
| ~ spl12_194
| ~ spl12_205 ),
inference(forward_subsumption_resolution,[],[f3543,f220]) ).
fof(f3547,plain,
( ~ spl12_152
| ~ spl12_194
| ~ spl12_205 ),
inference(avatar_contradiction_clause,[],[f3546]) ).
fof(f3550,plain,
( spl12_211
| ~ spl12_149
| ~ spl12_224 ),
inference(avatar_split_clause,[],[f3523,f1570,f1213,f1512]) ).
fof(f3555,plain,
( e22 != op2(e22,e23)
| ~ spl12_190 ),
inference(forward_demodulation,[],[f193,f1422]) ).
fof(f3556,plain,
( ~ spl12_225
| ~ spl12_234 ),
inference(avatar_split_clause,[],[f3247,f1618,f1574]) ).
fof(f3560,plain,
( e21 != op2(e21,e21)
| ~ spl12_181 ),
inference(forward_demodulation,[],[f206,f1384]) ).
fof(f3562,plain,
( e22 != op2(e21,e21)
| ~ spl12_214 ),
inference(forward_demodulation,[],[f203,f1527]) ).
fof(f3566,plain,
( spl12_216
| ~ spl12_154
| ~ spl12_234 ),
inference(avatar_split_clause,[],[f3539,f1618,f1244,f1534]) ).
fof(f3571,plain,
( ~ spl12_180
| ~ spl12_181 ),
inference(avatar_split_clause,[],[f3245,f1382,f1378]) ).
fof(f3576,plain,
( e20 != op2(e20,e20)
| ~ spl12_175 ),
inference(forward_demodulation,[],[f187,f1358]) ).
fof(f3577,plain,
( op2(e20,e20) != e22
| ~ spl12_190 ),
inference(forward_demodulation,[],[f186,f1422]) ).
fof(f3578,plain,
( spl12_194
| ~ spl12_143
| ~ spl12_203 ),
inference(avatar_split_clause,[],[f3512,f1476,f1184,f1438]) ).
fof(f3580,plain,
( ~ spl12_211
| ~ spl12_214 ),
inference(avatar_split_clause,[],[f3562,f1525,f1512]) ).
fof(f3586,plain,
( ~ spl12_173
| ~ spl12_175 ),
inference(avatar_split_clause,[],[f3576,f1356,f1348]) ).
fof(f3587,plain,
( ~ spl12_187
| ~ spl12_190 ),
inference(avatar_split_clause,[],[f3577,f1420,f1408]) ).
fof(f3595,plain,
( ~ spl12_226
| ~ spl12_234 ),
inference(avatar_split_clause,[],[f3215,f1618,f1579]) ).
fof(f3596,plain,
( e20 != op2(e23,e22)
| ~ spl12_205 ),
inference(forward_demodulation,[],[f167,f1487]) ).
fof(f3606,plain,
( ~ spl12_223
| ~ spl12_205 ),
inference(avatar_split_clause,[],[f3596,f1485,f1565]) ).
fof(f3687,plain,
( e22 = h2(e11)
| ~ spl12_211 ),
inference(forward_demodulation,[],[f300,f1514]) ).
fof(f3688,plain,
( spl12_84
| ~ spl12_211 ),
inference(avatar_split_clause,[],[f3687,f1512,f894]) ).
fof(f3700,plain,
( e22 != op2(e23,e20)
| ~ spl12_229 ),
inference(forward_demodulation,[],[f169,f1595]) ).
fof(f3720,plain,
( e21 = op2(e21,e21)
| ~ spl12_140
| ~ spl12_181 ),
inference(forward_demodulation,[],[f1172,f1384]) ).
fof(f3721,plain,
( $false
| ~ spl12_140
| ~ spl12_181
| spl12_206 ),
inference(forward_subsumption_resolution,[],[f3720,f1491]) ).
fof(f3722,plain,
( ~ spl12_140
| ~ spl12_181
| spl12_206 ),
inference(avatar_contradiction_clause,[],[f3721]) ).
fof(f3727,plain,
( e21 = op2(e22,e22)
| ~ spl12_145
| ~ spl12_211 ),
inference(forward_demodulation,[],[f1196,f1514]) ).
fof(f3735,plain,
( e23 = op2(e23,e23)
| ~ spl12_143
| ~ spl12_218 ),
inference(forward_demodulation,[],[f1186,f1544]) ).
fof(f3736,plain,
( op2(e20,e20) = e22
| ~ spl12_144
| ~ spl12_202 ),
inference(forward_demodulation,[],[f1191,f1474]) ).
fof(f3743,plain,
( ~ spl12_206
| ~ spl12_181 ),
inference(avatar_split_clause,[],[f3560,f1382,f1490]) ).
fof(f3746,plain,
( ~ spl12_185
| ~ spl12_224 ),
inference(avatar_split_clause,[],[f3230,f1570,f1399]) ).
fof(f3747,plain,
( e20 != op2(e21,e20)
| ~ spl12_173 ),
inference(forward_demodulation,[],[f212,f1350]) ).
fof(f3757,plain,
( $false
| ~ spl12_143
| ~ spl12_218
| spl12_236 ),
inference(forward_subsumption_resolution,[],[f3735,f1631]) ).
fof(f3758,plain,
( ~ spl12_143
| ~ spl12_218
| spl12_236 ),
inference(avatar_contradiction_clause,[],[f3757]) ).
fof(f3759,plain,
( $false
| ~ spl12_144
| spl12_187
| ~ spl12_202 ),
inference(forward_subsumption_resolution,[],[f3736,f1409]) ).
fof(f3760,plain,
( ~ spl12_144
| spl12_187
| ~ spl12_202 ),
inference(avatar_contradiction_clause,[],[f3759]) ).
fof(f3772,plain,
( spl12_180
| ~ spl12_152
| ~ spl12_205 ),
inference(avatar_split_clause,[],[f3537,f1485,f1228,f1378]) ).
fof(f3784,plain,
( e22 != op2(e20,e21)
| ~ spl12_190 ),
inference(forward_demodulation,[],[f184,f1422]) ).
fof(f3801,plain,
( ~ spl12_188
| ~ spl12_190 ),
inference(avatar_split_clause,[],[f3784,f1420,f1412]) ).
fof(f3812,plain,
( spl12_230
| ~ spl12_138
| ~ spl12_190 ),
inference(avatar_split_clause,[],[f3508,f1420,f1160,f1598]) ).
fof(f3815,plain,
( ~ spl12_230
| ~ spl12_231 ),
inference(avatar_split_clause,[],[f3223,f1602,f1598]) ).
fof(f3818,plain,
( spl12_224
| ~ spl12_150
| ~ spl12_214 ),
inference(avatar_split_clause,[],[f3524,f1525,f1218,f1570]) ).
fof(f3821,plain,
( ~ spl12_195
| ~ spl12_216 ),
inference(avatar_split_clause,[],[f3268,f1534,f1442]) ).
fof(f3837,plain,
( ~ spl12_228
| ~ spl12_190 ),
inference(avatar_split_clause,[],[f3555,f1420,f1588]) ).
fof(f3840,plain,
( ~ spl12_174
| ~ spl12_205 ),
inference(avatar_split_clause,[],[f3342,f1485,f1352]) ).
fof(f3847,plain,
( op2(e20,e20) != e21
| spl12_152
| ~ spl12_205 ),
inference(forward_demodulation,[],[f1229,f1487]) ).
fof(f3848,plain,
( ~ spl12_177
| ~ spl12_173 ),
inference(avatar_split_clause,[],[f3747,f1348,f1365]) ).
fof(f3853,plain,
( ~ spl12_180
| spl12_152
| ~ spl12_205 ),
inference(avatar_split_clause,[],[f3847,f1485,f1228,f1378]) ).
fof(f3921,plain,
( e20 != op2(e22,e22)
| ~ spl12_222 ),
inference(forward_demodulation,[],[f171,f1562]) ).
fof(f3934,plain,
( op2(e20,e20) != e21
| ~ spl12_182 ),
inference(forward_demodulation,[],[f187,f1388]) ).
fof(f3948,plain,
( op2(e22,e23) = h3(e10)
| ~ spl12_230 ),
inference(forward_demodulation,[],[f305,f1600]) ).
fof(f3949,plain,
( e22 = op2(e22,e23)
| ~ spl12_109
| ~ spl12_230 ),
inference(forward_demodulation,[],[f3948,f1012]) ).
fof(f3950,plain,
( $false
| ~ spl12_109
| spl12_228
| ~ spl12_230 ),
inference(forward_subsumption_resolution,[],[f3949,f1589]) ).
fof(f3951,plain,
( ~ spl12_109
| spl12_228
| ~ spl12_230 ),
inference(avatar_contradiction_clause,[],[f3950]) ).
fof(f3970,plain,
( e22 = op2(e21,e21)
| ~ spl12_139
| ~ spl12_182 ),
inference(forward_demodulation,[],[f1167,f1388]) ).
fof(f3971,plain,
( $false
| ~ spl12_139
| ~ spl12_182
| spl12_211 ),
inference(forward_subsumption_resolution,[],[f3970,f1513]) ).
fof(f3972,plain,
( ~ spl12_139
| ~ spl12_182
| spl12_211 ),
inference(avatar_contradiction_clause,[],[f3971]) ).
fof(f3981,plain,
( e21 != op2(e21,e22)
| ~ spl12_206 ),
inference(forward_demodulation,[],[f179,f1492]) ).
fof(f3994,plain,
( ~ spl12_207
| ~ spl12_206 ),
inference(avatar_split_clause,[],[f3981,f1490,f1494]) ).
fof(f4008,plain,
( ~ spl12_182
| ~ spl12_181 ),
inference(avatar_split_clause,[],[f3453,f1382,f1386]) ).
fof(f4010,plain,
( ~ spl12_195
| ~ spl12_194 ),
inference(avatar_split_clause,[],[f3291,f1438,f1442]) ).
fof(f4012,plain,
( e21 = op2(e21,e23)
| ~ spl12_20
| ~ spl12_216 ),
inference(forward_demodulation,[],[f3353,f604]) ).
fof(f4013,plain,
( ~ spl12_230
| ~ spl12_232 ),
inference(avatar_split_clause,[],[f3257,f1607,f1598]) ).
fof(f4025,plain,
( e22 != op2(e23,e20)
| ~ spl12_191 ),
inference(forward_demodulation,[],[f208,f1427]) ).
fof(f4026,plain,
( ~ spl12_186
| ~ spl12_234 ),
inference(avatar_split_clause,[],[f3220,f1618,f1403]) ).
fof(f4035,plain,
( $false
| ~ spl12_20
| spl12_208
| ~ spl12_216 ),
inference(forward_subsumption_resolution,[],[f4012,f1499]) ).
fof(f4036,plain,
( ~ spl12_20
| spl12_208
| ~ spl12_216 ),
inference(avatar_contradiction_clause,[],[f4035]) ).
fof(f4042,plain,
( ~ spl12_193
| ~ spl12_191 ),
inference(avatar_split_clause,[],[f4025,f1425,f1433]) ).
fof(f4051,plain,
( $false
| ~ spl12_145
| ~ spl12_211
| spl12_224 ),
inference(forward_subsumption_resolution,[],[f3727,f1571]) ).
fof(f4052,plain,
( ~ spl12_145
| ~ spl12_211
| spl12_224 ),
inference(avatar_contradiction_clause,[],[f4051]) ).
fof(f4054,plain,
( e21 != op2(e22,e21)
| ~ spl12_185 ),
inference(forward_demodulation,[],[f176,f1401]) ).
fof(f4057,plain,
( ~ spl12_209
| ~ spl12_185 ),
inference(avatar_split_clause,[],[f4054,f1399,f1503]) ).
fof(f4059,plain,
( e20 = op2(e21,e21)
| ~ spl12_151
| ~ spl12_185 ),
inference(forward_demodulation,[],[f1225,f1401]) ).
fof(f4061,plain,
( ~ spl12_221
| ~ spl12_222 ),
inference(avatar_split_clause,[],[f3921,f1560,f1556]) ).
fof(f4062,plain,
( $false
| ~ spl12_151
| ~ spl12_185
| spl12_201 ),
inference(forward_subsumption_resolution,[],[f4059,f1469]) ).
fof(f4063,plain,
( ~ spl12_151
| ~ spl12_185
| spl12_201 ),
inference(avatar_contradiction_clause,[],[f4062]) ).
fof(f4081,plain,
( ~ spl12_193
| ~ spl12_229 ),
inference(avatar_split_clause,[],[f3700,f1593,f1433]) ).
fof(f4233,plain,
( op2(e21,e22) = h2(e10)
| ~ spl12_211 ),
inference(forward_demodulation,[],[f301,f1514]) ).
fof(f4234,plain,
( e21 = h2(e10)
| ~ spl12_207
| ~ spl12_211 ),
inference(forward_demodulation,[],[f4233,f1496]) ).
fof(f4238,plain,
( spl12_20
| ~ spl12_207
| ~ spl12_211 ),
inference(avatar_split_clause,[],[f4234,f1512,f1494,f603]) ).
fof(f4243,plain,
( op2(e20,e20) = e22
| ~ spl12_139
| ~ spl12_175 ),
inference(forward_demodulation,[],[f1167,f1358]) ).
fof(f4244,plain,
( $false
| ~ spl12_139
| ~ spl12_175
| spl12_187 ),
inference(forward_subsumption_resolution,[],[f4243,f1409]) ).
fof(f4245,plain,
( ~ spl12_139
| ~ spl12_175
| spl12_187 ),
inference(avatar_contradiction_clause,[],[f4244]) ).
fof(f4264,plain,
( ~ spl12_180
| ~ spl12_182 ),
inference(avatar_split_clause,[],[f3934,f1386,f1378]) ).
fof(f4265,plain,
( ~ spl12_207
| ~ spl12_184 ),
inference(avatar_split_clause,[],[f3469,f1395,f1494]) ).
fof(f4327,plain,
( e20 = h2(e10)
| ~ spl12_202
| ~ spl12_211 ),
inference(forward_demodulation,[],[f4233,f1474]) ).
fof(f4331,plain,
( spl12_15
| ~ spl12_202
| ~ spl12_211 ),
inference(avatar_split_clause,[],[f4327,f1512,f1472,f579]) ).
fof(f4354,plain,
( e21 = op2(e21,e21)
| ~ spl12_150
| ~ spl12_209 ),
inference(forward_demodulation,[],[f1220,f1505]) ).
fof(f4355,plain,
( $false
| ~ spl12_150
| spl12_206
| ~ spl12_209 ),
inference(forward_subsumption_resolution,[],[f4354,f1491]) ).
fof(f4356,plain,
( ~ spl12_150
| spl12_206
| ~ spl12_209 ),
inference(avatar_contradiction_clause,[],[f4355]) ).
fof(f4358,plain,
( e20 = op2(e22,e22)
| ~ spl12_151
| ~ spl12_192 ),
inference(forward_demodulation,[],[f1225,f1431]) ).
fof(f4359,plain,
( $false
| ~ spl12_151
| ~ spl12_192
| spl12_221 ),
inference(forward_subsumption_resolution,[],[f4358,f1557]) ).
fof(f4360,plain,
( ~ spl12_151
| ~ spl12_192
| spl12_221 ),
inference(avatar_contradiction_clause,[],[f4359]) ).
fof(f4363,plain,
( e13 = op1(e12,e12)
| ~ spl12_156
| ~ spl12_254 ),
inference(forward_demodulation,[],[f1258,f1726]) ).
fof(f4367,plain,
( e13 = op1(e13,e13)
| ~ spl12_165
| ~ spl12_295 ),
inference(forward_demodulation,[],[f1302,f1908]) ).
fof(f4368,plain,
( op1(e10,e10) = e12
| ~ spl12_167
| ~ spl12_285 ),
inference(forward_demodulation,[],[f1311,f1862]) ).
fof(f4370,plain,
( e10 = op1(e11,e11)
| ~ spl12_169
| ~ spl12_249 ),
inference(forward_demodulation,[],[f1321,f1705]) ).
fof(f4371,plain,
( $false
| ~ spl12_165
| ~ spl12_295
| spl12_300 ),
inference(forward_subsumption_resolution,[],[f4367,f1935]) ).
fof(f4372,plain,
( ~ spl12_165
| ~ spl12_295
| spl12_300 ),
inference(avatar_contradiction_clause,[],[f4371]) ).
fof(f4373,plain,
( $false
| ~ spl12_167
| spl12_251
| ~ spl12_285 ),
inference(forward_subsumption_resolution,[],[f4368,f1713]) ).
fof(f4374,plain,
( ~ spl12_167
| spl12_251
| ~ spl12_285 ),
inference(avatar_contradiction_clause,[],[f4373]) ).
fof(f4376,plain,
( $false
| ~ spl12_169
| ~ spl12_249
| spl12_265 ),
inference(forward_subsumption_resolution,[],[f4370,f1773]) ).
fof(f4377,plain,
( ~ spl12_169
| ~ spl12_249
| spl12_265 ),
inference(avatar_contradiction_clause,[],[f4376]) ).
fof(f4380,plain,
( op1(e10,e10) = e13
| ~ spl12_161
| ~ spl12_267 ),
inference(forward_demodulation,[],[f1282,f1782]) ).
fof(f4396,plain,
( op1(e10,e10) = e11
| ~ spl12_170
| ~ spl12_269 ),
inference(forward_demodulation,[],[f1326,f1791]) ).
fof(f4398,plain,
( e13 = op1(e11,e11)
| ~ spl12_172
| ~ spl12_298 ),
inference(forward_demodulation,[],[f1342,f1924]) ).
fof(f4401,plain,
( e10 = e11
| ~ spl12_170
| ~ spl12_237
| ~ spl12_269 ),
inference(forward_demodulation,[],[f4396,f1654]) ).
fof(f4404,plain,
( $false
| ~ spl12_170
| ~ spl12_237
| ~ spl12_269 ),
inference(forward_subsumption_resolution,[],[f4401,f218]) ).
fof(f4405,plain,
( ~ spl12_170
| ~ spl12_237
| ~ spl12_269 ),
inference(avatar_contradiction_clause,[],[f4404]) ).
fof(f4407,plain,
( spl12_294
| ~ spl12_156
| ~ spl12_254 ),
inference(avatar_split_clause,[],[f4363,f1724,f1256,f1902]) ).
fof(f4411,plain,
( ~ spl12_294
| ~ spl12_295 ),
inference(avatar_split_clause,[],[f3169,f1906,f1902]) ).
fof(f4412,plain,
( ~ spl12_294
| ~ spl12_260 ),
inference(avatar_split_clause,[],[f3380,f1750,f1902]) ).
fof(f4418,plain,
( ~ spl12_289
| ~ spl12_298 ),
inference(avatar_split_clause,[],[f3188,f1922,f1878]) ).
fof(f4420,plain,
( ~ spl12_290
| ~ spl12_298 ),
inference(avatar_split_clause,[],[f3161,f1922,f1883]) ).
fof(f4422,plain,
( spl12_280
| ~ spl12_172
| ~ spl12_298 ),
inference(avatar_split_clause,[],[f4398,f1922,f1340,f1838]) ).
fof(f4424,plain,
( ~ spl12_265
| ~ spl12_269 ),
inference(avatar_split_clause,[],[f3203,f1789,f1772]) ).
fof(f4429,plain,
( e10 != op1(e11,e10)
| ~ spl12_237 ),
inference(forward_demodulation,[],[f164,f1654]) ).
fof(f4432,plain,
( e12 != op1(e10,e11)
| ~ spl12_254 ),
inference(forward_demodulation,[],[f136,f1726]) ).
fof(f4447,plain,
( ~ spl12_252
| ~ spl12_254 ),
inference(avatar_split_clause,[],[f4432,f1724,f1716]) ).
fof(f4512,plain,
( e10 = e12
| ~ spl12_266
| ~ spl12_276 ),
inference(superposition,[],[f1822,f1778]) ).
fof(f4517,plain,
( $false
| ~ spl12_266
| ~ spl12_276 ),
inference(forward_subsumption_resolution,[],[f4512,f217]) ).
fof(f4518,plain,
( ~ spl12_266
| ~ spl12_276 ),
inference(avatar_contradiction_clause,[],[f4517]) ).
fof(f4548,plain,
( e10 != op1(e11,e13)
| ~ spl12_286 ),
inference(forward_demodulation,[],[f143,f1866]) ).
fof(f4561,plain,
( e12 = op1(e11,e11)
| ~ spl12_157
| ~ spl12_246 ),
inference(forward_demodulation,[],[f1263,f1692]) ).
fof(f4564,plain,
( e13 = op1(e13,e13)
| ~ spl12_161
| ~ spl12_282 ),
inference(forward_demodulation,[],[f1282,f1848]) ).
fof(f4565,plain,
( $false
| ~ spl12_161
| ~ spl12_282
| spl12_300 ),
inference(forward_subsumption_resolution,[],[f4564,f1935]) ).
fof(f4566,plain,
( ~ spl12_161
| ~ spl12_282
| spl12_300 ),
inference(avatar_contradiction_clause,[],[f4565]) ).
fof(f4568,plain,
( op1(e10,e10) = e13
| ~ spl12_165
| ~ spl12_286 ),
inference(forward_demodulation,[],[f1302,f1866]) ).
fof(f4572,plain,
( $false
| ~ spl12_165
| spl12_258
| ~ spl12_286 ),
inference(forward_subsumption_resolution,[],[f4568,f1743]) ).
fof(f4573,plain,
( ~ spl12_165
| spl12_258
| ~ spl12_286 ),
inference(avatar_contradiction_clause,[],[f4572]) ).
fof(f4588,plain,
( spl12_258
| ~ spl12_161
| ~ spl12_267 ),
inference(avatar_split_clause,[],[f4380,f1780,f1280,f1742]) ).
fof(f4590,plain,
( ~ spl12_237
| ~ spl12_242 ),
inference(avatar_split_clause,[],[f3212,f1673,f1652]) ).
fof(f4600,plain,
( ~ spl12_275
| ~ spl12_278 ),
inference(avatar_split_clause,[],[f3204,f1829,f1816]) ).
fof(f4603,plain,
( ~ spl12_259
| ~ spl12_280 ),
inference(avatar_split_clause,[],[f3207,f1838,f1746]) ).
fof(f4613,plain,
( spl12_275
| ~ spl12_157
| ~ spl12_246 ),
inference(avatar_split_clause,[],[f4561,f1690,f1261,f1816]) ).
fof(f4753,plain,
( op1(e10,e10) = e12
| ~ spl12_157
| ~ spl12_239 ),
inference(forward_demodulation,[],[f1263,f1662]) ).
fof(f4754,plain,
( $false
| ~ spl12_157
| ~ spl12_239
| spl12_251 ),
inference(forward_subsumption_resolution,[],[f4753,f1713]) ).
fof(f4755,plain,
( ~ spl12_157
| ~ spl12_239
| spl12_251 ),
inference(avatar_contradiction_clause,[],[f4754]) ).
fof(f4771,plain,
( op1(e10,e10) = e11
| ~ spl12_170
| ~ spl12_269 ),
inference(forward_demodulation,[],[f1326,f1791]) ).
fof(f4777,plain,
( $false
| ~ spl12_170
| spl12_244
| ~ spl12_269 ),
inference(forward_subsumption_resolution,[],[f4771,f1683]) ).
fof(f4778,plain,
( ~ spl12_170
| spl12_244
| ~ spl12_269 ),
inference(avatar_contradiction_clause,[],[f4777]) ).
fof(f4794,plain,
( spl12_269
| ~ spl12_298 ),
inference(avatar_split_clause,[],[f3278,f1922,f1789]) ).
fof(f4798,plain,
( e13 != op1(e10,e11)
| ~ spl12_258 ),
inference(forward_demodulation,[],[f140,f1744]) ).
fof(f4823,plain,
( ~ spl12_243
| ~ spl12_269 ),
inference(avatar_split_clause,[],[f3168,f1789,f1677]) ).
fof(f4824,plain,
( ~ spl12_268
| ~ spl12_269 ),
inference(avatar_split_clause,[],[f3202,f1789,f1785]) ).
fof(f4825,plain,
( ~ spl12_238
| ~ spl12_269 ),
inference(avatar_split_clause,[],[f3205,f1789,f1656]) ).
fof(f4829,plain,
( ~ spl12_259
| ~ spl12_258 ),
inference(avatar_split_clause,[],[f4798,f1742,f1746]) ).
fof(f4830,plain,
( ~ spl12_241
| ~ spl12_267 ),
inference(avatar_split_clause,[],[f3432,f1780,f1669]) ).
fof(f4849,plain,
( ~ spl12_241
| ~ spl12_237 ),
inference(avatar_split_clause,[],[f4429,f1652,f1669]) ).
fof(f4855,plain,
( ~ spl12_258
| ~ spl12_264 ),
inference(avatar_split_clause,[],[f3211,f1767,f1742]) ).
fof(f4857,plain,
( ~ spl12_239
| ~ spl12_266 ),
inference(avatar_split_clause,[],[f3201,f1776,f1660]) ).
fof(f4862,plain,
( ~ spl12_267
| ~ spl12_286 ),
inference(avatar_split_clause,[],[f4548,f1864,f1780]) ).
fof(f4966,plain,
( op1(e10,e10) = e12
| ~ spl12_162
| ~ spl12_266 ),
inference(forward_demodulation,[],[f1287,f1778]) ).
fof(f4967,plain,
( $false
| ~ spl12_162
| spl12_251
| ~ spl12_266 ),
inference(forward_subsumption_resolution,[],[f4966,f1713]) ).
fof(f4968,plain,
( ~ spl12_162
| spl12_251
| ~ spl12_266 ),
inference(avatar_contradiction_clause,[],[f4967]) ).
fof(f4974,plain,
( e10 = op1(e11,e11)
| ~ spl12_164
| ~ spl12_248 ),
inference(forward_demodulation,[],[f1297,f1701]) ).
fof(f4975,plain,
( $false
| ~ spl12_164
| ~ spl12_248
| spl12_265 ),
inference(forward_subsumption_resolution,[],[f4974,f1773]) ).
fof(f4976,plain,
( ~ spl12_164
| ~ spl12_248
| spl12_265 ),
inference(avatar_contradiction_clause,[],[f4975]) ).
fof(f5120,plain,
( h2(e12) = op2(op2(e21,e22),e21)
| ~ spl12_211 ),
inference(forward_demodulation,[],[f299,f1514]) ).
fof(f5121,plain,
( op2(e20,e21) = h2(e12)
| ~ spl12_202
| ~ spl12_211 ),
inference(forward_demodulation,[],[f5120,f1474]) ).
fof(f5122,plain,
( e23 = h2(e12)
| ~ spl12_195
| ~ spl12_202
| ~ spl12_211 ),
inference(forward_demodulation,[],[f5121,f1444]) ).
fof(f5123,plain,
( spl12_87
| ~ spl12_195
| ~ spl12_202
| ~ spl12_211 ),
inference(avatar_split_clause,[],[f5122,f1512,f1472,f1442,f912]) ).
fof(f5125,plain,
( h2(op1(e12,e11)) != op2(e23,h2(e11))
| spl12_74
| ~ spl12_87 ),
inference(superposition,[],[f854,f913]) ).
fof(f5127,plain,
( op2(e23,e22) != h2(op1(e12,e11))
| spl12_74
| ~ spl12_84
| ~ spl12_87 ),
inference(forward_demodulation,[],[f5125,f895]) ).
fof(f5130,plain,
( op2(e23,e22) != h2(e11)
| spl12_74
| ~ spl12_84
| ~ spl12_87
| ~ spl12_273 ),
inference(forward_demodulation,[],[f5127,f1809]) ).
fof(f5131,plain,
( e22 != op2(e23,e22)
| spl12_74
| ~ spl12_84
| ~ spl12_87
| ~ spl12_273 ),
inference(forward_demodulation,[],[f5130,f895]) ).
fof(f5132,plain,
( $false
| spl12_74
| ~ spl12_84
| ~ spl12_87
| ~ spl12_229
| ~ spl12_273 ),
inference(forward_subsumption_resolution,[],[f5131,f1595]) ).
fof(f5133,plain,
( spl12_74
| ~ spl12_84
| ~ spl12_87
| ~ spl12_229
| ~ spl12_273 ),
inference(avatar_contradiction_clause,[],[f5132]) ).
fof(f5134,plain,
( op2(e20,e20) != h2(op1(e10,e10))
| ~ spl12_15
| spl12_65 ),
inference(forward_demodulation,[],[f818,f580]) ).
fof(f5136,plain,
( op2(e20,e20) != h2(e10)
| ~ spl12_15
| spl12_65
| ~ spl12_237 ),
inference(forward_demodulation,[],[f5134,f1654]) ).
fof(f5138,plain,
( e20 != op2(e20,e20)
| ~ spl12_15
| spl12_65
| ~ spl12_237 ),
inference(forward_demodulation,[],[f5136,f580]) ).
fof(f5140,plain,
( $false
| ~ spl12_15
| spl12_65
| ~ spl12_173
| ~ spl12_237 ),
inference(forward_subsumption_resolution,[],[f5138,f1350]) ).
fof(f5141,plain,
( ~ spl12_15
| spl12_65
| ~ spl12_173
| ~ spl12_237 ),
inference(avatar_contradiction_clause,[],[f5140]) ).
fof(f5144,plain,
( h2(op1(e10,e11)) != op2(h2(e10),e22)
| spl12_66
| ~ spl12_84 ),
inference(forward_demodulation,[],[f822,f895]) ).
fof(f5146,plain,
( op2(e20,e22) != h2(op1(e10,e11))
| ~ spl12_15
| spl12_66
| ~ spl12_84 ),
inference(forward_demodulation,[],[f5144,f580]) ).
fof(f5148,plain,
( op2(e20,e22) != h2(e13)
| ~ spl12_15
| spl12_66
| ~ spl12_84
| ~ spl12_259 ),
inference(forward_demodulation,[],[f5146,f1748]) ).
fof(f5149,plain,
( e21 != op2(e20,e22)
| ~ spl12_15
| ~ spl12_17
| spl12_66
| ~ spl12_84
| ~ spl12_259 ),
inference(forward_demodulation,[],[f5148,f589]) ).
fof(f5150,plain,
( $false
| ~ spl12_15
| ~ spl12_17
| spl12_66
| ~ spl12_84
| ~ spl12_182
| ~ spl12_259 ),
inference(forward_subsumption_resolution,[],[f5149,f1388]) ).
fof(f5151,plain,
( ~ spl12_15
| ~ spl12_17
| spl12_66
| ~ spl12_84
| ~ spl12_182
| ~ spl12_259 ),
inference(avatar_contradiction_clause,[],[f5150]) ).
fof(f5153,plain,
( h2(op1(e10,e12)) != op2(h2(e10),e23)
| spl12_67
| ~ spl12_87 ),
inference(forward_demodulation,[],[f826,f913]) ).
fof(f5155,plain,
( op2(e20,e23) != h2(op1(e10,e12))
| ~ spl12_15
| spl12_67
| ~ spl12_87 ),
inference(forward_demodulation,[],[f5153,f580]) ).
fof(f5157,plain,
( op2(e20,e23) != h2(e11)
| ~ spl12_15
| spl12_67
| ~ spl12_87
| ~ spl12_246 ),
inference(forward_demodulation,[],[f5155,f1692]) ).
fof(f5159,plain,
( e22 != op2(e20,e23)
| ~ spl12_15
| spl12_67
| ~ spl12_84
| ~ spl12_87
| ~ spl12_246 ),
inference(forward_demodulation,[],[f5157,f895]) ).
fof(f5160,plain,
( $false
| ~ spl12_15
| spl12_67
| ~ spl12_84
| ~ spl12_87
| ~ spl12_190
| ~ spl12_246 ),
inference(forward_subsumption_resolution,[],[f5159,f1422]) ).
fof(f5161,plain,
( ~ spl12_15
| spl12_67
| ~ spl12_84
| ~ spl12_87
| ~ spl12_190
| ~ spl12_246 ),
inference(avatar_contradiction_clause,[],[f5160]) ).
fof(f5163,plain,
( h2(op1(e10,e13)) != op2(h2(e10),e21)
| ~ spl12_17
| spl12_68 ),
inference(forward_demodulation,[],[f830,f589]) ).
fof(f5165,plain,
( op2(e20,e21) != h2(op1(e10,e13))
| ~ spl12_15
| ~ spl12_17
| spl12_68 ),
inference(forward_demodulation,[],[f5163,f580]) ).
fof(f5167,plain,
( op2(e20,e21) != h2(e12)
| ~ spl12_15
| ~ spl12_17
| spl12_68
| ~ spl12_254 ),
inference(forward_demodulation,[],[f5165,f1726]) ).
fof(f5169,plain,
( e23 != op2(e20,e21)
| ~ spl12_15
| ~ spl12_17
| spl12_68
| ~ spl12_87
| ~ spl12_254 ),
inference(forward_demodulation,[],[f5167,f913]) ).
fof(f5170,plain,
( $false
| ~ spl12_15
| ~ spl12_17
| spl12_68
| ~ spl12_87
| ~ spl12_195
| ~ spl12_254 ),
inference(forward_subsumption_resolution,[],[f5169,f1444]) ).
fof(f5171,plain,
( ~ spl12_15
| ~ spl12_17
| spl12_68
| ~ spl12_87
| ~ spl12_195
| ~ spl12_254 ),
inference(avatar_contradiction_clause,[],[f5170]) ).
fof(f5173,plain,
( h2(op1(e11,e10)) != op2(h2(e11),e20)
| ~ spl12_15
| spl12_69 ),
inference(forward_demodulation,[],[f834,f580]) ).
fof(f5175,plain,
( op2(e22,e20) != h2(op1(e11,e10))
| ~ spl12_15
| spl12_69
| ~ spl12_84 ),
inference(forward_demodulation,[],[f5173,f895]) ).
fof(f5177,plain,
( op2(e22,e20) != h2(e11)
| ~ spl12_15
| spl12_69
| ~ spl12_84
| ~ spl12_248 ),
inference(forward_demodulation,[],[f5175,f1701]) ).
fof(f5179,plain,
( e22 != op2(e22,e20)
| ~ spl12_15
| spl12_69
| ~ spl12_84
| ~ spl12_248 ),
inference(forward_demodulation,[],[f5177,f895]) ).
fof(f5180,plain,
( $false
| ~ spl12_15
| spl12_69
| ~ spl12_84
| ~ spl12_192
| ~ spl12_248 ),
inference(forward_subsumption_resolution,[],[f5179,f1431]) ).
fof(f5181,plain,
( ~ spl12_15
| spl12_69
| ~ spl12_84
| ~ spl12_192
| ~ spl12_248 ),
inference(avatar_contradiction_clause,[],[f5180]) ).
fof(f5183,plain,
( op2(e22,e22) != h2(op1(e11,e11))
| spl12_70
| ~ spl12_84 ),
inference(forward_demodulation,[],[f838,f895]) ).
fof(f5185,plain,
( op2(e22,e22) != h2(e12)
| spl12_70
| ~ spl12_84
| ~ spl12_275 ),
inference(forward_demodulation,[],[f5183,f1818]) ).
fof(f5187,plain,
( e23 != op2(e22,e22)
| spl12_70
| ~ spl12_84
| ~ spl12_87
| ~ spl12_275 ),
inference(forward_demodulation,[],[f5185,f913]) ).
fof(f5189,plain,
( $false
| spl12_70
| ~ spl12_84
| ~ spl12_87
| ~ spl12_230
| ~ spl12_275 ),
inference(forward_subsumption_resolution,[],[f5187,f1600]) ).
fof(f5190,plain,
( spl12_70
| ~ spl12_84
| ~ spl12_87
| ~ spl12_230
| ~ spl12_275 ),
inference(avatar_contradiction_clause,[],[f5189]) ).
fof(f5192,plain,
( h2(op1(e11,e12)) != op2(h2(e11),e23)
| spl12_71
| ~ spl12_87 ),
inference(forward_demodulation,[],[f842,f913]) ).
fof(f5194,plain,
( op2(e22,e23) != h2(op1(e11,e12))
| spl12_71
| ~ spl12_84
| ~ spl12_87 ),
inference(forward_demodulation,[],[f5192,f895]) ).
fof(f5196,plain,
( op2(e22,e23) != h2(e10)
| spl12_71
| ~ spl12_84
| ~ spl12_87
| ~ spl12_266 ),
inference(forward_demodulation,[],[f5194,f1778]) ).
fof(f5197,plain,
( e20 != op2(e22,e23)
| ~ spl12_15
| spl12_71
| ~ spl12_84
| ~ spl12_87
| ~ spl12_266 ),
inference(forward_demodulation,[],[f5196,f580]) ).
fof(f5198,plain,
( $false
| ~ spl12_15
| spl12_71
| ~ spl12_84
| ~ spl12_87
| ~ spl12_222
| ~ spl12_266 ),
inference(forward_subsumption_resolution,[],[f5197,f1562]) ).
fof(f5199,plain,
( ~ spl12_15
| spl12_71
| ~ spl12_84
| ~ spl12_87
| ~ spl12_222
| ~ spl12_266 ),
inference(avatar_contradiction_clause,[],[f5198]) ).
fof(f5201,plain,
( h2(op1(e11,e13)) != op2(h2(e11),e21)
| ~ spl12_17
| spl12_72 ),
inference(forward_demodulation,[],[f846,f589]) ).
fof(f5203,plain,
( op2(e22,e21) != h2(op1(e11,e13))
| ~ spl12_17
| spl12_72
| ~ spl12_84 ),
inference(forward_demodulation,[],[f5201,f895]) ).
fof(f5205,plain,
( op2(e22,e21) != h2(e13)
| ~ spl12_17
| spl12_72
| ~ spl12_84
| ~ spl12_282 ),
inference(forward_demodulation,[],[f5203,f1848]) ).
fof(f5207,plain,
( e21 != op2(e22,e21)
| ~ spl12_17
| spl12_72
| ~ spl12_84
| ~ spl12_282 ),
inference(forward_demodulation,[],[f5205,f589]) ).
fof(f5208,plain,
( $false
| ~ spl12_17
| spl12_72
| ~ spl12_84
| ~ spl12_209
| ~ spl12_282 ),
inference(forward_subsumption_resolution,[],[f5207,f1505]) ).
fof(f5209,plain,
( ~ spl12_17
| spl12_72
| ~ spl12_84
| ~ spl12_209
| ~ spl12_282 ),
inference(avatar_contradiction_clause,[],[f5208]) ).
fof(f5211,plain,
( h2(op1(e12,e10)) != op2(h2(e12),e20)
| ~ spl12_15
| spl12_73 ),
inference(forward_demodulation,[],[f850,f580]) ).
fof(f5213,plain,
( op2(e23,e20) != h2(op1(e12,e10))
| ~ spl12_15
| spl12_73
| ~ spl12_87 ),
inference(forward_demodulation,[],[f5211,f913]) ).
fof(f5215,plain,
( op2(e23,e20) != h2(e12)
| ~ spl12_15
| spl12_73
| ~ spl12_87
| ~ spl12_256 ),
inference(forward_demodulation,[],[f5213,f1735]) ).
fof(f5217,plain,
( e23 != op2(e23,e20)
| ~ spl12_15
| spl12_73
| ~ spl12_87
| ~ spl12_256 ),
inference(forward_demodulation,[],[f5215,f913]) ).
fof(f5218,plain,
( $false
| ~ spl12_15
| spl12_73
| ~ spl12_87
| ~ spl12_200
| ~ spl12_256 ),
inference(forward_subsumption_resolution,[],[f5217,f1465]) ).
fof(f5219,plain,
( ~ spl12_15
| spl12_73
| ~ spl12_87
| ~ spl12_200
| ~ spl12_256 ),
inference(avatar_contradiction_clause,[],[f5218]) ).
fof(f5221,plain,
( op2(e23,e23) != h2(op1(e12,e12))
| spl12_75
| ~ spl12_87 ),
inference(forward_demodulation,[],[f858,f913]) ).
fof(f5223,plain,
( op2(e23,e23) != h2(e13)
| spl12_75
| ~ spl12_87
| ~ spl12_294 ),
inference(forward_demodulation,[],[f5221,f1904]) ).
fof(f5225,plain,
( e21 != op2(e23,e23)
| ~ spl12_17
| spl12_75
| ~ spl12_87
| ~ spl12_294 ),
inference(forward_demodulation,[],[f5223,f589]) ).
fof(f5227,plain,
( $false
| ~ spl12_17
| spl12_75
| ~ spl12_87
| ~ spl12_234
| ~ spl12_294 ),
inference(forward_subsumption_resolution,[],[f5225,f1620]) ).
fof(f5228,plain,
( ~ spl12_17
| spl12_75
| ~ spl12_87
| ~ spl12_234
| ~ spl12_294 ),
inference(avatar_contradiction_clause,[],[f5227]) ).
fof(f5230,plain,
( h2(op1(e12,e13)) != op2(h2(e12),e21)
| ~ spl12_17
| spl12_76 ),
inference(forward_demodulation,[],[f862,f589]) ).
fof(f5232,plain,
( op2(e23,e21) != h2(op1(e12,e13))
| ~ spl12_17
| spl12_76
| ~ spl12_87 ),
inference(forward_demodulation,[],[f5230,f913]) ).
fof(f5234,plain,
( op2(e23,e21) != h2(e10)
| ~ spl12_17
| spl12_76
| ~ spl12_87
| ~ spl12_286 ),
inference(forward_demodulation,[],[f5232,f1866]) ).
fof(f5235,plain,
( e20 != op2(e23,e21)
| ~ spl12_15
| ~ spl12_17
| spl12_76
| ~ spl12_87
| ~ spl12_286 ),
inference(forward_demodulation,[],[f5234,f580]) ).
fof(f5236,plain,
( $false
| ~ spl12_15
| ~ spl12_17
| spl12_76
| ~ spl12_87
| ~ spl12_205
| ~ spl12_286 ),
inference(forward_subsumption_resolution,[],[f5235,f1487]) ).
fof(f5237,plain,
( ~ spl12_15
| ~ spl12_17
| spl12_76
| ~ spl12_87
| ~ spl12_205
| ~ spl12_286 ),
inference(avatar_contradiction_clause,[],[f5236]) ).
fof(f5239,plain,
( h2(op1(e13,e10)) != op2(h2(e13),e20)
| ~ spl12_15
| spl12_77 ),
inference(forward_demodulation,[],[f866,f580]) ).
fof(f5241,plain,
( op2(e21,e20) != h2(op1(e13,e10))
| ~ spl12_15
| ~ spl12_17
| spl12_77 ),
inference(forward_demodulation,[],[f5239,f589]) ).
fof(f5243,plain,
( op2(e21,e20) != h2(e13)
| ~ spl12_15
| ~ spl12_17
| spl12_77
| ~ spl12_264 ),
inference(forward_demodulation,[],[f5241,f1769]) ).
fof(f5245,plain,
( e21 != op2(e21,e20)
| ~ spl12_15
| ~ spl12_17
| spl12_77
| ~ spl12_264 ),
inference(forward_demodulation,[],[f5243,f589]) ).
fof(f5246,plain,
( $false
| ~ spl12_15
| ~ spl12_17
| spl12_77
| ~ spl12_184
| ~ spl12_264 ),
inference(forward_subsumption_resolution,[],[f5245,f1397]) ).
fof(f5247,plain,
( ~ spl12_15
| ~ spl12_17
| spl12_77
| ~ spl12_184
| ~ spl12_264 ),
inference(avatar_contradiction_clause,[],[f5246]) ).
fof(f5249,plain,
( h2(op1(e13,e11)) != op2(h2(e13),e22)
| spl12_78
| ~ spl12_84 ),
inference(forward_demodulation,[],[f870,f895]) ).
fof(f5251,plain,
( op2(e21,e22) != h2(op1(e13,e11))
| ~ spl12_17
| spl12_78
| ~ spl12_84 ),
inference(forward_demodulation,[],[f5249,f589]) ).
fof(f5253,plain,
( op2(e21,e22) != h2(e10)
| ~ spl12_17
| spl12_78
| ~ spl12_84
| ~ spl12_269 ),
inference(forward_demodulation,[],[f5251,f1791]) ).
fof(f5255,plain,
( e20 != op2(e21,e22)
| ~ spl12_15
| ~ spl12_17
| spl12_78
| ~ spl12_84
| ~ spl12_269 ),
inference(forward_demodulation,[],[f5253,f580]) ).
fof(f5256,plain,
( $false
| ~ spl12_15
| ~ spl12_17
| spl12_78
| ~ spl12_84
| ~ spl12_202
| ~ spl12_269 ),
inference(forward_subsumption_resolution,[],[f5255,f1474]) ).
fof(f5257,plain,
( ~ spl12_15
| ~ spl12_17
| spl12_78
| ~ spl12_84
| ~ spl12_202
| ~ spl12_269 ),
inference(avatar_contradiction_clause,[],[f5256]) ).
fof(f5259,plain,
( h2(op1(e13,e12)) != op2(h2(e13),e23)
| spl12_79
| ~ spl12_87 ),
inference(forward_demodulation,[],[f874,f913]) ).
fof(f5261,plain,
( op2(e21,e23) != h2(op1(e13,e12))
| ~ spl12_17
| spl12_79
| ~ spl12_87 ),
inference(forward_demodulation,[],[f5259,f589]) ).
fof(f5263,plain,
( op2(e21,e23) != h2(e12)
| ~ spl12_17
| spl12_79
| ~ spl12_87
| ~ spl12_293 ),
inference(forward_demodulation,[],[f5261,f1899]) ).
fof(f5265,plain,
( e23 != op2(e21,e23)
| ~ spl12_17
| spl12_79
| ~ spl12_87
| ~ spl12_293 ),
inference(forward_demodulation,[],[f5263,f913]) ).
fof(f5266,plain,
( $false
| ~ spl12_17
| spl12_79
| ~ spl12_87
| ~ spl12_218
| ~ spl12_293 ),
inference(forward_subsumption_resolution,[],[f5265,f1544]) ).
fof(f5267,plain,
( ~ spl12_17
| spl12_79
| ~ spl12_87
| ~ spl12_218
| ~ spl12_293 ),
inference(avatar_contradiction_clause,[],[f5266]) ).
fof(f5269,plain,
( op2(e21,e21) != h2(op1(e13,e13))
| ~ spl12_17
| spl12_80 ),
inference(forward_demodulation,[],[f878,f589]) ).
fof(f5271,plain,
( op2(e21,e21) != h2(e11)
| ~ spl12_17
| spl12_80
| ~ spl12_298 ),
inference(forward_demodulation,[],[f5269,f1924]) ).
fof(f5273,plain,
( e22 != op2(e21,e21)
| ~ spl12_17
| spl12_80
| ~ spl12_84
| ~ spl12_298 ),
inference(forward_demodulation,[],[f5271,f895]) ).
fof(f5275,plain,
( $false
| ~ spl12_17
| spl12_80
| ~ spl12_84
| ~ spl12_211
| ~ spl12_298 ),
inference(forward_subsumption_resolution,[],[f5273,f1514]) ).
fof(f5276,plain,
( ~ spl12_17
| spl12_80
| ~ spl12_84
| ~ spl12_211
| ~ spl12_298 ),
inference(avatar_contradiction_clause,[],[f5275]) ).
cnf(s12,plain,
( spl12_11
| ~ spl12_15 ),
inference(sat_conversion,[],[f582]) ).
cnf(s13,plain,
( spl12_16
| ~ spl12_17 ),
inference(sat_conversion,[],[f591]) ).
cnf(s59,plain,
( ~ spl12_11
| ~ spl12_16
| ~ spl12_65
| ~ spl12_66
| ~ spl12_67
| ~ spl12_68
| ~ spl12_69
| ~ spl12_70
| ~ spl12_71
| ~ spl12_72
| ~ spl12_73
| ~ spl12_74
| ~ spl12_75
| ~ spl12_76
| ~ spl12_77
| ~ spl12_78
| ~ spl12_79
| ~ spl12_80
| ~ spl12_84
| ~ spl12_87 ),
inference(sat_conversion,[],[f917]) ).
cnf(s98,plain,
spl12_105,
inference(sat_conversion,[],[f1152]) ).
cnf(s99,plain,
spl12_17,
inference(sat_conversion,[],[f1153]) ).
cnf(s100,plain,
spl12_2,
inference(sat_conversion,[],[f1154]) ).
cnf(s101,plain,
( ~ spl12_137
| spl12_138 ),
inference(sat_conversion,[],[f1163]) ).
cnf(s102,plain,
( ~ spl12_137
| spl12_139 ),
inference(sat_conversion,[],[f1168]) ).
cnf(s103,plain,
( ~ spl12_137
| spl12_140 ),
inference(sat_conversion,[],[f1173]) ).
cnf(s105,plain,
( ~ spl12_142
| spl12_143 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s106,plain,
( ~ spl12_142
| spl12_144 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s107,plain,
( ~ spl12_142
| spl12_145 ),
inference(sat_conversion,[],[f1197]) ).
cnf(s108,plain,
( ~ spl12_142
| spl12_146 ),
inference(sat_conversion,[],[f1202]) ).
cnf(s112,plain,
( spl12_137
| spl12_142
| spl12_148
| spl12_151 ),
inference(sat_conversion,[],[f1226]) ).
cnf(s113,plain,
( spl12_137
| spl12_142
| spl12_147
| spl12_152 ),
inference(sat_conversion,[],[f1231]) ).
cnf(s114,plain,
( spl12_137
| spl12_142
| spl12_149
| spl12_152 ),
inference(sat_conversion,[],[f1232]) ).
cnf(s115,plain,
( spl12_137
| spl12_142
| spl12_150
| spl12_152 ),
inference(sat_conversion,[],[f1233]) ).
cnf(s116,plain,
( spl12_137
| spl12_142
| spl12_151
| spl12_152 ),
inference(sat_conversion,[],[f1234]) ).
cnf(s122,plain,
( spl12_137
| spl12_142
| spl12_149
| spl12_154 ),
inference(sat_conversion,[],[f1248]) ).
cnf(s123,plain,
( spl12_137
| spl12_142
| spl12_150
| spl12_154 ),
inference(sat_conversion,[],[f1249]) ).
cnf(s124,plain,
( spl12_137
| spl12_142
| spl12_151
| spl12_154 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s125,plain,
( spl12_155
| spl12_156 ),
inference(sat_conversion,[],[f1259]) ).
cnf(s126,plain,
( spl12_155
| spl12_157 ),
inference(sat_conversion,[],[f1264]) ).
cnf(s129,plain,
( ~ spl12_160
| spl12_161 ),
inference(sat_conversion,[],[f1283]) ).
cnf(s130,plain,
( ~ spl12_160
| spl12_162 ),
inference(sat_conversion,[],[f1288]) ).
cnf(s132,plain,
( ~ spl12_160
| spl12_164 ),
inference(sat_conversion,[],[f1298]) ).
cnf(s137,plain,
( ~ spl12_155
| spl12_160
| spl12_165
| spl12_170 ),
inference(sat_conversion,[],[f1327]) ).
cnf(s138,plain,
( ~ spl12_155
| spl12_160
| spl12_167
| spl12_170 ),
inference(sat_conversion,[],[f1328]) ).
cnf(s140,plain,
( ~ spl12_155
| spl12_160
| spl12_169
| spl12_170 ),
inference(sat_conversion,[],[f1330]) ).
cnf(s145,plain,
( ~ spl12_155
| spl12_160
| spl12_165
| spl12_172 ),
inference(sat_conversion,[],[f1343]) ).
cnf(s149,plain,
( spl12_173
| spl12_174
| spl12_175
| spl12_176 ),
inference(sat_conversion,[],[f1363]) ).
cnf(s150,plain,
( spl12_173
| spl12_177
| spl12_178
| spl12_179 ),
inference(sat_conversion,[],[f1376]) ).
cnf(s151,plain,
( spl12_180
| spl12_181
| spl12_182
| spl12_183 ),
inference(sat_conversion,[],[f1393]) ).
cnf(s152,plain,
( spl12_180
| spl12_184
| spl12_185
| spl12_186 ),
inference(sat_conversion,[],[f1406]) ).
cnf(s157,plain,
( spl12_177
| spl12_201
| spl12_202
| spl12_203 ),
inference(sat_conversion,[],[f1479]) ).
cnf(s159,plain,
( spl12_184
| spl12_206
| spl12_207
| spl12_208 ),
inference(sat_conversion,[],[f1501]) ).
cnf(s160,plain,
( spl12_181
| spl12_206
| spl12_209
| spl12_210 ),
inference(sat_conversion,[],[f1510]) ).
cnf(s161,plain,
( spl12_191
| spl12_211
| spl12_212
| spl12_213 ),
inference(sat_conversion,[],[f1523]) ).
cnf(s162,plain,
( spl12_188
| spl12_211
| spl12_214
| spl12_215 ),
inference(sat_conversion,[],[f1532]) ).
cnf(s166,plain,
( spl12_175
| spl12_202
| spl12_221
| spl12_223 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s168,plain,
( spl12_182
| spl12_207
| spl12_224
| spl12_226 ),
inference(sat_conversion,[],[f1582]) ).
cnf(s169,plain,
( spl12_192
| spl12_214
| spl12_227
| spl12_228 ),
inference(sat_conversion,[],[f1591]) ).
cnf(s170,plain,
( spl12_189
| spl12_212
| spl12_227
| spl12_229 ),
inference(sat_conversion,[],[f1596]) ).
cnf(s174,plain,
( spl12_176
| spl12_203
| spl12_222
| spl12_233 ),
inference(sat_conversion,[],[f1616]) ).
cnf(s180,plain,
( spl12_197
| spl12_218
| spl12_231
| spl12_236 ),
inference(sat_conversion,[],[f1634]) ).
cnf(s181,plain,
( spl12_173
| spl12_180
| spl12_187
| spl12_194 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s182,plain,
( spl12_174
| spl12_181
| spl12_188
| spl12_195 ),
inference(sat_conversion,[],[f1636]) ).
cnf(s188,plain,
( spl12_203
| spl12_208
| spl12_213
| spl12_218 ),
inference(sat_conversion,[],[f1642]) ).
cnf(s192,plain,
( spl12_222
| spl12_225
| spl12_228
| spl12_231 ),
inference(sat_conversion,[],[f1646]) ).
cnf(s193,plain,
( spl12_179
| spl12_186
| spl12_193
| spl12_200 ),
inference(sat_conversion,[],[f1647]) ).
cnf(s195,plain,
( spl12_223
| spl12_226
| spl12_229
| spl12_232 ),
inference(sat_conversion,[],[f1649]) ).
cnf(s197,plain,
( spl12_237
| spl12_238
| spl12_239
| spl12_240 ),
inference(sat_conversion,[],[f1667]) ).
cnf(s198,plain,
( spl12_237
| spl12_241
| spl12_242
| spl12_243 ),
inference(sat_conversion,[],[f1680]) ).
cnf(s200,plain,
( spl12_244
| spl12_248
| spl12_249
| spl12_250 ),
inference(sat_conversion,[],[f1710]) ).
cnf(s203,plain,
( spl12_258
| spl12_259
| spl12_260
| spl12_261 ),
inference(sat_conversion,[],[f1757]) ).
cnf(s205,plain,
( spl12_241
| spl12_265
| spl12_266
| spl12_267 ),
inference(sat_conversion,[],[f1783]) ).
cnf(s213,plain,
( spl12_242
| spl12_268
| spl12_285
| spl12_286 ),
inference(sat_conversion,[],[f1867]) ).
cnf(s215,plain,
( spl12_249
| spl12_273
| spl12_288
| spl12_289 ),
inference(sat_conversion,[],[f1881]) ).
cnf(s216,plain,
( spl12_246
| spl12_271
| spl12_288
| spl12_290 ),
inference(sat_conversion,[],[f1886]) ).
cnf(s217,plain,
( spl12_256
| spl12_278
| spl12_291
| spl12_292 ),
inference(sat_conversion,[],[f1895]) ).
cnf(s218,plain,
( spl12_253
| spl12_276
| spl12_291
| spl12_293 ),
inference(sat_conversion,[],[f1900]) ).
cnf(s222,plain,
( spl12_240
| spl12_267
| spl12_286
| spl12_297 ),
inference(sat_conversion,[],[f1920]) ).
cnf(s225,plain,
( spl12_257
| spl12_279
| spl12_293
| spl12_299 ),
inference(sat_conversion,[],[f1931]) ).
cnf(s227,plain,
( spl12_264
| spl12_284
| spl12_296
| spl12_300 ),
inference(sat_conversion,[],[f1937]) ).
cnf(s228,plain,
( spl12_261
| spl12_282
| spl12_295
| spl12_300 ),
inference(sat_conversion,[],[f1938]) ).
cnf(s230,plain,
( spl12_238
| spl12_245
| spl12_252
| spl12_259 ),
inference(sat_conversion,[],[f1940]) ).
cnf(s245,plain,
spl12_298,
inference(sat_conversion,[],[f1959]) ).
cnf(s246,plain,
spl12_234,
inference(sat_conversion,[],[f1960]) ).
cnf(s253,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_173
| ~ spl12_180 ),
inference(sat_conversion,[],[f1984]) ).
cnf(s255,plain,
( ~ spl12_22
| ~ spl12_105
| ~ spl12_190
| spl12_228 ),
inference(sat_conversion,[],[f2000]) ).
cnf(s263,plain,
( spl12_22
| ~ spl12_105
| ~ spl12_175
| ~ spl12_189 ),
inference(sat_conversion,[],[f2022]) ).
cnf(s264,plain,
( spl12_22
| ~ spl12_105
| ~ spl12_176
| ~ spl12_190 ),
inference(sat_conversion,[],[f2026]) ).
cnf(s270,plain,
( ~ spl12_2
| ~ spl12_7 ),
inference(sat_conversion,[],[f2042]) ).
cnf(s273,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_177
| ~ spl12_184 ),
inference(sat_conversion,[],[f2052]) ).
cnf(s287,plain,
( ~ spl12_190
| ~ spl12_197 ),
inference(sat_conversion,[],[f2111]) ).
cnf(s296,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_201
| ~ spl12_206 ),
inference(sat_conversion,[],[f2158]) ).
cnf(s297,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_202
| ~ spl12_207 ),
inference(sat_conversion,[],[f2162]) ).
cnf(s300,plain,
( ~ spl12_206
| ~ spl12_211 ),
inference(sat_conversion,[],[f2174]) ).
cnf(s302,plain,
( ~ spl12_207
| ~ spl12_212 ),
inference(sat_conversion,[],[f2182]) ).
cnf(s305,plain,
( spl12_22
| ~ spl12_105
| ~ spl12_201
| ~ spl12_211 ),
inference(sat_conversion,[],[f2193]) ).
cnf(s307,plain,
( ~ spl12_209
| ~ spl12_214 ),
inference(sat_conversion,[],[f2202]) ).
cnf(s319,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_221
| ~ spl12_224 ),
inference(sat_conversion,[],[f2257]) ).
cnf(s321,plain,
( ~ spl12_224
| ~ spl12_227 ),
inference(sat_conversion,[],[f2265]) ).
cnf(s327,plain,
( ~ spl12_227
| ~ spl12_230 ),
inference(sat_conversion,[],[f2292]) ).
cnf(s332,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_233
| ~ spl12_234 ),
inference(sat_conversion,[],[f2319]) ).
cnf(s339,plain,
( ~ spl12_173
| ~ spl12_194 ),
inference(sat_conversion,[],[f2349]) ).
cnf(s346,plain,
( ~ spl12_234
| ~ spl12_236 ),
inference(sat_conversion,[],[f2384]) ).
cnf(s350,plain,
( ~ spl12_246
| ~ spl12_253 ),
inference(sat_conversion,[],[f2398]) ).
cnf(s353,plain,
( ~ spl12_237
| ~ spl12_244 ),
inference(sat_conversion,[],[f2409]) ).
cnf(s356,plain,
( ~ spl12_240
| ~ spl12_254 ),
inference(sat_conversion,[],[f2420]) ).
cnf(s358,plain,
( ~ spl12_241
| ~ spl12_248 ),
inference(sat_conversion,[],[f2427]) ).
cnf(s362,plain,
( ~ spl12_249
| ~ spl12_256 ),
inference(sat_conversion,[],[f2445]) ).
cnf(s364,plain,
( ~ spl12_250
| ~ spl12_257 ),
inference(sat_conversion,[],[f2452]) ).
cnf(s370,plain,
( ~ spl12_254
| ~ spl12_261 ),
inference(sat_conversion,[],[f2477]) ).
cnf(s377,plain,
( ~ spl12_266
| ~ spl12_271 ),
inference(sat_conversion,[],[f2507]) ).
cnf(s389,plain,
( ~ spl12_269
| ~ spl12_284 ),
inference(sat_conversion,[],[f2552]) ).
cnf(s395,plain,
( ~ spl12_237
| ~ spl12_258 ),
inference(sat_conversion,[],[f2579]) ).
cnf(s399,plain,
( ~ spl12_269
| ~ spl12_279 ),
inference(sat_conversion,[],[f2607]) ).
cnf(s401,plain,
( ~ spl12_267
| ~ spl12_282 ),
inference(sat_conversion,[],[f2618]) ).
cnf(s415,plain,
( ~ spl12_286
| ~ spl12_292 ),
inference(sat_conversion,[],[f2675]) ).
cnf(s416,plain,
( ~ spl12_239
| ~ spl12_260 ),
inference(sat_conversion,[],[f2680]) ).
cnf(s425,plain,
( ~ spl12_293
| ~ spl12_296 ),
inference(sat_conversion,[],[f2730]) ).
cnf(s427,plain,
( ~ spl12_288
| ~ spl12_294 ),
inference(sat_conversion,[],[f2738]) ).
cnf(s433,plain,
( ~ spl12_297
| ~ spl12_298 ),
inference(sat_conversion,[],[f2788]) ).
cnf(s435,plain,
( ~ spl12_250
| ~ spl12_264 ),
inference(sat_conversion,[],[f2799]) ).
cnf(s442,plain,
( ~ spl12_298
| ~ spl12_299 ),
inference(sat_conversion,[],[f2848]) ).
cnf(s452,plain,
( ~ spl12_242
| ~ spl12_249 ),
inference(sat_conversion,[],[f2905]) ).
cnf(s462,plain,
( ~ spl12_291
| ~ spl12_294 ),
inference(sat_conversion,[],[f2984]) ).
cnf(s465,plain,
( ~ spl12_298
| ~ spl12_300 ),
inference(sat_conversion,[],[f3016]) ).
cnf(s479,plain,
( ~ spl12_286
| ~ spl12_295 ),
inference(sat_conversion,[],[f3143]) ).
cnf(s486,plain,
( spl12_22
| ~ spl12_105
| ~ spl12_215
| ~ spl12_234 ),
inference(sat_conversion,[],[f3282]) ).
cnf(s487,plain,
( ~ spl12_210
| ~ spl12_234 ),
inference(sat_conversion,[],[f3285]) ).
cnf(s488,plain,
( spl12_205
| ~ spl12_234 ),
inference(sat_conversion,[],[f3289]) ).
cnf(s492,plain,
( ~ spl12_179
| ~ spl12_205 ),
inference(sat_conversion,[],[f3296]) ).
cnf(s494,plain,
( ~ spl12_209
| ~ spl12_224 ),
inference(sat_conversion,[],[f3302]) ).
cnf(s498,plain,
( ~ spl12_194
| ~ spl12_200 ),
inference(sat_conversion,[],[f3312]) ).
cnf(s504,plain,
( spl12_109
| ~ spl12_214
| ~ spl12_224 ),
inference(sat_conversion,[],[f3359]) ).
cnf(s510,plain,
( spl12_254
| ~ spl12_269
| ~ spl12_298 ),
inference(sat_conversion,[],[f3384]) ).
cnf(s515,plain,
( ~ spl12_251
| ~ spl12_254 ),
inference(sat_conversion,[],[f3395]) ).
cnf(s516,plain,
( ~ spl12_244
| ~ spl12_245 ),
inference(sat_conversion,[],[f3396]) ).
cnf(s522,plain,
( ~ spl12_190
| ~ spl12_213 ),
inference(sat_conversion,[],[f3451]) ).
cnf(s523,plain,
( spl12_190
| ~ spl12_205
| ~ spl12_234 ),
inference(sat_conversion,[],[f3452]) ).
cnf(s524,plain,
( ~ spl12_183
| ~ spl12_234 ),
inference(sat_conversion,[],[f3457]) ).
cnf(s531,plain,
( ~ spl12_208
| ~ spl12_234 ),
inference(sat_conversion,[],[f3466]) ).
cnf(s539,plain,
( ~ spl12_144
| ~ spl12_212
| spl12_227 ),
inference(sat_conversion,[],[f3517]) ).
cnf(s540,plain,
( ~ spl12_146
| ~ spl12_184
| spl12_201 ),
inference(sat_conversion,[],[f3519]) ).
cnf(s541,plain,
( ~ spl12_147
| ~ spl12_231
| spl12_236 ),
inference(sat_conversion,[],[f3527]) ).
cnf(s543,plain,
( ~ spl12_151
| ~ spl12_178
| ~ spl12_194 ),
inference(sat_conversion,[],[f3532]) ).
cnf(s544,plain,
( ~ spl12_148
| ~ spl12_193
| spl12_221 ),
inference(sat_conversion,[],[f3541]) ).
cnf(s546,plain,
( ~ spl12_152
| ~ spl12_194
| ~ spl12_205 ),
inference(sat_conversion,[],[f3547]) ).
cnf(s547,plain,
( ~ spl12_149
| spl12_211
| ~ spl12_224 ),
inference(sat_conversion,[],[f3550]) ).
cnf(s549,plain,
( ~ spl12_225
| ~ spl12_234 ),
inference(sat_conversion,[],[f3556]) ).
cnf(s551,plain,
( ~ spl12_154
| spl12_216
| ~ spl12_234 ),
inference(sat_conversion,[],[f3566]) ).
cnf(s554,plain,
( ~ spl12_180
| ~ spl12_181 ),
inference(sat_conversion,[],[f3571]) ).
cnf(s555,plain,
( ~ spl12_143
| spl12_194
| ~ spl12_203 ),
inference(sat_conversion,[],[f3578]) ).
cnf(s559,plain,
( ~ spl12_211
| ~ spl12_214 ),
inference(sat_conversion,[],[f3580]) ).
cnf(s565,plain,
( ~ spl12_173
| ~ spl12_175 ),
inference(sat_conversion,[],[f3586]) ).
cnf(s566,plain,
( ~ spl12_187
| ~ spl12_190 ),
inference(sat_conversion,[],[f3587]) ).
cnf(s572,plain,
( ~ spl12_226
| ~ spl12_234 ),
inference(sat_conversion,[],[f3595]) ).
cnf(s577,plain,
( ~ spl12_205
| ~ spl12_223 ),
inference(sat_conversion,[],[f3606]) ).
cnf(s590,plain,
( spl12_84
| ~ spl12_211 ),
inference(sat_conversion,[],[f3688]) ).
cnf(s593,plain,
( ~ spl12_140
| ~ spl12_181
| spl12_206 ),
inference(sat_conversion,[],[f3722]) ).
cnf(s598,plain,
( ~ spl12_181
| ~ spl12_206 ),
inference(sat_conversion,[],[f3743]) ).
cnf(s600,plain,
( ~ spl12_185
| ~ spl12_224 ),
inference(sat_conversion,[],[f3746]) ).
cnf(s603,plain,
( ~ spl12_143
| ~ spl12_218
| spl12_236 ),
inference(sat_conversion,[],[f3758]) ).
cnf(s604,plain,
( ~ spl12_144
| spl12_187
| ~ spl12_202 ),
inference(sat_conversion,[],[f3760]) ).
cnf(s612,plain,
( ~ spl12_152
| spl12_180
| ~ spl12_205 ),
inference(sat_conversion,[],[f3772]) ).
cnf(s640,plain,
( ~ spl12_188
| ~ spl12_190 ),
inference(sat_conversion,[],[f3801]) ).
cnf(s646,plain,
( ~ spl12_138
| ~ spl12_190
| spl12_230 ),
inference(sat_conversion,[],[f3812]) ).
cnf(s647,plain,
( ~ spl12_230
| ~ spl12_231 ),
inference(sat_conversion,[],[f3815]) ).
cnf(s648,plain,
( ~ spl12_150
| ~ spl12_214
| spl12_224 ),
inference(sat_conversion,[],[f3818]) ).
cnf(s651,plain,
( ~ spl12_195
| ~ spl12_216 ),
inference(sat_conversion,[],[f3821]) ).
cnf(s663,plain,
( ~ spl12_190
| ~ spl12_228 ),
inference(sat_conversion,[],[f3837]) ).
cnf(s672,plain,
( ~ spl12_174
| ~ spl12_205 ),
inference(sat_conversion,[],[f3840]) ).
cnf(s677,plain,
( ~ spl12_173
| ~ spl12_177 ),
inference(sat_conversion,[],[f3848]) ).
cnf(s681,plain,
( spl12_152
| ~ spl12_180
| ~ spl12_205 ),
inference(sat_conversion,[],[f3853]) ).
cnf(s692,plain,
( ~ spl12_109
| spl12_228
| ~ spl12_230 ),
inference(sat_conversion,[],[f3951]) ).
cnf(s696,plain,
( ~ spl12_139
| ~ spl12_182
| spl12_211 ),
inference(sat_conversion,[],[f3972]) ).
cnf(s710,plain,
( ~ spl12_206
| ~ spl12_207 ),
inference(sat_conversion,[],[f3994]) ).
cnf(s732,plain,
( ~ spl12_181
| ~ spl12_182 ),
inference(sat_conversion,[],[f4008]) ).
cnf(s737,plain,
( ~ spl12_194
| ~ spl12_195 ),
inference(sat_conversion,[],[f4010]) ).
cnf(s749,plain,
( ~ spl12_230
| ~ spl12_232 ),
inference(sat_conversion,[],[f4013]) ).
cnf(s752,plain,
( ~ spl12_186
| ~ spl12_234 ),
inference(sat_conversion,[],[f4026]) ).
cnf(s757,plain,
( ~ spl12_20
| spl12_208
| ~ spl12_216 ),
inference(sat_conversion,[],[f4036]) ).
cnf(s763,plain,
( ~ spl12_191
| ~ spl12_193 ),
inference(sat_conversion,[],[f4042]) ).
cnf(s770,plain,
( ~ spl12_145
| ~ spl12_211
| spl12_224 ),
inference(sat_conversion,[],[f4052]) ).
cnf(s773,plain,
( ~ spl12_185
| ~ spl12_209 ),
inference(sat_conversion,[],[f4057]) ).
cnf(s782,plain,
( ~ spl12_221
| ~ spl12_222 ),
inference(sat_conversion,[],[f4061]) ).
cnf(s785,plain,
( ~ spl12_151
| ~ spl12_185
| spl12_201 ),
inference(sat_conversion,[],[f4063]) ).
cnf(s806,plain,
( ~ spl12_193
| ~ spl12_229 ),
inference(sat_conversion,[],[f4081]) ).
cnf(s830,plain,
( spl12_20
| ~ spl12_207
| ~ spl12_211 ),
inference(sat_conversion,[],[f4238]) ).
cnf(s831,plain,
( ~ spl12_139
| ~ spl12_175
| spl12_187 ),
inference(sat_conversion,[],[f4245]) ).
cnf(s850,plain,
( ~ spl12_180
| ~ spl12_182 ),
inference(sat_conversion,[],[f4264]) ).
cnf(s852,plain,
( ~ spl12_184
| ~ spl12_207 ),
inference(sat_conversion,[],[f4265]) ).
cnf(s884,plain,
( spl12_15
| ~ spl12_202
| ~ spl12_211 ),
inference(sat_conversion,[],[f4331]) ).
cnf(s886,plain,
( ~ spl12_150
| spl12_206
| ~ spl12_209 ),
inference(sat_conversion,[],[f4356]) ).
cnf(s887,plain,
( ~ spl12_151
| ~ spl12_192
| spl12_221 ),
inference(sat_conversion,[],[f4360]) ).
cnf(s889,plain,
( ~ spl12_165
| ~ spl12_295
| spl12_300 ),
inference(sat_conversion,[],[f4372]) ).
cnf(s890,plain,
( ~ spl12_167
| spl12_251
| ~ spl12_285 ),
inference(sat_conversion,[],[f4374]) ).
cnf(s891,plain,
( ~ spl12_169
| ~ spl12_249
| spl12_265 ),
inference(sat_conversion,[],[f4377]) ).
cnf(s897,plain,
( ~ spl12_170
| ~ spl12_237
| ~ spl12_269 ),
inference(sat_conversion,[],[f4405]) ).
cnf(s898,plain,
( ~ spl12_156
| ~ spl12_254
| spl12_294 ),
inference(sat_conversion,[],[f4407]) ).
cnf(s899,plain,
( ~ spl12_294
| ~ spl12_295 ),
inference(sat_conversion,[],[f4411]) ).
cnf(s900,plain,
( ~ spl12_260
| ~ spl12_294 ),
inference(sat_conversion,[],[f4412]) ).
cnf(s904,plain,
( ~ spl12_289
| ~ spl12_298 ),
inference(sat_conversion,[],[f4418]) ).
cnf(s905,plain,
( ~ spl12_290
| ~ spl12_298 ),
inference(sat_conversion,[],[f4420]) ).
cnf(s906,plain,
( ~ spl12_172
| spl12_280
| ~ spl12_298 ),
inference(sat_conversion,[],[f4422]) ).
cnf(s907,plain,
( ~ spl12_265
| ~ spl12_269 ),
inference(sat_conversion,[],[f4424]) ).
cnf(s909,plain,
( ~ spl12_252
| ~ spl12_254 ),
inference(sat_conversion,[],[f4447]) ).
cnf(s914,plain,
( ~ spl12_266
| ~ spl12_276 ),
inference(sat_conversion,[],[f4518]) ).
cnf(s915,plain,
( ~ spl12_161
| ~ spl12_282
| spl12_300 ),
inference(sat_conversion,[],[f4566]) ).
cnf(s916,plain,
( ~ spl12_165
| spl12_258
| ~ spl12_286 ),
inference(sat_conversion,[],[f4573]) ).
cnf(s919,plain,
( ~ spl12_161
| spl12_258
| ~ spl12_267 ),
inference(sat_conversion,[],[f4588]) ).
cnf(s921,plain,
( ~ spl12_237
| ~ spl12_242 ),
inference(sat_conversion,[],[f4590]) ).
cnf(s925,plain,
( ~ spl12_275
| ~ spl12_278 ),
inference(sat_conversion,[],[f4600]) ).
cnf(s928,plain,
( ~ spl12_259
| ~ spl12_280 ),
inference(sat_conversion,[],[f4603]) ).
cnf(s934,plain,
( ~ spl12_157
| ~ spl12_246
| spl12_275 ),
inference(sat_conversion,[],[f4613]) ).
cnf(s949,plain,
( ~ spl12_157
| ~ spl12_239
| spl12_251 ),
inference(sat_conversion,[],[f4755]) ).
cnf(s955,plain,
( ~ spl12_170
| spl12_244
| ~ spl12_269 ),
inference(sat_conversion,[],[f4778]) ).
cnf(s967,plain,
( spl12_269
| ~ spl12_298 ),
inference(sat_conversion,[],[f4794]) ).
cnf(s972,plain,
( ~ spl12_243
| ~ spl12_269 ),
inference(sat_conversion,[],[f4823]) ).
cnf(s973,plain,
( ~ spl12_268
| ~ spl12_269 ),
inference(sat_conversion,[],[f4824]) ).
cnf(s974,plain,
( ~ spl12_238
| ~ spl12_269 ),
inference(sat_conversion,[],[f4825]) ).
cnf(s979,plain,
( ~ spl12_258
| ~ spl12_259 ),
inference(sat_conversion,[],[f4829]) ).
cnf(s980,plain,
( ~ spl12_241
| ~ spl12_267 ),
inference(sat_conversion,[],[f4830]) ).
cnf(s985,plain,
( ~ spl12_237
| ~ spl12_241 ),
inference(sat_conversion,[],[f4849]) ).
cnf(s992,plain,
( ~ spl12_258
| ~ spl12_264 ),
inference(sat_conversion,[],[f4855]) ).
cnf(s994,plain,
( ~ spl12_239
| ~ spl12_266 ),
inference(sat_conversion,[],[f4857]) ).
cnf(s1002,plain,
( ~ spl12_267
| ~ spl12_286 ),
inference(sat_conversion,[],[f4862]) ).
cnf(s1011,plain,
( ~ spl12_162
| spl12_251
| ~ spl12_266 ),
inference(sat_conversion,[],[f4968]) ).
cnf(s1013,plain,
( ~ spl12_164
| ~ spl12_248
| spl12_265 ),
inference(sat_conversion,[],[f4976]) ).
cnf(s1029,plain,
( spl12_87
| ~ spl12_195
| ~ spl12_202
| ~ spl12_211 ),
inference(sat_conversion,[],[f5123]) ).
cnf(s1031,plain,
( spl12_74
| ~ spl12_84
| ~ spl12_87
| ~ spl12_229
| ~ spl12_273 ),
inference(sat_conversion,[],[f5133]) ).
cnf(s1032,plain,
( ~ spl12_15
| spl12_65
| ~ spl12_173
| ~ spl12_237 ),
inference(sat_conversion,[],[f5141]) ).
cnf(s1033,plain,
( ~ spl12_15
| ~ spl12_17
| spl12_66
| ~ spl12_84
| ~ spl12_182
| ~ spl12_259 ),
inference(sat_conversion,[],[f5151]) ).
cnf(s1034,plain,
( ~ spl12_15
| spl12_67
| ~ spl12_84
| ~ spl12_87
| ~ spl12_190
| ~ spl12_246 ),
inference(sat_conversion,[],[f5161]) ).
cnf(s1035,plain,
( ~ spl12_15
| ~ spl12_17
| spl12_68
| ~ spl12_87
| ~ spl12_195
| ~ spl12_254 ),
inference(sat_conversion,[],[f5171]) ).
cnf(s1036,plain,
( ~ spl12_15
| spl12_69
| ~ spl12_84
| ~ spl12_192
| ~ spl12_248 ),
inference(sat_conversion,[],[f5181]) ).
cnf(s1037,plain,
( spl12_70
| ~ spl12_84
| ~ spl12_87
| ~ spl12_230
| ~ spl12_275 ),
inference(sat_conversion,[],[f5190]) ).
cnf(s1038,plain,
( ~ spl12_15
| spl12_71
| ~ spl12_84
| ~ spl12_87
| ~ spl12_222
| ~ spl12_266 ),
inference(sat_conversion,[],[f5199]) ).
cnf(s1039,plain,
( ~ spl12_17
| spl12_72
| ~ spl12_84
| ~ spl12_209
| ~ spl12_282 ),
inference(sat_conversion,[],[f5209]) ).
cnf(s1040,plain,
( ~ spl12_15
| spl12_73
| ~ spl12_87
| ~ spl12_200
| ~ spl12_256 ),
inference(sat_conversion,[],[f5219]) ).
cnf(s1041,plain,
( ~ spl12_17
| spl12_75
| ~ spl12_87
| ~ spl12_234
| ~ spl12_294 ),
inference(sat_conversion,[],[f5228]) ).
cnf(s1042,plain,
( ~ spl12_15
| ~ spl12_17
| spl12_76
| ~ spl12_87
| ~ spl12_205
| ~ spl12_286 ),
inference(sat_conversion,[],[f5237]) ).
cnf(s1043,plain,
( ~ spl12_15
| ~ spl12_17
| spl12_77
| ~ spl12_184
| ~ spl12_264 ),
inference(sat_conversion,[],[f5247]) ).
cnf(s1044,plain,
( ~ spl12_15
| ~ spl12_17
| spl12_78
| ~ spl12_84
| ~ spl12_202
| ~ spl12_269 ),
inference(sat_conversion,[],[f5257]) ).
cnf(s1045,plain,
( ~ spl12_17
| spl12_79
| ~ spl12_87
| ~ spl12_218
| ~ spl12_293 ),
inference(sat_conversion,[],[f5267]) ).
cnf(s1046,plain,
( ~ spl12_17
| spl12_80
| ~ spl12_84
| ~ spl12_211
| ~ spl12_298 ),
inference(sat_conversion,[],[f5276]) ).
cnf(s1047,plain,
~ spl12_186,
inference(rat,[],[s752,s246]) ).
cnf(s1048,plain,
~ spl12_226,
inference(rat,[],[s572,s246]) ).
cnf(s1049,plain,
~ spl12_225,
inference(rat,[],[s549,s246]) ).
cnf(s1050,plain,
~ spl12_208,
inference(rat,[],[s531,s246]) ).
cnf(s1051,plain,
~ spl12_183,
inference(rat,[],[s524,s246]) ).
cnf(s1053,plain,
spl12_205,
inference(rat,[],[s488,s246]) ).
cnf(s1054,plain,
~ spl12_210,
inference(rat,[],[s487,s246]) ).
cnf(s1056,plain,
~ spl12_236,
inference(rat,[],[s346,s246]) ).
cnf(s1057,plain,
~ spl12_174,
inference(rat,[],[s672,s1053]) ).
cnf(s1058,plain,
~ spl12_223,
inference(rat,[],[s577,s1053]) ).
cnf(s1059,plain,
spl12_190,
inference(rat,[],[s523,s246,s1053]) ).
cnf(s1062,plain,
~ spl12_179,
inference(rat,[],[s492,s1053]) ).
cnf(s1063,plain,
~ spl12_228,
inference(rat,[],[s663,s1059]) ).
cnf(s1064,plain,
~ spl12_188,
inference(rat,[],[s640,s1059]) ).
cnf(s1065,plain,
~ spl12_187,
inference(rat,[],[s566,s1059]) ).
cnf(s1066,plain,
~ spl12_213,
inference(rat,[],[s522,s1059]) ).
cnf(s1067,plain,
~ spl12_197,
inference(rat,[],[s287,s1059]) ).
cnf(s1068,plain,
spl12_269,
inference(rat,[],[s967,s245]) ).
cnf(s1070,plain,
~ spl12_290,
inference(rat,[],[s905,s245]) ).
cnf(s1071,plain,
~ spl12_289,
inference(rat,[],[s904,s245]) ).
cnf(s1072,plain,
~ spl12_300,
inference(rat,[],[s465,s245]) ).
cnf(s1073,plain,
~ spl12_299,
inference(rat,[],[s442,s245]) ).
cnf(s1074,plain,
~ spl12_297,
inference(rat,[],[s433,s245]) ).
cnf(s1075,plain,
~ spl12_238,
inference(rat,[],[s974,s1068]) ).
cnf(s1076,plain,
~ spl12_268,
inference(rat,[],[s973,s1068]) ).
cnf(s1077,plain,
~ spl12_243,
inference(rat,[],[s972,s1068]) ).
cnf(s1078,plain,
~ spl12_265,
inference(rat,[],[s907,s1068]) ).
cnf(s1079,plain,
spl12_254,
inference(rat,[],[s510,s245,s1068]) ).
cnf(s1080,plain,
~ spl12_279,
inference(rat,[],[s399,s1068]) ).
cnf(s1081,plain,
~ spl12_284,
inference(rat,[],[s389,s1068]) ).
cnf(s1082,plain,
~ spl12_252,
inference(rat,[],[s909,s1079]) ).
cnf(s1083,plain,
~ spl12_251,
inference(rat,[],[s515,s1079]) ).
cnf(s1084,plain,
~ spl12_261,
inference(rat,[],[s370,s1079]) ).
cnf(s1085,plain,
~ spl12_240,
inference(rat,[],[s356,s1079]) ).
cnf(s1092,plain,
( spl12_245
| spl12_259 ),
inference(rat,[],[s230,s1082,s1075]) ).
cnf(s1094,plain,
( spl12_282
| spl12_295 ),
inference(rat,[],[s228,s1072,s1084]) ).
cnf(s1095,plain,
( spl12_264
| spl12_296 ),
inference(rat,[],[s227,s1072,s1081]) ).
cnf(s1096,plain,
( spl12_257
| spl12_293 ),
inference(rat,[],[s225,s1073,s1080]) ).
cnf(s1097,plain,
( spl12_267
| spl12_286 ),
inference(rat,[],[s222,s1074,s1085]) ).
cnf(s1098,plain,
( spl12_246
| spl12_271
| spl12_288 ),
inference(rat,[],[s216,s1070]) ).
cnf(s1099,plain,
( spl12_249
| spl12_273
| spl12_288 ),
inference(rat,[],[s215,s1071]) ).
cnf(s1100,plain,
( spl12_242
| spl12_285
| spl12_286 ),
inference(rat,[],[s213,s1076]) ).
cnf(s1104,plain,
( spl12_241
| spl12_266
| spl12_267 ),
inference(rat,[],[s205,s1078]) ).
cnf(s1105,plain,
( spl12_258
| spl12_259
| spl12_260 ),
inference(rat,[],[s203,s1084]) ).
cnf(s1108,plain,
( spl12_237
| spl12_241
| spl12_242 ),
inference(rat,[],[s198,s1077]) ).
cnf(s1109,plain,
( spl12_237
| spl12_239 ),
inference(rat,[],[s197,s1085,s1075]) ).
cnf(s1110,plain,
( spl12_229
| spl12_232 ),
inference(rat,[],[s195,s1048,s1058]) ).
cnf(s1111,plain,
( spl12_193
| spl12_200 ),
inference(rat,[],[s193,s1047,s1062]) ).
cnf(s1112,plain,
( spl12_222
| spl12_231 ),
inference(rat,[],[s192,s1063,s1049]) ).
cnf(s1114,plain,
( spl12_203
| spl12_218 ),
inference(rat,[],[s188,s1066,s1050]) ).
cnf(s1115,plain,
( spl12_181
| spl12_195 ),
inference(rat,[],[s182,s1064,s1057]) ).
cnf(s1116,plain,
( spl12_173
| spl12_180
| spl12_194 ),
inference(rat,[],[s181,s1065]) ).
cnf(s1117,plain,
( spl12_218
| spl12_231 ),
inference(rat,[],[s180,s1056,s1067]) ).
cnf(s1120,plain,
( spl12_192
| spl12_214
| spl12_227 ),
inference(rat,[],[s169,s1063]) ).
cnf(s1121,plain,
( spl12_182
| spl12_207
| spl12_224 ),
inference(rat,[],[s168,s1048]) ).
cnf(s1123,plain,
( spl12_175
| spl12_202
| spl12_221 ),
inference(rat,[],[s166,s1058]) ).
cnf(s1125,plain,
( spl12_211
| spl12_214
| spl12_215 ),
inference(rat,[],[s162,s1064]) ).
cnf(s1126,plain,
( spl12_191
| spl12_211
| spl12_212 ),
inference(rat,[],[s161,s1066]) ).
cnf(s1127,plain,
( spl12_181
| spl12_206
| spl12_209 ),
inference(rat,[],[s160,s1054]) ).
cnf(s1128,plain,
( spl12_184
| spl12_206
| spl12_207 ),
inference(rat,[],[s159,s1050]) ).
cnf(s1131,plain,
( spl12_180
| spl12_184
| spl12_185 ),
inference(rat,[],[s152,s1047]) ).
cnf(s1132,plain,
( spl12_180
| spl12_181
| spl12_182 ),
inference(rat,[],[s151,s1051]) ).
cnf(s1133,plain,
( spl12_173
| spl12_177
| spl12_178 ),
inference(rat,[],[s150,s1062]) ).
cnf(s1134,plain,
( spl12_173
| spl12_175
| spl12_176 ),
inference(rat,[],[s149,s1057]) ).
cnf(s1135,plain,
~ spl12_7,
inference(rat,[],[s270,s100]) ).
cnf(s1136,plain,
~ spl12_233,
inference(rat,[],[s332,s246,s100,s1135]) ).
cnf(s1138,plain,
~ spl12_22,
inference(rat,[],[s255,s1063,s1059,s98]) ).
cnf(s1139,plain,
~ spl12_215,
inference(rat,[],[s486,s246,s98,s1138]) ).
cnf(s1140,plain,
~ spl12_176,
inference(rat,[],[s264,s1059,s98,s1138]) ).
cnf(s1151,plain,
spl12_16,
inference(rat,[],[s13,s99]) ).
cnf(s1153,plain,
( ~ spl12_207
| spl12_20
| spl12_191 ),
inference(rat,[],[s1126,s302,s830]) ).
cnf(s1154,plain,
( spl12_207
| ~ spl12_194
| spl12_173 ),
inference(rat,[],[s106,s112,s539,s543,s544,s170,s1133,s319,s321,s273,s1121,s1128,s263,s102,s831,s1134,s732,s598,s1115,s737,s806,s1111,s498,s100,s1135,s1065,s1140,s1138,s98]) ).
cnf(s1155,plain,
( spl12_180
| spl12_173 ),
inference(rat,[],[s124,s107,s785,s551,s770,s305,s600,s757,s1126,s1131,s1153,s302,s852,s1154,s763,s1111,s498,s1116,s102,s831,s1134,s246,s98,s1138,s1050,s1065,s1140]) ).
cnf(s1157,plain,
( spl12_206
| spl12_173 ),
inference(rat,[],[s107,s770,s123,s1125,s886,s307,s494,s1127,s102,s831,s1134,s551,s651,s1115,s554,s1155,s1139,s246,s1065,s1140]) ).
cnf(s1158,plain,
spl12_173,
inference(rat,[],[s1114,s555,s603,s105,s122,s547,s1121,s300,s710,s1157,s551,s651,s1115,s546,s554,s681,s850,s1155,s102,s831,s1134,s1056,s246,s1053,s1065,s1140]) ).
cnf(s1159,plain,
~ spl12_177,
inference(rat,[],[s677,s1158]) ).
cnf(s1163,plain,
~ spl12_175,
inference(rat,[],[s565,s1158]) ).
cnf(s1165,plain,
~ spl12_194,
inference(rat,[],[s339,s1158]) ).
cnf(s1166,plain,
~ spl12_180,
inference(rat,[],[s253,s1135,s100,s1158]) ).
cnf(s1173,plain,
~ spl12_152,
inference(rat,[],[s612,s1053,s1166]) ).
cnf(s1174,plain,
~ spl12_207,
inference(rat,[],[s105,s113,s103,s555,s541,s593,s174,s1112,s1127,s782,s773,s1123,s1131,s297,s710,s852,s1173,s1165,s1056,s1140,s1136,s1163,s1166,s100,s1135]) ).
cnf(s1175,plain,
( spl12_224
| spl12_211 ),
inference(rat,[],[s157,s555,s604,s105,s106,s115,s296,s102,s1127,s696,s732,s648,s1121,s307,s1125,s1159,s1165,s1065,s1173,s100,s1135,s1174,s1139]) ).
cnf(s1176,plain,
spl12_211,
inference(rat,[],[s114,s101,s106,s646,s604,s692,s1123,s504,s547,s319,s1175,s1125,s1173,s1059,s1065,s1063,s1163,s100,s1135,s1139]) ).
cnf(s1177,plain,
spl12_84,
inference(rat,[],[s590,s1176]) ).
cnf(s1179,plain,
~ spl12_214,
inference(rat,[],[s559,s1176]) ).
cnf(s1180,plain,
~ spl12_206,
inference(rat,[],[s300,s1176]) ).
cnf(s1181,plain,
~ spl12_201,
inference(rat,[],[s305,s1138,s98,s1176]) ).
cnf(s1183,plain,
spl12_80,
inference(rat,[],[s1046,s245,s1176,s99,s1177]) ).
cnf(s1185,plain,
spl12_184,
inference(rat,[],[s1128,s1174,s1180]) ).
cnf(s1186,plain,
~ spl12_146,
inference(rat,[],[s540,s1185,s1181]) ).
cnf(s1189,plain,
~ spl12_142,
inference(rat,[],[s108,s1186]) ).
cnf(s1190,plain,
( ~ spl12_295
| ~ spl12_259
| ~ spl12_155 ),
inference(rat,[],[s919,s129,s1097,s145,s479,s889,s979,s906,s928,s1072,s245]) ).
cnf(s1191,plain,
( ~ spl12_259
| ~ spl12_155 ),
inference(rat,[],[s916,s145,s1097,s129,s401,s915,s1094,s1190,s906,s928,s979,s1072,s245]) ).
cnf(s1192,plain,
( ~ spl12_160
| spl12_237 ),
inference(rat,[],[s980,s1097,s1108,s479,s452,s1094,s200,s915,s1013,s129,s132,s516,s1092,s364,s1096,s425,s1095,s992,s1105,s1191,s126,s949,s416,s1109,s1072,s1078,s1083]) ).
cnf(s1193,plain,
spl12_237,
inference(rat,[],[s1104,s401,s358,s1094,s200,s889,s891,s137,s140,s1192,s364,s1096,s425,s1095,s955,s992,s516,s1105,s1092,s1191,s126,s416,s949,s994,s1109,s1072,s1078,s1068,s1083]) ).
cnf(s1195,plain,
~ spl12_241,
inference(rat,[],[s985,s1193]) ).
cnf(s1196,plain,
~ spl12_242,
inference(rat,[],[s921,s1193]) ).
cnf(s1197,plain,
~ spl12_170,
inference(rat,[],[s897,s1068,s1193]) ).
cnf(s1198,plain,
~ spl12_258,
inference(rat,[],[s395,s1193]) ).
cnf(s1199,plain,
~ spl12_244,
inference(rat,[],[s353,s1193]) ).
cnf(s1203,plain,
~ spl12_160,
inference(rat,[],[s1104,s919,s1011,s129,s130,s1195,s1198,s1083]) ).
cnf(s1205,plain,
~ spl12_267,
inference(rat,[],[s125,s898,s138,s899,s890,s1094,s1100,s401,s1002,s1079,s1203,s1197,s1083,s1196]) ).
cnf(s1206,plain,
spl12_286,
inference(rat,[],[s1097,s1205]) ).
cnf(s1207,plain,
spl12_266,
inference(rat,[],[s1104,s1195,s1205]) ).
cnf(s1209,plain,
~ spl12_295,
inference(rat,[],[s479,s1206]) ).
cnf(s1210,plain,
~ spl12_292,
inference(rat,[],[s415,s1206]) ).
cnf(s1212,plain,
~ spl12_165,
inference(rat,[],[s916,s1198,s1206]) ).
cnf(s1213,plain,
~ spl12_276,
inference(rat,[],[s914,s1207]) ).
cnf(s1214,plain,
~ spl12_271,
inference(rat,[],[s377,s1207]) ).
cnf(s1217,plain,
spl12_282,
inference(rat,[],[s1094,s1209]) ).
cnf(s1218,plain,
~ spl12_155,
inference(rat,[],[s137,s1203,s1197,s1212]) ).
cnf(s1226,plain,
spl12_157,
inference(rat,[],[s126,s1218]) ).
cnf(s1227,plain,
spl12_156,
inference(rat,[],[s125,s1218]) ).
cnf(s1229,plain,
spl12_294,
inference(rat,[],[s898,s1079,s1227]) ).
cnf(s1230,plain,
~ spl12_260,
inference(rat,[],[s900,s1229]) ).
cnf(s1231,plain,
~ spl12_291,
inference(rat,[],[s462,s1229]) ).
cnf(s1232,plain,
~ spl12_288,
inference(rat,[],[s427,s1229]) ).
cnf(s1234,plain,
spl12_259,
inference(rat,[],[s1105,s1198,s1230]) ).
cnf(s1235,plain,
spl12_246,
inference(rat,[],[s1098,s1214,s1232]) ).
cnf(s1237,plain,
spl12_275,
inference(rat,[],[s934,s1226,s1235]) ).
cnf(s1238,plain,
~ spl12_253,
inference(rat,[],[s350,s1235]) ).
cnf(s1242,plain,
~ spl12_278,
inference(rat,[],[s925,s1237]) ).
cnf(s1244,plain,
spl12_293,
inference(rat,[],[s218,s1231,s1213,s1238]) ).
cnf(s1245,plain,
spl12_256,
inference(rat,[],[s217,s1210,s1231,s1242]) ).
cnf(s1247,plain,
~ spl12_296,
inference(rat,[],[s425,s1244]) ).
cnf(s1252,plain,
~ spl12_249,
inference(rat,[],[s362,s1245]) ).
cnf(s1254,plain,
spl12_264,
inference(rat,[],[s1095,s1247]) ).
cnf(s1255,plain,
spl12_273,
inference(rat,[],[s1099,s1232,s1252]) ).
cnf(s1257,plain,
~ spl12_250,
inference(rat,[],[s435,s1254]) ).
cnf(s1262,plain,
spl12_248,
inference(rat,[],[s200,s1252,s1199,s1257]) ).
cnf(s1267,plain,
~ spl12_182,
inference(rat,[],[s1036,s59,s1031,s1043,s1040,s1045,s1037,s1034,s1033,s1041,s1039,s1038,s1042,s1032,s1035,s1044,s12,s1029,s884,s1123,s1111,s782,s806,s1120,s1117,s1112,s1110,s327,s647,s749,s646,s101,s115,s886,s1127,s1115,s732,s1262,s1177,s1151,s1183,s1255,s1254,s99,s1185,s1245,s1244,s1237,s1235,s1059,s1234,s1229,s246,s1217,s1207,s1206,s1053,s1193,s1158,s1079,s1068,s1176,s1163,s1179,s1189,s1173,s1180]) ).
cnf(s1268,plain,
spl12_181,
inference(rat,[],[s1132,s1166,s1267]) ).
cnf(s1269,plain,
spl12_224,
inference(rat,[],[s1121,s1174,s1267]) ).
cnf(s1272,plain,
~ spl12_140,
inference(rat,[],[s593,s1180,s1268]) ).
cnf(s1275,plain,
~ spl12_227,
inference(rat,[],[s321,s1269]) ).
cnf(s1276,plain,
~ spl12_221,
inference(rat,[],[s319,s1135,s100,s1269]) ).
cnf(s1281,plain,
~ spl12_137,
inference(rat,[],[s103,s1272]) ).
cnf(s1283,plain,
spl12_192,
inference(rat,[],[s1120,s1179,s1275]) ).
cnf(s1295,plain,
spl12_151,
inference(rat,[],[s116,s1173,s1189,s1281]) ).
cnf(s1296,plain,
$false,
inference(rat,[],[s887,s1276,s1283,s1295]) ).
fof(f5277,plain,
$false,
inference(avatar_sat_refutation,[],[s1296]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG116+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.17 % Computer : n002.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 19:33:07 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 Running first-order model finding
% 0.09/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.05/0.38 % (675540)Will run a generic schedule for satisfiability detection.
% 1.05/0.38 % (675550)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4076448356:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.05/0.38 % (675546)% WARNING: option uhcvi not known.
% 1.05/0.38 % (675545)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2631736801_2999 on theBenchmark for (2999ds/0Mi)
% 1.05/0.38 % (675548)dis+10_1_sil=32000:sp=arity:random_seed=738708097:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.05/0.38 % (675547)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3862563436:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.05/0.38 % (675549)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=676883758:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.05/0.38 % (675551)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3300211726:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.05/0.38 % (675546)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=456060514:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.05/0.38 % (675550)Instruction limit reached!
% 1.05/0.38 % (675550)------------------------------
% 1.05/0.38 % (675550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.05/0.38 % (675550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.05/0.38 % (675550)CaDiCaL version: 2.1.3
% 1.05/0.38 % (675550)Termination reason: Instruction limit
% 1.05/0.38 % (675550)Termination phase: Saturation
% 1.05/0.38 % (675550)Time elapsed: 0.037 s
% 1.05/0.38 % (675550)Peak memory usage: 13 MB
% 1.05/0.38 % (675550)Instructions burned: 132 (million)
% 1.05/0.38 % Detected minimum model sizes of [8]
% 1.05/0.38 % Detected maximum model sizes of [max]
% 1.05/0.38 % TRYING [8]
% 1.05/0.38 % (675559)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1922026484:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.05/0.38 % (675548)Instruction limit reached!
% 1.05/0.38 % (675548)------------------------------
% 1.05/0.38 % (675548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.05/0.38 % (675548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.05/0.38 % (675548)CaDiCaL version: 2.1.3
% 1.05/0.38 % (675548)Termination reason: Instruction limit
% 1.05/0.38 % (675548)Termination phase: Saturation
% 1.05/0.38 % (675548)Time elapsed: 0.053 s
% 1.05/0.38 % (675548)Peak memory usage: 12 MB
% 1.05/0.38 % (675548)Instructions burned: 103 (million)
% 1.05/0.38 % Detected minimum model sizes of [8]
% 1.05/0.38 % Detected maximum model sizes of [max]
% 1.05/0.38 % TRYING [8]
% 1.05/0.38 % (675549)Instruction limit reached!
% 1.05/0.38 % (675549)------------------------------
% 1.05/0.38 % (675549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.05/0.38 % (675549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.05/0.38 % (675549)CaDiCaL version: 2.1.3
% 1.05/0.38 % (675549)Termination reason: Instruction limit
% 1.05/0.38 % (675549)Termination phase: Saturation
% 1.05/0.38 % (675549)Time elapsed: 0.057 s
% 1.05/0.38 % (675549)Peak memory usage: 13 MB
% 1.05/0.38 % (675549)Instructions burned: 116 (million)
% 1.05/0.38 % (675561)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1879377174:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.05/0.38 % (675562)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=2940123525:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.05/0.38 % (675551)Instruction limit reached!
% 1.05/0.38 % (675551)------------------------------
% 1.05/0.38 % (675551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.05/0.38 % (675551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.05/0.38 % (675551)CaDiCaL version: 2.1.3
% 1.05/0.38 % (675551)Termination reason: Instruction limit
% 1.05/0.38 % (675551)Termination phase: Saturation
% 1.05/0.38 % (675551)Time elapsed: 0.086 s
% 1.05/0.38 % (675551)Peak memory usage: 13 MB
% 1.05/0.38 % (675551)Instructions burned: 160 (million)
% 1.05/0.38 % (675565)ott-21_1_sil=16000:fs=off:random_seed=4071766357:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.05/0.38 % (675546) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-675540-675546"...
% 1.05/0.38 % TRYING [9]
% 1.05/0.38 % (675546)...printing done.
% 1.05/0.38 % (675546)Refutation found. Thanks to Tanya!
% 1.05/0.38 % SZS status Theorem for theBenchmark
% 1.05/0.38 % SZS output start Proof for theBenchmark
% See solution above
% 1.05/0.40 % (675546)------------------------------
% 1.05/0.40 % (675546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.05/0.40 % (675546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.05/0.40 % (675546)CaDiCaL version: 2.1.3
% 1.05/0.40 % (675546)Termination reason: Refutation
% 1.05/0.40 % (675546)Time elapsed: 0.130 s
% 1.05/0.40 % (675546)Peak memory usage: 15 MB
% 1.05/0.40 % (675546)Instructions burned: 252 (million)
% 1.05/0.40 % (675540)Success in time 0.174 s
% 1.05/0.40 % Vampire exiting
%------------------------------------------------------------------------------