%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG038+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 : n011.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:20:35 AM UTC 2026
% Result : Theorem 0.83s 0.38s
% Output : Refutation 0.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 130
% Syntax : Number of formulae : 854 ( 167 unt; 116 def)
% Number of atoms : 2936 (1357 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 3444 (1362 ~;1556 |; 410 &)
% ( 116 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 120 ( 118 usr; 119 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e10) = e11
| op1(e10,e10) = e12
| op1(e10,e10) = e13 )
& ( op1(e10,e11) = e10
| op1(e10,e11) = e11
| op1(e10,e11) = e12
| op1(e10,e11) = e13 )
& ( op1(e10,e12) = e10
| op1(e10,e12) = e11
| op1(e10,e12) = e12
| op1(e10,e12) = e13 )
& ( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e12
| op1(e10,e13) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 )
& ( op1(e11,e11) = e10
| op1(e11,e11) = e11
| op1(e11,e11) = e12
| op1(e11,e11) = e13 )
& ( op1(e11,e12) = e10
| op1(e11,e12) = e11
| op1(e11,e12) = e12
| op1(e11,e12) = e13 )
& ( op1(e11,e13) = e10
| op1(e11,e13) = e11
| op1(e11,e13) = e12
| op1(e11,e13) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e10) = e11
| op1(e12,e10) = e12
| op1(e12,e10) = e13 )
& ( op1(e12,e11) = e10
| op1(e12,e11) = e11
| op1(e12,e11) = e12
| op1(e12,e11) = e13 )
& ( op1(e12,e12) = e10
| op1(e12,e12) = e11
| op1(e12,e12) = e12
| op1(e12,e12) = e13 )
& ( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12
| op1(e12,e13) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e10) = e11
| op1(e13,e10) = e12
| op1(e13,e10) = e13 )
& ( op1(e13,e11) = e10
| op1(e13,e11) = e11
| op1(e13,e11) = e12
| op1(e13,e11) = e13 )
& ( op1(e13,e12) = e10
| op1(e13,e12) = e11
| op1(e13,e12) = e12
| op1(e13,e12) = e13 )
& ( op1(e13,e13) = e10
| op1(e13,e13) = e11
| op1(e13,e13) = e12
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( op1(unit1,e10) = e10
& op1(e10,unit1) = e10
& op1(unit1,e11) = e11
& op1(e11,unit1) = e11
& op1(unit1,e12) = e12
& op1(e12,unit1) = e12
& op1(unit1,e13) = e13
& op1(e13,unit1) = e13
& ( unit1 = e10
| unit1 = e11
| unit1 = e12
| unit1 = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,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',ax3) ).
fof(f5,axiom,
( op2(unit2,e20) = e20
& op2(e20,unit2) = e20
& op2(unit2,e21) = e21
& op2(e21,unit2) = e21
& op2(unit2,e22) = e22
& op2(e22,unit2) = e22
& op2(unit2,e23) = e23
& op2(e23,unit2) = e23
& ( unit2 = e20
| unit2 = e21
| unit2 = e22
| unit2 = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,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',ax6) ).
fof(f7,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',ax7) ).
fof(f8,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',ax8) ).
fof(f9,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax9) ).
fof(f10,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f14,axiom,
( e10 = op1(e11,op1(e11,op1(e11,e11)))
& e12 = op1(e11,op1(e11,e11))
& e13 = op1(e11,e11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
( e20 = op2(e21,op2(e21,op2(e21,e21)))
& e22 = op2(e21,op2(e21,e21))
& e23 = op2(e21,e21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
fof(f17,axiom,
( h2(e11) = e21
& h2(e10) = op2(e21,op2(e21,op2(e21,e21)))
& h2(e12) = op2(e21,op2(e21,e21))
& h2(e13) = op2(e21,e21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f19,axiom,
( h4(e11) = e23
& h4(e10) = op2(e23,op2(e23,op2(e23,e23)))
& h4(e12) = op2(e23,op2(e23,e23))
& h4(e13) = op2(e23,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax19) ).
fof(f20,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(f21,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)],[f20]) ).
fof(f24,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,[],[f21]) ).
fof(f34,plain,
( e13 = op1(e12,e11)
| e12 = op1(e12,e11)
| e11 = op1(e12,e11)
| e10 = op1(e12,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f36,plain,
( e13 = op1(e12,e13)
| e12 = op1(e12,e13)
| e11 = op1(e12,e13)
| e10 = op1(e12,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f39,plain,
( e13 = op1(e13,e12)
| e12 = op1(e13,e12)
| e11 = op1(e13,e12)
| e10 = op1(e13,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f41,plain,
( e13 = unit1
| e12 = unit1
| e11 = unit1
| e10 = unit1 ),
inference(cnf_transformation,[],[f2]) ).
fof(f42,plain,
e13 = op1(e13,unit1),
inference(cnf_transformation,[],[f2]) ).
fof(f43,plain,
e13 = op1(unit1,e13),
inference(cnf_transformation,[],[f2]) ).
fof(f44,plain,
e12 = op1(e12,unit1),
inference(cnf_transformation,[],[f2]) ).
fof(f45,plain,
e12 = op1(unit1,e12),
inference(cnf_transformation,[],[f2]) ).
fof(f46,plain,
e11 = op1(e11,unit1),
inference(cnf_transformation,[],[f2]) ).
fof(f47,plain,
e11 = op1(unit1,e11),
inference(cnf_transformation,[],[f2]) ).
fof(f48,plain,
e10 = op1(e10,unit1),
inference(cnf_transformation,[],[f2]) ).
fof(f49,plain,
e10 = op1(unit1,e10),
inference(cnf_transformation,[],[f2]) ).
fof(f53,plain,
( e11 = op1(e13,e10)
| e11 = op1(e12,e10)
| e11 = op1(e11,e10)
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[],[f3]) ).
fof(f55,plain,
( e12 = op1(e13,e10)
| e12 = op1(e12,e10)
| e12 = op1(e11,e10)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f3]) ).
fof(f57,plain,
( e13 = op1(e13,e10)
| e13 = op1(e12,e10)
| e13 = op1(e11,e10)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f3]) ).
fof(f58,plain,
( e10 = op1(e11,e13)
| e10 = op1(e11,e12)
| e10 = op1(e11,e11)
| e10 = op1(e11,e10) ),
inference(cnf_transformation,[],[f3]) ).
fof(f63,plain,
( e12 = op1(e13,e11)
| e12 = op1(e12,e11)
| e12 = op1(e11,e11)
| e12 = op1(e10,e11) ),
inference(cnf_transformation,[],[f3]) ).
fof(f73,plain,
( e13 = op1(e13,e12)
| e13 = op1(e12,e12)
| e13 = op1(e11,e12)
| e13 = op1(e10,e12) ),
inference(cnf_transformation,[],[f3]) ).
fof(f75,plain,
( e10 = op1(e13,e13)
| e10 = op1(e12,e13)
| e10 = op1(e11,e13)
| e10 = op1(e10,e13) ),
inference(cnf_transformation,[],[f3]) ).
fof(f98,plain,
( e23 = unit2
| e22 = unit2
| e21 = unit2
| e20 = unit2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f99,plain,
e23 = op2(e23,unit2),
inference(cnf_transformation,[],[f5]) ).
fof(f100,plain,
e23 = op2(unit2,e23),
inference(cnf_transformation,[],[f5]) ).
fof(f101,plain,
e22 = op2(e22,unit2),
inference(cnf_transformation,[],[f5]) ).
fof(f102,plain,
e22 = op2(unit2,e22),
inference(cnf_transformation,[],[f5]) ).
fof(f103,plain,
e21 = op2(e21,unit2),
inference(cnf_transformation,[],[f5]) ).
fof(f104,plain,
e21 = op2(unit2,e21),
inference(cnf_transformation,[],[f5]) ).
fof(f105,plain,
e20 = op2(e20,unit2),
inference(cnf_transformation,[],[f5]) ).
fof(f106,plain,
e20 = op2(unit2,e20),
inference(cnf_transformation,[],[f5]) ).
fof(f115,plain,
( e20 = op2(e21,e23)
| e20 = op2(e21,e22)
| e20 = op2(e21,e21)
| e20 = op2(e21,e20) ),
inference(cnf_transformation,[],[f6]) ).
fof(f116,plain,
( e20 = op2(e23,e21)
| e20 = op2(e22,e21)
| e20 = op2(e21,e21)
| e20 = op2(e20,e21) ),
inference(cnf_transformation,[],[f6]) ).
fof(f125,plain,
( e21 = op2(e22,e23)
| e21 = op2(e22,e22)
| e21 = op2(e22,e21)
| e21 = op2(e22,e20) ),
inference(cnf_transformation,[],[f6]) ).
fof(f126,plain,
( e21 = op2(e23,e22)
| e21 = op2(e22,e22)
| e21 = op2(e21,e22)
| e21 = op2(e20,e22) ),
inference(cnf_transformation,[],[f6]) ).
fof(f130,plain,
( e23 = op2(e23,e22)
| e23 = op2(e22,e22)
| e23 = op2(e21,e22)
| e23 = op2(e20,e22) ),
inference(cnf_transformation,[],[f6]) ).
fof(f131,plain,
( e20 = op2(e23,e23)
| e20 = op2(e23,e22)
| e20 = op2(e23,e21)
| e20 = op2(e23,e20) ),
inference(cnf_transformation,[],[f6]) ).
fof(f135,plain,
( e22 = op2(e23,e23)
| e22 = op2(e23,e22)
| e22 = op2(e23,e21)
| e22 = op2(e23,e20) ),
inference(cnf_transformation,[],[f6]) ).
fof(f143,plain,
op1(e13,e10) != op1(e13,e12),
inference(cnf_transformation,[],[f7]) ).
fof(f146,plain,
op1(e12,e11) != op1(e12,e13),
inference(cnf_transformation,[],[f7]) ).
fof(f150,plain,
op1(e12,e10) != op1(e12,e11),
inference(cnf_transformation,[],[f7]) ).
fof(f153,plain,
op1(e11,e11) != op1(e11,e12),
inference(cnf_transformation,[],[f7]) ).
fof(f156,plain,
op1(e11,e10) != op1(e11,e11),
inference(cnf_transformation,[],[f7]) ).
fof(f165,plain,
op1(e11,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f7]) ).
fof(f167,plain,
op1(e10,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f7]) ).
fof(f170,plain,
op1(e11,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f7]) ).
fof(f172,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f7]) ).
fof(f174,plain,
op1(e10,e12) != op1(e11,e12),
inference(cnf_transformation,[],[f7]) ).
fof(f177,plain,
op1(e11,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f7]) ).
fof(f179,plain,
op1(e10,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f7]) ).
fof(f191,plain,
op2(e23,e20) != op2(e23,e22),
inference(cnf_transformation,[],[f8]) ).
fof(f200,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f8]) ).
fof(f201,plain,
op2(e21,e21) != op2(e21,e22),
inference(cnf_transformation,[],[f8]) ).
fof(f212,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f8]) ).
fof(f218,plain,
op2(e21,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f8]) ).
fof(f222,plain,
op2(e20,e22) != op2(e21,e22),
inference(cnf_transformation,[],[f8]) ).
fof(f227,plain,
op2(e20,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f8]) ).
fof(f231,plain,
op2(e21,e20) != op2(e22,e20),
inference(cnf_transformation,[],[f8]) ).
fof(f235,plain,
e12 != e13,
inference(cnf_transformation,[],[f9]) ).
fof(f236,plain,
e11 != e13,
inference(cnf_transformation,[],[f9]) ).
fof(f237,plain,
e11 != e12,
inference(cnf_transformation,[],[f9]) ).
fof(f238,plain,
e10 != e13,
inference(cnf_transformation,[],[f9]) ).
fof(f239,plain,
e10 != e12,
inference(cnf_transformation,[],[f9]) ).
fof(f240,plain,
e10 != e11,
inference(cnf_transformation,[],[f9]) ).
fof(f241,plain,
e22 != e23,
inference(cnf_transformation,[],[f10]) ).
fof(f242,plain,
e21 != e23,
inference(cnf_transformation,[],[f10]) ).
fof(f243,plain,
e21 != e22,
inference(cnf_transformation,[],[f10]) ).
fof(f244,plain,
e20 != e23,
inference(cnf_transformation,[],[f10]) ).
fof(f245,plain,
e20 != e22,
inference(cnf_transformation,[],[f10]) ).
fof(f246,plain,
e20 != e21,
inference(cnf_transformation,[],[f10]) ).
fof(f271,plain,
e13 = op1(e11,e11),
inference(cnf_transformation,[],[f14]) ).
fof(f272,plain,
e12 = op1(e11,op1(e11,e11)),
inference(cnf_transformation,[],[f14]) ).
fof(f274,plain,
e23 = op2(e21,e21),
inference(cnf_transformation,[],[f15]) ).
fof(f275,plain,
e22 = op2(e21,op2(e21,e21)),
inference(cnf_transformation,[],[f15]) ).
fof(f281,plain,
op2(e21,e21) = h2(e13),
inference(cnf_transformation,[],[f17]) ).
fof(f282,plain,
op2(e21,op2(e21,e21)) = h2(e12),
inference(cnf_transformation,[],[f17]) ).
fof(f283,plain,
op2(e21,op2(e21,op2(e21,e21))) = h2(e10),
inference(cnf_transformation,[],[f17]) ).
fof(f284,plain,
e21 = h2(e11),
inference(cnf_transformation,[],[f17]) ).
fof(f292,plain,
e23 = h4(e11),
inference(cnf_transformation,[],[f19]) ).
fof(f304,plain,
( e20 != h2(e10)
| ~ sP5 ),
inference(cnf_transformation,[],[f24]) ).
fof(f307,plain,
( e21 != h2(e11)
| ~ sP4 ),
inference(cnf_transformation,[],[f24]) ).
fof(f354,plain,
( e23 != h2(e13)
| e22 != h2(e12)
| 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,[],[f24]) ).
fof(f458,definition,
( spl8_11
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl8_11])],[avatar_definition]) ).
fof(f477,definition,
( spl8_15
<=> e20 = h2(e10) ),
introduced(definition,[new_symbols(definition,[spl8_15])],[avatar_definition]) ).
fof(f478,plain,
( e20 = h2(e10)
| ~ spl8_15 ),
inference(avatar_component_clause,[],[f477]) ).
fof(f480,plain,
( ~ spl8_11
| ~ spl8_15 ),
inference(avatar_split_clause,[],[f304,f477,f458]) ).
fof(f482,definition,
( spl8_16
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl8_16])],[avatar_definition]) ).
fof(f496,definition,
( spl8_19
<=> e21 = h2(e11) ),
introduced(definition,[new_symbols(definition,[spl8_19])],[avatar_definition]) ).
fof(f497,plain,
( e21 = h2(e11)
| ~ spl8_19 ),
inference(avatar_component_clause,[],[f496]) ).
fof(f499,plain,
( ~ spl8_16
| ~ spl8_19 ),
inference(avatar_split_clause,[],[f307,f496,f482]) ).
fof(f568,definition,
( spl8_34
<=> e20 = h4(e11) ),
introduced(definition,[new_symbols(definition,[spl8_34])],[avatar_definition]) ).
fof(f569,plain,
( e20 = h4(e11)
| ~ spl8_34 ),
inference(avatar_component_clause,[],[f568]) ).
fof(f570,plain,
( e20 != h4(e11)
| spl8_34 ),
inference(avatar_component_clause,[],[f568]) ).
fof(f714,definition,
( spl8_65
<=> h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_65])],[avatar_definition]) ).
fof(f716,plain,
( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| spl8_65 ),
inference(avatar_component_clause,[],[f714]) ).
fof(f718,definition,
( spl8_66
<=> h2(op1(e10,e11)) = op2(h2(e10),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_66])],[avatar_definition]) ).
fof(f720,plain,
( h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| spl8_66 ),
inference(avatar_component_clause,[],[f718]) ).
fof(f722,definition,
( spl8_67
<=> h2(op1(e10,e12)) = op2(h2(e10),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_67])],[avatar_definition]) ).
fof(f724,plain,
( h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| spl8_67 ),
inference(avatar_component_clause,[],[f722]) ).
fof(f726,definition,
( spl8_68
<=> h2(op1(e10,e13)) = op2(h2(e10),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_68])],[avatar_definition]) ).
fof(f728,plain,
( h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| spl8_68 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f730,definition,
( spl8_69
<=> h2(op1(e11,e10)) = op2(h2(e11),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_69])],[avatar_definition]) ).
fof(f732,plain,
( h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| spl8_69 ),
inference(avatar_component_clause,[],[f730]) ).
fof(f734,definition,
( spl8_70
<=> h2(op1(e11,e11)) = op2(h2(e11),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_70])],[avatar_definition]) ).
fof(f736,plain,
( h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| spl8_70 ),
inference(avatar_component_clause,[],[f734]) ).
fof(f738,definition,
( spl8_71
<=> h2(op1(e11,e12)) = op2(h2(e11),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_71])],[avatar_definition]) ).
fof(f740,plain,
( h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| spl8_71 ),
inference(avatar_component_clause,[],[f738]) ).
fof(f742,definition,
( spl8_72
<=> h2(op1(e11,e13)) = op2(h2(e11),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_72])],[avatar_definition]) ).
fof(f744,plain,
( h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| spl8_72 ),
inference(avatar_component_clause,[],[f742]) ).
fof(f746,definition,
( spl8_73
<=> h2(op1(e12,e10)) = op2(h2(e12),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_73])],[avatar_definition]) ).
fof(f748,plain,
( h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| spl8_73 ),
inference(avatar_component_clause,[],[f746]) ).
fof(f750,definition,
( spl8_74
<=> h2(op1(e12,e11)) = op2(h2(e12),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_74])],[avatar_definition]) ).
fof(f752,plain,
( h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| spl8_74 ),
inference(avatar_component_clause,[],[f750]) ).
fof(f754,definition,
( spl8_75
<=> h2(op1(e12,e12)) = op2(h2(e12),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_75])],[avatar_definition]) ).
fof(f756,plain,
( h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| spl8_75 ),
inference(avatar_component_clause,[],[f754]) ).
fof(f758,definition,
( spl8_76
<=> h2(op1(e12,e13)) = op2(h2(e12),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_76])],[avatar_definition]) ).
fof(f760,plain,
( h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| spl8_76 ),
inference(avatar_component_clause,[],[f758]) ).
fof(f762,definition,
( spl8_77
<=> h2(op1(e13,e10)) = op2(h2(e13),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_77])],[avatar_definition]) ).
fof(f764,plain,
( h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| spl8_77 ),
inference(avatar_component_clause,[],[f762]) ).
fof(f766,definition,
( spl8_78
<=> h2(op1(e13,e11)) = op2(h2(e13),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_78])],[avatar_definition]) ).
fof(f768,plain,
( h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| spl8_78 ),
inference(avatar_component_clause,[],[f766]) ).
fof(f770,definition,
( spl8_79
<=> h2(op1(e13,e12)) = op2(h2(e13),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_79])],[avatar_definition]) ).
fof(f772,plain,
( h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| spl8_79 ),
inference(avatar_component_clause,[],[f770]) ).
fof(f774,definition,
( spl8_80
<=> h2(op1(e13,e13)) = op2(h2(e13),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_80])],[avatar_definition]) ).
fof(f776,plain,
( h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| spl8_80 ),
inference(avatar_component_clause,[],[f774]) ).
fof(f787,definition,
( spl8_83
<=> e22 = h2(e12) ),
introduced(definition,[new_symbols(definition,[spl8_83])],[avatar_definition]) ).
fof(f788,plain,
( e22 = h2(e12)
| ~ spl8_83 ),
inference(avatar_component_clause,[],[f787]) ).
fof(f818,definition,
( spl8_88
<=> e23 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl8_88])],[avatar_definition]) ).
fof(f819,plain,
( e23 = h2(e13)
| ~ spl8_88 ),
inference(avatar_component_clause,[],[f818]) ).
fof(f822,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_83
| ~ spl8_88 ),
inference(avatar_split_clause,[],[f354,f818,f787,f482,f458,f774,f770,f766,f762,f758,f754,f750,f746,f742,f738,f734,f730,f726,f722,f718,f714]) ).
fof(f1026,definition,
( spl8_134
<=> e23 = h4(e11) ),
introduced(definition,[new_symbols(definition,[spl8_134])],[avatar_definition]) ).
fof(f1027,plain,
( e23 = h4(e11)
| ~ spl8_134 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1049,plain,
spl8_134,
inference(avatar_split_clause,[],[f292,f1026]) ).
fof(f1051,plain,
spl8_19,
inference(avatar_split_clause,[],[f284,f496]) ).
fof(f1054,definition,
( spl8_137
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl8_137])],[avatar_definition]) ).
fof(f1055,plain,
( e20 = op2(e20,e20)
| ~ spl8_137 ),
inference(avatar_component_clause,[],[f1054]) ).
fof(f1058,definition,
( spl8_138
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_138])],[avatar_definition]) ).
fof(f1059,plain,
( e20 = op2(e21,e21)
| ~ spl8_138 ),
inference(avatar_component_clause,[],[f1058]) ).
fof(f1066,definition,
( spl8_140
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl8_140])],[avatar_definition]) ).
fof(f1067,plain,
( e20 = op2(e23,e23)
| ~ spl8_140 ),
inference(avatar_component_clause,[],[f1066]) ).
fof(f1079,definition,
( spl8_143
<=> e21 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl8_143])],[avatar_definition]) ).
fof(f1080,plain,
( e21 = op2(e22,e22)
| ~ spl8_143 ),
inference(avatar_component_clause,[],[f1079]) ).
fof(f1100,definition,
( spl8_148
<=> e22 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl8_148])],[avatar_definition]) ).
fof(f1101,plain,
( e22 = op2(e23,e23)
| ~ spl8_148 ),
inference(avatar_component_clause,[],[f1100]) ).
fof(f1109,definition,
( spl8_150
<=> e23 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_150])],[avatar_definition]) ).
fof(f1110,plain,
( e23 = op2(e21,e21)
| ~ spl8_150 ),
inference(avatar_component_clause,[],[f1109]) ).
fof(f1113,definition,
( spl8_151
<=> e23 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl8_151])],[avatar_definition]) ).
fof(f1114,plain,
( e23 = op2(e22,e22)
| ~ spl8_151 ),
inference(avatar_component_clause,[],[f1113]) ).
fof(f1122,definition,
( spl8_153
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl8_153])],[avatar_definition]) ).
fof(f1123,plain,
( e10 = op1(e10,e10)
| ~ spl8_153 ),
inference(avatar_component_clause,[],[f1122]) ).
fof(f1126,definition,
( spl8_154
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_154])],[avatar_definition]) ).
fof(f1127,plain,
( e10 = op1(e11,e11)
| ~ spl8_154 ),
inference(avatar_component_clause,[],[f1126]) ).
fof(f1134,definition,
( spl8_156
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_156])],[avatar_definition]) ).
fof(f1135,plain,
( e10 = op1(e13,e13)
| ~ spl8_156 ),
inference(avatar_component_clause,[],[f1134]) ).
fof(f1139,definition,
( spl8_157
<=> op1(e10,e10) = e11 ),
introduced(definition,[new_symbols(definition,[spl8_157])],[avatar_definition]) ).
fof(f1140,plain,
( op1(e10,e10) = e11
| ~ spl8_157 ),
inference(avatar_component_clause,[],[f1139]) ).
fof(f1143,definition,
( spl8_158
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_158])],[avatar_definition]) ).
fof(f1144,plain,
( e11 = op1(e11,e11)
| ~ spl8_158 ),
inference(avatar_component_clause,[],[f1143]) ).
fof(f1156,definition,
( spl8_161
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[spl8_161])],[avatar_definition]) ).
fof(f1157,plain,
( op1(e10,e10) = e12
| ~ spl8_161 ),
inference(avatar_component_clause,[],[f1156]) ).
fof(f1160,definition,
( spl8_162
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_162])],[avatar_definition]) ).
fof(f1161,plain,
( e12 = op1(e11,e11)
| ~ spl8_162 ),
inference(avatar_component_clause,[],[f1160]) ).
fof(f1173,definition,
( spl8_165
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl8_165])],[avatar_definition]) ).
fof(f1174,plain,
( op1(e10,e10) = e13
| ~ spl8_165 ),
inference(avatar_component_clause,[],[f1173]) ).
fof(f1177,definition,
( spl8_166
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_166])],[avatar_definition]) ).
fof(f1178,plain,
( e13 = op1(e11,e11)
| ~ spl8_166 ),
inference(avatar_component_clause,[],[f1177]) ).
fof(f1181,definition,
( spl8_167
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl8_167])],[avatar_definition]) ).
fof(f1182,plain,
( e13 = op1(e12,e12)
| ~ spl8_167 ),
inference(avatar_component_clause,[],[f1181]) ).
fof(f1190,definition,
( spl8_169
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl8_169])],[avatar_definition]) ).
fof(f1192,plain,
( e20 = op2(e20,e21)
| ~ spl8_169 ),
inference(avatar_component_clause,[],[f1190]) ).
fof(f1194,definition,
( spl8_170
<=> e20 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_170])],[avatar_definition]) ).
fof(f1196,plain,
( e20 = op2(e20,e22)
| ~ spl8_170 ),
inference(avatar_component_clause,[],[f1194]) ).
fof(f1203,definition,
( spl8_172
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl8_172])],[avatar_definition]) ).
fof(f1205,plain,
( e20 = op2(e21,e20)
| ~ spl8_172 ),
inference(avatar_component_clause,[],[f1203]) ).
fof(f1207,definition,
( spl8_173
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_173])],[avatar_definition]) ).
fof(f1209,plain,
( e20 = op2(e22,e20)
| ~ spl8_173 ),
inference(avatar_component_clause,[],[f1207]) ).
fof(f1211,definition,
( spl8_174
<=> e20 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_174])],[avatar_definition]) ).
fof(f1213,plain,
( e20 = op2(e23,e20)
| ~ spl8_174 ),
inference(avatar_component_clause,[],[f1211]) ).
fof(f1216,definition,
( spl8_175
<=> e21 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl8_175])],[avatar_definition]) ).
fof(f1218,plain,
( e21 = op2(e20,e21)
| ~ spl8_175 ),
inference(avatar_component_clause,[],[f1216]) ).
fof(f1220,definition,
( spl8_176
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_176])],[avatar_definition]) ).
fof(f1222,plain,
( e21 = op2(e20,e22)
| ~ spl8_176 ),
inference(avatar_component_clause,[],[f1220]) ).
fof(f1229,definition,
( spl8_178
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl8_178])],[avatar_definition]) ).
fof(f1231,plain,
( e21 = op2(e21,e20)
| ~ spl8_178 ),
inference(avatar_component_clause,[],[f1229]) ).
fof(f1233,definition,
( spl8_179
<=> e21 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_179])],[avatar_definition]) ).
fof(f1235,plain,
( e21 = op2(e22,e20)
| ~ spl8_179 ),
inference(avatar_component_clause,[],[f1233]) ).
fof(f1246,definition,
( spl8_182
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_182])],[avatar_definition]) ).
fof(f1248,plain,
( e22 = op2(e20,e22)
| ~ spl8_182 ),
inference(avatar_component_clause,[],[f1246]) ).
fof(f1259,definition,
( spl8_185
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_185])],[avatar_definition]) ).
fof(f1261,plain,
( e22 = op2(e22,e20)
| ~ spl8_185 ),
inference(avatar_component_clause,[],[f1259]) ).
fof(f1263,definition,
( spl8_186
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_186])],[avatar_definition]) ).
fof(f1265,plain,
( e22 = op2(e23,e20)
| ~ spl8_186 ),
inference(avatar_component_clause,[],[f1263]) ).
fof(f1272,definition,
( spl8_188
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_188])],[avatar_definition]) ).
fof(f1274,plain,
( e23 = op2(e20,e22)
| ~ spl8_188 ),
inference(avatar_component_clause,[],[f1272]) ).
fof(f1276,definition,
( spl8_189
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl8_189])],[avatar_definition]) ).
fof(f1278,plain,
( e23 = op2(e20,e23)
| ~ spl8_189 ),
inference(avatar_component_clause,[],[f1276]) ).
fof(f1289,definition,
( spl8_192
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_192])],[avatar_definition]) ).
fof(f1291,plain,
( e23 = op2(e23,e20)
| ~ spl8_192 ),
inference(avatar_component_clause,[],[f1289]) ).
fof(f1294,definition,
( spl8_193
<=> e20 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl8_193])],[avatar_definition]) ).
fof(f1296,plain,
( e20 = op2(e21,e22)
| ~ spl8_193 ),
inference(avatar_component_clause,[],[f1294]) ).
fof(f1298,definition,
( spl8_194
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_194])],[avatar_definition]) ).
fof(f1300,plain,
( e20 = op2(e21,e23)
| ~ spl8_194 ),
inference(avatar_component_clause,[],[f1298]) ).
fof(f1301,plain,
( spl8_172
| spl8_138
| spl8_193
| spl8_194 ),
inference(avatar_split_clause,[],[f115,f1298,f1294,f1058,f1203]) ).
fof(f1303,definition,
( spl8_195
<=> e20 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl8_195])],[avatar_definition]) ).
fof(f1305,plain,
( e20 = op2(e22,e21)
| ~ spl8_195 ),
inference(avatar_component_clause,[],[f1303]) ).
fof(f1307,definition,
( spl8_196
<=> e20 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl8_196])],[avatar_definition]) ).
fof(f1309,plain,
( e20 = op2(e23,e21)
| ~ spl8_196 ),
inference(avatar_component_clause,[],[f1307]) ).
fof(f1310,plain,
( spl8_169
| spl8_138
| spl8_195
| spl8_196 ),
inference(avatar_split_clause,[],[f116,f1307,f1303,f1058,f1190]) ).
fof(f1312,definition,
( spl8_197
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl8_197])],[avatar_definition]) ).
fof(f1314,plain,
( e21 = op2(e21,e22)
| ~ spl8_197 ),
inference(avatar_component_clause,[],[f1312]) ).
fof(f1316,definition,
( spl8_198
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_198])],[avatar_definition]) ).
fof(f1318,plain,
( e21 = op2(e21,e23)
| ~ spl8_198 ),
inference(avatar_component_clause,[],[f1316]) ).
fof(f1321,definition,
( spl8_199
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl8_199])],[avatar_definition]) ).
fof(f1323,plain,
( e21 = op2(e22,e21)
| ~ spl8_199 ),
inference(avatar_component_clause,[],[f1321]) ).
fof(f1334,definition,
( spl8_202
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_202])],[avatar_definition]) ).
fof(f1336,plain,
( e22 = op2(e21,e23)
| ~ spl8_202 ),
inference(avatar_component_clause,[],[f1334]) ).
fof(f1343,definition,
( spl8_204
<=> e22 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl8_204])],[avatar_definition]) ).
fof(f1345,plain,
( e22 = op2(e23,e21)
| ~ spl8_204 ),
inference(avatar_component_clause,[],[f1343]) ).
fof(f1348,definition,
( spl8_205
<=> e23 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl8_205])],[avatar_definition]) ).
fof(f1352,definition,
( spl8_206
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_206])],[avatar_definition]) ).
fof(f1371,definition,
( spl8_210
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_210])],[avatar_definition]) ).
fof(f1376,definition,
( spl8_211
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl8_211])],[avatar_definition]) ).
fof(f1379,plain,
( spl8_179
| spl8_199
| spl8_143
| spl8_211 ),
inference(avatar_split_clause,[],[f125,f1376,f1079,f1321,f1233]) ).
fof(f1381,definition,
( spl8_212
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_212])],[avatar_definition]) ).
fof(f1383,plain,
( e21 = op2(e23,e22)
| ~ spl8_212 ),
inference(avatar_component_clause,[],[f1381]) ).
fof(f1384,plain,
( spl8_176
| spl8_197
| spl8_143
| spl8_212 ),
inference(avatar_split_clause,[],[f126,f1381,f1079,f1312,f1220]) ).
fof(f1391,definition,
( spl8_214
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_214])],[avatar_definition]) ).
fof(f1393,plain,
( e22 = op2(e23,e22)
| ~ spl8_214 ),
inference(avatar_component_clause,[],[f1391]) ).
fof(f1401,definition,
( spl8_216
<=> e23 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_216])],[avatar_definition]) ).
fof(f1404,plain,
( spl8_188
| spl8_205
| spl8_151
| spl8_216 ),
inference(avatar_split_clause,[],[f130,f1401,f1113,f1348,f1272]) ).
fof(f1405,plain,
( spl8_174
| spl8_196
| spl8_210
| spl8_140 ),
inference(avatar_split_clause,[],[f131,f1066,f1371,f1307,f1211]) ).
fof(f1409,plain,
( spl8_186
| spl8_204
| spl8_214
| spl8_148 ),
inference(avatar_split_clause,[],[f135,f1100,f1391,f1343,f1263]) ).
fof(f1414,definition,
( spl8_217
<=> e20 = unit2 ),
introduced(definition,[new_symbols(definition,[spl8_217])],[avatar_definition]) ).
fof(f1416,plain,
( e20 = unit2
| ~ spl8_217 ),
inference(avatar_component_clause,[],[f1414]) ).
fof(f1418,definition,
( spl8_218
<=> e21 = unit2 ),
introduced(definition,[new_symbols(definition,[spl8_218])],[avatar_definition]) ).
fof(f1420,plain,
( e21 = unit2
| ~ spl8_218 ),
inference(avatar_component_clause,[],[f1418]) ).
fof(f1422,definition,
( spl8_219
<=> e22 = unit2 ),
introduced(definition,[new_symbols(definition,[spl8_219])],[avatar_definition]) ).
fof(f1424,plain,
( e22 = unit2
| ~ spl8_219 ),
inference(avatar_component_clause,[],[f1422]) ).
fof(f1426,definition,
( spl8_220
<=> e23 = unit2 ),
introduced(definition,[new_symbols(definition,[spl8_220])],[avatar_definition]) ).
fof(f1428,plain,
( e23 = unit2
| ~ spl8_220 ),
inference(avatar_component_clause,[],[f1426]) ).
fof(f1429,plain,
( spl8_217
| spl8_218
| spl8_219
| spl8_220 ),
inference(avatar_split_clause,[],[f98,f1426,f1422,f1418,f1414]) ).
fof(f1451,definition,
( spl8_222
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_222])],[avatar_definition]) ).
fof(f1455,definition,
( spl8_223
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl8_223])],[avatar_definition]) ).
fof(f1457,plain,
( e10 = op1(e10,e13)
| ~ spl8_223 ),
inference(avatar_component_clause,[],[f1455]) ).
fof(f1460,definition,
( spl8_224
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_224])],[avatar_definition]) ).
fof(f1462,plain,
( e10 = op1(e11,e10)
| ~ spl8_224 ),
inference(avatar_component_clause,[],[f1460]) ).
fof(f1464,definition,
( spl8_225
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl8_225])],[avatar_definition]) ).
fof(f1466,plain,
( e10 = op1(e12,e10)
| ~ spl8_225 ),
inference(avatar_component_clause,[],[f1464]) ).
fof(f1473,definition,
( spl8_227
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl8_227])],[avatar_definition]) ).
fof(f1475,plain,
( e11 = op1(e10,e11)
| ~ spl8_227 ),
inference(avatar_component_clause,[],[f1473]) ).
fof(f1486,definition,
( spl8_230
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_230])],[avatar_definition]) ).
fof(f1488,plain,
( e11 = op1(e11,e10)
| ~ spl8_230 ),
inference(avatar_component_clause,[],[f1486]) ).
fof(f1490,definition,
( spl8_231
<=> e11 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl8_231])],[avatar_definition]) ).
fof(f1492,plain,
( e11 = op1(e12,e10)
| ~ spl8_231 ),
inference(avatar_component_clause,[],[f1490]) ).
fof(f1494,definition,
( spl8_232
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_232])],[avatar_definition]) ).
fof(f1496,plain,
( e11 = op1(e13,e10)
| ~ spl8_232 ),
inference(avatar_component_clause,[],[f1494]) ).
fof(f1497,plain,
( spl8_157
| spl8_230
| spl8_231
| spl8_232 ),
inference(avatar_split_clause,[],[f53,f1494,f1490,f1486,f1139]) ).
fof(f1499,definition,
( spl8_233
<=> e12 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl8_233])],[avatar_definition]) ).
fof(f1501,plain,
( e12 = op1(e10,e11)
| ~ spl8_233 ),
inference(avatar_component_clause,[],[f1499]) ).
fof(f1503,definition,
( spl8_234
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_234])],[avatar_definition]) ).
fof(f1505,plain,
( e12 = op1(e10,e12)
| ~ spl8_234 ),
inference(avatar_component_clause,[],[f1503]) ).
fof(f1512,definition,
( spl8_236
<=> e12 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_236])],[avatar_definition]) ).
fof(f1514,plain,
( e12 = op1(e11,e10)
| ~ spl8_236 ),
inference(avatar_component_clause,[],[f1512]) ).
fof(f1516,definition,
( spl8_237
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl8_237])],[avatar_definition]) ).
fof(f1518,plain,
( e12 = op1(e12,e10)
| ~ spl8_237 ),
inference(avatar_component_clause,[],[f1516]) ).
fof(f1520,definition,
( spl8_238
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_238])],[avatar_definition]) ).
fof(f1522,plain,
( e12 = op1(e13,e10)
| ~ spl8_238 ),
inference(avatar_component_clause,[],[f1520]) ).
fof(f1523,plain,
( spl8_161
| spl8_236
| spl8_237
| spl8_238 ),
inference(avatar_split_clause,[],[f55,f1520,f1516,f1512,f1156]) ).
fof(f1529,definition,
( spl8_240
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_240])],[avatar_definition]) ).
fof(f1531,plain,
( e13 = op1(e10,e12)
| ~ spl8_240 ),
inference(avatar_component_clause,[],[f1529]) ).
fof(f1533,definition,
( spl8_241
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl8_241])],[avatar_definition]) ).
fof(f1535,plain,
( e13 = op1(e10,e13)
| ~ spl8_241 ),
inference(avatar_component_clause,[],[f1533]) ).
fof(f1538,definition,
( spl8_242
<=> e13 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_242])],[avatar_definition]) ).
fof(f1542,definition,
( spl8_243
<=> e13 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl8_243])],[avatar_definition]) ).
fof(f1544,plain,
( e13 = op1(e12,e10)
| ~ spl8_243 ),
inference(avatar_component_clause,[],[f1542]) ).
fof(f1546,definition,
( spl8_244
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_244])],[avatar_definition]) ).
fof(f1548,plain,
( e13 = op1(e13,e10)
| ~ spl8_244 ),
inference(avatar_component_clause,[],[f1546]) ).
fof(f1549,plain,
( spl8_165
| spl8_242
| spl8_243
| spl8_244 ),
inference(avatar_split_clause,[],[f57,f1546,f1542,f1538,f1173]) ).
fof(f1551,definition,
( spl8_245
<=> e10 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl8_245])],[avatar_definition]) ).
fof(f1553,plain,
( e10 = op1(e11,e12)
| ~ spl8_245 ),
inference(avatar_component_clause,[],[f1551]) ).
fof(f1555,definition,
( spl8_246
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_246])],[avatar_definition]) ).
fof(f1557,plain,
( e10 = op1(e11,e13)
| ~ spl8_246 ),
inference(avatar_component_clause,[],[f1555]) ).
fof(f1558,plain,
( spl8_224
| spl8_154
| spl8_245
| spl8_246 ),
inference(avatar_split_clause,[],[f58,f1555,f1551,f1126,f1460]) ).
fof(f1560,definition,
( spl8_247
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_247])],[avatar_definition]) ).
fof(f1562,plain,
( e10 = op1(e12,e11)
| ~ spl8_247 ),
inference(avatar_component_clause,[],[f1560]) ).
fof(f1573,definition,
( spl8_250
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_250])],[avatar_definition]) ).
fof(f1575,plain,
( e11 = op1(e11,e13)
| ~ spl8_250 ),
inference(avatar_component_clause,[],[f1573]) ).
fof(f1578,definition,
( spl8_251
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_251])],[avatar_definition]) ).
fof(f1591,definition,
( spl8_254
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_254])],[avatar_definition]) ).
fof(f1593,plain,
( e12 = op1(e11,e13)
| ~ spl8_254 ),
inference(avatar_component_clause,[],[f1591]) ).
fof(f1596,definition,
( spl8_255
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_255])],[avatar_definition]) ).
fof(f1600,definition,
( spl8_256
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_256])],[avatar_definition]) ).
fof(f1602,plain,
( e12 = op1(e13,e11)
| ~ spl8_256 ),
inference(avatar_component_clause,[],[f1600]) ).
fof(f1603,plain,
( spl8_233
| spl8_162
| spl8_255
| spl8_256 ),
inference(avatar_split_clause,[],[f63,f1600,f1596,f1160,f1499]) ).
fof(f1605,definition,
( spl8_257
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl8_257])],[avatar_definition]) ).
fof(f1614,definition,
( spl8_259
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_259])],[avatar_definition]) ).
fof(f1623,definition,
( spl8_261
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl8_261])],[avatar_definition]) ).
fof(f1628,definition,
( spl8_262
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_262])],[avatar_definition]) ).
fof(f1633,definition,
( spl8_263
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl8_263])],[avatar_definition]) ).
fof(f1635,plain,
( e11 = op1(e12,e13)
| ~ spl8_263 ),
inference(avatar_component_clause,[],[f1633]) ).
fof(f1638,definition,
( spl8_264
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_264])],[avatar_definition]) ).
fof(f1640,plain,
( e11 = op1(e13,e12)
| ~ spl8_264 ),
inference(avatar_component_clause,[],[f1638]) ).
fof(f1643,definition,
( spl8_265
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl8_265])],[avatar_definition]) ).
fof(f1648,definition,
( spl8_266
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_266])],[avatar_definition]) ).
fof(f1653,definition,
( spl8_267
<=> e13 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl8_267])],[avatar_definition]) ).
fof(f1658,definition,
( spl8_268
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_268])],[avatar_definition]) ).
fof(f1661,plain,
( spl8_240
| spl8_257
| spl8_167
| spl8_268 ),
inference(avatar_split_clause,[],[f73,f1658,f1181,f1605,f1529]) ).
fof(f1663,plain,
( spl8_223
| spl8_246
| spl8_261
| spl8_156 ),
inference(avatar_split_clause,[],[f75,f1134,f1623,f1555,f1455]) ).
fof(f1671,definition,
( spl8_269
<=> e10 = unit1 ),
introduced(definition,[new_symbols(definition,[spl8_269])],[avatar_definition]) ).
fof(f1673,plain,
( e10 = unit1
| ~ spl8_269 ),
inference(avatar_component_clause,[],[f1671]) ).
fof(f1675,definition,
( spl8_270
<=> e11 = unit1 ),
introduced(definition,[new_symbols(definition,[spl8_270])],[avatar_definition]) ).
fof(f1677,plain,
( e11 = unit1
| ~ spl8_270 ),
inference(avatar_component_clause,[],[f1675]) ).
fof(f1679,definition,
( spl8_271
<=> e12 = unit1 ),
introduced(definition,[new_symbols(definition,[spl8_271])],[avatar_definition]) ).
fof(f1681,plain,
( e12 = unit1
| ~ spl8_271 ),
inference(avatar_component_clause,[],[f1679]) ).
fof(f1683,definition,
( spl8_272
<=> e13 = unit1 ),
introduced(definition,[new_symbols(definition,[spl8_272])],[avatar_definition]) ).
fof(f1685,plain,
( e13 = unit1
| ~ spl8_272 ),
inference(avatar_component_clause,[],[f1683]) ).
fof(f1686,plain,
( spl8_269
| spl8_270
| spl8_271
| spl8_272 ),
inference(avatar_split_clause,[],[f41,f1683,f1679,f1675,f1671]) ).
fof(f1696,plain,
( spl8_247
| spl8_251
| spl8_255
| spl8_259 ),
inference(avatar_split_clause,[],[f34,f1614,f1596,f1578,f1560]) ).
fof(f1698,plain,
( spl8_261
| spl8_263
| spl8_265
| spl8_267 ),
inference(avatar_split_clause,[],[f36,f1653,f1643,f1633,f1623]) ).
fof(f1701,plain,
( spl8_262
| spl8_264
| spl8_266
| spl8_268 ),
inference(avatar_split_clause,[],[f39,f1658,f1648,f1638,f1628]) ).
fof(f1705,plain,
( h2(op1(e12,e11)) != op2(h2(e12),e21)
| ~ spl8_19
| spl8_74 ),
inference(forward_demodulation,[],[f752,f497]) ).
fof(f1706,plain,
( e13 = op1(e13,e10)
| ~ spl8_269 ),
inference(forward_demodulation,[],[f42,f1673]) ).
fof(f1707,plain,
( spl8_244
| ~ spl8_269 ),
inference(avatar_split_clause,[],[f1706,f1671,f1546]) ).
fof(f1716,plain,
( e13 = op1(e13,e12)
| ~ spl8_271 ),
inference(forward_demodulation,[],[f42,f1681]) ).
fof(f1717,plain,
( spl8_268
| ~ spl8_271 ),
inference(avatar_split_clause,[],[f1716,f1679,f1658]) ).
fof(f1743,plain,
( e11 = op1(e11,e13)
| ~ spl8_272 ),
inference(forward_demodulation,[],[f46,f1685]) ).
fof(f1744,plain,
( spl8_250
| ~ spl8_272 ),
inference(avatar_split_clause,[],[f1743,f1683,f1573]) ).
fof(f1755,plain,
( e11 = op1(e11,e11)
| ~ spl8_270 ),
inference(forward_demodulation,[],[f46,f1677]) ).
fof(f1756,plain,
( spl8_158
| ~ spl8_270 ),
inference(avatar_split_clause,[],[f1755,f1675,f1143]) ).
fof(f1762,plain,
( e23 = op2(e23,e20)
| ~ spl8_217 ),
inference(forward_demodulation,[],[f99,f1416]) ).
fof(f1763,plain,
( spl8_192
| ~ spl8_217 ),
inference(avatar_split_clause,[],[f1762,f1414,f1289]) ).
fof(f1767,plain,
( e23 = op2(e21,e23)
| ~ spl8_218 ),
inference(forward_demodulation,[],[f100,f1420]) ).
fof(f1768,plain,
( spl8_206
| ~ spl8_218 ),
inference(avatar_split_clause,[],[f1767,f1418,f1352]) ).
fof(f1783,plain,
( e21 = op2(e21,e23)
| ~ spl8_220 ),
inference(forward_demodulation,[],[f103,f1428]) ).
fof(f1784,plain,
( spl8_198
| ~ spl8_220 ),
inference(avatar_split_clause,[],[f1783,f1426,f1316]) ).
fof(f1800,plain,
( e23 = op2(e20,e23)
| ~ spl8_217 ),
inference(forward_demodulation,[],[f100,f1416]) ).
fof(f1801,plain,
( spl8_189
| ~ spl8_217 ),
inference(avatar_split_clause,[],[f1800,f1414,f1276]) ).
fof(f1802,plain,
( e22 = op2(e22,e20)
| ~ spl8_217 ),
inference(forward_demodulation,[],[f101,f1416]) ).
fof(f1803,plain,
( spl8_185
| ~ spl8_217 ),
inference(avatar_split_clause,[],[f1802,f1414,f1259]) ).
fof(f1804,plain,
( e22 = op2(e20,e22)
| ~ spl8_217 ),
inference(forward_demodulation,[],[f102,f1416]) ).
fof(f1805,plain,
( spl8_182
| ~ spl8_217 ),
inference(avatar_split_clause,[],[f1804,f1414,f1246]) ).
fof(f1806,plain,
( e21 = op2(e21,e20)
| ~ spl8_217 ),
inference(forward_demodulation,[],[f103,f1416]) ).
fof(f1807,plain,
( spl8_178
| ~ spl8_217 ),
inference(avatar_split_clause,[],[f1806,f1414,f1229]) ).
fof(f1808,plain,
( e21 = op2(e20,e21)
| ~ spl8_217 ),
inference(forward_demodulation,[],[f104,f1416]) ).
fof(f1809,plain,
( spl8_175
| ~ spl8_217 ),
inference(avatar_split_clause,[],[f1808,f1414,f1216]) ).
fof(f1810,plain,
( e20 = op2(e20,e20)
| ~ spl8_217 ),
inference(forward_demodulation,[],[f105,f1416]) ).
fof(f1811,plain,
( spl8_137
| ~ spl8_217 ),
inference(avatar_split_clause,[],[f1810,f1414,f1054]) ).
fof(f1813,plain,
spl8_166,
inference(avatar_split_clause,[],[f271,f1177]) ).
fof(f1814,plain,
spl8_150,
inference(avatar_split_clause,[],[f274,f1109]) ).
fof(f1849,plain,
( e21 = e23
| ~ spl8_143
| ~ spl8_151 ),
inference(superposition,[],[f1114,f1080]) ).
fof(f1854,plain,
( $false
| ~ spl8_143
| ~ spl8_151 ),
inference(forward_subsumption_resolution,[],[f1849,f242]) ).
fof(f1855,plain,
( ~ spl8_143
| ~ spl8_151 ),
inference(avatar_contradiction_clause,[],[f1854]) ).
fof(f1882,plain,
( e11 = e13
| ~ spl8_158
| ~ spl8_166 ),
inference(forward_demodulation,[],[f1178,f1144]) ).
fof(f1883,plain,
( $false
| ~ spl8_158
| ~ spl8_166 ),
inference(forward_subsumption_resolution,[],[f1882,f236]) ).
fof(f1884,plain,
( ~ spl8_158
| ~ spl8_166 ),
inference(avatar_contradiction_clause,[],[f1883]) ).
fof(f1889,plain,
( e13 = op1(e10,e13)
| ~ spl8_269 ),
inference(forward_demodulation,[],[f43,f1673]) ).
fof(f1890,plain,
( spl8_241
| ~ spl8_269 ),
inference(avatar_split_clause,[],[f1889,f1671,f1533]) ).
fof(f1891,plain,
( e12 = op1(e12,e10)
| ~ spl8_269 ),
inference(forward_demodulation,[],[f44,f1673]) ).
fof(f1892,plain,
( spl8_237
| ~ spl8_269 ),
inference(avatar_split_clause,[],[f1891,f1671,f1516]) ).
fof(f1893,plain,
( e12 = op1(e10,e12)
| ~ spl8_269 ),
inference(forward_demodulation,[],[f45,f1673]) ).
fof(f1894,plain,
( spl8_234
| ~ spl8_269 ),
inference(avatar_split_clause,[],[f1893,f1671,f1503]) ).
fof(f1895,plain,
( e11 = op1(e11,e10)
| ~ spl8_269 ),
inference(forward_demodulation,[],[f46,f1673]) ).
fof(f1896,plain,
( spl8_230
| ~ spl8_269 ),
inference(avatar_split_clause,[],[f1895,f1671,f1486]) ).
fof(f1897,plain,
( e11 = op1(e10,e11)
| ~ spl8_269 ),
inference(forward_demodulation,[],[f47,f1673]) ).
fof(f1898,plain,
( spl8_227
| ~ spl8_269 ),
inference(avatar_split_clause,[],[f1897,f1671,f1473]) ).
fof(f1899,plain,
( e10 = op1(e10,e10)
| ~ spl8_269 ),
inference(forward_demodulation,[],[f48,f1673]) ).
fof(f1918,plain,
( e21 = e22
| ~ spl8_176
| ~ spl8_182 ),
inference(superposition,[],[f1248,f1222]) ).
fof(f1922,plain,
( $false
| ~ spl8_176
| ~ spl8_182 ),
inference(forward_subsumption_resolution,[],[f1918,f243]) ).
fof(f1923,plain,
( ~ spl8_176
| ~ spl8_182 ),
inference(avatar_contradiction_clause,[],[f1922]) ).
fof(f1962,plain,
( e22 = e23
| ~ spl8_186
| ~ spl8_192 ),
inference(forward_demodulation,[],[f1291,f1265]) ).
fof(f1963,plain,
( $false
| ~ spl8_186
| ~ spl8_192 ),
inference(forward_subsumption_resolution,[],[f1962,f241]) ).
fof(f1964,plain,
( ~ spl8_186
| ~ spl8_192 ),
inference(avatar_contradiction_clause,[],[f1963]) ).
fof(f1973,plain,
( e20 = e22
| ~ spl8_194
| ~ spl8_202 ),
inference(superposition,[],[f1336,f1300]) ).
fof(f1977,plain,
( $false
| ~ spl8_194
| ~ spl8_202 ),
inference(forward_subsumption_resolution,[],[f1973,f245]) ).
fof(f1978,plain,
( ~ spl8_194
| ~ spl8_202 ),
inference(avatar_contradiction_clause,[],[f1977]) ).
fof(f1980,plain,
( e20 = e22
| ~ spl8_196
| ~ spl8_204 ),
inference(superposition,[],[f1345,f1309]) ).
fof(f1984,plain,
( $false
| ~ spl8_196
| ~ spl8_204 ),
inference(forward_subsumption_resolution,[],[f1980,f245]) ).
fof(f1985,plain,
( ~ spl8_196
| ~ spl8_204 ),
inference(avatar_contradiction_clause,[],[f1984]) ).
fof(f2035,plain,
( e20 = e23
| ~ spl8_34
| ~ spl8_134 ),
inference(forward_demodulation,[],[f569,f1027]) ).
fof(f2037,plain,
( e20 = e23
| ~ spl8_174
| ~ spl8_192 ),
inference(forward_demodulation,[],[f1213,f1291]) ).
fof(f2083,plain,
( e20 = e21
| ~ spl8_172
| ~ spl8_178 ),
inference(forward_demodulation,[],[f1205,f1231]) ).
fof(f2109,plain,
( $false
| ~ spl8_172
| ~ spl8_178 ),
inference(forward_subsumption_resolution,[],[f2083,f246]) ).
fof(f2110,plain,
( ~ spl8_172
| ~ spl8_178 ),
inference(avatar_contradiction_clause,[],[f2109]) ).
fof(f2121,plain,
( e20 != e23
| spl8_34
| ~ spl8_134 ),
inference(forward_demodulation,[],[f570,f1027]) ).
fof(f2127,plain,
( $false
| spl8_34
| ~ spl8_134
| ~ spl8_174
| ~ spl8_192 ),
inference(forward_subsumption_resolution,[],[f2037,f2121]) ).
fof(f2128,plain,
( spl8_34
| ~ spl8_134
| ~ spl8_174
| ~ spl8_192 ),
inference(avatar_contradiction_clause,[],[f2127]) ).
fof(f2134,plain,
( e20 = e23
| ~ spl8_138
| ~ spl8_150 ),
inference(forward_demodulation,[],[f1059,f1110]) ).
fof(f2135,plain,
( $false
| spl8_34
| ~ spl8_134
| ~ spl8_138
| ~ spl8_150 ),
inference(forward_subsumption_resolution,[],[f2134,f2121]) ).
fof(f2136,plain,
( spl8_34
| ~ spl8_134
| ~ spl8_138
| ~ spl8_150 ),
inference(avatar_contradiction_clause,[],[f2135]) ).
fof(f2149,plain,
( $false
| ~ spl8_34
| ~ spl8_134 ),
inference(forward_subsumption_resolution,[],[f244,f2035]) ).
fof(f2150,plain,
( ~ spl8_34
| ~ spl8_134 ),
inference(avatar_contradiction_clause,[],[f2149]) ).
fof(f2199,plain,
( e20 = e21
| ~ spl8_169
| ~ spl8_175 ),
inference(superposition,[],[f1218,f1192]) ).
fof(f2203,plain,
( $false
| ~ spl8_169
| ~ spl8_175 ),
inference(forward_subsumption_resolution,[],[f2199,f246]) ).
fof(f2204,plain,
( ~ spl8_169
| ~ spl8_175 ),
inference(avatar_contradiction_clause,[],[f2203]) ).
fof(f2247,plain,
( e22 = e23
| ~ spl8_182
| ~ spl8_188 ),
inference(forward_demodulation,[],[f1274,f1248]) ).
fof(f2248,plain,
( $false
| ~ spl8_182
| ~ spl8_188 ),
inference(forward_subsumption_resolution,[],[f2247,f241]) ).
fof(f2249,plain,
( ~ spl8_182
| ~ spl8_188 ),
inference(avatar_contradiction_clause,[],[f2248]) ).
fof(f2301,plain,
( e20 = e21
| ~ spl8_193
| ~ spl8_197 ),
inference(forward_demodulation,[],[f1296,f1314]) ).
fof(f2302,plain,
( $false
| ~ spl8_193
| ~ spl8_197 ),
inference(forward_subsumption_resolution,[],[f2301,f246]) ).
fof(f2303,plain,
( ~ spl8_193
| ~ spl8_197 ),
inference(avatar_contradiction_clause,[],[f2302]) ).
fof(f2321,plain,
( e20 = op2(e20,e22)
| ~ spl8_219 ),
inference(forward_demodulation,[],[f105,f1424]) ).
fof(f2331,plain,
( spl8_170
| ~ spl8_219 ),
inference(avatar_split_clause,[],[f2321,f1422,f1194]) ).
fof(f2335,plain,
( e20 = op2(e22,e20)
| ~ spl8_219 ),
inference(forward_demodulation,[],[f106,f1424]) ).
fof(f2336,plain,
( spl8_173
| ~ spl8_219 ),
inference(avatar_split_clause,[],[f2335,f1422,f1207]) ).
fof(f2386,plain,
( e21 = e22
| ~ spl8_212
| ~ spl8_214 ),
inference(superposition,[],[f1393,f1383]) ).
fof(f2391,plain,
( $false
| ~ spl8_212
| ~ spl8_214 ),
inference(forward_subsumption_resolution,[],[f2386,f243]) ).
fof(f2392,plain,
( ~ spl8_212
| ~ spl8_214 ),
inference(avatar_contradiction_clause,[],[f2391]) ).
fof(f2487,plain,
( e10 = e11
| ~ spl8_224
| ~ spl8_230 ),
inference(superposition,[],[f1488,f1462]) ).
fof(f2491,plain,
( $false
| ~ spl8_224
| ~ spl8_230 ),
inference(forward_subsumption_resolution,[],[f2487,f240]) ).
fof(f2492,plain,
( ~ spl8_224
| ~ spl8_230 ),
inference(avatar_contradiction_clause,[],[f2491]) ).
fof(f2494,plain,
( e11 = e12
| ~ spl8_227
| ~ spl8_233 ),
inference(forward_demodulation,[],[f1501,f1475]) ).
fof(f2495,plain,
( $false
| ~ spl8_227
| ~ spl8_233 ),
inference(forward_subsumption_resolution,[],[f2494,f237]) ).
fof(f2496,plain,
( ~ spl8_227
| ~ spl8_233 ),
inference(avatar_contradiction_clause,[],[f2495]) ).
fof(f2498,plain,
( e10 = e12
| ~ spl8_225
| ~ spl8_237 ),
inference(forward_demodulation,[],[f1518,f1466]) ).
fof(f2499,plain,
( $false
| ~ spl8_225
| ~ spl8_237 ),
inference(forward_subsumption_resolution,[],[f2498,f239]) ).
fof(f2500,plain,
( ~ spl8_225
| ~ spl8_237 ),
inference(avatar_contradiction_clause,[],[f2499]) ).
fof(f2502,plain,
( e12 = e13
| ~ spl8_234
| ~ spl8_240 ),
inference(forward_demodulation,[],[f1531,f1505]) ).
fof(f2503,plain,
( $false
| ~ spl8_234
| ~ spl8_240 ),
inference(forward_subsumption_resolution,[],[f2502,f235]) ).
fof(f2504,plain,
( ~ spl8_234
| ~ spl8_240 ),
inference(avatar_contradiction_clause,[],[f2503]) ).
fof(f2518,plain,
( h2(e10) != op2(h2(e12),e21)
| ~ spl8_19
| spl8_74
| ~ spl8_247 ),
inference(superposition,[],[f1705,f1562]) ).
fof(f2532,plain,
( e12 = e13
| ~ spl8_162
| ~ spl8_166 ),
inference(superposition,[],[f1161,f1178]) ).
fof(f2537,plain,
( $false
| ~ spl8_162
| ~ spl8_166 ),
inference(forward_subsumption_resolution,[],[f2532,f235]) ).
fof(f2538,plain,
( ~ spl8_162
| ~ spl8_166 ),
inference(avatar_contradiction_clause,[],[f2537]) ).
fof(f2543,plain,
( e10 = e12
| ~ spl8_246
| ~ spl8_254 ),
inference(forward_demodulation,[],[f1593,f1557]) ).
fof(f2544,plain,
( $false
| ~ spl8_246
| ~ spl8_254 ),
inference(forward_subsumption_resolution,[],[f2543,f239]) ).
fof(f2545,plain,
( ~ spl8_246
| ~ spl8_254 ),
inference(avatar_contradiction_clause,[],[f2544]) ).
fof(f2557,plain,
( e10 = e13
| ~ spl8_154
| ~ spl8_166 ),
inference(superposition,[],[f1127,f1178]) ).
fof(f2563,plain,
( $false
| ~ spl8_154
| ~ spl8_166 ),
inference(forward_subsumption_resolution,[],[f2557,f238]) ).
fof(f2564,plain,
( ~ spl8_154
| ~ spl8_166 ),
inference(avatar_contradiction_clause,[],[f2563]) ).
fof(f2677,plain,
( e10 = op1(e10,e12)
| ~ spl8_271 ),
inference(forward_demodulation,[],[f48,f1681]) ).
fof(f2678,plain,
( spl8_222
| ~ spl8_271 ),
inference(avatar_split_clause,[],[f2677,f1679,f1451]) ).
fof(f2679,plain,
( e10 = op1(e12,e10)
| ~ spl8_271 ),
inference(forward_demodulation,[],[f49,f1681]) ).
fof(f2683,plain,
( spl8_225
| ~ spl8_271 ),
inference(avatar_split_clause,[],[f2679,f1679,f1464]) ).
fof(f2704,plain,
( e10 = e13
| ~ spl8_223
| ~ spl8_241 ),
inference(superposition,[],[f1457,f1535]) ).
fof(f2710,plain,
( $false
| ~ spl8_223
| ~ spl8_241 ),
inference(forward_subsumption_resolution,[],[f2704,f238]) ).
fof(f2711,plain,
( ~ spl8_223
| ~ spl8_241 ),
inference(avatar_contradiction_clause,[],[f2710]) ).
fof(f2743,plain,
( e12 = e13
| ~ spl8_161
| ~ spl8_165 ),
inference(forward_demodulation,[],[f1174,f1157]) ).
fof(f2744,plain,
( $false
| ~ spl8_161
| ~ spl8_165 ),
inference(forward_subsumption_resolution,[],[f2743,f235]) ).
fof(f2745,plain,
( ~ spl8_161
| ~ spl8_165 ),
inference(avatar_contradiction_clause,[],[f2744]) ).
fof(f2760,plain,
( e10 = e13
| ~ spl8_225
| ~ spl8_243 ),
inference(forward_demodulation,[],[f1544,f1466]) ).
fof(f2761,plain,
( $false
| ~ spl8_225
| ~ spl8_243 ),
inference(forward_subsumption_resolution,[],[f2760,f238]) ).
fof(f2762,plain,
( ~ spl8_225
| ~ spl8_243 ),
inference(avatar_contradiction_clause,[],[f2761]) ).
fof(f2763,plain,
( e11 = e13
| ~ spl8_157
| ~ spl8_165 ),
inference(forward_demodulation,[],[f1174,f1140]) ).
fof(f2765,plain,
( $false
| ~ spl8_157
| ~ spl8_165 ),
inference(forward_subsumption_resolution,[],[f2763,f236]) ).
fof(f2766,plain,
( ~ spl8_157
| ~ spl8_165 ),
inference(avatar_contradiction_clause,[],[f2765]) ).
fof(f2768,plain,
( e10 = e12
| ~ spl8_224
| ~ spl8_236 ),
inference(forward_demodulation,[],[f1514,f1462]) ).
fof(f2769,plain,
( $false
| ~ spl8_224
| ~ spl8_236 ),
inference(forward_subsumption_resolution,[],[f2768,f239]) ).
fof(f2770,plain,
( ~ spl8_224
| ~ spl8_236 ),
inference(avatar_contradiction_clause,[],[f2769]) ).
fof(f2917,plain,
( e23 = h2(e13)
| ~ spl8_150 ),
inference(forward_demodulation,[],[f281,f1110]) ).
fof(f2918,plain,
( spl8_88
| ~ spl8_150 ),
inference(avatar_split_clause,[],[f2917,f1109,f818]) ).
fof(f2947,plain,
( e13 != op1(e11,e10)
| ~ spl8_166 ),
inference(forward_demodulation,[],[f156,f1178]) ).
fof(f2974,plain,
( e10 != op1(e10,e12)
| ~ spl8_245 ),
inference(forward_demodulation,[],[f174,f1553]) ).
fof(f3022,plain,
( e22 != op2(e21,e23)
| ~ spl8_148 ),
inference(forward_demodulation,[],[f212,f1101]) ).
fof(f3044,plain,
( e21 != op2(e20,e21)
| ~ spl8_199 ),
inference(forward_demodulation,[],[f227,f1323]) ).
fof(f3049,plain,
( e20 != op2(e21,e20)
| ~ spl8_173 ),
inference(forward_demodulation,[],[f231,f1209]) ).
fof(f3053,plain,
( e12 = op1(e11,e13)
| ~ spl8_166 ),
inference(forward_demodulation,[],[f272,f1178]) ).
fof(f3054,plain,
( e11 = e12
| ~ spl8_166
| ~ spl8_250 ),
inference(forward_demodulation,[],[f3053,f1575]) ).
fof(f3055,plain,
( $false
| ~ spl8_166
| ~ spl8_250 ),
inference(forward_subsumption_resolution,[],[f3054,f237]) ).
fof(f3056,plain,
( ~ spl8_166
| ~ spl8_250 ),
inference(avatar_contradiction_clause,[],[f3055]) ).
fof(f3060,plain,
( spl8_254
| ~ spl8_166 ),
inference(avatar_split_clause,[],[f3053,f1177,f1591]) ).
fof(f3061,plain,
( e13 != op1(e12,e11)
| ~ spl8_166 ),
inference(forward_demodulation,[],[f177,f1178]) ).
fof(f3063,plain,
( e13 != op1(e11,e12)
| ~ spl8_166 ),
inference(forward_demodulation,[],[f153,f1178]) ).
fof(f3065,plain,
( ~ spl8_242
| ~ spl8_166 ),
inference(avatar_split_clause,[],[f2947,f1177,f1538]) ).
fof(f3071,plain,
( ~ spl8_259
| ~ spl8_166 ),
inference(avatar_split_clause,[],[f3061,f1177,f1614]) ).
fof(f3073,plain,
( ~ spl8_257
| ~ spl8_166 ),
inference(avatar_split_clause,[],[f3063,f1177,f1605]) ).
fof(f3118,plain,
( e11 = e12
| ~ spl8_232
| ~ spl8_238 ),
inference(forward_demodulation,[],[f1522,f1496]) ).
fof(f3119,plain,
( $false
| ~ spl8_232
| ~ spl8_238 ),
inference(forward_subsumption_resolution,[],[f3118,f237]) ).
fof(f3120,plain,
( ~ spl8_232
| ~ spl8_238 ),
inference(avatar_contradiction_clause,[],[f3119]) ).
fof(f3121,plain,
( e10 = e11
| ~ spl8_225
| ~ spl8_231 ),
inference(superposition,[],[f1492,f1466]) ).
fof(f3126,plain,
( $false
| ~ spl8_225
| ~ spl8_231 ),
inference(forward_subsumption_resolution,[],[f3121,f240]) ).
fof(f3127,plain,
( ~ spl8_225
| ~ spl8_231 ),
inference(avatar_contradiction_clause,[],[f3126]) ).
fof(f3128,plain,
( ~ spl8_222
| ~ spl8_245 ),
inference(avatar_split_clause,[],[f2974,f1551,f1451]) ).
fof(f3131,plain,
( spl8_153
| ~ spl8_269 ),
inference(avatar_split_clause,[],[f1899,f1671,f1122]) ).
fof(f3259,plain,
( e22 = op2(e21,e23)
| ~ spl8_150 ),
inference(forward_demodulation,[],[f275,f1110]) ).
fof(f3270,plain,
( ~ spl8_202
| ~ spl8_148 ),
inference(avatar_split_clause,[],[f3022,f1100,f1334]) ).
fof(f3271,plain,
( spl8_202
| ~ spl8_150 ),
inference(avatar_split_clause,[],[f3259,f1109,f1334]) ).
fof(f3273,plain,
( e23 != op2(e21,e22)
| ~ spl8_150 ),
inference(forward_demodulation,[],[f201,f1110]) ).
fof(f3275,plain,
( e20 != op2(e21,e22)
| ~ spl8_170 ),
inference(forward_demodulation,[],[f222,f1196]) ).
fof(f3277,plain,
( e23 != op2(e21,e23)
| ~ spl8_150 ),
inference(forward_demodulation,[],[f200,f1110]) ).
fof(f3302,plain,
( ~ spl8_193
| ~ spl8_170 ),
inference(avatar_split_clause,[],[f3275,f1194,f1294]) ).
fof(f3308,plain,
( ~ spl8_172
| ~ spl8_173 ),
inference(avatar_split_clause,[],[f3049,f1207,f1203]) ).
fof(f3325,plain,
( ~ spl8_206
| ~ spl8_150 ),
inference(avatar_split_clause,[],[f3277,f1109,f1352]) ).
fof(f3372,plain,
( e21 = e22
| ~ spl8_179
| ~ spl8_185 ),
inference(superposition,[],[f1261,f1235]) ).
fof(f3378,plain,
( $false
| ~ spl8_179
| ~ spl8_185 ),
inference(forward_subsumption_resolution,[],[f3372,f243]) ).
fof(f3379,plain,
( ~ spl8_179
| ~ spl8_185 ),
inference(avatar_contradiction_clause,[],[f3378]) ).
fof(f3383,plain,
( $false
| ~ spl8_175
| ~ spl8_199 ),
inference(forward_subsumption_resolution,[],[f3044,f1218]) ).
fof(f3384,plain,
( ~ spl8_175
| ~ spl8_199 ),
inference(avatar_contradiction_clause,[],[f3383]) ).
fof(f3399,plain,
( e21 = e22
| ~ spl8_198
| ~ spl8_202 ),
inference(superposition,[],[f1336,f1318]) ).
fof(f3404,plain,
( $false
| ~ spl8_198
| ~ spl8_202 ),
inference(forward_subsumption_resolution,[],[f3399,f243]) ).
fof(f3405,plain,
( ~ spl8_198
| ~ spl8_202 ),
inference(avatar_contradiction_clause,[],[f3404]) ).
fof(f3490,plain,
( op2(e21,e23) = h2(e12)
| ~ spl8_150 ),
inference(forward_demodulation,[],[f282,f1110]) ).
fof(f3491,plain,
( e22 = h2(e12)
| ~ spl8_150
| ~ spl8_202 ),
inference(forward_demodulation,[],[f3490,f1336]) ).
fof(f3492,plain,
( spl8_83
| ~ spl8_150
| ~ spl8_202 ),
inference(avatar_split_clause,[],[f3491,f1334,f1109,f787]) ).
fof(f3493,plain,
( op2(e22,e21) != h2(e10)
| ~ spl8_19
| spl8_74
| ~ spl8_83
| ~ spl8_247 ),
inference(superposition,[],[f2518,f788]) ).
fof(f3494,plain,
( e20 != h2(e10)
| ~ spl8_19
| spl8_74
| ~ spl8_83
| ~ spl8_195
| ~ spl8_247 ),
inference(forward_demodulation,[],[f3493,f1305]) ).
fof(f3495,plain,
( ~ spl8_15
| ~ spl8_19
| spl8_74
| ~ spl8_83
| ~ spl8_195
| ~ spl8_247 ),
inference(avatar_split_clause,[],[f3494,f1560,f1303,f787,f750,f496,f477]) ).
fof(f3663,plain,
( h2(e10) = op2(e21,op2(e21,e23))
| ~ spl8_150 ),
inference(forward_demodulation,[],[f283,f1110]) ).
fof(f3664,plain,
( op2(e21,e22) = h2(e10)
| ~ spl8_150
| ~ spl8_202 ),
inference(forward_demodulation,[],[f3663,f1336]) ).
fof(f3665,plain,
( e20 = h2(e10)
| ~ spl8_150
| ~ spl8_193
| ~ spl8_202 ),
inference(forward_demodulation,[],[f3664,f1296]) ).
fof(f3668,plain,
( h2(e10) != op2(h2(e10),h2(e10))
| spl8_65
| ~ spl8_153 ),
inference(forward_demodulation,[],[f716,f1123]) ).
fof(f3670,plain,
( spl8_15
| ~ spl8_150
| ~ spl8_193
| ~ spl8_202 ),
inference(avatar_split_clause,[],[f3665,f1334,f1294,f1109,f477]) ).
fof(f3675,plain,
( e20 != op2(e20,e20)
| ~ spl8_15
| spl8_65
| ~ spl8_153 ),
inference(forward_demodulation,[],[f3668,f478]) ).
fof(f3676,plain,
( $false
| ~ spl8_15
| spl8_65
| ~ spl8_137
| ~ spl8_153 ),
inference(forward_subsumption_resolution,[],[f3675,f1055]) ).
fof(f3677,plain,
( ~ spl8_15
| spl8_65
| ~ spl8_137
| ~ spl8_153 ),
inference(avatar_contradiction_clause,[],[f3676]) ).
fof(f3679,plain,
( h2(op1(e10,e11)) != op2(h2(e10),e21)
| ~ spl8_19
| spl8_66 ),
inference(forward_demodulation,[],[f720,f497]) ).
fof(f3681,plain,
( op2(e20,e21) != h2(op1(e10,e11))
| ~ spl8_15
| ~ spl8_19
| spl8_66 ),
inference(forward_demodulation,[],[f3679,f478]) ).
fof(f3683,plain,
( op2(e20,e21) != h2(e11)
| ~ spl8_15
| ~ spl8_19
| spl8_66
| ~ spl8_227 ),
inference(forward_demodulation,[],[f3681,f1475]) ).
fof(f3684,plain,
( e21 != op2(e20,e21)
| ~ spl8_15
| ~ spl8_19
| spl8_66
| ~ spl8_227 ),
inference(forward_demodulation,[],[f3683,f497]) ).
fof(f3685,plain,
( $false
| ~ spl8_15
| ~ spl8_19
| spl8_66
| ~ spl8_175
| ~ spl8_227 ),
inference(forward_subsumption_resolution,[],[f3684,f1218]) ).
fof(f3686,plain,
( ~ spl8_15
| ~ spl8_19
| spl8_66
| ~ spl8_175
| ~ spl8_227 ),
inference(avatar_contradiction_clause,[],[f3685]) ).
fof(f3688,plain,
( h2(op1(e10,e12)) != op2(h2(e10),e22)
| spl8_67
| ~ spl8_83 ),
inference(forward_demodulation,[],[f724,f788]) ).
fof(f3690,plain,
( op2(e20,e22) != h2(op1(e10,e12))
| ~ spl8_15
| spl8_67
| ~ spl8_83 ),
inference(forward_demodulation,[],[f3688,f478]) ).
fof(f3692,plain,
( op2(e20,e22) != h2(e12)
| ~ spl8_15
| spl8_67
| ~ spl8_83
| ~ spl8_234 ),
inference(forward_demodulation,[],[f3690,f1505]) ).
fof(f3694,plain,
( e22 != op2(e20,e22)
| ~ spl8_15
| spl8_67
| ~ spl8_83
| ~ spl8_234 ),
inference(forward_demodulation,[],[f3692,f788]) ).
fof(f3695,plain,
( $false
| ~ spl8_15
| spl8_67
| ~ spl8_83
| ~ spl8_182
| ~ spl8_234 ),
inference(forward_subsumption_resolution,[],[f3694,f1248]) ).
fof(f3696,plain,
( ~ spl8_15
| spl8_67
| ~ spl8_83
| ~ spl8_182
| ~ spl8_234 ),
inference(avatar_contradiction_clause,[],[f3695]) ).
fof(f3698,plain,
( h2(op1(e10,e13)) != op2(h2(e10),e23)
| spl8_68
| ~ spl8_88 ),
inference(forward_demodulation,[],[f728,f819]) ).
fof(f3700,plain,
( op2(e20,e23) != h2(op1(e10,e13))
| ~ spl8_15
| spl8_68
| ~ spl8_88 ),
inference(forward_demodulation,[],[f3698,f478]) ).
fof(f3702,plain,
( op2(e20,e23) != h2(e13)
| ~ spl8_15
| spl8_68
| ~ spl8_88
| ~ spl8_241 ),
inference(forward_demodulation,[],[f3700,f1535]) ).
fof(f3704,plain,
( e23 != op2(e20,e23)
| ~ spl8_15
| spl8_68
| ~ spl8_88
| ~ spl8_241 ),
inference(forward_demodulation,[],[f3702,f819]) ).
fof(f3705,plain,
( $false
| ~ spl8_15
| spl8_68
| ~ spl8_88
| ~ spl8_189
| ~ spl8_241 ),
inference(forward_subsumption_resolution,[],[f3704,f1278]) ).
fof(f3706,plain,
( ~ spl8_15
| spl8_68
| ~ spl8_88
| ~ spl8_189
| ~ spl8_241 ),
inference(avatar_contradiction_clause,[],[f3705]) ).
fof(f3708,plain,
( h2(op1(e11,e10)) != op2(h2(e11),e20)
| ~ spl8_15
| spl8_69 ),
inference(forward_demodulation,[],[f732,f478]) ).
fof(f3710,plain,
( op2(e21,e20) != h2(op1(e11,e10))
| ~ spl8_15
| ~ spl8_19
| spl8_69 ),
inference(forward_demodulation,[],[f3708,f497]) ).
fof(f3712,plain,
( op2(e21,e20) != h2(e11)
| ~ spl8_15
| ~ spl8_19
| spl8_69
| ~ spl8_230 ),
inference(forward_demodulation,[],[f3710,f1488]) ).
fof(f3714,plain,
( e21 != op2(e21,e20)
| ~ spl8_15
| ~ spl8_19
| spl8_69
| ~ spl8_230 ),
inference(forward_demodulation,[],[f3712,f497]) ).
fof(f3715,plain,
( $false
| ~ spl8_15
| ~ spl8_19
| spl8_69
| ~ spl8_178
| ~ spl8_230 ),
inference(forward_subsumption_resolution,[],[f3714,f1231]) ).
fof(f3716,plain,
( ~ spl8_15
| ~ spl8_19
| spl8_69
| ~ spl8_178
| ~ spl8_230 ),
inference(avatar_contradiction_clause,[],[f3715]) ).
fof(f3718,plain,
( op2(e21,e21) != h2(op1(e11,e11))
| ~ spl8_19
| spl8_70 ),
inference(forward_demodulation,[],[f736,f497]) ).
fof(f3720,plain,
( op2(e21,e21) != h2(e13)
| ~ spl8_19
| spl8_70
| ~ spl8_166 ),
inference(forward_demodulation,[],[f3718,f1178]) ).
fof(f3722,plain,
( e23 != op2(e21,e21)
| ~ spl8_19
| spl8_70
| ~ spl8_88
| ~ spl8_166 ),
inference(forward_demodulation,[],[f3720,f819]) ).
fof(f3724,plain,
( $false
| ~ spl8_19
| spl8_70
| ~ spl8_88
| ~ spl8_150
| ~ spl8_166 ),
inference(forward_subsumption_resolution,[],[f3722,f1110]) ).
fof(f3725,plain,
( ~ spl8_19
| spl8_70
| ~ spl8_88
| ~ spl8_150
| ~ spl8_166 ),
inference(avatar_contradiction_clause,[],[f3724]) ).
fof(f3727,plain,
( h2(op1(e11,e12)) != op2(h2(e11),e22)
| spl8_71
| ~ spl8_83 ),
inference(forward_demodulation,[],[f740,f788]) ).
fof(f3729,plain,
( op2(e21,e22) != h2(op1(e11,e12))
| ~ spl8_19
| spl8_71
| ~ spl8_83 ),
inference(forward_demodulation,[],[f3727,f497]) ).
fof(f3731,plain,
( op2(e21,e22) != h2(e10)
| ~ spl8_19
| spl8_71
| ~ spl8_83
| ~ spl8_245 ),
inference(forward_demodulation,[],[f3729,f1553]) ).
fof(f3732,plain,
( e20 != op2(e21,e22)
| ~ spl8_15
| ~ spl8_19
| spl8_71
| ~ spl8_83
| ~ spl8_245 ),
inference(forward_demodulation,[],[f3731,f478]) ).
fof(f3733,plain,
( $false
| ~ spl8_15
| ~ spl8_19
| spl8_71
| ~ spl8_83
| ~ spl8_193
| ~ spl8_245 ),
inference(forward_subsumption_resolution,[],[f3732,f1296]) ).
fof(f3734,plain,
( ~ spl8_15
| ~ spl8_19
| spl8_71
| ~ spl8_83
| ~ spl8_193
| ~ spl8_245 ),
inference(avatar_contradiction_clause,[],[f3733]) ).
fof(f3736,plain,
( h2(op1(e11,e13)) != op2(h2(e11),e23)
| spl8_72
| ~ spl8_88 ),
inference(forward_demodulation,[],[f744,f819]) ).
fof(f3738,plain,
( op2(e21,e23) != h2(op1(e11,e13))
| ~ spl8_19
| spl8_72
| ~ spl8_88 ),
inference(forward_demodulation,[],[f3736,f497]) ).
fof(f3740,plain,
( op2(e21,e23) != h2(e12)
| ~ spl8_19
| spl8_72
| ~ spl8_88
| ~ spl8_254 ),
inference(forward_demodulation,[],[f3738,f1593]) ).
fof(f3742,plain,
( e22 != op2(e21,e23)
| ~ spl8_19
| spl8_72
| ~ spl8_83
| ~ spl8_88
| ~ spl8_254 ),
inference(forward_demodulation,[],[f3740,f788]) ).
fof(f3743,plain,
( $false
| ~ spl8_19
| spl8_72
| ~ spl8_83
| ~ spl8_88
| ~ spl8_202
| ~ spl8_254 ),
inference(forward_subsumption_resolution,[],[f3742,f1336]) ).
fof(f3744,plain,
( ~ spl8_19
| spl8_72
| ~ spl8_83
| ~ spl8_88
| ~ spl8_202
| ~ spl8_254 ),
inference(avatar_contradiction_clause,[],[f3743]) ).
fof(f3746,plain,
( h2(op1(e12,e10)) != op2(h2(e12),e20)
| ~ spl8_15
| spl8_73 ),
inference(forward_demodulation,[],[f748,f478]) ).
fof(f3748,plain,
( op2(e22,e20) != h2(op1(e12,e10))
| ~ spl8_15
| spl8_73
| ~ spl8_83 ),
inference(forward_demodulation,[],[f3746,f788]) ).
fof(f3750,plain,
( op2(e22,e20) != h2(e12)
| ~ spl8_15
| spl8_73
| ~ spl8_83
| ~ spl8_237 ),
inference(forward_demodulation,[],[f3748,f1518]) ).
fof(f3752,plain,
( e22 != op2(e22,e20)
| ~ spl8_15
| spl8_73
| ~ spl8_83
| ~ spl8_237 ),
inference(forward_demodulation,[],[f3750,f788]) ).
fof(f3753,plain,
( $false
| ~ spl8_15
| spl8_73
| ~ spl8_83
| ~ spl8_185
| ~ spl8_237 ),
inference(forward_subsumption_resolution,[],[f3752,f1261]) ).
fof(f3754,plain,
( ~ spl8_15
| spl8_73
| ~ spl8_83
| ~ spl8_185
| ~ spl8_237 ),
inference(avatar_contradiction_clause,[],[f3753]) ).
fof(f3756,plain,
( op2(e22,e22) != h2(op1(e12,e12))
| spl8_75
| ~ spl8_83 ),
inference(forward_demodulation,[],[f756,f788]) ).
fof(f3758,plain,
( op2(e22,e22) != h2(e13)
| spl8_75
| ~ spl8_83
| ~ spl8_167 ),
inference(forward_demodulation,[],[f3756,f1182]) ).
fof(f3760,plain,
( e23 != op2(e22,e22)
| spl8_75
| ~ spl8_83
| ~ spl8_88
| ~ spl8_167 ),
inference(forward_demodulation,[],[f3758,f819]) ).
fof(f3762,plain,
( $false
| spl8_75
| ~ spl8_83
| ~ spl8_88
| ~ spl8_151
| ~ spl8_167 ),
inference(forward_subsumption_resolution,[],[f3760,f1114]) ).
fof(f3763,plain,
( spl8_75
| ~ spl8_83
| ~ spl8_88
| ~ spl8_151
| ~ spl8_167 ),
inference(avatar_contradiction_clause,[],[f3762]) ).
fof(f3765,plain,
( h2(op1(e12,e13)) != op2(h2(e12),e23)
| spl8_76
| ~ spl8_88 ),
inference(forward_demodulation,[],[f760,f819]) ).
fof(f3767,plain,
( op2(e22,e23) != h2(op1(e12,e13))
| spl8_76
| ~ spl8_83
| ~ spl8_88 ),
inference(forward_demodulation,[],[f3765,f788]) ).
fof(f3769,plain,
( op2(e22,e23) != h2(e11)
| spl8_76
| ~ spl8_83
| ~ spl8_88
| ~ spl8_263 ),
inference(forward_demodulation,[],[f3767,f1635]) ).
fof(f3770,plain,
( e21 != op2(e22,e23)
| ~ spl8_19
| spl8_76
| ~ spl8_83
| ~ spl8_88
| ~ spl8_263 ),
inference(forward_demodulation,[],[f3769,f497]) ).
fof(f3774,plain,
( h2(op1(e13,e10)) != op2(h2(e13),e20)
| ~ spl8_15
| spl8_77 ),
inference(forward_demodulation,[],[f764,f478]) ).
fof(f3776,plain,
( op2(e23,e20) != h2(op1(e13,e10))
| ~ spl8_15
| spl8_77
| ~ spl8_88 ),
inference(forward_demodulation,[],[f3774,f819]) ).
fof(f3778,plain,
( op2(e23,e20) != h2(e13)
| ~ spl8_15
| spl8_77
| ~ spl8_88
| ~ spl8_244 ),
inference(forward_demodulation,[],[f3776,f1548]) ).
fof(f3780,plain,
( e23 != op2(e23,e20)
| ~ spl8_15
| spl8_77
| ~ spl8_88
| ~ spl8_244 ),
inference(forward_demodulation,[],[f3778,f819]) ).
fof(f3781,plain,
( $false
| ~ spl8_15
| spl8_77
| ~ spl8_88
| ~ spl8_192
| ~ spl8_244 ),
inference(forward_subsumption_resolution,[],[f3780,f1291]) ).
fof(f3782,plain,
( ~ spl8_15
| spl8_77
| ~ spl8_88
| ~ spl8_192
| ~ spl8_244 ),
inference(avatar_contradiction_clause,[],[f3781]) ).
fof(f3784,plain,
( h2(op1(e13,e11)) != op2(h2(e13),e21)
| ~ spl8_19
| spl8_78 ),
inference(forward_demodulation,[],[f768,f497]) ).
fof(f3786,plain,
( op2(e23,e21) != h2(op1(e13,e11))
| ~ spl8_19
| spl8_78
| ~ spl8_88 ),
inference(forward_demodulation,[],[f3784,f819]) ).
fof(f3788,plain,
( op2(e23,e21) != h2(e12)
| ~ spl8_19
| spl8_78
| ~ spl8_88
| ~ spl8_256 ),
inference(forward_demodulation,[],[f3786,f1602]) ).
fof(f3790,plain,
( e22 != op2(e23,e21)
| ~ spl8_19
| spl8_78
| ~ spl8_83
| ~ spl8_88
| ~ spl8_256 ),
inference(forward_demodulation,[],[f3788,f788]) ).
fof(f3791,plain,
( $false
| ~ spl8_19
| spl8_78
| ~ spl8_83
| ~ spl8_88
| ~ spl8_204
| ~ spl8_256 ),
inference(forward_subsumption_resolution,[],[f3790,f1345]) ).
fof(f3792,plain,
( ~ spl8_19
| spl8_78
| ~ spl8_83
| ~ spl8_88
| ~ spl8_204
| ~ spl8_256 ),
inference(avatar_contradiction_clause,[],[f3791]) ).
fof(f3794,plain,
( h2(op1(e13,e12)) != op2(h2(e13),e22)
| spl8_79
| ~ spl8_83 ),
inference(forward_demodulation,[],[f772,f788]) ).
fof(f3796,plain,
( op2(e23,e22) != h2(op1(e13,e12))
| spl8_79
| ~ spl8_83
| ~ spl8_88 ),
inference(forward_demodulation,[],[f3794,f819]) ).
fof(f3798,plain,
( op2(e23,e22) != h2(e11)
| spl8_79
| ~ spl8_83
| ~ spl8_88
| ~ spl8_264 ),
inference(forward_demodulation,[],[f3796,f1640]) ).
fof(f3800,plain,
( e21 != op2(e23,e22)
| ~ spl8_19
| spl8_79
| ~ spl8_83
| ~ spl8_88
| ~ spl8_264 ),
inference(forward_demodulation,[],[f3798,f497]) ).
fof(f3801,plain,
( $false
| ~ spl8_19
| spl8_79
| ~ spl8_83
| ~ spl8_88
| ~ spl8_212
| ~ spl8_264 ),
inference(forward_subsumption_resolution,[],[f3800,f1383]) ).
fof(f3802,plain,
( ~ spl8_19
| spl8_79
| ~ spl8_83
| ~ spl8_88
| ~ spl8_212
| ~ spl8_264 ),
inference(avatar_contradiction_clause,[],[f3801]) ).
fof(f3804,plain,
( op2(e23,e23) != h2(op1(e13,e13))
| spl8_80
| ~ spl8_88 ),
inference(forward_demodulation,[],[f776,f819]) ).
fof(f3806,plain,
( op2(e23,e23) != h2(e10)
| spl8_80
| ~ spl8_88
| ~ spl8_156 ),
inference(forward_demodulation,[],[f3804,f1135]) ).
fof(f3808,plain,
( e20 != op2(e23,e23)
| ~ spl8_15
| spl8_80
| ~ spl8_88
| ~ spl8_156 ),
inference(forward_demodulation,[],[f3806,f478]) ).
fof(f3810,plain,
( $false
| ~ spl8_15
| spl8_80
| ~ spl8_88
| ~ spl8_140
| ~ spl8_156 ),
inference(forward_subsumption_resolution,[],[f3808,f1067]) ).
fof(f3811,plain,
( ~ spl8_15
| spl8_80
| ~ spl8_88
| ~ spl8_140
| ~ spl8_156 ),
inference(avatar_contradiction_clause,[],[f3810]) ).
fof(f3818,plain,
( e10 != op1(e12,e13)
| ~ spl8_247 ),
inference(forward_demodulation,[],[f146,f1562]) ).
fof(f3820,plain,
( e12 != op1(e12,e13)
| ~ spl8_254 ),
inference(forward_demodulation,[],[f165,f1593]) ).
fof(f3821,plain,
( e13 != op1(e12,e13)
| ~ spl8_241 ),
inference(forward_demodulation,[],[f167,f1535]) ).
fof(f3832,plain,
( ~ spl8_261
| ~ spl8_247 ),
inference(avatar_split_clause,[],[f3818,f1560,f1623]) ).
fof(f3834,plain,
( ~ spl8_265
| ~ spl8_254 ),
inference(avatar_split_clause,[],[f3820,f1591,f1643]) ).
fof(f3835,plain,
( ~ spl8_267
| ~ spl8_241 ),
inference(avatar_split_clause,[],[f3821,f1533,f1653]) ).
fof(f3844,plain,
( ~ spl8_211
| ~ spl8_19
| spl8_76
| ~ spl8_83
| ~ spl8_88
| ~ spl8_263 ),
inference(avatar_split_clause,[],[f3770,f1633,f818,f787,f758,f496,f1376]) ).
fof(f3848,plain,
( e23 != op2(e23,e22)
| ~ spl8_192 ),
inference(forward_demodulation,[],[f191,f1291]) ).
fof(f3849,plain,
( e20 != op2(e23,e22)
| ~ spl8_193 ),
inference(forward_demodulation,[],[f218,f1296]) ).
fof(f3856,plain,
( ~ spl8_205
| ~ spl8_150 ),
inference(avatar_split_clause,[],[f3273,f1109,f1348]) ).
fof(f3873,plain,
( ~ spl8_216
| ~ spl8_192 ),
inference(avatar_split_clause,[],[f3848,f1289,f1401]) ).
fof(f3874,plain,
( ~ spl8_210
| ~ spl8_193 ),
inference(avatar_split_clause,[],[f3849,f1294,f1371]) ).
fof(f3894,plain,
( e13 != op1(e13,e12)
| ~ spl8_244 ),
inference(forward_demodulation,[],[f143,f1548]) ).
fof(f3896,plain,
( e10 != op1(e13,e12)
| ~ spl8_245 ),
inference(forward_demodulation,[],[f170,f1553]) ).
fof(f3897,plain,
( e12 != op1(e13,e12)
| ~ spl8_234 ),
inference(forward_demodulation,[],[f172,f1505]) ).
fof(f3904,plain,
( e12 != op1(e12,e11)
| ~ spl8_237 ),
inference(forward_demodulation,[],[f150,f1518]) ).
fof(f3905,plain,
( e11 != op1(e12,e11)
| ~ spl8_227 ),
inference(forward_demodulation,[],[f179,f1475]) ).
fof(f3909,plain,
( ~ spl8_268
| ~ spl8_244 ),
inference(avatar_split_clause,[],[f3894,f1546,f1658]) ).
fof(f3911,plain,
( ~ spl8_266
| ~ spl8_234 ),
inference(avatar_split_clause,[],[f3897,f1503,f1648]) ).
fof(f3913,plain,
( ~ spl8_255
| ~ spl8_237 ),
inference(avatar_split_clause,[],[f3904,f1516,f1596]) ).
fof(f3914,plain,
( ~ spl8_251
| ~ spl8_227 ),
inference(avatar_split_clause,[],[f3905,f1473,f1578]) ).
fof(f3933,plain,
( ~ spl8_262
| ~ spl8_245 ),
inference(avatar_split_clause,[],[f3896,f1551,f1628]) ).
cnf(s12,plain,
( ~ spl8_11
| ~ spl8_15 ),
inference(sat_conversion,[],[f480]) ).
cnf(s15,plain,
( ~ spl8_16
| ~ spl8_19 ),
inference(sat_conversion,[],[f499]) ).
cnf(s62,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_83
| ~ spl8_88 ),
inference(sat_conversion,[],[f822]) ).
cnf(s97,plain,
spl8_134,
inference(sat_conversion,[],[f1049]) ).
cnf(s99,plain,
spl8_19,
inference(sat_conversion,[],[f1051]) ).
cnf(s117,plain,
( spl8_138
| spl8_172
| spl8_193
| spl8_194 ),
inference(sat_conversion,[],[f1301]) ).
cnf(s118,plain,
( spl8_138
| spl8_169
| spl8_195
| spl8_196 ),
inference(sat_conversion,[],[f1310]) ).
cnf(s127,plain,
( spl8_143
| spl8_179
| spl8_199
| spl8_211 ),
inference(sat_conversion,[],[f1379]) ).
cnf(s128,plain,
( spl8_143
| spl8_176
| spl8_197
| spl8_212 ),
inference(sat_conversion,[],[f1384]) ).
cnf(s132,plain,
( spl8_151
| spl8_188
| spl8_205
| spl8_216 ),
inference(sat_conversion,[],[f1404]) ).
cnf(s133,plain,
( spl8_140
| spl8_174
| spl8_196
| spl8_210 ),
inference(sat_conversion,[],[f1405]) ).
cnf(s137,plain,
( spl8_148
| spl8_186
| spl8_204
| spl8_214 ),
inference(sat_conversion,[],[f1409]) ).
cnf(s141,plain,
( spl8_217
| spl8_218
| spl8_219
| spl8_220 ),
inference(sat_conversion,[],[f1429]) ).
cnf(s161,plain,
( spl8_157
| spl8_230
| spl8_231
| spl8_232 ),
inference(sat_conversion,[],[f1497]) ).
cnf(s163,plain,
( spl8_161
| spl8_236
| spl8_237
| spl8_238 ),
inference(sat_conversion,[],[f1523]) ).
cnf(s165,plain,
( spl8_165
| spl8_242
| spl8_243
| spl8_244 ),
inference(sat_conversion,[],[f1549]) ).
cnf(s166,plain,
( spl8_154
| spl8_224
| spl8_245
| spl8_246 ),
inference(sat_conversion,[],[f1558]) ).
cnf(s171,plain,
( spl8_162
| spl8_233
| spl8_255
| spl8_256 ),
inference(sat_conversion,[],[f1603]) ).
cnf(s181,plain,
( spl8_167
| spl8_240
| spl8_257
| spl8_268 ),
inference(sat_conversion,[],[f1661]) ).
cnf(s183,plain,
( spl8_156
| spl8_223
| spl8_246
| spl8_261 ),
inference(sat_conversion,[],[f1663]) ).
cnf(s190,plain,
( spl8_269
| spl8_270
| spl8_271
| spl8_272 ),
inference(sat_conversion,[],[f1686]) ).
cnf(s200,plain,
( spl8_247
| spl8_251
| spl8_255
| spl8_259 ),
inference(sat_conversion,[],[f1696]) ).
cnf(s202,plain,
( spl8_261
| spl8_263
| spl8_265
| spl8_267 ),
inference(sat_conversion,[],[f1698]) ).
cnf(s205,plain,
( spl8_262
| spl8_264
| spl8_266
| spl8_268 ),
inference(sat_conversion,[],[f1701]) ).
cnf(s207,plain,
( spl8_244
| ~ spl8_269 ),
inference(sat_conversion,[],[f1707]) ).
cnf(s211,plain,
( spl8_268
| ~ spl8_271 ),
inference(sat_conversion,[],[f1717]) ).
cnf(s228,plain,
( spl8_250
| ~ spl8_272 ),
inference(sat_conversion,[],[f1744]) ).
cnf(s234,plain,
( spl8_158
| ~ spl8_270 ),
inference(sat_conversion,[],[f1756]) ).
cnf(s238,plain,
( spl8_192
| ~ spl8_217 ),
inference(sat_conversion,[],[f1763]) ).
cnf(s240,plain,
( spl8_206
| ~ spl8_218 ),
inference(sat_conversion,[],[f1768]) ).
cnf(s246,plain,
( spl8_198
| ~ spl8_220 ),
inference(sat_conversion,[],[f1784]) ).
cnf(s255,plain,
( spl8_189
| ~ spl8_217 ),
inference(sat_conversion,[],[f1801]) ).
cnf(s256,plain,
( spl8_185
| ~ spl8_217 ),
inference(sat_conversion,[],[f1803]) ).
cnf(s257,plain,
( spl8_182
| ~ spl8_217 ),
inference(sat_conversion,[],[f1805]) ).
cnf(s258,plain,
( spl8_178
| ~ spl8_217 ),
inference(sat_conversion,[],[f1807]) ).
cnf(s259,plain,
( spl8_175
| ~ spl8_217 ),
inference(sat_conversion,[],[f1809]) ).
cnf(s260,plain,
( spl8_137
| ~ spl8_217 ),
inference(sat_conversion,[],[f1811]) ).
cnf(s262,plain,
spl8_166,
inference(sat_conversion,[],[f1813]) ).
cnf(s263,plain,
spl8_150,
inference(sat_conversion,[],[f1814]) ).
cnf(s273,plain,
( ~ spl8_143
| ~ spl8_151 ),
inference(sat_conversion,[],[f1855]) ).
cnf(s279,plain,
( ~ spl8_158
| ~ spl8_166 ),
inference(sat_conversion,[],[f1884]) ).
cnf(s282,plain,
( spl8_241
| ~ spl8_269 ),
inference(sat_conversion,[],[f1890]) ).
cnf(s283,plain,
( spl8_237
| ~ spl8_269 ),
inference(sat_conversion,[],[f1892]) ).
cnf(s284,plain,
( spl8_234
| ~ spl8_269 ),
inference(sat_conversion,[],[f1894]) ).
cnf(s285,plain,
( spl8_230
| ~ spl8_269 ),
inference(sat_conversion,[],[f1896]) ).
cnf(s286,plain,
( spl8_227
| ~ spl8_269 ),
inference(sat_conversion,[],[f1898]) ).
cnf(s292,plain,
( ~ spl8_176
| ~ spl8_182 ),
inference(sat_conversion,[],[f1923]) ).
cnf(s303,plain,
( ~ spl8_186
| ~ spl8_192 ),
inference(sat_conversion,[],[f1964]) ).
cnf(s307,plain,
( ~ spl8_194
| ~ spl8_202 ),
inference(sat_conversion,[],[f1978]) ).
cnf(s309,plain,
( ~ spl8_196
| ~ spl8_204 ),
inference(sat_conversion,[],[f1985]) ).
cnf(s347,plain,
( ~ spl8_172
| ~ spl8_178 ),
inference(sat_conversion,[],[f2110]) ).
cnf(s358,plain,
( spl8_34
| ~ spl8_134
| ~ spl8_174
| ~ spl8_192 ),
inference(sat_conversion,[],[f2128]) ).
cnf(s365,plain,
( spl8_34
| ~ spl8_134
| ~ spl8_138
| ~ spl8_150 ),
inference(sat_conversion,[],[f2136]) ).
cnf(s387,plain,
( ~ spl8_34
| ~ spl8_134 ),
inference(sat_conversion,[],[f2150]) ).
cnf(s408,plain,
( ~ spl8_169
| ~ spl8_175 ),
inference(sat_conversion,[],[f2204]) ).
cnf(s419,plain,
( ~ spl8_182
| ~ spl8_188 ),
inference(sat_conversion,[],[f2249]) ).
cnf(s427,plain,
( ~ spl8_193
| ~ spl8_197 ),
inference(sat_conversion,[],[f2303]) ).
cnf(s445,plain,
( spl8_170
| ~ spl8_219 ),
inference(sat_conversion,[],[f2331]) ).
cnf(s447,plain,
( spl8_173
| ~ spl8_219 ),
inference(sat_conversion,[],[f2336]) ).
cnf(s453,plain,
( ~ spl8_212
| ~ spl8_214 ),
inference(sat_conversion,[],[f2392]) ).
cnf(s471,plain,
( ~ spl8_224
| ~ spl8_230 ),
inference(sat_conversion,[],[f2492]) ).
cnf(s472,plain,
( ~ spl8_227
| ~ spl8_233 ),
inference(sat_conversion,[],[f2496]) ).
cnf(s473,plain,
( ~ spl8_225
| ~ spl8_237 ),
inference(sat_conversion,[],[f2500]) ).
cnf(s474,plain,
( ~ spl8_234
| ~ spl8_240 ),
inference(sat_conversion,[],[f2504]) ).
cnf(s482,plain,
( ~ spl8_162
| ~ spl8_166 ),
inference(sat_conversion,[],[f2538]) ).
cnf(s484,plain,
( ~ spl8_246
| ~ spl8_254 ),
inference(sat_conversion,[],[f2545]) ).
cnf(s488,plain,
( ~ spl8_154
| ~ spl8_166 ),
inference(sat_conversion,[],[f2564]) ).
cnf(s525,plain,
( spl8_222
| ~ spl8_271 ),
inference(sat_conversion,[],[f2678]) ).
cnf(s527,plain,
( spl8_225
| ~ spl8_271 ),
inference(sat_conversion,[],[f2683]) ).
cnf(s533,plain,
( ~ spl8_223
| ~ spl8_241 ),
inference(sat_conversion,[],[f2711]) ).
cnf(s542,plain,
( ~ spl8_161
| ~ spl8_165 ),
inference(sat_conversion,[],[f2745]) ).
cnf(s546,plain,
( ~ spl8_225
| ~ spl8_243 ),
inference(sat_conversion,[],[f2762]) ).
cnf(s547,plain,
( ~ spl8_157
| ~ spl8_165 ),
inference(sat_conversion,[],[f2766]) ).
cnf(s548,plain,
( ~ spl8_224
| ~ spl8_236 ),
inference(sat_conversion,[],[f2770]) ).
cnf(s584,plain,
( spl8_88
| ~ spl8_150 ),
inference(sat_conversion,[],[f2918]) ).
cnf(s590,plain,
( ~ spl8_166
| ~ spl8_250 ),
inference(sat_conversion,[],[f3056]) ).
cnf(s606,plain,
( ~ spl8_166
| spl8_254 ),
inference(sat_conversion,[],[f3060]) ).
cnf(s607,plain,
( ~ spl8_166
| ~ spl8_242 ),
inference(sat_conversion,[],[f3065]) ).
cnf(s612,plain,
( ~ spl8_166
| ~ spl8_259 ),
inference(sat_conversion,[],[f3071]) ).
cnf(s614,plain,
( ~ spl8_166
| ~ spl8_257 ),
inference(sat_conversion,[],[f3073]) ).
cnf(s626,plain,
( ~ spl8_232
| ~ spl8_238 ),
inference(sat_conversion,[],[f3120]) ).
cnf(s628,plain,
( ~ spl8_225
| ~ spl8_231 ),
inference(sat_conversion,[],[f3127]) ).
cnf(s629,plain,
( ~ spl8_222
| ~ spl8_245 ),
inference(sat_conversion,[],[f3128]) ).
cnf(s633,plain,
( spl8_153
| ~ spl8_269 ),
inference(sat_conversion,[],[f3131]) ).
cnf(s667,plain,
( ~ spl8_148
| ~ spl8_202 ),
inference(sat_conversion,[],[f3270]) ).
cnf(s668,plain,
( ~ spl8_150
| spl8_202 ),
inference(sat_conversion,[],[f3271]) ).
cnf(s678,plain,
( ~ spl8_170
| ~ spl8_193 ),
inference(sat_conversion,[],[f3302]) ).
cnf(s684,plain,
( ~ spl8_172
| ~ spl8_173 ),
inference(sat_conversion,[],[f3308]) ).
cnf(s710,plain,
( ~ spl8_150
| ~ spl8_206 ),
inference(sat_conversion,[],[f3325]) ).
cnf(s738,plain,
( ~ spl8_179
| ~ spl8_185 ),
inference(sat_conversion,[],[f3379]) ).
cnf(s739,plain,
( ~ spl8_175
| ~ spl8_199 ),
inference(sat_conversion,[],[f3384]) ).
cnf(s741,plain,
( ~ spl8_198
| ~ spl8_202 ),
inference(sat_conversion,[],[f3405]) ).
cnf(s751,plain,
( spl8_83
| ~ spl8_150
| ~ spl8_202 ),
inference(sat_conversion,[],[f3492]) ).
cnf(s752,plain,
( ~ spl8_15
| ~ spl8_19
| spl8_74
| ~ spl8_83
| ~ spl8_195
| ~ spl8_247 ),
inference(sat_conversion,[],[f3495]) ).
cnf(s773,plain,
( spl8_15
| ~ spl8_150
| ~ spl8_193
| ~ spl8_202 ),
inference(sat_conversion,[],[f3670]) ).
cnf(s775,plain,
( ~ spl8_15
| spl8_65
| ~ spl8_137
| ~ spl8_153 ),
inference(sat_conversion,[],[f3677]) ).
cnf(s776,plain,
( ~ spl8_15
| ~ spl8_19
| spl8_66
| ~ spl8_175
| ~ spl8_227 ),
inference(sat_conversion,[],[f3686]) ).
cnf(s777,plain,
( ~ spl8_15
| spl8_67
| ~ spl8_83
| ~ spl8_182
| ~ spl8_234 ),
inference(sat_conversion,[],[f3696]) ).
cnf(s778,plain,
( ~ spl8_15
| spl8_68
| ~ spl8_88
| ~ spl8_189
| ~ spl8_241 ),
inference(sat_conversion,[],[f3706]) ).
cnf(s779,plain,
( ~ spl8_15
| ~ spl8_19
| spl8_69
| ~ spl8_178
| ~ spl8_230 ),
inference(sat_conversion,[],[f3716]) ).
cnf(s780,plain,
( ~ spl8_19
| spl8_70
| ~ spl8_88
| ~ spl8_150
| ~ spl8_166 ),
inference(sat_conversion,[],[f3725]) ).
cnf(s781,plain,
( ~ spl8_15
| ~ spl8_19
| spl8_71
| ~ spl8_83
| ~ spl8_193
| ~ spl8_245 ),
inference(sat_conversion,[],[f3734]) ).
cnf(s782,plain,
( ~ spl8_19
| spl8_72
| ~ spl8_83
| ~ spl8_88
| ~ spl8_202
| ~ spl8_254 ),
inference(sat_conversion,[],[f3744]) ).
cnf(s783,plain,
( ~ spl8_15
| spl8_73
| ~ spl8_83
| ~ spl8_185
| ~ spl8_237 ),
inference(sat_conversion,[],[f3754]) ).
cnf(s784,plain,
( spl8_75
| ~ spl8_83
| ~ spl8_88
| ~ spl8_151
| ~ spl8_167 ),
inference(sat_conversion,[],[f3763]) ).
cnf(s786,plain,
( ~ spl8_15
| spl8_77
| ~ spl8_88
| ~ spl8_192
| ~ spl8_244 ),
inference(sat_conversion,[],[f3782]) ).
cnf(s787,plain,
( ~ spl8_19
| spl8_78
| ~ spl8_83
| ~ spl8_88
| ~ spl8_204
| ~ spl8_256 ),
inference(sat_conversion,[],[f3792]) ).
cnf(s788,plain,
( ~ spl8_19
| spl8_79
| ~ spl8_83
| ~ spl8_88
| ~ spl8_212
| ~ spl8_264 ),
inference(sat_conversion,[],[f3802]) ).
cnf(s789,plain,
( ~ spl8_15
| spl8_80
| ~ spl8_88
| ~ spl8_140
| ~ spl8_156 ),
inference(sat_conversion,[],[f3811]) ).
cnf(s792,plain,
( ~ spl8_247
| ~ spl8_261 ),
inference(sat_conversion,[],[f3832]) ).
cnf(s794,plain,
( ~ spl8_254
| ~ spl8_265 ),
inference(sat_conversion,[],[f3834]) ).
cnf(s795,plain,
( ~ spl8_241
| ~ spl8_267 ),
inference(sat_conversion,[],[f3835]) ).
cnf(s801,plain,
( ~ spl8_19
| spl8_76
| ~ spl8_83
| ~ spl8_88
| ~ spl8_211
| ~ spl8_263 ),
inference(sat_conversion,[],[f3844]) ).
cnf(s804,plain,
( ~ spl8_150
| ~ spl8_205 ),
inference(sat_conversion,[],[f3856]) ).
cnf(s808,plain,
( ~ spl8_192
| ~ spl8_216 ),
inference(sat_conversion,[],[f3873]) ).
cnf(s809,plain,
( ~ spl8_193
| ~ spl8_210 ),
inference(sat_conversion,[],[f3874]) ).
cnf(s822,plain,
( ~ spl8_244
| ~ spl8_268 ),
inference(sat_conversion,[],[f3909]) ).
cnf(s824,plain,
( ~ spl8_234
| ~ spl8_266 ),
inference(sat_conversion,[],[f3911]) ).
cnf(s826,plain,
( ~ spl8_237
| ~ spl8_255 ),
inference(sat_conversion,[],[f3913]) ).
cnf(s827,plain,
( ~ spl8_227
| ~ spl8_251 ),
inference(sat_conversion,[],[f3914]) ).
cnf(s837,plain,
( ~ spl8_245
| ~ spl8_262 ),
inference(sat_conversion,[],[f3933]) ).
cnf(s839,plain,
~ spl8_205,
inference(rat,[],[s804,s263]) ).
cnf(s840,plain,
~ spl8_206,
inference(rat,[],[s710,s263]) ).
cnf(s845,plain,
spl8_202,
inference(rat,[],[s668,s263]) ).
cnf(s846,plain,
spl8_88,
inference(rat,[],[s584,s263]) ).
cnf(s849,plain,
~ spl8_198,
inference(rat,[],[s741,s845]) ).
cnf(s851,plain,
~ spl8_148,
inference(rat,[],[s667,s845]) ).
cnf(s852,plain,
~ spl8_194,
inference(rat,[],[s307,s845]) ).
cnf(s853,plain,
spl8_83,
inference(rat,[],[s751,s263,s845]) ).
cnf(s856,plain,
~ spl8_257,
inference(rat,[],[s614,s262]) ).
cnf(s857,plain,
~ spl8_259,
inference(rat,[],[s612,s262]) ).
cnf(s860,plain,
~ spl8_242,
inference(rat,[],[s607,s262]) ).
cnf(s861,plain,
spl8_254,
inference(rat,[],[s606,s262]) ).
cnf(s862,plain,
~ spl8_250,
inference(rat,[],[s590,s262]) ).
cnf(s863,plain,
~ spl8_154,
inference(rat,[],[s488,s262]) ).
cnf(s864,plain,
~ spl8_162,
inference(rat,[],[s482,s262]) ).
cnf(s865,plain,
~ spl8_158,
inference(rat,[],[s279,s262]) ).
cnf(s866,plain,
~ spl8_265,
inference(rat,[],[s794,s861]) ).
cnf(s867,plain,
~ spl8_246,
inference(rat,[],[s484,s861]) ).
cnf(s868,plain,
~ spl8_220,
inference(rat,[],[s246,s849]) ).
cnf(s869,plain,
~ spl8_218,
inference(rat,[],[s240,s840]) ).
cnf(s870,plain,
~ spl8_270,
inference(rat,[],[s234,s865]) ).
cnf(s871,plain,
~ spl8_272,
inference(rat,[],[s228,s862]) ).
cnf(s873,plain,
( spl8_261
| spl8_263
| spl8_267 ),
inference(rat,[],[s202,s866]) ).
cnf(s874,plain,
( spl8_247
| spl8_251
| spl8_255 ),
inference(rat,[],[s200,s857]) ).
cnf(s878,plain,
( spl8_269
| spl8_271 ),
inference(rat,[],[s190,s871,s870]) ).
cnf(s882,plain,
( spl8_156
| spl8_223
| spl8_261 ),
inference(rat,[],[s183,s867]) ).
cnf(s883,plain,
( spl8_167
| spl8_240
| spl8_268 ),
inference(rat,[],[s181,s856]) ).
cnf(s886,plain,
( spl8_233
| spl8_255
| spl8_256 ),
inference(rat,[],[s171,s864]) ).
cnf(s890,plain,
( spl8_224
| spl8_245 ),
inference(rat,[],[s166,s867,s863]) ).
cnf(s891,plain,
( spl8_165
| spl8_243
| spl8_244 ),
inference(rat,[],[s165,s860]) ).
cnf(s899,plain,
( spl8_217
| spl8_219 ),
inference(rat,[],[s141,s868,s869]) ).
cnf(s902,plain,
( spl8_186
| spl8_204
| spl8_214 ),
inference(rat,[],[s137,s851]) ).
cnf(s905,plain,
( spl8_151
| spl8_188
| spl8_216 ),
inference(rat,[],[s132,s839]) ).
cnf(s910,plain,
( spl8_138
| spl8_172
| spl8_193 ),
inference(rat,[],[s117,s852]) ).
cnf(s916,plain,
spl8_72,
inference(rat,[],[s782,s861,s845,s846,s853,s99]) ).
cnf(s917,plain,
spl8_70,
inference(rat,[],[s780,s262,s263,s846,s99]) ).
cnf(s918,plain,
~ spl8_34,
inference(rat,[],[s387,s97]) ).
cnf(s919,plain,
~ spl8_138,
inference(rat,[],[s365,s263,s97,s918]) ).
cnf(s929,plain,
( spl8_11
| spl8_16
| ~ spl8_65
| ~ spl8_66
| ~ spl8_67
| ~ spl8_68
| ~ spl8_69
| ~ spl8_71
| ~ spl8_73
| ~ spl8_74
| ~ spl8_75
| ~ spl8_76
| ~ spl8_77
| ~ spl8_78
| ~ spl8_79
| ~ spl8_80 ),
inference(rat,[],[s62,s846,s853,s916,s917]) ).
cnf(s943,plain,
~ spl8_16,
inference(rat,[],[s15,s99]) ).
cnf(s945,plain,
~ spl8_219,
inference(rat,[],[s910,s678,s684,s445,s447,s919]) ).
cnf(s946,plain,
spl8_217,
inference(rat,[],[s899,s945]) ).
cnf(s947,plain,
spl8_137,
inference(rat,[],[s260,s946]) ).
cnf(s948,plain,
spl8_175,
inference(rat,[],[s259,s946]) ).
cnf(s949,plain,
spl8_178,
inference(rat,[],[s258,s946]) ).
cnf(s950,plain,
spl8_182,
inference(rat,[],[s257,s946]) ).
cnf(s951,plain,
spl8_185,
inference(rat,[],[s256,s946]) ).
cnf(s952,plain,
spl8_189,
inference(rat,[],[s255,s946]) ).
cnf(s953,plain,
spl8_192,
inference(rat,[],[s238,s946]) ).
cnf(s960,plain,
~ spl8_199,
inference(rat,[],[s739,s948]) ).
cnf(s961,plain,
~ spl8_169,
inference(rat,[],[s408,s948]) ).
cnf(s963,plain,
~ spl8_172,
inference(rat,[],[s347,s949]) ).
cnf(s964,plain,
~ spl8_188,
inference(rat,[],[s419,s950]) ).
cnf(s966,plain,
~ spl8_176,
inference(rat,[],[s292,s950]) ).
cnf(s968,plain,
~ spl8_179,
inference(rat,[],[s738,s951]) ).
cnf(s974,plain,
~ spl8_216,
inference(rat,[],[s808,s953]) ).
cnf(s976,plain,
~ spl8_186,
inference(rat,[],[s303,s953]) ).
cnf(s977,plain,
~ spl8_174,
inference(rat,[],[s358,s918,s97,s953]) ).
cnf(s979,plain,
spl8_193,
inference(rat,[],[s910,s919,s963]) ).
cnf(s980,plain,
spl8_151,
inference(rat,[],[s905,s974,s964]) ).
cnf(s982,plain,
~ spl8_210,
inference(rat,[],[s809,s979]) ).
cnf(s983,plain,
~ spl8_197,
inference(rat,[],[s427,s979]) ).
cnf(s985,plain,
spl8_15,
inference(rat,[],[s773,s845,s263,s979]) ).
cnf(s987,plain,
~ spl8_143,
inference(rat,[],[s273,s980]) ).
cnf(s988,plain,
~ spl8_11,
inference(rat,[],[s12,s985]) ).
cnf(s989,plain,
spl8_212,
inference(rat,[],[s128,s983,s966,s987]) ).
cnf(s990,plain,
spl8_211,
inference(rat,[],[s127,s968,s960,s987]) ).
cnf(s991,plain,
~ spl8_214,
inference(rat,[],[s453,s989]) ).
cnf(s995,plain,
spl8_204,
inference(rat,[],[s902,s976,s991]) ).
cnf(s998,plain,
~ spl8_196,
inference(rat,[],[s309,s995]) ).
cnf(s999,plain,
spl8_195,
inference(rat,[],[s118,s961,s919,s998]) ).
cnf(s1000,plain,
spl8_140,
inference(rat,[],[s133,s982,s977,s998]) ).
cnf(s1007,plain,
~ spl8_271,
inference(rat,[],[s626,s163,s161,s471,s548,s542,s547,s890,s891,s822,s629,s473,s546,s628,s211,s525,s527]) ).
cnf(s1008,plain,
spl8_269,
inference(rat,[],[s878,s1007]) ).
cnf(s1009,plain,
spl8_153,
inference(rat,[],[s633,s1008]) ).
cnf(s1010,plain,
spl8_227,
inference(rat,[],[s286,s1008]) ).
cnf(s1011,plain,
spl8_230,
inference(rat,[],[s285,s1008]) ).
cnf(s1012,plain,
spl8_234,
inference(rat,[],[s284,s1008]) ).
cnf(s1013,plain,
spl8_237,
inference(rat,[],[s283,s1008]) ).
cnf(s1014,plain,
spl8_241,
inference(rat,[],[s282,s1008]) ).
cnf(s1015,plain,
spl8_244,
inference(rat,[],[s207,s1008]) ).
cnf(s1020,plain,
spl8_65,
inference(rat,[],[s775,s985,s947,s1009]) ).
cnf(s1021,plain,
~ spl8_251,
inference(rat,[],[s827,s1010]) ).
cnf(s1022,plain,
~ spl8_233,
inference(rat,[],[s472,s1010]) ).
cnf(s1025,plain,
spl8_66,
inference(rat,[],[s776,s985,s948,s99,s1010]) ).
cnf(s1027,plain,
~ spl8_224,
inference(rat,[],[s471,s1011]) ).
cnf(s1029,plain,
spl8_69,
inference(rat,[],[s779,s985,s949,s99,s1011]) ).
cnf(s1030,plain,
~ spl8_266,
inference(rat,[],[s824,s1012]) ).
cnf(s1032,plain,
~ spl8_240,
inference(rat,[],[s474,s1012]) ).
cnf(s1034,plain,
spl8_67,
inference(rat,[],[s777,s985,s950,s853,s1012]) ).
cnf(s1035,plain,
~ spl8_255,
inference(rat,[],[s826,s1013]) ).
cnf(s1039,plain,
spl8_73,
inference(rat,[],[s783,s985,s951,s853,s1013]) ).
cnf(s1041,plain,
~ spl8_267,
inference(rat,[],[s795,s1014]) ).
cnf(s1042,plain,
~ spl8_223,
inference(rat,[],[s533,s1014]) ).
cnf(s1046,plain,
spl8_68,
inference(rat,[],[s778,s985,s952,s846,s1014]) ).
cnf(s1047,plain,
~ spl8_268,
inference(rat,[],[s822,s1015]) ).
cnf(s1050,plain,
spl8_77,
inference(rat,[],[s786,s985,s953,s846,s1015]) ).
cnf(s1051,plain,
spl8_247,
inference(rat,[],[s874,s1035,s1021]) ).
cnf(s1052,plain,
spl8_245,
inference(rat,[],[s890,s1027]) ).
cnf(s1053,plain,
spl8_167,
inference(rat,[],[s883,s1047,s1032]) ).
cnf(s1054,plain,
spl8_256,
inference(rat,[],[s886,s1022,s1035]) ).
cnf(s1055,plain,
~ spl8_261,
inference(rat,[],[s792,s1051]) ).
cnf(s1057,plain,
spl8_74,
inference(rat,[],[s752,s999,s985,s853,s99,s1051]) ).
cnf(s1058,plain,
~ spl8_262,
inference(rat,[],[s837,s1052]) ).
cnf(s1062,plain,
spl8_71,
inference(rat,[],[s781,s985,s979,s853,s99,s1052]) ).
cnf(s1067,plain,
spl8_75,
inference(rat,[],[s784,s980,s853,s846,s1053]) ).
cnf(s1071,plain,
spl8_78,
inference(rat,[],[s787,s995,s99,s846,s853,s1054]) ).
cnf(s1072,plain,
spl8_263,
inference(rat,[],[s873,s1041,s1055]) ).
cnf(s1073,plain,
spl8_156,
inference(rat,[],[s882,s1042,s1055]) ).
cnf(s1074,plain,
spl8_264,
inference(rat,[],[s205,s1047,s1030,s1058]) ).
cnf(s1077,plain,
spl8_76,
inference(rat,[],[s801,s990,s99,s846,s853,s1072]) ).
cnf(s1081,plain,
spl8_80,
inference(rat,[],[s789,s1000,s985,s846,s1073]) ).
cnf(s1084,plain,
spl8_79,
inference(rat,[],[s788,s989,s99,s846,s853,s1074]) ).
cnf(s1085,plain,
$false,
inference(rat,[],[s929,s1071,s1084,s1057,s1050,s988,s1067,s1020,s1039,s1062,s1029,s1046,s1034,s1025,s943,s1077,s1081]) ).
fof(f3936,plain,
$false,
inference(avatar_sat_refutation,[],[s1085]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG038+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.08/0.19 % Computer : n011.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 19:20:01 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/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.83/0.38 % (3686530)Will run a generic schedule for satisfiability detection.
% 0.83/0.38 % (3686546)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1480539413:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.83/0.38 % (3686543)% WARNING: option uhcvi not known.
% 0.83/0.38 % (3686542)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2892958814_2999 on theBenchmark for (2999ds/0Mi)
% 0.83/0.38 % (3686544)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=223357094:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.83/0.38 % (3686543)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3353848765:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.83/0.38 % (3686547)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1694593790:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.83/0.38 % (3686545)dis+10_1_sil=32000:sp=arity:random_seed=2460294986:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.83/0.38 % (3686548)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=965285532:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.83/0.38 % (3686546)Instruction limit reached!
% 0.83/0.38 % (3686546)------------------------------
% 0.83/0.38 % (3686546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.83/0.38 % (3686546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.83/0.38 % (3686546)CaDiCaL version: 2.1.3
% 0.83/0.38 % (3686546)Termination reason: Instruction limit
% 0.83/0.38 % (3686546)Termination phase: Saturation
% 0.83/0.38 % (3686546)Time elapsed: 0.033 s
% 0.83/0.38 % (3686546)Peak memory usage: 13 MB
% 0.83/0.38 % (3686546)Instructions burned: 118 (million)
% 0.83/0.38 % Detected minimum model sizes of [8]
% 0.83/0.38 % Detected maximum model sizes of [max]
% 0.83/0.38 % TRYING [8]
% 0.83/0.38 % (3686563)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=547953455:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.83/0.38 % Detected minimum model sizes of [8]
% 0.83/0.38 % Detected maximum model sizes of [max]
% 0.83/0.38 % TRYING [8]
% 0.83/0.38 % (3686545)Instruction limit reached!
% 0.83/0.38 % (3686545)------------------------------
% 0.83/0.38 % (3686545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.83/0.38 % (3686545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.83/0.38 % (3686545)CaDiCaL version: 2.1.3
% 0.83/0.38 % (3686545)Termination reason: Instruction limit
% 0.83/0.38 % (3686545)Termination phase: Saturation
% 0.83/0.38 % (3686545)Time elapsed: 0.053 s
% 0.83/0.38 % (3686545)Peak memory usage: 12 MB
% 0.83/0.38 % (3686545)Instructions burned: 104 (million)
% 0.83/0.38 % (3686547)Instruction limit reached!
% 0.83/0.38 % (3686547)------------------------------
% 0.83/0.38 % (3686547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.83/0.38 % (3686547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.83/0.38 % (3686547)CaDiCaL version: 2.1.3
% 0.83/0.38 % (3686547)Termination reason: Instruction limit
% 0.83/0.38 % (3686547)Termination phase: Saturation
% 0.83/0.38 % (3686547)Time elapsed: 0.072 s
% 0.83/0.38 % (3686547)Peak memory usage: 13 MB
% 0.83/0.38 % (3686547)Instructions burned: 131 (million)
% 0.83/0.38 % (3686574)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3741139985:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 0.83/0.38 % (3686543) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3686530-3686543"...
% 0.83/0.38 % (3686548)Instruction limit reached!
% 0.83/0.38 % (3686548)------------------------------
% 0.83/0.38 % (3686548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.83/0.38 % (3686548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.83/0.38 % (3686548)CaDiCaL version: 2.1.3
% 0.83/0.38 % (3686548)Termination reason: Instruction limit
% 0.83/0.38 % (3686548)Termination phase: Saturation
% 0.83/0.38 % (3686548)Time elapsed: 0.086 s
% 0.83/0.38 % (3686548)Peak memory usage: 13 MB
% 0.83/0.38 % (3686548)Instructions burned: 159 (million)
% 0.83/0.38 % (3686581)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=771536452:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.83/0.38 % (3686543)...printing done.
% 0.83/0.38 % (3686543)Refutation found. Thanks to Tanya!
% 0.83/0.38 % SZS status Theorem for theBenchmark
% 0.83/0.38 % SZS output start Proof for theBenchmark
% See solution above
% 0.83/0.39 % (3686543)------------------------------
% 0.83/0.39 % (3686543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.83/0.39 % (3686543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.83/0.39 % (3686543)CaDiCaL version: 2.1.3
% 0.83/0.39 % (3686543)Termination reason: Refutation
% 0.83/0.39 % (3686543)Time elapsed: 0.097 s
% 0.83/0.39 % (3686543)Peak memory usage: 14 MB
% 0.83/0.39 % (3686543)Instructions burned: 188 (million)
% 0.83/0.39 % (3686530)Success in time 0.151 s
% 0.83/0.39 % Vampire exiting
%------------------------------------------------------------------------------