%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG110+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:46 AM UTC 2026
% Result : Theorem 0.18s 0.32s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 147
% Syntax : Number of formulae : 987 ( 149 unt; 131 def)
% Number of atoms : 3481 (1541 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 4094 (1600 ~;1925 |; 438 &)
% ( 131 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 135 ( 133 usr; 134 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(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,e10) = e10
& op1(e10,e10) != e10 )
| ( op1(e11,e10) = e11
& op1(e10,e11) != e10 )
| ( op1(e12,e10) = e12
& op1(e10,e12) != e10 )
| ( op1(e13,e10) = e13
& op1(e10,e13) != e10 ) )
& ( ( op1(e10,e11) = e10
& op1(e11,e10) != e11 )
| ( op1(e11,e11) = e11
& op1(e11,e11) != e11 )
| ( op1(e12,e11) = e12
& op1(e11,e12) != e11 )
| ( op1(e13,e11) = e13
& op1(e11,e13) != e11 ) )
& ( ( op1(e10,e12) = e10
& op1(e12,e10) != e12 )
| ( op1(e11,e12) = e11
& op1(e12,e11) != e12 )
| ( op1(e12,e12) = e12
& op1(e12,e12) != e12 )
| ( op1(e13,e12) = e13
& op1(e12,e13) != e12 ) )
& ( ( op1(e10,e13) = e10
& op1(e13,e10) != e13 )
| ( op1(e11,e13) = e11
& op1(e13,e11) != e13 )
| ( op1(e12,e13) = e12
& op1(e13,e12) != e13 )
| ( op1(e13,e13) = e13
& op1(e13,e13) != e13 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( ( ( op2(e20,e20) = e20
& op2(e20,e20) != e20 )
| ( op2(e21,e20) = e21
& op2(e20,e21) != e20 )
| ( op2(e22,e20) = e22
& op2(e20,e22) != e20 )
| ( op2(e23,e20) = e23
& op2(e20,e23) != e20 ) )
& ( ( op2(e20,e21) = e20
& op2(e21,e20) != e21 )
| ( op2(e21,e21) = e21
& op2(e21,e21) != e21 )
| ( op2(e22,e21) = e22
& op2(e21,e22) != e21 )
| ( op2(e23,e21) = e23
& op2(e21,e23) != e21 ) )
& ( ( op2(e20,e22) = e20
& op2(e22,e20) != e22 )
| ( op2(e21,e22) = e21
& op2(e22,e21) != e22 )
| ( op2(e22,e22) = e22
& op2(e22,e22) != e22 )
| ( op2(e23,e22) = e23
& op2(e22,e23) != e22 ) )
& ( ( op2(e20,e23) = e20
& op2(e23,e20) != e23 )
| ( op2(e21,e23) = e21
& op2(e23,e21) != e23 )
| ( op2(e22,e23) = e22
& op2(e23,e22) != e23 )
| ( op2(e23,e23) = e23
& op2(e23,e23) != e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e10 = op1(op1(e12,e12),op1(e12,e12))
& e11 = op1(op1(op1(e12,e12),op1(e12,e12)),op1(e12,e12))
& e13 = op1(e12,e12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e20 = op2(op2(e22,e22),op2(e22,e22))
& e21 = op2(op2(op2(e22,e22),op2(e22,e22)),op2(e22,e22))
& e23 = op2(e22,e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( h1(e12) = e20
& h1(e10) = op2(op2(e20,e20),op2(e20,e20))
& h1(e11) = op2(op2(op2(e20,e20),op2(e20,e20)),op2(e20,e20))
& h1(e13) = op2(e20,e20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
( h2(e12) = e21
& h2(e10) = op2(op2(e21,e21),op2(e21,e21))
& h2(e11) = op2(op2(op2(e21,e21),op2(e21,e21)),op2(e21,e21))
& h2(e13) = op2(e21,e21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
( h3(e12) = e22
& h3(e10) = op2(op2(e22,e22),op2(e22,e22))
& h3(e11) = op2(op2(op2(e22,e22),op2(e22,e22)),op2(e22,e22))
& h3(e13) = op2(e22,e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
( h4(e12) = e23
& h4(e10) = op2(op2(e23,e23),op2(e23,e23))
& h4(e11) = op2(op2(op2(e23,e23),op2(e23,e23)),op2(e23,e23))
& h4(e13) = op2(e23,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f18,conjecture,
( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f19,negated_conjecture,
~ ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f20,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) ) )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) ) )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) ) )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) ) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f40,plain,
( e11 = op1(e13,e10)
| e11 = op1(e12,e10)
| e11 = op1(e11,e10)
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[],[f2]) ).
fof(f41,plain,
( e12 = op1(e10,e13)
| e12 = op1(e10,e12)
| e12 = op1(e10,e11)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f2]) ).
fof(f43,plain,
( e13 = op1(e10,e13)
| e13 = op1(e10,e12)
| e13 = op1(e10,e11)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f2]) ).
fof(f44,plain,
( e13 = op1(e13,e10)
| e13 = op1(e12,e10)
| e13 = op1(e11,e10)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f2]) ).
fof(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(f47,plain,
( e11 = op1(e11,e13)
| e11 = op1(e11,e12)
| e11 = op1(e11,e11)
| e11 = op1(e11,e10) ),
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(f51,plain,
( e13 = op1(e11,e13)
| e13 = op1(e11,e12)
| e13 = op1(e11,e11)
| e13 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f53,plain,
( e10 = op1(e12,e13)
| e10 = op1(e12,e12)
| e10 = op1(e12,e11)
| e10 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f54,plain,
( e10 = op1(e13,e12)
| e10 = op1(e12,e12)
| e10 = op1(e11,e12)
| e10 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f55,plain,
( e11 = op1(e12,e13)
| e11 = op1(e12,e12)
| e11 = op1(e12,e11)
| e11 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f56,plain,
( e11 = op1(e13,e12)
| e11 = op1(e12,e12)
| e11 = op1(e11,e12)
| e11 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f58,plain,
( e12 = op1(e13,e12)
| e12 = op1(e12,e12)
| e12 = op1(e11,e12)
| e12 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f65,plain,
( e12 = op1(e13,e13)
| e12 = op1(e13,e12)
| e12 = op1(e13,e11)
| e12 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f68,plain,
( e13 = op1(e13,e13)
| e13 = op1(e12,e13)
| e13 = op1(e11,e13)
| e13 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f83,plain,
( e23 = op2(e23,e22)
| e22 = op2(e23,e22)
| e21 = op2(e23,e22)
| e20 = op2(e23,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f86,plain,
( e20 = op2(e23,e20)
| e20 = op2(e22,e20)
| e20 = op2(e21,e20)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f90,plain,
( e22 = op2(e23,e20)
| e22 = op2(e22,e20)
| e22 = op2(e21,e20)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f4]) ).
fof(f92,plain,
( e23 = op2(e23,e20)
| e23 = op2(e22,e20)
| e23 = op2(e21,e20)
| op2(e20,e20) = e23 ),
inference(cnf_transformation,[],[f4]) ).
fof(f93,plain,
( e20 = op2(e21,e23)
| e20 = op2(e21,e22)
| e20 = op2(e21,e21)
| e20 = 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(f98,plain,
( e22 = op2(e23,e21)
| e22 = op2(e22,e21)
| e22 = op2(e21,e21)
| e22 = op2(e20,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f99,plain,
( e23 = op2(e21,e23)
| e23 = op2(e21,e22)
| e23 = op2(e21,e21)
| e23 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f102,plain,
( e20 = op2(e23,e22)
| e20 = op2(e22,e22)
| e20 = op2(e21,e22)
| e20 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f105,plain,
( e22 = op2(e22,e23)
| e22 = op2(e22,e22)
| e22 = op2(e22,e21)
| e22 = op2(e22,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f106,plain,
( e22 = op2(e23,e22)
| e22 = op2(e22,e22)
| e22 = op2(e21,e22)
| e22 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f117,plain,
op1(e13,e12) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f118,plain,
op1(e13,e11) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f119,plain,
op1(e13,e11) != op1(e13,e12),
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(f124,plain,
op1(e12,e11) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f126,plain,
op1(e12,e10) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f132,plain,
op1(e11,e10) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f133,plain,
op1(e11,e10) != op1(e11,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f135,plain,
op1(e10,e12) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f137,plain,
op1(e10,e11) != op1(e10,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f138,plain,
op1(e10,e10) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f141,plain,
op1(e12,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f144,plain,
op1(e10,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f145,plain,
op1(e10,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(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(f151,plain,
op1(e10,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f165,plain,
op2(e23,e22) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f167,plain,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f168,plain,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f169,plain,
op2(e23,e20) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f170,plain,
op2(e23,e20) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f172,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f179,plain,
op2(e21,e21) != op2(e21,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f184,plain,
op2(e20,e21) != op2(e20,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f185,plain,
op2(e20,e21) != op2(e20,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f187,plain,
op2(e20,e20) != op2(e20,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f190,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f194,plain,
op2(e20,e23) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f195,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f197,plain,
op2(e21,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f213,plain,
e12 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f214,plain,
e11 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f215,plain,
e11 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f216,plain,
e10 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f217,plain,
e10 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f218,plain,
e10 != e11,
inference(cnf_transformation,[],[f7]) ).
fof(f219,plain,
e22 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f221,plain,
e21 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f222,plain,
e20 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f224,plain,
e20 != e21,
inference(cnf_transformation,[],[f8]) ).
fof(f245,plain,
( e13 = op1(e13,e10)
| e12 = op1(e12,e10)
| e11 = op1(e11,e10)
| e10 != op1(e10,e10) ),
inference(cnf_transformation,[],[f10]) ).
fof(f246,plain,
( e13 = op1(e13,e10)
| e12 = op1(e12,e10)
| e11 = op1(e11,e10)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f10]) ).
fof(f258,plain,
( e13 = op1(e13,e11)
| e11 != op1(e11,e12)
| e11 = op1(e11,e11)
| e10 = op1(e10,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f260,plain,
( e13 = op1(e13,e11)
| e11 != op1(e11,e12)
| e11 != op1(e11,e11)
| e10 = op1(e10,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f262,plain,
( e13 = op1(e13,e11)
| e12 = op1(e12,e11)
| e11 = op1(e11,e11)
| e10 = op1(e10,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f264,plain,
( e13 = op1(e13,e11)
| e12 = op1(e12,e11)
| e11 != op1(e11,e11)
| e10 = op1(e10,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f266,plain,
( e11 != op1(e11,e13)
| e11 != op1(e11,e12)
| e11 = op1(e11,e11)
| e10 = op1(e10,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f268,plain,
( e11 != op1(e11,e13)
| e11 != op1(e11,e12)
| e11 != op1(e11,e11)
| e10 = op1(e10,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f270,plain,
( e11 != op1(e11,e13)
| e12 = op1(e12,e11)
| e11 = op1(e11,e11)
| e10 = op1(e10,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f272,plain,
( e11 != op1(e11,e13)
| e12 = op1(e12,e11)
| e11 != op1(e11,e11)
| e10 = op1(e10,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f274,plain,
( e13 = op1(e13,e12)
| e12 != op1(e12,e12)
| e11 = op1(e11,e12)
| e10 = op1(e10,e12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f278,plain,
( e13 = op1(e13,e12)
| e12 = op1(e12,e12)
| e11 = op1(e11,e12)
| e10 = op1(e10,e12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f294,plain,
( e13 = op1(e13,e13)
| e12 = op1(e12,e13)
| e11 = op1(e11,e13)
| e10 = op1(e10,e13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f302,plain,
( e13 != op1(e13,e13)
| e12 = op1(e12,e13)
| e11 = op1(e11,e13)
| e10 = op1(e10,e13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f306,plain,
( e23 = op2(e23,e20)
| e20 != op2(e20,e22)
| e21 = op2(e21,e20)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f11]) ).
fof(f326,plain,
( e23 = op2(e23,e21)
| e22 = op2(e22,e21)
| e21 = op2(e21,e21)
| e20 = op2(e20,e21) ),
inference(cnf_transformation,[],[f11]) ).
fof(f328,plain,
( e23 = op2(e23,e21)
| e22 = op2(e22,e21)
| e21 != op2(e21,e21)
| e20 = op2(e20,e21) ),
inference(cnf_transformation,[],[f11]) ).
fof(f342,plain,
( e23 = op2(e23,e22)
| e22 = op2(e22,e22)
| e21 = op2(e21,e22)
| e20 = op2(e20,e22) ),
inference(cnf_transformation,[],[f11]) ).
fof(f357,plain,
( e23 = op2(e23,e23)
| e22 = op2(e22,e23)
| e21 = op2(e21,e23)
| e23 != op2(e23,e20) ),
inference(cnf_transformation,[],[f11]) ).
fof(f369,plain,
e13 = op1(e12,e12),
inference(cnf_transformation,[],[f12]) ).
fof(f370,plain,
e11 = op1(op1(op1(e12,e12),op1(e12,e12)),op1(e12,e12)),
inference(cnf_transformation,[],[f12]) ).
fof(f371,plain,
e10 = op1(op1(e12,e12),op1(e12,e12)),
inference(cnf_transformation,[],[f12]) ).
fof(f372,plain,
e23 = op2(e22,e22),
inference(cnf_transformation,[],[f13]) ).
fof(f373,plain,
e21 = op2(op2(op2(e22,e22),op2(e22,e22)),op2(e22,e22)),
inference(cnf_transformation,[],[f13]) ).
fof(f374,plain,
e20 = op2(op2(e22,e22),op2(e22,e22)),
inference(cnf_transformation,[],[f13]) ).
fof(f378,plain,
e20 = h1(e12),
inference(cnf_transformation,[],[f14]) ).
fof(f379,plain,
op2(e21,e21) = h2(e13),
inference(cnf_transformation,[],[f15]) ).
fof(f380,plain,
h2(e11) = op2(op2(op2(e21,e21),op2(e21,e21)),op2(e21,e21)),
inference(cnf_transformation,[],[f15]) ).
fof(f381,plain,
h2(e10) = op2(op2(e21,e21),op2(e21,e21)),
inference(cnf_transformation,[],[f15]) ).
fof(f382,plain,
e21 = h2(e12),
inference(cnf_transformation,[],[f15]) ).
fof(f386,plain,
e22 = h3(e12),
inference(cnf_transformation,[],[f16]) ).
fof(f390,plain,
e23 = h4(e12),
inference(cnf_transformation,[],[f17]) ).
fof(f399,plain,
( e20 != h2(e13)
| ~ sP5 ),
inference(cnf_transformation,[],[f20]) ).
fof(f404,plain,
( e21 != h2(e12)
| ~ sP4 ),
inference(cnf_transformation,[],[f20]) ).
fof(f441,plain,
( e23 != h2(e10)
| e22 != h2(e11)
| sP4
| sP5
| 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(f561,definition,
( spl8_3
<=> e20 = h1(e12) ),
introduced(definition,[new_symbols(definition,[spl8_3])],[avatar_definition]) ).
fof(f562,plain,
( e20 = h1(e12)
| ~ spl8_3 ),
inference(avatar_component_clause,[],[f561]) ).
fof(f585,definition,
( spl8_8
<=> e21 = h1(e12) ),
introduced(definition,[new_symbols(definition,[spl8_8])],[avatar_definition]) ).
fof(f586,plain,
( e21 = h1(e12)
| ~ spl8_8 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f587,plain,
( e21 != h1(e12)
| spl8_8 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f600,definition,
( spl8_11
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl8_11])],[avatar_definition]) ).
fof(f604,definition,
( spl8_12
<=> e20 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl8_12])],[avatar_definition]) ).
fof(f605,plain,
( e20 = h2(e13)
| ~ spl8_12 ),
inference(avatar_component_clause,[],[f604]) ).
fof(f607,plain,
( ~ spl8_11
| ~ spl8_12 ),
inference(avatar_split_clause,[],[f399,f604,f600]) ).
fof(f624,definition,
( spl8_16
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl8_16])],[avatar_definition]) ).
fof(f633,definition,
( spl8_18
<=> e21 = h2(e12) ),
introduced(definition,[new_symbols(definition,[spl8_18])],[avatar_definition]) ).
fof(f634,plain,
( e21 = h2(e12)
| ~ spl8_18 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f636,plain,
( ~ spl8_16
| ~ spl8_18 ),
inference(avatar_split_clause,[],[f404,f633,f624]) ).
fof(f657,definition,
( spl8_23
<=> e20 = h3(e12) ),
introduced(definition,[new_symbols(definition,[spl8_23])],[avatar_definition]) ).
fof(f658,plain,
( e20 = h3(e12)
| ~ spl8_23 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f659,plain,
( e20 != h3(e12)
| spl8_23 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f729,definition,
( spl8_38
<=> e21 = h4(e12) ),
introduced(definition,[new_symbols(definition,[spl8_38])],[avatar_definition]) ).
fof(f730,plain,
( e21 = h4(e12)
| ~ spl8_38 ),
inference(avatar_component_clause,[],[f729]) ).
fof(f731,plain,
( e21 != h4(e12)
| spl8_38 ),
inference(avatar_component_clause,[],[f729]) ).
fof(f856,definition,
( spl8_65
<=> h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_65])],[avatar_definition]) ).
fof(f858,plain,
( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| spl8_65 ),
inference(avatar_component_clause,[],[f856]) ).
fof(f860,definition,
( spl8_66
<=> h2(op1(e10,e11)) = op2(h2(e10),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_66])],[avatar_definition]) ).
fof(f862,plain,
( h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| spl8_66 ),
inference(avatar_component_clause,[],[f860]) ).
fof(f864,definition,
( spl8_67
<=> h2(op1(e10,e12)) = op2(h2(e10),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_67])],[avatar_definition]) ).
fof(f866,plain,
( h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| spl8_67 ),
inference(avatar_component_clause,[],[f864]) ).
fof(f868,definition,
( spl8_68
<=> h2(op1(e10,e13)) = op2(h2(e10),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_68])],[avatar_definition]) ).
fof(f870,plain,
( h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| spl8_68 ),
inference(avatar_component_clause,[],[f868]) ).
fof(f872,definition,
( spl8_69
<=> h2(op1(e11,e10)) = op2(h2(e11),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_69])],[avatar_definition]) ).
fof(f874,plain,
( h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| spl8_69 ),
inference(avatar_component_clause,[],[f872]) ).
fof(f876,definition,
( spl8_70
<=> h2(op1(e11,e11)) = op2(h2(e11),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_70])],[avatar_definition]) ).
fof(f878,plain,
( h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| spl8_70 ),
inference(avatar_component_clause,[],[f876]) ).
fof(f880,definition,
( spl8_71
<=> h2(op1(e11,e12)) = op2(h2(e11),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_71])],[avatar_definition]) ).
fof(f882,plain,
( h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| spl8_71 ),
inference(avatar_component_clause,[],[f880]) ).
fof(f884,definition,
( spl8_72
<=> h2(op1(e11,e13)) = op2(h2(e11),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_72])],[avatar_definition]) ).
fof(f886,plain,
( h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| spl8_72 ),
inference(avatar_component_clause,[],[f884]) ).
fof(f888,definition,
( spl8_73
<=> h2(op1(e12,e10)) = op2(h2(e12),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_73])],[avatar_definition]) ).
fof(f890,plain,
( h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| spl8_73 ),
inference(avatar_component_clause,[],[f888]) ).
fof(f892,definition,
( spl8_74
<=> h2(op1(e12,e11)) = op2(h2(e12),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_74])],[avatar_definition]) ).
fof(f894,plain,
( h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| spl8_74 ),
inference(avatar_component_clause,[],[f892]) ).
fof(f896,definition,
( spl8_75
<=> h2(op1(e12,e12)) = op2(h2(e12),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_75])],[avatar_definition]) ).
fof(f898,plain,
( h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| spl8_75 ),
inference(avatar_component_clause,[],[f896]) ).
fof(f900,definition,
( spl8_76
<=> h2(op1(e12,e13)) = op2(h2(e12),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_76])],[avatar_definition]) ).
fof(f902,plain,
( h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| spl8_76 ),
inference(avatar_component_clause,[],[f900]) ).
fof(f904,definition,
( spl8_77
<=> h2(op1(e13,e10)) = op2(h2(e13),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_77])],[avatar_definition]) ).
fof(f906,plain,
( h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| spl8_77 ),
inference(avatar_component_clause,[],[f904]) ).
fof(f908,definition,
( spl8_78
<=> h2(op1(e13,e11)) = op2(h2(e13),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_78])],[avatar_definition]) ).
fof(f910,plain,
( h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| spl8_78 ),
inference(avatar_component_clause,[],[f908]) ).
fof(f912,definition,
( spl8_79
<=> h2(op1(e13,e12)) = op2(h2(e13),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_79])],[avatar_definition]) ).
fof(f914,plain,
( h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| spl8_79 ),
inference(avatar_component_clause,[],[f912]) ).
fof(f916,definition,
( spl8_80
<=> h2(op1(e13,e13)) = op2(h2(e13),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_80])],[avatar_definition]) ).
fof(f918,plain,
( h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| spl8_80 ),
inference(avatar_component_clause,[],[f916]) ).
fof(f924,definition,
( spl8_82
<=> e23 = h2(e10) ),
introduced(definition,[new_symbols(definition,[spl8_82])],[avatar_definition]) ).
fof(f925,plain,
( e23 = h2(e10)
| ~ spl8_82 ),
inference(avatar_component_clause,[],[f924]) ).
fof(f934,definition,
( spl8_84
<=> e22 = h2(e11) ),
introduced(definition,[new_symbols(definition,[spl8_84])],[avatar_definition]) ).
fof(f935,plain,
( e22 = h2(e11)
| ~ spl8_84 ),
inference(avatar_component_clause,[],[f934]) ).
fof(f937,plain,
( ~ spl8_65
| ~ spl8_66
| ~ spl8_67
| ~ spl8_68
| ~ spl8_69
| ~ spl8_70
| ~ spl8_71
| ~ spl8_72
| ~ spl8_73
| ~ spl8_74
| ~ spl8_75
| ~ spl8_76
| ~ spl8_77
| ~ spl8_78
| ~ spl8_79
| ~ spl8_80
| spl8_11
| spl8_16
| ~ spl8_84
| ~ spl8_82 ),
inference(avatar_split_clause,[],[f441,f924,f934,f624,f600,f916,f912,f908,f904,f900,f896,f892,f888,f884,f880,f876,f872,f868,f864,f860,f856]) ).
fof(f1041,definition,
( spl8_107
<=> e22 = h3(e12) ),
introduced(definition,[new_symbols(definition,[spl8_107])],[avatar_definition]) ).
fof(f1042,plain,
( e22 = h3(e12)
| ~ spl8_107 ),
inference(avatar_component_clause,[],[f1041]) ).
fof(f1176,definition,
( spl8_135
<=> e23 = h4(e12) ),
introduced(definition,[new_symbols(definition,[spl8_135])],[avatar_definition]) ).
fof(f1177,plain,
( e23 = h4(e12)
| ~ spl8_135 ),
inference(avatar_component_clause,[],[f1176]) ).
fof(f1191,plain,
spl8_135,
inference(avatar_split_clause,[],[f390,f1176]) ).
fof(f1192,plain,
spl8_107,
inference(avatar_split_clause,[],[f386,f1041]) ).
fof(f1193,plain,
spl8_18,
inference(avatar_split_clause,[],[f382,f633]) ).
fof(f1194,plain,
spl8_3,
inference(avatar_split_clause,[],[f378,f561]) ).
fof(f1196,definition,
( spl8_137
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl8_137])],[avatar_definition]) ).
fof(f1200,definition,
( spl8_138
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl8_138])],[avatar_definition]) ).
fof(f1202,plain,
( e21 = op2(e21,e20)
| ~ spl8_138 ),
inference(avatar_component_clause,[],[f1200]) ).
fof(f1204,definition,
( spl8_139
<=> e20 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_139])],[avatar_definition]) ).
fof(f1205,plain,
( e20 = op2(e20,e22)
| ~ spl8_139 ),
inference(avatar_component_clause,[],[f1204]) ).
fof(f1208,definition,
( spl8_140
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_140])],[avatar_definition]) ).
fof(f1210,plain,
( e23 = op2(e23,e20)
| ~ spl8_140 ),
inference(avatar_component_clause,[],[f1208]) ).
fof(f1212,plain,
( spl8_137
| spl8_138
| ~ spl8_139
| spl8_140 ),
inference(avatar_split_clause,[],[f306,f1208,f1204,f1200,f1196]) ).
fof(f1214,definition,
( spl8_141
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl8_141])],[avatar_definition]) ).
fof(f1220,definition,
( spl8_142
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_142])],[avatar_definition]) ).
fof(f1222,plain,
( e22 = op2(e22,e20)
| ~ spl8_142 ),
inference(avatar_component_clause,[],[f1220]) ).
fof(f1240,definition,
( spl8_144
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_144])],[avatar_definition]) ).
fof(f1242,plain,
( e21 = op2(e21,e21)
| ~ spl8_144 ),
inference(avatar_component_clause,[],[f1240]) ).
fof(f1244,definition,
( spl8_145
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl8_145])],[avatar_definition]) ).
fof(f1245,plain,
( e21 = op2(e21,e22)
| ~ spl8_145 ),
inference(avatar_component_clause,[],[f1244]) ).
fof(f1248,definition,
( spl8_146
<=> e23 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl8_146])],[avatar_definition]) ).
fof(f1250,plain,
( e23 = op2(e23,e21)
| ~ spl8_146 ),
inference(avatar_component_clause,[],[f1248]) ).
fof(f1256,definition,
( spl8_147
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl8_147])],[avatar_definition]) ).
fof(f1258,plain,
( e22 = op2(e22,e21)
| ~ spl8_147 ),
inference(avatar_component_clause,[],[f1256]) ).
fof(f1260,plain,
( spl8_141
| spl8_144
| spl8_147
| spl8_146 ),
inference(avatar_split_clause,[],[f326,f1248,f1256,f1240,f1214]) ).
fof(f1262,plain,
( spl8_141
| ~ spl8_144
| spl8_147
| spl8_146 ),
inference(avatar_split_clause,[],[f328,f1248,f1256,f1240,f1214]) ).
fof(f1264,definition,
( spl8_148
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_148])],[avatar_definition]) ).
fof(f1265,plain,
( e21 = op2(e21,e23)
| ~ spl8_148 ),
inference(avatar_component_clause,[],[f1264]) ).
fof(f1276,definition,
( spl8_149
<=> e22 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl8_149])],[avatar_definition]) ).
fof(f1277,plain,
( e22 = op2(e22,e22)
| ~ spl8_149 ),
inference(avatar_component_clause,[],[f1276]) ).
fof(f1278,plain,
( e22 != op2(e22,e22)
| spl8_149 ),
inference(avatar_component_clause,[],[f1276]) ).
fof(f1280,definition,
( spl8_150
<=> e23 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_150])],[avatar_definition]) ).
fof(f1288,plain,
( spl8_139
| spl8_145
| spl8_149
| spl8_150 ),
inference(avatar_split_clause,[],[f342,f1280,f1276,f1244,f1204]) ).
fof(f1292,definition,
( spl8_151
<=> e22 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl8_151])],[avatar_definition]) ).
fof(f1293,plain,
( e22 = op2(e22,e23)
| ~ spl8_151 ),
inference(avatar_component_clause,[],[f1292]) ).
fof(f1304,definition,
( spl8_152
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl8_152])],[avatar_definition]) ).
fof(f1311,plain,
( ~ spl8_140
| spl8_148
| spl8_151
| spl8_152 ),
inference(avatar_split_clause,[],[f357,f1304,f1292,f1264,f1208]) ).
fof(f1324,definition,
( spl8_153
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl8_153])],[avatar_definition]) ).
fof(f1328,definition,
( spl8_154
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_154])],[avatar_definition]) ).
fof(f1330,plain,
( e11 = op1(e11,e10)
| ~ spl8_154 ),
inference(avatar_component_clause,[],[f1328]) ).
fof(f1332,definition,
( spl8_155
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_155])],[avatar_definition]) ).
fof(f1333,plain,
( e10 = op1(e10,e12)
| ~ spl8_155 ),
inference(avatar_component_clause,[],[f1332]) ).
fof(f1336,definition,
( spl8_156
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_156])],[avatar_definition]) ).
fof(f1342,definition,
( spl8_157
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl8_157])],[avatar_definition]) ).
fof(f1348,definition,
( spl8_158
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl8_158])],[avatar_definition]) ).
fof(f1351,plain,
( ~ spl8_153
| spl8_154
| spl8_158
| spl8_156 ),
inference(avatar_split_clause,[],[f245,f1336,f1348,f1328,f1324]) ).
fof(f1352,plain,
( spl8_153
| spl8_154
| spl8_158
| spl8_156 ),
inference(avatar_split_clause,[],[f246,f1336,f1348,f1328,f1324]) ).
fof(f1356,definition,
( spl8_159
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl8_159])],[avatar_definition]) ).
fof(f1368,definition,
( spl8_160
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_160])],[avatar_definition]) ).
fof(f1370,plain,
( e11 = op1(e11,e11)
| ~ spl8_160 ),
inference(avatar_component_clause,[],[f1368]) ).
fof(f1372,definition,
( spl8_161
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl8_161])],[avatar_definition]) ).
fof(f1373,plain,
( e11 = op1(e11,e12)
| ~ spl8_161 ),
inference(avatar_component_clause,[],[f1372]) ).
fof(f1376,definition,
( spl8_162
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_162])],[avatar_definition]) ).
fof(f1378,plain,
( e13 = op1(e13,e11)
| ~ spl8_162 ),
inference(avatar_component_clause,[],[f1376]) ).
fof(f1380,plain,
( spl8_157
| spl8_160
| ~ spl8_161
| spl8_162 ),
inference(avatar_split_clause,[],[f258,f1376,f1372,f1368,f1342]) ).
fof(f1382,plain,
( spl8_157
| ~ spl8_160
| ~ spl8_161
| spl8_162 ),
inference(avatar_split_clause,[],[f260,f1376,f1372,f1368,f1342]) ).
fof(f1384,definition,
( spl8_163
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_163])],[avatar_definition]) ).
fof(f1386,plain,
( e12 = op1(e12,e11)
| ~ spl8_163 ),
inference(avatar_component_clause,[],[f1384]) ).
fof(f1388,plain,
( spl8_157
| spl8_160
| spl8_163
| spl8_162 ),
inference(avatar_split_clause,[],[f262,f1376,f1384,f1368,f1342]) ).
fof(f1390,plain,
( spl8_157
| ~ spl8_160
| spl8_163
| spl8_162 ),
inference(avatar_split_clause,[],[f264,f1376,f1384,f1368,f1342]) ).
fof(f1392,definition,
( spl8_164
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_164])],[avatar_definition]) ).
fof(f1396,plain,
( spl8_157
| spl8_160
| ~ spl8_161
| ~ spl8_164 ),
inference(avatar_split_clause,[],[f266,f1392,f1372,f1368,f1342]) ).
fof(f1398,plain,
( spl8_157
| ~ spl8_160
| ~ spl8_161
| ~ spl8_164 ),
inference(avatar_split_clause,[],[f268,f1392,f1372,f1368,f1342]) ).
fof(f1400,plain,
( spl8_157
| spl8_160
| spl8_163
| ~ spl8_164 ),
inference(avatar_split_clause,[],[f270,f1392,f1384,f1368,f1342]) ).
fof(f1402,plain,
( spl8_157
| ~ spl8_160
| spl8_163
| ~ spl8_164 ),
inference(avatar_split_clause,[],[f272,f1392,f1384,f1368,f1342]) ).
fof(f1404,definition,
( spl8_165
<=> e12 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl8_165])],[avatar_definition]) ).
fof(f1408,definition,
( spl8_166
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_166])],[avatar_definition]) ).
fof(f1412,plain,
( spl8_155
| spl8_161
| ~ spl8_165
| spl8_166 ),
inference(avatar_split_clause,[],[f274,f1408,f1404,f1372,f1332]) ).
fof(f1416,plain,
( spl8_155
| spl8_161
| spl8_165
| spl8_166 ),
inference(avatar_split_clause,[],[f278,f1408,f1404,f1372,f1332]) ).
fof(f1420,definition,
( spl8_167
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl8_167])],[avatar_definition]) ).
fof(f1421,plain,
( e12 = op1(e12,e13)
| ~ spl8_167 ),
inference(avatar_component_clause,[],[f1420]) ).
fof(f1432,definition,
( spl8_168
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_168])],[avatar_definition]) ).
fof(f1440,plain,
( spl8_159
| spl8_164
| spl8_167
| spl8_168 ),
inference(avatar_split_clause,[],[f294,f1432,f1420,f1392,f1356]) ).
fof(f1448,plain,
( spl8_159
| spl8_164
| spl8_167
| ~ spl8_168 ),
inference(avatar_split_clause,[],[f302,f1432,f1420,f1392,f1356]) ).
fof(f1453,definition,
( spl8_169
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl8_169])],[avatar_definition]) ).
fof(f1455,plain,
( e20 = op2(e21,e20)
| ~ spl8_169 ),
inference(avatar_component_clause,[],[f1453]) ).
fof(f1457,definition,
( spl8_170
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_170])],[avatar_definition]) ).
fof(f1459,plain,
( e20 = op2(e22,e20)
| ~ spl8_170 ),
inference(avatar_component_clause,[],[f1457]) ).
fof(f1461,definition,
( spl8_171
<=> e20 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_171])],[avatar_definition]) ).
fof(f1464,plain,
( spl8_137
| spl8_169
| spl8_170
| spl8_171 ),
inference(avatar_split_clause,[],[f86,f1461,f1457,f1453,f1196]) ).
fof(f1470,definition,
( spl8_173
<=> e21 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl8_173])],[avatar_definition]) ).
fof(f1478,definition,
( spl8_175
<=> e21 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl8_175])],[avatar_definition]) ).
fof(f1480,plain,
( e21 = op2(e20,e23)
| ~ spl8_175 ),
inference(avatar_component_clause,[],[f1478]) ).
fof(f1492,definition,
( spl8_178
<=> op2(e20,e20) = e22 ),
introduced(definition,[new_symbols(definition,[spl8_178])],[avatar_definition]) ).
fof(f1494,plain,
( op2(e20,e20) = e22
| ~ spl8_178 ),
inference(avatar_component_clause,[],[f1492]) ).
fof(f1496,definition,
( spl8_179
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl8_179])],[avatar_definition]) ).
fof(f1500,definition,
( spl8_180
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_180])],[avatar_definition]) ).
fof(f1502,plain,
( e22 = op2(e20,e22)
| ~ spl8_180 ),
inference(avatar_component_clause,[],[f1500]) ).
fof(f1509,definition,
( spl8_182
<=> e22 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl8_182])],[avatar_definition]) ).
fof(f1511,plain,
( e22 = op2(e21,e20)
| ~ spl8_182 ),
inference(avatar_component_clause,[],[f1509]) ).
fof(f1513,definition,
( spl8_183
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_183])],[avatar_definition]) ).
fof(f1515,plain,
( e22 = op2(e23,e20)
| ~ spl8_183 ),
inference(avatar_component_clause,[],[f1513]) ).
fof(f1516,plain,
( spl8_178
| spl8_182
| spl8_142
| spl8_183 ),
inference(avatar_split_clause,[],[f90,f1513,f1220,f1509,f1492]) ).
fof(f1518,definition,
( spl8_184
<=> op2(e20,e20) = e23 ),
introduced(definition,[new_symbols(definition,[spl8_184])],[avatar_definition]) ).
fof(f1520,plain,
( op2(e20,e20) = e23
| ~ spl8_184 ),
inference(avatar_component_clause,[],[f1518]) ).
fof(f1535,definition,
( spl8_188
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl8_188])],[avatar_definition]) ).
fof(f1537,plain,
( e23 = op2(e21,e20)
| ~ spl8_188 ),
inference(avatar_component_clause,[],[f1535]) ).
fof(f1539,definition,
( spl8_189
<=> e23 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_189])],[avatar_definition]) ).
fof(f1541,plain,
( e23 = op2(e22,e20)
| ~ spl8_189 ),
inference(avatar_component_clause,[],[f1539]) ).
fof(f1542,plain,
( spl8_184
| spl8_188
| spl8_189
| spl8_140 ),
inference(avatar_split_clause,[],[f92,f1208,f1539,f1535,f1518]) ).
fof(f1544,definition,
( spl8_190
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_190])],[avatar_definition]) ).
fof(f1546,plain,
( e20 = op2(e21,e21)
| ~ spl8_190 ),
inference(avatar_component_clause,[],[f1544]) ).
fof(f1548,definition,
( spl8_191
<=> e20 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl8_191])],[avatar_definition]) ).
fof(f1550,plain,
( e20 = op2(e21,e22)
| ~ spl8_191 ),
inference(avatar_component_clause,[],[f1548]) ).
fof(f1552,definition,
( spl8_192
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_192])],[avatar_definition]) ).
fof(f1555,plain,
( spl8_169
| spl8_190
| spl8_191
| spl8_192 ),
inference(avatar_split_clause,[],[f93,f1552,f1548,f1544,f1453]) ).
fof(f1567,definition,
( spl8_195
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl8_195])],[avatar_definition]) ).
fof(f1569,plain,
( e21 = op2(e22,e21)
| ~ spl8_195 ),
inference(avatar_component_clause,[],[f1567]) ).
fof(f1571,definition,
( spl8_196
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl8_196])],[avatar_definition]) ).
fof(f1574,plain,
( spl8_173
| spl8_144
| spl8_195
| spl8_196 ),
inference(avatar_split_clause,[],[f96,f1571,f1567,f1240,f1470]) ).
fof(f1576,definition,
( spl8_197
<=> e22 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_197])],[avatar_definition]) ).
fof(f1580,definition,
( spl8_198
<=> e22 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl8_198])],[avatar_definition]) ).
fof(f1582,plain,
( e22 = op2(e21,e22)
| ~ spl8_198 ),
inference(avatar_component_clause,[],[f1580]) ).
fof(f1589,definition,
( spl8_200
<=> e22 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl8_200])],[avatar_definition]) ).
fof(f1591,plain,
( e22 = op2(e23,e21)
| ~ spl8_200 ),
inference(avatar_component_clause,[],[f1589]) ).
fof(f1592,plain,
( spl8_179
| spl8_197
| spl8_147
| spl8_200 ),
inference(avatar_split_clause,[],[f98,f1589,f1256,f1576,f1496]) ).
fof(f1594,definition,
( spl8_201
<=> e23 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_201])],[avatar_definition]) ).
fof(f1596,plain,
( e23 = op2(e21,e21)
| ~ spl8_201 ),
inference(avatar_component_clause,[],[f1594]) ).
fof(f1598,definition,
( spl8_202
<=> e23 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl8_202])],[avatar_definition]) ).
fof(f1602,definition,
( spl8_203
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_203])],[avatar_definition]) ).
fof(f1604,plain,
( e23 = op2(e21,e23)
| ~ spl8_203 ),
inference(avatar_component_clause,[],[f1602]) ).
fof(f1605,plain,
( spl8_188
| spl8_201
| spl8_202
| spl8_203 ),
inference(avatar_split_clause,[],[f99,f1602,f1598,f1594,f1535]) ).
fof(f1612,definition,
( spl8_205
<=> e20 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl8_205])],[avatar_definition]) ).
fof(f1614,plain,
( e20 = op2(e22,e22)
| ~ spl8_205 ),
inference(avatar_component_clause,[],[f1612]) ).
fof(f1621,definition,
( spl8_207
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_207])],[avatar_definition]) ).
fof(f1624,plain,
( spl8_139
| spl8_191
| spl8_205
| spl8_207 ),
inference(avatar_split_clause,[],[f102,f1621,f1612,f1548,f1204]) ).
fof(f1635,definition,
( spl8_210
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_210])],[avatar_definition]) ).
fof(f1637,plain,
( e21 = op2(e23,e22)
| ~ spl8_210 ),
inference(avatar_component_clause,[],[f1635]) ).
fof(f1639,plain,
( spl8_142
| spl8_147
| spl8_149
| spl8_151 ),
inference(avatar_split_clause,[],[f105,f1292,f1276,f1256,f1220]) ).
fof(f1641,definition,
( spl8_211
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_211])],[avatar_definition]) ).
fof(f1644,plain,
( spl8_180
| spl8_198
| spl8_149
| spl8_211 ),
inference(avatar_split_clause,[],[f106,f1641,f1276,f1580,f1500]) ).
fof(f1646,definition,
( spl8_212
<=> e23 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl8_212])],[avatar_definition]) ).
fof(f1648,plain,
( e23 = op2(e22,e22)
| ~ spl8_212 ),
inference(avatar_component_clause,[],[f1646]) ).
fof(f1656,definition,
( spl8_214
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl8_214])],[avatar_definition]) ).
fof(f1658,plain,
( e20 = op2(e23,e23)
| ~ spl8_214 ),
inference(avatar_component_clause,[],[f1656]) ).
fof(f1689,plain,
( spl8_207
| spl8_210
| spl8_211
| spl8_150 ),
inference(avatar_split_clause,[],[f83,f1280,f1641,f1635,f1621]) ).
fof(f1693,definition,
( spl8_217
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_217])],[avatar_definition]) ).
fof(f1695,plain,
( e10 = op1(e11,e10)
| ~ spl8_217 ),
inference(avatar_component_clause,[],[f1693]) ).
fof(f1697,definition,
( spl8_218
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl8_218])],[avatar_definition]) ).
fof(f1699,plain,
( e10 = op1(e12,e10)
| ~ spl8_218 ),
inference(avatar_component_clause,[],[f1697]) ).
fof(f1706,definition,
( spl8_220
<=> op1(e10,e10) = e11 ),
introduced(definition,[new_symbols(definition,[spl8_220])],[avatar_definition]) ).
fof(f1710,definition,
( spl8_221
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl8_221])],[avatar_definition]) ).
fof(f1712,plain,
( e11 = op1(e10,e11)
| ~ spl8_221 ),
inference(avatar_component_clause,[],[f1710]) ).
fof(f1714,definition,
( spl8_222
<=> e11 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_222])],[avatar_definition]) ).
fof(f1718,definition,
( spl8_223
<=> e11 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl8_223])],[avatar_definition]) ).
fof(f1720,plain,
( e11 = op1(e10,e13)
| ~ spl8_223 ),
inference(avatar_component_clause,[],[f1718]) ).
fof(f1723,definition,
( spl8_224
<=> e11 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl8_224])],[avatar_definition]) ).
fof(f1725,plain,
( e11 = op1(e12,e10)
| ~ spl8_224 ),
inference(avatar_component_clause,[],[f1723]) ).
fof(f1727,definition,
( spl8_225
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_225])],[avatar_definition]) ).
fof(f1730,plain,
( spl8_220
| spl8_154
| spl8_224
| spl8_225 ),
inference(avatar_split_clause,[],[f40,f1727,f1723,f1328,f1706]) ).
fof(f1732,definition,
( spl8_226
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[spl8_226])],[avatar_definition]) ).
fof(f1734,plain,
( op1(e10,e10) = e12
| ~ spl8_226 ),
inference(avatar_component_clause,[],[f1732]) ).
fof(f1736,definition,
( spl8_227
<=> e12 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl8_227])],[avatar_definition]) ).
fof(f1738,plain,
( e12 = op1(e10,e11)
| ~ spl8_227 ),
inference(avatar_component_clause,[],[f1736]) ).
fof(f1740,definition,
( spl8_228
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_228])],[avatar_definition]) ).
fof(f1742,plain,
( e12 = op1(e10,e12)
| ~ spl8_228 ),
inference(avatar_component_clause,[],[f1740]) ).
fof(f1744,definition,
( spl8_229
<=> e12 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl8_229])],[avatar_definition]) ).
fof(f1747,plain,
( spl8_226
| spl8_227
| spl8_228
| spl8_229 ),
inference(avatar_split_clause,[],[f41,f1744,f1740,f1736,f1732]) ).
fof(f1753,definition,
( spl8_231
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_231])],[avatar_definition]) ).
fof(f1755,plain,
( e12 = op1(e13,e10)
| ~ spl8_231 ),
inference(avatar_component_clause,[],[f1753]) ).
fof(f1758,definition,
( spl8_232
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl8_232])],[avatar_definition]) ).
fof(f1760,plain,
( op1(e10,e10) = e13
| ~ spl8_232 ),
inference(avatar_component_clause,[],[f1758]) ).
fof(f1762,definition,
( spl8_233
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl8_233])],[avatar_definition]) ).
fof(f1764,plain,
( e13 = op1(e10,e11)
| ~ spl8_233 ),
inference(avatar_component_clause,[],[f1762]) ).
fof(f1766,definition,
( spl8_234
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_234])],[avatar_definition]) ).
fof(f1770,definition,
( spl8_235
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl8_235])],[avatar_definition]) ).
fof(f1772,plain,
( e13 = op1(e10,e13)
| ~ spl8_235 ),
inference(avatar_component_clause,[],[f1770]) ).
fof(f1773,plain,
( spl8_232
| spl8_233
| spl8_234
| spl8_235 ),
inference(avatar_split_clause,[],[f43,f1770,f1766,f1762,f1758]) ).
fof(f1775,definition,
( spl8_236
<=> e13 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_236])],[avatar_definition]) ).
fof(f1777,plain,
( e13 = op1(e11,e10)
| ~ spl8_236 ),
inference(avatar_component_clause,[],[f1775]) ).
fof(f1779,definition,
( spl8_237
<=> e13 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl8_237])],[avatar_definition]) ).
fof(f1781,plain,
( e13 = op1(e12,e10)
| ~ spl8_237 ),
inference(avatar_component_clause,[],[f1779]) ).
fof(f1782,plain,
( spl8_232
| spl8_236
| spl8_237
| spl8_156 ),
inference(avatar_split_clause,[],[f44,f1336,f1779,f1775,f1758]) ).
fof(f1784,definition,
( spl8_238
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_238])],[avatar_definition]) ).
fof(f1786,plain,
( e10 = op1(e11,e11)
| ~ spl8_238 ),
inference(avatar_component_clause,[],[f1784]) ).
fof(f1788,definition,
( spl8_239
<=> e10 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl8_239])],[avatar_definition]) ).
fof(f1790,plain,
( e10 = op1(e11,e12)
| ~ spl8_239 ),
inference(avatar_component_clause,[],[f1788]) ).
fof(f1792,definition,
( spl8_240
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_240])],[avatar_definition]) ).
fof(f1794,plain,
( e10 = op1(e11,e13)
| ~ spl8_240 ),
inference(avatar_component_clause,[],[f1792]) ).
fof(f1795,plain,
( spl8_217
| spl8_238
| spl8_239
| spl8_240 ),
inference(avatar_split_clause,[],[f45,f1792,f1788,f1784,f1693]) ).
fof(f1797,definition,
( spl8_241
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_241])],[avatar_definition]) ).
fof(f1799,plain,
( e10 = op1(e12,e11)
| ~ spl8_241 ),
inference(avatar_component_clause,[],[f1797]) ).
fof(f1801,definition,
( spl8_242
<=> e10 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_242])],[avatar_definition]) ).
fof(f1803,plain,
( e10 = op1(e13,e11)
| ~ spl8_242 ),
inference(avatar_component_clause,[],[f1801]) ).
fof(f1804,plain,
( spl8_157
| spl8_238
| spl8_241
| spl8_242 ),
inference(avatar_split_clause,[],[f46,f1801,f1797,f1784,f1342]) ).
fof(f1805,plain,
( spl8_154
| spl8_160
| spl8_161
| spl8_164 ),
inference(avatar_split_clause,[],[f47,f1392,f1372,f1368,f1328]) ).
fof(f1807,definition,
( spl8_243
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_243])],[avatar_definition]) ).
fof(f1809,plain,
( e11 = op1(e12,e11)
| ~ spl8_243 ),
inference(avatar_component_clause,[],[f1807]) ).
fof(f1811,definition,
( spl8_244
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_244])],[avatar_definition]) ).
fof(f1814,plain,
( spl8_221
| spl8_160
| spl8_243
| spl8_244 ),
inference(avatar_split_clause,[],[f48,f1811,f1807,f1368,f1710]) ).
fof(f1820,definition,
( spl8_246
<=> e12 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl8_246])],[avatar_definition]) ).
fof(f1822,plain,
( e12 = op1(e11,e12)
| ~ spl8_246 ),
inference(avatar_component_clause,[],[f1820]) ).
fof(f1829,definition,
( spl8_248
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_248])],[avatar_definition]) ).
fof(f1831,plain,
( e12 = op1(e13,e11)
| ~ spl8_248 ),
inference(avatar_component_clause,[],[f1829]) ).
fof(f1834,definition,
( spl8_249
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_249])],[avatar_definition]) ).
fof(f1836,plain,
( e13 = op1(e11,e11)
| ~ spl8_249 ),
inference(avatar_component_clause,[],[f1834]) ).
fof(f1838,definition,
( spl8_250
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl8_250])],[avatar_definition]) ).
fof(f1842,definition,
( spl8_251
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_251])],[avatar_definition]) ).
fof(f1844,plain,
( e13 = op1(e11,e13)
| ~ spl8_251 ),
inference(avatar_component_clause,[],[f1842]) ).
fof(f1845,plain,
( spl8_236
| spl8_249
| spl8_250
| spl8_251 ),
inference(avatar_split_clause,[],[f51,f1842,f1838,f1834,f1775]) ).
fof(f1852,definition,
( spl8_253
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl8_253])],[avatar_definition]) ).
fof(f1854,plain,
( e10 = op1(e12,e12)
| ~ spl8_253 ),
inference(avatar_component_clause,[],[f1852]) ).
fof(f1856,definition,
( spl8_254
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl8_254])],[avatar_definition]) ).
fof(f1859,plain,
( spl8_218
| spl8_241
| spl8_253
| spl8_254 ),
inference(avatar_split_clause,[],[f53,f1856,f1852,f1797,f1697]) ).
fof(f1861,definition,
( spl8_255
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_255])],[avatar_definition]) ).
fof(f1864,plain,
( spl8_155
| spl8_239
| spl8_253
| spl8_255 ),
inference(avatar_split_clause,[],[f54,f1861,f1852,f1788,f1332]) ).
fof(f1866,definition,
( spl8_256
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl8_256])],[avatar_definition]) ).
fof(f1868,plain,
( e11 = op1(e12,e12)
| ~ spl8_256 ),
inference(avatar_component_clause,[],[f1866]) ).
fof(f1870,definition,
( spl8_257
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl8_257])],[avatar_definition]) ).
fof(f1872,plain,
( e11 = op1(e12,e13)
| ~ spl8_257 ),
inference(avatar_component_clause,[],[f1870]) ).
fof(f1873,plain,
( spl8_224
| spl8_243
| spl8_256
| spl8_257 ),
inference(avatar_split_clause,[],[f55,f1870,f1866,f1807,f1723]) ).
fof(f1875,definition,
( spl8_258
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_258])],[avatar_definition]) ).
fof(f1877,plain,
( e11 = op1(e13,e12)
| ~ spl8_258 ),
inference(avatar_component_clause,[],[f1875]) ).
fof(f1878,plain,
( spl8_222
| spl8_161
| spl8_256
| spl8_258 ),
inference(avatar_split_clause,[],[f56,f1875,f1866,f1372,f1714]) ).
fof(f1881,definition,
( spl8_259
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_259])],[avatar_definition]) ).
fof(f1883,plain,
( e12 = op1(e13,e12)
| ~ spl8_259 ),
inference(avatar_component_clause,[],[f1881]) ).
fof(f1884,plain,
( spl8_228
| spl8_246
| spl8_165
| spl8_259 ),
inference(avatar_split_clause,[],[f58,f1881,f1404,f1820,f1740]) ).
fof(f1886,definition,
( spl8_260
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl8_260])],[avatar_definition]) ).
fof(f1888,plain,
( e13 = op1(e12,e12)
| ~ spl8_260 ),
inference(avatar_component_clause,[],[f1886]) ).
fof(f1890,definition,
( spl8_261
<=> e13 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl8_261])],[avatar_definition]) ).
fof(f1896,definition,
( spl8_262
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_262])],[avatar_definition]) ).
fof(f1898,plain,
( e10 = op1(e13,e13)
| ~ spl8_262 ),
inference(avatar_component_clause,[],[f1896]) ).
fof(f1908,definition,
( spl8_264
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_264])],[avatar_definition]) ).
fof(f1910,plain,
( e12 = op1(e13,e13)
| ~ spl8_264 ),
inference(avatar_component_clause,[],[f1908]) ).
fof(f1911,plain,
( spl8_231
| spl8_248
| spl8_259
| spl8_264 ),
inference(avatar_split_clause,[],[f65,f1908,f1881,f1829,f1753]) ).
fof(f1914,plain,
( spl8_235
| spl8_251
| spl8_261
| spl8_168 ),
inference(avatar_split_clause,[],[f68,f1432,f1890,f1842,f1770]) ).
fof(f1931,plain,
( e20 != e21
| ~ spl8_3
| spl8_8 ),
inference(forward_demodulation,[],[f587,f562]) ).
fof(f1934,plain,
( h2(op1(e12,e11)) != op2(e21,h2(e11))
| ~ spl8_18
| spl8_74 ),
inference(forward_demodulation,[],[f894,f634]) ).
fof(f1935,plain,
spl8_260,
inference(avatar_split_clause,[],[f369,f1886]) ).
fof(f1936,plain,
spl8_212,
inference(avatar_split_clause,[],[f372,f1646]) ).
fof(f1945,plain,
( e20 = e21
| ~ spl8_3
| ~ spl8_8 ),
inference(forward_demodulation,[],[f586,f562]) ).
fof(f1992,plain,
( e21 = e23
| ~ spl8_38
| ~ spl8_135 ),
inference(forward_demodulation,[],[f730,f1177]) ).
fof(f1998,plain,
( e23 = op2(e23,e20)
| ~ spl8_38
| ~ spl8_135
| ~ spl8_138 ),
inference(superposition,[],[f1202,f1992]) ).
fof(f2017,plain,
( e21 != e23
| spl8_38
| ~ spl8_135 ),
inference(forward_demodulation,[],[f731,f1177]) ).
fof(f2018,plain,
( e20 = e21
| ~ spl8_138
| ~ spl8_169 ),
inference(superposition,[],[f1455,f1202]) ).
fof(f2022,plain,
( $false
| ~ spl8_3
| spl8_8
| ~ spl8_138
| ~ spl8_169 ),
inference(forward_subsumption_resolution,[],[f2018,f1931]) ).
fof(f2023,plain,
( ~ spl8_3
| spl8_8
| ~ spl8_138
| ~ spl8_169 ),
inference(avatar_contradiction_clause,[],[f2022]) ).
fof(f2042,plain,
( e21 = e22
| ~ spl8_138
| ~ spl8_182 ),
inference(superposition,[],[f1511,f1202]) ).
fof(f2047,plain,
( $false
| ~ spl8_138
| ~ spl8_182 ),
inference(forward_subsumption_resolution,[],[f2042,f221]) ).
fof(f2048,plain,
( ~ spl8_138
| ~ spl8_182 ),
inference(avatar_contradiction_clause,[],[f2047]) ).
fof(f2058,plain,
( e21 = e22
| ~ spl8_147
| ~ spl8_195 ),
inference(forward_demodulation,[],[f1569,f1258]) ).
fof(f2060,plain,
( $false
| ~ spl8_147
| ~ spl8_195 ),
inference(forward_subsumption_resolution,[],[f2058,f221]) ).
fof(f2061,plain,
( ~ spl8_147
| ~ spl8_195 ),
inference(avatar_contradiction_clause,[],[f2060]) ).
fof(f2068,plain,
( e22 = e23
| ~ spl8_178
| ~ spl8_184 ),
inference(forward_demodulation,[],[f1520,f1494]) ).
fof(f2069,plain,
( $false
| ~ spl8_178
| ~ spl8_184 ),
inference(forward_subsumption_resolution,[],[f2068,f219]) ).
fof(f2070,plain,
( ~ spl8_178
| ~ spl8_184 ),
inference(avatar_contradiction_clause,[],[f2069]) ).
fof(f2088,plain,
( e20 = e22
| ~ spl8_23
| ~ spl8_107 ),
inference(forward_demodulation,[],[f658,f1042]) ).
fof(f2130,plain,
( e20 != e22
| spl8_23
| ~ spl8_107 ),
inference(forward_demodulation,[],[f659,f1042]) ).
fof(f2136,plain,
( e21 = e23
| ~ spl8_138
| ~ spl8_188 ),
inference(superposition,[],[f1537,f1202]) ).
fof(f2142,plain,
( $false
| spl8_38
| ~ spl8_135
| ~ spl8_138
| ~ spl8_188 ),
inference(forward_subsumption_resolution,[],[f2136,f2017]) ).
fof(f2143,plain,
( spl8_38
| ~ spl8_135
| ~ spl8_138
| ~ spl8_188 ),
inference(avatar_contradiction_clause,[],[f2142]) ).
fof(f2146,plain,
( e20 = e23
| ~ spl8_170
| ~ spl8_189 ),
inference(superposition,[],[f1459,f1541]) ).
fof(f2148,plain,
( $false
| ~ spl8_170
| ~ spl8_189 ),
inference(forward_subsumption_resolution,[],[f2146,f222]) ).
fof(f2149,plain,
( ~ spl8_170
| ~ spl8_189 ),
inference(avatar_contradiction_clause,[],[f2148]) ).
fof(f2160,plain,
( e20 = e21
| ~ spl8_144
| ~ spl8_190 ),
inference(superposition,[],[f1546,f1242]) ).
fof(f2164,plain,
( $false
| ~ spl8_3
| spl8_8
| ~ spl8_144
| ~ spl8_190 ),
inference(forward_subsumption_resolution,[],[f2160,f1931]) ).
fof(f2165,plain,
( ~ spl8_3
| spl8_8
| ~ spl8_144
| ~ spl8_190 ),
inference(avatar_contradiction_clause,[],[f2164]) ).
fof(f2181,plain,
( e20 = e22
| ~ spl8_191
| ~ spl8_198 ),
inference(superposition,[],[f1582,f1550]) ).
fof(f2186,plain,
( $false
| spl8_23
| ~ spl8_107
| ~ spl8_191
| ~ spl8_198 ),
inference(forward_subsumption_resolution,[],[f2181,f2130]) ).
fof(f2187,plain,
( spl8_23
| ~ spl8_107
| ~ spl8_191
| ~ spl8_198 ),
inference(avatar_contradiction_clause,[],[f2186]) ).
fof(f2363,plain,
( e20 = e22
| ~ spl8_139
| ~ spl8_180 ),
inference(superposition,[],[f1502,f1205]) ).
fof(f2368,plain,
( $false
| spl8_23
| ~ spl8_107
| ~ spl8_139
| ~ spl8_180 ),
inference(forward_subsumption_resolution,[],[f2363,f2130]) ).
fof(f2369,plain,
( spl8_23
| ~ spl8_107
| ~ spl8_139
| ~ spl8_180 ),
inference(avatar_contradiction_clause,[],[f2368]) ).
fof(f2382,plain,
( e22 = e23
| ~ spl8_146
| ~ spl8_200 ),
inference(superposition,[],[f1591,f1250]) ).
fof(f2386,plain,
( $false
| ~ spl8_146
| ~ spl8_200 ),
inference(forward_subsumption_resolution,[],[f2382,f219]) ).
fof(f2387,plain,
( ~ spl8_146
| ~ spl8_200 ),
inference(avatar_contradiction_clause,[],[f2386]) ).
fof(f2414,plain,
( e22 = e23
| ~ spl8_149
| ~ spl8_212 ),
inference(superposition,[],[f1277,f1648]) ).
fof(f2419,plain,
( $false
| ~ spl8_149
| ~ spl8_212 ),
inference(forward_subsumption_resolution,[],[f2414,f219]) ).
fof(f2420,plain,
( ~ spl8_149
| ~ spl8_212 ),
inference(avatar_contradiction_clause,[],[f2419]) ).
fof(f2459,plain,
( e20 = e22
| ~ spl8_142
| ~ spl8_170 ),
inference(forward_demodulation,[],[f1459,f1222]) ).
fof(f2460,plain,
( $false
| spl8_23
| ~ spl8_107
| ~ spl8_142
| ~ spl8_170 ),
inference(forward_subsumption_resolution,[],[f2459,f2130]) ).
fof(f2461,plain,
( spl8_23
| ~ spl8_107
| ~ spl8_142
| ~ spl8_170 ),
inference(avatar_contradiction_clause,[],[f2460]) ).
fof(f2483,plain,
( e20 = e21
| ~ spl8_145
| ~ spl8_191 ),
inference(superposition,[],[f1550,f1245]) ).
fof(f2488,plain,
( $false
| ~ spl8_3
| spl8_8
| ~ spl8_145
| ~ spl8_191 ),
inference(forward_subsumption_resolution,[],[f2483,f1931]) ).
fof(f2489,plain,
( ~ spl8_3
| spl8_8
| ~ spl8_145
| ~ spl8_191 ),
inference(avatar_contradiction_clause,[],[f2488]) ).
fof(f2495,plain,
( e20 = e23
| ~ spl8_205
| ~ spl8_212 ),
inference(forward_demodulation,[],[f1614,f1648]) ).
fof(f2498,plain,
( $false
| ~ spl8_205
| ~ spl8_212 ),
inference(forward_subsumption_resolution,[],[f2495,f222]) ).
fof(f2499,plain,
( ~ spl8_205
| ~ spl8_212 ),
inference(avatar_contradiction_clause,[],[f2498]) ).
fof(f2533,plain,
( e22 = op2(e22,e22)
| ~ spl8_23
| ~ spl8_107
| ~ spl8_139 ),
inference(superposition,[],[f1205,f2088]) ).
fof(f2572,plain,
( $false
| ~ spl8_23
| ~ spl8_107
| ~ spl8_139
| spl8_149 ),
inference(forward_subsumption_resolution,[],[f2533,f1278]) ).
fof(f2573,plain,
( ~ spl8_23
| ~ spl8_107
| ~ spl8_139
| spl8_149 ),
inference(avatar_contradiction_clause,[],[f2572]) ).
fof(f2690,plain,
( e10 = e11
| ~ spl8_218
| ~ spl8_224 ),
inference(forward_demodulation,[],[f1725,f1699]) ).
fof(f2691,plain,
( $false
| ~ spl8_218
| ~ spl8_224 ),
inference(forward_subsumption_resolution,[],[f2690,f218]) ).
fof(f2692,plain,
( ~ spl8_218
| ~ spl8_224 ),
inference(avatar_contradiction_clause,[],[f2691]) ).
fof(f2721,plain,
( e12 = e13
| ~ spl8_226
| ~ spl8_232 ),
inference(forward_demodulation,[],[f1760,f1734]) ).
fof(f2722,plain,
( $false
| ~ spl8_226
| ~ spl8_232 ),
inference(forward_subsumption_resolution,[],[f2721,f213]) ).
fof(f2723,plain,
( ~ spl8_226
| ~ spl8_232 ),
inference(avatar_contradiction_clause,[],[f2722]) ).
fof(f2724,plain,
( e10 = e11
| ~ spl8_154
| ~ spl8_217 ),
inference(superposition,[],[f1695,f1330]) ).
fof(f2729,plain,
( $false
| ~ spl8_154
| ~ spl8_217 ),
inference(forward_subsumption_resolution,[],[f2724,f218]) ).
fof(f2730,plain,
( ~ spl8_154
| ~ spl8_217 ),
inference(avatar_contradiction_clause,[],[f2729]) ).
fof(f2741,plain,
( e11 = e12
| ~ spl8_221
| ~ spl8_227 ),
inference(superposition,[],[f1738,f1712]) ).
fof(f2746,plain,
( $false
| ~ spl8_221
| ~ spl8_227 ),
inference(forward_subsumption_resolution,[],[f2741,f215]) ).
fof(f2747,plain,
( ~ spl8_221
| ~ spl8_227 ),
inference(avatar_contradiction_clause,[],[f2746]) ).
fof(f2754,plain,
( e11 = e13
| ~ spl8_154
| ~ spl8_236 ),
inference(forward_demodulation,[],[f1777,f1330]) ).
fof(f2755,plain,
( $false
| ~ spl8_154
| ~ spl8_236 ),
inference(forward_subsumption_resolution,[],[f2754,f214]) ).
fof(f2756,plain,
( ~ spl8_154
| ~ spl8_236 ),
inference(avatar_contradiction_clause,[],[f2755]) ).
fof(f2758,plain,
( e11 = e13
| ~ spl8_160
| ~ spl8_249 ),
inference(forward_demodulation,[],[f1836,f1370]) ).
fof(f2759,plain,
( $false
| ~ spl8_160
| ~ spl8_249 ),
inference(forward_subsumption_resolution,[],[f2758,f214]) ).
fof(f2760,plain,
( ~ spl8_160
| ~ spl8_249 ),
inference(avatar_contradiction_clause,[],[f2759]) ).
fof(f2762,plain,
( e10 = e13
| ~ spl8_218
| ~ spl8_237 ),
inference(forward_demodulation,[],[f1781,f1699]) ).
fof(f2763,plain,
( $false
| ~ spl8_218
| ~ spl8_237 ),
inference(forward_subsumption_resolution,[],[f2762,f216]) ).
fof(f2764,plain,
( ~ spl8_218
| ~ spl8_237 ),
inference(avatar_contradiction_clause,[],[f2763]) ).
fof(f2766,plain,
( e10 = e11
| ~ spl8_160
| ~ spl8_238 ),
inference(superposition,[],[f1786,f1370]) ).
fof(f2770,plain,
( $false
| ~ spl8_160
| ~ spl8_238 ),
inference(forward_subsumption_resolution,[],[f2766,f218]) ).
fof(f2771,plain,
( ~ spl8_160
| ~ spl8_238 ),
inference(avatar_contradiction_clause,[],[f2770]) ).
fof(f2774,plain,
( e10 = e13
| ~ spl8_162
| ~ spl8_242 ),
inference(superposition,[],[f1803,f1378]) ).
fof(f2775,plain,
( e10 = e13
| ~ spl8_162
| ~ spl8_242 ),
inference(superposition,[],[f1378,f1803]) ).
fof(f2776,plain,
( $false
| ~ spl8_162
| ~ spl8_242 ),
inference(forward_subsumption_resolution,[],[f2775,f216]) ).
fof(f2777,plain,
( ~ spl8_162
| ~ spl8_242 ),
inference(avatar_contradiction_clause,[],[f2776]) ).
fof(f2778,plain,
( $false
| ~ spl8_162
| ~ spl8_242 ),
inference(forward_subsumption_resolution,[],[f2774,f216]) ).
fof(f2779,plain,
( ~ spl8_162
| ~ spl8_242 ),
inference(avatar_contradiction_clause,[],[f2778]) ).
fof(f2780,plain,
( e10 = e12
| ~ spl8_163
| ~ spl8_241 ),
inference(forward_demodulation,[],[f1799,f1386]) ).
fof(f2781,plain,
( $false
| ~ spl8_163
| ~ spl8_241 ),
inference(forward_subsumption_resolution,[],[f2780,f217]) ).
fof(f2782,plain,
( ~ spl8_163
| ~ spl8_241 ),
inference(avatar_contradiction_clause,[],[f2781]) ).
fof(f2804,plain,
( e10 = e12
| ~ spl8_239
| ~ spl8_246 ),
inference(superposition,[],[f1822,f1790]) ).
fof(f2809,plain,
( $false
| ~ spl8_239
| ~ spl8_246 ),
inference(forward_subsumption_resolution,[],[f2804,f217]) ).
fof(f2810,plain,
( ~ spl8_239
| ~ spl8_246 ),
inference(avatar_contradiction_clause,[],[f2809]) ).
fof(f2865,plain,
( e10 = e13
| ~ spl8_240
| ~ spl8_251 ),
inference(forward_demodulation,[],[f1844,f1794]) ).
fof(f2866,plain,
( $false
| ~ spl8_240
| ~ spl8_251 ),
inference(forward_subsumption_resolution,[],[f2865,f216]) ).
fof(f2867,plain,
( ~ spl8_240
| ~ spl8_251 ),
inference(avatar_contradiction_clause,[],[f2866]) ).
fof(f2869,plain,
( e11 = e13
| ~ spl8_221
| ~ spl8_233 ),
inference(superposition,[],[f1712,f1764]) ).
fof(f2875,plain,
( $false
| ~ spl8_221
| ~ spl8_233 ),
inference(forward_subsumption_resolution,[],[f2869,f214]) ).
fof(f2876,plain,
( ~ spl8_221
| ~ spl8_233 ),
inference(avatar_contradiction_clause,[],[f2875]) ).
fof(f2977,plain,
( e11 = e12
| ~ spl8_167
| ~ spl8_257 ),
inference(forward_demodulation,[],[f1872,f1421]) ).
fof(f2978,plain,
( $false
| ~ spl8_167
| ~ spl8_257 ),
inference(forward_subsumption_resolution,[],[f2977,f215]) ).
fof(f2979,plain,
( ~ spl8_167
| ~ spl8_257 ),
inference(avatar_contradiction_clause,[],[f2978]) ).
fof(f2984,plain,
( e10 = e11
| ~ spl8_241
| ~ spl8_243 ),
inference(forward_demodulation,[],[f1809,f1799]) ).
fof(f2985,plain,
( $false
| ~ spl8_241
| ~ spl8_243 ),
inference(forward_subsumption_resolution,[],[f2984,f218]) ).
fof(f2986,plain,
( ~ spl8_241
| ~ spl8_243 ),
inference(avatar_contradiction_clause,[],[f2985]) ).
fof(f2989,plain,
( e12 = e13
| ~ spl8_162
| ~ spl8_248 ),
inference(superposition,[],[f1831,f1378]) ).
fof(f2995,plain,
( $false
| ~ spl8_162
| ~ spl8_248 ),
inference(forward_subsumption_resolution,[],[f2989,f213]) ).
fof(f2996,plain,
( ~ spl8_162
| ~ spl8_248 ),
inference(avatar_contradiction_clause,[],[f2995]) ).
fof(f3014,plain,
( e11 = e12
| ~ spl8_258
| ~ spl8_259 ),
inference(superposition,[],[f1883,f1877]) ).
fof(f3020,plain,
( $false
| ~ spl8_258
| ~ spl8_259 ),
inference(forward_subsumption_resolution,[],[f3014,f215]) ).
fof(f3021,plain,
( ~ spl8_258
| ~ spl8_259 ),
inference(avatar_contradiction_clause,[],[f3020]) ).
fof(f3022,plain,
( e10 = e12
| ~ spl8_155
| ~ spl8_228 ),
inference(superposition,[],[f1742,f1333]) ).
fof(f3027,plain,
( $false
| ~ spl8_155
| ~ spl8_228 ),
inference(forward_subsumption_resolution,[],[f3022,f217]) ).
fof(f3028,plain,
( ~ spl8_155
| ~ spl8_228 ),
inference(avatar_contradiction_clause,[],[f3027]) ).
fof(f3033,plain,
( e11 = e13
| ~ spl8_256
| ~ spl8_260 ),
inference(forward_demodulation,[],[f1888,f1868]) ).
fof(f3034,plain,
( $false
| ~ spl8_256
| ~ spl8_260 ),
inference(forward_subsumption_resolution,[],[f3033,f214]) ).
fof(f3035,plain,
( ~ spl8_256
| ~ spl8_260 ),
inference(avatar_contradiction_clause,[],[f3034]) ).
fof(f3065,plain,
( e11 = e13
| ~ spl8_223
| ~ spl8_235 ),
inference(superposition,[],[f1720,f1772]) ).
fof(f3071,plain,
( $false
| ~ spl8_223
| ~ spl8_235 ),
inference(forward_subsumption_resolution,[],[f3065,f214]) ).
fof(f3072,plain,
( ~ spl8_223
| ~ spl8_235 ),
inference(avatar_contradiction_clause,[],[f3071]) ).
fof(f3093,plain,
( e10 = e11
| ~ spl8_161
| ~ spl8_239 ),
inference(superposition,[],[f1790,f1373]) ).
fof(f3098,plain,
( $false
| ~ spl8_161
| ~ spl8_239 ),
inference(forward_subsumption_resolution,[],[f3093,f218]) ).
fof(f3099,plain,
( ~ spl8_161
| ~ spl8_239 ),
inference(avatar_contradiction_clause,[],[f3098]) ).
fof(f3103,plain,
( h2(e11) != op2(e21,h2(e11))
| ~ spl8_18
| spl8_74
| ~ spl8_243 ),
inference(superposition,[],[f1934,f1809]) ).
fof(f3145,plain,
( e10 = e13
| ~ spl8_253
| ~ spl8_260 ),
inference(forward_demodulation,[],[f1888,f1854]) ).
fof(f3146,plain,
( $false
| ~ spl8_253
| ~ spl8_260 ),
inference(forward_subsumption_resolution,[],[f3145,f216]) ).
fof(f3147,plain,
( ~ spl8_253
| ~ spl8_260 ),
inference(avatar_contradiction_clause,[],[f3146]) ).
fof(f3154,plain,
( e10 = e12
| ~ spl8_262
| ~ spl8_264 ),
inference(superposition,[],[f1910,f1898]) ).
fof(f3158,plain,
( $false
| ~ spl8_262
| ~ spl8_264 ),
inference(forward_subsumption_resolution,[],[f3154,f217]) ).
fof(f3159,plain,
( ~ spl8_262
| ~ spl8_264 ),
inference(avatar_contradiction_clause,[],[f3158]) ).
fof(f3172,plain,
( e10 != op1(e13,e12)
| ~ spl8_262 ),
inference(forward_demodulation,[],[f117,f1898]) ).
fof(f3174,plain,
( e11 != op1(e13,e11)
| ~ spl8_258 ),
inference(forward_demodulation,[],[f119,f1877]) ).
fof(f3176,plain,
( e11 != op1(e13,e10)
| ~ spl8_258 ),
inference(forward_demodulation,[],[f121,f1877]) ).
fof(f3177,plain,
( e13 != op1(e13,e10)
| ~ spl8_162 ),
inference(forward_demodulation,[],[f122,f1378]) ).
fof(f3178,plain,
( e12 != op1(e12,e12)
| ~ spl8_167 ),
inference(forward_demodulation,[],[f123,f1421]) ).
fof(f3179,plain,
( ~ spl8_165
| ~ spl8_167 ),
inference(avatar_split_clause,[],[f3178,f1420,f1404]) ).
fof(f3181,plain,
( e12 != op1(e12,e11)
| ~ spl8_167 ),
inference(forward_demodulation,[],[f124,f1421]) ).
fof(f3184,plain,
( e12 != op1(e12,e10)
| ~ spl8_167 ),
inference(forward_demodulation,[],[f126,f1421]) ).
fof(f3197,plain,
( e11 != op1(e10,e12)
| ~ spl8_223 ),
inference(forward_demodulation,[],[f135,f1720]) ).
fof(f3200,plain,
( e10 != op1(e10,e11)
| ~ spl8_155 ),
inference(forward_demodulation,[],[f137,f1333]) ).
fof(f3201,plain,
( op1(e10,e10) != e11
| ~ spl8_223 ),
inference(forward_demodulation,[],[f138,f1720]) ).
fof(f3204,plain,
( e10 != op1(e12,e13)
| ~ spl8_262 ),
inference(forward_demodulation,[],[f141,f1898]) ).
fof(f3208,plain,
( e10 != op1(e10,e13)
| ~ spl8_262 ),
inference(forward_demodulation,[],[f144,f1898]) ).
fof(f3209,plain,
( e12 != op1(e10,e13)
| ~ spl8_167 ),
inference(forward_demodulation,[],[f145,f1421]) ).
fof(f3215,plain,
( e13 != op1(e11,e12)
| ~ spl8_260 ),
inference(forward_demodulation,[],[f149,f1888]) ).
fof(f3219,plain,
( e13 != op1(e10,e12)
| ~ spl8_260 ),
inference(forward_demodulation,[],[f151,f1888]) ).
fof(f3239,plain,
( e21 != op2(e23,e21)
| ~ spl8_210 ),
inference(forward_demodulation,[],[f167,f1637]) ).
fof(f3257,plain,
( e22 != op2(e21,e21)
| ~ spl8_198 ),
inference(forward_demodulation,[],[f179,f1582]) ).
fof(f3263,plain,
( e20 != op2(e20,e21)
| ~ spl8_139 ),
inference(forward_demodulation,[],[f185,f1205]) ).
fof(f3265,plain,
( e20 != op2(e20,e20)
| ~ spl8_139 ),
inference(forward_demodulation,[],[f187,f1205]) ).
fof(f3273,plain,
( e21 != op2(e20,e23)
| ~ spl8_148 ),
inference(forward_demodulation,[],[f194,f1265]) ).
fof(f3277,plain,
( e23 != op2(e21,e22)
| ~ spl8_212 ),
inference(forward_demodulation,[],[f197,f1648]) ).
fof(f3295,plain,
( e10 = op1(e13,e13)
| ~ spl8_260 ),
inference(forward_demodulation,[],[f371,f1888]) ).
fof(f3296,plain,
( e20 = op2(e23,e23)
| ~ spl8_212 ),
inference(forward_demodulation,[],[f374,f1648]) ).
fof(f3306,plain,
( e20 = e23
| ~ spl8_190
| ~ spl8_201 ),
inference(forward_demodulation,[],[f1546,f1596]) ).
fof(f3309,plain,
( e23 != op2(e23,e23)
| ~ spl8_140 ),
inference(forward_demodulation,[],[f168,f1210]) ).
fof(f3313,plain,
( spl8_214
| ~ spl8_212 ),
inference(avatar_split_clause,[],[f3296,f1646,f1656]) ).
fof(f3314,plain,
( ~ spl8_196
| ~ spl8_210 ),
inference(avatar_split_clause,[],[f3239,f1635,f1571]) ).
fof(f3315,plain,
( e23 != op2(e23,e21)
| ~ spl8_140 ),
inference(forward_demodulation,[],[f170,f1210]) ).
fof(f3319,plain,
( $false
| ~ spl8_190
| ~ spl8_201 ),
inference(forward_subsumption_resolution,[],[f3306,f222]) ).
fof(f3320,plain,
( ~ spl8_190
| ~ spl8_201 ),
inference(avatar_contradiction_clause,[],[f3319]) ).
fof(f3332,plain,
( e23 != op2(e23,e22)
| ~ spl8_212 ),
inference(forward_demodulation,[],[f195,f1648]) ).
fof(f3334,plain,
( e22 != op2(e22,e23)
| ~ spl8_147 ),
inference(forward_demodulation,[],[f172,f1258]) ).
fof(f3341,plain,
( ~ spl8_150
| ~ spl8_212 ),
inference(avatar_split_clause,[],[f3332,f1646,f1280]) ).
fof(f3347,plain,
( ~ spl8_137
| ~ spl8_139 ),
inference(avatar_split_clause,[],[f3265,f1204,f1196]) ).
fof(f3349,plain,
( ~ spl8_152
| ~ spl8_140 ),
inference(avatar_split_clause,[],[f3309,f1208,f1304]) ).
fof(f3350,plain,
( ~ spl8_146
| ~ spl8_140 ),
inference(avatar_split_clause,[],[f3315,f1208,f1248]) ).
fof(f3351,plain,
( ~ spl8_202
| ~ spl8_212 ),
inference(avatar_split_clause,[],[f3277,f1646,f1598]) ).
fof(f3406,plain,
( e20 = h2(e13)
| ~ spl8_190 ),
inference(forward_demodulation,[],[f379,f1546]) ).
fof(f3407,plain,
( spl8_12
| ~ spl8_190 ),
inference(avatar_split_clause,[],[f3406,f1544,f604]) ).
fof(f3413,plain,
( e20 != op2(e23,e22)
| ~ spl8_214 ),
inference(forward_demodulation,[],[f165,f1658]) ).
fof(f3418,plain,
( e20 != op2(e23,e20)
| ~ spl8_214 ),
inference(forward_demodulation,[],[f168,f1658]) ).
fof(f3434,plain,
( e21 != op2(e20,e21)
| ~ spl8_175 ),
inference(forward_demodulation,[],[f184,f1480]) ).
fof(f3442,plain,
( e20 != op2(e21,e23)
| ~ spl8_214 ),
inference(forward_demodulation,[],[f190,f1658]) ).
fof(f3473,plain,
( op2(e20,e20) = h2(e10)
| ~ spl8_190 ),
inference(forward_demodulation,[],[f381,f1546]) ).
fof(f3474,plain,
( e23 = h2(e10)
| ~ spl8_184
| ~ spl8_190 ),
inference(forward_demodulation,[],[f3473,f1520]) ).
fof(f3475,plain,
( spl8_82
| ~ spl8_184
| ~ spl8_190 ),
inference(avatar_split_clause,[],[f3474,f1544,f1518,f924]) ).
fof(f3507,plain,
( e11 = op1(op1(e13,e13),e13)
| ~ spl8_260 ),
inference(forward_demodulation,[],[f370,f1888]) ).
fof(f3508,plain,
( e11 = op1(e10,e13)
| ~ spl8_260
| ~ spl8_262 ),
inference(forward_demodulation,[],[f3507,f1898]) ).
fof(f3509,plain,
( e21 = op2(op2(e23,e23),e23)
| ~ spl8_212 ),
inference(forward_demodulation,[],[f373,f1648]) ).
fof(f3510,plain,
( e21 = op2(e20,e23)
| ~ spl8_212
| ~ spl8_214 ),
inference(forward_demodulation,[],[f3509,f1658]) ).
fof(f3522,plain,
( h2(e11) = op2(op2(e20,e20),e20)
| ~ spl8_190 ),
inference(forward_demodulation,[],[f380,f1546]) ).
fof(f3523,plain,
( op2(e23,e20) = h2(e11)
| ~ spl8_184
| ~ spl8_190 ),
inference(forward_demodulation,[],[f3522,f1520]) ).
fof(f3524,plain,
( e22 = h2(e11)
| ~ spl8_183
| ~ spl8_184
| ~ spl8_190 ),
inference(forward_demodulation,[],[f3523,f1515]) ).
fof(f3525,plain,
( spl8_84
| ~ spl8_183
| ~ spl8_184
| ~ spl8_190 ),
inference(avatar_split_clause,[],[f3524,f1544,f1518,f1513,f934]) ).
fof(f3526,plain,
( e22 != op2(e21,e22)
| ~ spl8_18
| spl8_74
| ~ spl8_84
| ~ spl8_243 ),
inference(superposition,[],[f3103,f935]) ).
fof(f3529,plain,
( op2(e23,e23) != h2(op1(e10,e10))
| spl8_65
| ~ spl8_82 ),
inference(forward_demodulation,[],[f858,f925]) ).
fof(f3531,plain,
( op2(e23,e23) != h2(e13)
| spl8_65
| ~ spl8_82
| ~ spl8_232 ),
inference(forward_demodulation,[],[f3529,f1760]) ).
fof(f3533,plain,
( e20 != op2(e23,e23)
| ~ spl8_12
| spl8_65
| ~ spl8_82
| ~ spl8_232 ),
inference(forward_demodulation,[],[f3531,f605]) ).
fof(f3535,plain,
( $false
| ~ spl8_12
| spl8_65
| ~ spl8_82
| ~ spl8_214
| ~ spl8_232 ),
inference(forward_subsumption_resolution,[],[f3533,f1658]) ).
fof(f3536,plain,
( ~ spl8_12
| spl8_65
| ~ spl8_82
| ~ spl8_214
| ~ spl8_232 ),
inference(avatar_contradiction_clause,[],[f3535]) ).
fof(f3539,plain,
( h2(op1(e10,e11)) != op2(h2(e10),e22)
| spl8_66
| ~ spl8_84 ),
inference(forward_demodulation,[],[f862,f935]) ).
fof(f3541,plain,
( op2(e23,e22) != h2(op1(e10,e11))
| spl8_66
| ~ spl8_82
| ~ spl8_84 ),
inference(forward_demodulation,[],[f3539,f925]) ).
fof(f3543,plain,
( op2(e23,e22) != h2(e12)
| spl8_66
| ~ spl8_82
| ~ spl8_84
| ~ spl8_227 ),
inference(forward_demodulation,[],[f3541,f1738]) ).
fof(f3544,plain,
( e21 != op2(e23,e22)
| ~ spl8_18
| spl8_66
| ~ spl8_82
| ~ spl8_84
| ~ spl8_227 ),
inference(forward_demodulation,[],[f3543,f634]) ).
fof(f3548,plain,
( h2(op1(e10,e12)) != op2(h2(e10),e21)
| ~ spl8_18
| spl8_67 ),
inference(forward_demodulation,[],[f866,f634]) ).
fof(f3550,plain,
( op2(e23,e21) != h2(op1(e10,e12))
| ~ spl8_18
| spl8_67
| ~ spl8_82 ),
inference(forward_demodulation,[],[f3548,f925]) ).
fof(f3552,plain,
( op2(e23,e21) != h2(e10)
| ~ spl8_18
| spl8_67
| ~ spl8_82
| ~ spl8_155 ),
inference(forward_demodulation,[],[f3550,f1333]) ).
fof(f3554,plain,
( e23 != op2(e23,e21)
| ~ spl8_18
| spl8_67
| ~ spl8_82
| ~ spl8_155 ),
inference(forward_demodulation,[],[f3552,f925]) ).
fof(f3555,plain,
( $false
| ~ spl8_18
| spl8_67
| ~ spl8_82
| ~ spl8_146
| ~ spl8_155 ),
inference(forward_subsumption_resolution,[],[f3554,f1250]) ).
fof(f3556,plain,
( ~ spl8_18
| spl8_67
| ~ spl8_82
| ~ spl8_146
| ~ spl8_155 ),
inference(avatar_contradiction_clause,[],[f3555]) ).
fof(f3558,plain,
( h2(op1(e10,e13)) != op2(h2(e10),e20)
| ~ spl8_12
| spl8_68 ),
inference(forward_demodulation,[],[f870,f605]) ).
fof(f3560,plain,
( op2(e23,e20) != h2(op1(e10,e13))
| ~ spl8_12
| spl8_68
| ~ spl8_82 ),
inference(forward_demodulation,[],[f3558,f925]) ).
fof(f3562,plain,
( op2(e23,e20) != h2(e11)
| ~ spl8_12
| spl8_68
| ~ spl8_82
| ~ spl8_223 ),
inference(forward_demodulation,[],[f3560,f1720]) ).
fof(f3564,plain,
( e22 != op2(e23,e20)
| ~ spl8_12
| spl8_68
| ~ spl8_82
| ~ spl8_84
| ~ spl8_223 ),
inference(forward_demodulation,[],[f3562,f935]) ).
fof(f3565,plain,
( $false
| ~ spl8_12
| spl8_68
| ~ spl8_82
| ~ spl8_84
| ~ spl8_183
| ~ spl8_223 ),
inference(forward_subsumption_resolution,[],[f3564,f1515]) ).
fof(f3566,plain,
( ~ spl8_12
| spl8_68
| ~ spl8_82
| ~ spl8_84
| ~ spl8_183
| ~ spl8_223 ),
inference(avatar_contradiction_clause,[],[f3565]) ).
fof(f3568,plain,
( h2(op1(e11,e10)) != op2(h2(e11),e23)
| spl8_69
| ~ spl8_82 ),
inference(forward_demodulation,[],[f874,f925]) ).
fof(f3570,plain,
( op2(e22,e23) != h2(op1(e11,e10))
| spl8_69
| ~ spl8_82
| ~ spl8_84 ),
inference(forward_demodulation,[],[f3568,f935]) ).
fof(f3572,plain,
( op2(e22,e23) != h2(e11)
| spl8_69
| ~ spl8_82
| ~ spl8_84
| ~ spl8_154 ),
inference(forward_demodulation,[],[f3570,f1330]) ).
fof(f3574,plain,
( e22 != op2(e22,e23)
| spl8_69
| ~ spl8_82
| ~ spl8_84
| ~ spl8_154 ),
inference(forward_demodulation,[],[f3572,f935]) ).
fof(f3575,plain,
( $false
| spl8_69
| ~ spl8_82
| ~ spl8_84
| ~ spl8_151
| ~ spl8_154 ),
inference(forward_subsumption_resolution,[],[f3574,f1293]) ).
fof(f3576,plain,
( spl8_69
| ~ spl8_82
| ~ spl8_84
| ~ spl8_151
| ~ spl8_154 ),
inference(avatar_contradiction_clause,[],[f3575]) ).
fof(f3578,plain,
( op2(e22,e22) != h2(op1(e11,e11))
| spl8_70
| ~ spl8_84 ),
inference(forward_demodulation,[],[f878,f935]) ).
fof(f3580,plain,
( op2(e22,e22) != h2(e10)
| spl8_70
| ~ spl8_84
| ~ spl8_238 ),
inference(forward_demodulation,[],[f3578,f1786]) ).
fof(f3582,plain,
( e23 != op2(e22,e22)
| spl8_70
| ~ spl8_82
| ~ spl8_84
| ~ spl8_238 ),
inference(forward_demodulation,[],[f3580,f925]) ).
fof(f3584,plain,
( $false
| spl8_70
| ~ spl8_82
| ~ spl8_84
| ~ spl8_212
| ~ spl8_238 ),
inference(forward_subsumption_resolution,[],[f3582,f1648]) ).
fof(f3585,plain,
( spl8_70
| ~ spl8_82
| ~ spl8_84
| ~ spl8_212
| ~ spl8_238 ),
inference(avatar_contradiction_clause,[],[f3584]) ).
fof(f3587,plain,
( h2(op1(e11,e12)) != op2(h2(e11),e21)
| ~ spl8_18
| spl8_71 ),
inference(forward_demodulation,[],[f882,f634]) ).
fof(f3589,plain,
( op2(e22,e21) != h2(op1(e11,e12))
| ~ spl8_18
| spl8_71
| ~ spl8_84 ),
inference(forward_demodulation,[],[f3587,f935]) ).
fof(f3591,plain,
( op2(e22,e21) != h2(e12)
| ~ spl8_18
| spl8_71
| ~ spl8_84
| ~ spl8_246 ),
inference(forward_demodulation,[],[f3589,f1822]) ).
fof(f3592,plain,
( e21 != op2(e22,e21)
| ~ spl8_18
| spl8_71
| ~ spl8_84
| ~ spl8_246 ),
inference(forward_demodulation,[],[f3591,f634]) ).
fof(f3596,plain,
( h2(op1(e11,e13)) != op2(h2(e11),e20)
| ~ spl8_12
| spl8_72 ),
inference(forward_demodulation,[],[f886,f605]) ).
fof(f3598,plain,
( op2(e22,e20) != h2(op1(e11,e13))
| ~ spl8_12
| spl8_72
| ~ spl8_84 ),
inference(forward_demodulation,[],[f3596,f935]) ).
fof(f3600,plain,
( op2(e22,e20) != h2(e13)
| ~ spl8_12
| spl8_72
| ~ spl8_84
| ~ spl8_251 ),
inference(forward_demodulation,[],[f3598,f1844]) ).
fof(f3602,plain,
( e20 != op2(e22,e20)
| ~ spl8_12
| spl8_72
| ~ spl8_84
| ~ spl8_251 ),
inference(forward_demodulation,[],[f3600,f605]) ).
fof(f3603,plain,
( $false
| ~ spl8_12
| spl8_72
| ~ spl8_84
| ~ spl8_170
| ~ spl8_251 ),
inference(forward_subsumption_resolution,[],[f3602,f1459]) ).
fof(f3604,plain,
( ~ spl8_12
| spl8_72
| ~ spl8_84
| ~ spl8_170
| ~ spl8_251 ),
inference(avatar_contradiction_clause,[],[f3603]) ).
fof(f3606,plain,
( h2(op1(e12,e10)) != op2(h2(e12),e23)
| spl8_73
| ~ spl8_82 ),
inference(forward_demodulation,[],[f890,f925]) ).
fof(f3608,plain,
( op2(e21,e23) != h2(op1(e12,e10))
| ~ spl8_18
| spl8_73
| ~ spl8_82 ),
inference(forward_demodulation,[],[f3606,f634]) ).
fof(f3610,plain,
( op2(e21,e23) != h2(e10)
| ~ spl8_18
| spl8_73
| ~ spl8_82
| ~ spl8_218 ),
inference(forward_demodulation,[],[f3608,f1699]) ).
fof(f3612,plain,
( e23 != op2(e21,e23)
| ~ spl8_18
| spl8_73
| ~ spl8_82
| ~ spl8_218 ),
inference(forward_demodulation,[],[f3610,f925]) ).
fof(f3613,plain,
( $false
| ~ spl8_18
| spl8_73
| ~ spl8_82
| ~ spl8_203
| ~ spl8_218 ),
inference(forward_subsumption_resolution,[],[f3612,f1604]) ).
fof(f3614,plain,
( ~ spl8_18
| spl8_73
| ~ spl8_82
| ~ spl8_203
| ~ spl8_218 ),
inference(avatar_contradiction_clause,[],[f3613]) ).
fof(f3616,plain,
( op2(e21,e21) != h2(op1(e12,e12))
| ~ spl8_18
| spl8_75 ),
inference(forward_demodulation,[],[f898,f634]) ).
fof(f3618,plain,
( op2(e21,e21) != h2(e13)
| ~ spl8_18
| spl8_75
| ~ spl8_260 ),
inference(forward_demodulation,[],[f3616,f1888]) ).
fof(f3620,plain,
( e20 != op2(e21,e21)
| ~ spl8_12
| ~ spl8_18
| spl8_75
| ~ spl8_260 ),
inference(forward_demodulation,[],[f3618,f605]) ).
fof(f3622,plain,
( $false
| ~ spl8_12
| ~ spl8_18
| spl8_75
| ~ spl8_190
| ~ spl8_260 ),
inference(forward_subsumption_resolution,[],[f3620,f1546]) ).
fof(f3623,plain,
( ~ spl8_12
| ~ spl8_18
| spl8_75
| ~ spl8_190
| ~ spl8_260 ),
inference(avatar_contradiction_clause,[],[f3622]) ).
fof(f3625,plain,
( h2(op1(e12,e13)) != op2(h2(e12),e20)
| ~ spl8_12
| spl8_76 ),
inference(forward_demodulation,[],[f902,f605]) ).
fof(f3627,plain,
( op2(e21,e20) != h2(op1(e12,e13))
| ~ spl8_12
| ~ spl8_18
| spl8_76 ),
inference(forward_demodulation,[],[f3625,f634]) ).
fof(f3629,plain,
( op2(e21,e20) != h2(e12)
| ~ spl8_12
| ~ spl8_18
| spl8_76
| ~ spl8_167 ),
inference(forward_demodulation,[],[f3627,f1421]) ).
fof(f3630,plain,
( e21 != op2(e21,e20)
| ~ spl8_12
| ~ spl8_18
| spl8_76
| ~ spl8_167 ),
inference(forward_demodulation,[],[f3629,f634]) ).
fof(f3631,plain,
( $false
| ~ spl8_12
| ~ spl8_18
| spl8_76
| ~ spl8_138
| ~ spl8_167 ),
inference(forward_subsumption_resolution,[],[f3630,f1202]) ).
fof(f3632,plain,
( ~ spl8_12
| ~ spl8_18
| spl8_76
| ~ spl8_138
| ~ spl8_167 ),
inference(avatar_contradiction_clause,[],[f3631]) ).
fof(f3634,plain,
( h2(op1(e13,e10)) != op2(h2(e13),e23)
| spl8_77
| ~ spl8_82 ),
inference(forward_demodulation,[],[f906,f925]) ).
fof(f3636,plain,
( op2(e20,e23) != h2(op1(e13,e10))
| ~ spl8_12
| spl8_77
| ~ spl8_82 ),
inference(forward_demodulation,[],[f3634,f605]) ).
fof(f3638,plain,
( op2(e20,e23) != h2(e12)
| ~ spl8_12
| spl8_77
| ~ spl8_82
| ~ spl8_231 ),
inference(forward_demodulation,[],[f3636,f1755]) ).
fof(f3640,plain,
( e21 != op2(e20,e23)
| ~ spl8_12
| ~ spl8_18
| spl8_77
| ~ spl8_82
| ~ spl8_231 ),
inference(forward_demodulation,[],[f3638,f634]) ).
fof(f3641,plain,
( $false
| ~ spl8_12
| ~ spl8_18
| spl8_77
| ~ spl8_82
| ~ spl8_175
| ~ spl8_231 ),
inference(forward_subsumption_resolution,[],[f3640,f1480]) ).
fof(f3642,plain,
( ~ spl8_12
| ~ spl8_18
| spl8_77
| ~ spl8_82
| ~ spl8_175
| ~ spl8_231 ),
inference(avatar_contradiction_clause,[],[f3641]) ).
fof(f3644,plain,
( h2(op1(e13,e11)) != op2(h2(e13),e22)
| spl8_78
| ~ spl8_84 ),
inference(forward_demodulation,[],[f910,f935]) ).
fof(f3646,plain,
( op2(e20,e22) != h2(op1(e13,e11))
| ~ spl8_12
| spl8_78
| ~ spl8_84 ),
inference(forward_demodulation,[],[f3644,f605]) ).
fof(f3648,plain,
( op2(e20,e22) != h2(e13)
| ~ spl8_12
| spl8_78
| ~ spl8_84
| ~ spl8_162 ),
inference(forward_demodulation,[],[f3646,f1378]) ).
fof(f3650,plain,
( e20 != op2(e20,e22)
| ~ spl8_12
| spl8_78
| ~ spl8_84
| ~ spl8_162 ),
inference(forward_demodulation,[],[f3648,f605]) ).
fof(f3651,plain,
( $false
| ~ spl8_12
| spl8_78
| ~ spl8_84
| ~ spl8_139
| ~ spl8_162 ),
inference(forward_subsumption_resolution,[],[f3650,f1205]) ).
fof(f3652,plain,
( ~ spl8_12
| spl8_78
| ~ spl8_84
| ~ spl8_139
| ~ spl8_162 ),
inference(avatar_contradiction_clause,[],[f3651]) ).
fof(f3654,plain,
( h2(op1(e13,e12)) != op2(h2(e13),e21)
| ~ spl8_18
| spl8_79 ),
inference(forward_demodulation,[],[f914,f634]) ).
fof(f3656,plain,
( op2(e20,e21) != h2(op1(e13,e12))
| ~ spl8_12
| ~ spl8_18
| spl8_79 ),
inference(forward_demodulation,[],[f3654,f605]) ).
fof(f3658,plain,
( op2(e20,e21) != h2(e11)
| ~ spl8_12
| ~ spl8_18
| spl8_79
| ~ spl8_258 ),
inference(forward_demodulation,[],[f3656,f1877]) ).
fof(f3660,plain,
( e22 != op2(e20,e21)
| ~ spl8_12
| ~ spl8_18
| spl8_79
| ~ spl8_84
| ~ spl8_258 ),
inference(forward_demodulation,[],[f3658,f935]) ).
fof(f3664,plain,
( op2(e20,e20) != h2(op1(e13,e13))
| ~ spl8_12
| spl8_80 ),
inference(forward_demodulation,[],[f918,f605]) ).
fof(f3666,plain,
( op2(e20,e20) != h2(e10)
| ~ spl8_12
| spl8_80
| ~ spl8_262 ),
inference(forward_demodulation,[],[f3664,f1898]) ).
fof(f3668,plain,
( op2(e20,e20) != e23
| ~ spl8_12
| spl8_80
| ~ spl8_82
| ~ spl8_262 ),
inference(forward_demodulation,[],[f3666,f925]) ).
fof(f3670,plain,
( $false
| ~ spl8_12
| spl8_80
| ~ spl8_82
| ~ spl8_184
| ~ spl8_262 ),
inference(forward_subsumption_resolution,[],[f3668,f1520]) ).
fof(f3671,plain,
( ~ spl8_12
| spl8_80
| ~ spl8_82
| ~ spl8_184
| ~ spl8_262 ),
inference(avatar_contradiction_clause,[],[f3670]) ).
fof(f3676,plain,
( e13 != op1(e13,e13)
| ~ spl8_162 ),
inference(forward_demodulation,[],[f118,f1378]) ).
fof(f3680,plain,
( spl8_262
| ~ spl8_260 ),
inference(avatar_split_clause,[],[f3295,f1886,f1896]) ).
fof(f3689,plain,
( ~ spl8_168
| ~ spl8_162 ),
inference(avatar_split_clause,[],[f3676,f1376,f1432]) ).
fof(f3696,plain,
( ~ spl8_159
| ~ spl8_262 ),
inference(avatar_split_clause,[],[f3208,f1896,f1356]) ).
fof(f3697,plain,
( spl8_223
| ~ spl8_260
| ~ spl8_262 ),
inference(avatar_split_clause,[],[f3508,f1896,f1886,f1718]) ).
fof(f3698,plain,
( ~ spl8_255
| ~ spl8_262 ),
inference(avatar_split_clause,[],[f3172,f1896,f1861]) ).
fof(f3699,plain,
( ~ spl8_254
| ~ spl8_262 ),
inference(avatar_split_clause,[],[f3204,f1896,f1856]) ).
fof(f3702,plain,
( e13 != op1(e13,e12)
| ~ spl8_260 ),
inference(forward_demodulation,[],[f147,f1888]) ).
fof(f3705,plain,
( e11 != op1(e11,e13)
| ~ spl8_154 ),
inference(forward_demodulation,[],[f132,f1330]) ).
fof(f3708,plain,
( e11 != op1(e11,e12)
| ~ spl8_154 ),
inference(forward_demodulation,[],[f133,f1330]) ).
fof(f3709,plain,
( ~ spl8_250
| ~ spl8_260 ),
inference(avatar_split_clause,[],[f3215,f1886,f1838]) ).
fof(f3711,plain,
( e13 != op1(e12,e13)
| ~ spl8_260 ),
inference(forward_demodulation,[],[f123,f1888]) ).
fof(f3717,plain,
( ~ spl8_234
| ~ spl8_260 ),
inference(avatar_split_clause,[],[f3219,f1886,f1766]) ).
fof(f3723,plain,
( ~ spl8_166
| ~ spl8_260 ),
inference(avatar_split_clause,[],[f3702,f1886,f1408]) ).
fof(f3725,plain,
( ~ spl8_161
| ~ spl8_154 ),
inference(avatar_split_clause,[],[f3708,f1328,f1372]) ).
fof(f3726,plain,
( ~ spl8_261
| ~ spl8_260 ),
inference(avatar_split_clause,[],[f3711,f1886,f1890]) ).
fof(f3737,plain,
( ~ spl8_222
| ~ spl8_223 ),
inference(avatar_split_clause,[],[f3197,f1718,f1714]) ).
fof(f3738,plain,
( ~ spl8_220
| ~ spl8_223 ),
inference(avatar_split_clause,[],[f3201,f1718,f1706]) ).
fof(f3743,plain,
( ~ spl8_244
| ~ spl8_258 ),
inference(avatar_split_clause,[],[f3174,f1875,f1811]) ).
fof(f3744,plain,
( ~ spl8_225
| ~ spl8_258 ),
inference(avatar_split_clause,[],[f3176,f1875,f1727]) ).
fof(f3759,plain,
( ~ spl8_164
| ~ spl8_154 ),
inference(avatar_split_clause,[],[f3705,f1328,f1392]) ).
fof(f3774,plain,
( ~ spl8_156
| ~ spl8_162 ),
inference(avatar_split_clause,[],[f3177,f1376,f1336]) ).
fof(f3777,plain,
( ~ spl8_229
| ~ spl8_167 ),
inference(avatar_split_clause,[],[f3209,f1420,f1744]) ).
fof(f3779,plain,
( ~ spl8_163
| ~ spl8_167 ),
inference(avatar_split_clause,[],[f3181,f1420,f1384]) ).
fof(f3796,plain,
( ~ spl8_210
| ~ spl8_18
| spl8_66
| ~ spl8_82
| ~ spl8_84
| ~ spl8_227 ),
inference(avatar_split_clause,[],[f3544,f1736,f934,f924,f860,f633,f1635]) ).
fof(f3804,plain,
( e22 != op2(e23,e22)
| ~ spl8_183 ),
inference(forward_demodulation,[],[f169,f1515]) ).
fof(f3805,plain,
( ~ spl8_207
| ~ spl8_214 ),
inference(avatar_split_clause,[],[f3413,f1656,f1621]) ).
fof(f3809,plain,
( ~ spl8_192
| ~ spl8_214 ),
inference(avatar_split_clause,[],[f3442,f1656,f1552]) ).
fof(f3816,plain,
( ~ spl8_173
| ~ spl8_175 ),
inference(avatar_split_clause,[],[f3434,f1478,f1470]) ).
fof(f3833,plain,
( ~ spl8_195
| ~ spl8_18
| spl8_71
| ~ spl8_84
| ~ spl8_246 ),
inference(avatar_split_clause,[],[f3592,f1820,f934,f880,f633,f1567]) ).
fof(f3837,plain,
( ~ spl8_198
| ~ spl8_18
| spl8_74
| ~ spl8_84
| ~ spl8_243 ),
inference(avatar_split_clause,[],[f3526,f1807,f934,f892,f633,f1580]) ).
fof(f3838,plain,
( ~ spl8_141
| ~ spl8_139 ),
inference(avatar_split_clause,[],[f3263,f1204,f1214]) ).
fof(f3844,plain,
( ~ spl8_175
| ~ spl8_148 ),
inference(avatar_split_clause,[],[f3273,f1264,f1478]) ).
fof(f3861,plain,
( spl8_175
| ~ spl8_212
| ~ spl8_214 ),
inference(avatar_split_clause,[],[f3510,f1656,f1646,f1478]) ).
fof(f3891,plain,
( ~ spl8_211
| ~ spl8_183 ),
inference(avatar_split_clause,[],[f3804,f1513,f1641]) ).
fof(f3903,plain,
( ~ spl8_197
| ~ spl8_198 ),
inference(avatar_split_clause,[],[f3257,f1580,f1576]) ).
fof(f3907,plain,
( ~ spl8_158
| ~ spl8_167 ),
inference(avatar_split_clause,[],[f3184,f1420,f1348]) ).
fof(f3909,plain,
( ~ spl8_157
| ~ spl8_155 ),
inference(avatar_split_clause,[],[f3200,f1332,f1342]) ).
fof(f3918,plain,
( spl8_140
| ~ spl8_38
| ~ spl8_135
| ~ spl8_138 ),
inference(avatar_split_clause,[],[f1998,f1200,f1176,f729,f1208]) ).
fof(f3925,plain,
( ~ spl8_179
| ~ spl8_12
| ~ spl8_18
| spl8_79
| ~ spl8_84
| ~ spl8_258 ),
inference(avatar_split_clause,[],[f3660,f1875,f934,f912,f633,f604,f1496]) ).
fof(f3929,plain,
( ~ spl8_151
| ~ spl8_147 ),
inference(avatar_split_clause,[],[f3334,f1256,f1292]) ).
fof(f3954,plain,
( ~ spl8_171
| ~ spl8_214 ),
inference(avatar_split_clause,[],[f3418,f1656,f1461]) ).
fof(f4025,plain,
( $false
| ~ spl8_3
| ~ spl8_8 ),
inference(forward_subsumption_resolution,[],[f224,f1945]) ).
fof(f4026,plain,
( ~ spl8_3
| ~ spl8_8 ),
inference(avatar_contradiction_clause,[],[f4025]) ).
cnf(s9,plain,
( ~ spl8_11
| ~ spl8_12 ),
inference(sat_conversion,[],[f607]) ).
cnf(s14,plain,
( ~ spl8_16
| ~ spl8_18 ),
inference(sat_conversion,[],[f636]) ).
cnf(s51,plain,
( spl8_11
| spl8_16
| ~ spl8_65
| ~ spl8_66
| ~ spl8_67
| ~ spl8_68
| ~ spl8_69
| ~ spl8_70
| ~ spl8_71
| ~ spl8_72
| ~ spl8_73
| ~ spl8_74
| ~ spl8_75
| ~ spl8_76
| ~ spl8_77
| ~ spl8_78
| ~ spl8_79
| ~ spl8_80
| ~ spl8_82
| ~ spl8_84 ),
inference(sat_conversion,[],[f937]) ).
cnf(s97,plain,
spl8_135,
inference(sat_conversion,[],[f1191]) ).
cnf(s98,plain,
spl8_107,
inference(sat_conversion,[],[f1192]) ).
cnf(s99,plain,
spl8_18,
inference(sat_conversion,[],[f1193]) ).
cnf(s100,plain,
spl8_3,
inference(sat_conversion,[],[f1194]) ).
cnf(s102,plain,
( spl8_137
| spl8_138
| ~ spl8_139
| spl8_140 ),
inference(sat_conversion,[],[f1212]) ).
cnf(s122,plain,
( spl8_141
| spl8_144
| spl8_146
| spl8_147 ),
inference(sat_conversion,[],[f1260]) ).
cnf(s124,plain,
( spl8_141
| ~ spl8_144
| spl8_146
| spl8_147 ),
inference(sat_conversion,[],[f1262]) ).
cnf(s138,plain,
( spl8_139
| spl8_145
| spl8_149
| spl8_150 ),
inference(sat_conversion,[],[f1288]) ).
cnf(s153,plain,
( ~ spl8_140
| spl8_148
| spl8_151
| spl8_152 ),
inference(sat_conversion,[],[f1311]) ).
cnf(s169,plain,
( ~ spl8_153
| spl8_154
| spl8_156
| spl8_158 ),
inference(sat_conversion,[],[f1351]) ).
cnf(s170,plain,
( spl8_153
| spl8_154
| spl8_156
| spl8_158 ),
inference(sat_conversion,[],[f1352]) ).
cnf(s182,plain,
( spl8_157
| spl8_160
| ~ spl8_161
| spl8_162 ),
inference(sat_conversion,[],[f1380]) ).
cnf(s184,plain,
( spl8_157
| ~ spl8_160
| ~ spl8_161
| spl8_162 ),
inference(sat_conversion,[],[f1382]) ).
cnf(s186,plain,
( spl8_157
| spl8_160
| spl8_162
| spl8_163 ),
inference(sat_conversion,[],[f1388]) ).
cnf(s188,plain,
( spl8_157
| ~ spl8_160
| spl8_162
| spl8_163 ),
inference(sat_conversion,[],[f1390]) ).
cnf(s190,plain,
( spl8_157
| spl8_160
| ~ spl8_161
| ~ spl8_164 ),
inference(sat_conversion,[],[f1396]) ).
cnf(s192,plain,
( spl8_157
| ~ spl8_160
| ~ spl8_161
| ~ spl8_164 ),
inference(sat_conversion,[],[f1398]) ).
cnf(s194,plain,
( spl8_157
| spl8_160
| spl8_163
| ~ spl8_164 ),
inference(sat_conversion,[],[f1400]) ).
cnf(s196,plain,
( spl8_157
| ~ spl8_160
| spl8_163
| ~ spl8_164 ),
inference(sat_conversion,[],[f1402]) ).
cnf(s198,plain,
( spl8_155
| spl8_161
| ~ spl8_165
| spl8_166 ),
inference(sat_conversion,[],[f1412]) ).
cnf(s202,plain,
( spl8_155
| spl8_161
| spl8_165
| spl8_166 ),
inference(sat_conversion,[],[f1416]) ).
cnf(s218,plain,
( spl8_159
| spl8_164
| spl8_167
| spl8_168 ),
inference(sat_conversion,[],[f1440]) ).
cnf(s226,plain,
( spl8_159
| spl8_164
| spl8_167
| ~ spl8_168 ),
inference(sat_conversion,[],[f1448]) ).
cnf(s230,plain,
( spl8_137
| spl8_169
| spl8_170
| spl8_171 ),
inference(sat_conversion,[],[f1464]) ).
cnf(s234,plain,
( spl8_142
| spl8_178
| spl8_182
| spl8_183 ),
inference(sat_conversion,[],[f1516]) ).
cnf(s236,plain,
( spl8_140
| spl8_184
| spl8_188
| spl8_189 ),
inference(sat_conversion,[],[f1542]) ).
cnf(s237,plain,
( spl8_169
| spl8_190
| spl8_191
| spl8_192 ),
inference(sat_conversion,[],[f1555]) ).
cnf(s240,plain,
( spl8_144
| spl8_173
| spl8_195
| spl8_196 ),
inference(sat_conversion,[],[f1574]) ).
cnf(s242,plain,
( spl8_147
| spl8_179
| spl8_197
| spl8_200 ),
inference(sat_conversion,[],[f1592]) ).
cnf(s243,plain,
( spl8_188
| spl8_201
| spl8_202
| spl8_203 ),
inference(sat_conversion,[],[f1605]) ).
cnf(s246,plain,
( spl8_139
| spl8_191
| spl8_205
| spl8_207 ),
inference(sat_conversion,[],[f1624]) ).
cnf(s249,plain,
( spl8_142
| spl8_147
| spl8_149
| spl8_151 ),
inference(sat_conversion,[],[f1639]) ).
cnf(s250,plain,
( spl8_149
| spl8_180
| spl8_198
| spl8_211 ),
inference(sat_conversion,[],[f1644]) ).
cnf(s275,plain,
( spl8_150
| spl8_207
| spl8_210
| spl8_211 ),
inference(sat_conversion,[],[f1689]) ).
cnf(s280,plain,
( spl8_154
| spl8_220
| spl8_224
| spl8_225 ),
inference(sat_conversion,[],[f1730]) ).
cnf(s281,plain,
( spl8_226
| spl8_227
| spl8_228
| spl8_229 ),
inference(sat_conversion,[],[f1747]) ).
cnf(s283,plain,
( spl8_232
| spl8_233
| spl8_234
| spl8_235 ),
inference(sat_conversion,[],[f1773]) ).
cnf(s284,plain,
( spl8_156
| spl8_232
| spl8_236
| spl8_237 ),
inference(sat_conversion,[],[f1782]) ).
cnf(s285,plain,
( spl8_217
| spl8_238
| spl8_239
| spl8_240 ),
inference(sat_conversion,[],[f1795]) ).
cnf(s286,plain,
( spl8_157
| spl8_238
| spl8_241
| spl8_242 ),
inference(sat_conversion,[],[f1804]) ).
cnf(s287,plain,
( spl8_154
| spl8_160
| spl8_161
| spl8_164 ),
inference(sat_conversion,[],[f1805]) ).
cnf(s288,plain,
( spl8_160
| spl8_221
| spl8_243
| spl8_244 ),
inference(sat_conversion,[],[f1814]) ).
cnf(s291,plain,
( spl8_236
| spl8_249
| spl8_250
| spl8_251 ),
inference(sat_conversion,[],[f1845]) ).
cnf(s293,plain,
( spl8_218
| spl8_241
| spl8_253
| spl8_254 ),
inference(sat_conversion,[],[f1859]) ).
cnf(s294,plain,
( spl8_155
| spl8_239
| spl8_253
| spl8_255 ),
inference(sat_conversion,[],[f1864]) ).
cnf(s295,plain,
( spl8_224
| spl8_243
| spl8_256
| spl8_257 ),
inference(sat_conversion,[],[f1873]) ).
cnf(s296,plain,
( spl8_161
| spl8_222
| spl8_256
| spl8_258 ),
inference(sat_conversion,[],[f1878]) ).
cnf(s298,plain,
( spl8_165
| spl8_228
| spl8_246
| spl8_259 ),
inference(sat_conversion,[],[f1884]) ).
cnf(s305,plain,
( spl8_231
| spl8_248
| spl8_259
| spl8_264 ),
inference(sat_conversion,[],[f1911]) ).
cnf(s308,plain,
( spl8_168
| spl8_235
| spl8_251
| spl8_261 ),
inference(sat_conversion,[],[f1914]) ).
cnf(s325,plain,
spl8_260,
inference(sat_conversion,[],[f1935]) ).
cnf(s326,plain,
spl8_212,
inference(sat_conversion,[],[f1936]) ).
cnf(s346,plain,
( ~ spl8_3
| spl8_8
| ~ spl8_138
| ~ spl8_169 ),
inference(sat_conversion,[],[f2023]) ).
cnf(s352,plain,
( ~ spl8_138
| ~ spl8_182 ),
inference(sat_conversion,[],[f2048]) ).
cnf(s355,plain,
( ~ spl8_147
| ~ spl8_195 ),
inference(sat_conversion,[],[f2061]) ).
cnf(s356,plain,
( ~ spl8_178
| ~ spl8_184 ),
inference(sat_conversion,[],[f2070]) ).
cnf(s376,plain,
( spl8_38
| ~ spl8_135
| ~ spl8_138
| ~ spl8_188 ),
inference(sat_conversion,[],[f2143]) ).
cnf(s377,plain,
( ~ spl8_170
| ~ spl8_189 ),
inference(sat_conversion,[],[f2149]) ).
cnf(s381,plain,
( ~ spl8_3
| spl8_8
| ~ spl8_144
| ~ spl8_190 ),
inference(sat_conversion,[],[f2165]) ).
cnf(s386,plain,
( spl8_23
| ~ spl8_107
| ~ spl8_191
| ~ spl8_198 ),
inference(sat_conversion,[],[f2187]) ).
cnf(s422,plain,
( spl8_23
| ~ spl8_107
| ~ spl8_139
| ~ spl8_180 ),
inference(sat_conversion,[],[f2369]) ).
cnf(s426,plain,
( ~ spl8_146
| ~ spl8_200 ),
inference(sat_conversion,[],[f2387]) ).
cnf(s431,plain,
( ~ spl8_149
| ~ spl8_212 ),
inference(sat_conversion,[],[f2420]) ).
cnf(s436,plain,
( spl8_23
| ~ spl8_107
| ~ spl8_142
| ~ spl8_170 ),
inference(sat_conversion,[],[f2461]) ).
cnf(s442,plain,
( ~ spl8_3
| spl8_8
| ~ spl8_145
| ~ spl8_191 ),
inference(sat_conversion,[],[f2489]) ).
cnf(s445,plain,
( ~ spl8_205
| ~ spl8_212 ),
inference(sat_conversion,[],[f2499]) ).
cnf(s459,plain,
( ~ spl8_23
| ~ spl8_107
| ~ spl8_139
| spl8_149 ),
inference(sat_conversion,[],[f2573]) ).
cnf(s473,plain,
( ~ spl8_218
| ~ spl8_224 ),
inference(sat_conversion,[],[f2692]) ).
cnf(s481,plain,
( ~ spl8_226
| ~ spl8_232 ),
inference(sat_conversion,[],[f2723]) ).
cnf(s483,plain,
( ~ spl8_154
| ~ spl8_217 ),
inference(sat_conversion,[],[f2730]) ).
cnf(s487,plain,
( ~ spl8_221
| ~ spl8_227 ),
inference(sat_conversion,[],[f2747]) ).
cnf(s488,plain,
( ~ spl8_154
| ~ spl8_236 ),
inference(sat_conversion,[],[f2756]) ).
cnf(s489,plain,
( ~ spl8_160
| ~ spl8_249 ),
inference(sat_conversion,[],[f2760]) ).
cnf(s490,plain,
( ~ spl8_218
| ~ spl8_237 ),
inference(sat_conversion,[],[f2764]) ).
cnf(s492,plain,
( ~ spl8_160
| ~ spl8_238 ),
inference(sat_conversion,[],[f2771]) ).
cnf(s493,plain,
( ~ spl8_162
| ~ spl8_242 ),
inference(sat_conversion,[],[f2777]) ).
cnf(s494,plain,
( ~ spl8_162
| ~ spl8_242 ),
inference(sat_conversion,[],[f2779]) ).
cnf(s495,plain,
( ~ spl8_163
| ~ spl8_241 ),
inference(sat_conversion,[],[f2782]) ).
cnf(s500,plain,
( ~ spl8_239
| ~ spl8_246 ),
inference(sat_conversion,[],[f2810]) ).
cnf(s512,plain,
( ~ spl8_240
| ~ spl8_251 ),
inference(sat_conversion,[],[f2867]) ).
cnf(s514,plain,
( ~ spl8_221
| ~ spl8_233 ),
inference(sat_conversion,[],[f2876]) ).
cnf(s534,plain,
( ~ spl8_167
| ~ spl8_257 ),
inference(sat_conversion,[],[f2979]) ).
cnf(s535,plain,
( ~ spl8_241
| ~ spl8_243 ),
inference(sat_conversion,[],[f2986]) ).
cnf(s537,plain,
( ~ spl8_162
| ~ spl8_248 ),
inference(sat_conversion,[],[f2996]) ).
cnf(s541,plain,
( ~ spl8_258
| ~ spl8_259 ),
inference(sat_conversion,[],[f3021]) ).
cnf(s543,plain,
( ~ spl8_155
| ~ spl8_228 ),
inference(sat_conversion,[],[f3028]) ).
cnf(s544,plain,
( ~ spl8_256
| ~ spl8_260 ),
inference(sat_conversion,[],[f3035]) ).
cnf(s553,plain,
( ~ spl8_223
| ~ spl8_235 ),
inference(sat_conversion,[],[f3072]) ).
cnf(s556,plain,
( ~ spl8_161
| ~ spl8_239 ),
inference(sat_conversion,[],[f3099]) ).
cnf(s561,plain,
( ~ spl8_253
| ~ spl8_260 ),
inference(sat_conversion,[],[f3147]) ).
cnf(s564,plain,
( ~ spl8_262
| ~ spl8_264 ),
inference(sat_conversion,[],[f3159]) ).
cnf(s569,plain,
( ~ spl8_165
| ~ spl8_167 ),
inference(sat_conversion,[],[f3179]) ).
cnf(s573,plain,
( ~ spl8_212
| spl8_214 ),
inference(sat_conversion,[],[f3313]) ).
cnf(s574,plain,
( ~ spl8_196
| ~ spl8_210 ),
inference(sat_conversion,[],[f3314]) ).
cnf(s575,plain,
( ~ spl8_190
| ~ spl8_201 ),
inference(sat_conversion,[],[f3320]) ).
cnf(s585,plain,
( ~ spl8_150
| ~ spl8_212 ),
inference(sat_conversion,[],[f3341]) ).
cnf(s590,plain,
( ~ spl8_137
| ~ spl8_139 ),
inference(sat_conversion,[],[f3347]) ).
cnf(s592,plain,
( ~ spl8_140
| ~ spl8_152 ),
inference(sat_conversion,[],[f3349]) ).
cnf(s593,plain,
( ~ spl8_140
| ~ spl8_146 ),
inference(sat_conversion,[],[f3350]) ).
cnf(s594,plain,
( ~ spl8_202
| ~ spl8_212 ),
inference(sat_conversion,[],[f3351]) ).
cnf(s603,plain,
( spl8_12
| ~ spl8_190 ),
inference(sat_conversion,[],[f3407]) ).
cnf(s607,plain,
( spl8_82
| ~ spl8_184
| ~ spl8_190 ),
inference(sat_conversion,[],[f3475]) ).
cnf(s615,plain,
( spl8_84
| ~ spl8_183
| ~ spl8_184
| ~ spl8_190 ),
inference(sat_conversion,[],[f3525]) ).
cnf(s617,plain,
( ~ spl8_12
| spl8_65
| ~ spl8_82
| ~ spl8_214
| ~ spl8_232 ),
inference(sat_conversion,[],[f3536]) ).
cnf(s619,plain,
( ~ spl8_18
| spl8_67
| ~ spl8_82
| ~ spl8_146
| ~ spl8_155 ),
inference(sat_conversion,[],[f3556]) ).
cnf(s620,plain,
( ~ spl8_12
| spl8_68
| ~ spl8_82
| ~ spl8_84
| ~ spl8_183
| ~ spl8_223 ),
inference(sat_conversion,[],[f3566]) ).
cnf(s621,plain,
( spl8_69
| ~ spl8_82
| ~ spl8_84
| ~ spl8_151
| ~ spl8_154 ),
inference(sat_conversion,[],[f3576]) ).
cnf(s622,plain,
( spl8_70
| ~ spl8_82
| ~ spl8_84
| ~ spl8_212
| ~ spl8_238 ),
inference(sat_conversion,[],[f3585]) ).
cnf(s624,plain,
( ~ spl8_12
| spl8_72
| ~ spl8_84
| ~ spl8_170
| ~ spl8_251 ),
inference(sat_conversion,[],[f3604]) ).
cnf(s625,plain,
( ~ spl8_18
| spl8_73
| ~ spl8_82
| ~ spl8_203
| ~ spl8_218 ),
inference(sat_conversion,[],[f3614]) ).
cnf(s626,plain,
( ~ spl8_12
| ~ spl8_18
| spl8_75
| ~ spl8_190
| ~ spl8_260 ),
inference(sat_conversion,[],[f3623]) ).
cnf(s627,plain,
( ~ spl8_12
| ~ spl8_18
| spl8_76
| ~ spl8_138
| ~ spl8_167 ),
inference(sat_conversion,[],[f3632]) ).
cnf(s628,plain,
( ~ spl8_12
| ~ spl8_18
| spl8_77
| ~ spl8_82
| ~ spl8_175
| ~ spl8_231 ),
inference(sat_conversion,[],[f3642]) ).
cnf(s629,plain,
( ~ spl8_12
| spl8_78
| ~ spl8_84
| ~ spl8_139
| ~ spl8_162 ),
inference(sat_conversion,[],[f3652]) ).
cnf(s631,plain,
( ~ spl8_12
| spl8_80
| ~ spl8_82
| ~ spl8_184
| ~ spl8_262 ),
inference(sat_conversion,[],[f3671]) ).
cnf(s632,plain,
( ~ spl8_260
| spl8_262 ),
inference(sat_conversion,[],[f3680]) ).
cnf(s636,plain,
( ~ spl8_162
| ~ spl8_168 ),
inference(sat_conversion,[],[f3689]) ).
cnf(s640,plain,
( ~ spl8_159
| ~ spl8_262 ),
inference(sat_conversion,[],[f3696]) ).
cnf(s641,plain,
( spl8_223
| ~ spl8_260
| ~ spl8_262 ),
inference(sat_conversion,[],[f3697]) ).
cnf(s642,plain,
( ~ spl8_255
| ~ spl8_262 ),
inference(sat_conversion,[],[f3698]) ).
cnf(s643,plain,
( ~ spl8_254
| ~ spl8_262 ),
inference(sat_conversion,[],[f3699]) ).
cnf(s644,plain,
( ~ spl8_250
| ~ spl8_260 ),
inference(sat_conversion,[],[f3709]) ).
cnf(s645,plain,
( ~ spl8_234
| ~ spl8_260 ),
inference(sat_conversion,[],[f3717]) ).
cnf(s648,plain,
( ~ spl8_166
| ~ spl8_260 ),
inference(sat_conversion,[],[f3723]) ).
cnf(s650,plain,
( ~ spl8_154
| ~ spl8_161 ),
inference(sat_conversion,[],[f3725]) ).
cnf(s651,plain,
( ~ spl8_260
| ~ spl8_261 ),
inference(sat_conversion,[],[f3726]) ).
cnf(s656,plain,
( ~ spl8_222
| ~ spl8_223 ),
inference(sat_conversion,[],[f3737]) ).
cnf(s657,plain,
( ~ spl8_220
| ~ spl8_223 ),
inference(sat_conversion,[],[f3738]) ).
cnf(s661,plain,
( ~ spl8_244
| ~ spl8_258 ),
inference(sat_conversion,[],[f3743]) ).
cnf(s662,plain,
( ~ spl8_225
| ~ spl8_258 ),
inference(sat_conversion,[],[f3744]) ).
cnf(s667,plain,
( ~ spl8_154
| ~ spl8_164 ),
inference(sat_conversion,[],[f3759]) ).
cnf(s675,plain,
( ~ spl8_156
| ~ spl8_162 ),
inference(sat_conversion,[],[f3774]) ).
cnf(s677,plain,
( ~ spl8_167
| ~ spl8_229 ),
inference(sat_conversion,[],[f3777]) ).
cnf(s680,plain,
( ~ spl8_163
| ~ spl8_167 ),
inference(sat_conversion,[],[f3779]) ).
cnf(s686,plain,
( ~ spl8_18
| spl8_66
| ~ spl8_82
| ~ spl8_84
| ~ spl8_210
| ~ spl8_227 ),
inference(sat_conversion,[],[f3796]) ).
cnf(s692,plain,
( ~ spl8_207
| ~ spl8_214 ),
inference(sat_conversion,[],[f3805]) ).
cnf(s695,plain,
( ~ spl8_192
| ~ spl8_214 ),
inference(sat_conversion,[],[f3809]) ).
cnf(s699,plain,
( ~ spl8_173
| ~ spl8_175 ),
inference(sat_conversion,[],[f3816]) ).
cnf(s709,plain,
( ~ spl8_18
| spl8_71
| ~ spl8_84
| ~ spl8_195
| ~ spl8_246 ),
inference(sat_conversion,[],[f3833]) ).
cnf(s710,plain,
( ~ spl8_18
| spl8_74
| ~ spl8_84
| ~ spl8_198
| ~ spl8_243 ),
inference(sat_conversion,[],[f3837]) ).
cnf(s711,plain,
( ~ spl8_139
| ~ spl8_141 ),
inference(sat_conversion,[],[f3838]) ).
cnf(s722,plain,
( ~ spl8_148
| ~ spl8_175 ),
inference(sat_conversion,[],[f3844]) ).
cnf(s736,plain,
( spl8_175
| ~ spl8_212
| ~ spl8_214 ),
inference(sat_conversion,[],[f3861]) ).
cnf(s769,plain,
( ~ spl8_183
| ~ spl8_211 ),
inference(sat_conversion,[],[f3891]) ).
cnf(s778,plain,
( ~ spl8_197
| ~ spl8_198 ),
inference(sat_conversion,[],[f3903]) ).
cnf(s789,plain,
( ~ spl8_158
| ~ spl8_167 ),
inference(sat_conversion,[],[f3907]) ).
cnf(s791,plain,
( ~ spl8_155
| ~ spl8_157 ),
inference(sat_conversion,[],[f3909]) ).
cnf(s798,plain,
( ~ spl8_38
| ~ spl8_135
| ~ spl8_138
| spl8_140 ),
inference(sat_conversion,[],[f3918]) ).
cnf(s802,plain,
( ~ spl8_12
| ~ spl8_18
| spl8_79
| ~ spl8_84
| ~ spl8_179
| ~ spl8_258 ),
inference(sat_conversion,[],[f3925]) ).
cnf(s808,plain,
( ~ spl8_147
| ~ spl8_151 ),
inference(sat_conversion,[],[f3929]) ).
cnf(s851,plain,
( ~ spl8_171
| ~ spl8_214 ),
inference(sat_conversion,[],[f3954]) ).
cnf(s879,plain,
( ~ spl8_3
| ~ spl8_8 ),
inference(sat_conversion,[],[f4026]) ).
cnf(s883,plain,
~ spl8_202,
inference(rat,[],[s594,s326]) ).
cnf(s884,plain,
~ spl8_150,
inference(rat,[],[s585,s326]) ).
cnf(s885,plain,
spl8_214,
inference(rat,[],[s573,s326]) ).
cnf(s887,plain,
~ spl8_205,
inference(rat,[],[s445,s326]) ).
cnf(s888,plain,
~ spl8_149,
inference(rat,[],[s431,s326]) ).
cnf(s890,plain,
~ spl8_171,
inference(rat,[],[s851,s885]) ).
cnf(s892,plain,
~ spl8_192,
inference(rat,[],[s695,s885]) ).
cnf(s893,plain,
~ spl8_207,
inference(rat,[],[s692,s885]) ).
cnf(s896,plain,
spl8_175,
inference(rat,[],[s736,s326,s885]) ).
cnf(s899,plain,
~ spl8_148,
inference(rat,[],[s722,s896]) ).
cnf(s901,plain,
~ spl8_173,
inference(rat,[],[s699,s896]) ).
cnf(s903,plain,
~ spl8_261,
inference(rat,[],[s651,s325]) ).
cnf(s904,plain,
~ spl8_166,
inference(rat,[],[s648,s325]) ).
cnf(s905,plain,
~ spl8_234,
inference(rat,[],[s645,s325]) ).
cnf(s906,plain,
~ spl8_250,
inference(rat,[],[s644,s325]) ).
cnf(s907,plain,
spl8_262,
inference(rat,[],[s632,s325]) ).
cnf(s908,plain,
~ spl8_253,
inference(rat,[],[s561,s325]) ).
cnf(s909,plain,
~ spl8_256,
inference(rat,[],[s544,s325]) ).
cnf(s910,plain,
~ spl8_254,
inference(rat,[],[s643,s907]) ).
cnf(s911,plain,
~ spl8_255,
inference(rat,[],[s642,s907]) ).
cnf(s912,plain,
~ spl8_159,
inference(rat,[],[s640,s907]) ).
cnf(s913,plain,
~ spl8_264,
inference(rat,[],[s564,s907]) ).
cnf(s915,plain,
spl8_223,
inference(rat,[],[s641,s325,s907]) ).
cnf(s916,plain,
~ spl8_220,
inference(rat,[],[s657,s915]) ).
cnf(s917,plain,
~ spl8_222,
inference(rat,[],[s656,s915]) ).
cnf(s918,plain,
~ spl8_235,
inference(rat,[],[s553,s915]) ).
cnf(s925,plain,
( spl8_168
| spl8_251 ),
inference(rat,[],[s308,s903,s918]) ).
cnf(s928,plain,
( spl8_231
| spl8_248
| spl8_259 ),
inference(rat,[],[s305,s913]) ).
cnf(s930,plain,
( spl8_161
| spl8_258 ),
inference(rat,[],[s296,s909,s917]) ).
cnf(s931,plain,
( spl8_224
| spl8_243
| spl8_257 ),
inference(rat,[],[s295,s909]) ).
cnf(s932,plain,
( spl8_155
| spl8_239 ),
inference(rat,[],[s294,s911,s908]) ).
cnf(s933,plain,
( spl8_218
| spl8_241 ),
inference(rat,[],[s293,s910,s908]) ).
cnf(s935,plain,
( spl8_236
| spl8_249
| spl8_251 ),
inference(rat,[],[s291,s906]) ).
cnf(s936,plain,
( spl8_232
| spl8_233 ),
inference(rat,[],[s283,s918,s905]) ).
cnf(s937,plain,
( spl8_154
| spl8_224
| spl8_225 ),
inference(rat,[],[s280,s916]) ).
cnf(s939,plain,
( spl8_210
| spl8_211 ),
inference(rat,[],[s275,s893,s884]) ).
cnf(s951,plain,
( spl8_180
| spl8_198
| spl8_211 ),
inference(rat,[],[s250,s888]) ).
cnf(s952,plain,
( spl8_142
| spl8_147
| spl8_151 ),
inference(rat,[],[s249,s888]) ).
cnf(s954,plain,
( spl8_139
| spl8_191 ),
inference(rat,[],[s246,s893,s887]) ).
cnf(s957,plain,
( spl8_188
| spl8_201
| spl8_203 ),
inference(rat,[],[s243,s883]) ).
cnf(s958,plain,
( spl8_144
| spl8_195
| spl8_196 ),
inference(rat,[],[s240,s901]) ).
cnf(s961,plain,
( spl8_169
| spl8_190
| spl8_191 ),
inference(rat,[],[s237,s892]) ).
cnf(s964,plain,
( spl8_137
| spl8_169
| spl8_170 ),
inference(rat,[],[s230,s890]) ).
cnf(s967,plain,
( spl8_164
| spl8_167
| ~ spl8_168 ),
inference(rat,[],[s226,s912]) ).
cnf(s969,plain,
( spl8_164
| spl8_167
| spl8_168 ),
inference(rat,[],[s218,s912]) ).
cnf(s972,plain,
( spl8_155
| spl8_161
| spl8_165 ),
inference(rat,[],[s202,s904]) ).
cnf(s976,plain,
( spl8_155
| spl8_161
| ~ spl8_165 ),
inference(rat,[],[s198,s904]) ).
cnf(s983,plain,
( ~ spl8_140
| spl8_151
| spl8_152 ),
inference(rat,[],[s153,s899]) ).
cnf(s990,plain,
( spl8_139
| spl8_145 ),
inference(rat,[],[s138,s884,s888]) ).
cnf(s992,plain,
~ spl8_8,
inference(rat,[],[s879,s100]) ).
cnf(s1007,plain,
~ spl8_16,
inference(rat,[],[s14,s99]) ).
cnf(s1010,plain,
spl8_139,
inference(rat,[],[s442,s990,s954,s100,s992]) ).
cnf(s1011,plain,
~ spl8_141,
inference(rat,[],[s711,s1010]) ).
cnf(s1012,plain,
~ spl8_137,
inference(rat,[],[s590,s1010]) ).
cnf(s1013,plain,
( spl8_146
| spl8_147 ),
inference(rat,[],[s122,s124,s1011]) ).
cnf(s1014,plain,
( spl8_140
| spl8_184 ),
inference(rat,[],[s377,s236,s964,s376,s798,s346,s102,s1012,s97,s100,s992,s1010]) ).
cnf(s1015,plain,
~ spl8_140,
inference(rat,[],[s808,s1013,s983,s592,s593]) ).
cnf(s1016,plain,
~ spl8_23,
inference(rat,[],[s459,s888,s98,s1010]) ).
cnf(s1017,plain,
~ spl8_180,
inference(rat,[],[s422,s1016,s98,s1010]) ).
cnf(s1018,plain,
spl8_138,
inference(rat,[],[s102,s1010,s1012,s1015]) ).
cnf(s1019,plain,
spl8_184,
inference(rat,[],[s1014,s1015]) ).
cnf(s1021,plain,
~ spl8_182,
inference(rat,[],[s352,s1018]) ).
cnf(s1022,plain,
~ spl8_169,
inference(rat,[],[s346,s992,s100,s1018]) ).
cnf(s1023,plain,
~ spl8_38,
inference(rat,[],[s798,s1015,s97,s1018]) ).
cnf(s1024,plain,
~ spl8_188,
inference(rat,[],[s376,s1023,s97,s1018]) ).
cnf(s1029,plain,
~ spl8_178,
inference(rat,[],[s356,s1019]) ).
cnf(s1032,plain,
spl8_170,
inference(rat,[],[s964,s1012,s1022]) ).
cnf(s1038,plain,
~ spl8_142,
inference(rat,[],[s436,s1016,s98,s1032]) ).
cnf(s1039,plain,
spl8_183,
inference(rat,[],[s234,s1021,s1029,s1038]) ).
cnf(s1040,plain,
~ spl8_211,
inference(rat,[],[s769,s1039]) ).
cnf(s1042,plain,
spl8_210,
inference(rat,[],[s939,s1040]) ).
cnf(s1043,plain,
spl8_198,
inference(rat,[],[s951,s1017,s1040]) ).
cnf(s1045,plain,
~ spl8_196,
inference(rat,[],[s574,s1042]) ).
cnf(s1046,plain,
~ spl8_197,
inference(rat,[],[s778,s1043]) ).
cnf(s1047,plain,
~ spl8_191,
inference(rat,[],[s386,s1016,s98,s1043]) ).
cnf(s1048,plain,
spl8_190,
inference(rat,[],[s961,s1022,s1047]) ).
cnf(s1049,plain,
spl8_12,
inference(rat,[],[s603,s1048]) ).
cnf(s1050,plain,
~ spl8_201,
inference(rat,[],[s575,s1048]) ).
cnf(s1051,plain,
~ spl8_144,
inference(rat,[],[s381,s992,s100,s1048]) ).
cnf(s1052,plain,
spl8_82,
inference(rat,[],[s607,s1019,s1048]) ).
cnf(s1053,plain,
spl8_84,
inference(rat,[],[s615,s1039,s1019,s1048]) ).
cnf(s1054,plain,
spl8_80,
inference(rat,[],[s631,s907,s1019,s1052,s1049]) ).
cnf(s1055,plain,
spl8_75,
inference(rat,[],[s626,s325,s1048,s99,s1049]) ).
cnf(s1056,plain,
spl8_68,
inference(rat,[],[s620,s915,s1039,s1053,s1052,s1049]) ).
cnf(s1057,plain,
~ spl8_11,
inference(rat,[],[s9,s1049]) ).
cnf(s1059,plain,
spl8_203,
inference(rat,[],[s957,s1024,s1050]) ).
cnf(s1060,plain,
spl8_195,
inference(rat,[],[s958,s1045,s1051]) ).
cnf(s1062,plain,
~ spl8_147,
inference(rat,[],[s355,s1060]) ).
cnf(s1064,plain,
spl8_146,
inference(rat,[],[s1013,s1062]) ).
cnf(s1065,plain,
spl8_151,
inference(rat,[],[s952,s1038,s1062]) ).
cnf(s1066,plain,
~ spl8_200,
inference(rat,[],[s426,s1064]) ).
cnf(s1069,plain,
spl8_179,
inference(rat,[],[s242,s1062,s1046,s1066]) ).
cnf(s1071,plain,
( spl8_161
| spl8_155 ),
inference(rat,[],[s976,s972]) ).
cnf(s1072,plain,
spl8_155,
inference(rat,[],[s1071,s556,s932]) ).
cnf(s1073,plain,
~ spl8_157,
inference(rat,[],[s791,s1072]) ).
cnf(s1074,plain,
~ spl8_228,
inference(rat,[],[s543,s1072]) ).
cnf(s1075,plain,
spl8_67,
inference(rat,[],[s619,s1064,s1052,s99,s1072]) ).
cnf(s1076,plain,
( spl8_164
| spl8_167 ),
inference(rat,[],[s969,s967]) ).
cnf(s1077,plain,
( spl8_163
| ~ spl8_164 ),
inference(rat,[],[s194,s196,s1073]) ).
cnf(s1078,plain,
( ~ spl8_164
| spl8_225 ),
inference(rat,[],[s1077,s495,s933,s473,s937,s667]) ).
cnf(s1079,plain,
( ~ spl8_160
| spl8_241
| spl8_163 ),
inference(rat,[],[s493,s286,s188,s492,s1073]) ).
cnf(s1080,plain,
( ~ spl8_218
| ~ spl8_154
| ~ spl8_258 ),
inference(rat,[],[s686,s51,s281,s622,s628,s624,s617,s481,s286,s928,s925,s284,s629,s494,s537,s636,s675,s186,s1079,s710,s535,s931,s625,s473,s490,s802,s680,s677,s534,s627,s709,s298,s569,s1076,s1078,s662,s541,s488,s621,s99,s1053,s1042,s1052,s1007,s1057,s1075,s1056,s1055,s1054,s1074,s326,s896,s1049,s1032,s885,s1073,s1010,s1043,s1059,s1065,s1060,s1018,s1069]) ).
cnf(s1081,plain,
( ~ spl8_160
| ~ spl8_154
| spl8_239 ),
inference(rat,[],[s512,s935,s285,s489,s492,s488,s483]) ).
cnf(s1082,plain,
( ~ spl8_221
| spl8_229 ),
inference(rat,[],[s481,s281,s936,s487,s514,s1074]) ).
cnf(s1083,plain,
( spl8_156
| spl8_154
| spl8_158 ),
inference(rat,[],[s169,s170]) ).
cnf(s1084,plain,
( ~ spl8_160
| ~ spl8_258 ),
inference(rat,[],[s1083,s675,s1081,s188,s789,s680,s500,s298,s569,s1076,s1078,s662,s541,s1073,s1074]) ).
cnf(s1085,plain,
spl8_161,
inference(rat,[],[s933,s1080,s535,s287,s288,s1084,s1082,s677,s1076,s1078,s661,s662,s930]) ).
cnf(s1087,plain,
~ spl8_154,
inference(rat,[],[s650,s1085]) ).
cnf(s1092,plain,
~ spl8_160,
inference(rat,[],[s1083,s789,s675,s1076,s184,s192,s1087,s1085,s1073]) ).
cnf(s1093,plain,
~ spl8_164,
inference(rat,[],[s190,s1073,s1085,s1092]) ).
cnf(s1094,plain,
spl8_162,
inference(rat,[],[s182,s1073,s1085,s1092]) ).
cnf(s1095,plain,
spl8_167,
inference(rat,[],[s1076,s1093]) ).
cnf(s1096,plain,
~ spl8_156,
inference(rat,[],[s675,s1094]) ).
cnf(s1103,plain,
~ spl8_158,
inference(rat,[],[s789,s1095]) ).
cnf(s1110,plain,
$false,
inference(rat,[],[s1083,s1087,s1103,s1096]) ).
fof(f4027,plain,
$false,
inference(avatar_sat_refutation,[],[s1110]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG110+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.20 % Computer : n013.cluster.edu
% 0.06/0.20 % Model : x86_64 x86_64
% 0.06/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.20 % Memory : 8046.5625MB
% 0.06/0.20 % OS : Linux 6.8.0-71-generic
% 0.06/0.20 % CPULimit : 300
% 0.06/0.20 % WCLimit : 300
% 0.06/0.20 % DateTime : Mon Sep 28 19:28:52 UTC 2026
% 0.06/0.20 % CPUTime :
% 0.06/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.22 Running first-order model finding
% 0.06/0.22 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.18/0.32 % (1479258)Will run a generic schedule for satisfiability detection.
% 0.18/0.32 % (1479264)% WARNING: option uhcvi not known.
% 0.18/0.32 % (1479264)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3366143067:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.32 % (1479267)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=681453335:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.32 % (1479263)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3222573312_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.32 % (1479265)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=752820574:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.32 % (1479266)dis+10_1_sil=32000:sp=arity:random_seed=3322728462:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.32 % (1479269)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2846515720:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.32 % (1479268)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3524585700:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.32 % Detected minimum model sizes of [8]
% 0.18/0.32 % Detected maximum model sizes of [max]
% 0.18/0.32 % TRYING [8]
% 0.18/0.32 % (1479264) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1479258-1479264"...
% 0.18/0.32 % (1479264)...printing done.
% 0.18/0.32 % (1479264)Refutation found. Thanks to Tanya!
% 0.18/0.32 % SZS status Theorem for theBenchmark
% 0.18/0.32 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.33 % (1479264)------------------------------
% 0.18/0.33 % (1479264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.33 % (1479264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.33 % (1479264)CaDiCaL version: 2.1.3
% 0.18/0.33 % (1479264)Termination reason: Refutation
% 0.18/0.33 % (1479264)Time elapsed: 0.057 s
% 0.18/0.33 % (1479264)Peak memory usage: 14 MB
% 0.18/0.33 % (1479264)Instructions burned: 200 (million)
% 0.18/0.33 % (1479258)Success in time 0.092 s
% 0.18/0.34 % Vampire exiting
%------------------------------------------------------------------------------