%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG107+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 : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:22:45 AM UTC 2026
% Result : Theorem 0.76s 0.41s
% Output : Refutation 0.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 167
% Syntax : Number of formulae : 1145 ( 172 unt; 151 def)
% Number of atoms : 3832 (1630 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 4434 (1747 ~;2100 |; 436 &)
% ( 151 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 159 ( 157 usr; 158 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)) = e10
& op1(e11,op1(e10,e11)) = e11
& op1(e12,op1(e10,e12)) = e12
& op1(e13,op1(e10,e13)) = e13 )
| ( op1(e10,op1(e11,e10)) = e10
& op1(e11,op1(e11,e11)) = e11
& op1(e12,op1(e11,e12)) = e12
& op1(e13,op1(e11,e13)) = e13 )
| ( op1(e10,op1(e12,e10)) = e10
& op1(e11,op1(e12,e11)) = e11
& op1(e12,op1(e12,e12)) = e12
& op1(e13,op1(e12,e13)) = e13 )
| ( op1(e10,op1(e13,e10)) = e10
& op1(e11,op1(e13,e11)) = e11
& op1(e12,op1(e13,e12)) = e12
& op1(e13,op1(e13,e13)) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( ( op2(e20,op2(e20,e20)) = e20
& op2(e21,op2(e20,e21)) = e21
& op2(e22,op2(e20,e22)) = e22
& op2(e23,op2(e20,e23)) = e23 )
| ( op2(e20,op2(e21,e20)) = e20
& op2(e21,op2(e21,e21)) = e21
& op2(e22,op2(e21,e22)) = e22
& op2(e23,op2(e21,e23)) = e23 )
| ( op2(e20,op2(e22,e20)) = e20
& op2(e21,op2(e22,e21)) = e21
& op2(e22,op2(e22,e22)) = e22
& op2(e23,op2(e22,e23)) = e23 )
| ( op2(e20,op2(e23,e20)) = e20
& op2(e21,op2(e23,e21)) = e21
& op2(e22,op2(e23,e22)) = e22
& op2(e23,op2(e23,e23)) = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e10 = op1(e12,e12)
& e11 = op1(e12,op1(e12,e12))
& e13 = op1(op1(e12,op1(e12,e12)),op1(e12,e12)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e20 = op2(e22,e22)
& e21 = op2(e22,op2(e22,e22))
& e23 = op2(op2(e22,op2(e22,e22)),op2(e22,e22)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( h1(e12) = e20
& h1(e10) = op2(e20,e20)
& h1(e11) = op2(e20,op2(e20,e20))
& h1(e13) = op2(op2(e20,op2(e20,e20)),op2(e20,e20)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
( h2(e12) = e21
& h2(e10) = op2(e21,e21)
& h2(e11) = op2(e21,op2(e21,e21))
& h2(e13) = op2(op2(e21,op2(e21,e21)),op2(e21,e21)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
( h3(e12) = e22
& h3(e10) = op2(e22,e22)
& h3(e11) = op2(e22,op2(e22,e22))
& h3(e13) = op2(op2(e22,op2(e22,e22)),op2(e22,e22)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f18,conjecture,
( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
file('/export/starexec/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(f23,plain,
( e13 = op1(e10,e12)
| e12 = op1(e10,e12)
| e11 = op1(e10,e12)
| e10 = op1(e10,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f24,plain,
( e13 = op1(e10,e13)
| e12 = op1(e10,e13)
| e11 = op1(e10,e13)
| e10 = op1(e10,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f30,plain,
( e13 = op1(e12,e11)
| e12 = op1(e12,e11)
| e11 = op1(e12,e11)
| e10 = op1(e12,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f33,plain,
( e13 = op1(e13,e10)
| e12 = op1(e13,e10)
| e11 = op1(e13,e10)
| e10 = op1(e13,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f35,plain,
( e13 = op1(e13,e12)
| e12 = op1(e13,e12)
| e11 = op1(e13,e12)
| e10 = op1(e13,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f38,plain,
( e10 = op1(e13,e10)
| e10 = op1(e12,e10)
| e10 = op1(e11,e10)
| 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(f43,plain,
( e13 = op1(e10,e13)
| e13 = op1(e10,e12)
| e13 = op1(e10,e11)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f2]) ).
fof(f45,plain,
( e10 = op1(e11,e13)
| e10 = op1(e11,e12)
| e10 = op1(e11,e11)
| e10 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f46,plain,
( e10 = op1(e13,e11)
| e10 = op1(e12,e11)
| e10 = op1(e11,e11)
| e10 = op1(e10,e11) ),
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(f56,plain,
( e11 = op1(e13,e12)
| e11 = op1(e12,e12)
| e11 = op1(e11,e12)
| e11 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f59,plain,
( e13 = op1(e12,e13)
| e13 = op1(e12,e12)
| e13 = op1(e12,e11)
| e13 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(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(f70,plain,
( e23 = op2(e20,e21)
| e22 = op2(e20,e21)
| e21 = op2(e20,e21)
| e20 = op2(e20,e21) ),
inference(cnf_transformation,[],[f3]) ).
fof(f71,plain,
( e23 = op2(e20,e22)
| e22 = op2(e20,e22)
| e21 = op2(e20,e22)
| e20 = op2(e20,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f78,plain,
( e23 = op2(e22,e21)
| e22 = op2(e22,e21)
| e21 = op2(e22,e21)
| e20 = op2(e22,e21) ),
inference(cnf_transformation,[],[f3]) ).
fof(f80,plain,
( e23 = op2(e22,e23)
| e22 = op2(e22,e23)
| e21 = op2(e22,e23)
| e20 = op2(e22,e23) ),
inference(cnf_transformation,[],[f3]) ).
fof(f81,plain,
( e23 = op2(e23,e20)
| e22 = op2(e23,e20)
| e21 = op2(e23,e20)
| e20 = op2(e23,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f83,plain,
( e23 = op2(e23,e22)
| e22 = op2(e23,e22)
| e21 = op2(e23,e22)
| e20 = op2(e23,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f85,plain,
( e20 = op2(e20,e23)
| e20 = op2(e20,e22)
| e20 = op2(e20,e21)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f87,plain,
( e21 = op2(e20,e23)
| e21 = op2(e20,e22)
| e21 = op2(e20,e21)
| op2(e20,e20) = e21 ),
inference(cnf_transformation,[],[f4]) ).
fof(f89,plain,
( e22 = op2(e20,e23)
| e22 = op2(e20,e22)
| e22 = op2(e20,e21)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f4]) ).
fof(f90,plain,
( e22 = op2(e23,e20)
| e22 = op2(e22,e20)
| e22 = op2(e21,e20)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f4]) ).
fof(f93,plain,
( e20 = op2(e21,e23)
| e20 = op2(e21,e22)
| e20 = op2(e21,e21)
| e20 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f95,plain,
( e21 = op2(e21,e23)
| e21 = op2(e21,e22)
| e21 = op2(e21,e21)
| e21 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f96,plain,
( e21 = op2(e23,e21)
| e21 = op2(e22,e21)
| e21 = op2(e21,e21)
| e21 = op2(e20,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f104,plain,
( e21 = op2(e23,e22)
| e21 = op2(e22,e22)
| e21 = op2(e21,e22)
| e21 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f106,plain,
( e22 = op2(e23,e22)
| e22 = op2(e22,e22)
| e22 = op2(e21,e22)
| e22 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f110,plain,
( e20 = op2(e23,e23)
| e20 = op2(e22,e23)
| e20 = op2(e21,e23)
| e20 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f119,plain,
op1(e13,e11) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f120,plain,
op1(e13,e10) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f121,plain,
op1(e13,e10) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f122,plain,
op1(e13,e10) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f123,plain,
op1(e12,e12) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f125,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f127,plain,
op1(e12,e10) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f128,plain,
op1(e12,e10) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f130,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f138,plain,
op1(e10,e10) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f139,plain,
op1(e10,e10) != op1(e10,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f144,plain,
op1(e10,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f146,plain,
op1(e10,e13) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f147,plain,
op1(e12,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f149,plain,
op1(e11,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f150,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f151,plain,
op1(e10,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f153,plain,
op1(e12,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f155,plain,
op1(e11,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f157,plain,
op1(e10,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f158,plain,
op1(e10,e11) != op1(e11,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f159,plain,
op1(e12,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f160,plain,
op1(e11,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f161,plain,
op1(e11,e10) != op1(e12,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
op1(e10,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f163,plain,
op1(e10,e10) != op1(e12,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f169,plain,
op2(e23,e20) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f171,plain,
op2(e22,e22) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f172,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f173,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f174,plain,
op2(e22,e20) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f176,plain,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f185,plain,
op2(e20,e21) != op2(e20,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f186,plain,
op2(e20,e20) != op2(e20,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f195,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f197,plain,
op2(e21,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f198,plain,
op2(e20,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f199,plain,
op2(e20,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f201,plain,
op2(e22,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f205,plain,
op2(e20,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f206,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f207,plain,
op2(e22,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f208,plain,
op2(e21,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f209,plain,
op2(e21,e20) != op2(e22,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(f224,plain,
e20 != e21,
inference(cnf_transformation,[],[f8]) ).
fof(f241,plain,
( e13 = op1(e13,op1(e10,e13))
| ~ sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f242,plain,
( e12 = op1(e12,op1(e10,e12))
| ~ sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f243,plain,
( e11 = op1(e11,op1(e10,e11))
| ~ sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f247,plain,
( e11 = op1(e11,op1(e11,e11))
| ~ sP0 ),
inference(cnf_transformation,[],[f10]) ).
fof(f248,plain,
( e10 = op1(e10,op1(e11,e10))
| ~ sP0 ),
inference(cnf_transformation,[],[f10]) ).
fof(f250,plain,
( e10 = op1(e10,op1(e13,e10))
| e12 = op1(e12,op1(e12,e12))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f252,plain,
( e10 = op1(e10,op1(e13,e10))
| e10 = op1(e10,op1(e12,e10))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f265,plain,
( e23 = op2(e23,op2(e20,e23))
| ~ sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f266,plain,
( e22 = op2(e22,op2(e20,e22))
| ~ sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f267,plain,
( e21 = op2(e21,op2(e20,e21))
| ~ sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f269,plain,
( e23 = op2(e23,op2(e21,e23))
| ~ sP2 ),
inference(cnf_transformation,[],[f11]) ).
fof(f271,plain,
( e21 = op2(e21,op2(e21,e21))
| ~ sP2 ),
inference(cnf_transformation,[],[f11]) ).
fof(f272,plain,
( e20 = op2(e20,op2(e21,e20))
| ~ sP2 ),
inference(cnf_transformation,[],[f11]) ).
fof(f274,plain,
( e20 = op2(e20,op2(e23,e20))
| e22 = op2(e22,op2(e22,e22))
| sP2
| sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f289,plain,
e13 = op1(op1(e12,op1(e12,e12)),op1(e12,e12)),
inference(cnf_transformation,[],[f12]) ).
fof(f290,plain,
e11 = op1(e12,op1(e12,e12)),
inference(cnf_transformation,[],[f12]) ).
fof(f291,plain,
e10 = op1(e12,e12),
inference(cnf_transformation,[],[f12]) ).
fof(f292,plain,
e23 = op2(op2(e22,op2(e22,e22)),op2(e22,e22)),
inference(cnf_transformation,[],[f13]) ).
fof(f293,plain,
e21 = op2(e22,op2(e22,e22)),
inference(cnf_transformation,[],[f13]) ).
fof(f294,plain,
e20 = op2(e22,e22),
inference(cnf_transformation,[],[f13]) ).
fof(f298,plain,
e20 = h1(e12),
inference(cnf_transformation,[],[f14]) ).
fof(f299,plain,
h2(e13) = op2(op2(e21,op2(e21,e21)),op2(e21,e21)),
inference(cnf_transformation,[],[f15]) ).
fof(f300,plain,
op2(e21,op2(e21,e21)) = h2(e11),
inference(cnf_transformation,[],[f15]) ).
fof(f301,plain,
op2(e21,e21) = h2(e10),
inference(cnf_transformation,[],[f15]) ).
fof(f302,plain,
e21 = h2(e12),
inference(cnf_transformation,[],[f15]) ).
fof(f306,plain,
e22 = h3(e12),
inference(cnf_transformation,[],[f16]) ).
fof(f322,plain,
( e20 != h2(e10)
| ~ sP9 ),
inference(cnf_transformation,[],[f20]) ).
fof(f324,plain,
( e21 != h2(e12)
| ~ sP8 ),
inference(cnf_transformation,[],[f20]) ).
fof(f363,plain,
( e23 != h2(e11)
| e22 != h2(e13)
| sP8
| sP9
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(cnf_transformation,[],[f20]) ).
fof(f419,plain,
( e10 = op1(e10,op1(e13,e10))
| e10 = op1(e10,op1(e12,e10))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f252]) ).
fof(f421,plain,
( e10 = op1(e10,op1(e13,e10))
| e12 = op1(e12,op1(e12,e12))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f250]) ).
fof(f423,plain,
( e10 = op1(e10,op1(e11,e10))
| sP0 ),
inference(consistent_polarity_flipping,[],[f248]) ).
fof(f424,plain,
( e11 = op1(e11,op1(e11,e11))
| sP0 ),
inference(consistent_polarity_flipping,[],[f247]) ).
fof(f441,plain,
( e20 = op2(e20,op2(e23,e20))
| e22 = op2(e22,op2(e22,e22))
| sP2
| ~ sP3 ),
inference(consistent_polarity_flipping,[],[f274]) ).
fof(f444,plain,
( e21 = op2(e21,op2(e20,e21))
| sP3 ),
inference(consistent_polarity_flipping,[],[f267]) ).
fof(f445,plain,
( e22 = op2(e22,op2(e20,e22))
| sP3 ),
inference(consistent_polarity_flipping,[],[f266]) ).
fof(f446,plain,
( e23 = op2(e23,op2(e20,e23))
| sP3 ),
inference(consistent_polarity_flipping,[],[f265]) ).
fof(f525,definition,
( spl12_3
<=> e20 = h1(e12) ),
introduced(definition,[new_symbols(definition,[spl12_3])],[avatar_definition]) ).
fof(f526,plain,
( e20 = h1(e12)
| ~ spl12_3 ),
inference(avatar_component_clause,[],[f525]) ).
fof(f549,definition,
( spl12_8
<=> e21 = h1(e12) ),
introduced(definition,[new_symbols(definition,[spl12_8])],[avatar_definition]) ).
fof(f550,plain,
( e21 = h1(e12)
| ~ spl12_8 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f551,plain,
( e21 != h1(e12)
| spl12_8 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f564,definition,
( spl12_11
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl12_11])],[avatar_definition]) ).
fof(f583,definition,
( spl12_15
<=> e20 = h2(e10) ),
introduced(definition,[new_symbols(definition,[spl12_15])],[avatar_definition]) ).
fof(f584,plain,
( e20 = h2(e10)
| ~ spl12_15 ),
inference(avatar_component_clause,[],[f583]) ).
fof(f586,plain,
( ~ spl12_11
| ~ spl12_15 ),
inference(avatar_split_clause,[],[f322,f583,f564]) ).
fof(f588,definition,
( spl12_16
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl12_16])],[avatar_definition]) ).
fof(f597,definition,
( spl12_18
<=> e21 = h2(e12) ),
introduced(definition,[new_symbols(definition,[spl12_18])],[avatar_definition]) ).
fof(f598,plain,
( e21 = h2(e12)
| ~ spl12_18 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f600,plain,
( ~ spl12_16
| ~ spl12_18 ),
inference(avatar_split_clause,[],[f324,f597,f588]) ).
fof(f645,definition,
( spl12_28
<=> e21 = h3(e12) ),
introduced(definition,[new_symbols(definition,[spl12_28])],[avatar_definition]) ).
fof(f646,plain,
( e21 = h3(e12)
| ~ spl12_28 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f647,plain,
( e21 != h3(e12)
| spl12_28 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f820,definition,
( spl12_65
<=> h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_65])],[avatar_definition]) ).
fof(f822,plain,
( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| spl12_65 ),
inference(avatar_component_clause,[],[f820]) ).
fof(f824,definition,
( spl12_66
<=> h2(op1(e10,e11)) = op2(h2(e10),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_66])],[avatar_definition]) ).
fof(f826,plain,
( h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| spl12_66 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f828,definition,
( spl12_67
<=> h2(op1(e10,e12)) = op2(h2(e10),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_67])],[avatar_definition]) ).
fof(f830,plain,
( h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| spl12_67 ),
inference(avatar_component_clause,[],[f828]) ).
fof(f832,definition,
( spl12_68
<=> h2(op1(e10,e13)) = op2(h2(e10),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_68])],[avatar_definition]) ).
fof(f834,plain,
( h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| spl12_68 ),
inference(avatar_component_clause,[],[f832]) ).
fof(f836,definition,
( spl12_69
<=> h2(op1(e11,e10)) = op2(h2(e11),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_69])],[avatar_definition]) ).
fof(f838,plain,
( h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| spl12_69 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f840,definition,
( spl12_70
<=> h2(op1(e11,e11)) = op2(h2(e11),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_70])],[avatar_definition]) ).
fof(f842,plain,
( h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| spl12_70 ),
inference(avatar_component_clause,[],[f840]) ).
fof(f844,definition,
( spl12_71
<=> h2(op1(e11,e12)) = op2(h2(e11),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_71])],[avatar_definition]) ).
fof(f846,plain,
( h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| spl12_71 ),
inference(avatar_component_clause,[],[f844]) ).
fof(f848,definition,
( spl12_72
<=> h2(op1(e11,e13)) = op2(h2(e11),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_72])],[avatar_definition]) ).
fof(f850,plain,
( h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| spl12_72 ),
inference(avatar_component_clause,[],[f848]) ).
fof(f852,definition,
( spl12_73
<=> h2(op1(e12,e10)) = op2(h2(e12),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_73])],[avatar_definition]) ).
fof(f854,plain,
( h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| spl12_73 ),
inference(avatar_component_clause,[],[f852]) ).
fof(f856,definition,
( spl12_74
<=> h2(op1(e12,e11)) = op2(h2(e12),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_74])],[avatar_definition]) ).
fof(f858,plain,
( h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| spl12_74 ),
inference(avatar_component_clause,[],[f856]) ).
fof(f860,definition,
( spl12_75
<=> h2(op1(e12,e12)) = op2(h2(e12),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_75])],[avatar_definition]) ).
fof(f862,plain,
( h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| spl12_75 ),
inference(avatar_component_clause,[],[f860]) ).
fof(f864,definition,
( spl12_76
<=> h2(op1(e12,e13)) = op2(h2(e12),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_76])],[avatar_definition]) ).
fof(f866,plain,
( h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| spl12_76 ),
inference(avatar_component_clause,[],[f864]) ).
fof(f868,definition,
( spl12_77
<=> h2(op1(e13,e10)) = op2(h2(e13),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_77])],[avatar_definition]) ).
fof(f870,plain,
( h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| spl12_77 ),
inference(avatar_component_clause,[],[f868]) ).
fof(f872,definition,
( spl12_78
<=> h2(op1(e13,e11)) = op2(h2(e13),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_78])],[avatar_definition]) ).
fof(f874,plain,
( h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| spl12_78 ),
inference(avatar_component_clause,[],[f872]) ).
fof(f876,definition,
( spl12_79
<=> h2(op1(e13,e12)) = op2(h2(e13),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_79])],[avatar_definition]) ).
fof(f878,plain,
( h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| spl12_79 ),
inference(avatar_component_clause,[],[f876]) ).
fof(f880,definition,
( spl12_80
<=> h2(op1(e13,e13)) = op2(h2(e13),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_80])],[avatar_definition]) ).
fof(f882,plain,
( h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| spl12_80 ),
inference(avatar_component_clause,[],[f880]) ).
fof(f884,definition,
( spl12_81
<=> e22 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl12_81])],[avatar_definition]) ).
fof(f885,plain,
( e22 = h2(e13)
| ~ spl12_81 ),
inference(avatar_component_clause,[],[f884]) ).
fof(f908,definition,
( spl12_86
<=> e23 = h2(e11) ),
introduced(definition,[new_symbols(definition,[spl12_86])],[avatar_definition]) ).
fof(f909,plain,
( e23 = h2(e11)
| ~ spl12_86 ),
inference(avatar_component_clause,[],[f908]) ).
fof(f911,plain,
( ~ spl12_65
| ~ spl12_66
| ~ spl12_67
| ~ spl12_68
| ~ spl12_69
| ~ spl12_70
| ~ spl12_71
| ~ spl12_72
| ~ spl12_73
| ~ spl12_74
| ~ spl12_75
| ~ spl12_76
| ~ spl12_77
| ~ spl12_78
| ~ spl12_79
| ~ spl12_80
| spl12_11
| spl12_16
| ~ spl12_81
| ~ spl12_86 ),
inference(avatar_split_clause,[],[f363,f908,f884,f588,f564,f880,f876,f872,f868,f864,f860,f856,f852,f848,f844,f840,f836,f832,f828,f824,f820]) ).
fof(f1005,definition,
( spl12_107
<=> e22 = h3(e12) ),
introduced(definition,[new_symbols(definition,[spl12_107])],[avatar_definition]) ).
fof(f1006,plain,
( e22 = h3(e12)
| ~ spl12_107 ),
inference(avatar_component_clause,[],[f1005]) ).
fof(f1156,plain,
spl12_107,
inference(avatar_split_clause,[],[f306,f1005]) ).
fof(f1157,plain,
spl12_18,
inference(avatar_split_clause,[],[f302,f597]) ).
fof(f1158,plain,
spl12_3,
inference(avatar_split_clause,[],[f298,f525]) ).
fof(f1160,definition,
( spl12_137
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl12_137])],[avatar_definition]) ).
fof(f1164,definition,
( spl12_138
<=> e23 = op2(e23,op2(e20,e23)) ),
introduced(definition,[new_symbols(definition,[spl12_138])],[avatar_definition]) ).
fof(f1166,plain,
( e23 = op2(e23,op2(e20,e23))
| ~ spl12_138 ),
inference(avatar_component_clause,[],[f1164]) ).
fof(f1167,plain,
( spl12_137
| spl12_138 ),
inference(avatar_split_clause,[],[f446,f1164,f1160]) ).
fof(f1169,definition,
( spl12_139
<=> e22 = op2(e22,op2(e20,e22)) ),
introduced(definition,[new_symbols(definition,[spl12_139])],[avatar_definition]) ).
fof(f1171,plain,
( e22 = op2(e22,op2(e20,e22))
| ~ spl12_139 ),
inference(avatar_component_clause,[],[f1169]) ).
fof(f1172,plain,
( spl12_137
| spl12_139 ),
inference(avatar_split_clause,[],[f445,f1169,f1160]) ).
fof(f1174,definition,
( spl12_140
<=> e21 = op2(e21,op2(e20,e21)) ),
introduced(definition,[new_symbols(definition,[spl12_140])],[avatar_definition]) ).
fof(f1176,plain,
( e21 = op2(e21,op2(e20,e21))
| ~ spl12_140 ),
inference(avatar_component_clause,[],[f1174]) ).
fof(f1177,plain,
( spl12_137
| spl12_140 ),
inference(avatar_split_clause,[],[f444,f1174,f1160]) ).
fof(f1184,definition,
( spl12_142
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl12_142])],[avatar_definition]) ).
fof(f1188,definition,
( spl12_143
<=> e23 = op2(e23,op2(e21,e23)) ),
introduced(definition,[new_symbols(definition,[spl12_143])],[avatar_definition]) ).
fof(f1190,plain,
( e23 = op2(e23,op2(e21,e23))
| ~ spl12_143 ),
inference(avatar_component_clause,[],[f1188]) ).
fof(f1191,plain,
( ~ spl12_142
| spl12_143 ),
inference(avatar_split_clause,[],[f269,f1188,f1184]) ).
fof(f1198,definition,
( spl12_145
<=> e21 = op2(e21,op2(e21,e21)) ),
introduced(definition,[new_symbols(definition,[spl12_145])],[avatar_definition]) ).
fof(f1200,plain,
( e21 = op2(e21,op2(e21,e21))
| ~ spl12_145 ),
inference(avatar_component_clause,[],[f1198]) ).
fof(f1201,plain,
( ~ spl12_142
| spl12_145 ),
inference(avatar_split_clause,[],[f271,f1198,f1184]) ).
fof(f1203,definition,
( spl12_146
<=> e20 = op2(e20,op2(e21,e20)) ),
introduced(definition,[new_symbols(definition,[spl12_146])],[avatar_definition]) ).
fof(f1205,plain,
( e20 = op2(e20,op2(e21,e20))
| ~ spl12_146 ),
inference(avatar_component_clause,[],[f1203]) ).
fof(f1206,plain,
( ~ spl12_142
| spl12_146 ),
inference(avatar_split_clause,[],[f272,f1203,f1184]) ).
fof(f1212,definition,
( spl12_148
<=> e20 = op2(e20,op2(e23,e20)) ),
introduced(definition,[new_symbols(definition,[spl12_148])],[avatar_definition]) ).
fof(f1214,plain,
( e20 = op2(e20,op2(e23,e20))
| ~ spl12_148 ),
inference(avatar_component_clause,[],[f1212]) ).
fof(f1217,definition,
( spl12_149
<=> e22 = op2(e22,op2(e22,e22)) ),
introduced(definition,[new_symbols(definition,[spl12_149])],[avatar_definition]) ).
fof(f1219,plain,
( e22 = op2(e22,op2(e22,e22))
| ~ spl12_149 ),
inference(avatar_component_clause,[],[f1217]) ).
fof(f1220,plain,
( ~ spl12_137
| spl12_142
| spl12_149
| spl12_148 ),
inference(avatar_split_clause,[],[f441,f1212,f1217,f1184,f1160]) ).
fof(f1256,definition,
( spl12_155
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl12_155])],[avatar_definition]) ).
fof(f1260,definition,
( spl12_156
<=> e13 = op1(e13,op1(e10,e13)) ),
introduced(definition,[new_symbols(definition,[spl12_156])],[avatar_definition]) ).
fof(f1262,plain,
( e13 = op1(e13,op1(e10,e13))
| ~ spl12_156 ),
inference(avatar_component_clause,[],[f1260]) ).
fof(f1263,plain,
( ~ spl12_155
| spl12_156 ),
inference(avatar_split_clause,[],[f241,f1260,f1256]) ).
fof(f1265,definition,
( spl12_157
<=> e12 = op1(e12,op1(e10,e12)) ),
introduced(definition,[new_symbols(definition,[spl12_157])],[avatar_definition]) ).
fof(f1267,plain,
( e12 = op1(e12,op1(e10,e12))
| ~ spl12_157 ),
inference(avatar_component_clause,[],[f1265]) ).
fof(f1268,plain,
( ~ spl12_155
| spl12_157 ),
inference(avatar_split_clause,[],[f242,f1265,f1256]) ).
fof(f1270,definition,
( spl12_158
<=> e11 = op1(e11,op1(e10,e11)) ),
introduced(definition,[new_symbols(definition,[spl12_158])],[avatar_definition]) ).
fof(f1272,plain,
( e11 = op1(e11,op1(e10,e11))
| ~ spl12_158 ),
inference(avatar_component_clause,[],[f1270]) ).
fof(f1273,plain,
( ~ spl12_155
| spl12_158 ),
inference(avatar_split_clause,[],[f243,f1270,f1256]) ).
fof(f1280,definition,
( spl12_160
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl12_160])],[avatar_definition]) ).
fof(f1294,definition,
( spl12_163
<=> e11 = op1(e11,op1(e11,e11)) ),
introduced(definition,[new_symbols(definition,[spl12_163])],[avatar_definition]) ).
fof(f1296,plain,
( e11 = op1(e11,op1(e11,e11))
| ~ spl12_163 ),
inference(avatar_component_clause,[],[f1294]) ).
fof(f1297,plain,
( spl12_160
| spl12_163 ),
inference(avatar_split_clause,[],[f424,f1294,f1280]) ).
fof(f1299,definition,
( spl12_164
<=> e10 = op1(e10,op1(e11,e10)) ),
introduced(definition,[new_symbols(definition,[spl12_164])],[avatar_definition]) ).
fof(f1301,plain,
( e10 = op1(e10,op1(e11,e10))
| ~ spl12_164 ),
inference(avatar_component_clause,[],[f1299]) ).
fof(f1302,plain,
( spl12_160
| spl12_164 ),
inference(avatar_split_clause,[],[f423,f1299,f1280]) ).
fof(f1308,definition,
( spl12_166
<=> e10 = op1(e10,op1(e13,e10)) ),
introduced(definition,[new_symbols(definition,[spl12_166])],[avatar_definition]) ).
fof(f1310,plain,
( e10 = op1(e10,op1(e13,e10))
| ~ spl12_166 ),
inference(avatar_component_clause,[],[f1308]) ).
fof(f1313,definition,
( spl12_167
<=> e12 = op1(e12,op1(e12,e12)) ),
introduced(definition,[new_symbols(definition,[spl12_167])],[avatar_definition]) ).
fof(f1315,plain,
( e12 = op1(e12,op1(e12,e12))
| ~ spl12_167 ),
inference(avatar_component_clause,[],[f1313]) ).
fof(f1316,plain,
( spl12_155
| ~ spl12_160
| spl12_167
| spl12_166 ),
inference(avatar_split_clause,[],[f421,f1308,f1313,f1280,f1256]) ).
fof(f1323,definition,
( spl12_169
<=> e10 = op1(e10,op1(e12,e10)) ),
introduced(definition,[new_symbols(definition,[spl12_169])],[avatar_definition]) ).
fof(f1325,plain,
( e10 = op1(e10,op1(e12,e10))
| ~ spl12_169 ),
inference(avatar_component_clause,[],[f1323]) ).
fof(f1326,plain,
( spl12_155
| ~ spl12_160
| spl12_169
| spl12_166 ),
inference(avatar_split_clause,[],[f419,f1308,f1323,f1280,f1256]) ).
fof(f1352,definition,
( spl12_173
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl12_173])],[avatar_definition]) ).
fof(f1353,plain,
( e20 != op2(e20,e20)
| spl12_173 ),
inference(avatar_component_clause,[],[f1352]) ).
fof(f1354,plain,
( e20 = op2(e20,e20)
| ~ spl12_173 ),
inference(avatar_component_clause,[],[f1352]) ).
fof(f1356,definition,
( spl12_174
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_174])],[avatar_definition]) ).
fof(f1358,plain,
( e20 = op2(e20,e21)
| ~ spl12_174 ),
inference(avatar_component_clause,[],[f1356]) ).
fof(f1360,definition,
( spl12_175
<=> e20 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_175])],[avatar_definition]) ).
fof(f1361,plain,
( e20 != op2(e20,e22)
| spl12_175 ),
inference(avatar_component_clause,[],[f1360]) ).
fof(f1364,definition,
( spl12_176
<=> e20 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_176])],[avatar_definition]) ).
fof(f1366,plain,
( e20 = op2(e20,e23)
| ~ spl12_176 ),
inference(avatar_component_clause,[],[f1364]) ).
fof(f1367,plain,
( spl12_173
| spl12_174
| spl12_175
| spl12_176 ),
inference(avatar_split_clause,[],[f85,f1364,f1360,f1356,f1352]) ).
fof(f1369,definition,
( spl12_177
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_177])],[avatar_definition]) ).
fof(f1371,plain,
( e20 = op2(e21,e20)
| ~ spl12_177 ),
inference(avatar_component_clause,[],[f1369]) ).
fof(f1377,definition,
( spl12_179
<=> e20 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_179])],[avatar_definition]) ).
fof(f1379,plain,
( e20 = op2(e23,e20)
| ~ spl12_179 ),
inference(avatar_component_clause,[],[f1377]) ).
fof(f1382,definition,
( spl12_180
<=> op2(e20,e20) = e21 ),
introduced(definition,[new_symbols(definition,[spl12_180])],[avatar_definition]) ).
fof(f1386,definition,
( spl12_181
<=> e21 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_181])],[avatar_definition]) ).
fof(f1388,plain,
( e21 = op2(e20,e21)
| ~ spl12_181 ),
inference(avatar_component_clause,[],[f1386]) ).
fof(f1390,definition,
( spl12_182
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_182])],[avatar_definition]) ).
fof(f1392,plain,
( e21 = op2(e20,e22)
| ~ spl12_182 ),
inference(avatar_component_clause,[],[f1390]) ).
fof(f1394,definition,
( spl12_183
<=> e21 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_183])],[avatar_definition]) ).
fof(f1396,plain,
( e21 = op2(e20,e23)
| ~ spl12_183 ),
inference(avatar_component_clause,[],[f1394]) ).
fof(f1397,plain,
( spl12_180
| spl12_181
| spl12_182
| spl12_183 ),
inference(avatar_split_clause,[],[f87,f1394,f1390,f1386,f1382]) ).
fof(f1399,definition,
( spl12_184
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_184])],[avatar_definition]) ).
fof(f1400,plain,
( e21 != op2(e21,e20)
| spl12_184 ),
inference(avatar_component_clause,[],[f1399]) ).
fof(f1403,definition,
( spl12_185
<=> e21 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_185])],[avatar_definition]) ).
fof(f1405,plain,
( e21 = op2(e22,e20)
| ~ spl12_185 ),
inference(avatar_component_clause,[],[f1403]) ).
fof(f1407,definition,
( spl12_186
<=> e21 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_186])],[avatar_definition]) ).
fof(f1409,plain,
( e21 = op2(e23,e20)
| ~ spl12_186 ),
inference(avatar_component_clause,[],[f1407]) ).
fof(f1412,definition,
( spl12_187
<=> op2(e20,e20) = e22 ),
introduced(definition,[new_symbols(definition,[spl12_187])],[avatar_definition]) ).
fof(f1414,plain,
( op2(e20,e20) = e22
| ~ spl12_187 ),
inference(avatar_component_clause,[],[f1412]) ).
fof(f1416,definition,
( spl12_188
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_188])],[avatar_definition]) ).
fof(f1418,plain,
( e22 = op2(e20,e21)
| ~ spl12_188 ),
inference(avatar_component_clause,[],[f1416]) ).
fof(f1420,definition,
( spl12_189
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_189])],[avatar_definition]) ).
fof(f1422,plain,
( e22 = op2(e20,e22)
| ~ spl12_189 ),
inference(avatar_component_clause,[],[f1420]) ).
fof(f1424,definition,
( spl12_190
<=> e22 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_190])],[avatar_definition]) ).
fof(f1426,plain,
( e22 = op2(e20,e23)
| ~ spl12_190 ),
inference(avatar_component_clause,[],[f1424]) ).
fof(f1427,plain,
( spl12_187
| spl12_188
| spl12_189
| spl12_190 ),
inference(avatar_split_clause,[],[f89,f1424,f1420,f1416,f1412]) ).
fof(f1429,definition,
( spl12_191
<=> e22 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_191])],[avatar_definition]) ).
fof(f1431,plain,
( e22 = op2(e21,e20)
| ~ spl12_191 ),
inference(avatar_component_clause,[],[f1429]) ).
fof(f1433,definition,
( spl12_192
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_192])],[avatar_definition]) ).
fof(f1434,plain,
( e22 != op2(e22,e20)
| spl12_192 ),
inference(avatar_component_clause,[],[f1433]) ).
fof(f1435,plain,
( e22 = op2(e22,e20)
| ~ spl12_192 ),
inference(avatar_component_clause,[],[f1433]) ).
fof(f1437,definition,
( spl12_193
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_193])],[avatar_definition]) ).
fof(f1439,plain,
( e22 = op2(e23,e20)
| ~ spl12_193 ),
inference(avatar_component_clause,[],[f1437]) ).
fof(f1440,plain,
( spl12_187
| spl12_191
| spl12_192
| spl12_193 ),
inference(avatar_split_clause,[],[f90,f1437,f1433,f1429,f1412]) ).
fof(f1446,definition,
( spl12_195
<=> e23 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_195])],[avatar_definition]) ).
fof(f1448,plain,
( e23 = op2(e20,e21)
| ~ spl12_195 ),
inference(avatar_component_clause,[],[f1446]) ).
fof(f1450,definition,
( spl12_196
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_196])],[avatar_definition]) ).
fof(f1459,definition,
( spl12_198
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_198])],[avatar_definition]) ).
fof(f1461,plain,
( e23 = op2(e21,e20)
| ~ spl12_198 ),
inference(avatar_component_clause,[],[f1459]) ).
fof(f1467,definition,
( spl12_200
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_200])],[avatar_definition]) ).
fof(f1469,plain,
( e23 = op2(e23,e20)
| ~ spl12_200 ),
inference(avatar_component_clause,[],[f1467]) ).
fof(f1472,definition,
( spl12_201
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_201])],[avatar_definition]) ).
fof(f1474,plain,
( e20 = op2(e21,e21)
| ~ spl12_201 ),
inference(avatar_component_clause,[],[f1472]) ).
fof(f1476,definition,
( spl12_202
<=> e20 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_202])],[avatar_definition]) ).
fof(f1480,definition,
( spl12_203
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_203])],[avatar_definition]) ).
fof(f1482,plain,
( e20 = op2(e21,e23)
| ~ spl12_203 ),
inference(avatar_component_clause,[],[f1480]) ).
fof(f1483,plain,
( spl12_177
| spl12_201
| spl12_202
| spl12_203 ),
inference(avatar_split_clause,[],[f93,f1480,f1476,f1472,f1369]) ).
fof(f1485,definition,
( spl12_204
<=> e20 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_204])],[avatar_definition]) ).
fof(f1494,definition,
( spl12_206
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_206])],[avatar_definition]) ).
fof(f1496,plain,
( e21 = op2(e21,e21)
| ~ spl12_206 ),
inference(avatar_component_clause,[],[f1494]) ).
fof(f1498,definition,
( spl12_207
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_207])],[avatar_definition]) ).
fof(f1500,plain,
( e21 = op2(e21,e22)
| ~ spl12_207 ),
inference(avatar_component_clause,[],[f1498]) ).
fof(f1502,definition,
( spl12_208
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_208])],[avatar_definition]) ).
fof(f1504,plain,
( e21 = op2(e21,e23)
| ~ spl12_208 ),
inference(avatar_component_clause,[],[f1502]) ).
fof(f1505,plain,
( spl12_184
| spl12_206
| spl12_207
| spl12_208 ),
inference(avatar_split_clause,[],[f95,f1502,f1498,f1494,f1399]) ).
fof(f1507,definition,
( spl12_209
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_209])],[avatar_definition]) ).
fof(f1511,definition,
( spl12_210
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_210])],[avatar_definition]) ).
fof(f1513,plain,
( e21 = op2(e23,e21)
| ~ spl12_210 ),
inference(avatar_component_clause,[],[f1511]) ).
fof(f1514,plain,
( spl12_181
| spl12_206
| spl12_209
| spl12_210 ),
inference(avatar_split_clause,[],[f96,f1511,f1507,f1494,f1386]) ).
fof(f1520,definition,
( spl12_212
<=> e22 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_212])],[avatar_definition]) ).
fof(f1522,plain,
( e22 = op2(e21,e22)
| ~ spl12_212 ),
inference(avatar_component_clause,[],[f1520]) ).
fof(f1529,definition,
( spl12_214
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_214])],[avatar_definition]) ).
fof(f1531,plain,
( e22 = op2(e22,e21)
| ~ spl12_214 ),
inference(avatar_component_clause,[],[f1529]) ).
fof(f1551,definition,
( spl12_219
<=> e23 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_219])],[avatar_definition]) ).
fof(f1555,definition,
( spl12_220
<=> e23 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_220])],[avatar_definition]) ).
fof(f1557,plain,
( e23 = op2(e23,e21)
| ~ spl12_220 ),
inference(avatar_component_clause,[],[f1555]) ).
fof(f1560,definition,
( spl12_221
<=> e20 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_221])],[avatar_definition]) ).
fof(f1562,plain,
( e20 = op2(e22,e22)
| ~ spl12_221 ),
inference(avatar_component_clause,[],[f1560]) ).
fof(f1564,definition,
( spl12_222
<=> e20 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_222])],[avatar_definition]) ).
fof(f1569,definition,
( spl12_223
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_223])],[avatar_definition]) ).
fof(f1574,definition,
( spl12_224
<=> e21 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_224])],[avatar_definition]) ).
fof(f1576,plain,
( e21 = op2(e22,e22)
| ~ spl12_224 ),
inference(avatar_component_clause,[],[f1574]) ).
fof(f1578,definition,
( spl12_225
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_225])],[avatar_definition]) ).
fof(f1580,plain,
( e21 = op2(e22,e23)
| ~ spl12_225 ),
inference(avatar_component_clause,[],[f1578]) ).
fof(f1583,definition,
( spl12_226
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_226])],[avatar_definition]) ).
fof(f1585,plain,
( e21 = op2(e23,e22)
| ~ spl12_226 ),
inference(avatar_component_clause,[],[f1583]) ).
fof(f1586,plain,
( spl12_182
| spl12_207
| spl12_224
| spl12_226 ),
inference(avatar_split_clause,[],[f104,f1583,f1574,f1498,f1390]) ).
fof(f1588,definition,
( spl12_227
<=> e22 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_227])],[avatar_definition]) ).
fof(f1589,plain,
( e22 != op2(e22,e22)
| spl12_227 ),
inference(avatar_component_clause,[],[f1588]) ).
fof(f1590,plain,
( e22 = op2(e22,e22)
| ~ spl12_227 ),
inference(avatar_component_clause,[],[f1588]) ).
fof(f1592,definition,
( spl12_228
<=> e22 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_228])],[avatar_definition]) ).
fof(f1597,definition,
( spl12_229
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_229])],[avatar_definition]) ).
fof(f1599,plain,
( e22 = op2(e23,e22)
| ~ spl12_229 ),
inference(avatar_component_clause,[],[f1597]) ).
fof(f1600,plain,
( spl12_189
| spl12_212
| spl12_227
| spl12_229 ),
inference(avatar_split_clause,[],[f106,f1597,f1588,f1520,f1420]) ).
fof(f1606,definition,
( spl12_231
<=> e23 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_231])],[avatar_definition]) ).
fof(f1608,plain,
( e23 = op2(e22,e23)
| ~ spl12_231 ),
inference(avatar_component_clause,[],[f1606]) ).
fof(f1611,definition,
( spl12_232
<=> e23 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_232])],[avatar_definition]) ).
fof(f1613,plain,
( e23 = op2(e23,e22)
| ~ spl12_232 ),
inference(avatar_component_clause,[],[f1611]) ).
fof(f1616,definition,
( spl12_233
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_233])],[avatar_definition]) ).
fof(f1618,plain,
( e20 = op2(e23,e23)
| ~ spl12_233 ),
inference(avatar_component_clause,[],[f1616]) ).
fof(f1620,plain,
( spl12_176
| spl12_203
| spl12_222
| spl12_233 ),
inference(avatar_split_clause,[],[f110,f1616,f1564,f1480,f1364]) ).
fof(f1640,plain,
( spl12_174
| spl12_181
| spl12_188
| spl12_195 ),
inference(avatar_split_clause,[],[f70,f1446,f1416,f1386,f1356]) ).
fof(f1641,plain,
( spl12_175
| spl12_182
| spl12_189
| spl12_196 ),
inference(avatar_split_clause,[],[f71,f1450,f1420,f1390,f1360]) ).
fof(f1648,plain,
( spl12_204
| spl12_209
| spl12_214
| spl12_219 ),
inference(avatar_split_clause,[],[f78,f1551,f1529,f1507,f1485]) ).
fof(f1650,plain,
( spl12_222
| spl12_225
| spl12_228
| spl12_231 ),
inference(avatar_split_clause,[],[f80,f1606,f1592,f1578,f1564]) ).
fof(f1651,plain,
( spl12_179
| spl12_186
| spl12_193
| spl12_200 ),
inference(avatar_split_clause,[],[f81,f1467,f1437,f1407,f1377]) ).
fof(f1653,plain,
( spl12_223
| spl12_226
| spl12_229
| spl12_232 ),
inference(avatar_split_clause,[],[f83,f1611,f1597,f1583,f1569]) ).
fof(f1656,definition,
( spl12_237
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl12_237])],[avatar_definition]) ).
fof(f1657,plain,
( e10 != op1(e10,e10)
| spl12_237 ),
inference(avatar_component_clause,[],[f1656]) ).
fof(f1658,plain,
( e10 = op1(e10,e10)
| ~ spl12_237 ),
inference(avatar_component_clause,[],[f1656]) ).
fof(f1660,definition,
( spl12_238
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_238])],[avatar_definition]) ).
fof(f1662,plain,
( e10 = op1(e10,e11)
| ~ spl12_238 ),
inference(avatar_component_clause,[],[f1660]) ).
fof(f1664,definition,
( spl12_239
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_239])],[avatar_definition]) ).
fof(f1665,plain,
( e10 != op1(e10,e12)
| spl12_239 ),
inference(avatar_component_clause,[],[f1664]) ).
fof(f1668,definition,
( spl12_240
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_240])],[avatar_definition]) ).
fof(f1670,plain,
( e10 = op1(e10,e13)
| ~ spl12_240 ),
inference(avatar_component_clause,[],[f1668]) ).
fof(f1673,definition,
( spl12_241
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl12_241])],[avatar_definition]) ).
fof(f1675,plain,
( e10 = op1(e11,e10)
| ~ spl12_241 ),
inference(avatar_component_clause,[],[f1673]) ).
fof(f1677,definition,
( spl12_242
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_242])],[avatar_definition]) ).
fof(f1681,definition,
( spl12_243
<=> e10 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_243])],[avatar_definition]) ).
fof(f1683,plain,
( e10 = op1(e13,e10)
| ~ spl12_243 ),
inference(avatar_component_clause,[],[f1681]) ).
fof(f1684,plain,
( spl12_237
| spl12_241
| spl12_242
| spl12_243 ),
inference(avatar_split_clause,[],[f38,f1681,f1677,f1673,f1656]) ).
fof(f1686,definition,
( spl12_244
<=> op1(e10,e10) = e11 ),
introduced(definition,[new_symbols(definition,[spl12_244])],[avatar_definition]) ).
fof(f1690,definition,
( spl12_245
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_245])],[avatar_definition]) ).
fof(f1692,plain,
( e11 = op1(e10,e11)
| ~ spl12_245 ),
inference(avatar_component_clause,[],[f1690]) ).
fof(f1694,definition,
( spl12_246
<=> e11 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_246])],[avatar_definition]) ).
fof(f1696,plain,
( e11 = op1(e10,e12)
| ~ spl12_246 ),
inference(avatar_component_clause,[],[f1694]) ).
fof(f1698,definition,
( spl12_247
<=> e11 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_247])],[avatar_definition]) ).
fof(f1700,plain,
( e11 = op1(e10,e13)
| ~ spl12_247 ),
inference(avatar_component_clause,[],[f1698]) ).
fof(f1701,plain,
( spl12_244
| spl12_245
| spl12_246
| spl12_247 ),
inference(avatar_split_clause,[],[f39,f1698,f1694,f1690,f1686]) ).
fof(f1703,definition,
( spl12_248
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl12_248])],[avatar_definition]) ).
fof(f1704,plain,
( e11 != op1(e11,e10)
| spl12_248 ),
inference(avatar_component_clause,[],[f1703]) ).
fof(f1707,definition,
( spl12_249
<=> e11 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_249])],[avatar_definition]) ).
fof(f1709,plain,
( e11 = op1(e12,e10)
| ~ spl12_249 ),
inference(avatar_component_clause,[],[f1707]) ).
fof(f1711,definition,
( spl12_250
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_250])],[avatar_definition]) ).
fof(f1713,plain,
( e11 = op1(e13,e10)
| ~ spl12_250 ),
inference(avatar_component_clause,[],[f1711]) ).
fof(f1716,definition,
( spl12_251
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[spl12_251])],[avatar_definition]) ).
fof(f1724,definition,
( spl12_253
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_253])],[avatar_definition]) ).
fof(f1726,plain,
( e12 = op1(e10,e12)
| ~ spl12_253 ),
inference(avatar_component_clause,[],[f1724]) ).
fof(f1728,definition,
( spl12_254
<=> e12 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_254])],[avatar_definition]) ).
fof(f1730,plain,
( e12 = op1(e10,e13)
| ~ spl12_254 ),
inference(avatar_component_clause,[],[f1728]) ).
fof(f1733,definition,
( spl12_255
<=> e12 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl12_255])],[avatar_definition]) ).
fof(f1735,plain,
( e12 = op1(e11,e10)
| ~ spl12_255 ),
inference(avatar_component_clause,[],[f1733]) ).
fof(f1737,definition,
( spl12_256
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_256])],[avatar_definition]) ).
fof(f1738,plain,
( e12 != op1(e12,e10)
| spl12_256 ),
inference(avatar_component_clause,[],[f1737]) ).
fof(f1739,plain,
( e12 = op1(e12,e10)
| ~ spl12_256 ),
inference(avatar_component_clause,[],[f1737]) ).
fof(f1741,definition,
( spl12_257
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_257])],[avatar_definition]) ).
fof(f1743,plain,
( e12 = op1(e13,e10)
| ~ spl12_257 ),
inference(avatar_component_clause,[],[f1741]) ).
fof(f1746,definition,
( spl12_258
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl12_258])],[avatar_definition]) ).
fof(f1750,definition,
( spl12_259
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_259])],[avatar_definition]) ).
fof(f1752,plain,
( e13 = op1(e10,e11)
| ~ spl12_259 ),
inference(avatar_component_clause,[],[f1750]) ).
fof(f1754,definition,
( spl12_260
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_260])],[avatar_definition]) ).
fof(f1756,plain,
( e13 = op1(e10,e12)
| ~ spl12_260 ),
inference(avatar_component_clause,[],[f1754]) ).
fof(f1758,definition,
( spl12_261
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_261])],[avatar_definition]) ).
fof(f1760,plain,
( e13 = op1(e10,e13)
| ~ spl12_261 ),
inference(avatar_component_clause,[],[f1758]) ).
fof(f1761,plain,
( spl12_258
| spl12_259
| spl12_260
| spl12_261 ),
inference(avatar_split_clause,[],[f43,f1758,f1754,f1750,f1746]) ).
fof(f1763,definition,
( spl12_262
<=> e13 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl12_262])],[avatar_definition]) ).
fof(f1765,plain,
( e13 = op1(e11,e10)
| ~ spl12_262 ),
inference(avatar_component_clause,[],[f1763]) ).
fof(f1767,definition,
( spl12_263
<=> e13 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_263])],[avatar_definition]) ).
fof(f1769,plain,
( e13 = op1(e12,e10)
| ~ spl12_263 ),
inference(avatar_component_clause,[],[f1767]) ).
fof(f1771,definition,
( spl12_264
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_264])],[avatar_definition]) ).
fof(f1776,definition,
( spl12_265
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_265])],[avatar_definition]) ).
fof(f1778,plain,
( e10 = op1(e11,e11)
| ~ spl12_265 ),
inference(avatar_component_clause,[],[f1776]) ).
fof(f1780,definition,
( spl12_266
<=> e10 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_266])],[avatar_definition]) ).
fof(f1784,definition,
( spl12_267
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_267])],[avatar_definition]) ).
fof(f1786,plain,
( e10 = op1(e11,e13)
| ~ spl12_267 ),
inference(avatar_component_clause,[],[f1784]) ).
fof(f1787,plain,
( spl12_241
| spl12_265
| spl12_266
| spl12_267 ),
inference(avatar_split_clause,[],[f45,f1784,f1780,f1776,f1673]) ).
fof(f1789,definition,
( spl12_268
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_268])],[avatar_definition]) ).
fof(f1793,definition,
( spl12_269
<=> e10 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_269])],[avatar_definition]) ).
fof(f1795,plain,
( e10 = op1(e13,e11)
| ~ spl12_269 ),
inference(avatar_component_clause,[],[f1793]) ).
fof(f1796,plain,
( spl12_238
| spl12_265
| spl12_268
| spl12_269 ),
inference(avatar_split_clause,[],[f46,f1793,f1789,f1776,f1660]) ).
fof(f1798,definition,
( spl12_270
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_270])],[avatar_definition]) ).
fof(f1799,plain,
( e11 != op1(e11,e11)
| spl12_270 ),
inference(avatar_component_clause,[],[f1798]) ).
fof(f1802,definition,
( spl12_271
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_271])],[avatar_definition]) ).
fof(f1804,plain,
( e11 = op1(e11,e12)
| ~ spl12_271 ),
inference(avatar_component_clause,[],[f1802]) ).
fof(f1806,definition,
( spl12_272
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_272])],[avatar_definition]) ).
fof(f1808,plain,
( e11 = op1(e11,e13)
| ~ spl12_272 ),
inference(avatar_component_clause,[],[f1806]) ).
fof(f1811,definition,
( spl12_273
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_273])],[avatar_definition]) ).
fof(f1815,definition,
( spl12_274
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_274])],[avatar_definition]) ).
fof(f1817,plain,
( e11 = op1(e13,e11)
| ~ spl12_274 ),
inference(avatar_component_clause,[],[f1815]) ).
fof(f1818,plain,
( spl12_245
| spl12_270
| spl12_273
| spl12_274 ),
inference(avatar_split_clause,[],[f48,f1815,f1811,f1798,f1690]) ).
fof(f1820,definition,
( spl12_275
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_275])],[avatar_definition]) ).
fof(f1824,definition,
( spl12_276
<=> e12 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_276])],[avatar_definition]) ).
fof(f1826,plain,
( e12 = op1(e11,e12)
| ~ spl12_276 ),
inference(avatar_component_clause,[],[f1824]) ).
fof(f1828,definition,
( spl12_277
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_277])],[avatar_definition]) ).
fof(f1830,plain,
( e12 = op1(e11,e13)
| ~ spl12_277 ),
inference(avatar_component_clause,[],[f1828]) ).
fof(f1831,plain,
( spl12_255
| spl12_275
| spl12_276
| spl12_277 ),
inference(avatar_split_clause,[],[f49,f1828,f1824,f1820,f1733]) ).
fof(f1833,definition,
( spl12_278
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_278])],[avatar_definition]) ).
fof(f1835,plain,
( e12 = op1(e12,e11)
| ~ spl12_278 ),
inference(avatar_component_clause,[],[f1833]) ).
fof(f1855,definition,
( spl12_283
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_283])],[avatar_definition]) ).
fof(f1857,plain,
( e13 = op1(e12,e11)
| ~ spl12_283 ),
inference(avatar_component_clause,[],[f1855]) ).
fof(f1859,definition,
( spl12_284
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_284])],[avatar_definition]) ).
fof(f1860,plain,
( e13 != op1(e13,e11)
| spl12_284 ),
inference(avatar_component_clause,[],[f1859]) ).
fof(f1861,plain,
( e13 = op1(e13,e11)
| ~ spl12_284 ),
inference(avatar_component_clause,[],[f1859]) ).
fof(f1864,definition,
( spl12_285
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_285])],[avatar_definition]) ).
fof(f1866,plain,
( e10 = op1(e12,e12)
| ~ spl12_285 ),
inference(avatar_component_clause,[],[f1864]) ).
fof(f1868,definition,
( spl12_286
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_286])],[avatar_definition]) ).
fof(f1873,definition,
( spl12_287
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_287])],[avatar_definition]) ).
fof(f1878,definition,
( spl12_288
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_288])],[avatar_definition]) ).
fof(f1880,plain,
( e11 = op1(e12,e12)
| ~ spl12_288 ),
inference(avatar_component_clause,[],[f1878]) ).
fof(f1887,definition,
( spl12_290
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_290])],[avatar_definition]) ).
fof(f1889,plain,
( e11 = op1(e13,e12)
| ~ spl12_290 ),
inference(avatar_component_clause,[],[f1887]) ).
fof(f1890,plain,
( spl12_246
| spl12_271
| spl12_288
| spl12_290 ),
inference(avatar_split_clause,[],[f56,f1887,f1878,f1802,f1694]) ).
fof(f1896,definition,
( spl12_292
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_292])],[avatar_definition]) ).
fof(f1898,plain,
( e12 = op1(e12,e13)
| ~ spl12_292 ),
inference(avatar_component_clause,[],[f1896]) ).
fof(f1901,definition,
( spl12_293
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_293])],[avatar_definition]) ).
fof(f1903,plain,
( e12 = op1(e13,e12)
| ~ spl12_293 ),
inference(avatar_component_clause,[],[f1901]) ).
fof(f1906,definition,
( spl12_294
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_294])],[avatar_definition]) ).
fof(f1908,plain,
( e13 = op1(e12,e12)
| ~ spl12_294 ),
inference(avatar_component_clause,[],[f1906]) ).
fof(f1910,definition,
( spl12_295
<=> e13 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_295])],[avatar_definition]) ).
fof(f1912,plain,
( e13 = op1(e12,e13)
| ~ spl12_295 ),
inference(avatar_component_clause,[],[f1910]) ).
fof(f1913,plain,
( spl12_263
| spl12_283
| spl12_294
| spl12_295 ),
inference(avatar_split_clause,[],[f59,f1910,f1906,f1855,f1767]) ).
fof(f1915,definition,
( spl12_296
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_296])],[avatar_definition]) ).
fof(f1917,plain,
( e13 = op1(e13,e12)
| ~ spl12_296 ),
inference(avatar_component_clause,[],[f1915]) ).
fof(f1920,definition,
( spl12_297
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_297])],[avatar_definition]) ).
fof(f1922,plain,
( e10 = op1(e13,e13)
| ~ spl12_297 ),
inference(avatar_component_clause,[],[f1920]) ).
fof(f1924,plain,
( spl12_240
| spl12_267
| spl12_286
| spl12_297 ),
inference(avatar_split_clause,[],[f62,f1920,f1868,f1784,f1668]) ).
fof(f1932,definition,
( spl12_299
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_299])],[avatar_definition]) ).
fof(f1934,plain,
( e12 = op1(e13,e13)
| ~ spl12_299 ),
inference(avatar_component_clause,[],[f1932]) ).
fof(f1936,plain,
( spl12_254
| spl12_277
| spl12_292
| spl12_299 ),
inference(avatar_split_clause,[],[f66,f1932,f1896,f1828,f1728]) ).
fof(f1938,definition,
( spl12_300
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_300])],[avatar_definition]) ).
fof(f1939,plain,
( e13 != op1(e13,e13)
| spl12_300 ),
inference(avatar_component_clause,[],[f1938]) ).
fof(f1943,plain,
( spl12_237
| spl12_244
| spl12_251
| spl12_258 ),
inference(avatar_split_clause,[],[f21,f1746,f1716,f1686,f1656]) ).
fof(f1945,plain,
( spl12_239
| spl12_246
| spl12_253
| spl12_260 ),
inference(avatar_split_clause,[],[f23,f1754,f1724,f1694,f1664]) ).
fof(f1946,plain,
( spl12_240
| spl12_247
| spl12_254
| spl12_261 ),
inference(avatar_split_clause,[],[f24,f1758,f1728,f1698,f1668]) ).
fof(f1952,plain,
( spl12_268
| spl12_273
| spl12_278
| spl12_283 ),
inference(avatar_split_clause,[],[f30,f1855,f1833,f1811,f1789]) ).
fof(f1955,plain,
( spl12_243
| spl12_250
| spl12_257
| spl12_264 ),
inference(avatar_split_clause,[],[f33,f1771,f1741,f1711,f1681]) ).
fof(f1957,plain,
( spl12_287
| spl12_290
| spl12_293
| spl12_296 ),
inference(avatar_split_clause,[],[f35,f1915,f1901,f1887,f1873]) ).
fof(f1959,plain,
( e20 != e21
| ~ spl12_3
| spl12_8 ),
inference(forward_demodulation,[],[f551,f526]) ).
fof(f1960,plain,
( e21 != e22
| spl12_28
| ~ spl12_107 ),
inference(superposition,[],[f647,f1006]) ).
fof(f1963,plain,
( h2(op1(e12,e11)) != op2(e21,h2(e11))
| ~ spl12_18
| spl12_74 ),
inference(forward_demodulation,[],[f858,f598]) ).
fof(f1964,plain,
spl12_285,
inference(avatar_split_clause,[],[f291,f1864]) ).
fof(f1965,plain,
spl12_221,
inference(avatar_split_clause,[],[f294,f1560]) ).
fof(f1966,plain,
( e21 = e22
| ~ spl12_181
| ~ spl12_188 ),
inference(superposition,[],[f1418,f1388]) ).
fof(f1970,plain,
( $false
| spl12_28
| ~ spl12_107
| ~ spl12_181
| ~ spl12_188 ),
inference(forward_subsumption_resolution,[],[f1966,f1960]) ).
fof(f1971,plain,
( spl12_28
| ~ spl12_107
| ~ spl12_181
| ~ spl12_188 ),
inference(avatar_contradiction_clause,[],[f1970]) ).
fof(f1972,plain,
( e21 = e22
| ~ spl12_28
| ~ spl12_107 ),
inference(forward_demodulation,[],[f646,f1006]) ).
fof(f1985,plain,
( $false
| ~ spl12_28
| ~ spl12_107 ),
inference(forward_subsumption_resolution,[],[f221,f1972]) ).
fof(f1986,plain,
( ~ spl12_28
| ~ spl12_107 ),
inference(avatar_contradiction_clause,[],[f1985]) ).
fof(f1987,plain,
( e21 != e22
| spl12_28
| ~ spl12_107 ),
inference(forward_demodulation,[],[f647,f1006]) ).
fof(f2006,plain,
( e20 = e21
| ~ spl12_3
| ~ spl12_8 ),
inference(forward_demodulation,[],[f550,f526]) ).
fof(f2039,plain,
( $false
| ~ spl12_3
| ~ spl12_8 ),
inference(forward_subsumption_resolution,[],[f224,f2006]) ).
fof(f2040,plain,
( ~ spl12_3
| ~ spl12_8 ),
inference(avatar_contradiction_clause,[],[f2039]) ).
fof(f2051,plain,
( e20 = e22
| ~ spl12_173
| ~ spl12_187 ),
inference(superposition,[],[f1414,f1354]) ).
fof(f2055,plain,
( $false
| ~ spl12_173
| ~ spl12_187 ),
inference(forward_subsumption_resolution,[],[f2051,f223]) ).
fof(f2056,plain,
( ~ spl12_173
| ~ spl12_187 ),
inference(avatar_contradiction_clause,[],[f2055]) ).
fof(f2067,plain,
( e21 = e22
| ~ spl12_185
| ~ spl12_192 ),
inference(superposition,[],[f1435,f1405]) ).
fof(f2071,plain,
( $false
| spl12_28
| ~ spl12_107
| ~ spl12_185
| ~ spl12_192 ),
inference(forward_subsumption_resolution,[],[f2067,f1987]) ).
fof(f2072,plain,
( spl12_28
| ~ spl12_107
| ~ spl12_185
| ~ spl12_192 ),
inference(avatar_contradiction_clause,[],[f2071]) ).
fof(f2157,plain,
( e22 = e23
| ~ spl12_191
| ~ spl12_198 ),
inference(forward_demodulation,[],[f1461,f1431]) ).
fof(f2158,plain,
( $false
| ~ spl12_191
| ~ spl12_198 ),
inference(forward_subsumption_resolution,[],[f2157,f219]) ).
fof(f2159,plain,
( ~ spl12_191
| ~ spl12_198 ),
inference(avatar_contradiction_clause,[],[f2158]) ).
fof(f2194,plain,
( e20 = e21
| ~ spl12_201
| ~ spl12_206 ),
inference(forward_demodulation,[],[f1496,f1474]) ).
fof(f2195,plain,
( $false
| ~ spl12_3
| spl12_8
| ~ spl12_201
| ~ spl12_206 ),
inference(forward_subsumption_resolution,[],[f2194,f1959]) ).
fof(f2196,plain,
( ~ spl12_3
| spl12_8
| ~ spl12_201
| ~ spl12_206 ),
inference(avatar_contradiction_clause,[],[f2195]) ).
fof(f2202,plain,
( e20 = e21
| ~ spl12_203
| ~ spl12_208 ),
inference(forward_demodulation,[],[f1504,f1482]) ).
fof(f2203,plain,
( $false
| ~ spl12_3
| spl12_8
| ~ spl12_203
| ~ spl12_208 ),
inference(forward_subsumption_resolution,[],[f2202,f1959]) ).
fof(f2204,plain,
( ~ spl12_3
| spl12_8
| ~ spl12_203
| ~ spl12_208 ),
inference(avatar_contradiction_clause,[],[f2203]) ).
fof(f2222,plain,
( e21 = e22
| ~ spl12_207
| ~ spl12_212 ),
inference(superposition,[],[f1522,f1500]) ).
fof(f2227,plain,
( $false
| spl12_28
| ~ spl12_107
| ~ spl12_207
| ~ spl12_212 ),
inference(forward_subsumption_resolution,[],[f2222,f1987]) ).
fof(f2228,plain,
( spl12_28
| ~ spl12_107
| ~ spl12_207
| ~ spl12_212 ),
inference(avatar_contradiction_clause,[],[f2227]) ).
fof(f2419,plain,
( e11 = e12
| ~ spl12_249
| ~ spl12_256 ),
inference(superposition,[],[f1739,f1709]) ).
fof(f2423,plain,
( $false
| ~ spl12_249
| ~ spl12_256 ),
inference(forward_subsumption_resolution,[],[f2419,f215]) ).
fof(f2424,plain,
( ~ spl12_249
| ~ spl12_256 ),
inference(avatar_contradiction_clause,[],[f2423]) ).
fof(f2486,plain,
( e10 = e11
| ~ spl12_267
| ~ spl12_272 ),
inference(forward_demodulation,[],[f1808,f1786]) ).
fof(f2487,plain,
( $false
| ~ spl12_267
| ~ spl12_272 ),
inference(forward_subsumption_resolution,[],[f2486,f218]) ).
fof(f2488,plain,
( ~ spl12_267
| ~ spl12_272 ),
inference(avatar_contradiction_clause,[],[f2487]) ).
fof(f2499,plain,
( e11 = e12
| ~ spl12_272
| ~ spl12_277 ),
inference(superposition,[],[f1830,f1808]) ).
fof(f2504,plain,
( $false
| ~ spl12_272
| ~ spl12_277 ),
inference(forward_subsumption_resolution,[],[f2499,f215]) ).
fof(f2505,plain,
( ~ spl12_272
| ~ spl12_277 ),
inference(avatar_contradiction_clause,[],[f2504]) ).
fof(f2532,plain,
( e10 = e11
| ~ spl12_238
| ~ spl12_245 ),
inference(superposition,[],[f1662,f1692]) ).
fof(f2538,plain,
( $false
| ~ spl12_238
| ~ spl12_245 ),
inference(forward_subsumption_resolution,[],[f2532,f218]) ).
fof(f2539,plain,
( ~ spl12_238
| ~ spl12_245 ),
inference(avatar_contradiction_clause,[],[f2538]) ).
fof(f2584,plain,
( e11 = e13
| ~ spl12_249
| ~ spl12_263 ),
inference(forward_demodulation,[],[f1709,f1769]) ).
fof(f2585,plain,
( $false
| ~ spl12_249
| ~ spl12_263 ),
inference(forward_subsumption_resolution,[],[f2584,f214]) ).
fof(f2586,plain,
( ~ spl12_249
| ~ spl12_263 ),
inference(avatar_contradiction_clause,[],[f2585]) ).
fof(f2600,plain,
( e10 = e11
| ~ spl12_285
| ~ spl12_288 ),
inference(forward_demodulation,[],[f1880,f1866]) ).
fof(f2601,plain,
( $false
| ~ spl12_285
| ~ spl12_288 ),
inference(forward_subsumption_resolution,[],[f2600,f218]) ).
fof(f2602,plain,
( ~ spl12_285
| ~ spl12_288 ),
inference(avatar_contradiction_clause,[],[f2601]) ).
fof(f2627,plain,
( e10 = e13
| ~ spl12_285
| ~ spl12_294 ),
inference(superposition,[],[f1908,f1866]) ).
fof(f2631,plain,
( $false
| ~ spl12_285
| ~ spl12_294 ),
inference(forward_subsumption_resolution,[],[f2627,f216]) ).
fof(f2632,plain,
( ~ spl12_285
| ~ spl12_294 ),
inference(avatar_contradiction_clause,[],[f2631]) ).
fof(f2735,plain,
( e10 != op1(e12,e11)
| ~ spl12_285 ),
inference(forward_demodulation,[],[f125,f1866]) ).
fof(f2738,plain,
( e10 != op1(e12,e10)
| ~ spl12_285 ),
inference(forward_demodulation,[],[f127,f1866]) ).
fof(f2755,plain,
( op1(e10,e10) != e12
| ~ spl12_253 ),
inference(forward_demodulation,[],[f139,f1726]) ).
fof(f2770,plain,
( e10 != op1(e11,e12)
| ~ spl12_285 ),
inference(forward_demodulation,[],[f149,f1866]) ).
fof(f2771,plain,
( e13 != op1(e10,e12)
| ~ spl12_296 ),
inference(forward_demodulation,[],[f150,f1917]) ).
fof(f2773,plain,
( e10 != op1(e10,e12)
| ~ spl12_285 ),
inference(forward_demodulation,[],[f151,f1866]) ).
fof(f2785,plain,
( e13 != op1(e10,e11)
| ~ spl12_283 ),
inference(forward_demodulation,[],[f157,f1857]) ).
fof(f2786,plain,
( e10 != op1(e10,e11)
| ~ spl12_265 ),
inference(forward_demodulation,[],[f158,f1778]) ).
fof(f2787,plain,
( e11 != op1(e12,e10)
| ~ spl12_250 ),
inference(forward_demodulation,[],[f159,f1713]) ).
fof(f2793,plain,
( op1(e10,e10) != e13
| ~ spl12_262 ),
inference(forward_demodulation,[],[f164,f1765]) ).
fof(f2808,plain,
( e20 != op2(e22,e21)
| ~ spl12_221 ),
inference(forward_demodulation,[],[f173,f1562]) ).
fof(f2810,plain,
( e21 != op2(e22,e20)
| ~ spl12_225 ),
inference(forward_demodulation,[],[f174,f1580]) ).
fof(f2841,plain,
( e20 != op2(e21,e22)
| ~ spl12_221 ),
inference(forward_demodulation,[],[f197,f1562]) ).
fof(f2842,plain,
( e23 != op2(e20,e22)
| ~ spl12_232 ),
inference(forward_demodulation,[],[f198,f1613]) ).
fof(f2844,plain,
( e20 != op2(e20,e22)
| ~ spl12_221 ),
inference(forward_demodulation,[],[f199,f1562]) ).
fof(f2851,plain,
( e22 != op2(e20,e21)
| ~ spl12_214 ),
inference(forward_demodulation,[],[f205,f1531]) ).
fof(f2853,plain,
( e21 != op2(e22,e20)
| ~ spl12_186 ),
inference(forward_demodulation,[],[f207,f1409]) ).
fof(f2862,plain,
( e11 = op1(e12,e10)
| ~ spl12_285 ),
inference(forward_demodulation,[],[f290,f1866]) ).
fof(f2866,plain,
( e10 = e13
| ~ spl12_241
| ~ spl12_262 ),
inference(forward_demodulation,[],[f1675,f1765]) ).
fof(f2867,plain,
( ~ spl12_242
| ~ spl12_285 ),
inference(avatar_split_clause,[],[f2738,f1864,f1677]) ).
fof(f2870,plain,
( ~ spl12_251
| ~ spl12_253 ),
inference(avatar_split_clause,[],[f2755,f1724,f1716]) ).
fof(f2872,plain,
( ~ spl12_249
| ~ spl12_250 ),
inference(avatar_split_clause,[],[f2787,f1711,f1707]) ).
fof(f2873,plain,
( spl12_249
| ~ spl12_285 ),
inference(avatar_split_clause,[],[f2862,f1864,f1707]) ).
fof(f2878,plain,
( $false
| ~ spl12_241
| ~ spl12_262 ),
inference(forward_subsumption_resolution,[],[f2866,f216]) ).
fof(f2879,plain,
( ~ spl12_241
| ~ spl12_262 ),
inference(avatar_contradiction_clause,[],[f2878]) ).
fof(f2885,plain,
( e13 != op1(e13,e13)
| ~ spl12_261 ),
inference(forward_demodulation,[],[f144,f1760]) ).
fof(f2886,plain,
( e10 != op1(e12,e13)
| ~ spl12_285 ),
inference(forward_demodulation,[],[f123,f1866]) ).
fof(f2892,plain,
( ~ spl12_260
| ~ spl12_296 ),
inference(avatar_split_clause,[],[f2771,f1915,f1754]) ).
fof(f2893,plain,
( ~ spl12_239
| ~ spl12_285 ),
inference(avatar_split_clause,[],[f2773,f1864,f1664]) ).
fof(f2895,plain,
( e13 != op1(e13,e10)
| ~ spl12_262 ),
inference(forward_demodulation,[],[f160,f1765]) ).
fof(f2899,plain,
( ~ spl12_300
| ~ spl12_261 ),
inference(avatar_split_clause,[],[f2885,f1758,f1938]) ).
fof(f2900,plain,
( ~ spl12_286
| ~ spl12_285 ),
inference(avatar_split_clause,[],[f2886,f1864,f1868]) ).
fof(f2903,plain,
( e10 != op1(e13,e12)
| ~ spl12_285 ),
inference(forward_demodulation,[],[f147,f1866]) ).
fof(f2907,plain,
( ~ spl12_287
| ~ spl12_285 ),
inference(avatar_split_clause,[],[f2903,f1864,f1873]) ).
fof(f2911,plain,
( ~ spl12_268
| ~ spl12_285 ),
inference(avatar_split_clause,[],[f2735,f1864,f1789]) ).
fof(f2935,plain,
( h2(e12) != op2(e21,h2(e11))
| ~ spl12_18
| spl12_74
| ~ spl12_278 ),
inference(superposition,[],[f1963,f1835]) ).
fof(f2936,plain,
( e21 != op2(e21,h2(e11))
| ~ spl12_18
| spl12_74
| ~ spl12_278 ),
inference(forward_demodulation,[],[f2935,f598]) ).
fof(f2971,plain,
( e12 != op1(e13,e10)
| ~ spl12_293 ),
inference(forward_demodulation,[],[f121,f1903]) ).
fof(f2978,plain,
( e10 != op1(e10,e10)
| ~ spl12_240 ),
inference(forward_demodulation,[],[f138,f1670]) ).
fof(f2984,plain,
( e13 != op1(e12,e11)
| ~ spl12_284 ),
inference(forward_demodulation,[],[f153,f1861]) ).
fof(f2987,plain,
( e10 != op1(e10,e10)
| ~ spl12_243 ),
inference(forward_demodulation,[],[f162,f1683]) ).
fof(f2988,plain,
( op1(e10,e10) != e11
| ~ spl12_249 ),
inference(forward_demodulation,[],[f163,f1709]) ).
fof(f2989,plain,
( e21 = op2(e22,e20)
| ~ spl12_221 ),
inference(forward_demodulation,[],[f293,f1562]) ).
fof(f2993,plain,
( ~ spl12_185
| ~ spl12_225 ),
inference(avatar_split_clause,[],[f2810,f1578,f1403]) ).
fof(f2995,plain,
( ~ spl12_185
| ~ spl12_186 ),
inference(avatar_split_clause,[],[f2853,f1407,f1403]) ).
fof(f2997,plain,
( spl12_185
| ~ spl12_221 ),
inference(avatar_split_clause,[],[f2989,f1560,f1403]) ).
fof(f3000,plain,
( e21 != op2(e20,e22)
| ~ spl12_181 ),
inference(forward_demodulation,[],[f185,f1388]) ).
fof(f3001,plain,
( ~ spl12_196
| ~ spl12_232 ),
inference(avatar_split_clause,[],[f2842,f1611,f1450]) ).
fof(f3002,plain,
( ~ spl12_175
| ~ spl12_221 ),
inference(avatar_split_clause,[],[f2844,f1560,f1360]) ).
fof(f3010,plain,
( e20 != op2(e22,e23)
| ~ spl12_221 ),
inference(forward_demodulation,[],[f171,f1562]) ).
fof(f3011,plain,
( e22 != op2(e22,e23)
| ~ spl12_214 ),
inference(forward_demodulation,[],[f172,f1531]) ).
fof(f3019,plain,
( e20 != op2(e23,e22)
| ~ spl12_221 ),
inference(forward_demodulation,[],[f195,f1562]) ).
fof(f3020,plain,
( ~ spl12_222
| ~ spl12_221 ),
inference(avatar_split_clause,[],[f3010,f1560,f1564]) ).
fof(f3025,plain,
( ~ spl12_202
| ~ spl12_221 ),
inference(avatar_split_clause,[],[f2841,f1560,f1476]) ).
fof(f3027,plain,
( ~ spl12_223
| ~ spl12_221 ),
inference(avatar_split_clause,[],[f3019,f1560,f1569]) ).
fof(f3062,plain,
( e20 = e22
| ~ spl12_221
| ~ spl12_227 ),
inference(superposition,[],[f1590,f1562]) ).
fof(f3067,plain,
( $false
| ~ spl12_221
| ~ spl12_227 ),
inference(forward_subsumption_resolution,[],[f3062,f223]) ).
fof(f3068,plain,
( ~ spl12_221
| ~ spl12_227 ),
inference(avatar_contradiction_clause,[],[f3067]) ).
fof(f3096,plain,
( e22 != op2(e23,e20)
| ~ spl12_229 ),
inference(forward_demodulation,[],[f169,f1599]) ).
fof(f3115,plain,
( op2(e20,e20) != e21
| ~ spl12_185 ),
inference(forward_demodulation,[],[f211,f1405]) ).
fof(f3117,plain,
( e23 = op2(e23,e22)
| ~ spl12_138
| ~ spl12_190 ),
inference(forward_demodulation,[],[f1166,f1426]) ).
fof(f3135,plain,
( e23 = op2(e23,e20)
| ~ spl12_143
| ~ spl12_203 ),
inference(forward_demodulation,[],[f1190,f1482]) ).
fof(f3151,plain,
( e22 = op2(e22,e20)
| ~ spl12_149
| ~ spl12_221 ),
inference(forward_demodulation,[],[f1219,f1562]) ).
fof(f3157,plain,
( $false
| ~ spl12_149
| spl12_192
| ~ spl12_221 ),
inference(forward_subsumption_resolution,[],[f3151,f1434]) ).
fof(f3158,plain,
( ~ spl12_149
| spl12_192
| ~ spl12_221 ),
inference(avatar_contradiction_clause,[],[f3157]) ).
fof(f3170,plain,
( ~ spl12_193
| ~ spl12_229 ),
inference(avatar_split_clause,[],[f3096,f1597,f1437]) ).
fof(f3172,plain,
( e20 != op2(e21,e20)
| ~ spl12_173 ),
inference(forward_demodulation,[],[f212,f1354]) ).
fof(f3173,plain,
( e21 != op2(e21,e20)
| ~ spl12_185 ),
inference(forward_demodulation,[],[f209,f1405]) ).
fof(f3174,plain,
( e23 != op2(e21,e20)
| ~ spl12_200 ),
inference(forward_demodulation,[],[f208,f1469]) ).
fof(f3178,plain,
( ~ spl12_177
| ~ spl12_173 ),
inference(avatar_split_clause,[],[f3172,f1352,f1369]) ).
fof(f3179,plain,
( ~ spl12_198
| ~ spl12_200 ),
inference(avatar_split_clause,[],[f3174,f1467,f1459]) ).
fof(f3190,plain,
( ~ spl12_184
| ~ spl12_185 ),
inference(avatar_split_clause,[],[f3173,f1403,f1399]) ).
fof(f3202,plain,
( e20 = e21
| ~ spl12_221
| ~ spl12_224 ),
inference(forward_demodulation,[],[f1576,f1562]) ).
fof(f3205,plain,
( ~ spl12_228
| ~ spl12_214 ),
inference(avatar_split_clause,[],[f3011,f1529,f1592]) ).
fof(f3207,plain,
( e20 != op2(e20,e23)
| ~ spl12_173 ),
inference(forward_demodulation,[],[f186,f1354]) ).
fof(f3211,plain,
( $false
| ~ spl12_3
| spl12_8
| ~ spl12_221
| ~ spl12_224 ),
inference(forward_subsumption_resolution,[],[f3202,f1959]) ).
fof(f3212,plain,
( ~ spl12_3
| spl12_8
| ~ spl12_221
| ~ spl12_224 ),
inference(avatar_contradiction_clause,[],[f3211]) ).
fof(f3281,plain,
( e21 != op2(e20,e21)
| ~ spl12_206 ),
inference(forward_demodulation,[],[f206,f1496]) ).
fof(f3282,plain,
( e23 = op2(e23,e21)
| ~ spl12_138
| ~ spl12_183 ),
inference(forward_demodulation,[],[f1166,f1396]) ).
fof(f3285,plain,
( spl12_220
| ~ spl12_138
| ~ spl12_183 ),
inference(avatar_split_clause,[],[f3282,f1394,f1164,f1555]) ).
fof(f3297,plain,
( ~ spl12_204
| ~ spl12_221 ),
inference(avatar_split_clause,[],[f2808,f1560,f1485]) ).
fof(f3298,plain,
( e21 != op2(e22,e21)
| ~ spl12_185 ),
inference(forward_demodulation,[],[f176,f1405]) ).
fof(f3304,plain,
( e23 != op2(e22,e21)
| ~ spl12_220 ),
inference(forward_demodulation,[],[f201,f1557]) ).
fof(f3307,plain,
( e21 != op2(e23,e21)
| ~ spl12_226 ),
inference(forward_demodulation,[],[f167,f1585]) ).
fof(f3311,plain,
( ~ spl12_209
| ~ spl12_185 ),
inference(avatar_split_clause,[],[f3298,f1403,f1507]) ).
fof(f3317,plain,
( ~ spl12_219
| ~ spl12_220 ),
inference(avatar_split_clause,[],[f3304,f1555,f1551]) ).
fof(f3348,plain,
( spl12_200
| ~ spl12_143
| ~ spl12_203 ),
inference(avatar_split_clause,[],[f3135,f1480,f1188,f1467]) ).
fof(f3352,plain,
( ~ spl12_180
| ~ spl12_185 ),
inference(avatar_split_clause,[],[f3115,f1403,f1382]) ).
fof(f3428,plain,
( e20 = h2(e10)
| ~ spl12_201 ),
inference(forward_demodulation,[],[f301,f1474]) ).
fof(f3429,plain,
( spl12_15
| ~ spl12_201 ),
inference(avatar_split_clause,[],[f3428,f1472,f583]) ).
fof(f3463,plain,
( e23 = op2(e23,e20)
| ~ spl12_138
| ~ spl12_176 ),
inference(forward_demodulation,[],[f1166,f1366]) ).
fof(f3484,plain,
( spl12_200
| ~ spl12_138
| ~ spl12_176 ),
inference(avatar_split_clause,[],[f3463,f1364,f1164,f1467]) ).
fof(f3492,plain,
( spl12_232
| ~ spl12_138
| ~ spl12_190 ),
inference(avatar_split_clause,[],[f3117,f1424,f1164,f1611]) ).
fof(f3494,plain,
( ~ spl12_181
| ~ spl12_206 ),
inference(avatar_split_clause,[],[f3281,f1494,f1386]) ).
fof(f3603,plain,
( e22 = op2(e22,e21)
| ~ spl12_139
| ~ spl12_182 ),
inference(forward_demodulation,[],[f1171,f1392]) ).
fof(f3604,plain,
( e21 = op2(e21,e20)
| ~ spl12_140
| ~ spl12_174 ),
inference(forward_demodulation,[],[f1176,f1358]) ).
fof(f3605,plain,
( $false
| ~ spl12_140
| ~ spl12_174
| spl12_184 ),
inference(forward_subsumption_resolution,[],[f3604,f1400]) ).
fof(f3606,plain,
( ~ spl12_140
| ~ spl12_174
| spl12_184 ),
inference(avatar_contradiction_clause,[],[f3605]) ).
fof(f3609,plain,
( e20 = op2(e20,e20)
| ~ spl12_146
| ~ spl12_177 ),
inference(forward_demodulation,[],[f1205,f1371]) ).
fof(f3612,plain,
( $false
| ~ spl12_146
| spl12_173
| ~ spl12_177 ),
inference(forward_subsumption_resolution,[],[f3609,f1353]) ).
fof(f3613,plain,
( ~ spl12_146
| spl12_173
| ~ spl12_177 ),
inference(avatar_contradiction_clause,[],[f3612]) ).
fof(f3616,plain,
( e20 = op2(e20,e22)
| ~ spl12_148
| ~ spl12_193 ),
inference(forward_demodulation,[],[f1214,f1439]) ).
fof(f3620,plain,
( $false
| ~ spl12_148
| spl12_175
| ~ spl12_193 ),
inference(forward_subsumption_resolution,[],[f3616,f1361]) ).
fof(f3621,plain,
( ~ spl12_148
| spl12_175
| ~ spl12_193 ),
inference(avatar_contradiction_clause,[],[f3620]) ).
fof(f3631,plain,
( ~ spl12_182
| ~ spl12_181 ),
inference(avatar_split_clause,[],[f3000,f1386,f1390]) ).
fof(f3639,plain,
( ~ spl12_210
| ~ spl12_226 ),
inference(avatar_split_clause,[],[f3307,f1583,f1511]) ).
fof(f3728,plain,
( e22 = op2(e22,e22)
| ~ spl12_139
| ~ spl12_189 ),
inference(forward_demodulation,[],[f1171,f1422]) ).
fof(f3729,plain,
( $false
| ~ spl12_139
| ~ spl12_189
| spl12_227 ),
inference(forward_subsumption_resolution,[],[f3728,f1589]) ).
fof(f3730,plain,
( ~ spl12_139
| ~ spl12_189
| spl12_227 ),
inference(avatar_contradiction_clause,[],[f3729]) ).
fof(f3741,plain,
( e21 = op2(e21,e20)
| ~ spl12_145
| ~ spl12_201 ),
inference(forward_demodulation,[],[f1200,f1474]) ).
fof(f3742,plain,
( $false
| ~ spl12_145
| spl12_184
| ~ spl12_201 ),
inference(forward_subsumption_resolution,[],[f3741,f1400]) ).
fof(f3743,plain,
( ~ spl12_145
| spl12_184
| ~ spl12_201 ),
inference(avatar_contradiction_clause,[],[f3742]) ).
fof(f3747,plain,
( e20 = op2(e20,e20)
| ~ spl12_148
| ~ spl12_179 ),
inference(forward_demodulation,[],[f1214,f1379]) ).
fof(f3748,plain,
( $false
| ~ spl12_148
| spl12_173
| ~ spl12_179 ),
inference(forward_subsumption_resolution,[],[f3747,f1353]) ).
fof(f3749,plain,
( ~ spl12_148
| spl12_173
| ~ spl12_179 ),
inference(avatar_contradiction_clause,[],[f3748]) ).
fof(f3758,plain,
( ~ spl12_176
| ~ spl12_173 ),
inference(avatar_split_clause,[],[f3207,f1352,f1364]) ).
fof(f3779,plain,
( ~ spl12_188
| ~ spl12_214 ),
inference(avatar_split_clause,[],[f2851,f1529,f1416]) ).
fof(f3780,plain,
( spl12_214
| ~ spl12_139
| ~ spl12_182 ),
inference(avatar_split_clause,[],[f3603,f1390,f1169,f1529]) ).
fof(f3880,plain,
( e21 = op2(e21,e23)
| ~ spl12_140
| ~ spl12_195 ),
inference(forward_demodulation,[],[f1176,f1448]) ).
fof(f3881,plain,
( e20 = e21
| ~ spl12_140
| ~ spl12_195
| ~ spl12_203 ),
inference(forward_demodulation,[],[f3880,f1482]) ).
fof(f3882,plain,
( $false
| ~ spl12_3
| spl12_8
| ~ spl12_140
| ~ spl12_195
| ~ spl12_203 ),
inference(forward_subsumption_resolution,[],[f3881,f1959]) ).
fof(f3883,plain,
( ~ spl12_3
| spl12_8
| ~ spl12_140
| ~ spl12_195
| ~ spl12_203 ),
inference(avatar_contradiction_clause,[],[f3882]) ).
fof(f3937,plain,
( e13 = op1(e13,e10)
| ~ spl12_156
| ~ spl12_240 ),
inference(forward_demodulation,[],[f1262,f1670]) ).
fof(f3943,plain,
( e11 = op1(e11,e10)
| ~ spl12_163
| ~ spl12_265 ),
inference(forward_demodulation,[],[f1296,f1778]) ).
fof(f3944,plain,
( e10 = op1(e10,e13)
| ~ spl12_164
| ~ spl12_262 ),
inference(forward_demodulation,[],[f1301,f1765]) ).
fof(f3946,plain,
( $false
| ~ spl12_163
| spl12_248
| ~ spl12_265 ),
inference(forward_subsumption_resolution,[],[f3943,f1704]) ).
fof(f3947,plain,
( ~ spl12_163
| spl12_248
| ~ spl12_265 ),
inference(avatar_contradiction_clause,[],[f3946]) ).
fof(f3953,plain,
( e12 = op1(e12,e10)
| ~ spl12_167
| ~ spl12_285 ),
inference(forward_demodulation,[],[f1315,f1866]) ).
fof(f3955,plain,
( e10 = op1(e10,e11)
| ~ spl12_169
| ~ spl12_249 ),
inference(forward_demodulation,[],[f1325,f1709]) ).
fof(f3959,plain,
( $false
| ~ spl12_167
| spl12_256
| ~ spl12_285 ),
inference(forward_subsumption_resolution,[],[f3953,f1738]) ).
fof(f3960,plain,
( ~ spl12_167
| spl12_256
| ~ spl12_285 ),
inference(avatar_contradiction_clause,[],[f3959]) ).
fof(f3964,plain,
( spl12_264
| ~ spl12_156
| ~ spl12_240 ),
inference(avatar_split_clause,[],[f3937,f1668,f1260,f1771]) ).
fof(f3968,plain,
( ~ spl12_264
| ~ spl12_262 ),
inference(avatar_split_clause,[],[f2895,f1763,f1771]) ).
fof(f3972,plain,
( e10 = op1(e10,e10)
| ~ spl12_166
| ~ spl12_243 ),
inference(forward_demodulation,[],[f1310,f1683]) ).
fof(f3976,plain,
( $false
| ~ spl12_166
| spl12_237
| ~ spl12_243 ),
inference(forward_subsumption_resolution,[],[f3972,f1657]) ).
fof(f3977,plain,
( ~ spl12_166
| spl12_237
| ~ spl12_243 ),
inference(avatar_contradiction_clause,[],[f3976]) ).
fof(f3992,plain,
( e10 != op1(e13,e13)
| ~ spl12_243 ),
inference(forward_demodulation,[],[f120,f1683]) ).
fof(f4000,plain,
( spl12_240
| ~ spl12_164
| ~ spl12_262 ),
inference(avatar_split_clause,[],[f3944,f1763,f1299,f1668]) ).
fof(f4001,plain,
( ~ spl12_238
| ~ spl12_265 ),
inference(avatar_split_clause,[],[f2786,f1776,f1660]) ).
fof(f4005,plain,
( ~ spl12_297
| ~ spl12_243 ),
inference(avatar_split_clause,[],[f3992,f1681,f1920]) ).
fof(f4012,plain,
( e11 != op1(e11,e10)
| ~ spl12_249 ),
inference(forward_demodulation,[],[f161,f1709]) ).
fof(f4017,plain,
( spl12_238
| ~ spl12_169
| ~ spl12_249 ),
inference(avatar_split_clause,[],[f3955,f1707,f1323,f1660]) ).
fof(f4020,plain,
( e12 != op1(e11,e11)
| ~ spl12_278 ),
inference(forward_demodulation,[],[f155,f1835]) ).
fof(f4071,plain,
( e13 = op1(e13,e11)
| ~ spl12_156
| ~ spl12_247 ),
inference(forward_demodulation,[],[f1262,f1700]) ).
fof(f4072,plain,
( $false
| ~ spl12_156
| ~ spl12_247
| spl12_284 ),
inference(forward_subsumption_resolution,[],[f4071,f1860]) ).
fof(f4073,plain,
( ~ spl12_156
| ~ spl12_247
| spl12_284 ),
inference(avatar_contradiction_clause,[],[f4072]) ).
fof(f4106,plain,
( e12 = op1(e12,e13)
| ~ spl12_157
| ~ spl12_260 ),
inference(forward_demodulation,[],[f1267,f1756]) ).
fof(f4109,plain,
( spl12_292
| ~ spl12_157
| ~ spl12_260 ),
inference(avatar_split_clause,[],[f4106,f1754,f1265,f1896]) ).
fof(f4113,plain,
( e10 != op1(e11,e13)
| ~ spl12_240 ),
inference(forward_demodulation,[],[f146,f1670]) ).
fof(f4118,plain,
( ~ spl12_267
| ~ spl12_240 ),
inference(avatar_split_clause,[],[f4113,f1668,f1784]) ).
fof(f4122,plain,
( ~ spl12_237
| ~ spl12_243 ),
inference(avatar_split_clause,[],[f2987,f1681,f1656]) ).
fof(f4127,plain,
( ~ spl12_275
| ~ spl12_278 ),
inference(avatar_split_clause,[],[f4020,f1833,f1820]) ).
fof(f4129,plain,
( e10 != op1(e13,e10)
| ~ spl12_269 ),
inference(forward_demodulation,[],[f122,f1795]) ).
fof(f4132,plain,
( ~ spl12_243
| ~ spl12_269 ),
inference(avatar_split_clause,[],[f4129,f1793,f1681]) ).
fof(f4136,plain,
( ~ spl12_257
| ~ spl12_293 ),
inference(avatar_split_clause,[],[f2971,f1901,f1741]) ).
fof(f4144,plain,
( e11 != op1(e12,e11)
| ~ spl12_249 ),
inference(forward_demodulation,[],[f128,f1709]) ).
fof(f4148,plain,
( ~ spl12_283
| ~ spl12_284 ),
inference(avatar_split_clause,[],[f2984,f1859,f1855]) ).
fof(f4170,plain,
( e12 = e13
| ~ spl12_255
| ~ spl12_262 ),
inference(forward_demodulation,[],[f1765,f1735]) ).
fof(f4171,plain,
( $false
| ~ spl12_255
| ~ spl12_262 ),
inference(forward_subsumption_resolution,[],[f4170,f213]) ).
fof(f4172,plain,
( ~ spl12_255
| ~ spl12_262 ),
inference(avatar_contradiction_clause,[],[f4171]) ).
fof(f4180,plain,
( e11 = e12
| ~ spl12_271
| ~ spl12_276 ),
inference(superposition,[],[f1826,f1804]) ).
fof(f4186,plain,
( $false
| ~ spl12_271
| ~ spl12_276 ),
inference(forward_subsumption_resolution,[],[f4180,f215]) ).
fof(f4187,plain,
( ~ spl12_271
| ~ spl12_276 ),
inference(avatar_contradiction_clause,[],[f4186]) ).
fof(f4206,plain,
( e10 != op1(e11,e11)
| ~ spl12_267 ),
inference(forward_demodulation,[],[f130,f1786]) ).
fof(f4223,plain,
( e13 = op1(e13,e13)
| ~ spl12_156
| ~ spl12_261 ),
inference(forward_demodulation,[],[f1262,f1760]) ).
fof(f4224,plain,
( $false
| ~ spl12_156
| ~ spl12_261
| spl12_300 ),
inference(forward_subsumption_resolution,[],[f4223,f1939]) ).
fof(f4225,plain,
( ~ spl12_156
| ~ spl12_261
| spl12_300 ),
inference(avatar_contradiction_clause,[],[f4224]) ).
fof(f4228,plain,
( ~ spl12_259
| ~ spl12_283 ),
inference(avatar_split_clause,[],[f2785,f1855,f1750]) ).
fof(f4231,plain,
( ~ spl12_237
| ~ spl12_240 ),
inference(avatar_split_clause,[],[f2978,f1668,f1656]) ).
fof(f4270,plain,
( e11 = op1(e11,e11)
| ~ spl12_158
| ~ spl12_245 ),
inference(forward_demodulation,[],[f1272,f1692]) ).
fof(f4271,plain,
( $false
| ~ spl12_158
| ~ spl12_245
| spl12_270 ),
inference(forward_subsumption_resolution,[],[f4270,f1799]) ).
fof(f4272,plain,
( ~ spl12_158
| ~ spl12_245
| spl12_270 ),
inference(avatar_contradiction_clause,[],[f4271]) ).
fof(f4297,plain,
( ~ spl12_244
| ~ spl12_249 ),
inference(avatar_split_clause,[],[f2988,f1707,f1686]) ).
fof(f4298,plain,
( e11 = e13
| ~ spl12_246
| ~ spl12_260 ),
inference(forward_demodulation,[],[f1696,f1756]) ).
fof(f4299,plain,
( ~ spl12_266
| ~ spl12_285 ),
inference(avatar_split_clause,[],[f2770,f1864,f1780]) ).
fof(f4303,plain,
( $false
| ~ spl12_246
| ~ spl12_260 ),
inference(forward_subsumption_resolution,[],[f4298,f214]) ).
fof(f4304,plain,
( ~ spl12_246
| ~ spl12_260 ),
inference(avatar_contradiction_clause,[],[f4303]) ).
fof(f4317,plain,
( e12 = e13
| ~ spl12_292
| ~ spl12_295 ),
inference(forward_demodulation,[],[f1912,f1898]) ).
fof(f4323,plain,
( ~ spl12_273
| ~ spl12_249 ),
inference(avatar_split_clause,[],[f4144,f1707,f1811]) ).
fof(f4326,plain,
( $false
| ~ spl12_292
| ~ spl12_295 ),
inference(forward_subsumption_resolution,[],[f4317,f213]) ).
fof(f4327,plain,
( ~ spl12_292
| ~ spl12_295 ),
inference(avatar_contradiction_clause,[],[f4326]) ).
fof(f4382,plain,
( ~ spl12_258
| ~ spl12_262 ),
inference(avatar_split_clause,[],[f2793,f1763,f1746]) ).
fof(f4388,plain,
( ~ spl12_248
| ~ spl12_249 ),
inference(avatar_split_clause,[],[f4012,f1707,f1703]) ).
fof(f4421,plain,
( e10 = e12
| ~ spl12_297
| ~ spl12_299 ),
inference(superposition,[],[f1934,f1922]) ).
fof(f4426,plain,
( $false
| ~ spl12_297
| ~ spl12_299 ),
inference(forward_subsumption_resolution,[],[f4421,f217]) ).
fof(f4427,plain,
( ~ spl12_297
| ~ spl12_299 ),
inference(avatar_contradiction_clause,[],[f4426]) ).
fof(f4431,plain,
( e11 != op1(e13,e11)
| ~ spl12_290 ),
inference(forward_demodulation,[],[f119,f1889]) ).
fof(f4439,plain,
( e11 != op1(e11,e11)
| ~ spl12_272 ),
inference(forward_demodulation,[],[f130,f1808]) ).
fof(f4480,plain,
( e10 = op1(e10,e12)
| ~ spl12_166
| ~ spl12_257 ),
inference(forward_demodulation,[],[f1310,f1743]) ).
fof(f4481,plain,
( $false
| ~ spl12_166
| spl12_239
| ~ spl12_257 ),
inference(forward_subsumption_resolution,[],[f4480,f1665]) ).
fof(f4482,plain,
( ~ spl12_166
| spl12_239
| ~ spl12_257 ),
inference(avatar_contradiction_clause,[],[f4481]) ).
fof(f4483,plain,
( e13 = op1(e13,e12)
| ~ spl12_156
| ~ spl12_254 ),
inference(forward_demodulation,[],[f1262,f1730]) ).
fof(f4493,plain,
( ~ spl12_274
| ~ spl12_290 ),
inference(avatar_split_clause,[],[f4431,f1887,f1815]) ).
fof(f4497,plain,
( spl12_296
| ~ spl12_156
| ~ spl12_254 ),
inference(avatar_split_clause,[],[f4483,f1728,f1260,f1915]) ).
fof(f4522,plain,
( e11 = op1(e11,e13)
| ~ spl12_158
| ~ spl12_259 ),
inference(forward_demodulation,[],[f1272,f1752]) ).
fof(f4551,plain,
( op2(e21,e20) = h2(e11)
| ~ spl12_201 ),
inference(forward_demodulation,[],[f300,f1474]) ).
fof(f4552,plain,
( e23 = h2(e11)
| ~ spl12_198
| ~ spl12_201 ),
inference(forward_demodulation,[],[f4551,f1461]) ).
fof(f4553,plain,
( spl12_86
| ~ spl12_198
| ~ spl12_201 ),
inference(avatar_split_clause,[],[f4552,f1472,f1459,f908]) ).
fof(f4554,plain,
( e21 != op2(e21,e23)
| ~ spl12_18
| spl12_74
| ~ spl12_86
| ~ spl12_278 ),
inference(superposition,[],[f2936,f909]) ).
fof(f4555,plain,
( $false
| ~ spl12_18
| spl12_74
| ~ spl12_86
| ~ spl12_208
| ~ spl12_278 ),
inference(forward_subsumption_resolution,[],[f4554,f1504]) ).
fof(f4556,plain,
( ~ spl12_18
| spl12_74
| ~ spl12_86
| ~ spl12_208
| ~ spl12_278 ),
inference(avatar_contradiction_clause,[],[f4555]) ).
fof(f4557,plain,
( op2(e20,e20) != h2(op1(e10,e10))
| ~ spl12_15
| spl12_65 ),
inference(forward_demodulation,[],[f822,f584]) ).
fof(f4559,plain,
( op2(e20,e20) != h2(e10)
| ~ spl12_15
| spl12_65
| ~ spl12_237 ),
inference(forward_demodulation,[],[f4557,f1658]) ).
fof(f4561,plain,
( e20 != op2(e20,e20)
| ~ spl12_15
| spl12_65
| ~ spl12_237 ),
inference(forward_demodulation,[],[f4559,f584]) ).
fof(f4563,plain,
( $false
| ~ spl12_15
| spl12_65
| ~ spl12_173
| ~ spl12_237 ),
inference(forward_subsumption_resolution,[],[f4561,f1354]) ).
fof(f4564,plain,
( ~ spl12_15
| spl12_65
| ~ spl12_173
| ~ spl12_237 ),
inference(avatar_contradiction_clause,[],[f4563]) ).
fof(f4567,plain,
( h2(op1(e10,e11)) != op2(h2(e10),e23)
| spl12_66
| ~ spl12_86 ),
inference(forward_demodulation,[],[f826,f909]) ).
fof(f4569,plain,
( op2(e20,e23) != h2(op1(e10,e11))
| ~ spl12_15
| spl12_66
| ~ spl12_86 ),
inference(forward_demodulation,[],[f4567,f584]) ).
fof(f4571,plain,
( op2(e20,e23) != h2(e13)
| ~ spl12_15
| spl12_66
| ~ spl12_86
| ~ spl12_259 ),
inference(forward_demodulation,[],[f4569,f1752]) ).
fof(f4572,plain,
( e22 != h2(e13)
| ~ spl12_15
| spl12_66
| ~ spl12_86
| ~ spl12_190
| ~ spl12_259 ),
inference(forward_demodulation,[],[f4571,f1426]) ).
fof(f4573,plain,
( ~ spl12_81
| ~ spl12_15
| spl12_66
| ~ spl12_86
| ~ spl12_190
| ~ spl12_259 ),
inference(avatar_split_clause,[],[f4572,f1750,f1424,f908,f824,f583,f884]) ).
fof(f4597,plain,
( e13 = op1(op1(e12,e10),e10)
| ~ spl12_285 ),
inference(forward_demodulation,[],[f289,f1866]) ).
fof(f4598,plain,
( e13 = op1(e11,e10)
| ~ spl12_249
| ~ spl12_285 ),
inference(forward_demodulation,[],[f4597,f1709]) ).
fof(f4599,plain,
( e23 = op2(op2(e22,e20),e20)
| ~ spl12_221 ),
inference(forward_demodulation,[],[f292,f1562]) ).
fof(f4600,plain,
( e23 = op2(e21,e20)
| ~ spl12_185
| ~ spl12_221 ),
inference(forward_demodulation,[],[f4599,f1405]) ).
fof(f4758,plain,
( h2(e13) = op2(op2(e21,e20),e20)
| ~ spl12_201 ),
inference(forward_demodulation,[],[f299,f1474]) ).
fof(f4759,plain,
( op2(e23,e20) = h2(e13)
| ~ spl12_198
| ~ spl12_201 ),
inference(forward_demodulation,[],[f4758,f1461]) ).
fof(f4760,plain,
( e22 = h2(e13)
| ~ spl12_193
| ~ spl12_198
| ~ spl12_201 ),
inference(forward_demodulation,[],[f4759,f1439]) ).
fof(f4764,plain,
( h2(op1(e10,e12)) != op2(h2(e10),e21)
| ~ spl12_18
| spl12_67 ),
inference(forward_demodulation,[],[f830,f598]) ).
fof(f4765,plain,
( spl12_81
| ~ spl12_193
| ~ spl12_198
| ~ spl12_201 ),
inference(avatar_split_clause,[],[f4760,f1472,f1459,f1437,f884]) ).
fof(f4767,plain,
( op2(e20,e21) != h2(op1(e10,e12))
| ~ spl12_15
| ~ spl12_18
| spl12_67 ),
inference(forward_demodulation,[],[f4764,f584]) ).
fof(f4769,plain,
( op2(e20,e21) != h2(e11)
| ~ spl12_15
| ~ spl12_18
| spl12_67
| ~ spl12_246 ),
inference(forward_demodulation,[],[f4767,f1696]) ).
fof(f4771,plain,
( e23 != op2(e20,e21)
| ~ spl12_15
| ~ spl12_18
| spl12_67
| ~ spl12_86
| ~ spl12_246 ),
inference(forward_demodulation,[],[f4769,f909]) ).
fof(f4773,plain,
( $false
| ~ spl12_15
| ~ spl12_18
| spl12_67
| ~ spl12_86
| ~ spl12_195
| ~ spl12_246 ),
inference(forward_subsumption_resolution,[],[f4771,f1448]) ).
fof(f4774,plain,
( ~ spl12_15
| ~ spl12_18
| spl12_67
| ~ spl12_86
| ~ spl12_195
| ~ spl12_246 ),
inference(avatar_contradiction_clause,[],[f4773]) ).
fof(f4776,plain,
( h2(op1(e10,e13)) != op2(e20,h2(e13))
| ~ spl12_15
| spl12_68 ),
inference(forward_demodulation,[],[f834,f584]) ).
fof(f4778,plain,
( h2(e12) != op2(e20,h2(e13))
| ~ spl12_15
| spl12_68
| ~ spl12_254 ),
inference(forward_demodulation,[],[f4776,f1730]) ).
fof(f4780,plain,
( e21 != op2(e20,h2(e13))
| ~ spl12_15
| ~ spl12_18
| spl12_68
| ~ spl12_254 ),
inference(forward_demodulation,[],[f4778,f598]) ).
fof(f4782,plain,
( e21 != op2(e20,e22)
| ~ spl12_15
| ~ spl12_18
| spl12_68
| ~ spl12_81
| ~ spl12_254 ),
inference(forward_demodulation,[],[f4780,f885]) ).
fof(f4783,plain,
( $false
| ~ spl12_15
| ~ spl12_18
| spl12_68
| ~ spl12_81
| ~ spl12_182
| ~ spl12_254 ),
inference(forward_subsumption_resolution,[],[f4782,f1392]) ).
fof(f4784,plain,
( ~ spl12_15
| ~ spl12_18
| spl12_68
| ~ spl12_81
| ~ spl12_182
| ~ spl12_254 ),
inference(avatar_contradiction_clause,[],[f4783]) ).
fof(f4786,plain,
( h2(op1(e11,e10)) != op2(h2(e11),e20)
| ~ spl12_15
| spl12_69 ),
inference(forward_demodulation,[],[f838,f584]) ).
fof(f4788,plain,
( op2(e23,e20) != h2(op1(e11,e10))
| ~ spl12_15
| spl12_69
| ~ spl12_86 ),
inference(forward_demodulation,[],[f4786,f909]) ).
fof(f4790,plain,
( op2(e23,e20) != h2(e13)
| ~ spl12_15
| spl12_69
| ~ spl12_86
| ~ spl12_262 ),
inference(forward_demodulation,[],[f4788,f1765]) ).
fof(f4792,plain,
( e22 != op2(e23,e20)
| ~ spl12_15
| spl12_69
| ~ spl12_81
| ~ spl12_86
| ~ spl12_262 ),
inference(forward_demodulation,[],[f4790,f885]) ).
fof(f4793,plain,
( $false
| ~ spl12_15
| spl12_69
| ~ spl12_81
| ~ spl12_86
| ~ spl12_193
| ~ spl12_262 ),
inference(forward_subsumption_resolution,[],[f4792,f1439]) ).
fof(f4794,plain,
( ~ spl12_15
| spl12_69
| ~ spl12_81
| ~ spl12_86
| ~ spl12_193
| ~ spl12_262 ),
inference(avatar_contradiction_clause,[],[f4793]) ).
fof(f4796,plain,
( op2(e23,e23) != h2(op1(e11,e11))
| spl12_70
| ~ spl12_86 ),
inference(forward_demodulation,[],[f842,f909]) ).
fof(f4798,plain,
( op2(e23,e23) != h2(e10)
| spl12_70
| ~ spl12_86
| ~ spl12_265 ),
inference(forward_demodulation,[],[f4796,f1778]) ).
fof(f4800,plain,
( e20 != op2(e23,e23)
| ~ spl12_15
| spl12_70
| ~ spl12_86
| ~ spl12_265 ),
inference(forward_demodulation,[],[f4798,f584]) ).
fof(f4802,plain,
( $false
| ~ spl12_15
| spl12_70
| ~ spl12_86
| ~ spl12_233
| ~ spl12_265 ),
inference(forward_subsumption_resolution,[],[f4800,f1618]) ).
fof(f4803,plain,
( ~ spl12_15
| spl12_70
| ~ spl12_86
| ~ spl12_233
| ~ spl12_265 ),
inference(avatar_contradiction_clause,[],[f4802]) ).
fof(f4805,plain,
( h2(op1(e11,e12)) != op2(h2(e11),e21)
| ~ spl12_18
| spl12_71 ),
inference(forward_demodulation,[],[f846,f598]) ).
fof(f4807,plain,
( op2(e23,e21) != h2(op1(e11,e12))
| ~ spl12_18
| spl12_71
| ~ spl12_86 ),
inference(forward_demodulation,[],[f4805,f909]) ).
fof(f4809,plain,
( op2(e23,e21) != h2(e12)
| ~ spl12_18
| spl12_71
| ~ spl12_86
| ~ spl12_276 ),
inference(forward_demodulation,[],[f4807,f1826]) ).
fof(f4810,plain,
( e21 != op2(e23,e21)
| ~ spl12_18
| spl12_71
| ~ spl12_86
| ~ spl12_276 ),
inference(forward_demodulation,[],[f4809,f598]) ).
fof(f4811,plain,
( $false
| ~ spl12_18
| spl12_71
| ~ spl12_86
| ~ spl12_210
| ~ spl12_276 ),
inference(forward_subsumption_resolution,[],[f4810,f1513]) ).
fof(f4812,plain,
( ~ spl12_18
| spl12_71
| ~ spl12_86
| ~ spl12_210
| ~ spl12_276 ),
inference(avatar_contradiction_clause,[],[f4811]) ).
fof(f4814,plain,
( h2(op1(e11,e13)) != op2(h2(e11),e22)
| spl12_72
| ~ spl12_81 ),
inference(forward_demodulation,[],[f850,f885]) ).
fof(f4816,plain,
( op2(e23,e22) != h2(op1(e11,e13))
| spl12_72
| ~ spl12_81
| ~ spl12_86 ),
inference(forward_demodulation,[],[f4814,f909]) ).
fof(f4818,plain,
( op2(e23,e22) != h2(e11)
| spl12_72
| ~ spl12_81
| ~ spl12_86
| ~ spl12_272 ),
inference(forward_demodulation,[],[f4816,f1808]) ).
fof(f4820,plain,
( e23 != op2(e23,e22)
| spl12_72
| ~ spl12_81
| ~ spl12_86
| ~ spl12_272 ),
inference(forward_demodulation,[],[f4818,f909]) ).
fof(f4821,plain,
( $false
| spl12_72
| ~ spl12_81
| ~ spl12_86
| ~ spl12_232
| ~ spl12_272 ),
inference(forward_subsumption_resolution,[],[f4820,f1613]) ).
fof(f4822,plain,
( spl12_72
| ~ spl12_81
| ~ spl12_86
| ~ spl12_232
| ~ spl12_272 ),
inference(avatar_contradiction_clause,[],[f4821]) ).
fof(f4824,plain,
( h2(op1(e12,e10)) != op2(h2(e12),e20)
| ~ spl12_15
| spl12_73 ),
inference(forward_demodulation,[],[f854,f584]) ).
fof(f4826,plain,
( op2(e21,e20) != h2(op1(e12,e10))
| ~ spl12_15
| ~ spl12_18
| spl12_73 ),
inference(forward_demodulation,[],[f4824,f598]) ).
fof(f4828,plain,
( op2(e21,e20) != h2(e11)
| ~ spl12_15
| ~ spl12_18
| spl12_73
| ~ spl12_249 ),
inference(forward_demodulation,[],[f4826,f1709]) ).
fof(f4830,plain,
( e23 != op2(e21,e20)
| ~ spl12_15
| ~ spl12_18
| spl12_73
| ~ spl12_86
| ~ spl12_249 ),
inference(forward_demodulation,[],[f4828,f909]) ).
fof(f4831,plain,
( $false
| ~ spl12_15
| ~ spl12_18
| spl12_73
| ~ spl12_86
| ~ spl12_198
| ~ spl12_249 ),
inference(forward_subsumption_resolution,[],[f4830,f1461]) ).
fof(f4832,plain,
( ~ spl12_15
| ~ spl12_18
| spl12_73
| ~ spl12_86
| ~ spl12_198
| ~ spl12_249 ),
inference(avatar_contradiction_clause,[],[f4831]) ).
fof(f4834,plain,
( op2(e21,e21) != h2(op1(e12,e12))
| ~ spl12_18
| spl12_75 ),
inference(forward_demodulation,[],[f862,f598]) ).
fof(f4836,plain,
( op2(e21,e21) != h2(e10)
| ~ spl12_18
| spl12_75
| ~ spl12_285 ),
inference(forward_demodulation,[],[f4834,f1866]) ).
fof(f4838,plain,
( e20 != op2(e21,e21)
| ~ spl12_15
| ~ spl12_18
| spl12_75
| ~ spl12_285 ),
inference(forward_demodulation,[],[f4836,f584]) ).
fof(f4840,plain,
( $false
| ~ spl12_15
| ~ spl12_18
| spl12_75
| ~ spl12_201
| ~ spl12_285 ),
inference(forward_subsumption_resolution,[],[f4838,f1474]) ).
fof(f4841,plain,
( ~ spl12_15
| ~ spl12_18
| spl12_75
| ~ spl12_201
| ~ spl12_285 ),
inference(avatar_contradiction_clause,[],[f4840]) ).
fof(f4843,plain,
( h2(op1(e12,e13)) != op2(h2(e12),e22)
| spl12_76
| ~ spl12_81 ),
inference(forward_demodulation,[],[f866,f885]) ).
fof(f4845,plain,
( op2(e21,e22) != h2(op1(e12,e13))
| ~ spl12_18
| spl12_76
| ~ spl12_81 ),
inference(forward_demodulation,[],[f4843,f598]) ).
fof(f4847,plain,
( op2(e21,e22) != h2(e13)
| ~ spl12_18
| spl12_76
| ~ spl12_81
| ~ spl12_295 ),
inference(forward_demodulation,[],[f4845,f1912]) ).
fof(f4848,plain,
( e22 != op2(e21,e22)
| ~ spl12_18
| spl12_76
| ~ spl12_81
| ~ spl12_295 ),
inference(forward_demodulation,[],[f4847,f885]) ).
fof(f4849,plain,
( $false
| ~ spl12_18
| spl12_76
| ~ spl12_81
| ~ spl12_212
| ~ spl12_295 ),
inference(forward_subsumption_resolution,[],[f4848,f1522]) ).
fof(f4850,plain,
( ~ spl12_18
| spl12_76
| ~ spl12_81
| ~ spl12_212
| ~ spl12_295 ),
inference(avatar_contradiction_clause,[],[f4849]) ).
fof(f4852,plain,
( h2(op1(e13,e10)) != op2(h2(e13),e20)
| ~ spl12_15
| spl12_77 ),
inference(forward_demodulation,[],[f870,f584]) ).
fof(f4854,plain,
( op2(e22,e20) != h2(op1(e13,e10))
| ~ spl12_15
| spl12_77
| ~ spl12_81 ),
inference(forward_demodulation,[],[f4852,f885]) ).
fof(f4856,plain,
( op2(e22,e20) != h2(e12)
| ~ spl12_15
| spl12_77
| ~ spl12_81
| ~ spl12_257 ),
inference(forward_demodulation,[],[f4854,f1743]) ).
fof(f4858,plain,
( e21 != op2(e22,e20)
| ~ spl12_15
| ~ spl12_18
| spl12_77
| ~ spl12_81
| ~ spl12_257 ),
inference(forward_demodulation,[],[f4856,f598]) ).
fof(f4859,plain,
( $false
| ~ spl12_15
| ~ spl12_18
| spl12_77
| ~ spl12_81
| ~ spl12_185
| ~ spl12_257 ),
inference(forward_subsumption_resolution,[],[f4858,f1405]) ).
fof(f4860,plain,
( ~ spl12_15
| ~ spl12_18
| spl12_77
| ~ spl12_81
| ~ spl12_185
| ~ spl12_257 ),
inference(avatar_contradiction_clause,[],[f4859]) ).
fof(f4862,plain,
( h2(op1(e13,e11)) != op2(h2(e13),e23)
| spl12_78
| ~ spl12_86 ),
inference(forward_demodulation,[],[f874,f909]) ).
fof(f4864,plain,
( op2(e22,e23) != h2(op1(e13,e11))
| spl12_78
| ~ spl12_81
| ~ spl12_86 ),
inference(forward_demodulation,[],[f4862,f885]) ).
fof(f4866,plain,
( op2(e22,e23) != h2(e11)
| spl12_78
| ~ spl12_81
| ~ spl12_86
| ~ spl12_274 ),
inference(forward_demodulation,[],[f4864,f1817]) ).
fof(f4868,plain,
( e23 != op2(e22,e23)
| spl12_78
| ~ spl12_81
| ~ spl12_86
| ~ spl12_274 ),
inference(forward_demodulation,[],[f4866,f909]) ).
fof(f4869,plain,
( $false
| spl12_78
| ~ spl12_81
| ~ spl12_86
| ~ spl12_231
| ~ spl12_274 ),
inference(forward_subsumption_resolution,[],[f4868,f1608]) ).
fof(f4870,plain,
( spl12_78
| ~ spl12_81
| ~ spl12_86
| ~ spl12_231
| ~ spl12_274 ),
inference(avatar_contradiction_clause,[],[f4869]) ).
fof(f4872,plain,
( h2(op1(e13,e12)) != op2(h2(e13),e21)
| ~ spl12_18
| spl12_79 ),
inference(forward_demodulation,[],[f878,f598]) ).
fof(f4874,plain,
( op2(e22,e21) != h2(op1(e13,e12))
| ~ spl12_18
| spl12_79
| ~ spl12_81 ),
inference(forward_demodulation,[],[f4872,f885]) ).
fof(f4876,plain,
( op2(e22,e21) != h2(e13)
| ~ spl12_18
| spl12_79
| ~ spl12_81
| ~ spl12_296 ),
inference(forward_demodulation,[],[f4874,f1917]) ).
fof(f4878,plain,
( e22 != op2(e22,e21)
| ~ spl12_18
| spl12_79
| ~ spl12_81
| ~ spl12_296 ),
inference(forward_demodulation,[],[f4876,f885]) ).
fof(f4879,plain,
( $false
| ~ spl12_18
| spl12_79
| ~ spl12_81
| ~ spl12_214
| ~ spl12_296 ),
inference(forward_subsumption_resolution,[],[f4878,f1531]) ).
fof(f4880,plain,
( ~ spl12_18
| spl12_79
| ~ spl12_81
| ~ spl12_214
| ~ spl12_296 ),
inference(avatar_contradiction_clause,[],[f4879]) ).
fof(f4882,plain,
( op2(e22,e22) != h2(op1(e13,e13))
| spl12_80
| ~ spl12_81 ),
inference(forward_demodulation,[],[f882,f885]) ).
fof(f4884,plain,
( op2(e22,e22) != h2(e10)
| spl12_80
| ~ spl12_81
| ~ spl12_297 ),
inference(forward_demodulation,[],[f4882,f1922]) ).
fof(f4886,plain,
( e20 != op2(e22,e22)
| ~ spl12_15
| spl12_80
| ~ spl12_81
| ~ spl12_297 ),
inference(forward_demodulation,[],[f4884,f584]) ).
fof(f4888,plain,
( $false
| ~ spl12_15
| spl12_80
| ~ spl12_81
| ~ spl12_221
| ~ spl12_297 ),
inference(forward_subsumption_resolution,[],[f4886,f1562]) ).
fof(f4889,plain,
( ~ spl12_15
| spl12_80
| ~ spl12_81
| ~ spl12_221
| ~ spl12_297 ),
inference(avatar_contradiction_clause,[],[f4888]) ).
fof(f4898,plain,
( e10 = e13
| ~ spl12_238
| ~ spl12_259 ),
inference(forward_demodulation,[],[f1662,f1752]) ).
fof(f4906,plain,
( ~ spl12_270
| ~ spl12_272 ),
inference(avatar_split_clause,[],[f4439,f1806,f1798]) ).
fof(f4913,plain,
( spl12_262
| ~ spl12_249
| ~ spl12_285 ),
inference(avatar_split_clause,[],[f4598,f1864,f1707,f1763]) ).
fof(f4929,plain,
( $false
| ~ spl12_238
| ~ spl12_259 ),
inference(forward_subsumption_resolution,[],[f4898,f216]) ).
fof(f4930,plain,
( ~ spl12_238
| ~ spl12_259 ),
inference(avatar_contradiction_clause,[],[f4929]) ).
fof(f4952,plain,
( ~ spl12_265
| ~ spl12_267 ),
inference(avatar_split_clause,[],[f4206,f1784,f1776]) ).
fof(f4966,plain,
( spl12_272
| ~ spl12_158
| ~ spl12_259 ),
inference(avatar_split_clause,[],[f4522,f1750,f1270,f1806]) ).
fof(f4999,plain,
( spl12_198
| ~ spl12_185
| ~ spl12_221 ),
inference(avatar_split_clause,[],[f4600,f1560,f1403,f1459]) ).
cnf(s12,plain,
( ~ spl12_11
| ~ spl12_15 ),
inference(sat_conversion,[],[f586]) ).
cnf(s14,plain,
( ~ spl12_16
| ~ spl12_18 ),
inference(sat_conversion,[],[f600]) ).
cnf(s53,plain,
( spl12_11
| spl12_16
| ~ spl12_65
| ~ spl12_66
| ~ spl12_67
| ~ spl12_68
| ~ spl12_69
| ~ spl12_70
| ~ spl12_71
| ~ spl12_72
| ~ spl12_73
| ~ spl12_74
| ~ spl12_75
| ~ spl12_76
| ~ spl12_77
| ~ spl12_78
| ~ spl12_79
| ~ spl12_80
| ~ spl12_81
| ~ spl12_86 ),
inference(sat_conversion,[],[f911]) ).
cnf(s98,plain,
spl12_107,
inference(sat_conversion,[],[f1156]) ).
cnf(s99,plain,
spl12_18,
inference(sat_conversion,[],[f1157]) ).
cnf(s100,plain,
spl12_3,
inference(sat_conversion,[],[f1158]) ).
cnf(s101,plain,
( spl12_137
| spl12_138 ),
inference(sat_conversion,[],[f1167]) ).
cnf(s102,plain,
( spl12_137
| spl12_139 ),
inference(sat_conversion,[],[f1172]) ).
cnf(s103,plain,
( spl12_137
| spl12_140 ),
inference(sat_conversion,[],[f1177]) ).
cnf(s105,plain,
( ~ spl12_142
| spl12_143 ),
inference(sat_conversion,[],[f1191]) ).
cnf(s107,plain,
( ~ spl12_142
| spl12_145 ),
inference(sat_conversion,[],[f1201]) ).
cnf(s108,plain,
( ~ spl12_142
| spl12_146 ),
inference(sat_conversion,[],[f1206]) ).
cnf(s110,plain,
( ~ spl12_137
| spl12_142
| spl12_148
| spl12_149 ),
inference(sat_conversion,[],[f1220]) ).
cnf(s125,plain,
( ~ spl12_155
| spl12_156 ),
inference(sat_conversion,[],[f1263]) ).
cnf(s126,plain,
( ~ spl12_155
| spl12_157 ),
inference(sat_conversion,[],[f1268]) ).
cnf(s127,plain,
( ~ spl12_155
| spl12_158 ),
inference(sat_conversion,[],[f1273]) ).
cnf(s131,plain,
( spl12_160
| spl12_163 ),
inference(sat_conversion,[],[f1297]) ).
cnf(s132,plain,
( spl12_160
| spl12_164 ),
inference(sat_conversion,[],[f1302]) ).
cnf(s134,plain,
( spl12_155
| ~ spl12_160
| spl12_166
| spl12_167 ),
inference(sat_conversion,[],[f1316]) ).
cnf(s136,plain,
( spl12_155
| ~ spl12_160
| spl12_166
| spl12_169 ),
inference(sat_conversion,[],[f1326]) ).
cnf(s149,plain,
( spl12_173
| spl12_174
| spl12_175
| spl12_176 ),
inference(sat_conversion,[],[f1367]) ).
cnf(s151,plain,
( spl12_180
| spl12_181
| spl12_182
| spl12_183 ),
inference(sat_conversion,[],[f1397]) ).
cnf(s153,plain,
( spl12_187
| spl12_188
| spl12_189
| spl12_190 ),
inference(sat_conversion,[],[f1427]) ).
cnf(s154,plain,
( spl12_187
| spl12_191
| spl12_192
| spl12_193 ),
inference(sat_conversion,[],[f1440]) ).
cnf(s157,plain,
( spl12_177
| spl12_201
| spl12_202
| spl12_203 ),
inference(sat_conversion,[],[f1483]) ).
cnf(s159,plain,
( spl12_184
| spl12_206
| spl12_207
| spl12_208 ),
inference(sat_conversion,[],[f1505]) ).
cnf(s160,plain,
( spl12_181
| spl12_206
| spl12_209
| spl12_210 ),
inference(sat_conversion,[],[f1514]) ).
cnf(s168,plain,
( spl12_182
| spl12_207
| spl12_224
| spl12_226 ),
inference(sat_conversion,[],[f1586]) ).
cnf(s170,plain,
( spl12_189
| spl12_212
| spl12_227
| spl12_229 ),
inference(sat_conversion,[],[f1600]) ).
cnf(s174,plain,
( spl12_176
| spl12_203
| spl12_222
| spl12_233 ),
inference(sat_conversion,[],[f1620]) ).
cnf(s182,plain,
( spl12_174
| spl12_181
| spl12_188
| spl12_195 ),
inference(sat_conversion,[],[f1640]) ).
cnf(s183,plain,
( spl12_175
| spl12_182
| spl12_189
| spl12_196 ),
inference(sat_conversion,[],[f1641]) ).
cnf(s190,plain,
( spl12_204
| spl12_209
| spl12_214
| spl12_219 ),
inference(sat_conversion,[],[f1648]) ).
cnf(s192,plain,
( spl12_222
| spl12_225
| spl12_228
| spl12_231 ),
inference(sat_conversion,[],[f1650]) ).
cnf(s193,plain,
( spl12_179
| spl12_186
| spl12_193
| spl12_200 ),
inference(sat_conversion,[],[f1651]) ).
cnf(s195,plain,
( spl12_223
| spl12_226
| spl12_229
| spl12_232 ),
inference(sat_conversion,[],[f1653]) ).
cnf(s198,plain,
( spl12_237
| spl12_241
| spl12_242
| spl12_243 ),
inference(sat_conversion,[],[f1684]) ).
cnf(s199,plain,
( spl12_244
| spl12_245
| spl12_246
| spl12_247 ),
inference(sat_conversion,[],[f1701]) ).
cnf(s203,plain,
( spl12_258
| spl12_259
| spl12_260
| spl12_261 ),
inference(sat_conversion,[],[f1761]) ).
cnf(s205,plain,
( spl12_241
| spl12_265
| spl12_266
| spl12_267 ),
inference(sat_conversion,[],[f1787]) ).
cnf(s206,plain,
( spl12_238
| spl12_265
| spl12_268
| spl12_269 ),
inference(sat_conversion,[],[f1796]) ).
cnf(s208,plain,
( spl12_245
| spl12_270
| spl12_273
| spl12_274 ),
inference(sat_conversion,[],[f1818]) ).
cnf(s209,plain,
( spl12_255
| spl12_275
| spl12_276
| spl12_277 ),
inference(sat_conversion,[],[f1831]) ).
cnf(s216,plain,
( spl12_246
| spl12_271
| spl12_288
| spl12_290 ),
inference(sat_conversion,[],[f1890]) ).
cnf(s219,plain,
( spl12_263
| spl12_283
| spl12_294
| spl12_295 ),
inference(sat_conversion,[],[f1913]) ).
cnf(s222,plain,
( spl12_240
| spl12_267
| spl12_286
| spl12_297 ),
inference(sat_conversion,[],[f1924]) ).
cnf(s226,plain,
( spl12_254
| spl12_277
| spl12_292
| spl12_299 ),
inference(sat_conversion,[],[f1936]) ).
cnf(s229,plain,
( spl12_237
| spl12_244
| spl12_251
| spl12_258 ),
inference(sat_conversion,[],[f1943]) ).
cnf(s231,plain,
( spl12_239
| spl12_246
| spl12_253
| spl12_260 ),
inference(sat_conversion,[],[f1945]) ).
cnf(s232,plain,
( spl12_240
| spl12_247
| spl12_254
| spl12_261 ),
inference(sat_conversion,[],[f1946]) ).
cnf(s238,plain,
( spl12_268
| spl12_273
| spl12_278
| spl12_283 ),
inference(sat_conversion,[],[f1952]) ).
cnf(s241,plain,
( spl12_243
| spl12_250
| spl12_257
| spl12_264 ),
inference(sat_conversion,[],[f1955]) ).
cnf(s243,plain,
( spl12_287
| spl12_290
| spl12_293
| spl12_296 ),
inference(sat_conversion,[],[f1957]) ).
cnf(s245,plain,
spl12_285,
inference(sat_conversion,[],[f1964]) ).
cnf(s246,plain,
spl12_221,
inference(sat_conversion,[],[f1965]) ).
cnf(s248,plain,
( spl12_28
| ~ spl12_107
| ~ spl12_181
| ~ spl12_188 ),
inference(sat_conversion,[],[f1971]) ).
cnf(s252,plain,
( ~ spl12_28
| ~ spl12_107 ),
inference(sat_conversion,[],[f1986]) ).
cnf(s266,plain,
( ~ spl12_3
| ~ spl12_8 ),
inference(sat_conversion,[],[f2040]) ).
cnf(s270,plain,
( ~ spl12_173
| ~ spl12_187 ),
inference(sat_conversion,[],[f2056]) ).
cnf(s274,plain,
( spl12_28
| ~ spl12_107
| ~ spl12_185
| ~ spl12_192 ),
inference(sat_conversion,[],[f2072]) ).
cnf(s294,plain,
( ~ spl12_191
| ~ spl12_198 ),
inference(sat_conversion,[],[f2159]) ).
cnf(s302,plain,
( ~ spl12_3
| spl12_8
| ~ spl12_201
| ~ spl12_206 ),
inference(sat_conversion,[],[f2196]) ).
cnf(s304,plain,
( ~ spl12_3
| spl12_8
| ~ spl12_203
| ~ spl12_208 ),
inference(sat_conversion,[],[f2204]) ).
cnf(s310,plain,
( spl12_28
| ~ spl12_107
| ~ spl12_207
| ~ spl12_212 ),
inference(sat_conversion,[],[f2228]) ).
cnf(s362,plain,
( ~ spl12_249
| ~ spl12_256 ),
inference(sat_conversion,[],[f2424]) ).
cnf(s377,plain,
( ~ spl12_267
| ~ spl12_272 ),
inference(sat_conversion,[],[f2488]) ).
cnf(s381,plain,
( ~ spl12_272
| ~ spl12_277 ),
inference(sat_conversion,[],[f2505]) ).
cnf(s389,plain,
( ~ spl12_238
| ~ spl12_245 ),
inference(sat_conversion,[],[f2539]) ).
cnf(s398,plain,
( ~ spl12_249
| ~ spl12_263 ),
inference(sat_conversion,[],[f2586]) ).
cnf(s400,plain,
( ~ spl12_285
| ~ spl12_288 ),
inference(sat_conversion,[],[f2602]) ).
cnf(s408,plain,
( ~ spl12_285
| ~ spl12_294 ),
inference(sat_conversion,[],[f2632]) ).
cnf(s435,plain,
( ~ spl12_242
| ~ spl12_285 ),
inference(sat_conversion,[],[f2867]) ).
cnf(s437,plain,
( ~ spl12_251
| ~ spl12_253 ),
inference(sat_conversion,[],[f2870]) ).
cnf(s439,plain,
( ~ spl12_249
| ~ spl12_250 ),
inference(sat_conversion,[],[f2872]) ).
cnf(s440,plain,
( spl12_249
| ~ spl12_285 ),
inference(sat_conversion,[],[f2873]) ).
cnf(s444,plain,
( ~ spl12_241
| ~ spl12_262 ),
inference(sat_conversion,[],[f2879]) ).
cnf(s447,plain,
( ~ spl12_260
| ~ spl12_296 ),
inference(sat_conversion,[],[f2892]) ).
cnf(s448,plain,
( ~ spl12_239
| ~ spl12_285 ),
inference(sat_conversion,[],[f2893]) ).
cnf(s453,plain,
( ~ spl12_261
| ~ spl12_300 ),
inference(sat_conversion,[],[f2899]) ).
cnf(s454,plain,
( ~ spl12_285
| ~ spl12_286 ),
inference(sat_conversion,[],[f2900]) ).
cnf(s457,plain,
( ~ spl12_285
| ~ spl12_287 ),
inference(sat_conversion,[],[f2907]) ).
cnf(s461,plain,
( ~ spl12_268
| ~ spl12_285 ),
inference(sat_conversion,[],[f2911]) ).
cnf(s469,plain,
( ~ spl12_185
| ~ spl12_225 ),
inference(sat_conversion,[],[f2993]) ).
cnf(s471,plain,
( ~ spl12_185
| ~ spl12_186 ),
inference(sat_conversion,[],[f2995]) ).
cnf(s472,plain,
( spl12_185
| ~ spl12_221 ),
inference(sat_conversion,[],[f2997]) ).
cnf(s474,plain,
( ~ spl12_196
| ~ spl12_232 ),
inference(sat_conversion,[],[f3001]) ).
cnf(s475,plain,
( ~ spl12_175
| ~ spl12_221 ),
inference(sat_conversion,[],[f3002]) ).
cnf(s483,plain,
( ~ spl12_221
| ~ spl12_222 ),
inference(sat_conversion,[],[f3020]) ).
cnf(s484,plain,
( ~ spl12_202
| ~ spl12_221 ),
inference(sat_conversion,[],[f3025]) ).
cnf(s486,plain,
( ~ spl12_221
| ~ spl12_223 ),
inference(sat_conversion,[],[f3027]) ).
cnf(s494,plain,
( ~ spl12_221
| ~ spl12_227 ),
inference(sat_conversion,[],[f3068]) ).
cnf(s507,plain,
( ~ spl12_149
| spl12_192
| ~ spl12_221 ),
inference(sat_conversion,[],[f3158]) ).
cnf(s513,plain,
( ~ spl12_193
| ~ spl12_229 ),
inference(sat_conversion,[],[f3170]) ).
cnf(s518,plain,
( ~ spl12_173
| ~ spl12_177 ),
inference(sat_conversion,[],[f3178]) ).
cnf(s519,plain,
( ~ spl12_198
| ~ spl12_200 ),
inference(sat_conversion,[],[f3179]) ).
cnf(s525,plain,
( ~ spl12_184
| ~ spl12_185 ),
inference(sat_conversion,[],[f3190]) ).
cnf(s538,plain,
( ~ spl12_214
| ~ spl12_228 ),
inference(sat_conversion,[],[f3205]) ).
cnf(s542,plain,
( ~ spl12_3
| spl12_8
| ~ spl12_221
| ~ spl12_224 ),
inference(sat_conversion,[],[f3212]) ).
cnf(s556,plain,
( ~ spl12_138
| ~ spl12_183
| spl12_220 ),
inference(sat_conversion,[],[f3285]) ).
cnf(s559,plain,
( ~ spl12_204
| ~ spl12_221 ),
inference(sat_conversion,[],[f3297]) ).
cnf(s561,plain,
( ~ spl12_185
| ~ spl12_209 ),
inference(sat_conversion,[],[f3311]) ).
cnf(s566,plain,
( ~ spl12_219
| ~ spl12_220 ),
inference(sat_conversion,[],[f3317]) ).
cnf(s584,plain,
( ~ spl12_143
| spl12_200
| ~ spl12_203 ),
inference(sat_conversion,[],[f3348]) ).
cnf(s589,plain,
( ~ spl12_180
| ~ spl12_185 ),
inference(sat_conversion,[],[f3352]) ).
cnf(s607,plain,
( spl12_15
| ~ spl12_201 ),
inference(sat_conversion,[],[f3429]) ).
cnf(s616,plain,
( ~ spl12_138
| ~ spl12_176
| spl12_200 ),
inference(sat_conversion,[],[f3484]) ).
cnf(s624,plain,
( ~ spl12_138
| ~ spl12_190
| spl12_232 ),
inference(sat_conversion,[],[f3492]) ).
cnf(s625,plain,
( ~ spl12_181
| ~ spl12_206 ),
inference(sat_conversion,[],[f3494]) ).
cnf(s660,plain,
( ~ spl12_140
| ~ spl12_174
| spl12_184 ),
inference(sat_conversion,[],[f3606]) ).
cnf(s662,plain,
( ~ spl12_146
| spl12_173
| ~ spl12_177 ),
inference(sat_conversion,[],[f3613]) ).
cnf(s663,plain,
( ~ spl12_148
| spl12_175
| ~ spl12_193 ),
inference(sat_conversion,[],[f3621]) ).
cnf(s673,plain,
( ~ spl12_181
| ~ spl12_182 ),
inference(sat_conversion,[],[f3631]) ).
cnf(s687,plain,
( ~ spl12_210
| ~ spl12_226 ),
inference(sat_conversion,[],[f3639]) ).
cnf(s705,plain,
( ~ spl12_139
| ~ spl12_189
| spl12_227 ),
inference(sat_conversion,[],[f3730]) ).
cnf(s708,plain,
( ~ spl12_145
| spl12_184
| ~ spl12_201 ),
inference(sat_conversion,[],[f3743]) ).
cnf(s709,plain,
( ~ spl12_148
| spl12_173
| ~ spl12_179 ),
inference(sat_conversion,[],[f3749]) ).
cnf(s715,plain,
( ~ spl12_173
| ~ spl12_176 ),
inference(sat_conversion,[],[f3758]) ).
cnf(s751,plain,
( ~ spl12_188
| ~ spl12_214 ),
inference(sat_conversion,[],[f3779]) ).
cnf(s760,plain,
( ~ spl12_139
| ~ spl12_182
| spl12_214 ),
inference(sat_conversion,[],[f3780]) ).
cnf(s763,plain,
( ~ spl12_3
| spl12_8
| ~ spl12_140
| ~ spl12_195
| ~ spl12_203 ),
inference(sat_conversion,[],[f3883]) ).
cnf(s776,plain,
( ~ spl12_163
| spl12_248
| ~ spl12_265 ),
inference(sat_conversion,[],[f3947]) ).
cnf(s779,plain,
( ~ spl12_167
| spl12_256
| ~ spl12_285 ),
inference(sat_conversion,[],[f3960]) ).
cnf(s781,plain,
( ~ spl12_156
| ~ spl12_240
| spl12_264 ),
inference(sat_conversion,[],[f3964]) ).
cnf(s782,plain,
( ~ spl12_262
| ~ spl12_264 ),
inference(sat_conversion,[],[f3968]) ).
cnf(s787,plain,
( ~ spl12_166
| spl12_237
| ~ spl12_243 ),
inference(sat_conversion,[],[f3977]) ).
cnf(s792,plain,
( ~ spl12_164
| spl12_240
| ~ spl12_262 ),
inference(sat_conversion,[],[f4000]) ).
cnf(s793,plain,
( ~ spl12_238
| ~ spl12_265 ),
inference(sat_conversion,[],[f4001]) ).
cnf(s796,plain,
( ~ spl12_243
| ~ spl12_297 ),
inference(sat_conversion,[],[f4005]) ).
cnf(s804,plain,
( ~ spl12_169
| spl12_238
| ~ spl12_249 ),
inference(sat_conversion,[],[f4017]) ).
cnf(s812,plain,
( ~ spl12_156
| ~ spl12_247
| spl12_284 ),
inference(sat_conversion,[],[f4073]) ).
cnf(s821,plain,
( ~ spl12_157
| ~ spl12_260
| spl12_292 ),
inference(sat_conversion,[],[f4109]) ).
cnf(s824,plain,
( ~ spl12_240
| ~ spl12_267 ),
inference(sat_conversion,[],[f4118]) ).
cnf(s828,plain,
( ~ spl12_237
| ~ spl12_243 ),
inference(sat_conversion,[],[f4122]) ).
cnf(s832,plain,
( ~ spl12_275
| ~ spl12_278 ),
inference(sat_conversion,[],[f4127]) ).
cnf(s834,plain,
( ~ spl12_243
| ~ spl12_269 ),
inference(sat_conversion,[],[f4132]) ).
cnf(s839,plain,
( ~ spl12_257
| ~ spl12_293 ),
inference(sat_conversion,[],[f4136]) ).
cnf(s849,plain,
( ~ spl12_283
| ~ spl12_284 ),
inference(sat_conversion,[],[f4148]) ).
cnf(s852,plain,
( ~ spl12_255
| ~ spl12_262 ),
inference(sat_conversion,[],[f4172]) ).
cnf(s854,plain,
( ~ spl12_271
| ~ spl12_276 ),
inference(sat_conversion,[],[f4187]) ).
cnf(s855,plain,
( ~ spl12_156
| ~ spl12_261
| spl12_300 ),
inference(sat_conversion,[],[f4225]) ).
cnf(s856,plain,
( ~ spl12_259
| ~ spl12_283 ),
inference(sat_conversion,[],[f4228]) ).
cnf(s860,plain,
( ~ spl12_237
| ~ spl12_240 ),
inference(sat_conversion,[],[f4231]) ).
cnf(s872,plain,
( ~ spl12_158
| ~ spl12_245
| spl12_270 ),
inference(sat_conversion,[],[f4272]) ).
cnf(s883,plain,
( ~ spl12_244
| ~ spl12_249 ),
inference(sat_conversion,[],[f4297]) ).
cnf(s889,plain,
( ~ spl12_266
| ~ spl12_285 ),
inference(sat_conversion,[],[f4299]) ).
cnf(s894,plain,
( ~ spl12_246
| ~ spl12_260 ),
inference(sat_conversion,[],[f4304]) ).
cnf(s911,plain,
( ~ spl12_249
| ~ spl12_273 ),
inference(sat_conversion,[],[f4323]) ).
cnf(s913,plain,
( ~ spl12_292
| ~ spl12_295 ),
inference(sat_conversion,[],[f4327]) ).
cnf(s937,plain,
( ~ spl12_258
| ~ spl12_262 ),
inference(sat_conversion,[],[f4382]) ).
cnf(s941,plain,
( ~ spl12_248
| ~ spl12_249 ),
inference(sat_conversion,[],[f4388]) ).
cnf(s945,plain,
( ~ spl12_297
| ~ spl12_299 ),
inference(sat_conversion,[],[f4427]) ).
cnf(s947,plain,
( ~ spl12_166
| spl12_239
| ~ spl12_257 ),
inference(sat_conversion,[],[f4482]) ).
cnf(s953,plain,
( ~ spl12_274
| ~ spl12_290 ),
inference(sat_conversion,[],[f4493]) ).
cnf(s955,plain,
( ~ spl12_156
| ~ spl12_254
| spl12_296 ),
inference(sat_conversion,[],[f4497]) ).
cnf(s963,plain,
( spl12_86
| ~ spl12_198
| ~ spl12_201 ),
inference(sat_conversion,[],[f4553]) ).
cnf(s964,plain,
( ~ spl12_18
| spl12_74
| ~ spl12_86
| ~ spl12_208
| ~ spl12_278 ),
inference(sat_conversion,[],[f4556]) ).
cnf(s965,plain,
( ~ spl12_15
| spl12_65
| ~ spl12_173
| ~ spl12_237 ),
inference(sat_conversion,[],[f4564]) ).
cnf(s966,plain,
( ~ spl12_15
| spl12_66
| ~ spl12_81
| ~ spl12_86
| ~ spl12_190
| ~ spl12_259 ),
inference(sat_conversion,[],[f4573]) ).
cnf(s991,plain,
( spl12_81
| ~ spl12_193
| ~ spl12_198
| ~ spl12_201 ),
inference(sat_conversion,[],[f4765]) ).
cnf(s993,plain,
( ~ spl12_15
| ~ spl12_18
| spl12_67
| ~ spl12_86
| ~ spl12_195
| ~ spl12_246 ),
inference(sat_conversion,[],[f4774]) ).
cnf(s994,plain,
( ~ spl12_15
| ~ spl12_18
| spl12_68
| ~ spl12_81
| ~ spl12_182
| ~ spl12_254 ),
inference(sat_conversion,[],[f4784]) ).
cnf(s995,plain,
( ~ spl12_15
| spl12_69
| ~ spl12_81
| ~ spl12_86
| ~ spl12_193
| ~ spl12_262 ),
inference(sat_conversion,[],[f4794]) ).
cnf(s996,plain,
( ~ spl12_15
| spl12_70
| ~ spl12_86
| ~ spl12_233
| ~ spl12_265 ),
inference(sat_conversion,[],[f4803]) ).
cnf(s997,plain,
( ~ spl12_18
| spl12_71
| ~ spl12_86
| ~ spl12_210
| ~ spl12_276 ),
inference(sat_conversion,[],[f4812]) ).
cnf(s998,plain,
( spl12_72
| ~ spl12_81
| ~ spl12_86
| ~ spl12_232
| ~ spl12_272 ),
inference(sat_conversion,[],[f4822]) ).
cnf(s999,plain,
( ~ spl12_15
| ~ spl12_18
| spl12_73
| ~ spl12_86
| ~ spl12_198
| ~ spl12_249 ),
inference(sat_conversion,[],[f4832]) ).
cnf(s1000,plain,
( ~ spl12_15
| ~ spl12_18
| spl12_75
| ~ spl12_201
| ~ spl12_285 ),
inference(sat_conversion,[],[f4841]) ).
cnf(s1001,plain,
( ~ spl12_18
| spl12_76
| ~ spl12_81
| ~ spl12_212
| ~ spl12_295 ),
inference(sat_conversion,[],[f4850]) ).
cnf(s1002,plain,
( ~ spl12_15
| ~ spl12_18
| spl12_77
| ~ spl12_81
| ~ spl12_185
| ~ spl12_257 ),
inference(sat_conversion,[],[f4860]) ).
cnf(s1003,plain,
( spl12_78
| ~ spl12_81
| ~ spl12_86
| ~ spl12_231
| ~ spl12_274 ),
inference(sat_conversion,[],[f4870]) ).
cnf(s1004,plain,
( ~ spl12_18
| spl12_79
| ~ spl12_81
| ~ spl12_214
| ~ spl12_296 ),
inference(sat_conversion,[],[f4880]) ).
cnf(s1005,plain,
( ~ spl12_15
| spl12_80
| ~ spl12_81
| ~ spl12_221
| ~ spl12_297 ),
inference(sat_conversion,[],[f4889]) ).
cnf(s1011,plain,
( ~ spl12_270
| ~ spl12_272 ),
inference(sat_conversion,[],[f4906]) ).
cnf(s1014,plain,
( ~ spl12_249
| spl12_262
| ~ spl12_285 ),
inference(sat_conversion,[],[f4913]) ).
cnf(s1018,plain,
( ~ spl12_238
| ~ spl12_259 ),
inference(sat_conversion,[],[f4930]) ).
cnf(s1026,plain,
( ~ spl12_265
| ~ spl12_267 ),
inference(sat_conversion,[],[f4952]) ).
cnf(s1033,plain,
( ~ spl12_158
| ~ spl12_259
| spl12_272 ),
inference(sat_conversion,[],[f4966]) ).
cnf(s1084,plain,
( ~ spl12_185
| spl12_198
| ~ spl12_221 ),
inference(sat_conversion,[],[f4999]) ).
cnf(s1093,plain,
~ spl12_204,
inference(rat,[],[s559,s246]) ).
cnf(s1094,plain,
~ spl12_227,
inference(rat,[],[s494,s246]) ).
cnf(s1095,plain,
~ spl12_223,
inference(rat,[],[s486,s246]) ).
cnf(s1096,plain,
~ spl12_202,
inference(rat,[],[s484,s246]) ).
cnf(s1097,plain,
~ spl12_222,
inference(rat,[],[s483,s246]) ).
cnf(s1098,plain,
~ spl12_175,
inference(rat,[],[s475,s246]) ).
cnf(s1099,plain,
spl12_185,
inference(rat,[],[s472,s246]) ).
cnf(s1102,plain,
spl12_198,
inference(rat,[],[s1084,s246,s1099]) ).
cnf(s1104,plain,
~ spl12_180,
inference(rat,[],[s589,s1099]) ).
cnf(s1105,plain,
~ spl12_209,
inference(rat,[],[s561,s1099]) ).
cnf(s1106,plain,
~ spl12_184,
inference(rat,[],[s525,s1099]) ).
cnf(s1107,plain,
~ spl12_186,
inference(rat,[],[s471,s1099]) ).
cnf(s1108,plain,
~ spl12_225,
inference(rat,[],[s469,s1099]) ).
cnf(s1111,plain,
~ spl12_200,
inference(rat,[],[s519,s1102]) ).
cnf(s1113,plain,
~ spl12_191,
inference(rat,[],[s294,s1102]) ).
cnf(s1116,plain,
~ spl12_266,
inference(rat,[],[s889,s245]) ).
cnf(s1118,plain,
~ spl12_268,
inference(rat,[],[s461,s245]) ).
cnf(s1119,plain,
~ spl12_287,
inference(rat,[],[s457,s245]) ).
cnf(s1120,plain,
~ spl12_286,
inference(rat,[],[s454,s245]) ).
cnf(s1121,plain,
~ spl12_239,
inference(rat,[],[s448,s245]) ).
cnf(s1122,plain,
spl12_249,
inference(rat,[],[s440,s245]) ).
cnf(s1123,plain,
~ spl12_242,
inference(rat,[],[s435,s245]) ).
cnf(s1124,plain,
~ spl12_294,
inference(rat,[],[s408,s245]) ).
cnf(s1125,plain,
~ spl12_288,
inference(rat,[],[s400,s245]) ).
cnf(s1126,plain,
spl12_262,
inference(rat,[],[s1014,s245,s1122]) ).
cnf(s1127,plain,
~ spl12_248,
inference(rat,[],[s941,s1122]) ).
cnf(s1128,plain,
~ spl12_273,
inference(rat,[],[s911,s1122]) ).
cnf(s1129,plain,
~ spl12_244,
inference(rat,[],[s883,s1122]) ).
cnf(s1130,plain,
~ spl12_250,
inference(rat,[],[s439,s1122]) ).
cnf(s1132,plain,
~ spl12_263,
inference(rat,[],[s398,s1122]) ).
cnf(s1133,plain,
~ spl12_256,
inference(rat,[],[s362,s1122]) ).
cnf(s1135,plain,
~ spl12_258,
inference(rat,[],[s937,s1126]) ).
cnf(s1136,plain,
~ spl12_255,
inference(rat,[],[s852,s1126]) ).
cnf(s1137,plain,
~ spl12_264,
inference(rat,[],[s782,s1126]) ).
cnf(s1138,plain,
~ spl12_241,
inference(rat,[],[s444,s1126]) ).
cnf(s1139,plain,
~ spl12_167,
inference(rat,[],[s779,s245,s1133]) ).
cnf(s1140,plain,
( spl12_290
| spl12_293
| spl12_296 ),
inference(rat,[],[s243,s1119]) ).
cnf(s1141,plain,
( spl12_243
| spl12_257 ),
inference(rat,[],[s241,s1137,s1130]) ).
cnf(s1143,plain,
( spl12_278
| spl12_283 ),
inference(rat,[],[s238,s1128,s1118]) ).
cnf(s1146,plain,
( spl12_246
| spl12_253
| spl12_260 ),
inference(rat,[],[s231,s1121]) ).
cnf(s1147,plain,
( spl12_237
| spl12_251 ),
inference(rat,[],[s229,s1135,s1129]) ).
cnf(s1151,plain,
( spl12_240
| spl12_267
| spl12_297 ),
inference(rat,[],[s222,s1120]) ).
cnf(s1154,plain,
( spl12_283
| spl12_295 ),
inference(rat,[],[s219,s1124,s1132]) ).
cnf(s1157,plain,
( spl12_246
| spl12_271
| spl12_290 ),
inference(rat,[],[s216,s1125]) ).
cnf(s1159,plain,
( spl12_275
| spl12_276
| spl12_277 ),
inference(rat,[],[s209,s1136]) ).
cnf(s1160,plain,
( spl12_245
| spl12_270
| spl12_274 ),
inference(rat,[],[s208,s1128]) ).
cnf(s1162,plain,
( spl12_238
| spl12_265
| spl12_269 ),
inference(rat,[],[s206,s1118]) ).
cnf(s1163,plain,
( spl12_265
| spl12_267 ),
inference(rat,[],[s205,s1116,s1138]) ).
cnf(s1164,plain,
( spl12_259
| spl12_260
| spl12_261 ),
inference(rat,[],[s203,s1135]) ).
cnf(s1166,plain,
( spl12_245
| spl12_246
| spl12_247 ),
inference(rat,[],[s199,s1129]) ).
cnf(s1167,plain,
( spl12_237
| spl12_243 ),
inference(rat,[],[s198,s1123,s1138]) ).
cnf(s1169,plain,
( spl12_226
| spl12_229
| spl12_232 ),
inference(rat,[],[s195,s1095]) ).
cnf(s1170,plain,
( spl12_179
| spl12_193 ),
inference(rat,[],[s193,s1111,s1107]) ).
cnf(s1171,plain,
( spl12_228
| spl12_231 ),
inference(rat,[],[s192,s1108,s1097]) ).
cnf(s1172,plain,
( spl12_214
| spl12_219 ),
inference(rat,[],[s190,s1105,s1093]) ).
cnf(s1175,plain,
( spl12_182
| spl12_189
| spl12_196 ),
inference(rat,[],[s183,s1098]) ).
cnf(s1180,plain,
( spl12_176
| spl12_203
| spl12_233 ),
inference(rat,[],[s174,s1097]) ).
cnf(s1183,plain,
( spl12_189
| spl12_212
| spl12_229 ),
inference(rat,[],[s170,s1094]) ).
cnf(s1187,plain,
( spl12_181
| spl12_206
| spl12_210 ),
inference(rat,[],[s160,s1105]) ).
cnf(s1188,plain,
( spl12_206
| spl12_207
| spl12_208 ),
inference(rat,[],[s159,s1106]) ).
cnf(s1190,plain,
( spl12_177
| spl12_201
| spl12_203 ),
inference(rat,[],[s157,s1096]) ).
cnf(s1192,plain,
( spl12_187
| spl12_192
| spl12_193 ),
inference(rat,[],[s154,s1113]) ).
cnf(s1193,plain,
( spl12_181
| spl12_182
| spl12_183 ),
inference(rat,[],[s151,s1104]) ).
cnf(s1195,plain,
( spl12_173
| spl12_174
| spl12_176 ),
inference(rat,[],[s149,s1098]) ).
cnf(s1199,plain,
( spl12_155
| ~ spl12_160
| spl12_166 ),
inference(rat,[],[s134,s1139]) ).
cnf(s1200,plain,
~ spl12_8,
inference(rat,[],[s266,s100]) ).
cnf(s1201,plain,
~ spl12_224,
inference(rat,[],[s542,s100,s246,s1200]) ).
cnf(s1202,plain,
~ spl12_28,
inference(rat,[],[s252,s98]) ).
cnf(s1203,plain,
~ spl12_192,
inference(rat,[],[s274,s98,s1099,s1202]) ).
cnf(s1204,plain,
~ spl12_149,
inference(rat,[],[s507,s246,s1203]) ).
cnf(s1215,plain,
~ spl12_16,
inference(rat,[],[s14,s99]) ).
cnf(s1219,plain,
( spl12_137
| spl12_173 ),
inference(rat,[],[s1195,s660,s616,s103,s101,s1106,s1111]) ).
cnf(s1220,plain,
( ~ spl12_148
| spl12_173 ),
inference(rat,[],[s1170,s663,s709,s1098]) ).
cnf(s1221,plain,
spl12_173,
inference(rat,[],[s1190,s584,s708,s662,s105,s107,s108,s110,s1220,s1219,s1111,s1106,s1204]) ).
cnf(s1224,plain,
~ spl12_176,
inference(rat,[],[s715,s1221]) ).
cnf(s1225,plain,
~ spl12_177,
inference(rat,[],[s518,s1221]) ).
cnf(s1227,plain,
~ spl12_187,
inference(rat,[],[s270,s1221]) ).
cnf(s1232,plain,
spl12_193,
inference(rat,[],[s1192,s1203,s1227]) ).
cnf(s1235,plain,
~ spl12_229,
inference(rat,[],[s513,s1232]) ).
cnf(s1236,plain,
~ spl12_148,
inference(rat,[],[s663,s1098,s1232]) ).
cnf(s1241,plain,
( ~ spl12_203
| spl12_137 ),
inference(rat,[],[s556,s1193,s566,s760,s1172,s751,s182,s625,s1188,s763,s304,s101,s660,s103,s310,s1183,s705,s102,s100,s1200,s1202,s98,s1235,s1094,s1106]) ).
cnf(s1242,plain,
( spl12_265
| spl12_246
| spl12_237 ),
inference(rat,[],[s1154,s849,s913,s812,s821,s125,s126,s1199,s132,s792,s1166,s824,s389,s1163,s1162,s834,s787,s1167,s1146,s437,s1147,s1126]) ).
cnf(s1243,plain,
( ~ spl12_265
| spl12_237 ),
inference(rat,[],[s125,s136,s781,s131,s804,s1151,s776,s793,s1026,s796,s787,s1167,s1137,s1122,s1127]) ).
cnf(s1244,plain,
( ~ spl12_156
| ~ spl12_261 ),
inference(rat,[],[s453,s855]) ).
cnf(s1245,plain,
spl12_237,
inference(rat,[],[s1244,s1164,s1018,s125,s1199,s132,s792,s894,s824,s1242,s1163,s1162,s1243,s787,s834,s1167,s1126]) ).
cnf(s1246,plain,
~ spl12_240,
inference(rat,[],[s860,s1245]) ).
cnf(s1247,plain,
~ spl12_243,
inference(rat,[],[s828,s1245]) ).
cnf(s1250,plain,
~ spl12_164,
inference(rat,[],[s792,s1126,s1246]) ).
cnf(s1251,plain,
spl12_257,
inference(rat,[],[s1141,s1247]) ).
cnf(s1252,plain,
spl12_160,
inference(rat,[],[s132,s1250]) ).
cnf(s1253,plain,
~ spl12_293,
inference(rat,[],[s839,s1251]) ).
cnf(s1254,plain,
~ spl12_166,
inference(rat,[],[s947,s1121,s1251]) ).
cnf(s1256,plain,
spl12_155,
inference(rat,[],[s1199,s1254,s1252]) ).
cnf(s1258,plain,
spl12_158,
inference(rat,[],[s127,s1256]) ).
cnf(s1259,plain,
spl12_157,
inference(rat,[],[s126,s1256]) ).
cnf(s1260,plain,
spl12_156,
inference(rat,[],[s125,s1256]) ).
cnf(s1261,plain,
~ spl12_261,
inference(rat,[],[s1244,s1260]) ).
cnf(s1262,plain,
~ spl12_260,
inference(rat,[],[s849,s812,s1154,s232,s913,s955,s821,s447,s1260,s1261,s1246,s1259]) ).
cnf(s1263,plain,
spl12_259,
inference(rat,[],[s1164,s1261,s1262]) ).
cnf(s1264,plain,
spl12_272,
inference(rat,[],[s1033,s1258,s1263]) ).
cnf(s1266,plain,
~ spl12_283,
inference(rat,[],[s856,s1263]) ).
cnf(s1271,plain,
~ spl12_270,
inference(rat,[],[s1011,s1264]) ).
cnf(s1272,plain,
~ spl12_277,
inference(rat,[],[s381,s1264]) ).
cnf(s1273,plain,
~ spl12_267,
inference(rat,[],[s377,s1264]) ).
cnf(s1275,plain,
spl12_278,
inference(rat,[],[s1143,s1266]) ).
cnf(s1276,plain,
spl12_295,
inference(rat,[],[s1154,s1266]) ).
cnf(s1277,plain,
~ spl12_245,
inference(rat,[],[s872,s1258,s1271]) ).
cnf(s1278,plain,
spl12_265,
inference(rat,[],[s1163,s1273]) ).
cnf(s1279,plain,
spl12_297,
inference(rat,[],[s1151,s1246,s1273]) ).
cnf(s1280,plain,
~ spl12_275,
inference(rat,[],[s832,s1275]) ).
cnf(s1283,plain,
~ spl12_292,
inference(rat,[],[s913,s1276]) ).
cnf(s1288,plain,
spl12_274,
inference(rat,[],[s1160,s1271,s1277]) ).
cnf(s1292,plain,
~ spl12_299,
inference(rat,[],[s945,s1279]) ).
cnf(s1295,plain,
spl12_276,
inference(rat,[],[s1159,s1272,s1280]) ).
cnf(s1296,plain,
~ spl12_290,
inference(rat,[],[s953,s1288]) ).
cnf(s1300,plain,
spl12_254,
inference(rat,[],[s226,s1272,s1283,s1292]) ).
cnf(s1303,plain,
~ spl12_271,
inference(rat,[],[s854,s1295]) ).
cnf(s1305,plain,
spl12_296,
inference(rat,[],[s1140,s1253,s1296]) ).
cnf(s1310,plain,
spl12_246,
inference(rat,[],[s1157,s1296,s1303]) ).
cnf(s1315,plain,
( spl12_181
| spl12_137 ),
inference(rat,[],[s993,s53,s1004,s994,s997,s1003,s998,s966,s1171,s153,s182,s538,s751,s760,s168,s1169,s687,s1187,s660,s103,s1000,s12,s999,s995,s965,s1002,s964,s1188,s302,s310,s1001,s1183,s705,s102,s996,s963,s1180,s1005,s607,s991,s1190,s1241,s99,s1310,s1215,s1305,s1300,s1295,s1288,s1264,s1263,s1227,s1201,s1235,s1232,s1102,s1225,s246,s1279,s1224,s1278,s1094,s1276,s1202,s98,s1200,s100,s1275,s1099,s1251,s1221,s1245,s1126,s1122,s245,s1106]) ).
cnf(s1316,plain,
spl12_137,
inference(rat,[],[s624,s474,s153,s1175,s248,s673,s1315,s705,s101,s102,s1227,s98,s1202,s1094]) ).
cnf(s1317,plain,
spl12_142,
inference(rat,[],[s110,s1204,s1236,s1316]) ).
cnf(s1319,plain,
spl12_145,
inference(rat,[],[s107,s1317]) ).
cnf(s1321,plain,
spl12_143,
inference(rat,[],[s105,s1317]) ).
cnf(s1322,plain,
~ spl12_201,
inference(rat,[],[s708,s1106,s1319]) ).
cnf(s1324,plain,
~ spl12_203,
inference(rat,[],[s584,s1111,s1321]) ).
cnf(s1326,plain,
$false,
inference(rat,[],[s1190,s1225,s1322,s1324]) ).
fof(f5040,plain,
$false,
inference(avatar_sat_refutation,[],[s1326]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG107+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n013.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 19:27:52 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.76/0.41 % (1477566)Will run a generic schedule for satisfiability detection.
% 0.76/0.41 % (1477577)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2257204748:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.76/0.41 % (1477572)% WARNING: option uhcvi not known.
% 0.76/0.41 % (1477571)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1123619946_2999 on theBenchmark for (2999ds/0Mi)
% 0.76/0.41 % (1477572)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=190711400:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.76/0.41 % (1477573)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4050278946:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.76/0.41 % (1477574)dis+10_1_sil=32000:sp=arity:random_seed=3268568179:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.76/0.41 % (1477575)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3913239316:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.76/0.41 % (1477576)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4041917951:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.76/0.41 % Detected minimum model sizes of [8]
% 0.76/0.41 % Detected maximum model sizes of [max]
% 0.76/0.41 % TRYING [8]
% 0.76/0.41 % (1477577)Instruction limit reached!
% 0.76/0.41 % (1477577)------------------------------
% 0.76/0.41 % (1477577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.41 % (1477577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.41 % (1477577)CaDiCaL version: 2.1.3
% 0.76/0.41 % (1477577)Termination reason: Instruction limit
% 0.76/0.41 % (1477577)Termination phase: Saturation
% 0.76/0.41 % (1477577)Time elapsed: 0.046 s
% 0.76/0.41 % (1477577)Peak memory usage: 13 MB
% 0.76/0.41 % (1477577)Instructions burned: 162 (million)
% 0.76/0.41 % (1477585)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1340248360:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.76/0.41 % (1477574)Instruction limit reached!
% 0.76/0.41 % (1477574)------------------------------
% 0.76/0.41 % (1477574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.41 % (1477574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.41 % (1477574)CaDiCaL version: 2.1.3
% 0.76/0.41 % (1477574)Termination reason: Instruction limit
% 0.76/0.41 % (1477574)Termination phase: Saturation
% 0.76/0.41 % (1477574)Time elapsed: 0.052 s
% 0.76/0.41 % (1477574)Peak memory usage: 12 MB
% 0.76/0.41 % (1477574)Instructions burned: 106 (million)
% 0.76/0.41 % (1477575)Instruction limit reached!
% 0.76/0.41 % (1477575)------------------------------
% 0.76/0.41 % (1477575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.41 % (1477575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.41 % (1477575)CaDiCaL version: 2.1.3
% 0.76/0.41 % (1477575)Termination reason: Instruction limit
% 0.76/0.41 % (1477575)Termination phase: Saturation
% 0.76/0.41 % (1477575)Time elapsed: 0.056 s
% 0.76/0.41 % (1477575)Peak memory usage: 13 MB
% 0.76/0.41 % (1477575)Instructions burned: 117 (million)
% 0.76/0.41 % Detected minimum model sizes of [8]
% 0.76/0.41 % (1477576)Instruction limit reached!
% 0.76/0.41 % (1477576)------------------------------
% 0.76/0.41 % (1477576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.41 % Detected maximum model sizes of [max]
% 0.76/0.41 % (1477576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.41 % (1477576)CaDiCaL version: 2.1.3
% 0.76/0.41 % (1477576)Termination reason: Instruction limit
% 0.76/0.41 % (1477576)Termination phase: Saturation
% 0.76/0.41 % (1477576)Time elapsed: 0.064 s
% 0.76/0.41 % (1477576)Peak memory usage: 14 MB
% 0.76/0.41 % (1477576)Instructions burned: 136 (million)
% 0.76/0.41 % TRYING [8]
% 0.76/0.41 % (1477587)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3440514196:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.76/0.41 % (1477588)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=2453675125:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.76/0.41 % (1477589)ott-21_1_sil=16000:fs=off:random_seed=3584572367:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.76/0.41 % (1477572) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1477566-1477572"...
% 0.76/0.41 % (1477572)...printing done.
% 0.76/0.41 % (1477572)Refutation found. Thanks to Tanya!
% 0.76/0.41 % SZS status Theorem for theBenchmark
% 0.76/0.41 % SZS output start Proof for theBenchmark
% See solution above
% 0.76/0.42 % (1477572)------------------------------
% 0.76/0.42 % (1477572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.42 % (1477572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.42 % (1477572)CaDiCaL version: 2.1.3
% 0.76/0.42 % (1477572)Termination reason: Refutation
% 0.76/0.42 % (1477572)Time elapsed: 0.121 s
% 0.76/0.42 % (1477572)Peak memory usage: 14 MB
% 0.76/0.42 % (1477572)Instructions burned: 239 (million)
% 0.76/0.42 % (1477566)Success in time 0.174 s
% 0.76/0.42 % Vampire exiting
%------------------------------------------------------------------------------