%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG125+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:23:12 AM UTC 2026
% Result : Theorem 0.38s 0.36s
% Output : Refutation 0.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 185
% Syntax : Number of formulae : 1368 ( 166 unt; 169 def)
% Number of atoms : 4628 (1850 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 5509 (2249 ~;2621 |; 470 &)
% ( 169 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 177 ( 175 usr; 176 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e10) = e11
| op1(e10,e10) = e12
| op1(e10,e10) = e13 )
& ( op1(e10,e11) = e10
| op1(e10,e11) = e11
| op1(e10,e11) = e12
| op1(e10,e11) = e13 )
& ( op1(e10,e12) = e10
| op1(e10,e12) = e11
| op1(e10,e12) = e12
| op1(e10,e12) = e13 )
& ( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e12
| op1(e10,e13) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 )
& ( op1(e11,e11) = e10
| op1(e11,e11) = e11
| op1(e11,e11) = e12
| op1(e11,e11) = e13 )
& ( op1(e11,e12) = e10
| op1(e11,e12) = e11
| op1(e11,e12) = e12
| op1(e11,e12) = e13 )
& ( op1(e11,e13) = e10
| op1(e11,e13) = e11
| op1(e11,e13) = e12
| op1(e11,e13) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e10) = e11
| op1(e12,e10) = e12
| op1(e12,e10) = e13 )
& ( op1(e12,e11) = e10
| op1(e12,e11) = e11
| op1(e12,e11) = e12
| op1(e12,e11) = e13 )
& ( op1(e12,e12) = e10
| op1(e12,e12) = e11
| op1(e12,e12) = e12
| op1(e12,e12) = e13 )
& ( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12
| op1(e12,e13) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e10) = e11
| op1(e13,e10) = e12
| op1(e13,e10) = e13 )
& ( op1(e13,e11) = e10
| op1(e13,e11) = e11
| op1(e13,e11) = e12
| op1(e13,e11) = e13 )
& ( op1(e13,e12) = e10
| op1(e13,e12) = e11
| op1(e13,e12) = e12
| op1(e13,e12) = e13 )
& ( op1(e13,e13) = e10
| op1(e13,e13) = e11
| op1(e13,e13) = e12
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e11) = e10
| op1(e10,e12) = e10
| op1(e10,e13) = e10 )
& ( op1(e10,e10) = e10
| op1(e11,e10) = e10
| op1(e12,e10) = e10
| op1(e13,e10) = e10 )
& ( op1(e10,e10) = e11
| op1(e10,e11) = e11
| op1(e10,e12) = e11
| op1(e10,e13) = e11 )
& ( op1(e10,e10) = e11
| op1(e11,e10) = e11
| op1(e12,e10) = e11
| op1(e13,e10) = e11 )
& ( op1(e10,e10) = e12
| op1(e10,e11) = e12
| op1(e10,e12) = e12
| op1(e10,e13) = e12 )
& ( op1(e10,e10) = e12
| op1(e11,e10) = e12
| op1(e12,e10) = e12
| op1(e13,e10) = e12 )
& ( op1(e10,e10) = e13
| op1(e10,e11) = e13
| op1(e10,e12) = e13
| op1(e10,e13) = e13 )
& ( op1(e10,e10) = e13
| op1(e11,e10) = e13
| op1(e12,e10) = e13
| op1(e13,e10) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e11) = e10
| op1(e11,e12) = e10
| op1(e11,e13) = e10 )
& ( op1(e10,e11) = e10
| op1(e11,e11) = e10
| op1(e12,e11) = e10
| op1(e13,e11) = e10 )
& ( op1(e11,e10) = e11
| op1(e11,e11) = e11
| op1(e11,e12) = e11
| op1(e11,e13) = e11 )
& ( op1(e10,e11) = e11
| op1(e11,e11) = e11
| op1(e12,e11) = e11
| op1(e13,e11) = e11 )
& ( op1(e11,e10) = e12
| op1(e11,e11) = e12
| op1(e11,e12) = e12
| op1(e11,e13) = e12 )
& ( op1(e10,e11) = e12
| op1(e11,e11) = e12
| op1(e12,e11) = e12
| op1(e13,e11) = e12 )
& ( op1(e11,e10) = e13
| op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e11,e13) = e13 )
& ( op1(e10,e11) = e13
| op1(e11,e11) = e13
| op1(e12,e11) = e13
| op1(e13,e11) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e11) = e10
| op1(e12,e12) = e10
| op1(e12,e13) = e10 )
& ( op1(e10,e12) = e10
| op1(e11,e12) = e10
| op1(e12,e12) = e10
| op1(e13,e12) = e10 )
& ( op1(e12,e10) = e11
| op1(e12,e11) = e11
| op1(e12,e12) = e11
| op1(e12,e13) = e11 )
& ( op1(e10,e12) = e11
| op1(e11,e12) = e11
| op1(e12,e12) = e11
| op1(e13,e12) = e11 )
& ( op1(e12,e10) = e12
| op1(e12,e11) = e12
| op1(e12,e12) = e12
| op1(e12,e13) = e12 )
& ( op1(e10,e12) = e12
| op1(e11,e12) = e12
| op1(e12,e12) = e12
| op1(e13,e12) = e12 )
& ( op1(e12,e10) = e13
| op1(e12,e11) = e13
| op1(e12,e12) = e13
| op1(e12,e13) = e13 )
& ( op1(e10,e12) = e13
| op1(e11,e12) = e13
| op1(e12,e12) = e13
| op1(e13,e12) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10 )
& ( op1(e10,e13) = e10
| op1(e11,e13) = e10
| op1(e12,e13) = e10
| op1(e13,e13) = e10 )
& ( op1(e13,e10) = e11
| op1(e13,e11) = e11
| op1(e13,e12) = e11
| op1(e13,e13) = e11 )
& ( op1(e10,e13) = e11
| op1(e11,e13) = e11
| op1(e12,e13) = e11
| op1(e13,e13) = e11 )
& ( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12
| op1(e13,e13) = e12 )
& ( op1(e10,e13) = e12
| op1(e11,e13) = e12
| op1(e12,e13) = e12
| op1(e13,e13) = e12 )
& ( op1(e13,e10) = e13
| op1(e13,e11) = e13
| op1(e13,e12) = e13
| op1(e13,e13) = e13 )
& ( op1(e10,e13) = e13
| op1(e11,e13) = e13
| op1(e12,e13) = e13
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(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/sandbox/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/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op1(e10,e10) != op1(e11,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e12,e10) != op1(e13,e10)
& op1(e10,e11) != op1(e11,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e12,e11) != op1(e13,e11)
& op1(e10,e12) != op1(e11,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e12,e12) != op1(e13,e12)
& op1(e10,e13) != op1(e11,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e12,e13) != op1(e13,e13)
& op1(e10,e10) != op1(e10,e11)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e12) != op1(e10,e13)
& op1(e11,e10) != op1(e11,e11)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e12) != op1(e11,e13)
& op1(e12,e10) != op1(e12,e11)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e12) != op1(e12,e13)
& op1(e13,e10) != op1(e13,e11)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e12) != op1(e13,e13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( op2(e20,e20) != op2(e21,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e22,e20) != op2(e23,e20)
& op2(e20,e21) != op2(e21,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e22,e21) != op2(e23,e21)
& op2(e20,e22) != op2(e21,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e22,e22) != op2(e23,e22)
& op2(e20,e23) != op2(e21,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e22,e23) != op2(e23,e23)
& op2(e20,e20) != op2(e20,e21)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e22) != op2(e20,e23)
& op2(e21,e20) != op2(e21,e21)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e22) != op2(e21,e23)
& op2(e22,e20) != op2(e22,e21)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e22) != op2(e22,e23)
& op2(e23,e20) != op2(e23,e21)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e22) != op2(e23,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f10,axiom,
( ( ( op1(e10,op1(e10,e10)) != op1(e10,e10)
& op1(e11,op1(e10,e11)) != op1(e10,e11)
& op1(e12,op1(e10,e12)) != op1(e10,e12)
& op1(e13,op1(e10,e13)) != op1(e10,e13) )
| ( op1(e10,op1(e11,e10)) != op1(e11,e10)
& op1(e11,op1(e11,e11)) != op1(e11,e11)
& op1(e12,op1(e11,e12)) != op1(e11,e12)
& op1(e13,op1(e11,e13)) != op1(e11,e13) )
| ( op1(e10,op1(e12,e10)) != op1(e12,e10)
& op1(e11,op1(e12,e11)) != op1(e12,e11)
& op1(e12,op1(e12,e12)) != op1(e12,e12)
& op1(e13,op1(e12,e13)) != op1(e12,e13) )
| ( op1(e10,op1(e13,e10)) != op1(e13,e10)
& op1(e11,op1(e13,e11)) != op1(e13,e11)
& op1(e12,op1(e13,e12)) != op1(e13,e12)
& op1(e13,op1(e13,e13)) != op1(e13,e13) ) )
& ( op1(e10,e10) = e10
| op1(e11,e11) = e11
| op1(e12,e12) = e12
| op1(e13,e13) = e13 )
& ( op1(e10,e10) != e10
| op1(e10,e10) = e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) = e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) = e10 )
& ( op1(e10,e10) != e13
| op1(e10,e13) = e10 )
& ( op1(e11,e11) != e10
| op1(e11,e10) = e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) = e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) = e11 )
& ( op1(e11,e11) != e13
| op1(e11,e13) = e11 )
& ( op1(e12,e12) != e10
| op1(e12,e10) = e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) = e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) = e12 )
& ( op1(e12,e12) != e13
| op1(e12,e13) = e12 )
& ( op1(e13,e13) != e10
| op1(e13,e10) = e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) = e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) = e13 )
& ( op1(e13,e13) != e13
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( ( ( op2(e20,op2(e20,e20)) != op2(e20,e20)
& op2(e21,op2(e20,e21)) != op2(e20,e21)
& op2(e22,op2(e20,e22)) != op2(e20,e22)
& op2(e23,op2(e20,e23)) != op2(e20,e23) )
| ( op2(e20,op2(e21,e20)) != op2(e21,e20)
& op2(e21,op2(e21,e21)) != op2(e21,e21)
& op2(e22,op2(e21,e22)) != op2(e21,e22)
& op2(e23,op2(e21,e23)) != op2(e21,e23) )
| ( op2(e20,op2(e22,e20)) != op2(e22,e20)
& op2(e21,op2(e22,e21)) != op2(e22,e21)
& op2(e22,op2(e22,e22)) != op2(e22,e22)
& op2(e23,op2(e22,e23)) != op2(e22,e23) )
| ( op2(e20,op2(e23,e20)) != op2(e23,e20)
& op2(e21,op2(e23,e21)) != op2(e23,e21)
& op2(e22,op2(e23,e22)) != op2(e23,e22)
& op2(e23,op2(e23,e23)) != op2(e23,e23) ) )
& ( op2(e20,e20) = e20
| op2(e21,e21) = e21
| op2(e22,e22) = e22
| op2(e23,e23) = e23 )
& ( op2(e20,e20) != e20
| op2(e20,e20) = e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) = e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) = e20 )
& ( op2(e20,e20) != e23
| op2(e20,e23) = e20 )
& ( op2(e21,e21) != e20
| op2(e21,e20) = e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) = e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) = e21 )
& ( op2(e21,e21) != e23
| op2(e21,e23) = e21 )
& ( op2(e22,e22) != e20
| op2(e22,e20) = e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) = e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) = e22 )
& ( op2(e22,e22) != e23
| op2(e22,e23) = e22 )
& ( op2(e23,e23) != e20
| op2(e23,e20) = e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) = e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) = e23 )
& ( op2(e23,e23) != e23
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e10 = op1(op1(e13,e13),op1(e13,e13))
& e11 = op1(e13,e13)
& e12 = op1(e13,op1(op1(e13,e13),op1(e13,e13))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e20 = op2(op2(e23,e23),op2(e23,e23))
& e21 = op2(e23,e23)
& e22 = op2(e23,op2(op2(e23,e23),op2(e23,e23))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( h1(e13) = e20
& h1(e10) = op2(op2(e20,e20),op2(e20,e20))
& h1(e11) = op2(e20,e20)
& h1(e12) = op2(e20,op2(op2(e20,e20),op2(e20,e20))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f16,axiom,
( h3(e13) = e22
& h3(e10) = op2(op2(e22,e22),op2(e22,e22))
& h3(e11) = op2(e22,e22)
& h3(e12) = op2(e22,op2(op2(e22,e22),op2(e22,e22))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
( h4(e13) = e23
& h4(e10) = op2(op2(e23,e23),op2(e23,e23))
& h4(e11) = op2(e23,e23)
& h4(e12) = op2(e23,op2(op2(e23,e23),op2(e23,e23))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f18,conjecture,
( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f19,negated_conjecture,
~ ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f20,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) ) )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) ) )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) ) )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) ) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f21,plain,
( op1(e10,e10) = e13
| op1(e10,e10) = e12
| op1(e10,e10) = e11
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f24,plain,
( e13 = op1(e10,e13)
| e12 = op1(e10,e13)
| e11 = op1(e10,e13)
| e10 = op1(e10,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f31,plain,
( e13 = op1(e12,e12)
| e12 = op1(e12,e12)
| e11 = op1(e12,e12)
| e10 = op1(e12,e12) ),
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(f39,plain,
( e11 = op1(e10,e13)
| e11 = op1(e10,e12)
| e11 = op1(e10,e11)
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[],[f2]) ).
fof(f41,plain,
( e12 = op1(e10,e13)
| e12 = op1(e10,e12)
| e12 = op1(e10,e11)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f2]) ).
fof(f42,plain,
( e12 = op1(e13,e10)
| e12 = op1(e12,e10)
| e12 = op1(e11,e10)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f2]) ).
fof(f43,plain,
( e13 = op1(e10,e13)
| e13 = op1(e10,e12)
| e13 = op1(e10,e11)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f2]) ).
fof(f44,plain,
( e13 = op1(e13,e10)
| e13 = op1(e12,e10)
| e13 = op1(e11,e10)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f2]) ).
fof(f48,plain,
( e11 = op1(e13,e11)
| e11 = op1(e12,e11)
| e11 = op1(e11,e11)
| e11 = op1(e10,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f49,plain,
( e12 = op1(e11,e13)
| e12 = op1(e11,e12)
| e12 = op1(e11,e11)
| e12 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f50,plain,
( e12 = op1(e13,e11)
| e12 = op1(e12,e11)
| e12 = op1(e11,e11)
| e12 = op1(e10,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f51,plain,
( e13 = op1(e11,e13)
| e13 = op1(e11,e12)
| e13 = op1(e11,e11)
| e13 = 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(f59,plain,
( e13 = op1(e12,e13)
| e13 = op1(e12,e12)
| e13 = op1(e12,e11)
| e13 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f60,plain,
( e13 = op1(e13,e12)
| e13 = op1(e12,e12)
| e13 = op1(e11,e12)
| e13 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f61,plain,
( e10 = op1(e13,e13)
| e10 = op1(e13,e12)
| e10 = op1(e13,e11)
| e10 = op1(e13,e10) ),
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(f66,plain,
( e12 = op1(e13,e13)
| e12 = op1(e12,e13)
| e12 = op1(e11,e13)
| e12 = op1(e10,e13) ),
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(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(f90,plain,
( e22 = op2(e23,e20)
| e22 = op2(e22,e20)
| e22 = op2(e21,e20)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f4]) ).
fof(f92,plain,
( e23 = op2(e23,e20)
| e23 = op2(e22,e20)
| e23 = op2(e21,e20)
| op2(e20,e20) = e23 ),
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(f99,plain,
( e23 = op2(e21,e23)
| e23 = op2(e21,e22)
| e23 = op2(e21,e21)
| e23 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f103,plain,
( e21 = op2(e22,e23)
| e21 = op2(e22,e22)
| e21 = op2(e22,e21)
| e21 = op2(e22,e20) ),
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(f107,plain,
( e23 = op2(e22,e23)
| e23 = op2(e22,e22)
| e23 = op2(e22,e21)
| e23 = op2(e22,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f108,plain,
( e23 = op2(e23,e22)
| e23 = op2(e22,e22)
| e23 = op2(e21,e22)
| e23 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f109,plain,
( e20 = op2(e23,e23)
| e20 = op2(e23,e22)
| e20 = op2(e23,e21)
| e20 = op2(e23,e20) ),
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(f113,plain,
( e22 = op2(e23,e23)
| e22 = op2(e23,e22)
| e22 = op2(e23,e21)
| e22 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f116,plain,
( e23 = op2(e23,e23)
| e23 = op2(e22,e23)
| e23 = op2(e21,e23)
| e23 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f133,plain,
op1(e11,e10) != op1(e11,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f138,plain,
op1(e10,e10) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f141,plain,
op1(e12,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f145,plain,
op1(e10,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f146,plain,
op1(e10,e13) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(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(f157,plain,
op1(e10,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f161,plain,
op1(e11,e10) != op1(e12,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(f170,plain,
op2(e23,e20) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f177,plain,
op2(e21,e22) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f178,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f182,plain,
op2(e21,e20) != op2(e21,e21),
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(f195,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f201,plain,
op2(e22,e21) != op2(e23,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(f210,plain,
op2(e20,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f211,plain,
op2(e20,e20) != op2(e22,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(f221,plain,
e21 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f223,plain,
e20 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f242,plain,
( op1(e10,e12) != op1(e12,op1(e10,e12))
| ~ sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f244,plain,
( op1(e10,e10) != op1(e10,op1(e10,e10))
| ~ sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f246,plain,
( op1(e11,e12) != op1(e12,op1(e11,e12))
| ~ sP0 ),
inference(cnf_transformation,[],[f10]) ).
fof(f248,plain,
( op1(e11,e10) != op1(e10,op1(e11,e10))
| ~ sP0 ),
inference(cnf_transformation,[],[f10]) ).
fof(f252,plain,
( op1(e13,e10) != op1(e10,op1(e13,e10))
| op1(e12,e10) != op1(e10,op1(e12,e10))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f255,plain,
( op1(e13,e11) != op1(e11,op1(e13,e11))
| op1(e12,e11) != op1(e11,op1(e12,e11))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f258,plain,
( op1(e13,e12) != op1(e12,op1(e13,e12))
| op1(e12,e12) != op1(e12,op1(e12,e12))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f265,plain,
( e13 = op1(e13,e13)
| e12 = op1(e12,e12)
| e11 = op1(e11,e11)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f10]) ).
fof(f267,plain,
( e10 = op1(e10,e12)
| op1(e10,e10) != e12 ),
inference(cnf_transformation,[],[f10]) ).
fof(f268,plain,
( e10 = op1(e10,e13)
| op1(e10,e10) != e13 ),
inference(cnf_transformation,[],[f10]) ).
fof(f269,plain,
( e11 = op1(e11,e10)
| e10 != op1(e11,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f272,plain,
( e12 = op1(e12,e10)
| e10 != op1(e12,e12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f273,plain,
( e12 = op1(e12,e11)
| e11 != op1(e12,e12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f274,plain,
( e12 = op1(e12,e13)
| e13 != op1(e12,e12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f276,plain,
( e13 = op1(e13,e11)
| e11 != op1(e13,e13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f279,plain,
( op2(e20,e22) != op2(e22,op2(e20,e22))
| ~ sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f281,plain,
( op2(e20,e20) != op2(e20,op2(e20,e20))
| ~ sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f283,plain,
( op2(e21,e22) != op2(e22,op2(e21,e22))
| ~ sP2 ),
inference(cnf_transformation,[],[f11]) ).
fof(f285,plain,
( op2(e21,e20) != op2(e20,op2(e21,e20))
| ~ sP2 ),
inference(cnf_transformation,[],[f11]) ).
fof(f289,plain,
( op2(e23,e20) != op2(e20,op2(e23,e20))
| op2(e22,e20) != op2(e20,op2(e22,e20))
| sP2
| sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f291,plain,
( op2(e23,e21) != op2(e21,op2(e23,e21))
| op2(e22,e22) != op2(e22,op2(e22,e22))
| sP2
| sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f292,plain,
( op2(e23,e21) != op2(e21,op2(e23,e21))
| op2(e22,e21) != op2(e21,op2(e22,e21))
| sP2
| sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f295,plain,
( op2(e23,e22) != op2(e22,op2(e23,e22))
| op2(e22,e22) != op2(e22,op2(e22,e22))
| sP2
| sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f302,plain,
( e23 = op2(e23,e23)
| e22 = op2(e22,e22)
| e21 = op2(e21,e21)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f11]) ).
fof(f305,plain,
( e20 = op2(e20,e23)
| op2(e20,e20) != e23 ),
inference(cnf_transformation,[],[f11]) ).
fof(f306,plain,
( e21 = op2(e21,e20)
| e20 != op2(e21,e21) ),
inference(cnf_transformation,[],[f11]) ).
fof(f308,plain,
( e21 = op2(e21,e23)
| e23 != op2(e21,e21) ),
inference(cnf_transformation,[],[f11]) ).
fof(f312,plain,
( e23 = op2(e23,e20)
| e20 != op2(e23,e23) ),
inference(cnf_transformation,[],[f11]) ).
fof(f313,plain,
( e23 = op2(e23,e21)
| e21 != op2(e23,e23) ),
inference(cnf_transformation,[],[f11]) ).
fof(f316,plain,
e11 = op1(e13,e13),
inference(cnf_transformation,[],[f12]) ).
fof(f317,plain,
e10 = op1(op1(e13,e13),op1(e13,e13)),
inference(cnf_transformation,[],[f12]) ).
fof(f319,plain,
e21 = op2(e23,e23),
inference(cnf_transformation,[],[f13]) ).
fof(f320,plain,
e20 = op2(op2(e23,e23),op2(e23,e23)),
inference(cnf_transformation,[],[f13]) ).
fof(f324,plain,
e20 = h1(e13),
inference(cnf_transformation,[],[f14]) ).
fof(f332,plain,
e22 = h3(e13),
inference(cnf_transformation,[],[f16]) ).
fof(f333,plain,
op2(e23,op2(op2(e23,e23),op2(e23,e23))) = h4(e12),
inference(cnf_transformation,[],[f17]) ).
fof(f334,plain,
op2(e23,e23) = h4(e11),
inference(cnf_transformation,[],[f17]) ).
fof(f335,plain,
op2(op2(e23,e23),op2(e23,e23)) = h4(e10),
inference(cnf_transformation,[],[f17]) ).
fof(f336,plain,
e23 = h4(e13),
inference(cnf_transformation,[],[f17]) ).
fof(f364,plain,
( e20 != h4(e10)
| ~ sP5 ),
inference(cnf_transformation,[],[f20]) ).
fof(f367,plain,
( e21 != h4(e11)
| ~ sP4 ),
inference(cnf_transformation,[],[f20]) ).
fof(f430,plain,
( e23 != h4(e13)
| e22 != h4(e12)
| sP4
| sP5
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e10)) != op2(h4(e10),h4(e10)) ),
inference(cnf_transformation,[],[f20]) ).
fof(f439,plain,
( op1(e13,e12) != op1(e12,op1(e13,e12))
| op1(e12,e12) != op1(e12,op1(e12,e12))
| sP0
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f258]) ).
fof(f442,plain,
( op1(e13,e11) != op1(e11,op1(e13,e11))
| op1(e12,e11) != op1(e11,op1(e12,e11))
| sP0
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f255]) ).
fof(f445,plain,
( op1(e13,e10) != op1(e10,op1(e13,e10))
| op1(e12,e10) != op1(e10,op1(e12,e10))
| sP0
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f252]) ).
fof(f449,plain,
( op1(e10,e10) != op1(e10,op1(e10,e10))
| sP1 ),
inference(consistent_polarity_flipping,[],[f244]) ).
fof(f451,plain,
( op1(e10,e12) != op1(e12,op1(e10,e12))
| sP1 ),
inference(consistent_polarity_flipping,[],[f242]) ).
fof(f459,plain,
( op2(e23,e22) != op2(e22,op2(e23,e22))
| op2(e22,e22) != op2(e22,op2(e22,e22))
| ~ sP2
| ~ sP3 ),
inference(consistent_polarity_flipping,[],[f295]) ).
fof(f462,plain,
( op2(e23,e21) != op2(e21,op2(e23,e21))
| op2(e22,e21) != op2(e21,op2(e22,e21))
| ~ sP2
| ~ sP3 ),
inference(consistent_polarity_flipping,[],[f292]) ).
fof(f463,plain,
( op2(e23,e21) != op2(e21,op2(e23,e21))
| op2(e22,e22) != op2(e22,op2(e22,e22))
| ~ sP2
| ~ sP3 ),
inference(consistent_polarity_flipping,[],[f291]) ).
fof(f465,plain,
( op2(e23,e20) != op2(e20,op2(e23,e20))
| op2(e22,e20) != op2(e20,op2(e22,e20))
| ~ sP2
| ~ sP3 ),
inference(consistent_polarity_flipping,[],[f289]) ).
fof(f469,plain,
( op2(e21,e20) != op2(e20,op2(e21,e20))
| sP2 ),
inference(consistent_polarity_flipping,[],[f285]) ).
fof(f471,plain,
( op2(e21,e22) != op2(e22,op2(e21,e22))
| sP2 ),
inference(consistent_polarity_flipping,[],[f283]) ).
fof(f473,plain,
( op2(e20,e20) != op2(e20,op2(e20,e20))
| sP3 ),
inference(consistent_polarity_flipping,[],[f281]) ).
fof(f475,plain,
( op2(e20,e22) != op2(e22,op2(e20,e22))
| sP3 ),
inference(consistent_polarity_flipping,[],[f279]) ).
fof(f479,plain,
( e23 != h4(e13)
| e22 != h4(e12)
| ~ sP4
| ~ sP5
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e10)) != op2(h4(e10),h4(e10)) ),
inference(consistent_polarity_flipping,[],[f430]) ).
fof(f542,plain,
( e21 != h4(e11)
| sP4 ),
inference(consistent_polarity_flipping,[],[f367]) ).
fof(f545,plain,
( e20 != h4(e10)
| sP5 ),
inference(consistent_polarity_flipping,[],[f364]) ).
fof(f570,definition,
( spl12_2
<=> e20 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition]) ).
fof(f571,plain,
( e20 = h1(e13)
| ~ spl12_2 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f594,definition,
( spl12_7
<=> e21 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl12_7])],[avatar_definition]) ).
fof(f595,plain,
( e21 = h1(e13)
| ~ spl12_7 ),
inference(avatar_component_clause,[],[f594]) ).
fof(f596,plain,
( e21 != h1(e13)
| spl12_7 ),
inference(avatar_component_clause,[],[f594]) ).
fof(f690,definition,
( spl12_27
<=> e21 = h3(e13) ),
introduced(definition,[new_symbols(definition,[spl12_27])],[avatar_definition]) ).
fof(f691,plain,
( e21 = h3(e13)
| ~ spl12_27 ),
inference(avatar_component_clause,[],[f690]) ).
fof(f692,plain,
( e21 != h3(e13)
| spl12_27 ),
inference(avatar_component_clause,[],[f690]) ).
fof(f710,definition,
( spl12_31
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl12_31])],[avatar_definition]) ).
fof(f714,definition,
( spl12_32
<=> e20 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl12_32])],[avatar_definition]) ).
fof(f715,plain,
( e20 = h4(e13)
| ~ spl12_32 ),
inference(avatar_component_clause,[],[f714]) ).
fof(f716,plain,
( e20 != h4(e13)
| spl12_32 ),
inference(avatar_component_clause,[],[f714]) ).
fof(f729,definition,
( spl12_35
<=> e20 = h4(e10) ),
introduced(definition,[new_symbols(definition,[spl12_35])],[avatar_definition]) ).
fof(f730,plain,
( e20 = h4(e10)
| ~ spl12_35 ),
inference(avatar_component_clause,[],[f729]) ).
fof(f732,plain,
( spl12_31
| ~ spl12_35 ),
inference(avatar_split_clause,[],[f545,f729,f710]) ).
fof(f734,definition,
( spl12_36
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl12_36])],[avatar_definition]) ).
fof(f738,definition,
( spl12_37
<=> e21 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl12_37])],[avatar_definition]) ).
fof(f739,plain,
( e21 = h4(e13)
| ~ spl12_37 ),
inference(avatar_component_clause,[],[f738]) ).
fof(f740,plain,
( e21 != h4(e13)
| spl12_37 ),
inference(avatar_component_clause,[],[f738]) ).
fof(f748,definition,
( spl12_39
<=> e21 = h4(e11) ),
introduced(definition,[new_symbols(definition,[spl12_39])],[avatar_definition]) ).
fof(f749,plain,
( e21 = h4(e11)
| ~ spl12_39 ),
inference(avatar_component_clause,[],[f748]) ).
fof(f751,plain,
( spl12_36
| ~ spl12_39 ),
inference(avatar_split_clause,[],[f542,f748,f734]) ).
fof(f1046,definition,
( spl12_105
<=> e22 = h3(e13) ),
introduced(definition,[new_symbols(definition,[spl12_105])],[avatar_definition]) ).
fof(f1047,plain,
( e22 = h3(e13)
| ~ spl12_105 ),
inference(avatar_component_clause,[],[f1046]) ).
fof(f1094,definition,
( spl12_113
<=> h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_113])],[avatar_definition]) ).
fof(f1096,plain,
( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| spl12_113 ),
inference(avatar_component_clause,[],[f1094]) ).
fof(f1098,definition,
( spl12_114
<=> h4(op1(e10,e11)) = op2(h4(e10),h4(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_114])],[avatar_definition]) ).
fof(f1100,plain,
( h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| spl12_114 ),
inference(avatar_component_clause,[],[f1098]) ).
fof(f1102,definition,
( spl12_115
<=> h4(op1(e10,e12)) = op2(h4(e10),h4(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_115])],[avatar_definition]) ).
fof(f1104,plain,
( h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| spl12_115 ),
inference(avatar_component_clause,[],[f1102]) ).
fof(f1106,definition,
( spl12_116
<=> h4(op1(e10,e13)) = op2(h4(e10),h4(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_116])],[avatar_definition]) ).
fof(f1108,plain,
( h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| spl12_116 ),
inference(avatar_component_clause,[],[f1106]) ).
fof(f1110,definition,
( spl12_117
<=> h4(op1(e11,e10)) = op2(h4(e11),h4(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_117])],[avatar_definition]) ).
fof(f1112,plain,
( h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| spl12_117 ),
inference(avatar_component_clause,[],[f1110]) ).
fof(f1114,definition,
( spl12_118
<=> h4(op1(e11,e11)) = op2(h4(e11),h4(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_118])],[avatar_definition]) ).
fof(f1116,plain,
( h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| spl12_118 ),
inference(avatar_component_clause,[],[f1114]) ).
fof(f1118,definition,
( spl12_119
<=> h4(op1(e11,e12)) = op2(h4(e11),h4(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_119])],[avatar_definition]) ).
fof(f1120,plain,
( h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| spl12_119 ),
inference(avatar_component_clause,[],[f1118]) ).
fof(f1122,definition,
( spl12_120
<=> h4(op1(e11,e13)) = op2(h4(e11),h4(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_120])],[avatar_definition]) ).
fof(f1124,plain,
( h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| spl12_120 ),
inference(avatar_component_clause,[],[f1122]) ).
fof(f1126,definition,
( spl12_121
<=> h4(op1(e12,e10)) = op2(h4(e12),h4(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_121])],[avatar_definition]) ).
fof(f1128,plain,
( h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| spl12_121 ),
inference(avatar_component_clause,[],[f1126]) ).
fof(f1130,definition,
( spl12_122
<=> h4(op1(e12,e11)) = op2(h4(e12),h4(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_122])],[avatar_definition]) ).
fof(f1132,plain,
( h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| spl12_122 ),
inference(avatar_component_clause,[],[f1130]) ).
fof(f1134,definition,
( spl12_123
<=> h4(op1(e12,e12)) = op2(h4(e12),h4(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_123])],[avatar_definition]) ).
fof(f1136,plain,
( h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| spl12_123 ),
inference(avatar_component_clause,[],[f1134]) ).
fof(f1138,definition,
( spl12_124
<=> h4(op1(e12,e13)) = op2(h4(e12),h4(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_124])],[avatar_definition]) ).
fof(f1140,plain,
( h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| spl12_124 ),
inference(avatar_component_clause,[],[f1138]) ).
fof(f1142,definition,
( spl12_125
<=> h4(op1(e13,e10)) = op2(h4(e13),h4(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_125])],[avatar_definition]) ).
fof(f1144,plain,
( h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| spl12_125 ),
inference(avatar_component_clause,[],[f1142]) ).
fof(f1146,definition,
( spl12_126
<=> h4(op1(e13,e11)) = op2(h4(e13),h4(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_126])],[avatar_definition]) ).
fof(f1148,plain,
( h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| spl12_126 ),
inference(avatar_component_clause,[],[f1146]) ).
fof(f1150,definition,
( spl12_127
<=> h4(op1(e13,e12)) = op2(h4(e13),h4(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_127])],[avatar_definition]) ).
fof(f1152,plain,
( h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| spl12_127 ),
inference(avatar_component_clause,[],[f1150]) ).
fof(f1154,definition,
( spl12_128
<=> h4(op1(e13,e13)) = op2(h4(e13),h4(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_128])],[avatar_definition]) ).
fof(f1156,plain,
( h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| spl12_128 ),
inference(avatar_component_clause,[],[f1154]) ).
fof(f1167,definition,
( spl12_131
<=> e22 = h4(e12) ),
introduced(definition,[new_symbols(definition,[spl12_131])],[avatar_definition]) ).
fof(f1168,plain,
( e22 = h4(e12)
| ~ spl12_131 ),
inference(avatar_component_clause,[],[f1167]) ).
fof(f1198,definition,
( spl12_136
<=> e23 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl12_136])],[avatar_definition]) ).
fof(f1199,plain,
( e23 = h4(e13)
| ~ spl12_136 ),
inference(avatar_component_clause,[],[f1198]) ).
fof(f1202,plain,
( ~ spl12_113
| ~ spl12_114
| ~ spl12_115
| ~ spl12_116
| ~ spl12_117
| ~ spl12_118
| ~ spl12_119
| ~ spl12_120
| ~ spl12_121
| ~ spl12_122
| ~ spl12_123
| ~ spl12_124
| ~ spl12_125
| ~ spl12_126
| ~ spl12_127
| ~ spl12_128
| ~ spl12_31
| ~ spl12_36
| ~ spl12_131
| ~ spl12_136 ),
inference(avatar_split_clause,[],[f479,f1198,f1167,f734,f710,f1154,f1150,f1146,f1142,f1138,f1134,f1130,f1126,f1122,f1118,f1114,f1110,f1106,f1102,f1098,f1094]) ).
fof(f1205,plain,
spl12_136,
inference(avatar_split_clause,[],[f336,f1198]) ).
fof(f1206,plain,
spl12_105,
inference(avatar_split_clause,[],[f332,f1046]) ).
fof(f1208,plain,
spl12_2,
inference(avatar_split_clause,[],[f324,f570]) ).
fof(f1210,definition,
( spl12_137
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl12_137])],[avatar_definition]) ).
fof(f1219,definition,
( spl12_139
<=> op2(e20,e22) = op2(e22,op2(e20,e22)) ),
introduced(definition,[new_symbols(definition,[spl12_139])],[avatar_definition]) ).
fof(f1221,plain,
( op2(e20,e22) != op2(e22,op2(e20,e22))
| spl12_139 ),
inference(avatar_component_clause,[],[f1219]) ).
fof(f1222,plain,
( spl12_137
| ~ spl12_139 ),
inference(avatar_split_clause,[],[f475,f1219,f1210]) ).
fof(f1229,definition,
( spl12_141
<=> op2(e20,e20) = op2(e20,op2(e20,e20)) ),
introduced(definition,[new_symbols(definition,[spl12_141])],[avatar_definition]) ).
fof(f1231,plain,
( op2(e20,e20) != op2(e20,op2(e20,e20))
| spl12_141 ),
inference(avatar_component_clause,[],[f1229]) ).
fof(f1232,plain,
( spl12_137
| ~ spl12_141 ),
inference(avatar_split_clause,[],[f473,f1229,f1210]) ).
fof(f1234,definition,
( spl12_142
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl12_142])],[avatar_definition]) ).
fof(f1243,definition,
( spl12_144
<=> op2(e21,e22) = op2(e22,op2(e21,e22)) ),
introduced(definition,[new_symbols(definition,[spl12_144])],[avatar_definition]) ).
fof(f1245,plain,
( op2(e21,e22) != op2(e22,op2(e21,e22))
| spl12_144 ),
inference(avatar_component_clause,[],[f1243]) ).
fof(f1246,plain,
( spl12_142
| ~ spl12_144 ),
inference(avatar_split_clause,[],[f471,f1243,f1234]) ).
fof(f1253,definition,
( spl12_146
<=> op2(e21,e20) = op2(e20,op2(e21,e20)) ),
introduced(definition,[new_symbols(definition,[spl12_146])],[avatar_definition]) ).
fof(f1255,plain,
( op2(e21,e20) != op2(e20,op2(e21,e20))
| spl12_146 ),
inference(avatar_component_clause,[],[f1253]) ).
fof(f1256,plain,
( spl12_142
| ~ spl12_146 ),
inference(avatar_split_clause,[],[f469,f1253,f1234]) ).
fof(f1262,definition,
( spl12_148
<=> op2(e23,e20) = op2(e20,op2(e23,e20)) ),
introduced(definition,[new_symbols(definition,[spl12_148])],[avatar_definition]) ).
fof(f1264,plain,
( op2(e23,e20) != op2(e20,op2(e23,e20))
| spl12_148 ),
inference(avatar_component_clause,[],[f1262]) ).
fof(f1267,definition,
( spl12_149
<=> op2(e22,e22) = op2(e22,op2(e22,e22)) ),
introduced(definition,[new_symbols(definition,[spl12_149])],[avatar_definition]) ).
fof(f1269,plain,
( op2(e22,e22) != op2(e22,op2(e22,e22))
| spl12_149 ),
inference(avatar_component_clause,[],[f1267]) ).
fof(f1272,definition,
( spl12_150
<=> op2(e22,e21) = op2(e21,op2(e22,e21)) ),
introduced(definition,[new_symbols(definition,[spl12_150])],[avatar_definition]) ).
fof(f1274,plain,
( op2(e22,e21) != op2(e21,op2(e22,e21))
| spl12_150 ),
inference(avatar_component_clause,[],[f1272]) ).
fof(f1277,definition,
( spl12_151
<=> op2(e22,e20) = op2(e20,op2(e22,e20)) ),
introduced(definition,[new_symbols(definition,[spl12_151])],[avatar_definition]) ).
fof(f1279,plain,
( op2(e22,e20) != op2(e20,op2(e22,e20))
| spl12_151 ),
inference(avatar_component_clause,[],[f1277]) ).
fof(f1280,plain,
( ~ spl12_137
| ~ spl12_142
| ~ spl12_151
| ~ spl12_148 ),
inference(avatar_split_clause,[],[f465,f1262,f1277,f1234,f1210]) ).
fof(f1282,definition,
( spl12_152
<=> op2(e23,e21) = op2(e21,op2(e23,e21)) ),
introduced(definition,[new_symbols(definition,[spl12_152])],[avatar_definition]) ).
fof(f1284,plain,
( op2(e23,e21) != op2(e21,op2(e23,e21))
| spl12_152 ),
inference(avatar_component_clause,[],[f1282]) ).
fof(f1286,plain,
( ~ spl12_137
| ~ spl12_142
| ~ spl12_149
| ~ spl12_152 ),
inference(avatar_split_clause,[],[f463,f1282,f1267,f1234,f1210]) ).
fof(f1287,plain,
( ~ spl12_137
| ~ spl12_142
| ~ spl12_150
| ~ spl12_152 ),
inference(avatar_split_clause,[],[f462,f1282,f1272,f1234,f1210]) ).
fof(f1290,definition,
( spl12_153
<=> op2(e23,e22) = op2(e22,op2(e23,e22)) ),
introduced(definition,[new_symbols(definition,[spl12_153])],[avatar_definition]) ).
fof(f1292,plain,
( op2(e23,e22) != op2(e22,op2(e23,e22))
| spl12_153 ),
inference(avatar_component_clause,[],[f1290]) ).
fof(f1294,plain,
( ~ spl12_137
| ~ spl12_142
| ~ spl12_149
| ~ spl12_153 ),
inference(avatar_split_clause,[],[f459,f1290,f1267,f1234,f1210]) ).
fof(f1306,definition,
( spl12_155
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl12_155])],[avatar_definition]) ).
fof(f1308,plain,
( e20 = op2(e20,e20)
| ~ spl12_155 ),
inference(avatar_component_clause,[],[f1306]) ).
fof(f1310,definition,
( spl12_156
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_156])],[avatar_definition]) ).
fof(f1312,plain,
( e21 = op2(e21,e21)
| ~ spl12_156 ),
inference(avatar_component_clause,[],[f1310]) ).
fof(f1314,definition,
( spl12_157
<=> e22 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_157])],[avatar_definition]) ).
fof(f1316,plain,
( e22 = op2(e22,e22)
| ~ spl12_157 ),
inference(avatar_component_clause,[],[f1314]) ).
fof(f1318,definition,
( spl12_158
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_158])],[avatar_definition]) ).
fof(f1320,plain,
( e23 = op2(e23,e23)
| ~ spl12_158 ),
inference(avatar_component_clause,[],[f1318]) ).
fof(f1321,plain,
( spl12_155
| spl12_156
| spl12_157
| spl12_158 ),
inference(avatar_split_clause,[],[f302,f1318,f1314,f1310,f1306]) ).
fof(f1323,definition,
( spl12_159
<=> op2(e20,e20) = e21 ),
introduced(definition,[new_symbols(definition,[spl12_159])],[avatar_definition]) ).
fof(f1325,plain,
( op2(e20,e20) != e21
| spl12_159 ),
inference(avatar_component_clause,[],[f1323]) ).
fof(f1327,definition,
( spl12_160
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_160])],[avatar_definition]) ).
fof(f1328,plain,
( e20 != op2(e20,e21)
| spl12_160 ),
inference(avatar_component_clause,[],[f1327]) ).
fof(f1332,definition,
( spl12_161
<=> op2(e20,e20) = e22 ),
introduced(definition,[new_symbols(definition,[spl12_161])],[avatar_definition]) ).
fof(f1333,plain,
( op2(e20,e20) = e22
| ~ spl12_161 ),
inference(avatar_component_clause,[],[f1332]) ).
fof(f1341,definition,
( spl12_163
<=> op2(e20,e20) = e23 ),
introduced(definition,[new_symbols(definition,[spl12_163])],[avatar_definition]) ).
fof(f1345,definition,
( spl12_164
<=> e20 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_164])],[avatar_definition]) ).
fof(f1348,plain,
( ~ spl12_163
| spl12_164 ),
inference(avatar_split_clause,[],[f305,f1345,f1341]) ).
fof(f1350,definition,
( spl12_165
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_165])],[avatar_definition]) ).
fof(f1351,plain,
( e20 = op2(e21,e21)
| ~ spl12_165 ),
inference(avatar_component_clause,[],[f1350]) ).
fof(f1354,definition,
( spl12_166
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_166])],[avatar_definition]) ).
fof(f1356,plain,
( e21 = op2(e21,e20)
| ~ spl12_166 ),
inference(avatar_component_clause,[],[f1354]) ).
fof(f1357,plain,
( ~ spl12_165
| spl12_166 ),
inference(avatar_split_clause,[],[f306,f1354,f1350]) ).
fof(f1359,definition,
( spl12_167
<=> e22 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_167])],[avatar_definition]) ).
fof(f1360,plain,
( e22 = op2(e21,e21)
| ~ spl12_167 ),
inference(avatar_component_clause,[],[f1359]) ).
fof(f1363,definition,
( spl12_168
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_168])],[avatar_definition]) ).
fof(f1365,plain,
( e21 = op2(e21,e22)
| ~ spl12_168 ),
inference(avatar_component_clause,[],[f1363]) ).
fof(f1368,definition,
( spl12_169
<=> e23 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_169])],[avatar_definition]) ).
fof(f1372,definition,
( spl12_170
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_170])],[avatar_definition]) ).
fof(f1375,plain,
( ~ spl12_169
| spl12_170 ),
inference(avatar_split_clause,[],[f308,f1372,f1368]) ).
fof(f1381,definition,
( spl12_172
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_172])],[avatar_definition]) ).
fof(f1383,plain,
( e22 = op2(e22,e20)
| ~ spl12_172 ),
inference(avatar_component_clause,[],[f1381]) ).
fof(f1386,definition,
( spl12_173
<=> e21 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_173])],[avatar_definition]) ).
fof(f1387,plain,
( e21 = op2(e22,e22)
| ~ spl12_173 ),
inference(avatar_component_clause,[],[f1386]) ).
fof(f1390,definition,
( spl12_174
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_174])],[avatar_definition]) ).
fof(f1392,plain,
( e22 = op2(e22,e21)
| ~ spl12_174 ),
inference(avatar_component_clause,[],[f1390]) ).
fof(f1395,definition,
( spl12_175
<=> e23 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_175])],[avatar_definition]) ).
fof(f1396,plain,
( e23 = op2(e22,e22)
| ~ spl12_175 ),
inference(avatar_component_clause,[],[f1395]) ).
fof(f1399,definition,
( spl12_176
<=> e22 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_176])],[avatar_definition]) ).
fof(f1401,plain,
( e22 = op2(e22,e23)
| ~ spl12_176 ),
inference(avatar_component_clause,[],[f1399]) ).
fof(f1404,definition,
( spl12_177
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_177])],[avatar_definition]) ).
fof(f1408,definition,
( spl12_178
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_178])],[avatar_definition]) ).
fof(f1411,plain,
( ~ spl12_177
| spl12_178 ),
inference(avatar_split_clause,[],[f312,f1408,f1404]) ).
fof(f1413,definition,
( spl12_179
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_179])],[avatar_definition]) ).
fof(f1414,plain,
( e21 = op2(e23,e23)
| ~ spl12_179 ),
inference(avatar_component_clause,[],[f1413]) ).
fof(f1417,definition,
( spl12_180
<=> e23 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_180])],[avatar_definition]) ).
fof(f1419,plain,
( e23 = op2(e23,e21)
| ~ spl12_180 ),
inference(avatar_component_clause,[],[f1417]) ).
fof(f1420,plain,
( ~ spl12_179
| spl12_180 ),
inference(avatar_split_clause,[],[f313,f1417,f1413]) ).
fof(f1422,definition,
( spl12_181
<=> e22 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_181])],[avatar_definition]) ).
fof(f1423,plain,
( e22 = op2(e23,e23)
| ~ spl12_181 ),
inference(avatar_component_clause,[],[f1422]) ).
fof(f1426,definition,
( spl12_182
<=> e23 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_182])],[avatar_definition]) ).
fof(f1428,plain,
( e23 = op2(e23,e22)
| ~ spl12_182 ),
inference(avatar_component_clause,[],[f1426]) ).
fof(f1431,definition,
( spl12_183
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl12_183])],[avatar_definition]) ).
fof(f1440,definition,
( spl12_185
<=> op1(e10,e12) = op1(e12,op1(e10,e12)) ),
introduced(definition,[new_symbols(definition,[spl12_185])],[avatar_definition]) ).
fof(f1442,plain,
( op1(e10,e12) != op1(e12,op1(e10,e12))
| spl12_185 ),
inference(avatar_component_clause,[],[f1440]) ).
fof(f1443,plain,
( spl12_183
| ~ spl12_185 ),
inference(avatar_split_clause,[],[f451,f1440,f1431]) ).
fof(f1450,definition,
( spl12_187
<=> op1(e10,e10) = op1(e10,op1(e10,e10)) ),
introduced(definition,[new_symbols(definition,[spl12_187])],[avatar_definition]) ).
fof(f1452,plain,
( op1(e10,e10) != op1(e10,op1(e10,e10))
| spl12_187 ),
inference(avatar_component_clause,[],[f1450]) ).
fof(f1453,plain,
( spl12_183
| ~ spl12_187 ),
inference(avatar_split_clause,[],[f449,f1450,f1431]) ).
fof(f1455,definition,
( spl12_188
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl12_188])],[avatar_definition]) ).
fof(f1464,definition,
( spl12_190
<=> op1(e11,e12) = op1(e12,op1(e11,e12)) ),
introduced(definition,[new_symbols(definition,[spl12_190])],[avatar_definition]) ).
fof(f1466,plain,
( op1(e11,e12) != op1(e12,op1(e11,e12))
| spl12_190 ),
inference(avatar_component_clause,[],[f1464]) ).
fof(f1467,plain,
( ~ spl12_188
| ~ spl12_190 ),
inference(avatar_split_clause,[],[f246,f1464,f1455]) ).
fof(f1474,definition,
( spl12_192
<=> op1(e11,e10) = op1(e10,op1(e11,e10)) ),
introduced(definition,[new_symbols(definition,[spl12_192])],[avatar_definition]) ).
fof(f1476,plain,
( op1(e11,e10) != op1(e10,op1(e11,e10))
| spl12_192 ),
inference(avatar_component_clause,[],[f1474]) ).
fof(f1477,plain,
( ~ spl12_188
| ~ spl12_192 ),
inference(avatar_split_clause,[],[f248,f1474,f1455]) ).
fof(f1483,definition,
( spl12_194
<=> op1(e13,e10) = op1(e10,op1(e13,e10)) ),
introduced(definition,[new_symbols(definition,[spl12_194])],[avatar_definition]) ).
fof(f1485,plain,
( op1(e13,e10) != op1(e10,op1(e13,e10))
| spl12_194 ),
inference(avatar_component_clause,[],[f1483]) ).
fof(f1488,definition,
( spl12_195
<=> op1(e12,e12) = op1(e12,op1(e12,e12)) ),
introduced(definition,[new_symbols(definition,[spl12_195])],[avatar_definition]) ).
fof(f1490,plain,
( op1(e12,e12) != op1(e12,op1(e12,e12))
| spl12_195 ),
inference(avatar_component_clause,[],[f1488]) ).
fof(f1493,definition,
( spl12_196
<=> op1(e12,e11) = op1(e11,op1(e12,e11)) ),
introduced(definition,[new_symbols(definition,[spl12_196])],[avatar_definition]) ).
fof(f1495,plain,
( op1(e12,e11) != op1(e11,op1(e12,e11))
| spl12_196 ),
inference(avatar_component_clause,[],[f1493]) ).
fof(f1498,definition,
( spl12_197
<=> op1(e12,e10) = op1(e10,op1(e12,e10)) ),
introduced(definition,[new_symbols(definition,[spl12_197])],[avatar_definition]) ).
fof(f1500,plain,
( op1(e12,e10) != op1(e10,op1(e12,e10))
| spl12_197 ),
inference(avatar_component_clause,[],[f1498]) ).
fof(f1501,plain,
( ~ spl12_183
| spl12_188
| ~ spl12_197
| ~ spl12_194 ),
inference(avatar_split_clause,[],[f445,f1483,f1498,f1455,f1431]) ).
fof(f1503,definition,
( spl12_198
<=> op1(e13,e11) = op1(e11,op1(e13,e11)) ),
introduced(definition,[new_symbols(definition,[spl12_198])],[avatar_definition]) ).
fof(f1505,plain,
( op1(e13,e11) != op1(e11,op1(e13,e11))
| spl12_198 ),
inference(avatar_component_clause,[],[f1503]) ).
fof(f1508,plain,
( ~ spl12_183
| spl12_188
| ~ spl12_196
| ~ spl12_198 ),
inference(avatar_split_clause,[],[f442,f1503,f1493,f1455,f1431]) ).
fof(f1511,definition,
( spl12_199
<=> op1(e13,e12) = op1(e12,op1(e13,e12)) ),
introduced(definition,[new_symbols(definition,[spl12_199])],[avatar_definition]) ).
fof(f1513,plain,
( op1(e13,e12) != op1(e12,op1(e13,e12))
| spl12_199 ),
inference(avatar_component_clause,[],[f1511]) ).
fof(f1515,plain,
( ~ spl12_183
| spl12_188
| ~ spl12_195
| ~ spl12_199 ),
inference(avatar_split_clause,[],[f439,f1511,f1488,f1455,f1431]) ).
fof(f1527,definition,
( spl12_201
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl12_201])],[avatar_definition]) ).
fof(f1529,plain,
( e10 = op1(e10,e10)
| ~ spl12_201 ),
inference(avatar_component_clause,[],[f1527]) ).
fof(f1531,definition,
( spl12_202
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_202])],[avatar_definition]) ).
fof(f1533,plain,
( e11 = op1(e11,e11)
| ~ spl12_202 ),
inference(avatar_component_clause,[],[f1531]) ).
fof(f1535,definition,
( spl12_203
<=> e12 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_203])],[avatar_definition]) ).
fof(f1537,plain,
( e12 = op1(e12,e12)
| ~ spl12_203 ),
inference(avatar_component_clause,[],[f1535]) ).
fof(f1539,definition,
( spl12_204
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_204])],[avatar_definition]) ).
fof(f1541,plain,
( e13 = op1(e13,e13)
| ~ spl12_204 ),
inference(avatar_component_clause,[],[f1539]) ).
fof(f1542,plain,
( spl12_201
| spl12_202
| spl12_203
| spl12_204 ),
inference(avatar_split_clause,[],[f265,f1539,f1535,f1531,f1527]) ).
fof(f1544,definition,
( spl12_205
<=> op1(e10,e10) = e11 ),
introduced(definition,[new_symbols(definition,[spl12_205])],[avatar_definition]) ).
fof(f1548,definition,
( spl12_206
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_206])],[avatar_definition]) ).
fof(f1550,plain,
( e10 = op1(e10,e11)
| ~ spl12_206 ),
inference(avatar_component_clause,[],[f1548]) ).
fof(f1553,definition,
( spl12_207
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[spl12_207])],[avatar_definition]) ).
fof(f1554,plain,
( op1(e10,e10) = e12
| ~ spl12_207 ),
inference(avatar_component_clause,[],[f1553]) ).
fof(f1557,definition,
( spl12_208
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_208])],[avatar_definition]) ).
fof(f1559,plain,
( e10 = op1(e10,e12)
| ~ spl12_208 ),
inference(avatar_component_clause,[],[f1557]) ).
fof(f1560,plain,
( ~ spl12_207
| spl12_208 ),
inference(avatar_split_clause,[],[f267,f1557,f1553]) ).
fof(f1562,definition,
( spl12_209
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl12_209])],[avatar_definition]) ).
fof(f1563,plain,
( op1(e10,e10) = e13
| ~ spl12_209 ),
inference(avatar_component_clause,[],[f1562]) ).
fof(f1566,definition,
( spl12_210
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_210])],[avatar_definition]) ).
fof(f1568,plain,
( e10 = op1(e10,e13)
| ~ spl12_210 ),
inference(avatar_component_clause,[],[f1566]) ).
fof(f1569,plain,
( ~ spl12_209
| spl12_210 ),
inference(avatar_split_clause,[],[f268,f1566,f1562]) ).
fof(f1571,definition,
( spl12_211
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_211])],[avatar_definition]) ).
fof(f1572,plain,
( e10 = op1(e11,e11)
| ~ spl12_211 ),
inference(avatar_component_clause,[],[f1571]) ).
fof(f1575,definition,
( spl12_212
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl12_212])],[avatar_definition]) ).
fof(f1577,plain,
( e11 = op1(e11,e10)
| ~ spl12_212 ),
inference(avatar_component_clause,[],[f1575]) ).
fof(f1578,plain,
( ~ spl12_211
| spl12_212 ),
inference(avatar_split_clause,[],[f269,f1575,f1571]) ).
fof(f1580,definition,
( spl12_213
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_213])],[avatar_definition]) ).
fof(f1581,plain,
( e12 = op1(e11,e11)
| ~ spl12_213 ),
inference(avatar_component_clause,[],[f1580]) ).
fof(f1584,definition,
( spl12_214
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_214])],[avatar_definition]) ).
fof(f1589,definition,
( spl12_215
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_215])],[avatar_definition]) ).
fof(f1590,plain,
( e13 = op1(e11,e11)
| ~ spl12_215 ),
inference(avatar_component_clause,[],[f1589]) ).
fof(f1598,definition,
( spl12_217
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_217])],[avatar_definition]) ).
fof(f1599,plain,
( e10 = op1(e12,e12)
| ~ spl12_217 ),
inference(avatar_component_clause,[],[f1598]) ).
fof(f1602,definition,
( spl12_218
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_218])],[avatar_definition]) ).
fof(f1604,plain,
( e12 = op1(e12,e10)
| ~ spl12_218 ),
inference(avatar_component_clause,[],[f1602]) ).
fof(f1605,plain,
( ~ spl12_217
| spl12_218 ),
inference(avatar_split_clause,[],[f272,f1602,f1598]) ).
fof(f1607,definition,
( spl12_219
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_219])],[avatar_definition]) ).
fof(f1608,plain,
( e11 = op1(e12,e12)
| ~ spl12_219 ),
inference(avatar_component_clause,[],[f1607]) ).
fof(f1611,definition,
( spl12_220
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_220])],[avatar_definition]) ).
fof(f1613,plain,
( e12 = op1(e12,e11)
| ~ spl12_220 ),
inference(avatar_component_clause,[],[f1611]) ).
fof(f1614,plain,
( ~ spl12_219
| spl12_220 ),
inference(avatar_split_clause,[],[f273,f1611,f1607]) ).
fof(f1616,definition,
( spl12_221
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_221])],[avatar_definition]) ).
fof(f1617,plain,
( e13 = op1(e12,e12)
| ~ spl12_221 ),
inference(avatar_component_clause,[],[f1616]) ).
fof(f1620,definition,
( spl12_222
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_222])],[avatar_definition]) ).
fof(f1622,plain,
( e12 = op1(e12,e13)
| ~ spl12_222 ),
inference(avatar_component_clause,[],[f1620]) ).
fof(f1623,plain,
( ~ spl12_221
| spl12_222 ),
inference(avatar_split_clause,[],[f274,f1620,f1616]) ).
fof(f1625,definition,
( spl12_223
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_223])],[avatar_definition]) ).
fof(f1626,plain,
( e10 = op1(e13,e13)
| ~ spl12_223 ),
inference(avatar_component_clause,[],[f1625]) ).
fof(f1629,definition,
( spl12_224
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_224])],[avatar_definition]) ).
fof(f1631,plain,
( e13 = op1(e13,e10)
| ~ spl12_224 ),
inference(avatar_component_clause,[],[f1629]) ).
fof(f1634,definition,
( spl12_225
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_225])],[avatar_definition]) ).
fof(f1635,plain,
( e11 = op1(e13,e13)
| ~ spl12_225 ),
inference(avatar_component_clause,[],[f1634]) ).
fof(f1638,definition,
( spl12_226
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_226])],[avatar_definition]) ).
fof(f1640,plain,
( e13 = op1(e13,e11)
| ~ spl12_226 ),
inference(avatar_component_clause,[],[f1638]) ).
fof(f1641,plain,
( ~ spl12_225
| spl12_226 ),
inference(avatar_split_clause,[],[f276,f1638,f1634]) ).
fof(f1643,definition,
( spl12_227
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_227])],[avatar_definition]) ).
fof(f1644,plain,
( e12 = op1(e13,e13)
| ~ spl12_227 ),
inference(avatar_component_clause,[],[f1643]) ).
fof(f1647,definition,
( spl12_228
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_228])],[avatar_definition]) ).
fof(f1649,plain,
( e13 = op1(e13,e12)
| ~ spl12_228 ),
inference(avatar_component_clause,[],[f1647]) ).
fof(f1653,definition,
( spl12_229
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_229])],[avatar_definition]) ).
fof(f1657,definition,
( spl12_230
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_230])],[avatar_definition]) ).
fof(f1659,plain,
( e20 = op2(e22,e20)
| ~ spl12_230 ),
inference(avatar_component_clause,[],[f1657]) ).
fof(f1661,definition,
( spl12_231
<=> e20 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_231])],[avatar_definition]) ).
fof(f1663,plain,
( e20 = op2(e23,e20)
| ~ spl12_231 ),
inference(avatar_component_clause,[],[f1661]) ).
fof(f1664,plain,
( spl12_155
| spl12_229
| spl12_230
| spl12_231 ),
inference(avatar_split_clause,[],[f86,f1661,f1657,f1653,f1306]) ).
fof(f1666,definition,
( spl12_232
<=> e21 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_232])],[avatar_definition]) ).
fof(f1668,plain,
( e21 = op2(e20,e21)
| ~ spl12_232 ),
inference(avatar_component_clause,[],[f1666]) ).
fof(f1670,definition,
( spl12_233
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_233])],[avatar_definition]) ).
fof(f1672,plain,
( e21 = op2(e20,e22)
| ~ spl12_233 ),
inference(avatar_component_clause,[],[f1670]) ).
fof(f1674,definition,
( spl12_234
<=> e21 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_234])],[avatar_definition]) ).
fof(f1677,plain,
( spl12_159
| spl12_232
| spl12_233
| spl12_234 ),
inference(avatar_split_clause,[],[f87,f1674,f1670,f1666,f1323]) ).
fof(f1679,definition,
( spl12_235
<=> e21 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_235])],[avatar_definition]) ).
fof(f1681,plain,
( e21 = op2(e22,e20)
| ~ spl12_235 ),
inference(avatar_component_clause,[],[f1679]) ).
fof(f1688,definition,
( spl12_237
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_237])],[avatar_definition]) ).
fof(f1690,plain,
( e22 = op2(e20,e21)
| ~ spl12_237 ),
inference(avatar_component_clause,[],[f1688]) ).
fof(f1692,definition,
( spl12_238
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_238])],[avatar_definition]) ).
fof(f1701,definition,
( spl12_240
<=> e22 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_240])],[avatar_definition]) ).
fof(f1703,plain,
( e22 = op2(e21,e20)
| ~ spl12_240 ),
inference(avatar_component_clause,[],[f1701]) ).
fof(f1705,definition,
( spl12_241
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_241])],[avatar_definition]) ).
fof(f1707,plain,
( e22 = op2(e23,e20)
| ~ spl12_241 ),
inference(avatar_component_clause,[],[f1705]) ).
fof(f1708,plain,
( spl12_161
| spl12_240
| spl12_172
| spl12_241 ),
inference(avatar_split_clause,[],[f90,f1705,f1381,f1701,f1332]) ).
fof(f1710,definition,
( spl12_242
<=> e23 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_242])],[avatar_definition]) ).
fof(f1714,definition,
( spl12_243
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_243])],[avatar_definition]) ).
fof(f1716,plain,
( e23 = op2(e20,e22)
| ~ spl12_243 ),
inference(avatar_component_clause,[],[f1714]) ).
fof(f1718,definition,
( spl12_244
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_244])],[avatar_definition]) ).
fof(f1720,plain,
( e23 = op2(e20,e23)
| ~ spl12_244 ),
inference(avatar_component_clause,[],[f1718]) ).
fof(f1723,definition,
( spl12_245
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_245])],[avatar_definition]) ).
fof(f1725,plain,
( e23 = op2(e21,e20)
| ~ spl12_245 ),
inference(avatar_component_clause,[],[f1723]) ).
fof(f1727,definition,
( spl12_246
<=> e23 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_246])],[avatar_definition]) ).
fof(f1729,plain,
( e23 = op2(e22,e20)
| ~ spl12_246 ),
inference(avatar_component_clause,[],[f1727]) ).
fof(f1730,plain,
( spl12_163
| spl12_245
| spl12_246
| spl12_178 ),
inference(avatar_split_clause,[],[f92,f1408,f1727,f1723,f1341]) ).
fof(f1736,definition,
( spl12_248
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_248])],[avatar_definition]) ).
fof(f1745,definition,
( spl12_250
<=> e20 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_250])],[avatar_definition]) ).
fof(f1747,plain,
( e20 = op2(e23,e21)
| ~ spl12_250 ),
inference(avatar_component_clause,[],[f1745]) ).
fof(f1751,definition,
( spl12_251
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_251])],[avatar_definition]) ).
fof(f1753,plain,
( e21 = op2(e22,e21)
| ~ spl12_251 ),
inference(avatar_component_clause,[],[f1751]) ).
fof(f1755,definition,
( spl12_252
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_252])],[avatar_definition]) ).
fof(f1757,plain,
( e21 = op2(e23,e21)
| ~ spl12_252 ),
inference(avatar_component_clause,[],[f1755]) ).
fof(f1758,plain,
( spl12_232
| spl12_156
| spl12_251
| spl12_252 ),
inference(avatar_split_clause,[],[f96,f1755,f1751,f1310,f1666]) ).
fof(f1760,definition,
( spl12_253
<=> e22 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_253])],[avatar_definition]) ).
fof(f1762,plain,
( e22 = op2(e21,e22)
| ~ spl12_253 ),
inference(avatar_component_clause,[],[f1760]) ).
fof(f1764,definition,
( spl12_254
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_254])],[avatar_definition]) ).
fof(f1766,plain,
( e22 = op2(e21,e23)
| ~ spl12_254 ),
inference(avatar_component_clause,[],[f1764]) ).
fof(f1767,plain,
( spl12_240
| spl12_167
| spl12_253
| spl12_254 ),
inference(avatar_split_clause,[],[f97,f1764,f1760,f1359,f1701]) ).
fof(f1769,definition,
( spl12_255
<=> e22 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_255])],[avatar_definition]) ).
fof(f1771,plain,
( e22 = op2(e23,e21)
| ~ spl12_255 ),
inference(avatar_component_clause,[],[f1769]) ).
fof(f1772,plain,
( spl12_237
| spl12_167
| spl12_174
| spl12_255 ),
inference(avatar_split_clause,[],[f98,f1769,f1390,f1359,f1688]) ).
fof(f1774,definition,
( spl12_256
<=> e23 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_256])],[avatar_definition]) ).
fof(f1776,plain,
( e23 = op2(e21,e22)
| ~ spl12_256 ),
inference(avatar_component_clause,[],[f1774]) ).
fof(f1778,definition,
( spl12_257
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_257])],[avatar_definition]) ).
fof(f1780,plain,
( e23 = op2(e21,e23)
| ~ spl12_257 ),
inference(avatar_component_clause,[],[f1778]) ).
fof(f1781,plain,
( spl12_245
| spl12_169
| spl12_256
| spl12_257 ),
inference(avatar_split_clause,[],[f99,f1778,f1774,f1368,f1723]) ).
fof(f1783,definition,
( spl12_258
<=> e23 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_258])],[avatar_definition]) ).
fof(f1788,definition,
( spl12_259
<=> e20 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_259])],[avatar_definition]) ).
fof(f1790,plain,
( e20 = op2(e22,e23)
| ~ spl12_259 ),
inference(avatar_component_clause,[],[f1788]) ).
fof(f1793,definition,
( spl12_260
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_260])],[avatar_definition]) ).
fof(f1795,plain,
( e20 = op2(e23,e22)
| ~ spl12_260 ),
inference(avatar_component_clause,[],[f1793]) ).
fof(f1798,definition,
( spl12_261
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_261])],[avatar_definition]) ).
fof(f1801,plain,
( spl12_235
| spl12_251
| spl12_173
| spl12_261 ),
inference(avatar_split_clause,[],[f103,f1798,f1386,f1751,f1679]) ).
fof(f1803,definition,
( spl12_262
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_262])],[avatar_definition]) ).
fof(f1806,plain,
( spl12_233
| spl12_168
| spl12_173
| spl12_262 ),
inference(avatar_split_clause,[],[f104,f1803,f1386,f1363,f1670]) ).
fof(f1807,plain,
( spl12_172
| spl12_174
| spl12_157
| spl12_176 ),
inference(avatar_split_clause,[],[f105,f1399,f1314,f1390,f1381]) ).
fof(f1809,definition,
( spl12_263
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_263])],[avatar_definition]) ).
fof(f1811,plain,
( e22 = op2(e23,e22)
| ~ spl12_263 ),
inference(avatar_component_clause,[],[f1809]) ).
fof(f1812,plain,
( spl12_238
| spl12_253
| spl12_157
| spl12_263 ),
inference(avatar_split_clause,[],[f106,f1809,f1314,f1760,f1692]) ).
fof(f1814,definition,
( spl12_264
<=> e23 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_264])],[avatar_definition]) ).
fof(f1816,plain,
( e23 = op2(e22,e23)
| ~ spl12_264 ),
inference(avatar_component_clause,[],[f1814]) ).
fof(f1817,plain,
( spl12_246
| spl12_258
| spl12_175
| spl12_264 ),
inference(avatar_split_clause,[],[f107,f1814,f1395,f1783,f1727]) ).
fof(f1818,plain,
( spl12_243
| spl12_256
| spl12_175
| spl12_182 ),
inference(avatar_split_clause,[],[f108,f1426,f1395,f1774,f1714]) ).
fof(f1819,plain,
( spl12_231
| spl12_250
| spl12_260
| spl12_177 ),
inference(avatar_split_clause,[],[f109,f1404,f1793,f1745,f1661]) ).
fof(f1820,plain,
( spl12_164
| spl12_248
| spl12_259
| spl12_177 ),
inference(avatar_split_clause,[],[f110,f1404,f1788,f1736,f1345]) ).
fof(f1823,plain,
( spl12_241
| spl12_255
| spl12_263
| spl12_181 ),
inference(avatar_split_clause,[],[f113,f1422,f1809,f1769,f1705]) ).
fof(f1826,plain,
( spl12_244
| spl12_257
| spl12_264
| spl12_158 ),
inference(avatar_split_clause,[],[f116,f1318,f1814,f1778,f1718]) ).
fof(f1827,plain,
( spl12_155
| spl12_159
| spl12_161
| spl12_163 ),
inference(avatar_split_clause,[],[f69,f1341,f1332,f1323,f1306]) ).
fof(f1828,plain,
( spl12_160
| spl12_232
| spl12_237
| spl12_242 ),
inference(avatar_split_clause,[],[f70,f1710,f1688,f1666,f1327]) ).
fof(f1834,plain,
( spl12_248
| spl12_170
| spl12_254
| spl12_257 ),
inference(avatar_split_clause,[],[f76,f1778,f1764,f1372,f1736]) ).
fof(f1843,plain,
( spl12_201
| spl12_206
| spl12_208
| spl12_210 ),
inference(avatar_split_clause,[],[f37,f1566,f1557,f1548,f1527]) ).
fof(f1849,definition,
( spl12_266
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_266])],[avatar_definition]) ).
fof(f1851,plain,
( e10 = op1(e12,e10)
| ~ spl12_266 ),
inference(avatar_component_clause,[],[f1849]) ).
fof(f1853,definition,
( spl12_267
<=> e10 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_267])],[avatar_definition]) ).
fof(f1855,plain,
( e10 = op1(e13,e10)
| ~ spl12_267 ),
inference(avatar_component_clause,[],[f1853]) ).
fof(f1858,definition,
( spl12_268
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_268])],[avatar_definition]) ).
fof(f1860,plain,
( e11 = op1(e10,e11)
| ~ spl12_268 ),
inference(avatar_component_clause,[],[f1858]) ).
fof(f1862,definition,
( spl12_269
<=> e11 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_269])],[avatar_definition]) ).
fof(f1864,plain,
( e11 = op1(e10,e12)
| ~ spl12_269 ),
inference(avatar_component_clause,[],[f1862]) ).
fof(f1866,definition,
( spl12_270
<=> e11 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_270])],[avatar_definition]) ).
fof(f1868,plain,
( e11 = op1(e10,e13)
| ~ spl12_270 ),
inference(avatar_component_clause,[],[f1866]) ).
fof(f1869,plain,
( spl12_205
| spl12_268
| spl12_269
| spl12_270 ),
inference(avatar_split_clause,[],[f39,f1866,f1862,f1858,f1544]) ).
fof(f1871,definition,
( spl12_271
<=> e11 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_271])],[avatar_definition]) ).
fof(f1880,definition,
( spl12_273
<=> e12 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_273])],[avatar_definition]) ).
fof(f1882,plain,
( e12 = op1(e10,e11)
| ~ spl12_273 ),
inference(avatar_component_clause,[],[f1880]) ).
fof(f1884,definition,
( spl12_274
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_274])],[avatar_definition]) ).
fof(f1886,plain,
( e12 = op1(e10,e12)
| ~ spl12_274 ),
inference(avatar_component_clause,[],[f1884]) ).
fof(f1888,definition,
( spl12_275
<=> e12 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_275])],[avatar_definition]) ).
fof(f1890,plain,
( e12 = op1(e10,e13)
| ~ spl12_275 ),
inference(avatar_component_clause,[],[f1888]) ).
fof(f1891,plain,
( spl12_207
| spl12_273
| spl12_274
| spl12_275 ),
inference(avatar_split_clause,[],[f41,f1888,f1884,f1880,f1553]) ).
fof(f1893,definition,
( spl12_276
<=> e12 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl12_276])],[avatar_definition]) ).
fof(f1895,plain,
( e12 = op1(e11,e10)
| ~ spl12_276 ),
inference(avatar_component_clause,[],[f1893]) ).
fof(f1897,definition,
( spl12_277
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_277])],[avatar_definition]) ).
fof(f1899,plain,
( e12 = op1(e13,e10)
| ~ spl12_277 ),
inference(avatar_component_clause,[],[f1897]) ).
fof(f1900,plain,
( spl12_207
| spl12_276
| spl12_218
| spl12_277 ),
inference(avatar_split_clause,[],[f42,f1897,f1602,f1893,f1553]) ).
fof(f1902,definition,
( spl12_278
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_278])],[avatar_definition]) ).
fof(f1904,plain,
( e13 = op1(e10,e11)
| ~ spl12_278 ),
inference(avatar_component_clause,[],[f1902]) ).
fof(f1906,definition,
( spl12_279
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_279])],[avatar_definition]) ).
fof(f1908,plain,
( e13 = op1(e10,e12)
| ~ spl12_279 ),
inference(avatar_component_clause,[],[f1906]) ).
fof(f1910,definition,
( spl12_280
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_280])],[avatar_definition]) ).
fof(f1912,plain,
( e13 = op1(e10,e13)
| ~ spl12_280 ),
inference(avatar_component_clause,[],[f1910]) ).
fof(f1913,plain,
( spl12_209
| spl12_278
| spl12_279
| spl12_280 ),
inference(avatar_split_clause,[],[f43,f1910,f1906,f1902,f1562]) ).
fof(f1915,definition,
( spl12_281
<=> e13 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl12_281])],[avatar_definition]) ).
fof(f1917,plain,
( e13 = op1(e11,e10)
| ~ spl12_281 ),
inference(avatar_component_clause,[],[f1915]) ).
fof(f1919,definition,
( spl12_282
<=> e13 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_282])],[avatar_definition]) ).
fof(f1921,plain,
( e13 = op1(e12,e10)
| ~ spl12_282 ),
inference(avatar_component_clause,[],[f1919]) ).
fof(f1922,plain,
( spl12_209
| spl12_281
| spl12_282
| spl12_224 ),
inference(avatar_split_clause,[],[f44,f1629,f1919,f1915,f1562]) ).
fof(f1928,definition,
( spl12_284
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_284])],[avatar_definition]) ).
fof(f1930,plain,
( e10 = op1(e11,e13)
| ~ spl12_284 ),
inference(avatar_component_clause,[],[f1928]) ).
fof(f1933,definition,
( spl12_285
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_285])],[avatar_definition]) ).
fof(f1935,plain,
( e10 = op1(e12,e11)
| ~ spl12_285 ),
inference(avatar_component_clause,[],[f1933]) ).
fof(f1937,definition,
( spl12_286
<=> e10 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_286])],[avatar_definition]) ).
fof(f1939,plain,
( e10 = op1(e13,e11)
| ~ spl12_286 ),
inference(avatar_component_clause,[],[f1937]) ).
fof(f1943,definition,
( spl12_287
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_287])],[avatar_definition]) ).
fof(f1945,plain,
( e11 = op1(e12,e11)
| ~ spl12_287 ),
inference(avatar_component_clause,[],[f1943]) ).
fof(f1947,definition,
( spl12_288
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_288])],[avatar_definition]) ).
fof(f1949,plain,
( e11 = op1(e13,e11)
| ~ spl12_288 ),
inference(avatar_component_clause,[],[f1947]) ).
fof(f1950,plain,
( spl12_268
| spl12_202
| spl12_287
| spl12_288 ),
inference(avatar_split_clause,[],[f48,f1947,f1943,f1531,f1858]) ).
fof(f1952,definition,
( spl12_289
<=> e12 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_289])],[avatar_definition]) ).
fof(f1954,plain,
( e12 = op1(e11,e12)
| ~ spl12_289 ),
inference(avatar_component_clause,[],[f1952]) ).
fof(f1956,definition,
( spl12_290
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_290])],[avatar_definition]) ).
fof(f1958,plain,
( e12 = op1(e11,e13)
| ~ spl12_290 ),
inference(avatar_component_clause,[],[f1956]) ).
fof(f1959,plain,
( spl12_276
| spl12_213
| spl12_289
| spl12_290 ),
inference(avatar_split_clause,[],[f49,f1956,f1952,f1580,f1893]) ).
fof(f1961,definition,
( spl12_291
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_291])],[avatar_definition]) ).
fof(f1963,plain,
( e12 = op1(e13,e11)
| ~ spl12_291 ),
inference(avatar_component_clause,[],[f1961]) ).
fof(f1964,plain,
( spl12_273
| spl12_213
| spl12_220
| spl12_291 ),
inference(avatar_split_clause,[],[f50,f1961,f1611,f1580,f1880]) ).
fof(f1966,definition,
( spl12_292
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_292])],[avatar_definition]) ).
fof(f1968,plain,
( e13 = op1(e11,e12)
| ~ spl12_292 ),
inference(avatar_component_clause,[],[f1966]) ).
fof(f1970,definition,
( spl12_293
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_293])],[avatar_definition]) ).
fof(f1972,plain,
( e13 = op1(e11,e13)
| ~ spl12_293 ),
inference(avatar_component_clause,[],[f1970]) ).
fof(f1973,plain,
( spl12_281
| spl12_215
| spl12_292
| spl12_293 ),
inference(avatar_split_clause,[],[f51,f1970,f1966,f1589,f1915]) ).
fof(f1975,definition,
( spl12_294
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_294])],[avatar_definition]) ).
fof(f1980,definition,
( spl12_295
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_295])],[avatar_definition]) ).
fof(f1982,plain,
( e10 = op1(e12,e13)
| ~ spl12_295 ),
inference(avatar_component_clause,[],[f1980]) ).
fof(f1983,plain,
( spl12_266
| spl12_285
| spl12_217
| spl12_295 ),
inference(avatar_split_clause,[],[f53,f1980,f1598,f1933,f1849]) ).
fof(f1985,definition,
( spl12_296
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_296])],[avatar_definition]) ).
fof(f1987,plain,
( e10 = op1(e13,e12)
| ~ spl12_296 ),
inference(avatar_component_clause,[],[f1985]) ).
fof(f1990,definition,
( spl12_297
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_297])],[avatar_definition]) ).
fof(f1993,plain,
( spl12_271
| spl12_287
| spl12_219
| spl12_297 ),
inference(avatar_split_clause,[],[f55,f1990,f1607,f1943,f1871]) ).
fof(f1995,definition,
( spl12_298
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_298])],[avatar_definition]) ).
fof(f1997,plain,
( e11 = op1(e13,e12)
| ~ spl12_298 ),
inference(avatar_component_clause,[],[f1995]) ).
fof(f1998,plain,
( spl12_269
| spl12_214
| spl12_219
| spl12_298 ),
inference(avatar_split_clause,[],[f56,f1995,f1607,f1584,f1862]) ).
fof(f1999,plain,
( spl12_218
| spl12_220
| spl12_203
| spl12_222 ),
inference(avatar_split_clause,[],[f57,f1620,f1535,f1611,f1602]) ).
fof(f2006,definition,
( spl12_300
<=> e13 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_300])],[avatar_definition]) ).
fof(f2008,plain,
( e13 = op1(e12,e13)
| ~ spl12_300 ),
inference(avatar_component_clause,[],[f2006]) ).
fof(f2009,plain,
( spl12_282
| spl12_294
| spl12_221
| spl12_300 ),
inference(avatar_split_clause,[],[f59,f2006,f1616,f1975,f1919]) ).
fof(f2010,plain,
( spl12_279
| spl12_292
| spl12_221
| spl12_228 ),
inference(avatar_split_clause,[],[f60,f1647,f1616,f1966,f1906]) ).
fof(f2011,plain,
( spl12_267
| spl12_286
| spl12_296
| spl12_223 ),
inference(avatar_split_clause,[],[f61,f1625,f1985,f1937,f1853]) ).
fof(f2012,plain,
( spl12_210
| spl12_284
| spl12_295
| spl12_223 ),
inference(avatar_split_clause,[],[f62,f1625,f1980,f1928,f1566]) ).
fof(f2016,plain,
( spl12_275
| spl12_290
| spl12_222
| spl12_227 ),
inference(avatar_split_clause,[],[f66,f1643,f1620,f1956,f1888]) ).
fof(f2018,plain,
( spl12_280
| spl12_293
| spl12_300
| spl12_204 ),
inference(avatar_split_clause,[],[f68,f1539,f2006,f1970,f1910]) ).
fof(f2019,plain,
( spl12_201
| spl12_205
| spl12_207
| spl12_209 ),
inference(avatar_split_clause,[],[f21,f1562,f1553,f1544,f1527]) ).
fof(f2022,plain,
( spl12_210
| spl12_270
| spl12_275
| spl12_280 ),
inference(avatar_split_clause,[],[f24,f1910,f1888,f1866,f1566]) ).
fof(f2029,plain,
( spl12_217
| spl12_219
| spl12_203
| spl12_221 ),
inference(avatar_split_clause,[],[f31,f1616,f1535,f1607,f1598]) ).
fof(f2035,plain,
( e20 != e21
| ~ spl12_2
| spl12_7 ),
inference(forward_demodulation,[],[f596,f571]) ).
fof(f2039,plain,
spl12_225,
inference(avatar_split_clause,[],[f316,f1634]) ).
fof(f2040,plain,
spl12_179,
inference(avatar_split_clause,[],[f319,f1413]) ).
fof(f2052,plain,
( e21 = e22
| ~ spl12_27
| ~ spl12_105 ),
inference(forward_demodulation,[],[f691,f1047]) ).
fof(f2062,plain,
( $false
| ~ spl12_27
| ~ spl12_105 ),
inference(forward_subsumption_resolution,[],[f221,f2052]) ).
fof(f2063,plain,
( ~ spl12_27
| ~ spl12_105 ),
inference(avatar_contradiction_clause,[],[f2062]) ).
fof(f2064,plain,
( e21 != e22
| spl12_27
| ~ spl12_105 ),
inference(forward_demodulation,[],[f692,f1047]) ).
fof(f2069,plain,
( e20 = e21
| ~ spl12_2
| ~ spl12_7 ),
inference(forward_demodulation,[],[f595,f571]) ).
fof(f2082,plain,
( e20 = e22
| ~ spl12_155
| ~ spl12_161 ),
inference(forward_demodulation,[],[f1308,f1333]) ).
fof(f2085,plain,
( $false
| ~ spl12_155
| ~ spl12_161 ),
inference(forward_subsumption_resolution,[],[f2082,f223]) ).
fof(f2086,plain,
( ~ spl12_155
| ~ spl12_161 ),
inference(avatar_contradiction_clause,[],[f2085]) ).
fof(f2094,plain,
( e20 = op2(e20,e20)
| ~ spl12_2
| ~ spl12_7
| ~ spl12_232 ),
inference(forward_demodulation,[],[f1668,f2069]) ).
fof(f2100,plain,
( op2(e20,e20) = e22
| ~ spl12_2
| ~ spl12_7
| ~ spl12_237 ),
inference(forward_demodulation,[],[f1690,f2069]) ).
fof(f2101,plain,
( e20 != op2(e20,e20)
| ~ spl12_2
| ~ spl12_7
| spl12_159 ),
inference(forward_demodulation,[],[f1325,f2069]) ).
fof(f2104,plain,
( spl12_155
| ~ spl12_2
| ~ spl12_7
| ~ spl12_232 ),
inference(avatar_split_clause,[],[f2094,f1666,f594,f570,f1306]) ).
fof(f2105,plain,
( spl12_161
| ~ spl12_2
| ~ spl12_7
| ~ spl12_237 ),
inference(avatar_split_clause,[],[f2100,f1688,f594,f570,f1332]) ).
fof(f2106,plain,
( ~ spl12_155
| ~ spl12_2
| ~ spl12_7
| spl12_159 ),
inference(avatar_split_clause,[],[f2101,f1323,f594,f570,f1306]) ).
fof(f2112,plain,
( e20 = e22
| ~ spl12_165
| ~ spl12_167 ),
inference(superposition,[],[f1360,f1351]) ).
fof(f2117,plain,
( $false
| ~ spl12_165
| ~ spl12_167 ),
inference(forward_subsumption_resolution,[],[f2112,f223]) ).
fof(f2118,plain,
( ~ spl12_165
| ~ spl12_167 ),
inference(avatar_contradiction_clause,[],[f2117]) ).
fof(f2128,plain,
( e20 = e23
| ~ spl12_32
| ~ spl12_136 ),
inference(forward_demodulation,[],[f715,f1199]) ).
fof(f2136,plain,
( e23 != op2(e23,e21)
| ~ spl12_32
| ~ spl12_136
| spl12_160 ),
inference(superposition,[],[f1328,f2128]) ).
fof(f2145,plain,
( ~ spl12_180
| ~ spl12_32
| ~ spl12_136
| spl12_160 ),
inference(avatar_split_clause,[],[f2136,f1327,f1198,f714,f1417]) ).
fof(f2149,plain,
( e20 != e23
| spl12_32
| ~ spl12_136 ),
inference(forward_demodulation,[],[f716,f1199]) ).
fof(f2155,plain,
( e21 = e22
| ~ spl12_157
| ~ spl12_173 ),
inference(forward_demodulation,[],[f1387,f1316]) ).
fof(f2156,plain,
( $false
| spl12_27
| ~ spl12_105
| ~ spl12_157
| ~ spl12_173 ),
inference(forward_subsumption_resolution,[],[f2155,f2064]) ).
fof(f2157,plain,
( spl12_27
| ~ spl12_105
| ~ spl12_157
| ~ spl12_173 ),
inference(avatar_contradiction_clause,[],[f2156]) ).
fof(f2173,plain,
( e21 = e23
| ~ spl12_37
| ~ spl12_136 ),
inference(forward_demodulation,[],[f739,f1199]) ).
fof(f2181,plain,
( e23 = op2(e23,e20)
| ~ spl12_37
| ~ spl12_136
| ~ spl12_166 ),
inference(superposition,[],[f1356,f2173]) ).
fof(f2194,plain,
( spl12_178
| ~ spl12_37
| ~ spl12_136
| ~ spl12_166 ),
inference(avatar_split_clause,[],[f2181,f1354,f1198,f738,f1408]) ).
fof(f2202,plain,
( e21 != e23
| spl12_37
| ~ spl12_136 ),
inference(forward_demodulation,[],[f740,f1199]) ).
fof(f2207,plain,
( e20 = e21
| ~ spl12_156
| ~ spl12_165 ),
inference(forward_demodulation,[],[f1312,f1351]) ).
fof(f2208,plain,
( $false
| ~ spl12_2
| spl12_7
| ~ spl12_156
| ~ spl12_165 ),
inference(forward_subsumption_resolution,[],[f2207,f2035]) ).
fof(f2209,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_156
| ~ spl12_165 ),
inference(avatar_contradiction_clause,[],[f2208]) ).
fof(f2211,plain,
( e22 = e23
| ~ spl12_157
| ~ spl12_175 ),
inference(forward_demodulation,[],[f1316,f1396]) ).
fof(f2212,plain,
( $false
| ~ spl12_157
| ~ spl12_175 ),
inference(forward_subsumption_resolution,[],[f2211,f219]) ).
fof(f2213,plain,
( ~ spl12_157
| ~ spl12_175 ),
inference(avatar_contradiction_clause,[],[f2212]) ).
fof(f2227,plain,
( e21 = e22
| ~ spl12_179
| ~ spl12_181 ),
inference(superposition,[],[f1423,f1414]) ).
fof(f2233,plain,
( $false
| spl12_27
| ~ spl12_105
| ~ spl12_179
| ~ spl12_181 ),
inference(forward_subsumption_resolution,[],[f2227,f2064]) ).
fof(f2234,plain,
( spl12_27
| ~ spl12_105
| ~ spl12_179
| ~ spl12_181 ),
inference(avatar_contradiction_clause,[],[f2233]) ).
fof(f2263,plain,
( e10 = e11
| ~ spl12_202
| ~ spl12_211 ),
inference(superposition,[],[f1572,f1533]) ).
fof(f2267,plain,
( $false
| ~ spl12_202
| ~ spl12_211 ),
inference(forward_subsumption_resolution,[],[f2263,f218]) ).
fof(f2268,plain,
( ~ spl12_202
| ~ spl12_211 ),
inference(avatar_contradiction_clause,[],[f2267]) ).
fof(f2270,plain,
( e10 = e12
| ~ spl12_211
| ~ spl12_213 ),
inference(superposition,[],[f1581,f1572]) ).
fof(f2274,plain,
( $false
| ~ spl12_211
| ~ spl12_213 ),
inference(forward_subsumption_resolution,[],[f2270,f217]) ).
fof(f2275,plain,
( ~ spl12_211
| ~ spl12_213 ),
inference(avatar_contradiction_clause,[],[f2274]) ).
fof(f2278,plain,
( e10 = e11
| ~ spl12_208
| ~ spl12_269 ),
inference(forward_demodulation,[],[f1864,f1559]) ).
fof(f2281,plain,
( $false
| ~ spl12_208
| ~ spl12_269 ),
inference(forward_subsumption_resolution,[],[f2278,f218]) ).
fof(f2282,plain,
( ~ spl12_208
| ~ spl12_269 ),
inference(avatar_contradiction_clause,[],[f2281]) ).
fof(f2286,plain,
( e10 = e13
| ~ spl12_211
| ~ spl12_215 ),
inference(superposition,[],[f1590,f1572]) ).
fof(f2292,plain,
( $false
| ~ spl12_211
| ~ spl12_215 ),
inference(forward_subsumption_resolution,[],[f2286,f216]) ).
fof(f2293,plain,
( ~ spl12_211
| ~ spl12_215 ),
inference(avatar_contradiction_clause,[],[f2292]) ).
fof(f2295,plain,
( e10 = e12
| ~ spl12_203
| ~ spl12_217 ),
inference(forward_demodulation,[],[f1599,f1537]) ).
fof(f2296,plain,
( $false
| ~ spl12_203
| ~ spl12_217 ),
inference(forward_subsumption_resolution,[],[f2295,f217]) ).
fof(f2297,plain,
( ~ spl12_203
| ~ spl12_217 ),
inference(avatar_contradiction_clause,[],[f2296]) ).
fof(f2299,plain,
( e10 = e11
| ~ spl12_217
| ~ spl12_219 ),
inference(forward_demodulation,[],[f1608,f1599]) ).
fof(f2300,plain,
( $false
| ~ spl12_217
| ~ spl12_219 ),
inference(forward_subsumption_resolution,[],[f2299,f218]) ).
fof(f2301,plain,
( ~ spl12_217
| ~ spl12_219 ),
inference(avatar_contradiction_clause,[],[f2300]) ).
fof(f2302,plain,
( e10 = e12
| ~ spl12_218
| ~ spl12_266 ),
inference(forward_demodulation,[],[f1851,f1604]) ).
fof(f2303,plain,
( $false
| ~ spl12_218
| ~ spl12_266 ),
inference(forward_subsumption_resolution,[],[f2302,f217]) ).
fof(f2304,plain,
( ~ spl12_218
| ~ spl12_266 ),
inference(avatar_contradiction_clause,[],[f2303]) ).
fof(f2311,plain,
( e11 = e13
| ~ spl12_219
| ~ spl12_221 ),
inference(superposition,[],[f1617,f1608]) ).
fof(f2317,plain,
( $false
| ~ spl12_219
| ~ spl12_221 ),
inference(forward_subsumption_resolution,[],[f2311,f214]) ).
fof(f2318,plain,
( ~ spl12_219
| ~ spl12_221 ),
inference(avatar_contradiction_clause,[],[f2317]) ).
fof(f2324,plain,
( e11 = e13
| ~ spl12_204
| ~ spl12_225 ),
inference(forward_demodulation,[],[f1635,f1541]) ).
fof(f2325,plain,
( $false
| ~ spl12_204
| ~ spl12_225 ),
inference(forward_subsumption_resolution,[],[f2324,f214]) ).
fof(f2326,plain,
( ~ spl12_204
| ~ spl12_225 ),
inference(avatar_contradiction_clause,[],[f2325]) ).
fof(f2327,plain,
( e10 = e13
| ~ spl12_201
| ~ spl12_209 ),
inference(forward_demodulation,[],[f1529,f1563]) ).
fof(f2328,plain,
( $false
| ~ spl12_201
| ~ spl12_209 ),
inference(forward_subsumption_resolution,[],[f2327,f216]) ).
fof(f2329,plain,
( ~ spl12_201
| ~ spl12_209 ),
inference(avatar_contradiction_clause,[],[f2328]) ).
fof(f2331,plain,
( e11 = e12
| ~ spl12_203
| ~ spl12_219 ),
inference(superposition,[],[f1537,f1608]) ).
fof(f2337,plain,
( $false
| ~ spl12_203
| ~ spl12_219 ),
inference(forward_subsumption_resolution,[],[f2331,f215]) ).
fof(f2338,plain,
( ~ spl12_203
| ~ spl12_219 ),
inference(avatar_contradiction_clause,[],[f2337]) ).
fof(f2345,plain,
( e11 = e12
| ~ spl12_225
| ~ spl12_227 ),
inference(superposition,[],[f1644,f1635]) ).
fof(f2351,plain,
( $false
| ~ spl12_225
| ~ spl12_227 ),
inference(forward_subsumption_resolution,[],[f2345,f215]) ).
fof(f2352,plain,
( ~ spl12_225
| ~ spl12_227 ),
inference(avatar_contradiction_clause,[],[f2351]) ).
fof(f2363,plain,
( e20 = e21
| ~ spl12_230
| ~ spl12_235 ),
inference(forward_demodulation,[],[f1681,f1659]) ).
fof(f2364,plain,
( $false
| ~ spl12_2
| spl12_7
| ~ spl12_230
| ~ spl12_235 ),
inference(forward_subsumption_resolution,[],[f2363,f2035]) ).
fof(f2365,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_230
| ~ spl12_235 ),
inference(avatar_contradiction_clause,[],[f2364]) ).
fof(f2367,plain,
( e21 = e23
| ~ spl12_158
| ~ spl12_179 ),
inference(superposition,[],[f1320,f1414]) ).
fof(f2373,plain,
( $false
| spl12_37
| ~ spl12_136
| ~ spl12_158
| ~ spl12_179 ),
inference(forward_subsumption_resolution,[],[f2367,f2202]) ).
fof(f2374,plain,
( spl12_37
| ~ spl12_136
| ~ spl12_158
| ~ spl12_179 ),
inference(avatar_contradiction_clause,[],[f2373]) ).
fof(f2375,plain,
( e21 = e22
| ~ spl12_174
| ~ spl12_251 ),
inference(forward_demodulation,[],[f1753,f1392]) ).
fof(f2376,plain,
( $false
| spl12_27
| ~ spl12_105
| ~ spl12_174
| ~ spl12_251 ),
inference(forward_subsumption_resolution,[],[f2375,f2064]) ).
fof(f2377,plain,
( spl12_27
| ~ spl12_105
| ~ spl12_174
| ~ spl12_251 ),
inference(avatar_contradiction_clause,[],[f2376]) ).
fof(f2382,plain,
( e21 = e22
| ~ spl12_232
| ~ spl12_237 ),
inference(superposition,[],[f1690,f1668]) ).
fof(f2387,plain,
( $false
| spl12_27
| ~ spl12_105
| ~ spl12_232
| ~ spl12_237 ),
inference(forward_subsumption_resolution,[],[f2382,f2064]) ).
fof(f2388,plain,
( spl12_27
| ~ spl12_105
| ~ spl12_232
| ~ spl12_237 ),
inference(avatar_contradiction_clause,[],[f2387]) ).
fof(f2438,plain,
( e21 = e23
| ~ spl12_166
| ~ spl12_245 ),
inference(superposition,[],[f1725,f1356]) ).
fof(f2444,plain,
( $false
| spl12_37
| ~ spl12_136
| ~ spl12_166
| ~ spl12_245 ),
inference(forward_subsumption_resolution,[],[f2438,f2202]) ).
fof(f2445,plain,
( spl12_37
| ~ spl12_136
| ~ spl12_166
| ~ spl12_245 ),
inference(avatar_contradiction_clause,[],[f2444]) ).
fof(f2457,plain,
( e22 = e23
| ~ spl12_180
| ~ spl12_255 ),
inference(forward_demodulation,[],[f1771,f1419]) ).
fof(f2458,plain,
( $false
| ~ spl12_180
| ~ spl12_255 ),
inference(forward_subsumption_resolution,[],[f2457,f219]) ).
fof(f2459,plain,
( ~ spl12_180
| ~ spl12_255 ),
inference(avatar_contradiction_clause,[],[f2458]) ).
fof(f2467,plain,
( e21 = e22
| ~ spl12_166
| ~ spl12_240 ),
inference(superposition,[],[f1703,f1356]) ).
fof(f2473,plain,
( $false
| spl12_27
| ~ spl12_105
| ~ spl12_166
| ~ spl12_240 ),
inference(forward_subsumption_resolution,[],[f2467,f2064]) ).
fof(f2474,plain,
( spl12_27
| ~ spl12_105
| ~ spl12_166
| ~ spl12_240 ),
inference(avatar_contradiction_clause,[],[f2473]) ).
fof(f2484,plain,
( e20 = e23
| ~ spl12_180
| ~ spl12_250 ),
inference(forward_demodulation,[],[f1747,f1419]) ).
fof(f2485,plain,
( $false
| spl12_32
| ~ spl12_136
| ~ spl12_180
| ~ spl12_250 ),
inference(forward_subsumption_resolution,[],[f2484,f2149]) ).
fof(f2486,plain,
( spl12_32
| ~ spl12_136
| ~ spl12_180
| ~ spl12_250 ),
inference(avatar_contradiction_clause,[],[f2485]) ).
fof(f2489,plain,
( e20 = e23
| ~ spl12_182
| ~ spl12_260 ),
inference(forward_demodulation,[],[f1795,f1428]) ).
fof(f2492,plain,
( $false
| spl12_32
| ~ spl12_136
| ~ spl12_182
| ~ spl12_260 ),
inference(forward_subsumption_resolution,[],[f2489,f2149]) ).
fof(f2493,plain,
( spl12_32
| ~ spl12_136
| ~ spl12_182
| ~ spl12_260 ),
inference(avatar_contradiction_clause,[],[f2492]) ).
fof(f2494,plain,
( e20 = e22
| ~ spl12_231
| ~ spl12_241 ),
inference(forward_demodulation,[],[f1663,f1707]) ).
fof(f2499,plain,
( $false
| ~ spl12_231
| ~ spl12_241 ),
inference(forward_subsumption_resolution,[],[f2494,f223]) ).
fof(f2500,plain,
( ~ spl12_231
| ~ spl12_241 ),
inference(avatar_contradiction_clause,[],[f2499]) ).
fof(f2538,plain,
( e21 = e23
| ~ spl12_168
| ~ spl12_256 ),
inference(superposition,[],[f1776,f1365]) ).
fof(f2544,plain,
( $false
| spl12_37
| ~ spl12_136
| ~ spl12_168
| ~ spl12_256 ),
inference(forward_subsumption_resolution,[],[f2538,f2202]) ).
fof(f2545,plain,
( spl12_37
| ~ spl12_136
| ~ spl12_168
| ~ spl12_256 ),
inference(avatar_contradiction_clause,[],[f2544]) ).
fof(f2547,plain,
( e22 = e23
| ~ spl12_254
| ~ spl12_257 ),
inference(superposition,[],[f1780,f1766]) ).
fof(f2551,plain,
( $false
| ~ spl12_254
| ~ spl12_257 ),
inference(forward_subsumption_resolution,[],[f2547,f219]) ).
fof(f2552,plain,
( ~ spl12_254
| ~ spl12_257 ),
inference(avatar_contradiction_clause,[],[f2551]) ).
fof(f2604,plain,
( e21 = e23
| ~ spl12_235
| ~ spl12_246 ),
inference(forward_demodulation,[],[f1681,f1729]) ).
fof(f2606,plain,
( $false
| spl12_37
| ~ spl12_136
| ~ spl12_235
| ~ spl12_246 ),
inference(forward_subsumption_resolution,[],[f2604,f2202]) ).
fof(f2607,plain,
( spl12_37
| ~ spl12_136
| ~ spl12_235
| ~ spl12_246 ),
inference(avatar_contradiction_clause,[],[f2606]) ).
fof(f2659,plain,
( e21 = e23
| ~ spl12_180
| ~ spl12_252 ),
inference(forward_demodulation,[],[f1757,f1419]) ).
fof(f2662,plain,
( $false
| spl12_37
| ~ spl12_136
| ~ spl12_180
| ~ spl12_252 ),
inference(forward_subsumption_resolution,[],[f2659,f2202]) ).
fof(f2663,plain,
( spl12_37
| ~ spl12_136
| ~ spl12_180
| ~ spl12_252 ),
inference(avatar_contradiction_clause,[],[f2662]) ).
fof(f2681,plain,
( e20 = e22
| ~ spl12_176
| ~ spl12_259 ),
inference(forward_demodulation,[],[f1790,f1401]) ).
fof(f2684,plain,
( $false
| ~ spl12_176
| ~ spl12_259 ),
inference(forward_subsumption_resolution,[],[f2681,f223]) ).
fof(f2685,plain,
( ~ spl12_176
| ~ spl12_259 ),
inference(avatar_contradiction_clause,[],[f2684]) ).
fof(f2686,plain,
( e22 = e23
| ~ spl12_172
| ~ spl12_246 ),
inference(forward_demodulation,[],[f1383,f1729]) ).
fof(f2689,plain,
( $false
| ~ spl12_172
| ~ spl12_246 ),
inference(forward_subsumption_resolution,[],[f2686,f219]) ).
fof(f2690,plain,
( ~ spl12_172
| ~ spl12_246 ),
inference(avatar_contradiction_clause,[],[f2689]) ).
fof(f2757,plain,
( e20 = e22
| ~ spl12_260
| ~ spl12_263 ),
inference(superposition,[],[f1811,f1795]) ).
fof(f2762,plain,
( $false
| ~ spl12_260
| ~ spl12_263 ),
inference(forward_subsumption_resolution,[],[f2757,f223]) ).
fof(f2763,plain,
( ~ spl12_260
| ~ spl12_263 ),
inference(avatar_contradiction_clause,[],[f2762]) ).
fof(f2765,plain,
( e20 = e23
| ~ spl12_259
| ~ spl12_264 ),
inference(superposition,[],[f1816,f1790]) ).
fof(f2770,plain,
( $false
| spl12_32
| ~ spl12_136
| ~ spl12_259
| ~ spl12_264 ),
inference(forward_subsumption_resolution,[],[f2765,f2149]) ).
fof(f2771,plain,
( spl12_32
| ~ spl12_136
| ~ spl12_259
| ~ spl12_264 ),
inference(avatar_contradiction_clause,[],[f2770]) ).
fof(f2781,plain,
( e10 = e13
| ~ spl12_224
| ~ spl12_267 ),
inference(forward_demodulation,[],[f1855,f1631]) ).
fof(f2782,plain,
( $false
| ~ spl12_224
| ~ spl12_267 ),
inference(forward_subsumption_resolution,[],[f2781,f216]) ).
fof(f2783,plain,
( ~ spl12_224
| ~ spl12_267 ),
inference(avatar_contradiction_clause,[],[f2782]) ).
fof(f2786,plain,
( e11 = e12
| ~ spl12_268
| ~ spl12_273 ),
inference(superposition,[],[f1882,f1860]) ).
fof(f2791,plain,
( $false
| ~ spl12_268
| ~ spl12_273 ),
inference(forward_subsumption_resolution,[],[f2786,f215]) ).
fof(f2792,plain,
( ~ spl12_268
| ~ spl12_273 ),
inference(avatar_contradiction_clause,[],[f2791]) ).
fof(f2806,plain,
( e10 = e12
| ~ spl12_201
| ~ spl12_207 ),
inference(superposition,[],[f1554,f1529]) ).
fof(f2811,plain,
( $false
| ~ spl12_201
| ~ spl12_207 ),
inference(forward_subsumption_resolution,[],[f2806,f217]) ).
fof(f2812,plain,
( ~ spl12_201
| ~ spl12_207 ),
inference(avatar_contradiction_clause,[],[f2811]) ).
fof(f2813,plain,
( e10 = e13
| ~ spl12_228
| ~ spl12_296 ),
inference(forward_demodulation,[],[f1987,f1649]) ).
fof(f2814,plain,
( $false
| ~ spl12_228
| ~ spl12_296 ),
inference(forward_subsumption_resolution,[],[f2813,f216]) ).
fof(f2815,plain,
( ~ spl12_228
| ~ spl12_296 ),
inference(avatar_contradiction_clause,[],[f2814]) ).
fof(f2820,plain,
( e11 = e12
| ~ spl12_212
| ~ spl12_276 ),
inference(superposition,[],[f1895,f1577]) ).
fof(f2825,plain,
( $false
| ~ spl12_212
| ~ spl12_276 ),
inference(forward_subsumption_resolution,[],[f2820,f215]) ).
fof(f2826,plain,
( ~ spl12_212
| ~ spl12_276 ),
inference(avatar_contradiction_clause,[],[f2825]) ).
fof(f2828,plain,
( e10 = e12
| ~ spl12_267
| ~ spl12_277 ),
inference(superposition,[],[f1899,f1855]) ).
fof(f2833,plain,
( $false
| ~ spl12_267
| ~ spl12_277 ),
inference(forward_subsumption_resolution,[],[f2828,f217]) ).
fof(f2834,plain,
( ~ spl12_267
| ~ spl12_277 ),
inference(avatar_contradiction_clause,[],[f2833]) ).
fof(f2836,plain,
( e11 = e13
| ~ spl12_268
| ~ spl12_278 ),
inference(superposition,[],[f1904,f1860]) ).
fof(f2842,plain,
( $false
| ~ spl12_268
| ~ spl12_278 ),
inference(forward_subsumption_resolution,[],[f2836,f214]) ).
fof(f2843,plain,
( ~ spl12_268
| ~ spl12_278 ),
inference(avatar_contradiction_clause,[],[f2842]) ).
fof(f2846,plain,
( e12 = e13
| ~ spl12_274
| ~ spl12_279 ),
inference(superposition,[],[f1886,f1908]) ).
fof(f2849,plain,
( $false
| ~ spl12_274
| ~ spl12_279 ),
inference(forward_subsumption_resolution,[],[f2846,f213]) ).
fof(f2850,plain,
( ~ spl12_274
| ~ spl12_279 ),
inference(avatar_contradiction_clause,[],[f2849]) ).
fof(f2862,plain,
( e10 = e11
| ~ spl12_223
| ~ spl12_225 ),
inference(superposition,[],[f1626,f1635]) ).
fof(f2868,plain,
( $false
| ~ spl12_223
| ~ spl12_225 ),
inference(forward_subsumption_resolution,[],[f2862,f218]) ).
fof(f2869,plain,
( ~ spl12_223
| ~ spl12_225 ),
inference(avatar_contradiction_clause,[],[f2868]) ).
fof(f2872,plain,
( e12 = e13
| ~ spl12_224
| ~ spl12_277 ),
inference(superposition,[],[f1899,f1631]) ).
fof(f2873,plain,
( $false
| ~ spl12_224
| ~ spl12_277 ),
inference(forward_subsumption_resolution,[],[f2872,f213]) ).
fof(f2874,plain,
( ~ spl12_224
| ~ spl12_277 ),
inference(avatar_contradiction_clause,[],[f2873]) ).
fof(f2878,plain,
( e11 = e13
| ~ spl12_212
| ~ spl12_281 ),
inference(superposition,[],[f1917,f1577]) ).
fof(f2884,plain,
( $false
| ~ spl12_212
| ~ spl12_281 ),
inference(forward_subsumption_resolution,[],[f2878,f214]) ).
fof(f2885,plain,
( ~ spl12_212
| ~ spl12_281 ),
inference(avatar_contradiction_clause,[],[f2884]) ).
fof(f2887,plain,
( e10 = e13
| ~ spl12_266
| ~ spl12_282 ),
inference(superposition,[],[f1921,f1851]) ).
fof(f2892,plain,
( $false
| ~ spl12_266
| ~ spl12_282 ),
inference(forward_subsumption_resolution,[],[f2887,f216]) ).
fof(f2893,plain,
( ~ spl12_266
| ~ spl12_282 ),
inference(avatar_contradiction_clause,[],[f2892]) ).
fof(f2894,plain,
( e10 = e13
| ~ spl12_226
| ~ spl12_286 ),
inference(forward_demodulation,[],[f1939,f1640]) ).
fof(f2895,plain,
( $false
| ~ spl12_226
| ~ spl12_286 ),
inference(forward_subsumption_resolution,[],[f2894,f216]) ).
fof(f2896,plain,
( ~ spl12_226
| ~ spl12_286 ),
inference(avatar_contradiction_clause,[],[f2895]) ).
fof(f2897,plain,
( e11 = e13
| ~ spl12_270
| ~ spl12_280 ),
inference(forward_demodulation,[],[f1868,f1912]) ).
fof(f2899,plain,
( e11 = e13
| ~ spl12_226
| ~ spl12_288 ),
inference(forward_demodulation,[],[f1949,f1640]) ).
fof(f2900,plain,
( $false
| ~ spl12_270
| ~ spl12_280 ),
inference(forward_subsumption_resolution,[],[f2897,f214]) ).
fof(f2901,plain,
( ~ spl12_270
| ~ spl12_280 ),
inference(avatar_contradiction_clause,[],[f2900]) ).
fof(f2902,plain,
( $false
| ~ spl12_226
| ~ spl12_288 ),
inference(forward_subsumption_resolution,[],[f2899,f214]) ).
fof(f2903,plain,
( ~ spl12_226
| ~ spl12_288 ),
inference(avatar_contradiction_clause,[],[f2902]) ).
fof(f2904,plain,
( e11 = e12
| ~ spl12_220
| ~ spl12_287 ),
inference(forward_demodulation,[],[f1945,f1613]) ).
fof(f2906,plain,
( $false
| ~ spl12_220
| ~ spl12_287 ),
inference(forward_subsumption_resolution,[],[f2904,f215]) ).
fof(f2907,plain,
( ~ spl12_220
| ~ spl12_287 ),
inference(avatar_contradiction_clause,[],[f2906]) ).
fof(f2908,plain,
( e12 = e13
| ~ spl12_226
| ~ spl12_291 ),
inference(forward_demodulation,[],[f1963,f1640]) ).
fof(f2909,plain,
( $false
| ~ spl12_226
| ~ spl12_291 ),
inference(forward_subsumption_resolution,[],[f2908,f213]) ).
fof(f2910,plain,
( ~ spl12_226
| ~ spl12_291 ),
inference(avatar_contradiction_clause,[],[f2909]) ).
fof(f2929,plain,
( e10 = e12
| ~ spl12_222
| ~ spl12_295 ),
inference(forward_demodulation,[],[f1982,f1622]) ).
fof(f2930,plain,
( $false
| ~ spl12_222
| ~ spl12_295 ),
inference(forward_subsumption_resolution,[],[f2929,f217]) ).
fof(f2931,plain,
( ~ spl12_222
| ~ spl12_295 ),
inference(avatar_contradiction_clause,[],[f2930]) ).
fof(f2935,plain,
( e10 = e12
| ~ spl12_206
| ~ spl12_273 ),
inference(superposition,[],[f1882,f1550]) ).
fof(f2940,plain,
( $false
| ~ spl12_206
| ~ spl12_273 ),
inference(forward_subsumption_resolution,[],[f2935,f217]) ).
fof(f2941,plain,
( ~ spl12_206
| ~ spl12_273 ),
inference(avatar_contradiction_clause,[],[f2940]) ).
fof(f2949,plain,
( e11 = e12
| ~ spl12_270
| ~ spl12_275 ),
inference(superposition,[],[f1890,f1868]) ).
fof(f2954,plain,
( $false
| ~ spl12_270
| ~ spl12_275 ),
inference(forward_subsumption_resolution,[],[f2949,f215]) ).
fof(f2955,plain,
( ~ spl12_270
| ~ spl12_275 ),
inference(avatar_contradiction_clause,[],[f2954]) ).
fof(f2963,plain,
( e11 = e13
| ~ spl12_269
| ~ spl12_279 ),
inference(superposition,[],[f1908,f1864]) ).
fof(f2969,plain,
( $false
| ~ spl12_269
| ~ spl12_279 ),
inference(forward_subsumption_resolution,[],[f2963,f214]) ).
fof(f2970,plain,
( ~ spl12_269
| ~ spl12_279 ),
inference(avatar_contradiction_clause,[],[f2969]) ).
fof(f2980,plain,
( e12 = e13
| ~ spl12_275
| ~ spl12_280 ),
inference(superposition,[],[f1912,f1890]) ).
fof(f2981,plain,
( e12 = e13
| ~ spl12_275
| ~ spl12_280 ),
inference(superposition,[],[f1890,f1912]) ).
fof(f2983,plain,
( $false
| ~ spl12_275
| ~ spl12_280 ),
inference(forward_subsumption_resolution,[],[f2981,f213]) ).
fof(f2984,plain,
( ~ spl12_275
| ~ spl12_280 ),
inference(avatar_contradiction_clause,[],[f2983]) ).
fof(f2985,plain,
( $false
| ~ spl12_275
| ~ spl12_280 ),
inference(forward_subsumption_resolution,[],[f2980,f213]) ).
fof(f2986,plain,
( ~ spl12_275
| ~ spl12_280 ),
inference(avatar_contradiction_clause,[],[f2985]) ).
fof(f2989,plain,
( e11 = e12
| ~ spl12_269
| ~ spl12_274 ),
inference(superposition,[],[f1886,f1864]) ).
fof(f2995,plain,
( $false
| ~ spl12_269
| ~ spl12_274 ),
inference(forward_subsumption_resolution,[],[f2989,f215]) ).
fof(f2996,plain,
( ~ spl12_269
| ~ spl12_274 ),
inference(avatar_contradiction_clause,[],[f2995]) ).
fof(f3010,plain,
( e10 = e11
| ~ spl12_285
| ~ spl12_287 ),
inference(forward_demodulation,[],[f1945,f1935]) ).
fof(f3011,plain,
( $false
| ~ spl12_285
| ~ spl12_287 ),
inference(forward_subsumption_resolution,[],[f3010,f218]) ).
fof(f3012,plain,
( ~ spl12_285
| ~ spl12_287 ),
inference(avatar_contradiction_clause,[],[f3011]) ).
fof(f3041,plain,
( e10 = e12
| ~ spl12_284
| ~ spl12_290 ),
inference(superposition,[],[f1958,f1930]) ).
fof(f3045,plain,
( $false
| ~ spl12_284
| ~ spl12_290 ),
inference(forward_subsumption_resolution,[],[f3041,f217]) ).
fof(f3046,plain,
( ~ spl12_284
| ~ spl12_290 ),
inference(avatar_contradiction_clause,[],[f3045]) ).
fof(f3067,plain,
( e12 = e13
| ~ spl12_203
| ~ spl12_221 ),
inference(superposition,[],[f1617,f1537]) ).
fof(f3073,plain,
( $false
| ~ spl12_203
| ~ spl12_221 ),
inference(forward_subsumption_resolution,[],[f3067,f213]) ).
fof(f3074,plain,
( ~ spl12_203
| ~ spl12_221 ),
inference(avatar_contradiction_clause,[],[f3073]) ).
fof(f3092,plain,
( e12 = e13
| ~ spl12_273
| ~ spl12_278 ),
inference(superposition,[],[f1904,f1882]) ).
fof(f3098,plain,
( $false
| ~ spl12_273
| ~ spl12_278 ),
inference(forward_subsumption_resolution,[],[f3092,f213]) ).
fof(f3099,plain,
( ~ spl12_273
| ~ spl12_278 ),
inference(avatar_contradiction_clause,[],[f3098]) ).
fof(f3112,plain,
( e12 = e13
| ~ spl12_218
| ~ spl12_282 ),
inference(superposition,[],[f1921,f1604]) ).
fof(f3118,plain,
( $false
| ~ spl12_218
| ~ spl12_282 ),
inference(forward_subsumption_resolution,[],[f3112,f213]) ).
fof(f3119,plain,
( ~ spl12_218
| ~ spl12_282 ),
inference(avatar_contradiction_clause,[],[f3118]) ).
fof(f3127,plain,
( e12 = e13
| ~ spl12_290
| ~ spl12_293 ),
inference(superposition,[],[f1972,f1958]) ).
fof(f3133,plain,
( $false
| ~ spl12_290
| ~ spl12_293 ),
inference(forward_subsumption_resolution,[],[f3127,f213]) ).
fof(f3134,plain,
( ~ spl12_290
| ~ spl12_293 ),
inference(avatar_contradiction_clause,[],[f3133]) ).
fof(f3136,plain,
( e10 = e11
| ~ spl12_210
| ~ spl12_270 ),
inference(superposition,[],[f1568,f1868]) ).
fof(f3142,plain,
( $false
| ~ spl12_210
| ~ spl12_270 ),
inference(forward_subsumption_resolution,[],[f3136,f218]) ).
fof(f3143,plain,
( ~ spl12_210
| ~ spl12_270 ),
inference(avatar_contradiction_clause,[],[f3142]) ).
fof(f3144,plain,
( e10 = e13
| ~ spl12_284
| ~ spl12_293 ),
inference(forward_demodulation,[],[f1930,f1972]) ).
fof(f3145,plain,
( $false
| ~ spl12_284
| ~ spl12_293 ),
inference(forward_subsumption_resolution,[],[f3144,f216]) ).
fof(f3146,plain,
( ~ spl12_284
| ~ spl12_293 ),
inference(avatar_contradiction_clause,[],[f3145]) ).
fof(f3153,plain,
( e12 = e13
| ~ spl12_289
| ~ spl12_292 ),
inference(superposition,[],[f1954,f1968]) ).
fof(f3156,plain,
( $false
| ~ spl12_289
| ~ spl12_292 ),
inference(forward_subsumption_resolution,[],[f3153,f213]) ).
fof(f3157,plain,
( ~ spl12_289
| ~ spl12_292 ),
inference(avatar_contradiction_clause,[],[f3156]) ).
fof(f3164,plain,
( e10 = e11
| ~ spl12_296
| ~ spl12_298 ),
inference(forward_demodulation,[],[f1997,f1987]) ).
fof(f3165,plain,
( $false
| ~ spl12_296
| ~ spl12_298 ),
inference(forward_subsumption_resolution,[],[f3164,f218]) ).
fof(f3166,plain,
( ~ spl12_296
| ~ spl12_298 ),
inference(avatar_contradiction_clause,[],[f3165]) ).
fof(f3197,plain,
( e10 = e12
| ~ spl12_220
| ~ spl12_285 ),
inference(forward_demodulation,[],[f1935,f1613]) ).
fof(f3198,plain,
( $false
| ~ spl12_220
| ~ spl12_285 ),
inference(forward_subsumption_resolution,[],[f3197,f217]) ).
fof(f3199,plain,
( ~ spl12_220
| ~ spl12_285 ),
inference(avatar_contradiction_clause,[],[f3198]) ).
fof(f3279,plain,
( e10 = e13
| ~ spl12_295
| ~ spl12_300 ),
inference(superposition,[],[f2008,f1982]) ).
fof(f3284,plain,
( $false
| ~ spl12_295
| ~ spl12_300 ),
inference(forward_subsumption_resolution,[],[f3279,f216]) ).
fof(f3285,plain,
( ~ spl12_295
| ~ spl12_300 ),
inference(avatar_contradiction_clause,[],[f3284]) ).
fof(f3304,plain,
( e21 = h4(e11)
| ~ spl12_179 ),
inference(forward_demodulation,[],[f334,f1414]) ).
fof(f3307,plain,
( spl12_39
| ~ spl12_179 ),
inference(avatar_split_clause,[],[f3304,f1413,f748]) ).
fof(f3340,plain,
( e11 != op1(e12,e13)
| ~ spl12_225 ),
inference(forward_demodulation,[],[f141,f1635]) ).
fof(f3345,plain,
( e10 != op1(e10,e13)
| ~ spl12_295 ),
inference(forward_demodulation,[],[f145,f1982]) ).
fof(f3346,plain,
( e12 != op1(e10,e13)
| ~ spl12_290 ),
inference(forward_demodulation,[],[f146,f1958]) ).
fof(f3352,plain,
( e13 != op1(e10,e12)
| ~ spl12_292 ),
inference(forward_demodulation,[],[f152,f1968]) ).
fof(f3353,plain,
( e13 != op1(e12,e11)
| ~ spl12_226 ),
inference(forward_demodulation,[],[f153,f1640]) ).
fof(f3354,plain,
( ~ spl12_294
| ~ spl12_226 ),
inference(avatar_split_clause,[],[f3353,f1638,f1975]) ).
fof(f3365,plain,
( op1(e10,e10) != e13
| ~ spl12_282 ),
inference(forward_demodulation,[],[f163,f1921]) ).
fof(f3366,plain,
( op1(e10,e10) != e11
| ~ spl12_212 ),
inference(forward_demodulation,[],[f164,f1577]) ).
fof(f3368,plain,
( e21 != op2(e23,e22)
| ~ spl12_179 ),
inference(forward_demodulation,[],[f165,f1414]) ).
fof(f3376,plain,
( e23 != op2(e23,e20)
| ~ spl12_180 ),
inference(forward_demodulation,[],[f170,f1419]) ).
fof(f3391,plain,
( e20 != op2(e21,e20)
| ~ spl12_165 ),
inference(forward_demodulation,[],[f182,f1351]) ).
fof(f3396,plain,
( op2(e20,e20) != e23
| ~ spl12_243 ),
inference(forward_demodulation,[],[f187,f1716]) ).
fof(f3399,plain,
( e21 != op2(e22,e23)
| ~ spl12_179 ),
inference(forward_demodulation,[],[f189,f1414]) ).
fof(f3401,plain,
( e21 != op2(e21,e23)
| ~ spl12_179 ),
inference(forward_demodulation,[],[f190,f1414]) ).
fof(f3404,plain,
( e21 != op2(e20,e23)
| ~ spl12_179 ),
inference(forward_demodulation,[],[f192,f1414]) ).
fof(f3413,plain,
( e23 != op2(e22,e21)
| ~ spl12_180 ),
inference(forward_demodulation,[],[f201,f1419]) ).
fof(f3416,plain,
( e23 != op2(e20,e21)
| ~ spl12_180 ),
inference(forward_demodulation,[],[f204,f1419]) ).
fof(f3418,plain,
( e20 != op2(e20,e21)
| ~ spl12_165 ),
inference(forward_demodulation,[],[f206,f1351]) ).
fof(f3423,plain,
( op2(e20,e20) != e22
| ~ spl12_241 ),
inference(forward_demodulation,[],[f210,f1707]) ).
fof(f3424,plain,
( op2(e20,e20) != e23
| ~ spl12_246 ),
inference(forward_demodulation,[],[f211,f1729]) ).
fof(f3425,plain,
( op2(e20,e20) != e21
| ~ spl12_166 ),
inference(forward_demodulation,[],[f212,f1356]) ).
fof(f3427,plain,
( e10 = op1(e11,e11)
| ~ spl12_225 ),
inference(forward_demodulation,[],[f317,f1635]) ).
fof(f3428,plain,
( e20 = op2(e21,e21)
| ~ spl12_179 ),
inference(forward_demodulation,[],[f320,f1414]) ).
fof(f3432,plain,
( e20 != op2(e20,e20)
| spl12_141
| ~ spl12_155 ),
inference(forward_demodulation,[],[f1231,f1308]) ).
fof(f3433,plain,
( $false
| spl12_141
| ~ spl12_155 ),
inference(forward_subsumption_resolution,[],[f3432,f1308]) ).
fof(f3434,plain,
( spl12_141
| ~ spl12_155 ),
inference(avatar_contradiction_clause,[],[f3433]) ).
fof(f3437,plain,
( e22 != op2(e22,e22)
| spl12_144
| ~ spl12_253 ),
inference(forward_demodulation,[],[f1245,f1762]) ).
fof(f3439,plain,
( e21 != op2(e20,e21)
| spl12_146
| ~ spl12_166 ),
inference(forward_demodulation,[],[f1255,f1356]) ).
fof(f3443,plain,
( e22 != op2(e20,e22)
| spl12_148
| ~ spl12_241 ),
inference(forward_demodulation,[],[f1264,f1707]) ).
fof(f3444,plain,
( e23 != op2(e21,e23)
| spl12_152
| ~ spl12_180 ),
inference(forward_demodulation,[],[f1284,f1419]) ).
fof(f3445,plain,
( e20 != op2(e22,e20)
| spl12_153
| ~ spl12_260 ),
inference(forward_demodulation,[],[f1292,f1795]) ).
fof(f3452,plain,
( e22 != op2(e21,e22)
| spl12_150
| ~ spl12_174 ),
inference(forward_demodulation,[],[f1274,f1392]) ).
fof(f3453,plain,
( e23 != op2(e20,e23)
| spl12_151
| ~ spl12_246 ),
inference(forward_demodulation,[],[f1279,f1729]) ).
fof(f3460,plain,
( ~ spl12_257
| spl12_152
| ~ spl12_180 ),
inference(avatar_split_clause,[],[f3444,f1417,f1282,f1778]) ).
fof(f3461,plain,
( e22 != op2(e21,e23)
| ~ spl12_253 ),
inference(forward_demodulation,[],[f177,f1762]) ).
fof(f3462,plain,
( e20 != op2(e21,e23)
| ~ spl12_165 ),
inference(forward_demodulation,[],[f178,f1351]) ).
fof(f3465,plain,
( ~ spl12_244
| spl12_151
| ~ spl12_246 ),
inference(avatar_split_clause,[],[f3453,f1727,f1277,f1718]) ).
fof(f3469,plain,
( e20 != op2(e20,e23)
| ~ spl12_155 ),
inference(forward_demodulation,[],[f186,f1308]) ).
fof(f3471,plain,
( ~ spl12_238
| spl12_148
| ~ spl12_241 ),
inference(avatar_split_clause,[],[f3443,f1705,f1262,f1692]) ).
fof(f3472,plain,
( ~ spl12_254
| ~ spl12_253 ),
inference(avatar_split_clause,[],[f3461,f1760,f1764]) ).
fof(f3473,plain,
( ~ spl12_248
| ~ spl12_165 ),
inference(avatar_split_clause,[],[f3462,f1350,f1736]) ).
fof(f3478,plain,
( spl12_165
| ~ spl12_179 ),
inference(avatar_split_clause,[],[f3428,f1413,f1350]) ).
fof(f3486,plain,
( ~ spl12_253
| spl12_150
| ~ spl12_174 ),
inference(avatar_split_clause,[],[f3452,f1390,f1272,f1760]) ).
fof(f3487,plain,
( ~ spl12_164
| ~ spl12_155 ),
inference(avatar_split_clause,[],[f3469,f1306,f1345]) ).
fof(f3488,plain,
( ~ spl12_229
| ~ spl12_165 ),
inference(avatar_split_clause,[],[f3391,f1350,f1653]) ).
fof(f3489,plain,
( ~ spl12_160
| ~ spl12_165 ),
inference(avatar_split_clause,[],[f3418,f1350,f1327]) ).
fof(f3491,plain,
( ~ spl12_159
| ~ spl12_166 ),
inference(avatar_split_clause,[],[f3425,f1354,f1323]) ).
fof(f3496,plain,
( ~ spl12_261
| ~ spl12_179 ),
inference(avatar_split_clause,[],[f3399,f1413,f1798]) ).
fof(f3499,plain,
( ~ spl12_230
| spl12_153
| ~ spl12_260 ),
inference(avatar_split_clause,[],[f3445,f1793,f1290,f1657]) ).
fof(f3501,plain,
( ~ spl12_232
| spl12_146
| ~ spl12_166 ),
inference(avatar_split_clause,[],[f3439,f1354,f1253,f1666]) ).
fof(f3506,plain,
( ~ spl12_157
| spl12_144
| ~ spl12_253 ),
inference(avatar_split_clause,[],[f3437,f1760,f1243,f1314]) ).
fof(f3509,plain,
( ~ spl12_258
| ~ spl12_180 ),
inference(avatar_split_clause,[],[f3413,f1417,f1783]) ).
fof(f3514,plain,
( ~ spl12_163
| ~ spl12_243 ),
inference(avatar_split_clause,[],[f3396,f1714,f1341]) ).
fof(f3516,plain,
( ~ spl12_170
| ~ spl12_179 ),
inference(avatar_split_clause,[],[f3401,f1413,f1372]) ).
fof(f3592,plain,
( op2(e20,e20) != e22
| ~ spl12_237 ),
inference(forward_demodulation,[],[f188,f1690]) ).
fof(f3606,plain,
( e21 != op2(e22,e21)
| spl12_139
| ~ spl12_233 ),
inference(forward_demodulation,[],[f1221,f1672]) ).
fof(f3607,plain,
( $false
| spl12_139
| ~ spl12_233
| ~ spl12_251 ),
inference(forward_subsumption_resolution,[],[f3606,f1753]) ).
fof(f3608,plain,
( spl12_139
| ~ spl12_233
| ~ spl12_251 ),
inference(avatar_contradiction_clause,[],[f3607]) ).
fof(f3620,plain,
( e22 != op2(e22,e22)
| spl12_149
| ~ spl12_157 ),
inference(forward_demodulation,[],[f1269,f1316]) ).
fof(f3621,plain,
( $false
| spl12_149
| ~ spl12_157 ),
inference(forward_subsumption_resolution,[],[f3620,f1316]) ).
fof(f3622,plain,
( spl12_149
| ~ spl12_157 ),
inference(avatar_contradiction_clause,[],[f3621]) ).
fof(f3623,plain,
( e23 != op2(e22,e23)
| spl12_144
| ~ spl12_256 ),
inference(forward_demodulation,[],[f1245,f1776]) ).
fof(f3630,plain,
( ~ spl12_262
| ~ spl12_179 ),
inference(avatar_split_clause,[],[f3368,f1413,f1803]) ).
fof(f3632,plain,
( e22 != op2(e23,e22)
| ~ spl12_157 ),
inference(forward_demodulation,[],[f195,f1316]) ).
fof(f3635,plain,
( ~ spl12_242
| ~ spl12_180 ),
inference(avatar_split_clause,[],[f3416,f1417,f1710]) ).
fof(f3638,plain,
( ~ spl12_234
| ~ spl12_179 ),
inference(avatar_split_clause,[],[f3404,f1413,f1674]) ).
fof(f3639,plain,
( ~ spl12_178
| ~ spl12_180 ),
inference(avatar_split_clause,[],[f3376,f1417,f1408]) ).
fof(f3643,plain,
( ~ spl12_161
| ~ spl12_237 ),
inference(avatar_split_clause,[],[f3592,f1688,f1332]) ).
fof(f3644,plain,
( ~ spl12_263
| ~ spl12_157 ),
inference(avatar_split_clause,[],[f3632,f1314,f1809]) ).
fof(f3651,plain,
( ~ spl12_161
| ~ spl12_241 ),
inference(avatar_split_clause,[],[f3423,f1705,f1332]) ).
fof(f3652,plain,
( ~ spl12_163
| ~ spl12_246 ),
inference(avatar_split_clause,[],[f3424,f1727,f1341]) ).
fof(f3666,plain,
( ~ spl12_264
| spl12_144
| ~ spl12_256 ),
inference(avatar_split_clause,[],[f3623,f1774,f1243,f1814]) ).
fof(f3712,plain,
( e10 != op1(e10,e10)
| spl12_187
| ~ spl12_201 ),
inference(forward_demodulation,[],[f1452,f1529]) ).
fof(f3713,plain,
( $false
| spl12_187
| ~ spl12_201 ),
inference(forward_subsumption_resolution,[],[f3712,f1529]) ).
fof(f3714,plain,
( spl12_187
| ~ spl12_201 ),
inference(avatar_contradiction_clause,[],[f3713]) ).
fof(f3716,plain,
( e12 != op1(e10,e12)
| spl12_194
| ~ spl12_277 ),
inference(forward_demodulation,[],[f1485,f1899]) ).
fof(f3717,plain,
( e13 != op1(e11,e13)
| spl12_198
| ~ spl12_226 ),
inference(forward_demodulation,[],[f1505,f1640]) ).
fof(f3718,plain,
( e10 != op1(e12,e10)
| spl12_199
| ~ spl12_296 ),
inference(forward_demodulation,[],[f1513,f1987]) ).
fof(f3726,plain,
( e12 != op1(e11,e12)
| spl12_196
| ~ spl12_220 ),
inference(forward_demodulation,[],[f1495,f1613]) ).
fof(f3727,plain,
( e13 != op1(e10,e13)
| spl12_197
| ~ spl12_282 ),
inference(forward_demodulation,[],[f1500,f1921]) ).
fof(f3732,plain,
( e13 != op1(e12,e13)
| spl12_190
| ~ spl12_292 ),
inference(forward_demodulation,[],[f1466,f1968]) ).
fof(f3734,plain,
( e11 != op1(e10,e11)
| spl12_192
| ~ spl12_212 ),
inference(forward_demodulation,[],[f1476,f1577]) ).
fof(f3740,plain,
( ~ spl12_274
| spl12_194
| ~ spl12_277 ),
inference(avatar_split_clause,[],[f3716,f1897,f1483,f1884]) ).
fof(f3741,plain,
( ~ spl12_293
| spl12_198
| ~ spl12_226 ),
inference(avatar_split_clause,[],[f3717,f1638,f1503,f1970]) ).
fof(f3743,plain,
( e11 != op1(e11,e12)
| ~ spl12_212 ),
inference(forward_demodulation,[],[f133,f1577]) ).
fof(f3746,plain,
( ~ spl12_289
| spl12_196
| ~ spl12_220 ),
inference(avatar_split_clause,[],[f3726,f1611,f1493,f1952]) ).
fof(f3748,plain,
( e10 != op1(e10,e13)
| ~ spl12_201 ),
inference(forward_demodulation,[],[f138,f1529]) ).
fof(f3753,plain,
( ~ spl12_280
| spl12_197
| ~ spl12_282 ),
inference(avatar_split_clause,[],[f3727,f1919,f1498,f1910]) ).
fof(f3758,plain,
( e11 != op1(e12,e11)
| ~ spl12_268 ),
inference(forward_demodulation,[],[f157,f1860]) ).
fof(f3762,plain,
( spl12_211
| ~ spl12_225 ),
inference(avatar_split_clause,[],[f3427,f1634,f1571]) ).
fof(f3766,plain,
( ~ spl12_287
| ~ spl12_268 ),
inference(avatar_split_clause,[],[f3758,f1858,f1943]) ).
fof(f3772,plain,
( ~ spl12_214
| ~ spl12_212 ),
inference(avatar_split_clause,[],[f3743,f1575,f1584]) ).
fof(f3773,plain,
( ~ spl12_205
| ~ spl12_212 ),
inference(avatar_split_clause,[],[f3366,f1575,f1544]) ).
fof(f3774,plain,
( ~ spl12_275
| ~ spl12_290 ),
inference(avatar_split_clause,[],[f3346,f1956,f1888]) ).
fof(f3777,plain,
( ~ spl12_279
| ~ spl12_292 ),
inference(avatar_split_clause,[],[f3352,f1966,f1906]) ).
fof(f3778,plain,
( ~ spl12_300
| spl12_190
| ~ spl12_292 ),
inference(avatar_split_clause,[],[f3732,f1966,f1464,f2006]) ).
fof(f3779,plain,
( ~ spl12_297
| ~ spl12_225 ),
inference(avatar_split_clause,[],[f3340,f1634,f1990]) ).
fof(f3780,plain,
( ~ spl12_266
| spl12_199
| ~ spl12_296 ),
inference(avatar_split_clause,[],[f3718,f1985,f1511,f1849]) ).
fof(f3781,plain,
( ~ spl12_268
| spl12_192
| ~ spl12_212 ),
inference(avatar_split_clause,[],[f3734,f1575,f1474,f1858]) ).
fof(f3856,plain,
( e11 != op1(e12,e11)
| spl12_185
| ~ spl12_269 ),
inference(forward_demodulation,[],[f1442,f1864]) ).
fof(f3857,plain,
( $false
| spl12_185
| ~ spl12_269
| ~ spl12_287 ),
inference(forward_subsumption_resolution,[],[f3856,f1945]) ).
fof(f3858,plain,
( spl12_185
| ~ spl12_269
| ~ spl12_287 ),
inference(avatar_contradiction_clause,[],[f3857]) ).
fof(f3870,plain,
( e12 != op1(e12,e12)
| spl12_195
| ~ spl12_203 ),
inference(forward_demodulation,[],[f1490,f1537]) ).
fof(f3871,plain,
( $false
| spl12_195
| ~ spl12_203 ),
inference(forward_subsumption_resolution,[],[f3870,f1537]) ).
fof(f3872,plain,
( spl12_195
| ~ spl12_203 ),
inference(avatar_contradiction_clause,[],[f3871]) ).
fof(f3876,plain,
( ~ spl12_210
| ~ spl12_201 ),
inference(avatar_split_clause,[],[f3748,f1527,f1566]) ).
fof(f3878,plain,
( ~ spl12_209
| ~ spl12_282 ),
inference(avatar_split_clause,[],[f3365,f1919,f1562]) ).
fof(f3879,plain,
( ~ spl12_210
| ~ spl12_295 ),
inference(avatar_split_clause,[],[f3345,f1980,f1566]) ).
fof(f3885,plain,
( e11 != op1(e12,e10)
| ~ spl12_212 ),
inference(forward_demodulation,[],[f161,f1577]) ).
fof(f3888,plain,
( ~ spl12_271
| ~ spl12_212 ),
inference(avatar_split_clause,[],[f3885,f1575,f1871]) ).
fof(f3935,plain,
( op2(e21,e21) = h4(e10)
| ~ spl12_179 ),
inference(forward_demodulation,[],[f335,f1414]) ).
fof(f3936,plain,
( e20 = h4(e10)
| ~ spl12_165
| ~ spl12_179 ),
inference(forward_demodulation,[],[f3935,f1351]) ).
fof(f3939,plain,
( spl12_35
| ~ spl12_165
| ~ spl12_179 ),
inference(avatar_split_clause,[],[f3936,f1413,f1350,f729]) ).
fof(f3940,plain,
( op2(e20,e20) != h4(op1(e10,e10))
| ~ spl12_35
| spl12_113 ),
inference(superposition,[],[f1096,f730]) ).
fof(f3942,plain,
( op2(e20,e20) != h4(e10)
| ~ spl12_35
| spl12_113
| ~ spl12_201 ),
inference(forward_demodulation,[],[f3940,f1529]) ).
fof(f3943,plain,
( e20 != op2(e20,e20)
| ~ spl12_35
| spl12_113
| ~ spl12_201 ),
inference(forward_demodulation,[],[f3942,f730]) ).
fof(f3944,plain,
( $false
| ~ spl12_35
| spl12_113
| ~ spl12_155
| ~ spl12_201 ),
inference(forward_subsumption_resolution,[],[f3943,f1308]) ).
fof(f3945,plain,
( ~ spl12_35
| spl12_113
| ~ spl12_155
| ~ spl12_201 ),
inference(avatar_contradiction_clause,[],[f3944]) ).
fof(f3947,plain,
( h4(op1(e10,e11)) != op2(h4(e10),e21)
| ~ spl12_39
| spl12_114 ),
inference(forward_demodulation,[],[f1100,f749]) ).
fof(f3949,plain,
( op2(e20,e21) != h4(op1(e10,e11))
| ~ spl12_35
| ~ spl12_39
| spl12_114 ),
inference(forward_demodulation,[],[f3947,f730]) ).
fof(f3951,plain,
( op2(e20,e21) != h4(e12)
| ~ spl12_35
| ~ spl12_39
| spl12_114
| ~ spl12_273 ),
inference(forward_demodulation,[],[f3949,f1882]) ).
fof(f3952,plain,
( e22 != h4(e12)
| ~ spl12_35
| ~ spl12_39
| spl12_114
| ~ spl12_237
| ~ spl12_273 ),
inference(forward_demodulation,[],[f3951,f1690]) ).
fof(f3953,plain,
( ~ spl12_131
| ~ spl12_35
| ~ spl12_39
| spl12_114
| ~ spl12_237
| ~ spl12_273 ),
inference(avatar_split_clause,[],[f3952,f1880,f1688,f1098,f748,f729,f1167]) ).
fof(f4282,plain,
( h4(e12) = op2(e23,op2(e21,e21))
| ~ spl12_179 ),
inference(forward_demodulation,[],[f333,f1414]) ).
fof(f4283,plain,
( op2(e23,e20) = h4(e12)
| ~ spl12_165
| ~ spl12_179 ),
inference(forward_demodulation,[],[f4282,f1351]) ).
fof(f4284,plain,
( e22 = h4(e12)
| ~ spl12_165
| ~ spl12_179
| ~ spl12_241 ),
inference(forward_demodulation,[],[f4283,f1707]) ).
fof(f4288,plain,
( h4(op1(e10,e12)) != op2(e20,h4(e12))
| ~ spl12_35
| spl12_115 ),
inference(forward_demodulation,[],[f1104,f730]) ).
fof(f4289,plain,
( spl12_131
| ~ spl12_165
| ~ spl12_179
| ~ spl12_241 ),
inference(avatar_split_clause,[],[f4284,f1705,f1413,f1350,f1167]) ).
fof(f4291,plain,
( h4(e11) != op2(e20,h4(e12))
| ~ spl12_35
| spl12_115
| ~ spl12_269 ),
inference(forward_demodulation,[],[f4288,f1864]) ).
fof(f4293,plain,
( e21 != op2(e20,h4(e12))
| ~ spl12_35
| ~ spl12_39
| spl12_115
| ~ spl12_269 ),
inference(forward_demodulation,[],[f4291,f749]) ).
fof(f4298,plain,
( e21 != op2(e20,e22)
| ~ spl12_35
| ~ spl12_39
| spl12_115
| ~ spl12_131
| ~ spl12_269 ),
inference(forward_demodulation,[],[f4293,f1168]) ).
fof(f4299,plain,
( $false
| ~ spl12_35
| ~ spl12_39
| spl12_115
| ~ spl12_131
| ~ spl12_233
| ~ spl12_269 ),
inference(forward_subsumption_resolution,[],[f4298,f1672]) ).
fof(f4300,plain,
( ~ spl12_35
| ~ spl12_39
| spl12_115
| ~ spl12_131
| ~ spl12_233
| ~ spl12_269 ),
inference(avatar_contradiction_clause,[],[f4299]) ).
fof(f4302,plain,
( h4(op1(e10,e13)) != op2(h4(e10),e23)
| spl12_116
| ~ spl12_136 ),
inference(forward_demodulation,[],[f1108,f1199]) ).
fof(f4304,plain,
( op2(e20,e23) != h4(op1(e10,e13))
| ~ spl12_35
| spl12_116
| ~ spl12_136 ),
inference(forward_demodulation,[],[f4302,f730]) ).
fof(f4306,plain,
( op2(e20,e23) != h4(e13)
| ~ spl12_35
| spl12_116
| ~ spl12_136
| ~ spl12_280 ),
inference(forward_demodulation,[],[f4304,f1912]) ).
fof(f4308,plain,
( e23 != op2(e20,e23)
| ~ spl12_35
| spl12_116
| ~ spl12_136
| ~ spl12_280 ),
inference(forward_demodulation,[],[f4306,f1199]) ).
fof(f4309,plain,
( $false
| ~ spl12_35
| spl12_116
| ~ spl12_136
| ~ spl12_244
| ~ spl12_280 ),
inference(forward_subsumption_resolution,[],[f4308,f1720]) ).
fof(f4310,plain,
( ~ spl12_35
| spl12_116
| ~ spl12_136
| ~ spl12_244
| ~ spl12_280 ),
inference(avatar_contradiction_clause,[],[f4309]) ).
fof(f4312,plain,
( h4(op1(e11,e10)) != op2(h4(e11),e20)
| ~ spl12_35
| spl12_117 ),
inference(forward_demodulation,[],[f1112,f730]) ).
fof(f4314,plain,
( op2(e21,e20) != h4(op1(e11,e10))
| ~ spl12_35
| ~ spl12_39
| spl12_117 ),
inference(forward_demodulation,[],[f4312,f749]) ).
fof(f4316,plain,
( op2(e21,e20) != h4(e11)
| ~ spl12_35
| ~ spl12_39
| spl12_117
| ~ spl12_212 ),
inference(forward_demodulation,[],[f4314,f1577]) ).
fof(f4318,plain,
( e21 != op2(e21,e20)
| ~ spl12_35
| ~ spl12_39
| spl12_117
| ~ spl12_212 ),
inference(forward_demodulation,[],[f4316,f749]) ).
fof(f4319,plain,
( $false
| ~ spl12_35
| ~ spl12_39
| spl12_117
| ~ spl12_166
| ~ spl12_212 ),
inference(forward_subsumption_resolution,[],[f4318,f1356]) ).
fof(f4320,plain,
( ~ spl12_35
| ~ spl12_39
| spl12_117
| ~ spl12_166
| ~ spl12_212 ),
inference(avatar_contradiction_clause,[],[f4319]) ).
fof(f4322,plain,
( op2(e21,e21) != h4(op1(e11,e11))
| ~ spl12_39
| spl12_118 ),
inference(forward_demodulation,[],[f1116,f749]) ).
fof(f4324,plain,
( op2(e21,e21) != h4(e10)
| ~ spl12_39
| spl12_118
| ~ spl12_211 ),
inference(forward_demodulation,[],[f4322,f1572]) ).
fof(f4326,plain,
( e20 != op2(e21,e21)
| ~ spl12_35
| ~ spl12_39
| spl12_118
| ~ spl12_211 ),
inference(forward_demodulation,[],[f4324,f730]) ).
fof(f4328,plain,
( $false
| ~ spl12_35
| ~ spl12_39
| spl12_118
| ~ spl12_165
| ~ spl12_211 ),
inference(forward_subsumption_resolution,[],[f4326,f1351]) ).
fof(f4329,plain,
( ~ spl12_35
| ~ spl12_39
| spl12_118
| ~ spl12_165
| ~ spl12_211 ),
inference(avatar_contradiction_clause,[],[f4328]) ).
fof(f4331,plain,
( h4(op1(e11,e12)) != op2(h4(e11),e22)
| spl12_119
| ~ spl12_131 ),
inference(forward_demodulation,[],[f1120,f1168]) ).
fof(f4333,plain,
( op2(e21,e22) != h4(op1(e11,e12))
| ~ spl12_39
| spl12_119
| ~ spl12_131 ),
inference(forward_demodulation,[],[f4331,f749]) ).
fof(f4335,plain,
( op2(e21,e22) != h4(e13)
| ~ spl12_39
| spl12_119
| ~ spl12_131
| ~ spl12_292 ),
inference(forward_demodulation,[],[f4333,f1968]) ).
fof(f4336,plain,
( e23 != op2(e21,e22)
| ~ spl12_39
| spl12_119
| ~ spl12_131
| ~ spl12_136
| ~ spl12_292 ),
inference(forward_demodulation,[],[f4335,f1199]) ).
fof(f4337,plain,
( $false
| ~ spl12_39
| spl12_119
| ~ spl12_131
| ~ spl12_136
| ~ spl12_256
| ~ spl12_292 ),
inference(forward_subsumption_resolution,[],[f4336,f1776]) ).
fof(f4338,plain,
( ~ spl12_39
| spl12_119
| ~ spl12_131
| ~ spl12_136
| ~ spl12_256
| ~ spl12_292 ),
inference(avatar_contradiction_clause,[],[f4337]) ).
fof(f4340,plain,
( h4(op1(e11,e13)) != op2(h4(e11),e23)
| spl12_120
| ~ spl12_136 ),
inference(forward_demodulation,[],[f1124,f1199]) ).
fof(f4342,plain,
( op2(e21,e23) != h4(op1(e11,e13))
| ~ spl12_39
| spl12_120
| ~ spl12_136 ),
inference(forward_demodulation,[],[f4340,f749]) ).
fof(f4344,plain,
( op2(e21,e23) != h4(e12)
| ~ spl12_39
| spl12_120
| ~ spl12_136
| ~ spl12_290 ),
inference(forward_demodulation,[],[f4342,f1958]) ).
fof(f4346,plain,
( e22 != op2(e21,e23)
| ~ spl12_39
| spl12_120
| ~ spl12_131
| ~ spl12_136
| ~ spl12_290 ),
inference(forward_demodulation,[],[f4344,f1168]) ).
fof(f4347,plain,
( $false
| ~ spl12_39
| spl12_120
| ~ spl12_131
| ~ spl12_136
| ~ spl12_254
| ~ spl12_290 ),
inference(forward_subsumption_resolution,[],[f4346,f1766]) ).
fof(f4348,plain,
( ~ spl12_39
| spl12_120
| ~ spl12_131
| ~ spl12_136
| ~ spl12_254
| ~ spl12_290 ),
inference(avatar_contradiction_clause,[],[f4347]) ).
fof(f4350,plain,
( h4(op1(e12,e10)) != op2(h4(e12),e20)
| ~ spl12_35
| spl12_121 ),
inference(forward_demodulation,[],[f1128,f730]) ).
fof(f4352,plain,
( op2(e22,e20) != h4(op1(e12,e10))
| ~ spl12_35
| spl12_121
| ~ spl12_131 ),
inference(forward_demodulation,[],[f4350,f1168]) ).
fof(f4354,plain,
( op2(e22,e20) != h4(e13)
| ~ spl12_35
| spl12_121
| ~ spl12_131
| ~ spl12_282 ),
inference(forward_demodulation,[],[f4352,f1921]) ).
fof(f4356,plain,
( e23 != op2(e22,e20)
| ~ spl12_35
| spl12_121
| ~ spl12_131
| ~ spl12_136
| ~ spl12_282 ),
inference(forward_demodulation,[],[f4354,f1199]) ).
fof(f4357,plain,
( $false
| ~ spl12_35
| spl12_121
| ~ spl12_131
| ~ spl12_136
| ~ spl12_246
| ~ spl12_282 ),
inference(forward_subsumption_resolution,[],[f4356,f1729]) ).
fof(f4358,plain,
( ~ spl12_35
| spl12_121
| ~ spl12_131
| ~ spl12_136
| ~ spl12_246
| ~ spl12_282 ),
inference(avatar_contradiction_clause,[],[f4357]) ).
fof(f4360,plain,
( h4(op1(e12,e11)) != op2(h4(e12),e21)
| ~ spl12_39
| spl12_122 ),
inference(forward_demodulation,[],[f1132,f749]) ).
fof(f4362,plain,
( op2(e22,e21) != h4(op1(e12,e11))
| ~ spl12_39
| spl12_122
| ~ spl12_131 ),
inference(forward_demodulation,[],[f4360,f1168]) ).
fof(f4364,plain,
( op2(e22,e21) != h4(e11)
| ~ spl12_39
| spl12_122
| ~ spl12_131
| ~ spl12_287 ),
inference(forward_demodulation,[],[f4362,f1945]) ).
fof(f4366,plain,
( e21 != op2(e22,e21)
| ~ spl12_39
| spl12_122
| ~ spl12_131
| ~ spl12_287 ),
inference(forward_demodulation,[],[f4364,f749]) ).
fof(f4367,plain,
( $false
| ~ spl12_39
| spl12_122
| ~ spl12_131
| ~ spl12_251
| ~ spl12_287 ),
inference(forward_subsumption_resolution,[],[f4366,f1753]) ).
fof(f4368,plain,
( ~ spl12_39
| spl12_122
| ~ spl12_131
| ~ spl12_251
| ~ spl12_287 ),
inference(avatar_contradiction_clause,[],[f4367]) ).
fof(f4370,plain,
( op2(e22,e22) != h4(op1(e12,e12))
| spl12_123
| ~ spl12_131 ),
inference(forward_demodulation,[],[f1136,f1168]) ).
fof(f4372,plain,
( op2(e22,e22) != h4(e12)
| spl12_123
| ~ spl12_131
| ~ spl12_203 ),
inference(forward_demodulation,[],[f4370,f1537]) ).
fof(f4374,plain,
( e22 != op2(e22,e22)
| spl12_123
| ~ spl12_131
| ~ spl12_203 ),
inference(forward_demodulation,[],[f4372,f1168]) ).
fof(f4376,plain,
( $false
| spl12_123
| ~ spl12_131
| ~ spl12_157
| ~ spl12_203 ),
inference(forward_subsumption_resolution,[],[f4374,f1316]) ).
fof(f4377,plain,
( spl12_123
| ~ spl12_131
| ~ spl12_157
| ~ spl12_203 ),
inference(avatar_contradiction_clause,[],[f4376]) ).
fof(f4379,plain,
( h4(op1(e12,e13)) != op2(h4(e12),e23)
| spl12_124
| ~ spl12_136 ),
inference(forward_demodulation,[],[f1140,f1199]) ).
fof(f4381,plain,
( op2(e22,e23) != h4(op1(e12,e13))
| spl12_124
| ~ spl12_131
| ~ spl12_136 ),
inference(forward_demodulation,[],[f4379,f1168]) ).
fof(f4383,plain,
( op2(e22,e23) != h4(e10)
| spl12_124
| ~ spl12_131
| ~ spl12_136
| ~ spl12_295 ),
inference(forward_demodulation,[],[f4381,f1982]) ).
fof(f4384,plain,
( e20 != op2(e22,e23)
| ~ spl12_35
| spl12_124
| ~ spl12_131
| ~ spl12_136
| ~ spl12_295 ),
inference(forward_demodulation,[],[f4383,f730]) ).
fof(f4385,plain,
( $false
| ~ spl12_35
| spl12_124
| ~ spl12_131
| ~ spl12_136
| ~ spl12_259
| ~ spl12_295 ),
inference(forward_subsumption_resolution,[],[f4384,f1790]) ).
fof(f4386,plain,
( ~ spl12_35
| spl12_124
| ~ spl12_131
| ~ spl12_136
| ~ spl12_259
| ~ spl12_295 ),
inference(avatar_contradiction_clause,[],[f4385]) ).
fof(f4388,plain,
( h4(op1(e13,e10)) != op2(h4(e13),e20)
| ~ spl12_35
| spl12_125 ),
inference(forward_demodulation,[],[f1144,f730]) ).
fof(f4390,plain,
( op2(e23,e20) != h4(op1(e13,e10))
| ~ spl12_35
| spl12_125
| ~ spl12_136 ),
inference(forward_demodulation,[],[f4388,f1199]) ).
fof(f4392,plain,
( op2(e23,e20) != h4(e12)
| ~ spl12_35
| spl12_125
| ~ spl12_136
| ~ spl12_277 ),
inference(forward_demodulation,[],[f4390,f1899]) ).
fof(f4394,plain,
( e22 != op2(e23,e20)
| ~ spl12_35
| spl12_125
| ~ spl12_131
| ~ spl12_136
| ~ spl12_277 ),
inference(forward_demodulation,[],[f4392,f1168]) ).
fof(f4395,plain,
( $false
| ~ spl12_35
| spl12_125
| ~ spl12_131
| ~ spl12_136
| ~ spl12_241
| ~ spl12_277 ),
inference(forward_subsumption_resolution,[],[f4394,f1707]) ).
fof(f4396,plain,
( ~ spl12_35
| spl12_125
| ~ spl12_131
| ~ spl12_136
| ~ spl12_241
| ~ spl12_277 ),
inference(avatar_contradiction_clause,[],[f4395]) ).
fof(f4398,plain,
( h4(op1(e13,e11)) != op2(h4(e13),e21)
| ~ spl12_39
| spl12_126 ),
inference(forward_demodulation,[],[f1148,f749]) ).
fof(f4400,plain,
( op2(e23,e21) != h4(op1(e13,e11))
| ~ spl12_39
| spl12_126
| ~ spl12_136 ),
inference(forward_demodulation,[],[f4398,f1199]) ).
fof(f4402,plain,
( op2(e23,e21) != h4(e13)
| ~ spl12_39
| spl12_126
| ~ spl12_136
| ~ spl12_226 ),
inference(forward_demodulation,[],[f4400,f1640]) ).
fof(f4404,plain,
( e23 != op2(e23,e21)
| ~ spl12_39
| spl12_126
| ~ spl12_136
| ~ spl12_226 ),
inference(forward_demodulation,[],[f4402,f1199]) ).
fof(f4405,plain,
( $false
| ~ spl12_39
| spl12_126
| ~ spl12_136
| ~ spl12_180
| ~ spl12_226 ),
inference(forward_subsumption_resolution,[],[f4404,f1419]) ).
fof(f4406,plain,
( ~ spl12_39
| spl12_126
| ~ spl12_136
| ~ spl12_180
| ~ spl12_226 ),
inference(avatar_contradiction_clause,[],[f4405]) ).
fof(f4408,plain,
( h4(op1(e13,e12)) != op2(h4(e13),e22)
| spl12_127
| ~ spl12_131 ),
inference(forward_demodulation,[],[f1152,f1168]) ).
fof(f4410,plain,
( op2(e23,e22) != h4(op1(e13,e12))
| spl12_127
| ~ spl12_131
| ~ spl12_136 ),
inference(forward_demodulation,[],[f4408,f1199]) ).
fof(f4412,plain,
( op2(e23,e22) != h4(e10)
| spl12_127
| ~ spl12_131
| ~ spl12_136
| ~ spl12_296 ),
inference(forward_demodulation,[],[f4410,f1987]) ).
fof(f4414,plain,
( e20 != op2(e23,e22)
| ~ spl12_35
| spl12_127
| ~ spl12_131
| ~ spl12_136
| ~ spl12_296 ),
inference(forward_demodulation,[],[f4412,f730]) ).
fof(f4415,plain,
( $false
| ~ spl12_35
| spl12_127
| ~ spl12_131
| ~ spl12_136
| ~ spl12_260
| ~ spl12_296 ),
inference(forward_subsumption_resolution,[],[f4414,f1795]) ).
fof(f4416,plain,
( ~ spl12_35
| spl12_127
| ~ spl12_131
| ~ spl12_136
| ~ spl12_260
| ~ spl12_296 ),
inference(avatar_contradiction_clause,[],[f4415]) ).
fof(f4418,plain,
( op2(e23,e23) != h4(op1(e13,e13))
| spl12_128
| ~ spl12_136 ),
inference(forward_demodulation,[],[f1156,f1199]) ).
fof(f4420,plain,
( op2(e23,e23) != h4(e11)
| spl12_128
| ~ spl12_136
| ~ spl12_225 ),
inference(forward_demodulation,[],[f4418,f1635]) ).
fof(f4422,plain,
( e21 != op2(e23,e23)
| ~ spl12_39
| spl12_128
| ~ spl12_136
| ~ spl12_225 ),
inference(forward_demodulation,[],[f4420,f749]) ).
fof(f4424,plain,
( $false
| ~ spl12_39
| spl12_128
| ~ spl12_136
| ~ spl12_179
| ~ spl12_225 ),
inference(forward_subsumption_resolution,[],[f4422,f1414]) ).
fof(f4425,plain,
( ~ spl12_39
| spl12_128
| ~ spl12_136
| ~ spl12_179
| ~ spl12_225 ),
inference(avatar_contradiction_clause,[],[f4424]) ).
cnf(s28,plain,
( spl12_31
| ~ spl12_35 ),
inference(sat_conversion,[],[f732]) ).
cnf(s31,plain,
( spl12_36
| ~ spl12_39 ),
inference(sat_conversion,[],[f751]) ).
cnf(s94,plain,
( ~ spl12_31
| ~ spl12_36
| ~ spl12_113
| ~ spl12_114
| ~ spl12_115
| ~ spl12_116
| ~ spl12_117
| ~ spl12_118
| ~ spl12_119
| ~ spl12_120
| ~ spl12_121
| ~ spl12_122
| ~ spl12_123
| ~ spl12_124
| ~ spl12_125
| ~ spl12_126
| ~ spl12_127
| ~ spl12_128
| ~ spl12_131
| ~ spl12_136 ),
inference(sat_conversion,[],[f1202]) ).
cnf(s97,plain,
spl12_136,
inference(sat_conversion,[],[f1205]) ).
cnf(s98,plain,
spl12_105,
inference(sat_conversion,[],[f1206]) ).
cnf(s100,plain,
spl12_2,
inference(sat_conversion,[],[f1208]) ).
cnf(s102,plain,
( spl12_137
| ~ spl12_139 ),
inference(sat_conversion,[],[f1222]) ).
cnf(s104,plain,
( spl12_137
| ~ spl12_141 ),
inference(sat_conversion,[],[f1232]) ).
cnf(s106,plain,
( spl12_142
| ~ spl12_144 ),
inference(sat_conversion,[],[f1246]) ).
cnf(s108,plain,
( spl12_142
| ~ spl12_146 ),
inference(sat_conversion,[],[f1256]) ).
cnf(s112,plain,
( ~ spl12_137
| ~ spl12_142
| ~ spl12_148
| ~ spl12_151 ),
inference(sat_conversion,[],[f1280]) ).
cnf(s114,plain,
( ~ spl12_137
| ~ spl12_142
| ~ spl12_149
| ~ spl12_152 ),
inference(sat_conversion,[],[f1286]) ).
cnf(s115,plain,
( ~ spl12_137
| ~ spl12_142
| ~ spl12_150
| ~ spl12_152 ),
inference(sat_conversion,[],[f1287]) ).
cnf(s118,plain,
( ~ spl12_137
| ~ spl12_142
| ~ spl12_149
| ~ spl12_153 ),
inference(sat_conversion,[],[f1294]) ).
cnf(s125,plain,
( spl12_155
| spl12_156
| spl12_157
| spl12_158 ),
inference(sat_conversion,[],[f1321]) ).
cnf(s128,plain,
( ~ spl12_163
| spl12_164 ),
inference(sat_conversion,[],[f1348]) ).
cnf(s129,plain,
( ~ spl12_165
| spl12_166 ),
inference(sat_conversion,[],[f1357]) ).
cnf(s131,plain,
( ~ spl12_169
| spl12_170 ),
inference(sat_conversion,[],[f1375]) ).
cnf(s135,plain,
( ~ spl12_177
| spl12_178 ),
inference(sat_conversion,[],[f1411]) ).
cnf(s136,plain,
( ~ spl12_179
| spl12_180 ),
inference(sat_conversion,[],[f1420]) ).
cnf(s139,plain,
( spl12_183
| ~ spl12_185 ),
inference(sat_conversion,[],[f1443]) ).
cnf(s141,plain,
( spl12_183
| ~ spl12_187 ),
inference(sat_conversion,[],[f1453]) ).
cnf(s143,plain,
( ~ spl12_188
| ~ spl12_190 ),
inference(sat_conversion,[],[f1467]) ).
cnf(s145,plain,
( ~ spl12_188
| ~ spl12_192 ),
inference(sat_conversion,[],[f1477]) ).
cnf(s149,plain,
( ~ spl12_183
| spl12_188
| ~ spl12_194
| ~ spl12_197 ),
inference(sat_conversion,[],[f1501]) ).
cnf(s152,plain,
( ~ spl12_183
| spl12_188
| ~ spl12_196
| ~ spl12_198 ),
inference(sat_conversion,[],[f1508]) ).
cnf(s155,plain,
( ~ spl12_183
| spl12_188
| ~ spl12_195
| ~ spl12_199 ),
inference(sat_conversion,[],[f1515]) ).
cnf(s162,plain,
( spl12_201
| spl12_202
| spl12_203
| spl12_204 ),
inference(sat_conversion,[],[f1542]) ).
cnf(s164,plain,
( ~ spl12_207
| spl12_208 ),
inference(sat_conversion,[],[f1560]) ).
cnf(s165,plain,
( ~ spl12_209
| spl12_210 ),
inference(sat_conversion,[],[f1569]) ).
cnf(s166,plain,
( ~ spl12_211
| spl12_212 ),
inference(sat_conversion,[],[f1578]) ).
cnf(s169,plain,
( ~ spl12_217
| spl12_218 ),
inference(sat_conversion,[],[f1605]) ).
cnf(s170,plain,
( ~ spl12_219
| spl12_220 ),
inference(sat_conversion,[],[f1614]) ).
cnf(s171,plain,
( ~ spl12_221
| spl12_222 ),
inference(sat_conversion,[],[f1623]) ).
cnf(s173,plain,
( ~ spl12_225
| spl12_226 ),
inference(sat_conversion,[],[f1641]) ).
cnf(s176,plain,
( spl12_155
| spl12_229
| spl12_230
| spl12_231 ),
inference(sat_conversion,[],[f1664]) ).
cnf(s177,plain,
( spl12_159
| spl12_232
| spl12_233
| spl12_234 ),
inference(sat_conversion,[],[f1677]) ).
cnf(s180,plain,
( spl12_161
| spl12_172
| spl12_240
| spl12_241 ),
inference(sat_conversion,[],[f1708]) ).
cnf(s182,plain,
( spl12_163
| spl12_178
| spl12_245
| spl12_246 ),
inference(sat_conversion,[],[f1730]) ).
cnf(s186,plain,
( spl12_156
| spl12_232
| spl12_251
| spl12_252 ),
inference(sat_conversion,[],[f1758]) ).
cnf(s187,plain,
( spl12_167
| spl12_240
| spl12_253
| spl12_254 ),
inference(sat_conversion,[],[f1767]) ).
cnf(s188,plain,
( spl12_167
| spl12_174
| spl12_237
| spl12_255 ),
inference(sat_conversion,[],[f1772]) ).
cnf(s189,plain,
( spl12_169
| spl12_245
| spl12_256
| spl12_257 ),
inference(sat_conversion,[],[f1781]) ).
cnf(s193,plain,
( spl12_173
| spl12_235
| spl12_251
| spl12_261 ),
inference(sat_conversion,[],[f1801]) ).
cnf(s194,plain,
( spl12_168
| spl12_173
| spl12_233
| spl12_262 ),
inference(sat_conversion,[],[f1806]) ).
cnf(s195,plain,
( spl12_157
| spl12_172
| spl12_174
| spl12_176 ),
inference(sat_conversion,[],[f1807]) ).
cnf(s196,plain,
( spl12_157
| spl12_238
| spl12_253
| spl12_263 ),
inference(sat_conversion,[],[f1812]) ).
cnf(s197,plain,
( spl12_175
| spl12_246
| spl12_258
| spl12_264 ),
inference(sat_conversion,[],[f1817]) ).
cnf(s198,plain,
( spl12_175
| spl12_182
| spl12_243
| spl12_256 ),
inference(sat_conversion,[],[f1818]) ).
cnf(s199,plain,
( spl12_177
| spl12_231
| spl12_250
| spl12_260 ),
inference(sat_conversion,[],[f1819]) ).
cnf(s200,plain,
( spl12_164
| spl12_177
| spl12_248
| spl12_259 ),
inference(sat_conversion,[],[f1820]) ).
cnf(s203,plain,
( spl12_181
| spl12_241
| spl12_255
| spl12_263 ),
inference(sat_conversion,[],[f1823]) ).
cnf(s206,plain,
( spl12_158
| spl12_244
| spl12_257
| spl12_264 ),
inference(sat_conversion,[],[f1826]) ).
cnf(s207,plain,
( spl12_155
| spl12_159
| spl12_161
| spl12_163 ),
inference(sat_conversion,[],[f1827]) ).
cnf(s208,plain,
( spl12_160
| spl12_232
| spl12_237
| spl12_242 ),
inference(sat_conversion,[],[f1828]) ).
cnf(s214,plain,
( spl12_170
| spl12_248
| spl12_254
| spl12_257 ),
inference(sat_conversion,[],[f1834]) ).
cnf(s223,plain,
( spl12_201
| spl12_206
| spl12_208
| spl12_210 ),
inference(sat_conversion,[],[f1843]) ).
cnf(s225,plain,
( spl12_205
| spl12_268
| spl12_269
| spl12_270 ),
inference(sat_conversion,[],[f1869]) ).
cnf(s227,plain,
( spl12_207
| spl12_273
| spl12_274
| spl12_275 ),
inference(sat_conversion,[],[f1891]) ).
cnf(s228,plain,
( spl12_207
| spl12_218
| spl12_276
| spl12_277 ),
inference(sat_conversion,[],[f1900]) ).
cnf(s229,plain,
( spl12_209
| spl12_278
| spl12_279
| spl12_280 ),
inference(sat_conversion,[],[f1913]) ).
cnf(s230,plain,
( spl12_209
| spl12_224
| spl12_281
| spl12_282 ),
inference(sat_conversion,[],[f1922]) ).
cnf(s234,plain,
( spl12_202
| spl12_268
| spl12_287
| spl12_288 ),
inference(sat_conversion,[],[f1950]) ).
cnf(s235,plain,
( spl12_213
| spl12_276
| spl12_289
| spl12_290 ),
inference(sat_conversion,[],[f1959]) ).
cnf(s236,plain,
( spl12_213
| spl12_220
| spl12_273
| spl12_291 ),
inference(sat_conversion,[],[f1964]) ).
cnf(s237,plain,
( spl12_215
| spl12_281
| spl12_292
| spl12_293 ),
inference(sat_conversion,[],[f1973]) ).
cnf(s239,plain,
( spl12_217
| spl12_266
| spl12_285
| spl12_295 ),
inference(sat_conversion,[],[f1983]) ).
cnf(s241,plain,
( spl12_219
| spl12_271
| spl12_287
| spl12_297 ),
inference(sat_conversion,[],[f1993]) ).
cnf(s242,plain,
( spl12_214
| spl12_219
| spl12_269
| spl12_298 ),
inference(sat_conversion,[],[f1998]) ).
cnf(s243,plain,
( spl12_203
| spl12_218
| spl12_220
| spl12_222 ),
inference(sat_conversion,[],[f1999]) ).
cnf(s245,plain,
( spl12_221
| spl12_282
| spl12_294
| spl12_300 ),
inference(sat_conversion,[],[f2009]) ).
cnf(s246,plain,
( spl12_221
| spl12_228
| spl12_279
| spl12_292 ),
inference(sat_conversion,[],[f2010]) ).
cnf(s247,plain,
( spl12_223
| spl12_267
| spl12_286
| spl12_296 ),
inference(sat_conversion,[],[f2011]) ).
cnf(s248,plain,
( spl12_210
| spl12_223
| spl12_284
| spl12_295 ),
inference(sat_conversion,[],[f2012]) ).
cnf(s252,plain,
( spl12_222
| spl12_227
| spl12_275
| spl12_290 ),
inference(sat_conversion,[],[f2016]) ).
cnf(s254,plain,
( spl12_204
| spl12_280
| spl12_293
| spl12_300 ),
inference(sat_conversion,[],[f2018]) ).
cnf(s255,plain,
( spl12_201
| spl12_205
| spl12_207
| spl12_209 ),
inference(sat_conversion,[],[f2019]) ).
cnf(s258,plain,
( spl12_210
| spl12_270
| spl12_275
| spl12_280 ),
inference(sat_conversion,[],[f2022]) ).
cnf(s265,plain,
( spl12_203
| spl12_217
| spl12_219
| spl12_221 ),
inference(sat_conversion,[],[f2029]) ).
cnf(s271,plain,
spl12_225,
inference(sat_conversion,[],[f2039]) ).
cnf(s272,plain,
spl12_179,
inference(sat_conversion,[],[f2040]) ).
cnf(s277,plain,
( ~ spl12_27
| ~ spl12_105 ),
inference(sat_conversion,[],[f2063]) ).
cnf(s281,plain,
( ~ spl12_155
| ~ spl12_161 ),
inference(sat_conversion,[],[f2086]) ).
cnf(s287,plain,
( ~ spl12_2
| ~ spl12_7
| spl12_155
| ~ spl12_232 ),
inference(sat_conversion,[],[f2104]) ).
cnf(s288,plain,
( ~ spl12_2
| ~ spl12_7
| spl12_161
| ~ spl12_237 ),
inference(sat_conversion,[],[f2105]) ).
cnf(s289,plain,
( ~ spl12_2
| ~ spl12_7
| ~ spl12_155
| spl12_159 ),
inference(sat_conversion,[],[f2106]) ).
cnf(s291,plain,
( ~ spl12_165
| ~ spl12_167 ),
inference(sat_conversion,[],[f2118]) ).
cnf(s296,plain,
( ~ spl12_32
| ~ spl12_136
| spl12_160
| ~ spl12_180 ),
inference(sat_conversion,[],[f2145]) ).
cnf(s299,plain,
( spl12_27
| ~ spl12_105
| ~ spl12_157
| ~ spl12_173 ),
inference(sat_conversion,[],[f2157]) ).
cnf(s306,plain,
( ~ spl12_37
| ~ spl12_136
| ~ spl12_166
| spl12_178 ),
inference(sat_conversion,[],[f2194]) ).
cnf(s311,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_156
| ~ spl12_165 ),
inference(sat_conversion,[],[f2209]) ).
cnf(s312,plain,
( ~ spl12_157
| ~ spl12_175 ),
inference(sat_conversion,[],[f2213]) ).
cnf(s316,plain,
( spl12_27
| ~ spl12_105
| ~ spl12_179
| ~ spl12_181 ),
inference(sat_conversion,[],[f2234]) ).
cnf(s325,plain,
( ~ spl12_202
| ~ spl12_211 ),
inference(sat_conversion,[],[f2268]) ).
cnf(s327,plain,
( ~ spl12_211
| ~ spl12_213 ),
inference(sat_conversion,[],[f2275]) ).
cnf(s329,plain,
( ~ spl12_208
| ~ spl12_269 ),
inference(sat_conversion,[],[f2282]) ).
cnf(s331,plain,
( ~ spl12_211
| ~ spl12_215 ),
inference(sat_conversion,[],[f2293]) ).
cnf(s332,plain,
( ~ spl12_203
| ~ spl12_217 ),
inference(sat_conversion,[],[f2297]) ).
cnf(s333,plain,
( ~ spl12_217
| ~ spl12_219 ),
inference(sat_conversion,[],[f2301]) ).
cnf(s334,plain,
( ~ spl12_218
| ~ spl12_266 ),
inference(sat_conversion,[],[f2304]) ).
cnf(s337,plain,
( ~ spl12_219
| ~ spl12_221 ),
inference(sat_conversion,[],[f2318]) ).
cnf(s339,plain,
( ~ spl12_204
| ~ spl12_225 ),
inference(sat_conversion,[],[f2326]) ).
cnf(s340,plain,
( ~ spl12_201
| ~ spl12_209 ),
inference(sat_conversion,[],[f2329]) ).
cnf(s342,plain,
( ~ spl12_203
| ~ spl12_219 ),
inference(sat_conversion,[],[f2338]) ).
cnf(s344,plain,
( ~ spl12_225
| ~ spl12_227 ),
inference(sat_conversion,[],[f2352]) ).
cnf(s347,plain,
( ~ spl12_2
| spl12_7
| ~ spl12_230
| ~ spl12_235 ),
inference(sat_conversion,[],[f2365]) ).
cnf(s349,plain,
( spl12_37
| ~ spl12_136
| ~ spl12_158
| ~ spl12_179 ),
inference(sat_conversion,[],[f2374]) ).
cnf(s350,plain,
( spl12_27
| ~ spl12_105
| ~ spl12_174
| ~ spl12_251 ),
inference(sat_conversion,[],[f2377]) ).
cnf(s352,plain,
( spl12_27
| ~ spl12_105
| ~ spl12_232
| ~ spl12_237 ),
inference(sat_conversion,[],[f2388]) ).
cnf(s364,plain,
( spl12_37
| ~ spl12_136
| ~ spl12_166
| ~ spl12_245 ),
inference(sat_conversion,[],[f2445]) ).
cnf(s368,plain,
( ~ spl12_180
| ~ spl12_255 ),
inference(sat_conversion,[],[f2459]) ).
cnf(s370,plain,
( spl12_27
| ~ spl12_105
| ~ spl12_166
| ~ spl12_240 ),
inference(sat_conversion,[],[f2474]) ).
cnf(s373,plain,
( spl12_32
| ~ spl12_136
| ~ spl12_180
| ~ spl12_250 ),
inference(sat_conversion,[],[f2486]) ).
cnf(s375,plain,
( spl12_32
| ~ spl12_136
| ~ spl12_182
| ~ spl12_260 ),
inference(sat_conversion,[],[f2493]) ).
cnf(s376,plain,
( ~ spl12_231
| ~ spl12_241 ),
inference(sat_conversion,[],[f2500]) ).
cnf(s386,plain,
( spl12_37
| ~ spl12_136
| ~ spl12_168
| ~ spl12_256 ),
inference(sat_conversion,[],[f2545]) ).
cnf(s388,plain,
( ~ spl12_254
| ~ spl12_257 ),
inference(sat_conversion,[],[f2552]) ).
cnf(s398,plain,
( spl12_37
| ~ spl12_136
| ~ spl12_235
| ~ spl12_246 ),
inference(sat_conversion,[],[f2607]) ).
cnf(s406,plain,
( spl12_37
| ~ spl12_136
| ~ spl12_180
| ~ spl12_252 ),
inference(sat_conversion,[],[f2663]) ).
cnf(s409,plain,
( ~ spl12_176
| ~ spl12_259 ),
inference(sat_conversion,[],[f2685]) ).
cnf(s410,plain,
( ~ spl12_172
| ~ spl12_246 ),
inference(sat_conversion,[],[f2690]) ).
cnf(s417,plain,
( ~ spl12_260
| ~ spl12_263 ),
inference(sat_conversion,[],[f2763]) ).
cnf(s419,plain,
( spl12_32
| ~ spl12_136
| ~ spl12_259
| ~ spl12_264 ),
inference(sat_conversion,[],[f2771]) ).
cnf(s422,plain,
( ~ spl12_224
| ~ spl12_267 ),
inference(sat_conversion,[],[f2783]) ).
cnf(s424,plain,
( ~ spl12_268
| ~ spl12_273 ),
inference(sat_conversion,[],[f2792]) ).
cnf(s430,plain,
( ~ spl12_201
| ~ spl12_207 ),
inference(sat_conversion,[],[f2812]) ).
cnf(s431,plain,
( ~ spl12_228
| ~ spl12_296 ),
inference(sat_conversion,[],[f2815]) ).
cnf(s433,plain,
( ~ spl12_212
| ~ spl12_276 ),
inference(sat_conversion,[],[f2826]) ).
cnf(s435,plain,
( ~ spl12_267
| ~ spl12_277 ),
inference(sat_conversion,[],[f2834]) ).
cnf(s437,plain,
( ~ spl12_268
| ~ spl12_278 ),
inference(sat_conversion,[],[f2843]) ).
cnf(s438,plain,
( ~ spl12_274
| ~ spl12_279 ),
inference(sat_conversion,[],[f2850]) ).
cnf(s443,plain,
( ~ spl12_223
| ~ spl12_225 ),
inference(sat_conversion,[],[f2869]) ).
cnf(s444,plain,
( ~ spl12_224
| ~ spl12_277 ),
inference(sat_conversion,[],[f2874]) ).
cnf(s447,plain,
( ~ spl12_212
| ~ spl12_281 ),
inference(sat_conversion,[],[f2885]) ).
cnf(s449,plain,
( ~ spl12_266
| ~ spl12_282 ),
inference(sat_conversion,[],[f2893]) ).
cnf(s450,plain,
( ~ spl12_226
| ~ spl12_286 ),
inference(sat_conversion,[],[f2896]) ).
cnf(s451,plain,
( ~ spl12_270
| ~ spl12_280 ),
inference(sat_conversion,[],[f2901]) ).
cnf(s452,plain,
( ~ spl12_226
| ~ spl12_288 ),
inference(sat_conversion,[],[f2903]) ).
cnf(s453,plain,
( ~ spl12_220
| ~ spl12_287 ),
inference(sat_conversion,[],[f2907]) ).
cnf(s454,plain,
( ~ spl12_226
| ~ spl12_291 ),
inference(sat_conversion,[],[f2910]) ).
cnf(s457,plain,
( ~ spl12_222
| ~ spl12_295 ),
inference(sat_conversion,[],[f2931]) ).
cnf(s459,plain,
( ~ spl12_206
| ~ spl12_273 ),
inference(sat_conversion,[],[f2941]) ).
cnf(s462,plain,
( ~ spl12_270
| ~ spl12_275 ),
inference(sat_conversion,[],[f2955]) ).
cnf(s464,plain,
( ~ spl12_269
| ~ spl12_279 ),
inference(sat_conversion,[],[f2970]) ).
cnf(s467,plain,
( ~ spl12_275
| ~ spl12_280 ),
inference(sat_conversion,[],[f2984]) ).
cnf(s468,plain,
( ~ spl12_275
| ~ spl12_280 ),
inference(sat_conversion,[],[f2986]) ).
cnf(s470,plain,
( ~ spl12_269
| ~ spl12_274 ),
inference(sat_conversion,[],[f2996]) ).
cnf(s473,plain,
( ~ spl12_285
| ~ spl12_287 ),
inference(sat_conversion,[],[f3012]) ).
cnf(s478,plain,
( ~ spl12_284
| ~ spl12_290 ),
inference(sat_conversion,[],[f3046]) ).
cnf(s484,plain,
( ~ spl12_203
| ~ spl12_221 ),
inference(sat_conversion,[],[f3074]) ).
cnf(s486,plain,
( ~ spl12_273
| ~ spl12_278 ),
inference(sat_conversion,[],[f3099]) ).
cnf(s488,plain,
( ~ spl12_218
| ~ spl12_282 ),
inference(sat_conversion,[],[f3119]) ).
cnf(s490,plain,
( ~ spl12_290
| ~ spl12_293 ),
inference(sat_conversion,[],[f3134]) ).
cnf(s492,plain,
( ~ spl12_210
| ~ spl12_270 ),
inference(sat_conversion,[],[f3143]) ).
cnf(s493,plain,
( ~ spl12_284
| ~ spl12_293 ),
inference(sat_conversion,[],[f3146]) ).
cnf(s494,plain,
( ~ spl12_289
| ~ spl12_292 ),
inference(sat_conversion,[],[f3157]) ).
cnf(s496,plain,
( ~ spl12_296
| ~ spl12_298 ),
inference(sat_conversion,[],[f3166]) ).
cnf(s501,plain,
( ~ spl12_220
| ~ spl12_285 ),
inference(sat_conversion,[],[f3199]) ).
cnf(s507,plain,
( ~ spl12_295
| ~ spl12_300 ),
inference(sat_conversion,[],[f3285]) ).
cnf(s513,plain,
( spl12_39
| ~ spl12_179 ),
inference(sat_conversion,[],[f3307]) ).
cnf(s514,plain,
( ~ spl12_226
| ~ spl12_294 ),
inference(sat_conversion,[],[f3354]) ).
cnf(s515,plain,
( spl12_141
| ~ spl12_155 ),
inference(sat_conversion,[],[f3434]) ).
cnf(s519,plain,
( spl12_152
| ~ spl12_180
| ~ spl12_257 ),
inference(sat_conversion,[],[f3460]) ).
cnf(s521,plain,
( spl12_151
| ~ spl12_244
| ~ spl12_246 ),
inference(sat_conversion,[],[f3465]) ).
cnf(s523,plain,
( spl12_148
| ~ spl12_238
| ~ spl12_241 ),
inference(sat_conversion,[],[f3471]) ).
cnf(s525,plain,
( ~ spl12_253
| ~ spl12_254 ),
inference(sat_conversion,[],[f3472]) ).
cnf(s526,plain,
( ~ spl12_165
| ~ spl12_248 ),
inference(sat_conversion,[],[f3473]) ).
cnf(s528,plain,
( spl12_165
| ~ spl12_179 ),
inference(sat_conversion,[],[f3478]) ).
cnf(s534,plain,
( spl12_150
| ~ spl12_174
| ~ spl12_253 ),
inference(sat_conversion,[],[f3486]) ).
cnf(s535,plain,
( ~ spl12_155
| ~ spl12_164 ),
inference(sat_conversion,[],[f3487]) ).
cnf(s537,plain,
( ~ spl12_165
| ~ spl12_229 ),
inference(sat_conversion,[],[f3488]) ).
cnf(s538,plain,
( ~ spl12_160
| ~ spl12_165 ),
inference(sat_conversion,[],[f3489]) ).
cnf(s540,plain,
( ~ spl12_159
| ~ spl12_166 ),
inference(sat_conversion,[],[f3491]) ).
cnf(s543,plain,
( ~ spl12_179
| ~ spl12_261 ),
inference(sat_conversion,[],[f3496]) ).
cnf(s546,plain,
( spl12_153
| ~ spl12_230
| ~ spl12_260 ),
inference(sat_conversion,[],[f3499]) ).
cnf(s549,plain,
( spl12_146
| ~ spl12_166
| ~ spl12_232 ),
inference(sat_conversion,[],[f3501]) ).
cnf(s554,plain,
( spl12_144
| ~ spl12_157
| ~ spl12_253 ),
inference(sat_conversion,[],[f3506]) ).
cnf(s557,plain,
( ~ spl12_180
| ~ spl12_258 ),
inference(sat_conversion,[],[f3509]) ).
cnf(s563,plain,
( ~ spl12_163
| ~ spl12_243 ),
inference(sat_conversion,[],[f3514]) ).
cnf(s566,plain,
( ~ spl12_170
| ~ spl12_179 ),
inference(sat_conversion,[],[f3516]) ).
cnf(s573,plain,
( spl12_139
| ~ spl12_233
| ~ spl12_251 ),
inference(sat_conversion,[],[f3608]) ).
cnf(s575,plain,
( spl12_149
| ~ spl12_157 ),
inference(sat_conversion,[],[f3622]) ).
cnf(s579,plain,
( ~ spl12_179
| ~ spl12_262 ),
inference(sat_conversion,[],[f3630]) ).
cnf(s580,plain,
( ~ spl12_180
| ~ spl12_242 ),
inference(sat_conversion,[],[f3635]) ).
cnf(s581,plain,
( ~ spl12_179
| ~ spl12_234 ),
inference(sat_conversion,[],[f3638]) ).
cnf(s582,plain,
( ~ spl12_178
| ~ spl12_180 ),
inference(sat_conversion,[],[f3639]) ).
cnf(s583,plain,
( ~ spl12_161
| ~ spl12_237 ),
inference(sat_conversion,[],[f3643]) ).
cnf(s584,plain,
( ~ spl12_157
| ~ spl12_263 ),
inference(sat_conversion,[],[f3644]) ).
cnf(s593,plain,
( ~ spl12_161
| ~ spl12_241 ),
inference(sat_conversion,[],[f3651]) ).
cnf(s594,plain,
( ~ spl12_163
| ~ spl12_246 ),
inference(sat_conversion,[],[f3652]) ).
cnf(s604,plain,
( spl12_144
| ~ spl12_256
| ~ spl12_264 ),
inference(sat_conversion,[],[f3666]) ).
cnf(s606,plain,
( spl12_187
| ~ spl12_201 ),
inference(sat_conversion,[],[f3714]) ).
cnf(s610,plain,
( spl12_194
| ~ spl12_274
| ~ spl12_277 ),
inference(sat_conversion,[],[f3740]) ).
cnf(s611,plain,
( spl12_198
| ~ spl12_226
| ~ spl12_293 ),
inference(sat_conversion,[],[f3741]) ).
cnf(s612,plain,
( spl12_196
| ~ spl12_220
| ~ spl12_289 ),
inference(sat_conversion,[],[f3746]) ).
cnf(s615,plain,
( spl12_197
| ~ spl12_280
| ~ spl12_282 ),
inference(sat_conversion,[],[f3753]) ).
cnf(s617,plain,
( spl12_211
| ~ spl12_225 ),
inference(sat_conversion,[],[f3762]) ).
cnf(s621,plain,
( ~ spl12_268
| ~ spl12_287 ),
inference(sat_conversion,[],[f3766]) ).
cnf(s627,plain,
( ~ spl12_212
| ~ spl12_214 ),
inference(sat_conversion,[],[f3772]) ).
cnf(s628,plain,
( ~ spl12_205
| ~ spl12_212 ),
inference(sat_conversion,[],[f3773]) ).
cnf(s629,plain,
( ~ spl12_275
| ~ spl12_290 ),
inference(sat_conversion,[],[f3774]) ).
cnf(s632,plain,
( ~ spl12_279
| ~ spl12_292 ),
inference(sat_conversion,[],[f3777]) ).
cnf(s633,plain,
( spl12_190
| ~ spl12_292
| ~ spl12_300 ),
inference(sat_conversion,[],[f3778]) ).
cnf(s634,plain,
( ~ spl12_225
| ~ spl12_297 ),
inference(sat_conversion,[],[f3779]) ).
cnf(s635,plain,
( spl12_199
| ~ spl12_266
| ~ spl12_296 ),
inference(sat_conversion,[],[f3780]) ).
cnf(s637,plain,
( spl12_192
| ~ spl12_212
| ~ spl12_268 ),
inference(sat_conversion,[],[f3781]) ).
cnf(s639,plain,
( spl12_185
| ~ spl12_269
| ~ spl12_287 ),
inference(sat_conversion,[],[f3858]) ).
cnf(s641,plain,
( spl12_195
| ~ spl12_203 ),
inference(sat_conversion,[],[f3872]) ).
cnf(s645,plain,
( ~ spl12_201
| ~ spl12_210 ),
inference(sat_conversion,[],[f3876]) ).
cnf(s647,plain,
( ~ spl12_209
| ~ spl12_282 ),
inference(sat_conversion,[],[f3878]) ).
cnf(s648,plain,
( ~ spl12_210
| ~ spl12_295 ),
inference(sat_conversion,[],[f3879]) ).
cnf(s653,plain,
( ~ spl12_212
| ~ spl12_271 ),
inference(sat_conversion,[],[f3888]) ).
cnf(s662,plain,
( spl12_35
| ~ spl12_165
| ~ spl12_179 ),
inference(sat_conversion,[],[f3939]) ).
cnf(s663,plain,
( ~ spl12_35
| spl12_113
| ~ spl12_155
| ~ spl12_201 ),
inference(sat_conversion,[],[f3945]) ).
cnf(s664,plain,
( ~ spl12_35
| ~ spl12_39
| spl12_114
| ~ spl12_131
| ~ spl12_237
| ~ spl12_273 ),
inference(sat_conversion,[],[f3953]) ).
cnf(s703,plain,
( spl12_131
| ~ spl12_165
| ~ spl12_179
| ~ spl12_241 ),
inference(sat_conversion,[],[f4289]) ).
cnf(s705,plain,
( ~ spl12_35
| ~ spl12_39
| spl12_115
| ~ spl12_131
| ~ spl12_233
| ~ spl12_269 ),
inference(sat_conversion,[],[f4300]) ).
cnf(s706,plain,
( ~ spl12_35
| spl12_116
| ~ spl12_136
| ~ spl12_244
| ~ spl12_280 ),
inference(sat_conversion,[],[f4310]) ).
cnf(s707,plain,
( ~ spl12_35
| ~ spl12_39
| spl12_117
| ~ spl12_166
| ~ spl12_212 ),
inference(sat_conversion,[],[f4320]) ).
cnf(s708,plain,
( ~ spl12_35
| ~ spl12_39
| spl12_118
| ~ spl12_165
| ~ spl12_211 ),
inference(sat_conversion,[],[f4329]) ).
cnf(s709,plain,
( ~ spl12_39
| spl12_119
| ~ spl12_131
| ~ spl12_136
| ~ spl12_256
| ~ spl12_292 ),
inference(sat_conversion,[],[f4338]) ).
cnf(s710,plain,
( ~ spl12_39
| spl12_120
| ~ spl12_131
| ~ spl12_136
| ~ spl12_254
| ~ spl12_290 ),
inference(sat_conversion,[],[f4348]) ).
cnf(s711,plain,
( ~ spl12_35
| spl12_121
| ~ spl12_131
| ~ spl12_136
| ~ spl12_246
| ~ spl12_282 ),
inference(sat_conversion,[],[f4358]) ).
cnf(s712,plain,
( ~ spl12_39
| spl12_122
| ~ spl12_131
| ~ spl12_251
| ~ spl12_287 ),
inference(sat_conversion,[],[f4368]) ).
cnf(s713,plain,
( spl12_123
| ~ spl12_131
| ~ spl12_157
| ~ spl12_203 ),
inference(sat_conversion,[],[f4377]) ).
cnf(s714,plain,
( ~ spl12_35
| spl12_124
| ~ spl12_131
| ~ spl12_136
| ~ spl12_259
| ~ spl12_295 ),
inference(sat_conversion,[],[f4386]) ).
cnf(s715,plain,
( ~ spl12_35
| spl12_125
| ~ spl12_131
| ~ spl12_136
| ~ spl12_241
| ~ spl12_277 ),
inference(sat_conversion,[],[f4396]) ).
cnf(s716,plain,
( ~ spl12_39
| spl12_126
| ~ spl12_136
| ~ spl12_180
| ~ spl12_226 ),
inference(sat_conversion,[],[f4406]) ).
cnf(s717,plain,
( ~ spl12_35
| spl12_127
| ~ spl12_131
| ~ spl12_136
| ~ spl12_260
| ~ spl12_296 ),
inference(sat_conversion,[],[f4416]) ).
cnf(s718,plain,
( ~ spl12_39
| spl12_128
| ~ spl12_136
| ~ spl12_179
| ~ spl12_225 ),
inference(sat_conversion,[],[f4425]) ).
cnf(s719,plain,
~ spl12_234,
inference(rat,[],[s581,s272]) ).
cnf(s720,plain,
~ spl12_262,
inference(rat,[],[s579,s272]) ).
cnf(s721,plain,
~ spl12_170,
inference(rat,[],[s566,s272]) ).
cnf(s722,plain,
~ spl12_261,
inference(rat,[],[s543,s272]) ).
cnf(s723,plain,
spl12_165,
inference(rat,[],[s528,s272]) ).
cnf(s724,plain,
spl12_39,
inference(rat,[],[s513,s272]) ).
cnf(s725,plain,
spl12_35,
inference(rat,[],[s662,s272,s723]) ).
cnf(s726,plain,
~ spl12_160,
inference(rat,[],[s538,s723]) ).
cnf(s727,plain,
~ spl12_229,
inference(rat,[],[s537,s723]) ).
cnf(s728,plain,
~ spl12_248,
inference(rat,[],[s526,s723]) ).
cnf(s730,plain,
~ spl12_167,
inference(rat,[],[s291,s723]) ).
cnf(s731,plain,
~ spl12_297,
inference(rat,[],[s634,s271]) ).
cnf(s732,plain,
spl12_211,
inference(rat,[],[s617,s271]) ).
cnf(s733,plain,
~ spl12_223,
inference(rat,[],[s443,s271]) ).
cnf(s734,plain,
~ spl12_227,
inference(rat,[],[s344,s271]) ).
cnf(s735,plain,
~ spl12_204,
inference(rat,[],[s339,s271]) ).
cnf(s737,plain,
~ spl12_215,
inference(rat,[],[s331,s732]) ).
cnf(s738,plain,
~ spl12_213,
inference(rat,[],[s327,s732]) ).
cnf(s739,plain,
~ spl12_202,
inference(rat,[],[s325,s732]) ).
cnf(s740,plain,
spl12_118,
inference(rat,[],[s708,s725,s723,s724,s732]) ).
cnf(s743,plain,
( spl12_280
| spl12_293
| spl12_300 ),
inference(rat,[],[s254,s735]) ).
cnf(s745,plain,
( spl12_222
| spl12_275
| spl12_290 ),
inference(rat,[],[s252,s734]) ).
cnf(s747,plain,
( spl12_210
| spl12_284
| spl12_295 ),
inference(rat,[],[s248,s733]) ).
cnf(s748,plain,
( spl12_267
| spl12_286
| spl12_296 ),
inference(rat,[],[s247,s733]) ).
cnf(s749,plain,
( spl12_219
| spl12_271
| spl12_287 ),
inference(rat,[],[s241,s731]) ).
cnf(s751,plain,
( spl12_281
| spl12_292
| spl12_293 ),
inference(rat,[],[s237,s737]) ).
cnf(s752,plain,
( spl12_220
| spl12_273
| spl12_291 ),
inference(rat,[],[s236,s738]) ).
cnf(s753,plain,
( spl12_276
| spl12_289
| spl12_290 ),
inference(rat,[],[s235,s738]) ).
cnf(s754,plain,
( spl12_268
| spl12_287
| spl12_288 ),
inference(rat,[],[s234,s739]) ).
cnf(s759,plain,
( spl12_254
| spl12_257 ),
inference(rat,[],[s214,s728,s721]) ).
cnf(s762,plain,
( spl12_232
| spl12_237
| spl12_242 ),
inference(rat,[],[s208,s726]) ).
cnf(s763,plain,
( spl12_164
| spl12_177
| spl12_259 ),
inference(rat,[],[s200,s728]) ).
cnf(s764,plain,
( spl12_168
| spl12_173
| spl12_233 ),
inference(rat,[],[s194,s720]) ).
cnf(s765,plain,
( spl12_173
| spl12_235
| spl12_251 ),
inference(rat,[],[s193,s722]) ).
cnf(s766,plain,
( spl12_174
| spl12_237
| spl12_255 ),
inference(rat,[],[s188,s730]) ).
cnf(s767,plain,
( spl12_240
| spl12_253
| spl12_254 ),
inference(rat,[],[s187,s730]) ).
cnf(s769,plain,
( spl12_159
| spl12_232
| spl12_233 ),
inference(rat,[],[s177,s719]) ).
cnf(s770,plain,
( spl12_155
| spl12_230
| spl12_231 ),
inference(rat,[],[s176,s727]) ).
cnf(s772,plain,
spl12_226,
inference(rat,[],[s173,s271]) ).
cnf(s773,plain,
~ spl12_294,
inference(rat,[],[s514,s772]) ).
cnf(s774,plain,
~ spl12_291,
inference(rat,[],[s454,s772]) ).
cnf(s775,plain,
~ spl12_288,
inference(rat,[],[s452,s772]) ).
cnf(s776,plain,
~ spl12_286,
inference(rat,[],[s450,s772]) ).
cnf(s777,plain,
spl12_212,
inference(rat,[],[s166,s732]) ).
cnf(s778,plain,
~ spl12_271,
inference(rat,[],[s653,s777]) ).
cnf(s779,plain,
~ spl12_205,
inference(rat,[],[s628,s777]) ).
cnf(s780,plain,
~ spl12_214,
inference(rat,[],[s627,s777]) ).
cnf(s781,plain,
~ spl12_281,
inference(rat,[],[s447,s777]) ).
cnf(s782,plain,
~ spl12_276,
inference(rat,[],[s433,s777]) ).
cnf(s783,plain,
( spl12_201
| spl12_203 ),
inference(rat,[],[s162,s735,s739]) ).
cnf(s784,plain,
spl12_180,
inference(rat,[],[s136,s272]) ).
cnf(s785,plain,
~ spl12_178,
inference(rat,[],[s582,s784]) ).
cnf(s786,plain,
~ spl12_242,
inference(rat,[],[s580,s784]) ).
cnf(s787,plain,
~ spl12_258,
inference(rat,[],[s557,s784]) ).
cnf(s788,plain,
~ spl12_255,
inference(rat,[],[s368,s784]) ).
cnf(s789,plain,
~ spl12_177,
inference(rat,[],[s135,s785]) ).
cnf(s790,plain,
~ spl12_169,
inference(rat,[],[s131,s721]) ).
cnf(s791,plain,
spl12_166,
inference(rat,[],[s129,s723]) ).
cnf(s792,plain,
~ spl12_159,
inference(rat,[],[s540,s791]) ).
cnf(s793,plain,
spl12_117,
inference(rat,[],[s707,s777,s725,s724,s791]) ).
cnf(s794,plain,
~ spl12_27,
inference(rat,[],[s277,s98]) ).
cnf(s795,plain,
~ spl12_240,
inference(rat,[],[s370,s98,s791,s794]) ).
cnf(s796,plain,
~ spl12_181,
inference(rat,[],[s316,s98,s272,s794]) ).
cnf(s797,plain,
~ spl12_37,
inference(rat,[],[s306,s785,s791,s97]) ).
cnf(s798,plain,
~ spl12_32,
inference(rat,[],[s296,s784,s726,s97]) ).
cnf(s799,plain,
spl12_128,
inference(rat,[],[s718,s271,s272,s724,s97]) ).
cnf(s800,plain,
spl12_126,
inference(rat,[],[s716,s772,s784,s724,s97]) ).
cnf(s801,plain,
~ spl12_252,
inference(rat,[],[s406,s97,s784,s797]) ).
cnf(s802,plain,
~ spl12_245,
inference(rat,[],[s364,s97,s791,s797]) ).
cnf(s803,plain,
~ spl12_158,
inference(rat,[],[s349,s272,s97,s797]) ).
cnf(s804,plain,
~ spl12_250,
inference(rat,[],[s373,s97,s784,s798]) ).
cnf(s807,plain,
( ~ spl12_31
| ~ spl12_36
| ~ spl12_113
| ~ spl12_114
| ~ spl12_115
| ~ spl12_116
| ~ spl12_119
| ~ spl12_120
| ~ spl12_121
| ~ spl12_122
| ~ spl12_123
| ~ spl12_124
| ~ spl12_125
| ~ spl12_127
| ~ spl12_131 ),
inference(rat,[],[s94,s97,s799,s800,s740,s793]) ).
cnf(s825,plain,
spl12_36,
inference(rat,[],[s31,s724]) ).
cnf(s826,plain,
spl12_31,
inference(rat,[],[s28,s725]) ).
cnf(s830,plain,
( spl12_7
| spl12_155 ),
inference(rat,[],[s102,s573,s118,s764,s106,s386,s604,s765,s198,s197,s347,s546,s375,s563,s594,s770,s199,s207,s376,s593,s203,s299,s312,s575,s584,s125,s311,s97,s797,s787,s100,s798,s789,s804,s792,s788,s796,s98,s794,s803,s723]) ).
cnf(s831,plain,
( ~ spl12_7
| spl12_155 ),
inference(rat,[],[s288,s583,s762,s287,s786,s100]) ).
cnf(s832,plain,
spl12_155,
inference(rat,[],[s831,s830]) ).
cnf(s838,plain,
~ spl12_164,
inference(rat,[],[s535,s832]) ).
cnf(s839,plain,
spl12_141,
inference(rat,[],[s515,s832]) ).
cnf(s841,plain,
~ spl12_161,
inference(rat,[],[s281,s832]) ).
cnf(s842,plain,
~ spl12_7,
inference(rat,[],[s289,s792,s100,s832]) ).
cnf(s847,plain,
spl12_259,
inference(rat,[],[s763,s789,s838]) ).
cnf(s848,plain,
~ spl12_163,
inference(rat,[],[s128,s838]) ).
cnf(s849,plain,
spl12_137,
inference(rat,[],[s104,s839]) ).
cnf(s850,plain,
~ spl12_156,
inference(rat,[],[s311,s723,s100,s842]) ).
cnf(s852,plain,
~ spl12_176,
inference(rat,[],[s409,s847]) ).
cnf(s853,plain,
~ spl12_264,
inference(rat,[],[s419,s798,s97,s847]) ).
cnf(s855,plain,
spl12_246,
inference(rat,[],[s182,s802,s785,s848]) ).
cnf(s857,plain,
~ spl12_172,
inference(rat,[],[s410,s855]) ).
cnf(s858,plain,
~ spl12_235,
inference(rat,[],[s398,s797,s97,s855]) ).
cnf(s859,plain,
spl12_241,
inference(rat,[],[s180,s841,s795,s857]) ).
cnf(s861,plain,
~ spl12_231,
inference(rat,[],[s376,s859]) ).
cnf(s862,plain,
spl12_131,
inference(rat,[],[s703,s723,s272,s859]) ).
cnf(s864,plain,
spl12_260,
inference(rat,[],[s199,s804,s789,s861]) ).
cnf(s865,plain,
~ spl12_263,
inference(rat,[],[s417,s864]) ).
cnf(s868,plain,
( spl12_269
| ~ spl12_203 ),
inference(rat,[],[s457,s745,s239,s490,s449,s751,s230,s632,s422,s229,s748,s165,s496,s451,s462,s492,s242,s225,s332,s621,s473,s486,s752,s453,s749,s342,s781,s776,s780,s779,s774,s778]) ).
cnf(s869,plain,
spl12_201,
inference(rat,[],[s143,s633,s155,s246,s635,s431,s748,s435,s228,s334,s245,s239,s647,s648,s255,s223,s164,s139,s329,s464,s639,s868,s459,s752,s453,s473,s749,s332,s342,s484,s641,s783,s776,s782,s773,s779,s774,s778]) ).
cnf(s870,plain,
~ spl12_210,
inference(rat,[],[s645,s869]) ).
cnf(s871,plain,
spl12_187,
inference(rat,[],[s606,s869]) ).
cnf(s872,plain,
~ spl12_207,
inference(rat,[],[s430,s869]) ).
cnf(s873,plain,
~ spl12_209,
inference(rat,[],[s340,s869]) ).
cnf(s874,plain,
spl12_113,
inference(rat,[],[s663,s832,s725,s869]) ).
cnf(s876,plain,
spl12_183,
inference(rat,[],[s141,s871]) ).
cnf(s877,plain,
( spl12_219
| spl12_217
| spl12_269 ),
inference(rat,[],[s334,s228,s239,s435,s457,s748,s171,s496,s473,s265,s242,s749,s868,s782,s872,s776,s780,s778]) ).
cnf(s878,plain,
~ spl12_266,
inference(rat,[],[s444,s228,s230,s334,s449,s782,s872,s781,s873]) ).
cnf(s879,plain,
( ~ spl12_270
| ~ spl12_268 ),
inference(rat,[],[s438,s229,s227,s451,s462,s437,s424,s873,s872]) ).
cnf(s880,plain,
( spl12_275
| spl12_270
| spl12_188
| ~ spl12_282
| spl12_273 ),
inference(rat,[],[s149,s615,s610,s258,s227,s228,s488,s876,s870,s872,s782]) ).
cnf(s881,plain,
( spl12_217
| spl12_269 ),
inference(rat,[],[s152,s611,s612,s743,s753,s468,s629,s880,s879,s145,s245,s637,s424,s507,s754,s239,s453,s501,s170,s337,s877,s878,s775,s777,s773,s782,s772,s876]) ).
cnf(s882,plain,
spl12_269,
inference(rat,[],[s422,s748,s230,s496,s488,s242,s169,s333,s881,s776,s781,s873,s780]) ).
cnf(s883,plain,
~ spl12_274,
inference(rat,[],[s470,s882]) ).
cnf(s884,plain,
~ spl12_279,
inference(rat,[],[s464,s882]) ).
cnf(s887,plain,
~ spl12_268,
inference(rat,[],[s467,s227,s229,s424,s437,s872,s883,s873,s884]) ).
cnf(s888,plain,
spl12_287,
inference(rat,[],[s754,s775,s887]) ).
cnf(s891,plain,
~ spl12_220,
inference(rat,[],[s453,s888]) ).
cnf(s894,plain,
spl12_273,
inference(rat,[],[s752,s774,s891]) ).
cnf(s896,plain,
~ spl12_278,
inference(rat,[],[s486,s894]) ).
cnf(s899,plain,
spl12_280,
inference(rat,[],[s229,s884,s873,s896]) ).
cnf(s900,plain,
~ spl12_275,
inference(rat,[],[s468,s899]) ).
cnf(s903,plain,
( ~ spl12_295
| spl12_257
| spl12_232 ),
inference(rat,[],[s717,s748,s807,s715,s435,s713,s709,s228,s243,s751,s711,s488,s710,s490,s245,s745,s171,s714,s457,s507,s195,s350,s705,s769,s712,s186,s664,s762,s759,s189,s706,s206,s725,s97,s864,s862,s776,s825,s826,s874,s859,s724,s782,s872,s891,s781,s855,s773,s900,s847,s853,s803,s899,s802,s790,s786,s894,s801,s850,s888,s792,s882,s852,s857,s794,s98]) ).
cnf(s904,plain,
~ spl12_284,
inference(rat,[],[s494,s753,s751,s478,s493,s782,s781]) ).
cnf(s905,plain,
spl12_295,
inference(rat,[],[s747,s870,s904]) ).
cnf(s922,plain,
spl12_232,
inference(rat,[],[s106,s554,s114,s767,s519,s388,s903,s575,s195,s350,s186,s849,s795,s784,s905,s857,s852,s98,s794,s850,s801]) ).
cnf(s927,plain,
spl12_146,
inference(rat,[],[s549,s791,s922]) ).
cnf(s928,plain,
~ spl12_237,
inference(rat,[],[s352,s794,s98,s922]) ).
cnf(s936,plain,
spl12_142,
inference(rat,[],[s108,s927]) ).
cnf(s937,plain,
spl12_174,
inference(rat,[],[s766,s788,s928]) ).
cnf(s940,plain,
~ spl12_251,
inference(rat,[],[s350,s794,s98,s937]) ).
cnf(s947,plain,
spl12_173,
inference(rat,[],[s765,s858,s940]) ).
cnf(s949,plain,
~ spl12_157,
inference(rat,[],[s299,s794,s98,s947]) ).
cnf(s952,plain,
spl12_257,
inference(rat,[],[s523,s112,s196,s521,s525,s206,s759,s859,s849,s936,s949,s865,s855,s803,s853]) ).
cnf(s955,plain,
~ spl12_254,
inference(rat,[],[s388,s952]) ).
cnf(s956,plain,
spl12_152,
inference(rat,[],[s519,s784,s952]) ).
cnf(s960,plain,
spl12_253,
inference(rat,[],[s767,s795,s955]) ).
cnf(s962,plain,
~ spl12_150,
inference(rat,[],[s115,s936,s849,s956]) ).
cnf(s965,plain,
$false,
inference(rat,[],[s534,s937,s960,s962]) ).
fof(f4426,plain,
$false,
inference(avatar_sat_refutation,[],[s965]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG125+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.05/0.17 % Computer : n003.cluster.edu
% 0.05/0.17 % Model : x86_64 x86_64
% 0.05/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.17 % Memory : 8046.5625MB
% 0.05/0.17 % OS : Linux 6.8.0-71-generic
% 0.05/0.17 % CPULimit : 300
% 0.05/0.17 % WCLimit : 300
% 0.05/0.17 % DateTime : Mon Sep 28 19:32:43 UTC 2026
% 0.05/0.17 % CPUTime :
% 0.05/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.05/0.20 Running first-order model finding
% 0.05/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.36 % (1900336)Will run a generic schedule for satisfiability detection.
% 0.38/0.36 % (1900343)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=681171284:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.38/0.36 % (1900342)% WARNING: option uhcvi not known.
% 0.38/0.36 % (1900341)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2732342744_2999 on theBenchmark for (2999ds/0Mi)
% 0.38/0.36 % (1900344)dis+10_1_sil=32000:sp=arity:random_seed=1902747438:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.38/0.36 % (1900346)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1668406538:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.38/0.36 % (1900345)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1046694601:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.38/0.36 % (1900347)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=837898022:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.38/0.36 % (1900342)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3874485790:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.38/0.36 % Detected minimum model sizes of [8]
% 0.38/0.36 % Detected maximum model sizes of [max]
% 0.38/0.36 % TRYING [8]
% 0.38/0.36 % (1900344)Instruction limit reached!
% 0.38/0.36 % (1900344)------------------------------
% 0.38/0.36 % (1900344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.38/0.36 % (1900344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.38/0.36 % (1900344)CaDiCaL version: 2.1.3
% 0.38/0.36 % (1900344)Termination reason: Instruction limit
% 0.38/0.36 % (1900344)Termination phase: Saturation
% 0.38/0.36 % (1900344)Time elapsed: 0.052 s
% 0.38/0.36 % (1900344)Peak memory usage: 12 MB
% 0.38/0.36 % (1900344)Instructions burned: 103 (million)
% 0.38/0.36 % (1900345)Instruction limit reached!
% 0.38/0.36 % (1900345)------------------------------
% 0.38/0.36 % (1900345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.38/0.36 % (1900345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.38/0.36 % (1900345)CaDiCaL version: 2.1.3
% 0.38/0.36 % (1900345)Termination reason: Instruction limit
% 0.38/0.36 % (1900345)Termination phase: Saturation
% 0.38/0.36 % (1900345)Time elapsed: 0.056 s
% 0.38/0.36 % (1900345)Peak memory usage: 13 MB
% 0.38/0.36 % (1900345)Instructions burned: 117 (million)
% 0.38/0.36 % (1900346)Instruction limit reached!
% 0.38/0.36 % (1900346)------------------------------
% 0.38/0.36 % (1900346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.38/0.36 % (1900346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.38/0.36 % (1900346)CaDiCaL version: 2.1.3
% 0.38/0.36 % (1900346)Termination reason: Instruction limit
% 0.38/0.36 % (1900346)Termination phase: Saturation
% 0.38/0.36 % (1900346)Time elapsed: 0.066 s
% 0.38/0.36 % (1900346)Peak memory usage: 13 MB
% 0.38/0.36 % (1900346)Instructions burned: 132 (million)
% 0.38/0.36 % (1900355)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=839412092:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.38/0.36 % (1900356)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3515513389:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.38/0.36 % (1900357)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=909644312:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.38/0.36 % (1900347)Instruction limit reached!
% 0.38/0.36 % (1900347)------------------------------
% 0.38/0.36 % (1900347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.38/0.36 % (1900347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.38/0.36 % (1900347)CaDiCaL version: 2.1.3
% 0.38/0.36 % (1900347)Termination reason: Instruction limit
% 0.38/0.36 % (1900347)Termination phase: Saturation
% 0.38/0.36 % (1900347)Time elapsed: 0.086 s
% 0.38/0.36 % (1900347)Peak memory usage: 13 MB
% 0.38/0.36 % (1900347)Instructions burned: 161 (million)
% 0.38/0.36 % (1900342) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1900336-1900342"...
% 0.38/0.36 % Detected minimum model sizes of [8]
% 0.38/0.36 % Detected maximum model sizes of [max]
% 0.38/0.36 % TRYING [8]
% 0.38/0.36 % (1900342)...printing done.
% 0.38/0.36 % (1900342)Refutation found. Thanks to Tanya!
% 0.38/0.36 % SZS status Theorem for theBenchmark
% 0.38/0.36 % SZS output start Proof for theBenchmark
% See solution above
% 0.38/0.37 % (1900342)------------------------------
% 0.38/0.37 % (1900342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.38/0.37 % (1900342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.38/0.37 % (1900342)CaDiCaL version: 2.1.3
% 0.38/0.37 % (1900342)Termination reason: Refutation
% 0.38/0.37 % (1900342)Time elapsed: 0.105 s
% 0.38/0.37 % (1900342)Peak memory usage: 14 MB
% 0.38/0.37 % (1900342)Instructions burned: 208 (million)
% 0.38/0.37 % (1900336)Success in time 0.153 s
% 0.38/0.37 % Vampire exiting
%------------------------------------------------------------------------------