%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG117+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 : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:22:48 AM UTC 2026
% Result : Theorem 0.39s 0.33s
% Output : Refutation 0.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 136
% Syntax : Number of formulae : 948 ( 166 unt; 120 def)
% Number of atoms : 3429 (1563 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 4019 (1538 ~;1911 |; 450 &)
% ( 120 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 124 ( 122 usr; 123 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e10) = e11
| op1(e10,e10) = e12
| op1(e10,e10) = e13 )
& ( op1(e10,e11) = e10
| op1(e10,e11) = e11
| op1(e10,e11) = e12
| op1(e10,e11) = e13 )
& ( op1(e10,e12) = e10
| op1(e10,e12) = e11
| op1(e10,e12) = e12
| op1(e10,e12) = e13 )
& ( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e12
| op1(e10,e13) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 )
& ( op1(e11,e11) = e10
| op1(e11,e11) = e11
| op1(e11,e11) = e12
| op1(e11,e11) = e13 )
& ( op1(e11,e12) = e10
| op1(e11,e12) = e11
| op1(e11,e12) = e12
| op1(e11,e12) = e13 )
& ( op1(e11,e13) = e10
| op1(e11,e13) = e11
| op1(e11,e13) = e12
| op1(e11,e13) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e10) = e11
| op1(e12,e10) = e12
| op1(e12,e10) = e13 )
& ( op1(e12,e11) = e10
| op1(e12,e11) = e11
| op1(e12,e11) = e12
| op1(e12,e11) = e13 )
& ( op1(e12,e12) = e10
| op1(e12,e12) = e11
| op1(e12,e12) = e12
| op1(e12,e12) = e13 )
& ( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12
| op1(e12,e13) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e10) = e11
| op1(e13,e10) = e12
| op1(e13,e10) = e13 )
& ( op1(e13,e11) = e10
| op1(e13,e11) = e11
| op1(e13,e11) = e12
| op1(e13,e11) = e13 )
& ( op1(e13,e12) = e10
| op1(e13,e12) = e11
| op1(e13,e12) = e12
| op1(e13,e12) = e13 )
& ( op1(e13,e13) = e10
| op1(e13,e13) = e11
| op1(e13,e13) = e12
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e11) = e10
| op1(e10,e12) = e10
| op1(e10,e13) = e10 )
& ( op1(e10,e10) = e10
| op1(e11,e10) = e10
| op1(e12,e10) = e10
| op1(e13,e10) = e10 )
& ( op1(e10,e10) = e11
| op1(e10,e11) = e11
| op1(e10,e12) = e11
| op1(e10,e13) = e11 )
& ( op1(e10,e10) = e11
| op1(e11,e10) = e11
| op1(e12,e10) = e11
| op1(e13,e10) = e11 )
& ( op1(e10,e10) = e12
| op1(e10,e11) = e12
| op1(e10,e12) = e12
| op1(e10,e13) = e12 )
& ( op1(e10,e10) = e12
| op1(e11,e10) = e12
| op1(e12,e10) = e12
| op1(e13,e10) = e12 )
& ( op1(e10,e10) = e13
| op1(e10,e11) = e13
| op1(e10,e12) = e13
| op1(e10,e13) = e13 )
& ( op1(e10,e10) = e13
| op1(e11,e10) = e13
| op1(e12,e10) = e13
| op1(e13,e10) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e11) = e10
| op1(e11,e12) = e10
| op1(e11,e13) = e10 )
& ( op1(e10,e11) = e10
| op1(e11,e11) = e10
| op1(e12,e11) = e10
| op1(e13,e11) = e10 )
& ( op1(e11,e10) = e11
| op1(e11,e11) = e11
| op1(e11,e12) = e11
| op1(e11,e13) = e11 )
& ( op1(e10,e11) = e11
| op1(e11,e11) = e11
| op1(e12,e11) = e11
| op1(e13,e11) = e11 )
& ( op1(e11,e10) = e12
| op1(e11,e11) = e12
| op1(e11,e12) = e12
| op1(e11,e13) = e12 )
& ( op1(e10,e11) = e12
| op1(e11,e11) = e12
| op1(e12,e11) = e12
| op1(e13,e11) = e12 )
& ( op1(e11,e10) = e13
| op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e11,e13) = e13 )
& ( op1(e10,e11) = e13
| op1(e11,e11) = e13
| op1(e12,e11) = e13
| op1(e13,e11) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e11) = e10
| op1(e12,e12) = e10
| op1(e12,e13) = e10 )
& ( op1(e10,e12) = e10
| op1(e11,e12) = e10
| op1(e12,e12) = e10
| op1(e13,e12) = e10 )
& ( op1(e12,e10) = e11
| op1(e12,e11) = e11
| op1(e12,e12) = e11
| op1(e12,e13) = e11 )
& ( op1(e10,e12) = e11
| op1(e11,e12) = e11
| op1(e12,e12) = e11
| op1(e13,e12) = e11 )
& ( op1(e12,e10) = e12
| op1(e12,e11) = e12
| op1(e12,e12) = e12
| op1(e12,e13) = e12 )
& ( op1(e10,e12) = e12
| op1(e11,e12) = e12
| op1(e12,e12) = e12
| op1(e13,e12) = e12 )
& ( op1(e12,e10) = e13
| op1(e12,e11) = e13
| op1(e12,e12) = e13
| op1(e12,e13) = e13 )
& ( op1(e10,e12) = e13
| op1(e11,e12) = e13
| op1(e12,e12) = e13
| op1(e13,e12) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10 )
& ( op1(e10,e13) = e10
| op1(e11,e13) = e10
| op1(e12,e13) = e10
| op1(e13,e13) = e10 )
& ( op1(e13,e10) = e11
| op1(e13,e11) = e11
| op1(e13,e12) = e11
| op1(e13,e13) = e11 )
& ( op1(e10,e13) = e11
| op1(e11,e13) = e11
| op1(e12,e13) = e11
| op1(e13,e13) = e11 )
& ( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12
| op1(e13,e13) = e12 )
& ( op1(e10,e13) = e12
| op1(e11,e13) = e12
| op1(e12,e13) = e12
| op1(e13,e13) = e12 )
& ( op1(e13,e10) = e13
| op1(e13,e11) = e13
| op1(e13,e12) = e13
| op1(e13,e13) = e13 )
& ( op1(e10,e13) = e13
| op1(e11,e13) = e13
| op1(e12,e13) = e13
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e20) = e21
| op2(e20,e20) = e22
| op2(e20,e20) = e23 )
& ( op2(e20,e21) = e20
| op2(e20,e21) = e21
| op2(e20,e21) = e22
| op2(e20,e21) = e23 )
& ( op2(e20,e22) = e20
| op2(e20,e22) = e21
| op2(e20,e22) = e22
| op2(e20,e22) = e23 )
& ( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22
| op2(e20,e23) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e20) = e21
| op2(e21,e20) = e22
| op2(e21,e20) = e23 )
& ( op2(e21,e21) = e20
| op2(e21,e21) = e21
| op2(e21,e21) = e22
| op2(e21,e21) = e23 )
& ( op2(e21,e22) = e20
| op2(e21,e22) = e21
| op2(e21,e22) = e22
| op2(e21,e22) = e23 )
& ( op2(e21,e23) = e20
| op2(e21,e23) = e21
| op2(e21,e23) = e22
| op2(e21,e23) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e20) = e21
| op2(e22,e20) = e22
| op2(e22,e20) = e23 )
& ( op2(e22,e21) = e20
| op2(e22,e21) = e21
| op2(e22,e21) = e22
| op2(e22,e21) = e23 )
& ( op2(e22,e22) = e20
| op2(e22,e22) = e21
| op2(e22,e22) = e22
| op2(e22,e22) = e23 )
& ( op2(e22,e23) = e20
| op2(e22,e23) = e21
| op2(e22,e23) = e22
| op2(e22,e23) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e20) = e21
| op2(e23,e20) = e22
| op2(e23,e20) = e23 )
& ( op2(e23,e21) = e20
| op2(e23,e21) = e21
| op2(e23,e21) = e22
| op2(e23,e21) = e23 )
& ( op2(e23,e22) = e20
| op2(e23,e22) = e21
| op2(e23,e22) = e22
| op2(e23,e22) = e23 )
& ( op2(e23,e23) = e20
| op2(e23,e23) = e21
| op2(e23,e23) = e22
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e22) = e20
| op2(e20,e23) = e20 )
& ( op2(e20,e20) = e20
| op2(e21,e20) = e20
| op2(e22,e20) = e20
| op2(e23,e20) = e20 )
& ( op2(e20,e20) = e21
| op2(e20,e21) = e21
| op2(e20,e22) = e21
| op2(e20,e23) = e21 )
& ( op2(e20,e20) = e21
| op2(e21,e20) = e21
| op2(e22,e20) = e21
| op2(e23,e20) = e21 )
& ( op2(e20,e20) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 )
& ( op2(e20,e20) = e22
| op2(e21,e20) = e22
| op2(e22,e20) = e22
| op2(e23,e20) = e22 )
& ( op2(e20,e20) = e23
| op2(e20,e21) = e23
| op2(e20,e22) = e23
| op2(e20,e23) = e23 )
& ( op2(e20,e20) = e23
| op2(e21,e20) = e23
| op2(e22,e20) = e23
| op2(e23,e20) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e21) = e20
| op2(e21,e22) = e20
| op2(e21,e23) = e20 )
& ( op2(e20,e21) = e20
| op2(e21,e21) = e20
| op2(e22,e21) = e20
| op2(e23,e21) = e20 )
& ( op2(e21,e20) = e21
| op2(e21,e21) = e21
| op2(e21,e22) = e21
| op2(e21,e23) = e21 )
& ( op2(e20,e21) = e21
| op2(e21,e21) = e21
| op2(e22,e21) = e21
| op2(e23,e21) = e21 )
& ( op2(e21,e20) = e22
| op2(e21,e21) = e22
| op2(e21,e22) = e22
| op2(e21,e23) = e22 )
& ( op2(e20,e21) = e22
| op2(e21,e21) = e22
| op2(e22,e21) = e22
| op2(e23,e21) = e22 )
& ( op2(e21,e20) = e23
| op2(e21,e21) = e23
| op2(e21,e22) = e23
| op2(e21,e23) = e23 )
& ( op2(e20,e21) = e23
| op2(e21,e21) = e23
| op2(e22,e21) = e23
| op2(e23,e21) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e21) = e20
| op2(e22,e22) = e20
| op2(e22,e23) = e20 )
& ( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e22,e22) = e20
| op2(e23,e22) = e20 )
& ( op2(e22,e20) = e21
| op2(e22,e21) = e21
| op2(e22,e22) = e21
| op2(e22,e23) = e21 )
& ( op2(e20,e22) = e21
| op2(e21,e22) = e21
| op2(e22,e22) = e21
| op2(e23,e22) = e21 )
& ( op2(e22,e20) = e22
| op2(e22,e21) = e22
| op2(e22,e22) = e22
| op2(e22,e23) = e22 )
& ( op2(e20,e22) = e22
| op2(e21,e22) = e22
| op2(e22,e22) = e22
| op2(e23,e22) = e22 )
& ( op2(e22,e20) = e23
| op2(e22,e21) = e23
| op2(e22,e22) = e23
| op2(e22,e23) = e23 )
& ( op2(e20,e22) = e23
| op2(e21,e22) = e23
| op2(e22,e22) = e23
| op2(e23,e22) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e23) = e20 )
& ( op2(e20,e23) = e20
| op2(e21,e23) = e20
| op2(e22,e23) = e20
| op2(e23,e23) = e20 )
& ( op2(e23,e20) = e21
| op2(e23,e21) = e21
| op2(e23,e22) = e21
| op2(e23,e23) = e21 )
& ( op2(e20,e23) = e21
| op2(e21,e23) = e21
| op2(e22,e23) = e21
| op2(e23,e23) = e21 )
& ( op2(e23,e20) = e22
| op2(e23,e21) = e22
| op2(e23,e22) = e22
| op2(e23,e23) = e22 )
& ( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22
| op2(e23,e23) = e22 )
& ( op2(e23,e20) = e23
| op2(e23,e21) = e23
| op2(e23,e22) = e23
| op2(e23,e23) = e23 )
& ( op2(e20,e23) = e23
| op2(e21,e23) = e23
| op2(e22,e23) = e23
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op1(e10,e10) != op1(e11,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e12,e10) != op1(e13,e10)
& op1(e10,e11) != op1(e11,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e12,e11) != op1(e13,e11)
& op1(e10,e12) != op1(e11,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e12,e12) != op1(e13,e12)
& op1(e10,e13) != op1(e11,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e12,e13) != op1(e13,e13)
& op1(e10,e10) != op1(e10,e11)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e12) != op1(e10,e13)
& op1(e11,e10) != op1(e11,e11)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e12) != op1(e11,e13)
& op1(e12,e10) != op1(e12,e11)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e12) != op1(e12,e13)
& op1(e13,e10) != op1(e13,e11)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e12) != op1(e13,e13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( op2(e20,e20) != op2(e21,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e22,e20) != op2(e23,e20)
& op2(e20,e21) != op2(e21,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e22,e21) != op2(e23,e21)
& op2(e20,e22) != op2(e21,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e22,e22) != op2(e23,e22)
& op2(e20,e23) != op2(e21,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e22,e23) != op2(e23,e23)
& op2(e20,e20) != op2(e20,e21)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e22) != op2(e20,e23)
& op2(e21,e20) != op2(e21,e21)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e22) != op2(e21,e23)
& op2(e22,e20) != op2(e22,e21)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e22) != op2(e22,e23)
& op2(e23,e20) != op2(e23,e21)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e22) != op2(e23,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f10,axiom,
( ( ( op1(e10,e10) = e10
& op1(e10,e10) != e10 )
| ( op1(e11,e11) = e10
& op1(e11,e10) != e11 )
| ( op1(e12,e12) = e10
& op1(e12,e10) != e12 )
| ( op1(e13,e13) = e10
& op1(e13,e10) != e13 ) )
& ( ( op1(e10,e10) = e11
& op1(e10,e11) != e10 )
| ( op1(e11,e11) = e11
& op1(e11,e11) != e11 )
| ( op1(e12,e12) = e11
& op1(e12,e11) != e12 )
| ( op1(e13,e13) = e11
& op1(e13,e11) != e13 ) )
& ( ( op1(e10,e10) = e12
& op1(e10,e12) != e10 )
| ( op1(e11,e11) = e12
& op1(e11,e12) != e11 )
| ( op1(e12,e12) = e12
& op1(e12,e12) != e12 )
| ( op1(e13,e13) = e12
& op1(e13,e12) != e13 ) )
& ( ( op1(e10,e10) = e13
& op1(e10,e13) != e10 )
| ( op1(e11,e11) = e13
& op1(e11,e13) != e11 )
| ( op1(e12,e12) = e13
& op1(e12,e13) != e12 )
| ( op1(e13,e13) = e13
& op1(e13,e13) != e13 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( ( ( op2(e20,e20) = e20
& op2(e20,e20) != e20 )
| ( op2(e21,e21) = e20
& op2(e21,e20) != e21 )
| ( op2(e22,e22) = e20
& op2(e22,e20) != e22 )
| ( op2(e23,e23) = e20
& op2(e23,e20) != e23 ) )
& ( ( op2(e20,e20) = e21
& op2(e20,e21) != e20 )
| ( op2(e21,e21) = e21
& op2(e21,e21) != e21 )
| ( op2(e22,e22) = e21
& op2(e22,e21) != e22 )
| ( op2(e23,e23) = e21
& op2(e23,e21) != e23 ) )
& ( ( op2(e20,e20) = e22
& op2(e20,e22) != e20 )
| ( op2(e21,e21) = e22
& op2(e21,e22) != e21 )
| ( op2(e22,e22) = e22
& op2(e22,e22) != e22 )
| ( op2(e23,e23) = e22
& op2(e23,e22) != e23 ) )
& ( ( op2(e20,e20) = e23
& op2(e20,e23) != e20 )
| ( op2(e21,e21) = e23
& op2(e21,e23) != e21 )
| ( op2(e22,e22) = e23
& op2(e22,e23) != e22 )
| ( op2(e23,e23) = e23
& op2(e23,e23) != e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e10 = op1(e13,op1(e13,e13))
& e11 = op1(op1(e13,e13),e13)
& e12 = op1(e13,e13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e20 = op2(e23,op2(e23,e23))
& e21 = op2(op2(e23,e23),e23)
& e22 = op2(e23,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( h1(e13) = e20
& h1(e10) = op2(e20,op2(e20,e20))
& h1(e11) = op2(op2(e20,e20),e20)
& h1(e12) = op2(e20,e20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f16,axiom,
( h3(e13) = e22
& h3(e10) = op2(e22,op2(e22,e22))
& h3(e11) = op2(op2(e22,e22),e22)
& h3(e12) = op2(e22,e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
( h4(e13) = e23
& h4(e10) = op2(e23,op2(e23,e23))
& h4(e11) = op2(op2(e23,e23),e23)
& h4(e12) = op2(e23,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f18,conjecture,
( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f19,negated_conjecture,
~ ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f20,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) ) )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) ) )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) ) )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) ) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f35,plain,
( e13 = op1(e13,e12)
| e12 = op1(e13,e12)
| e11 = op1(e13,e12)
| e10 = op1(e13,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f37,plain,
( e10 = op1(e10,e13)
| e10 = op1(e10,e12)
| e10 = op1(e10,e11)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f38,plain,
( e10 = op1(e13,e10)
| e10 = op1(e12,e10)
| e10 = op1(e11,e10)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f42,plain,
( e12 = op1(e13,e10)
| e12 = op1(e12,e10)
| e12 = op1(e11,e10)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f2]) ).
fof(f47,plain,
( e11 = op1(e11,e13)
| e11 = op1(e11,e12)
| e11 = op1(e11,e11)
| e11 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f49,plain,
( e12 = op1(e11,e13)
| e12 = op1(e11,e12)
| e12 = op1(e11,e11)
| e12 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f50,plain,
( e12 = op1(e13,e11)
| e12 = op1(e12,e11)
| e12 = op1(e11,e11)
| e12 = op1(e10,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f51,plain,
( e13 = op1(e11,e13)
| e13 = op1(e11,e12)
| e13 = op1(e11,e11)
| e13 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f52,plain,
( e13 = op1(e13,e11)
| e13 = op1(e12,e11)
| e13 = op1(e11,e11)
| e13 = op1(e10,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f57,plain,
( e12 = op1(e12,e13)
| e12 = op1(e12,e12)
| e12 = op1(e12,e11)
| e12 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f58,plain,
( e12 = op1(e13,e12)
| e12 = op1(e12,e12)
| e12 = op1(e11,e12)
| e12 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f60,plain,
( e13 = op1(e13,e12)
| e13 = op1(e12,e12)
| e13 = op1(e11,e12)
| e13 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f63,plain,
( e11 = op1(e13,e13)
| e11 = op1(e13,e12)
| e11 = op1(e13,e11)
| e11 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f67,plain,
( e13 = op1(e13,e13)
| e13 = op1(e13,e12)
| e13 = op1(e13,e11)
| e13 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f71,plain,
( e23 = op2(e20,e22)
| e22 = op2(e20,e22)
| e21 = op2(e20,e22)
| e20 = op2(e20,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f81,plain,
( e23 = op2(e23,e20)
| e22 = op2(e23,e20)
| e21 = op2(e23,e20)
| e20 = op2(e23,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f91,plain,
( e23 = op2(e20,e23)
| e23 = op2(e20,e22)
| e23 = op2(e20,e21)
| op2(e20,e20) = e23 ),
inference(cnf_transformation,[],[f4]) ).
fof(f97,plain,
( e22 = op2(e21,e23)
| e22 = op2(e21,e22)
| e22 = op2(e21,e21)
| e22 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f99,plain,
( e23 = op2(e21,e23)
| e23 = op2(e21,e22)
| e23 = op2(e21,e21)
| e23 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f101,plain,
( e20 = op2(e22,e23)
| e20 = op2(e22,e22)
| e20 = op2(e22,e21)
| e20 = op2(e22,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f104,plain,
( e21 = op2(e23,e22)
| e21 = op2(e22,e22)
| e21 = op2(e21,e22)
| e21 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f105,plain,
( e22 = op2(e22,e23)
| e22 = op2(e22,e22)
| e22 = op2(e22,e21)
| e22 = op2(e22,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f110,plain,
( e20 = op2(e23,e23)
| e20 = op2(e22,e23)
| e20 = op2(e21,e23)
| e20 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f111,plain,
( e21 = op2(e23,e23)
| e21 = op2(e23,e22)
| e21 = op2(e23,e21)
| e21 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f117,plain,
op1(e13,e12) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f118,plain,
op1(e13,e11) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f120,plain,
op1(e13,e10) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f125,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f133,plain,
op1(e11,e10) != op1(e11,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f137,plain,
op1(e10,e11) != op1(e10,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f142,plain,
op1(e11,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f143,plain,
op1(e11,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f148,plain,
op1(e11,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
op1(e10,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f169,plain,
op2(e23,e20) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f171,plain,
op2(e22,e22) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f178,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f187,plain,
op2(e20,e20) != op2(e20,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f190,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f195,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f198,plain,
op2(e20,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f199,plain,
op2(e20,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f203,plain,
op2(e21,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f209,plain,
op2(e21,e20) != op2(e22,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f210,plain,
op2(e20,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f213,plain,
e12 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f214,plain,
e11 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f215,plain,
e11 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f216,plain,
e10 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f217,plain,
e10 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f218,plain,
e10 != e11,
inference(cnf_transformation,[],[f7]) ).
fof(f219,plain,
e22 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f220,plain,
e21 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f221,plain,
e21 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f222,plain,
e20 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f224,plain,
e20 != e21,
inference(cnf_transformation,[],[f8]) ).
fof(f241,plain,
( e10 = op1(e13,e13)
| e12 != op1(e12,e10)
| e10 = op1(e11,e11)
| e10 != op1(e10,e10) ),
inference(cnf_transformation,[],[f10]) ).
fof(f242,plain,
( e10 = op1(e13,e13)
| e12 != op1(e12,e10)
| e10 = op1(e11,e11)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f10]) ).
fof(f245,plain,
( e10 = op1(e13,e13)
| e10 = op1(e12,e12)
| e10 = op1(e11,e11)
| e10 != op1(e10,e10) ),
inference(cnf_transformation,[],[f10]) ).
fof(f246,plain,
( e10 = op1(e13,e13)
| e10 = op1(e12,e12)
| e10 = op1(e11,e11)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f10]) ).
fof(f247,plain,
( e10 = op1(e13,e13)
| e10 = op1(e12,e12)
| e11 != op1(e11,e10)
| e10 != op1(e10,e10) ),
inference(cnf_transformation,[],[f10]) ).
fof(f248,plain,
( e10 = op1(e13,e13)
| e10 = op1(e12,e12)
| e11 != op1(e11,e10)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f10]) ).
fof(f257,plain,
( e11 = op1(e13,e13)
| e12 != op1(e12,e11)
| e11 = op1(e11,e11)
| e10 != op1(e10,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f258,plain,
( e11 = op1(e13,e13)
| e12 != op1(e12,e11)
| e11 = op1(e11,e11)
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[],[f10]) ).
fof(f260,plain,
( e11 = op1(e13,e13)
| e12 != op1(e12,e11)
| e11 != op1(e11,e11)
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[],[f10]) ).
fof(f262,plain,
( e11 = op1(e13,e13)
| e11 = op1(e12,e12)
| e11 = op1(e11,e11)
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[],[f10]) ).
fof(f264,plain,
( e11 = op1(e13,e13)
| e11 = op1(e12,e12)
| e11 != op1(e11,e11)
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[],[f10]) ).
fof(f286,plain,
( e13 != op1(e13,e12)
| e12 = op1(e12,e12)
| e12 = op1(e11,e11)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f10]) ).
fof(f288,plain,
( e13 != op1(e13,e12)
| e12 = op1(e12,e12)
| e11 != op1(e11,e12)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f10]) ).
fof(f294,plain,
( e13 = op1(e13,e13)
| e13 = op1(e12,e12)
| e13 = op1(e11,e11)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f10]) ).
fof(f318,plain,
( e23 != op2(e23,e20)
| e20 = op2(e22,e22)
| e20 = op2(e21,e21)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f11]) ).
fof(f326,plain,
( e21 = op2(e23,e23)
| e21 = op2(e22,e22)
| e21 = op2(e21,e21)
| op2(e20,e20) = e21 ),
inference(cnf_transformation,[],[f11]) ).
fof(f328,plain,
( e21 = op2(e23,e23)
| e21 = op2(e22,e22)
| e21 != op2(e21,e21)
| op2(e20,e20) = e21 ),
inference(cnf_transformation,[],[f11]) ).
fof(f358,plain,
( e23 = op2(e23,e23)
| e23 = op2(e22,e22)
| e23 = op2(e21,e21)
| op2(e20,e20) = e23 ),
inference(cnf_transformation,[],[f11]) ).
fof(f369,plain,
e12 = op1(e13,e13),
inference(cnf_transformation,[],[f12]) ).
fof(f370,plain,
e11 = op1(op1(e13,e13),e13),
inference(cnf_transformation,[],[f12]) ).
fof(f372,plain,
e22 = op2(e23,e23),
inference(cnf_transformation,[],[f13]) ).
fof(f373,plain,
e21 = op2(op2(e23,e23),e23),
inference(cnf_transformation,[],[f13]) ).
fof(f374,plain,
e20 = op2(e23,op2(e23,e23)),
inference(cnf_transformation,[],[f13]) ).
fof(f375,plain,
op2(e20,e20) = h1(e12),
inference(cnf_transformation,[],[f14]) ).
fof(f376,plain,
h1(e11) = op2(op2(e20,e20),e20),
inference(cnf_transformation,[],[f14]) ).
fof(f377,plain,
h1(e10) = op2(e20,op2(e20,e20)),
inference(cnf_transformation,[],[f14]) ).
fof(f378,plain,
e20 = h1(e13),
inference(cnf_transformation,[],[f14]) ).
fof(f386,plain,
e22 = h3(e13),
inference(cnf_transformation,[],[f16]) ).
fof(f390,plain,
e23 = h4(e13),
inference(cnf_transformation,[],[f17]) ).
fof(f391,plain,
( e20 != h1(e13)
| ~ sP7 ),
inference(cnf_transformation,[],[f20]) ).
fof(f396,plain,
( e21 != h1(e12)
| ~ sP6 ),
inference(cnf_transformation,[],[f20]) ).
fof(f425,plain,
( e23 != h1(e10)
| e22 != h1(e11)
| sP6
| sP7
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e10)) != op2(h1(e10),h1(e10)) ),
inference(cnf_transformation,[],[f20]) ).
fof(f548,plain,
( e23 != h1(e10)
| e22 != h1(e11)
| sP6
| ~ sP7
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e10)) != op2(h1(e10),h1(e10)) ),
inference(consistent_polarity_flipping,[],[f425]) ).
fof(f570,plain,
( e20 != h1(e13)
| sP7 ),
inference(consistent_polarity_flipping,[],[f391]) ).
fof(f572,definition,
( spl8_1
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl8_1])],[avatar_definition]) ).
fof(f576,definition,
( spl8_2
<=> e20 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition]) ).
fof(f577,plain,
( e20 = h1(e13)
| ~ spl8_2 ),
inference(avatar_component_clause,[],[f576]) ).
fof(f579,plain,
( spl8_1
| ~ spl8_2 ),
inference(avatar_split_clause,[],[f570,f576,f572]) ).
fof(f596,definition,
( spl8_6
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl8_6])],[avatar_definition]) ).
fof(f605,definition,
( spl8_8
<=> e21 = h1(e12) ),
introduced(definition,[new_symbols(definition,[spl8_8])],[avatar_definition]) ).
fof(f606,plain,
( e21 = h1(e12)
| ~ spl8_8 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f608,plain,
( ~ spl8_6
| ~ spl8_8 ),
inference(avatar_split_clause,[],[f396,f605,f596]) ).
fof(f672,definition,
( spl8_22
<=> e20 = h3(e13) ),
introduced(definition,[new_symbols(definition,[spl8_22])],[avatar_definition]) ).
fof(f673,plain,
( e20 = h3(e13)
| ~ spl8_22 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f674,plain,
( e20 != h3(e13)
| spl8_22 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f744,definition,
( spl8_37
<=> e21 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl8_37])],[avatar_definition]) ).
fof(f745,plain,
( e21 = h4(e13)
| ~ spl8_37 ),
inference(avatar_component_clause,[],[f744]) ).
fof(f746,plain,
( e21 != h4(e13)
| spl8_37 ),
inference(avatar_component_clause,[],[f744]) ).
fof(f764,definition,
( spl8_41
<=> h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_41])],[avatar_definition]) ).
fof(f766,plain,
( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| spl8_41 ),
inference(avatar_component_clause,[],[f764]) ).
fof(f768,definition,
( spl8_42
<=> h1(op1(e10,e11)) = op2(h1(e10),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_42])],[avatar_definition]) ).
fof(f770,plain,
( h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| spl8_42 ),
inference(avatar_component_clause,[],[f768]) ).
fof(f772,definition,
( spl8_43
<=> h1(op1(e10,e12)) = op2(h1(e10),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_43])],[avatar_definition]) ).
fof(f774,plain,
( h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| spl8_43 ),
inference(avatar_component_clause,[],[f772]) ).
fof(f776,definition,
( spl8_44
<=> h1(op1(e10,e13)) = op2(h1(e10),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_44])],[avatar_definition]) ).
fof(f778,plain,
( h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| spl8_44 ),
inference(avatar_component_clause,[],[f776]) ).
fof(f780,definition,
( spl8_45
<=> h1(op1(e11,e10)) = op2(h1(e11),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_45])],[avatar_definition]) ).
fof(f782,plain,
( h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| spl8_45 ),
inference(avatar_component_clause,[],[f780]) ).
fof(f784,definition,
( spl8_46
<=> h1(op1(e11,e11)) = op2(h1(e11),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_46])],[avatar_definition]) ).
fof(f786,plain,
( h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| spl8_46 ),
inference(avatar_component_clause,[],[f784]) ).
fof(f788,definition,
( spl8_47
<=> h1(op1(e11,e12)) = op2(h1(e11),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_47])],[avatar_definition]) ).
fof(f790,plain,
( h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| spl8_47 ),
inference(avatar_component_clause,[],[f788]) ).
fof(f792,definition,
( spl8_48
<=> h1(op1(e11,e13)) = op2(h1(e11),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_48])],[avatar_definition]) ).
fof(f794,plain,
( h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| spl8_48 ),
inference(avatar_component_clause,[],[f792]) ).
fof(f796,definition,
( spl8_49
<=> h1(op1(e12,e10)) = op2(h1(e12),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_49])],[avatar_definition]) ).
fof(f798,plain,
( h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| spl8_49 ),
inference(avatar_component_clause,[],[f796]) ).
fof(f800,definition,
( spl8_50
<=> h1(op1(e12,e11)) = op2(h1(e12),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_50])],[avatar_definition]) ).
fof(f802,plain,
( h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| spl8_50 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f804,definition,
( spl8_51
<=> h1(op1(e12,e12)) = op2(h1(e12),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_51])],[avatar_definition]) ).
fof(f806,plain,
( h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| spl8_51 ),
inference(avatar_component_clause,[],[f804]) ).
fof(f808,definition,
( spl8_52
<=> h1(op1(e12,e13)) = op2(h1(e12),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_52])],[avatar_definition]) ).
fof(f810,plain,
( h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| spl8_52 ),
inference(avatar_component_clause,[],[f808]) ).
fof(f812,definition,
( spl8_53
<=> h1(op1(e13,e10)) = op2(h1(e13),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_53])],[avatar_definition]) ).
fof(f814,plain,
( h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| spl8_53 ),
inference(avatar_component_clause,[],[f812]) ).
fof(f816,definition,
( spl8_54
<=> h1(op1(e13,e11)) = op2(h1(e13),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_54])],[avatar_definition]) ).
fof(f818,plain,
( h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| spl8_54 ),
inference(avatar_component_clause,[],[f816]) ).
fof(f820,definition,
( spl8_55
<=> h1(op1(e13,e12)) = op2(h1(e13),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_55])],[avatar_definition]) ).
fof(f822,plain,
( h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| spl8_55 ),
inference(avatar_component_clause,[],[f820]) ).
fof(f824,definition,
( spl8_56
<=> h1(op1(e13,e13)) = op2(h1(e13),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_56])],[avatar_definition]) ).
fof(f826,plain,
( h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| spl8_56 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f832,definition,
( spl8_58
<=> e23 = h1(e10) ),
introduced(definition,[new_symbols(definition,[spl8_58])],[avatar_definition]) ).
fof(f833,plain,
( e23 = h1(e10)
| ~ spl8_58 ),
inference(avatar_component_clause,[],[f832]) ).
fof(f842,definition,
( spl8_60
<=> e22 = h1(e11) ),
introduced(definition,[new_symbols(definition,[spl8_60])],[avatar_definition]) ).
fof(f843,plain,
( e22 = h1(e11)
| ~ spl8_60 ),
inference(avatar_component_clause,[],[f842]) ).
fof(f845,plain,
( ~ spl8_41
| ~ spl8_42
| ~ spl8_43
| ~ spl8_44
| ~ spl8_45
| ~ spl8_46
| ~ spl8_47
| ~ spl8_48
| ~ spl8_49
| ~ spl8_50
| ~ spl8_51
| ~ spl8_52
| ~ spl8_53
| ~ spl8_54
| ~ spl8_55
| ~ spl8_56
| ~ spl8_1
| spl8_6
| ~ spl8_60
| ~ spl8_58 ),
inference(avatar_split_clause,[],[f548,f832,f842,f596,f572,f824,f820,f816,f812,f808,f804,f800,f796,f792,f788,f784,f780,f776,f772,f768,f764]) ).
fof(f1052,definition,
( spl8_105
<=> e22 = h3(e13) ),
introduced(definition,[new_symbols(definition,[spl8_105])],[avatar_definition]) ).
fof(f1053,plain,
( e22 = h3(e13)
| ~ spl8_105 ),
inference(avatar_component_clause,[],[f1052]) ).
fof(f1204,definition,
( spl8_136
<=> e23 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl8_136])],[avatar_definition]) ).
fof(f1205,plain,
( e23 = h4(e13)
| ~ spl8_136 ),
inference(avatar_component_clause,[],[f1204]) ).
fof(f1211,plain,
spl8_136,
inference(avatar_split_clause,[],[f390,f1204]) ).
fof(f1212,plain,
spl8_105,
inference(avatar_split_clause,[],[f386,f1052]) ).
fof(f1214,plain,
spl8_2,
inference(avatar_split_clause,[],[f378,f576]) ).
fof(f1216,definition,
( spl8_137
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl8_137])],[avatar_definition]) ).
fof(f1217,plain,
( e20 = op2(e20,e20)
| ~ spl8_137 ),
inference(avatar_component_clause,[],[f1216]) ).
fof(f1220,definition,
( spl8_138
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_138])],[avatar_definition]) ).
fof(f1222,plain,
( e20 = op2(e21,e21)
| ~ spl8_138 ),
inference(avatar_component_clause,[],[f1220]) ).
fof(f1224,definition,
( spl8_139
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_139])],[avatar_definition]) ).
fof(f1228,definition,
( spl8_140
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl8_140])],[avatar_definition]) ).
fof(f1230,plain,
( e20 = op2(e23,e23)
| ~ spl8_140 ),
inference(avatar_component_clause,[],[f1228]) ).
fof(f1240,definition,
( spl8_142
<=> e20 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl8_142])],[avatar_definition]) ).
fof(f1248,definition,
( spl8_143
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_143])],[avatar_definition]) ).
fof(f1256,plain,
( spl8_137
| spl8_138
| spl8_142
| ~ spl8_143 ),
inference(avatar_split_clause,[],[f318,f1248,f1240,f1220,f1216]) ).
fof(f1264,definition,
( spl8_145
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_145])],[avatar_definition]) ).
fof(f1268,definition,
( spl8_146
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl8_146])],[avatar_definition]) ).
fof(f1272,definition,
( spl8_147
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl8_147])],[avatar_definition]) ).
fof(f1274,plain,
( e21 = op2(e23,e23)
| ~ spl8_147 ),
inference(avatar_component_clause,[],[f1272]) ).
fof(f1277,definition,
( spl8_148
<=> op2(e20,e20) = e21 ),
introduced(definition,[new_symbols(definition,[spl8_148])],[avatar_definition]) ).
fof(f1279,plain,
( op2(e20,e20) = e21
| ~ spl8_148 ),
inference(avatar_component_clause,[],[f1277]) ).
fof(f1284,definition,
( spl8_149
<=> e21 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl8_149])],[avatar_definition]) ).
fof(f1285,plain,
( e21 != op2(e22,e22)
| spl8_149 ),
inference(avatar_component_clause,[],[f1284]) ).
fof(f1288,plain,
( spl8_148
| spl8_145
| spl8_149
| spl8_147 ),
inference(avatar_split_clause,[],[f326,f1272,f1284,f1264,f1277]) ).
fof(f1290,plain,
( spl8_148
| ~ spl8_145
| spl8_149
| spl8_147 ),
inference(avatar_split_clause,[],[f328,f1272,f1284,f1264,f1277]) ).
fof(f1304,definition,
( spl8_151
<=> e20 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_151])],[avatar_definition]) ).
fof(f1305,plain,
( e20 = op2(e20,e22)
| ~ spl8_151 ),
inference(avatar_component_clause,[],[f1304]) ).
fof(f1308,definition,
( spl8_152
<=> e22 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_152])],[avatar_definition]) ).
fof(f1310,plain,
( e22 = op2(e21,e21)
| ~ spl8_152 ),
inference(avatar_component_clause,[],[f1308]) ).
fof(f1312,definition,
( spl8_153
<=> e22 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl8_153])],[avatar_definition]) ).
fof(f1313,plain,
( e22 = op2(e22,e22)
| ~ spl8_153 ),
inference(avatar_component_clause,[],[f1312]) ).
fof(f1316,definition,
( spl8_154
<=> e22 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl8_154])],[avatar_definition]) ).
fof(f1318,plain,
( e22 = op2(e23,e23)
| ~ spl8_154 ),
inference(avatar_component_clause,[],[f1316]) ).
fof(f1326,definition,
( spl8_156
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl8_156])],[avatar_definition]) ).
fof(f1327,plain,
( e21 = op2(e21,e22)
| ~ spl8_156 ),
inference(avatar_component_clause,[],[f1326]) ).
fof(f1348,definition,
( spl8_158
<=> e20 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl8_158])],[avatar_definition]) ).
fof(f1349,plain,
( e20 = op2(e20,e23)
| ~ spl8_158 ),
inference(avatar_component_clause,[],[f1348]) ).
fof(f1352,definition,
( spl8_159
<=> e23 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_159])],[avatar_definition]) ).
fof(f1354,plain,
( e23 = op2(e21,e21)
| ~ spl8_159 ),
inference(avatar_component_clause,[],[f1352]) ).
fof(f1356,definition,
( spl8_160
<=> e22 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl8_160])],[avatar_definition]) ).
fof(f1357,plain,
( e22 = op2(e22,e23)
| ~ spl8_160 ),
inference(avatar_component_clause,[],[f1356]) ).
fof(f1360,definition,
( spl8_161
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl8_161])],[avatar_definition]) ).
fof(f1362,plain,
( e23 = op2(e23,e23)
| ~ spl8_161 ),
inference(avatar_component_clause,[],[f1360]) ).
fof(f1365,definition,
( spl8_162
<=> op2(e20,e20) = e23 ),
introduced(definition,[new_symbols(definition,[spl8_162])],[avatar_definition]) ).
fof(f1367,plain,
( op2(e20,e20) = e23
| ~ spl8_162 ),
inference(avatar_component_clause,[],[f1365]) ).
fof(f1376,definition,
( spl8_164
<=> e23 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl8_164])],[avatar_definition]) ).
fof(f1378,plain,
( e23 = op2(e22,e22)
| ~ spl8_164 ),
inference(avatar_component_clause,[],[f1376]) ).
fof(f1380,plain,
( spl8_162
| spl8_159
| spl8_164
| spl8_161 ),
inference(avatar_split_clause,[],[f358,f1360,f1376,f1352,f1365]) ).
fof(f1392,definition,
( spl8_165
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl8_165])],[avatar_definition]) ).
fof(f1393,plain,
( e10 = op1(e10,e10)
| ~ spl8_165 ),
inference(avatar_component_clause,[],[f1392]) ).
fof(f1396,definition,
( spl8_166
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_166])],[avatar_definition]) ).
fof(f1398,plain,
( e10 = op1(e11,e11)
| ~ spl8_166 ),
inference(avatar_component_clause,[],[f1396]) ).
fof(f1400,definition,
( spl8_167
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl8_167])],[avatar_definition]) ).
fof(f1404,definition,
( spl8_168
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_168])],[avatar_definition]) ).
fof(f1406,plain,
( e10 = op1(e13,e13)
| ~ spl8_168 ),
inference(avatar_component_clause,[],[f1404]) ).
fof(f1407,plain,
( ~ spl8_165
| spl8_166
| ~ spl8_167
| spl8_168 ),
inference(avatar_split_clause,[],[f241,f1404,f1400,f1396,f1392]) ).
fof(f1408,plain,
( spl8_165
| spl8_166
| ~ spl8_167
| spl8_168 ),
inference(avatar_split_clause,[],[f242,f1404,f1400,f1396,f1392]) ).
fof(f1410,definition,
( spl8_169
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_169])],[avatar_definition]) ).
fof(f1416,definition,
( spl8_170
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl8_170])],[avatar_definition]) ).
fof(f1418,plain,
( e10 = op1(e12,e12)
| ~ spl8_170 ),
inference(avatar_component_clause,[],[f1416]) ).
fof(f1419,plain,
( ~ spl8_165
| spl8_166
| spl8_170
| spl8_168 ),
inference(avatar_split_clause,[],[f245,f1404,f1416,f1396,f1392]) ).
fof(f1420,plain,
( spl8_165
| spl8_166
| spl8_170
| spl8_168 ),
inference(avatar_split_clause,[],[f246,f1404,f1416,f1396,f1392]) ).
fof(f1421,plain,
( ~ spl8_165
| ~ spl8_169
| spl8_170
| spl8_168 ),
inference(avatar_split_clause,[],[f247,f1404,f1416,f1410,f1392]) ).
fof(f1422,plain,
( spl8_165
| ~ spl8_169
| spl8_170
| spl8_168 ),
inference(avatar_split_clause,[],[f248,f1404,f1416,f1410,f1392]) ).
fof(f1424,definition,
( spl8_171
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_171])],[avatar_definition]) ).
fof(f1425,plain,
( e13 = op1(e13,e10)
| ~ spl8_171 ),
inference(avatar_component_clause,[],[f1424]) ).
fof(f1436,definition,
( spl8_172
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl8_172])],[avatar_definition]) ).
fof(f1440,definition,
( spl8_173
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_173])],[avatar_definition]) ).
fof(f1442,plain,
( e11 = op1(e11,e11)
| ~ spl8_173 ),
inference(avatar_component_clause,[],[f1440]) ).
fof(f1444,definition,
( spl8_174
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_174])],[avatar_definition]) ).
fof(f1445,plain,
( e12 = op1(e12,e11)
| ~ spl8_174 ),
inference(avatar_component_clause,[],[f1444]) ).
fof(f1448,definition,
( spl8_175
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_175])],[avatar_definition]) ).
fof(f1450,plain,
( e11 = op1(e13,e13)
| ~ spl8_175 ),
inference(avatar_component_clause,[],[f1448]) ).
fof(f1451,plain,
( ~ spl8_172
| spl8_173
| ~ spl8_174
| spl8_175 ),
inference(avatar_split_clause,[],[f257,f1448,f1444,f1440,f1436]) ).
fof(f1453,definition,
( spl8_176
<=> op1(e10,e10) = e11 ),
introduced(definition,[new_symbols(definition,[spl8_176])],[avatar_definition]) ).
fof(f1455,plain,
( op1(e10,e10) = e11
| ~ spl8_176 ),
inference(avatar_component_clause,[],[f1453]) ).
fof(f1456,plain,
( spl8_176
| spl8_173
| ~ spl8_174
| spl8_175 ),
inference(avatar_split_clause,[],[f258,f1448,f1444,f1440,f1453]) ).
fof(f1458,plain,
( spl8_176
| ~ spl8_173
| ~ spl8_174
| spl8_175 ),
inference(avatar_split_clause,[],[f260,f1448,f1444,f1440,f1453]) ).
fof(f1460,definition,
( spl8_177
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl8_177])],[avatar_definition]) ).
fof(f1462,plain,
( e11 = op1(e12,e12)
| ~ spl8_177 ),
inference(avatar_component_clause,[],[f1460]) ).
fof(f1464,plain,
( spl8_176
| spl8_173
| spl8_177
| spl8_175 ),
inference(avatar_split_clause,[],[f262,f1448,f1460,f1440,f1453]) ).
fof(f1466,plain,
( spl8_176
| ~ spl8_173
| spl8_177
| spl8_175 ),
inference(avatar_split_clause,[],[f264,f1448,f1460,f1440,f1453]) ).
fof(f1468,definition,
( spl8_178
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_178])],[avatar_definition]) ).
fof(f1469,plain,
( e13 = op1(e13,e11)
| ~ spl8_178 ),
inference(avatar_component_clause,[],[f1468]) ).
fof(f1480,definition,
( spl8_179
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_179])],[avatar_definition]) ).
fof(f1481,plain,
( e10 = op1(e10,e12)
| ~ spl8_179 ),
inference(avatar_component_clause,[],[f1480]) ).
fof(f1484,definition,
( spl8_180
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_180])],[avatar_definition]) ).
fof(f1486,plain,
( e12 = op1(e11,e11)
| ~ spl8_180 ),
inference(avatar_component_clause,[],[f1484]) ).
fof(f1488,definition,
( spl8_181
<=> e12 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl8_181])],[avatar_definition]) ).
fof(f1489,plain,
( e12 = op1(e12,e12)
| ~ spl8_181 ),
inference(avatar_component_clause,[],[f1488]) ).
fof(f1492,definition,
( spl8_182
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_182])],[avatar_definition]) ).
fof(f1494,plain,
( e12 = op1(e13,e13)
| ~ spl8_182 ),
inference(avatar_component_clause,[],[f1492]) ).
fof(f1497,definition,
( spl8_183
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[spl8_183])],[avatar_definition]) ).
fof(f1499,plain,
( op1(e10,e10) = e12
| ~ spl8_183 ),
inference(avatar_component_clause,[],[f1497]) ).
fof(f1502,definition,
( spl8_184
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl8_184])],[avatar_definition]) ).
fof(f1503,plain,
( e11 = op1(e11,e12)
| ~ spl8_184 ),
inference(avatar_component_clause,[],[f1502]) ).
fof(f1512,definition,
( spl8_185
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_185])],[avatar_definition]) ).
fof(f1520,plain,
( spl8_183
| spl8_180
| spl8_181
| ~ spl8_185 ),
inference(avatar_split_clause,[],[f286,f1512,f1488,f1484,f1497]) ).
fof(f1522,plain,
( spl8_183
| ~ spl8_184
| spl8_181
| ~ spl8_185 ),
inference(avatar_split_clause,[],[f288,f1512,f1488,f1502,f1497]) ).
fof(f1524,definition,
( spl8_186
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl8_186])],[avatar_definition]) ).
fof(f1525,plain,
( e10 = op1(e10,e13)
| ~ spl8_186 ),
inference(avatar_component_clause,[],[f1524]) ).
fof(f1528,definition,
( spl8_187
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_187])],[avatar_definition]) ).
fof(f1530,plain,
( e13 = op1(e11,e11)
| ~ spl8_187 ),
inference(avatar_component_clause,[],[f1528]) ).
fof(f1532,definition,
( spl8_188
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl8_188])],[avatar_definition]) ).
fof(f1533,plain,
( e12 = op1(e12,e13)
| ~ spl8_188 ),
inference(avatar_component_clause,[],[f1532]) ).
fof(f1536,definition,
( spl8_189
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_189])],[avatar_definition]) ).
fof(f1538,plain,
( e13 = op1(e13,e13)
| ~ spl8_189 ),
inference(avatar_component_clause,[],[f1536]) ).
fof(f1541,definition,
( spl8_190
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl8_190])],[avatar_definition]) ).
fof(f1543,plain,
( op1(e10,e10) = e13
| ~ spl8_190 ),
inference(avatar_component_clause,[],[f1541]) ).
fof(f1546,definition,
( spl8_191
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_191])],[avatar_definition]) ).
fof(f1547,plain,
( e11 = op1(e11,e13)
| ~ spl8_191 ),
inference(avatar_component_clause,[],[f1546]) ).
fof(f1552,definition,
( spl8_192
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl8_192])],[avatar_definition]) ).
fof(f1554,plain,
( e13 = op1(e12,e12)
| ~ spl8_192 ),
inference(avatar_component_clause,[],[f1552]) ).
fof(f1556,plain,
( spl8_190
| spl8_187
| spl8_192
| spl8_189 ),
inference(avatar_split_clause,[],[f294,f1536,f1552,f1528,f1541]) ).
fof(f1573,definition,
( spl8_194
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_194])],[avatar_definition]) ).
fof(f1575,plain,
( e20 = op2(e22,e20)
| ~ spl8_194 ),
inference(avatar_component_clause,[],[f1573]) ).
fof(f1577,definition,
( spl8_195
<=> e20 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_195])],[avatar_definition]) ).
fof(f1586,definition,
( spl8_197
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_197])],[avatar_definition]) ).
fof(f1599,definition,
( spl8_200
<=> e21 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_200])],[avatar_definition]) ).
fof(f1608,definition,
( spl8_202
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_202])],[avatar_definition]) ).
fof(f1610,plain,
( e22 = op2(e20,e22)
| ~ spl8_202 ),
inference(avatar_component_clause,[],[f1608]) ).
fof(f1617,definition,
( spl8_204
<=> e22 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl8_204])],[avatar_definition]) ).
fof(f1619,plain,
( e22 = op2(e21,e20)
| ~ spl8_204 ),
inference(avatar_component_clause,[],[f1617]) ).
fof(f1621,definition,
( spl8_205
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_205])],[avatar_definition]) ).
fof(f1626,definition,
( spl8_206
<=> e23 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl8_206])],[avatar_definition]) ).
fof(f1628,plain,
( e23 = op2(e20,e21)
| ~ spl8_206 ),
inference(avatar_component_clause,[],[f1626]) ).
fof(f1630,definition,
( spl8_207
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_207])],[avatar_definition]) ).
fof(f1634,definition,
( spl8_208
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl8_208])],[avatar_definition]) ).
fof(f1636,plain,
( e23 = op2(e20,e23)
| ~ spl8_208 ),
inference(avatar_component_clause,[],[f1634]) ).
fof(f1637,plain,
( spl8_162
| spl8_206
| spl8_207
| spl8_208 ),
inference(avatar_split_clause,[],[f91,f1634,f1630,f1626,f1365]) ).
fof(f1639,definition,
( spl8_209
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl8_209])],[avatar_definition]) ).
fof(f1641,plain,
( e23 = op2(e21,e20)
| ~ spl8_209 ),
inference(avatar_component_clause,[],[f1639]) ).
fof(f1652,definition,
( spl8_212
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_212])],[avatar_definition]) ).
fof(f1657,definition,
( spl8_213
<=> e20 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl8_213])],[avatar_definition]) ).
fof(f1671,definition,
( spl8_216
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl8_216])],[avatar_definition]) ).
fof(f1673,plain,
( e21 = op2(e23,e21)
| ~ spl8_216 ),
inference(avatar_component_clause,[],[f1671]) ).
fof(f1676,definition,
( spl8_217
<=> e22 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl8_217])],[avatar_definition]) ).
fof(f1678,plain,
( e22 = op2(e21,e22)
| ~ spl8_217 ),
inference(avatar_component_clause,[],[f1676]) ).
fof(f1680,definition,
( spl8_218
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_218])],[avatar_definition]) ).
fof(f1683,plain,
( spl8_204
| spl8_152
| spl8_217
| spl8_218 ),
inference(avatar_split_clause,[],[f97,f1680,f1676,f1308,f1617]) ).
fof(f1690,definition,
( spl8_220
<=> e23 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl8_220])],[avatar_definition]) ).
fof(f1692,plain,
( e23 = op2(e21,e22)
| ~ spl8_220 ),
inference(avatar_component_clause,[],[f1690]) ).
fof(f1694,definition,
( spl8_221
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_221])],[avatar_definition]) ).
fof(f1696,plain,
( e23 = op2(e21,e23)
| ~ spl8_221 ),
inference(avatar_component_clause,[],[f1694]) ).
fof(f1697,plain,
( spl8_209
| spl8_159
| spl8_220
| spl8_221 ),
inference(avatar_split_clause,[],[f99,f1694,f1690,f1352,f1639]) ).
fof(f1704,definition,
( spl8_223
<=> e20 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl8_223])],[avatar_definition]) ).
fof(f1706,plain,
( e20 = op2(e22,e23)
| ~ spl8_223 ),
inference(avatar_component_clause,[],[f1704]) ).
fof(f1707,plain,
( spl8_194
| spl8_213
| spl8_142
| spl8_223 ),
inference(avatar_split_clause,[],[f101,f1704,f1240,f1657,f1573]) ).
fof(f1709,definition,
( spl8_224
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_224])],[avatar_definition]) ).
fof(f1711,plain,
( e20 = op2(e23,e22)
| ~ spl8_224 ),
inference(avatar_component_clause,[],[f1709]) ).
fof(f1714,definition,
( spl8_225
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl8_225])],[avatar_definition]) ).
fof(f1716,plain,
( e21 = op2(e22,e23)
| ~ spl8_225 ),
inference(avatar_component_clause,[],[f1714]) ).
fof(f1719,definition,
( spl8_226
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_226])],[avatar_definition]) ).
fof(f1721,plain,
( e21 = op2(e23,e22)
| ~ spl8_226 ),
inference(avatar_component_clause,[],[f1719]) ).
fof(f1722,plain,
( spl8_197
| spl8_156
| spl8_149
| spl8_226 ),
inference(avatar_split_clause,[],[f104,f1719,f1284,f1326,f1586]) ).
fof(f1723,plain,
( spl8_139
| spl8_146
| spl8_153
| spl8_160 ),
inference(avatar_split_clause,[],[f105,f1356,f1312,f1268,f1224]) ).
fof(f1736,plain,
( spl8_158
| spl8_212
| spl8_223
| spl8_140 ),
inference(avatar_split_clause,[],[f110,f1228,f1704,f1652,f1348]) ).
fof(f1737,plain,
( spl8_200
| spl8_216
| spl8_226
| spl8_147 ),
inference(avatar_split_clause,[],[f111,f1272,f1719,f1671,f1599]) ).
fof(f1745,plain,
( spl8_151
| spl8_197
| spl8_202
| spl8_207 ),
inference(avatar_split_clause,[],[f71,f1630,f1608,f1586,f1304]) ).
fof(f1755,plain,
( spl8_195
| spl8_200
| spl8_205
| spl8_143 ),
inference(avatar_split_clause,[],[f81,f1248,f1621,f1599,f1577]) ).
fof(f1759,plain,
( spl8_165
| spl8_172
| spl8_179
| spl8_186 ),
inference(avatar_split_clause,[],[f37,f1524,f1480,f1436,f1392]) ).
fof(f1761,definition,
( spl8_229
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_229])],[avatar_definition]) ).
fof(f1763,plain,
( e10 = op1(e11,e10)
| ~ spl8_229 ),
inference(avatar_component_clause,[],[f1761]) ).
fof(f1765,definition,
( spl8_230
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl8_230])],[avatar_definition]) ).
fof(f1767,plain,
( e10 = op1(e12,e10)
| ~ spl8_230 ),
inference(avatar_component_clause,[],[f1765]) ).
fof(f1769,definition,
( spl8_231
<=> e10 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_231])],[avatar_definition]) ).
fof(f1771,plain,
( e10 = op1(e13,e10)
| ~ spl8_231 ),
inference(avatar_component_clause,[],[f1769]) ).
fof(f1772,plain,
( spl8_165
| spl8_229
| spl8_230
| spl8_231 ),
inference(avatar_split_clause,[],[f38,f1769,f1765,f1761,f1392]) ).
fof(f1791,definition,
( spl8_236
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_236])],[avatar_definition]) ).
fof(f1796,definition,
( spl8_237
<=> e12 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl8_237])],[avatar_definition]) ).
fof(f1798,plain,
( e12 = op1(e10,e11)
| ~ spl8_237 ),
inference(avatar_component_clause,[],[f1796]) ).
fof(f1800,definition,
( spl8_238
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_238])],[avatar_definition]) ).
fof(f1802,plain,
( e12 = op1(e10,e12)
| ~ spl8_238 ),
inference(avatar_component_clause,[],[f1800]) ).
fof(f1809,definition,
( spl8_240
<=> e12 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_240])],[avatar_definition]) ).
fof(f1811,plain,
( e12 = op1(e11,e10)
| ~ spl8_240 ),
inference(avatar_component_clause,[],[f1809]) ).
fof(f1813,definition,
( spl8_241
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_241])],[avatar_definition]) ).
fof(f1816,plain,
( spl8_183
| spl8_240
| spl8_167
| spl8_241 ),
inference(avatar_split_clause,[],[f42,f1813,f1400,f1809,f1497]) ).
fof(f1818,definition,
( spl8_242
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl8_242])],[avatar_definition]) ).
fof(f1820,plain,
( e13 = op1(e10,e11)
| ~ spl8_242 ),
inference(avatar_component_clause,[],[f1818]) ).
fof(f1822,definition,
( spl8_243
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_243])],[avatar_definition]) ).
fof(f1824,plain,
( e13 = op1(e10,e12)
| ~ spl8_243 ),
inference(avatar_component_clause,[],[f1822]) ).
fof(f1831,definition,
( spl8_245
<=> e13 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_245])],[avatar_definition]) ).
fof(f1833,plain,
( e13 = op1(e11,e10)
| ~ spl8_245 ),
inference(avatar_component_clause,[],[f1831]) ).
fof(f1857,plain,
( spl8_169
| spl8_173
| spl8_184
| spl8_191 ),
inference(avatar_split_clause,[],[f47,f1546,f1502,f1440,f1410]) ).
fof(f1863,definition,
( spl8_252
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_252])],[avatar_definition]) ).
fof(f1865,plain,
( e11 = op1(e13,e11)
| ~ spl8_252 ),
inference(avatar_component_clause,[],[f1863]) ).
fof(f1868,definition,
( spl8_253
<=> e12 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl8_253])],[avatar_definition]) ).
fof(f1870,plain,
( e12 = op1(e11,e12)
| ~ spl8_253 ),
inference(avatar_component_clause,[],[f1868]) ).
fof(f1872,definition,
( spl8_254
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_254])],[avatar_definition]) ).
fof(f1875,plain,
( spl8_240
| spl8_180
| spl8_253
| spl8_254 ),
inference(avatar_split_clause,[],[f49,f1872,f1868,f1484,f1809]) ).
fof(f1877,definition,
( spl8_255
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_255])],[avatar_definition]) ).
fof(f1880,plain,
( spl8_237
| spl8_180
| spl8_174
| spl8_255 ),
inference(avatar_split_clause,[],[f50,f1877,f1444,f1484,f1796]) ).
fof(f1882,definition,
( spl8_256
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl8_256])],[avatar_definition]) ).
fof(f1884,plain,
( e13 = op1(e11,e12)
| ~ spl8_256 ),
inference(avatar_component_clause,[],[f1882]) ).
fof(f1886,definition,
( spl8_257
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_257])],[avatar_definition]) ).
fof(f1888,plain,
( e13 = op1(e11,e13)
| ~ spl8_257 ),
inference(avatar_component_clause,[],[f1886]) ).
fof(f1889,plain,
( spl8_245
| spl8_187
| spl8_256
| spl8_257 ),
inference(avatar_split_clause,[],[f51,f1886,f1882,f1528,f1831]) ).
fof(f1891,definition,
( spl8_258
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_258])],[avatar_definition]) ).
fof(f1894,plain,
( spl8_242
| spl8_187
| spl8_258
| spl8_178 ),
inference(avatar_split_clause,[],[f52,f1468,f1891,f1528,f1818]) ).
fof(f1901,definition,
( spl8_260
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_260])],[avatar_definition]) ).
fof(f1903,plain,
( e10 = op1(e13,e12)
| ~ spl8_260 ),
inference(avatar_component_clause,[],[f1901]) ).
fof(f1906,definition,
( spl8_261
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl8_261])],[avatar_definition]) ).
fof(f1908,plain,
( e11 = op1(e12,e13)
| ~ spl8_261 ),
inference(avatar_component_clause,[],[f1906]) ).
fof(f1911,definition,
( spl8_262
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_262])],[avatar_definition]) ).
fof(f1913,plain,
( e11 = op1(e13,e12)
| ~ spl8_262 ),
inference(avatar_component_clause,[],[f1911]) ).
fof(f1915,plain,
( spl8_167
| spl8_174
| spl8_181
| spl8_188 ),
inference(avatar_split_clause,[],[f57,f1532,f1488,f1444,f1400]) ).
fof(f1917,definition,
( spl8_263
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_263])],[avatar_definition]) ).
fof(f1920,plain,
( spl8_238
| spl8_253
| spl8_181
| spl8_263 ),
inference(avatar_split_clause,[],[f58,f1917,f1488,f1868,f1800]) ).
fof(f1926,plain,
( spl8_243
| spl8_256
| spl8_192
| spl8_185 ),
inference(avatar_split_clause,[],[f60,f1512,f1552,f1882,f1822]) ).
fof(f1929,plain,
( spl8_236
| spl8_252
| spl8_262
| spl8_175 ),
inference(avatar_split_clause,[],[f63,f1448,f1911,f1863,f1791]) ).
fof(f1933,plain,
( spl8_171
| spl8_178
| spl8_185
| spl8_189 ),
inference(avatar_split_clause,[],[f67,f1536,f1512,f1468,f1424]) ).
fof(f1949,plain,
( spl8_260
| spl8_262
| spl8_263
| spl8_185 ),
inference(avatar_split_clause,[],[f35,f1512,f1917,f1911,f1901]) ).
fof(f1952,plain,
( e20 != e22
| spl8_22
| ~ spl8_105 ),
inference(superposition,[],[f674,f1053]) ).
fof(f1954,plain,
spl8_182,
inference(avatar_split_clause,[],[f369,f1492]) ).
fof(f1955,plain,
spl8_154,
inference(avatar_split_clause,[],[f372,f1316]) ).
fof(f1971,plain,
( e20 = e21
| ~ spl8_137
| ~ spl8_148 ),
inference(forward_demodulation,[],[f1279,f1217]) ).
fof(f1972,plain,
( $false
| ~ spl8_137
| ~ spl8_148 ),
inference(forward_subsumption_resolution,[],[f1971,f224]) ).
fof(f1973,plain,
( ~ spl8_137
| ~ spl8_148 ),
inference(avatar_contradiction_clause,[],[f1972]) ).
fof(f1996,plain,
( e20 = e22
| ~ spl8_140
| ~ spl8_154 ),
inference(superposition,[],[f1318,f1230]) ).
fof(f2000,plain,
( $false
| spl8_22
| ~ spl8_105
| ~ spl8_140
| ~ spl8_154 ),
inference(forward_subsumption_resolution,[],[f1996,f1952]) ).
fof(f2001,plain,
( spl8_22
| ~ spl8_105
| ~ spl8_140
| ~ spl8_154 ),
inference(avatar_contradiction_clause,[],[f2000]) ).
fof(f2002,plain,
( e20 = e22
| ~ spl8_22
| ~ spl8_105 ),
inference(forward_demodulation,[],[f673,f1053]) ).
fof(f2012,plain,
( e21 = op2(e22,e22)
| ~ spl8_22
| ~ spl8_105
| ~ spl8_148 ),
inference(superposition,[],[f1279,f2002]) ).
fof(f2023,plain,
( e20 != e22
| spl8_22
| ~ spl8_105 ),
inference(forward_demodulation,[],[f674,f1053]) ).
fof(f2047,plain,
( e21 = e23
| ~ spl8_37
| ~ spl8_136 ),
inference(forward_demodulation,[],[f745,f1205]) ).
fof(f2071,plain,
( e21 != e23
| spl8_37
| ~ spl8_136 ),
inference(forward_demodulation,[],[f746,f1205]) ).
fof(f2073,plain,
( e22 = e23
| ~ spl8_154
| ~ spl8_161 ),
inference(superposition,[],[f1362,f1318]) ).
fof(f2077,plain,
( $false
| ~ spl8_154
| ~ spl8_161 ),
inference(forward_subsumption_resolution,[],[f2073,f219]) ).
fof(f2078,plain,
( ~ spl8_154
| ~ spl8_161 ),
inference(avatar_contradiction_clause,[],[f2077]) ).
fof(f2080,plain,
( e21 = e23
| ~ spl8_148
| ~ spl8_162 ),
inference(superposition,[],[f1367,f1279]) ).
fof(f2086,plain,
( $false
| spl8_37
| ~ spl8_136
| ~ spl8_148
| ~ spl8_162 ),
inference(forward_subsumption_resolution,[],[f2080,f2071]) ).
fof(f2087,plain,
( spl8_37
| ~ spl8_136
| ~ spl8_148
| ~ spl8_162 ),
inference(avatar_contradiction_clause,[],[f2086]) ).
fof(f2088,plain,
( e21 = e22
| ~ spl8_147
| ~ spl8_154 ),
inference(forward_demodulation,[],[f1274,f1318]) ).
fof(f2090,plain,
( $false
| ~ spl8_147
| ~ spl8_154 ),
inference(forward_subsumption_resolution,[],[f2088,f221]) ).
fof(f2091,plain,
( ~ spl8_147
| ~ spl8_154 ),
inference(avatar_contradiction_clause,[],[f2090]) ).
fof(f2108,plain,
( $false
| ~ spl8_37
| ~ spl8_136 ),
inference(forward_subsumption_resolution,[],[f220,f2047]) ).
fof(f2109,plain,
( ~ spl8_37
| ~ spl8_136 ),
inference(avatar_contradiction_clause,[],[f2108]) ).
fof(f2133,plain,
( e10 = e11
| ~ spl8_166
| ~ spl8_173 ),
inference(forward_demodulation,[],[f1442,f1398]) ).
fof(f2134,plain,
( $false
| ~ spl8_166
| ~ spl8_173 ),
inference(forward_subsumption_resolution,[],[f2133,f218]) ).
fof(f2135,plain,
( ~ spl8_166
| ~ spl8_173 ),
inference(avatar_contradiction_clause,[],[f2134]) ).
fof(f2141,plain,
( e10 = e11
| ~ spl8_165
| ~ spl8_176 ),
inference(forward_demodulation,[],[f1455,f1393]) ).
fof(f2142,plain,
( $false
| ~ spl8_165
| ~ spl8_176 ),
inference(forward_subsumption_resolution,[],[f2141,f218]) ).
fof(f2143,plain,
( ~ spl8_165
| ~ spl8_176 ),
inference(avatar_contradiction_clause,[],[f2142]) ).
fof(f2145,plain,
( e10 = e11
| ~ spl8_170
| ~ spl8_177 ),
inference(forward_demodulation,[],[f1462,f1418]) ).
fof(f2146,plain,
( $false
| ~ spl8_170
| ~ spl8_177 ),
inference(forward_subsumption_resolution,[],[f2145,f218]) ).
fof(f2147,plain,
( ~ spl8_170
| ~ spl8_177 ),
inference(avatar_contradiction_clause,[],[f2146]) ).
fof(f2154,plain,
( e10 = e12
| ~ spl8_168
| ~ spl8_182 ),
inference(forward_demodulation,[],[f1494,f1406]) ).
fof(f2155,plain,
( $false
| ~ spl8_168
| ~ spl8_182 ),
inference(forward_subsumption_resolution,[],[f2154,f217]) ).
fof(f2156,plain,
( ~ spl8_168
| ~ spl8_182 ),
inference(avatar_contradiction_clause,[],[f2155]) ).
fof(f2160,plain,
( e11 = e12
| ~ spl8_176
| ~ spl8_183 ),
inference(forward_demodulation,[],[f1499,f1455]) ).
fof(f2161,plain,
( $false
| ~ spl8_176
| ~ spl8_183 ),
inference(forward_subsumption_resolution,[],[f2160,f215]) ).
fof(f2162,plain,
( ~ spl8_176
| ~ spl8_183 ),
inference(avatar_contradiction_clause,[],[f2161]) ).
fof(f2164,plain,
( e11 = e13
| ~ spl8_173
| ~ spl8_187 ),
inference(superposition,[],[f1530,f1442]) ).
fof(f2169,plain,
( $false
| ~ spl8_173
| ~ spl8_187 ),
inference(forward_subsumption_resolution,[],[f2164,f214]) ).
fof(f2170,plain,
( ~ spl8_173
| ~ spl8_187 ),
inference(avatar_contradiction_clause,[],[f2169]) ).
fof(f2172,plain,
( e12 = e13
| ~ spl8_182
| ~ spl8_189 ),
inference(superposition,[],[f1538,f1494]) ).
fof(f2178,plain,
( $false
| ~ spl8_182
| ~ spl8_189 ),
inference(forward_subsumption_resolution,[],[f2172,f213]) ).
fof(f2179,plain,
( ~ spl8_182
| ~ spl8_189 ),
inference(avatar_contradiction_clause,[],[f2178]) ).
fof(f2181,plain,
( e11 = e13
| ~ spl8_176
| ~ spl8_190 ),
inference(superposition,[],[f1543,f1455]) ).
fof(f2186,plain,
( $false
| ~ spl8_176
| ~ spl8_190 ),
inference(forward_subsumption_resolution,[],[f2181,f214]) ).
fof(f2187,plain,
( ~ spl8_176
| ~ spl8_190 ),
inference(avatar_contradiction_clause,[],[f2186]) ).
fof(f2189,plain,
( e10 = e13
| ~ spl8_170
| ~ spl8_192 ),
inference(superposition,[],[f1554,f1418]) ).
fof(f2193,plain,
( $false
| ~ spl8_170
| ~ spl8_192 ),
inference(forward_subsumption_resolution,[],[f2189,f216]) ).
fof(f2194,plain,
( ~ spl8_170
| ~ spl8_192 ),
inference(avatar_contradiction_clause,[],[f2193]) ).
fof(f2195,plain,
( e11 = e12
| ~ spl8_175
| ~ spl8_182 ),
inference(superposition,[],[f1450,f1494]) ).
fof(f2201,plain,
( $false
| ~ spl8_175
| ~ spl8_182 ),
inference(forward_subsumption_resolution,[],[f2195,f215]) ).
fof(f2202,plain,
( ~ spl8_175
| ~ spl8_182 ),
inference(avatar_contradiction_clause,[],[f2201]) ).
fof(f2233,plain,
( e21 = e22
| ~ spl8_160
| ~ spl8_225 ),
inference(forward_demodulation,[],[f1716,f1357]) ).
fof(f2234,plain,
( $false
| ~ spl8_160
| ~ spl8_225 ),
inference(forward_subsumption_resolution,[],[f2233,f221]) ).
fof(f2235,plain,
( ~ spl8_160
| ~ spl8_225 ),
inference(avatar_contradiction_clause,[],[f2234]) ).
fof(f2281,plain,
( e20 = e23
| ~ spl8_138
| ~ spl8_159 ),
inference(forward_demodulation,[],[f1222,f1354]) ).
fof(f2283,plain,
( $false
| ~ spl8_138
| ~ spl8_159 ),
inference(forward_subsumption_resolution,[],[f2281,f222]) ).
fof(f2284,plain,
( ~ spl8_138
| ~ spl8_159 ),
inference(avatar_contradiction_clause,[],[f2283]) ).
fof(f2328,plain,
( e20 = e22
| ~ spl8_138
| ~ spl8_152 ),
inference(superposition,[],[f1310,f1222]) ).
fof(f2333,plain,
( $false
| spl8_22
| ~ spl8_105
| ~ spl8_138
| ~ spl8_152 ),
inference(forward_subsumption_resolution,[],[f2328,f2023]) ).
fof(f2334,plain,
( spl8_22
| ~ spl8_105
| ~ spl8_138
| ~ spl8_152 ),
inference(avatar_contradiction_clause,[],[f2333]) ).
fof(f2428,plain,
( e21 = e23
| ~ spl8_156
| ~ spl8_220 ),
inference(superposition,[],[f1692,f1327]) ).
fof(f2433,plain,
( $false
| spl8_37
| ~ spl8_136
| ~ spl8_156
| ~ spl8_220 ),
inference(forward_subsumption_resolution,[],[f2428,f2071]) ).
fof(f2434,plain,
( spl8_37
| ~ spl8_136
| ~ spl8_156
| ~ spl8_220 ),
inference(avatar_contradiction_clause,[],[f2433]) ).
fof(f2503,plain,
( e22 = e23
| ~ spl8_204
| ~ spl8_209 ),
inference(superposition,[],[f1641,f1619]) ).
fof(f2509,plain,
( $false
| ~ spl8_204
| ~ spl8_209 ),
inference(forward_subsumption_resolution,[],[f2503,f219]) ).
fof(f2510,plain,
( ~ spl8_204
| ~ spl8_209 ),
inference(avatar_contradiction_clause,[],[f2509]) ).
fof(f2546,plain,
( e20 = e21
| ~ spl8_224
| ~ spl8_226 ),
inference(forward_demodulation,[],[f1721,f1711]) ).
fof(f2547,plain,
( $false
| ~ spl8_224
| ~ spl8_226 ),
inference(forward_subsumption_resolution,[],[f2546,f224]) ).
fof(f2548,plain,
( ~ spl8_224
| ~ spl8_226 ),
inference(avatar_contradiction_clause,[],[f2547]) ).
fof(f2572,plain,
( e10 = e12
| ~ spl8_179
| ~ spl8_238 ),
inference(forward_demodulation,[],[f1802,f1481]) ).
fof(f2573,plain,
( $false
| ~ spl8_179
| ~ spl8_238 ),
inference(forward_subsumption_resolution,[],[f2572,f217]) ).
fof(f2574,plain,
( ~ spl8_179
| ~ spl8_238 ),
inference(avatar_contradiction_clause,[],[f2573]) ).
fof(f2593,plain,
( e10 = e12
| ~ spl8_229
| ~ spl8_240 ),
inference(forward_demodulation,[],[f1811,f1763]) ).
fof(f2594,plain,
( $false
| ~ spl8_229
| ~ spl8_240 ),
inference(forward_subsumption_resolution,[],[f2593,f217]) ).
fof(f2595,plain,
( ~ spl8_229
| ~ spl8_240 ),
inference(avatar_contradiction_clause,[],[f2594]) ).
fof(f2601,plain,
( e10 = e13
| ~ spl8_166
| ~ spl8_187 ),
inference(superposition,[],[f1530,f1398]) ).
fof(f2605,plain,
( $false
| ~ spl8_166
| ~ spl8_187 ),
inference(forward_subsumption_resolution,[],[f2601,f216]) ).
fof(f2606,plain,
( ~ spl8_166
| ~ spl8_187 ),
inference(avatar_contradiction_clause,[],[f2605]) ).
fof(f2608,plain,
( e10 = e12
| ~ spl8_165
| ~ spl8_183 ),
inference(forward_demodulation,[],[f1499,f1393]) ).
fof(f2609,plain,
( $false
| ~ spl8_165
| ~ spl8_183 ),
inference(forward_subsumption_resolution,[],[f2608,f217]) ).
fof(f2610,plain,
( ~ spl8_165
| ~ spl8_183 ),
inference(avatar_contradiction_clause,[],[f2609]) ).
fof(f2611,plain,
( e11 = e12
| ~ spl8_177
| ~ spl8_181 ),
inference(forward_demodulation,[],[f1489,f1462]) ).
fof(f2613,plain,
( $false
| ~ spl8_177
| ~ spl8_181 ),
inference(forward_subsumption_resolution,[],[f2611,f215]) ).
fof(f2614,plain,
( ~ spl8_177
| ~ spl8_181 ),
inference(avatar_contradiction_clause,[],[f2613]) ).
fof(f2633,plain,
( e10 = e13
| ~ spl8_171
| ~ spl8_231 ),
inference(forward_demodulation,[],[f1771,f1425]) ).
fof(f2634,plain,
( $false
| ~ spl8_171
| ~ spl8_231 ),
inference(forward_subsumption_resolution,[],[f2633,f216]) ).
fof(f2635,plain,
( ~ spl8_171
| ~ spl8_231 ),
inference(avatar_contradiction_clause,[],[f2634]) ).
fof(f2636,plain,
( e10 = e12
| ~ spl8_166
| ~ spl8_180 ),
inference(forward_demodulation,[],[f1486,f1398]) ).
fof(f2637,plain,
( $false
| ~ spl8_166
| ~ spl8_180 ),
inference(forward_subsumption_resolution,[],[f2636,f217]) ).
fof(f2638,plain,
( ~ spl8_166
| ~ spl8_180 ),
inference(avatar_contradiction_clause,[],[f2637]) ).
fof(f2766,plain,
( e11 = e13
| ~ spl8_184
| ~ spl8_256 ),
inference(forward_demodulation,[],[f1503,f1884]) ).
fof(f2767,plain,
( $false
| ~ spl8_184
| ~ spl8_256 ),
inference(forward_subsumption_resolution,[],[f2766,f214]) ).
fof(f2768,plain,
( ~ spl8_184
| ~ spl8_256 ),
inference(avatar_contradiction_clause,[],[f2767]) ).
fof(f2847,plain,
( e11 = e12
| ~ spl8_184
| ~ spl8_253 ),
inference(forward_demodulation,[],[f1870,f1503]) ).
fof(f2849,plain,
( $false
| ~ spl8_184
| ~ spl8_253 ),
inference(forward_subsumption_resolution,[],[f2847,f215]) ).
fof(f2850,plain,
( ~ spl8_184
| ~ spl8_253 ),
inference(avatar_contradiction_clause,[],[f2849]) ).
fof(f2851,plain,
( e12 = e13
| ~ spl8_240
| ~ spl8_245 ),
inference(forward_demodulation,[],[f1811,f1833]) ).
fof(f2853,plain,
( $false
| ~ spl8_240
| ~ spl8_245 ),
inference(forward_subsumption_resolution,[],[f2851,f213]) ).
fof(f2854,plain,
( ~ spl8_240
| ~ spl8_245 ),
inference(avatar_contradiction_clause,[],[f2853]) ).
fof(f2874,plain,
( e11 = e13
| ~ spl8_178
| ~ spl8_252 ),
inference(forward_demodulation,[],[f1865,f1469]) ).
fof(f2875,plain,
( $false
| ~ spl8_178
| ~ spl8_252 ),
inference(forward_subsumption_resolution,[],[f2874,f214]) ).
fof(f2876,plain,
( ~ spl8_178
| ~ spl8_252 ),
inference(avatar_contradiction_clause,[],[f2875]) ).
fof(f2885,plain,
( e12 = e13
| ~ spl8_238
| ~ spl8_243 ),
inference(forward_demodulation,[],[f1802,f1824]) ).
fof(f2887,plain,
( $false
| ~ spl8_238
| ~ spl8_243 ),
inference(forward_subsumption_resolution,[],[f2885,f213]) ).
fof(f2888,plain,
( ~ spl8_238
| ~ spl8_243 ),
inference(avatar_contradiction_clause,[],[f2887]) ).
fof(f2894,plain,
( e12 = e13
| ~ spl8_180
| ~ spl8_187 ),
inference(superposition,[],[f1530,f1486]) ).
fof(f2900,plain,
( $false
| ~ spl8_180
| ~ spl8_187 ),
inference(forward_subsumption_resolution,[],[f2894,f213]) ).
fof(f2901,plain,
( ~ spl8_180
| ~ spl8_187 ),
inference(avatar_contradiction_clause,[],[f2900]) ).
fof(f2942,plain,
( e11 = e12
| ~ spl8_188
| ~ spl8_261 ),
inference(superposition,[],[f1908,f1533]) ).
fof(f2947,plain,
( $false
| ~ spl8_188
| ~ spl8_261 ),
inference(forward_subsumption_resolution,[],[f2942,f215]) ).
fof(f2948,plain,
( ~ spl8_188
| ~ spl8_261 ),
inference(avatar_contradiction_clause,[],[f2947]) ).
fof(f2998,plain,
( e21 = h1(e12)
| ~ spl8_148 ),
inference(forward_demodulation,[],[f375,f1279]) ).
fof(f2999,plain,
( spl8_8
| ~ spl8_148 ),
inference(avatar_split_clause,[],[f2998,f1277,f605]) ).
fof(f3012,plain,
( e12 != op1(e13,e12)
| ~ spl8_182 ),
inference(forward_demodulation,[],[f117,f1494]) ).
fof(f3014,plain,
( e12 != op1(e13,e11)
| ~ spl8_182 ),
inference(forward_demodulation,[],[f118,f1494]) ).
fof(f3018,plain,
( e12 != op1(e13,e10)
| ~ spl8_182 ),
inference(forward_demodulation,[],[f120,f1494]) ).
fof(f3025,plain,
( e13 != op1(e12,e11)
| ~ spl8_192 ),
inference(forward_demodulation,[],[f125,f1554]) ).
fof(f3034,plain,
( e12 != op1(e11,e10)
| ~ spl8_253 ),
inference(forward_demodulation,[],[f133,f1870]) ).
fof(f3043,plain,
( e12 != op1(e11,e13)
| ~ spl8_182 ),
inference(forward_demodulation,[],[f142,f1494]) ).
fof(f3050,plain,
( e11 != op1(e11,e12)
| ~ spl8_262 ),
inference(forward_demodulation,[],[f148,f1913]) ).
fof(f3073,plain,
( e22 != op2(e23,e20)
| ~ spl8_154 ),
inference(forward_demodulation,[],[f168,f1318]) ).
fof(f3098,plain,
( e22 != op2(e21,e23)
| ~ spl8_154 ),
inference(forward_demodulation,[],[f190,f1318]) ).
fof(f3108,plain,
( e23 != op2(e20,e22)
| ~ spl8_164 ),
inference(forward_demodulation,[],[f199,f1378]) ).
fof(f3123,plain,
( e11 = op1(e12,e13)
| ~ spl8_182 ),
inference(forward_demodulation,[],[f370,f1494]) ).
fof(f3127,plain,
( e12 = e13
| ~ spl8_181
| ~ spl8_192 ),
inference(forward_demodulation,[],[f1489,f1554]) ).
fof(f3128,plain,
( ~ spl8_263
| ~ spl8_182 ),
inference(avatar_split_clause,[],[f3012,f1492,f1917]) ).
fof(f3134,plain,
( e11 != op1(e12,e13)
| ~ spl8_191 ),
inference(forward_demodulation,[],[f143,f1547]) ).
fof(f3135,plain,
( spl8_261
| ~ spl8_182 ),
inference(avatar_split_clause,[],[f3123,f1492,f1906]) ).
fof(f3139,plain,
( ~ spl8_241
| ~ spl8_182 ),
inference(avatar_split_clause,[],[f3018,f1492,f1813]) ).
fof(f3141,plain,
( e11 != op1(e13,e10)
| ~ spl8_176 ),
inference(forward_demodulation,[],[f162,f1455]) ).
fof(f3142,plain,
( e12 != op1(e10,e12)
| ~ spl8_237 ),
inference(forward_demodulation,[],[f137,f1798]) ).
fof(f3147,plain,
( $false
| ~ spl8_181
| ~ spl8_192 ),
inference(forward_subsumption_resolution,[],[f3127,f213]) ).
fof(f3148,plain,
( ~ spl8_181
| ~ spl8_192 ),
inference(avatar_contradiction_clause,[],[f3147]) ).
fof(f3152,plain,
( ~ spl8_261
| ~ spl8_191 ),
inference(avatar_split_clause,[],[f3134,f1546,f1906]) ).
fof(f3153,plain,
( ~ spl8_236
| ~ spl8_176 ),
inference(avatar_split_clause,[],[f3141,f1453,f1791]) ).
fof(f3154,plain,
( ~ spl8_238
| ~ spl8_237 ),
inference(avatar_split_clause,[],[f3142,f1796,f1800]) ).
fof(f3157,plain,
( e11 != op1(e11,e10)
| ~ spl8_176 ),
inference(forward_demodulation,[],[f164,f1455]) ).
fof(f3158,plain,
( ~ spl8_254
| ~ spl8_182 ),
inference(avatar_split_clause,[],[f3043,f1492,f1872]) ).
fof(f3159,plain,
( ~ spl8_255
| ~ spl8_182 ),
inference(avatar_split_clause,[],[f3014,f1492,f1877]) ).
fof(f3165,plain,
( e10 = e12
| ~ spl8_170
| ~ spl8_181 ),
inference(forward_demodulation,[],[f1489,f1418]) ).
fof(f3166,plain,
( $false
| ~ spl8_170
| ~ spl8_181 ),
inference(forward_subsumption_resolution,[],[f3165,f217]) ).
fof(f3167,plain,
( ~ spl8_170
| ~ spl8_181 ),
inference(avatar_contradiction_clause,[],[f3166]) ).
fof(f3169,plain,
( ~ spl8_240
| ~ spl8_253 ),
inference(avatar_split_clause,[],[f3034,f1868,f1809]) ).
fof(f3171,plain,
( ~ spl8_184
| ~ spl8_262 ),
inference(avatar_split_clause,[],[f3050,f1911,f1502]) ).
fof(f3175,plain,
( ~ spl8_169
| ~ spl8_176 ),
inference(avatar_split_clause,[],[f3157,f1453,f1410]) ).
fof(f3176,plain,
( ~ spl8_258
| ~ spl8_192 ),
inference(avatar_split_clause,[],[f3025,f1552,f1891]) ).
fof(f3273,plain,
( e21 = op2(e22,e23)
| ~ spl8_154 ),
inference(forward_demodulation,[],[f373,f1318]) ).
fof(f3274,plain,
( e20 = e21
| ~ spl8_154
| ~ spl8_223 ),
inference(forward_demodulation,[],[f3273,f1706]) ).
fof(f3275,plain,
( $false
| ~ spl8_154
| ~ spl8_223 ),
inference(forward_subsumption_resolution,[],[f3274,f224]) ).
fof(f3276,plain,
( ~ spl8_154
| ~ spl8_223 ),
inference(avatar_contradiction_clause,[],[f3275]) ).
fof(f3277,plain,
( e21 = e22
| ~ spl8_156
| ~ spl8_217 ),
inference(forward_demodulation,[],[f1327,f1678]) ).
fof(f3281,plain,
( spl8_225
| ~ spl8_154 ),
inference(avatar_split_clause,[],[f3273,f1316,f1714]) ).
fof(f3284,plain,
( e20 != op2(e22,e21)
| ~ spl8_138 ),
inference(forward_demodulation,[],[f203,f1222]) ).
fof(f3289,plain,
( e21 != op2(e23,e20)
| ~ spl8_148 ),
inference(forward_demodulation,[],[f210,f1279]) ).
fof(f3292,plain,
( e20 != op2(e21,e23)
| ~ spl8_138 ),
inference(forward_demodulation,[],[f178,f1222]) ).
fof(f3299,plain,
( $false
| ~ spl8_156
| ~ spl8_217 ),
inference(forward_subsumption_resolution,[],[f3277,f221]) ).
fof(f3300,plain,
( ~ spl8_156
| ~ spl8_217 ),
inference(avatar_contradiction_clause,[],[f3299]) ).
fof(f3303,plain,
( ~ spl8_213
| ~ spl8_138 ),
inference(avatar_split_clause,[],[f3284,f1220,f1657]) ).
fof(f3304,plain,
( ~ spl8_200
| ~ spl8_148 ),
inference(avatar_split_clause,[],[f3289,f1277,f1599]) ).
fof(f3305,plain,
( ~ spl8_212
| ~ spl8_138 ),
inference(avatar_split_clause,[],[f3292,f1220,f1652]) ).
fof(f3311,plain,
( e22 = e23
| ~ spl8_153
| ~ spl8_164 ),
inference(forward_demodulation,[],[f1313,f1378]) ).
fof(f3312,plain,
( e20 = e23
| ~ spl8_158
| ~ spl8_208 ),
inference(forward_demodulation,[],[f1349,f1636]) ).
fof(f3316,plain,
( ~ spl8_218
| ~ spl8_154 ),
inference(avatar_split_clause,[],[f3098,f1316,f1680]) ).
fof(f3320,plain,
( ~ spl8_205
| ~ spl8_154 ),
inference(avatar_split_clause,[],[f3073,f1316,f1621]) ).
fof(f3322,plain,
( $false
| ~ spl8_153
| ~ spl8_164 ),
inference(forward_subsumption_resolution,[],[f3311,f219]) ).
fof(f3323,plain,
( ~ spl8_153
| ~ spl8_164 ),
inference(avatar_contradiction_clause,[],[f3322]) ).
fof(f3324,plain,
( $false
| ~ spl8_158
| ~ spl8_208 ),
inference(forward_subsumption_resolution,[],[f3312,f222]) ).
fof(f3325,plain,
( ~ spl8_158
| ~ spl8_208 ),
inference(avatar_contradiction_clause,[],[f3324]) ).
fof(f3330,plain,
( e20 != op2(e23,e22)
| ~ spl8_151 ),
inference(forward_demodulation,[],[f198,f1305]) ).
fof(f3335,plain,
( ~ spl8_224
| ~ spl8_151 ),
inference(avatar_split_clause,[],[f3330,f1304,f1709]) ).
fof(f3337,plain,
( e21 != op2(e20,e22)
| ~ spl8_148 ),
inference(forward_demodulation,[],[f187,f1279]) ).
fof(f3338,plain,
( ~ spl8_197
| ~ spl8_148 ),
inference(avatar_split_clause,[],[f3337,f1277,f1586]) ).
fof(f3376,plain,
( e20 != op2(e23,e20)
| ~ spl8_224 ),
inference(forward_demodulation,[],[f169,f1711]) ).
fof(f3404,plain,
( e20 = op2(e23,e22)
| ~ spl8_154 ),
inference(forward_demodulation,[],[f374,f1318]) ).
fof(f3405,plain,
( op2(e21,e20) = h1(e11)
| ~ spl8_148 ),
inference(forward_demodulation,[],[f376,f1279]) ).
fof(f3406,plain,
( e22 = h1(e11)
| ~ spl8_148
| ~ spl8_204 ),
inference(forward_demodulation,[],[f3405,f1619]) ).
fof(f3407,plain,
( spl8_60
| ~ spl8_148
| ~ spl8_204 ),
inference(avatar_split_clause,[],[f3406,f1617,f1277,f842]) ).
fof(f3411,plain,
( op2(e20,e21) = h1(e10)
| ~ spl8_148 ),
inference(forward_demodulation,[],[f377,f1279]) ).
fof(f3412,plain,
( e23 = h1(e10)
| ~ spl8_148
| ~ spl8_206 ),
inference(forward_demodulation,[],[f3411,f1628]) ).
fof(f3413,plain,
( spl8_58
| ~ spl8_148
| ~ spl8_206 ),
inference(avatar_split_clause,[],[f3412,f1626,f1277,f832]) ).
fof(f3415,plain,
( h1(op1(e10,e11)) != op2(e23,h1(e11))
| spl8_42
| ~ spl8_58 ),
inference(superposition,[],[f770,f833]) ).
fof(f3416,plain,
( op2(e23,e22) != h1(op1(e10,e11))
| spl8_42
| ~ spl8_58
| ~ spl8_60 ),
inference(forward_demodulation,[],[f3415,f843]) ).
fof(f3419,plain,
( op2(e23,e22) != h1(e13)
| spl8_42
| ~ spl8_58
| ~ spl8_60
| ~ spl8_242 ),
inference(forward_demodulation,[],[f3416,f1820]) ).
fof(f3420,plain,
( e20 != op2(e23,e22)
| ~ spl8_2
| spl8_42
| ~ spl8_58
| ~ spl8_60
| ~ spl8_242 ),
inference(forward_demodulation,[],[f3419,f577]) ).
fof(f3421,plain,
( $false
| ~ spl8_2
| spl8_42
| ~ spl8_58
| ~ spl8_60
| ~ spl8_224
| ~ spl8_242 ),
inference(forward_subsumption_resolution,[],[f3420,f1711]) ).
fof(f3422,plain,
( ~ spl8_2
| spl8_42
| ~ spl8_58
| ~ spl8_60
| ~ spl8_224
| ~ spl8_242 ),
inference(avatar_contradiction_clause,[],[f3421]) ).
fof(f3423,plain,
( op2(e23,e23) != h1(op1(e10,e10))
| spl8_41
| ~ spl8_58 ),
inference(forward_demodulation,[],[f766,f833]) ).
fof(f3425,plain,
( op2(e23,e23) != h1(e11)
| spl8_41
| ~ spl8_58
| ~ spl8_176 ),
inference(forward_demodulation,[],[f3423,f1455]) ).
fof(f3427,plain,
( e22 != op2(e23,e23)
| spl8_41
| ~ spl8_58
| ~ spl8_60
| ~ spl8_176 ),
inference(forward_demodulation,[],[f3425,f843]) ).
fof(f3429,plain,
( $false
| spl8_41
| ~ spl8_58
| ~ spl8_60
| ~ spl8_154
| ~ spl8_176 ),
inference(forward_subsumption_resolution,[],[f3427,f1318]) ).
fof(f3430,plain,
( spl8_41
| ~ spl8_58
| ~ spl8_60
| ~ spl8_154
| ~ spl8_176 ),
inference(avatar_contradiction_clause,[],[f3429]) ).
fof(f3433,plain,
( h1(op1(e10,e12)) != op2(h1(e10),e21)
| ~ spl8_8
| spl8_43 ),
inference(forward_demodulation,[],[f774,f606]) ).
fof(f3435,plain,
( op2(e23,e21) != h1(op1(e10,e12))
| ~ spl8_8
| spl8_43
| ~ spl8_58 ),
inference(forward_demodulation,[],[f3433,f833]) ).
fof(f3437,plain,
( op2(e23,e21) != h1(e12)
| ~ spl8_8
| spl8_43
| ~ spl8_58
| ~ spl8_238 ),
inference(forward_demodulation,[],[f3435,f1802]) ).
fof(f3438,plain,
( e21 != op2(e23,e21)
| ~ spl8_8
| spl8_43
| ~ spl8_58
| ~ spl8_238 ),
inference(forward_demodulation,[],[f3437,f606]) ).
fof(f3439,plain,
( $false
| ~ spl8_8
| spl8_43
| ~ spl8_58
| ~ spl8_216
| ~ spl8_238 ),
inference(forward_subsumption_resolution,[],[f3438,f1673]) ).
fof(f3440,plain,
( ~ spl8_8
| spl8_43
| ~ spl8_58
| ~ spl8_216
| ~ spl8_238 ),
inference(avatar_contradiction_clause,[],[f3439]) ).
fof(f3442,plain,
( h1(op1(e10,e13)) != op2(h1(e10),e20)
| ~ spl8_2
| spl8_44 ),
inference(forward_demodulation,[],[f778,f577]) ).
fof(f3444,plain,
( op2(e23,e20) != h1(op1(e10,e13))
| ~ spl8_2
| spl8_44
| ~ spl8_58 ),
inference(forward_demodulation,[],[f3442,f833]) ).
fof(f3446,plain,
( op2(e23,e20) != h1(e10)
| ~ spl8_2
| spl8_44
| ~ spl8_58
| ~ spl8_186 ),
inference(forward_demodulation,[],[f3444,f1525]) ).
fof(f3448,plain,
( e23 != op2(e23,e20)
| ~ spl8_2
| spl8_44
| ~ spl8_58
| ~ spl8_186 ),
inference(forward_demodulation,[],[f3446,f833]) ).
fof(f3452,plain,
( h1(op1(e11,e10)) != op2(h1(e11),e23)
| spl8_45
| ~ spl8_58 ),
inference(forward_demodulation,[],[f782,f833]) ).
fof(f3454,plain,
( op2(e22,e23) != h1(op1(e11,e10))
| spl8_45
| ~ spl8_58
| ~ spl8_60 ),
inference(forward_demodulation,[],[f3452,f843]) ).
fof(f3456,plain,
( op2(e22,e23) != h1(e12)
| spl8_45
| ~ spl8_58
| ~ spl8_60
| ~ spl8_240 ),
inference(forward_demodulation,[],[f3454,f1811]) ).
fof(f3458,plain,
( e21 != op2(e22,e23)
| ~ spl8_8
| spl8_45
| ~ spl8_58
| ~ spl8_60
| ~ spl8_240 ),
inference(forward_demodulation,[],[f3456,f606]) ).
fof(f3459,plain,
( $false
| ~ spl8_8
| spl8_45
| ~ spl8_58
| ~ spl8_60
| ~ spl8_225
| ~ spl8_240 ),
inference(forward_subsumption_resolution,[],[f3458,f1716]) ).
fof(f3460,plain,
( ~ spl8_8
| spl8_45
| ~ spl8_58
| ~ spl8_60
| ~ spl8_225
| ~ spl8_240 ),
inference(avatar_contradiction_clause,[],[f3459]) ).
fof(f3462,plain,
( op2(e22,e22) != h1(op1(e11,e11))
| spl8_46
| ~ spl8_60 ),
inference(forward_demodulation,[],[f786,f843]) ).
fof(f3464,plain,
( op2(e22,e22) != h1(e10)
| spl8_46
| ~ spl8_60
| ~ spl8_166 ),
inference(forward_demodulation,[],[f3462,f1398]) ).
fof(f3466,plain,
( e23 != op2(e22,e22)
| spl8_46
| ~ spl8_58
| ~ spl8_60
| ~ spl8_166 ),
inference(forward_demodulation,[],[f3464,f833]) ).
fof(f3468,plain,
( $false
| spl8_46
| ~ spl8_58
| ~ spl8_60
| ~ spl8_164
| ~ spl8_166 ),
inference(forward_subsumption_resolution,[],[f3466,f1378]) ).
fof(f3469,plain,
( spl8_46
| ~ spl8_58
| ~ spl8_60
| ~ spl8_164
| ~ spl8_166 ),
inference(avatar_contradiction_clause,[],[f3468]) ).
fof(f3471,plain,
( h1(op1(e11,e12)) != op2(h1(e11),e21)
| ~ spl8_8
| spl8_47 ),
inference(forward_demodulation,[],[f790,f606]) ).
fof(f3473,plain,
( op2(e22,e21) != h1(op1(e11,e12))
| ~ spl8_8
| spl8_47
| ~ spl8_60 ),
inference(forward_demodulation,[],[f3471,f843]) ).
fof(f3475,plain,
( op2(e22,e21) != h1(e11)
| ~ spl8_8
| spl8_47
| ~ spl8_60
| ~ spl8_184 ),
inference(forward_demodulation,[],[f3473,f1503]) ).
fof(f3476,plain,
( e22 != op2(e22,e21)
| ~ spl8_8
| spl8_47
| ~ spl8_60
| ~ spl8_184 ),
inference(forward_demodulation,[],[f3475,f843]) ).
fof(f3480,plain,
( h1(op1(e11,e13)) != op2(h1(e11),e20)
| ~ spl8_2
| spl8_48 ),
inference(forward_demodulation,[],[f794,f577]) ).
fof(f3482,plain,
( op2(e22,e20) != h1(op1(e11,e13))
| ~ spl8_2
| spl8_48
| ~ spl8_60 ),
inference(forward_demodulation,[],[f3480,f843]) ).
fof(f3484,plain,
( op2(e22,e20) != h1(e13)
| ~ spl8_2
| spl8_48
| ~ spl8_60
| ~ spl8_257 ),
inference(forward_demodulation,[],[f3482,f1888]) ).
fof(f3486,plain,
( e20 != op2(e22,e20)
| ~ spl8_2
| spl8_48
| ~ spl8_60
| ~ spl8_257 ),
inference(forward_demodulation,[],[f3484,f577]) ).
fof(f3487,plain,
( $false
| ~ spl8_2
| spl8_48
| ~ spl8_60
| ~ spl8_194
| ~ spl8_257 ),
inference(forward_subsumption_resolution,[],[f3486,f1575]) ).
fof(f3488,plain,
( ~ spl8_2
| spl8_48
| ~ spl8_60
| ~ spl8_194
| ~ spl8_257 ),
inference(avatar_contradiction_clause,[],[f3487]) ).
fof(f3490,plain,
( h1(op1(e12,e10)) != op2(h1(e12),e23)
| spl8_49
| ~ spl8_58 ),
inference(forward_demodulation,[],[f798,f833]) ).
fof(f3492,plain,
( op2(e21,e23) != h1(op1(e12,e10))
| ~ spl8_8
| spl8_49
| ~ spl8_58 ),
inference(forward_demodulation,[],[f3490,f606]) ).
fof(f3494,plain,
( op2(e21,e23) != h1(e10)
| ~ spl8_8
| spl8_49
| ~ spl8_58
| ~ spl8_230 ),
inference(forward_demodulation,[],[f3492,f1767]) ).
fof(f3496,plain,
( e23 != op2(e21,e23)
| ~ spl8_8
| spl8_49
| ~ spl8_58
| ~ spl8_230 ),
inference(forward_demodulation,[],[f3494,f833]) ).
fof(f3497,plain,
( $false
| ~ spl8_8
| spl8_49
| ~ spl8_58
| ~ spl8_221
| ~ spl8_230 ),
inference(forward_subsumption_resolution,[],[f3496,f1696]) ).
fof(f3498,plain,
( ~ spl8_8
| spl8_49
| ~ spl8_58
| ~ spl8_221
| ~ spl8_230 ),
inference(avatar_contradiction_clause,[],[f3497]) ).
fof(f3500,plain,
( h1(op1(e12,e11)) != op2(h1(e12),e22)
| spl8_50
| ~ spl8_60 ),
inference(forward_demodulation,[],[f802,f843]) ).
fof(f3502,plain,
( op2(e21,e22) != h1(op1(e12,e11))
| ~ spl8_8
| spl8_50
| ~ spl8_60 ),
inference(forward_demodulation,[],[f3500,f606]) ).
fof(f3504,plain,
( op2(e21,e22) != h1(e12)
| ~ spl8_8
| spl8_50
| ~ spl8_60
| ~ spl8_174 ),
inference(forward_demodulation,[],[f3502,f1445]) ).
fof(f3506,plain,
( e21 != op2(e21,e22)
| ~ spl8_8
| spl8_50
| ~ spl8_60
| ~ spl8_174 ),
inference(forward_demodulation,[],[f3504,f606]) ).
fof(f3507,plain,
( $false
| ~ spl8_8
| spl8_50
| ~ spl8_60
| ~ spl8_156
| ~ spl8_174 ),
inference(forward_subsumption_resolution,[],[f3506,f1327]) ).
fof(f3508,plain,
( ~ spl8_8
| spl8_50
| ~ spl8_60
| ~ spl8_156
| ~ spl8_174 ),
inference(avatar_contradiction_clause,[],[f3507]) ).
fof(f3510,plain,
( op2(e21,e21) != h1(op1(e12,e12))
| ~ spl8_8
| spl8_51 ),
inference(forward_demodulation,[],[f806,f606]) ).
fof(f3512,plain,
( op2(e21,e21) != h1(e13)
| ~ spl8_8
| spl8_51
| ~ spl8_192 ),
inference(forward_demodulation,[],[f3510,f1554]) ).
fof(f3514,plain,
( e20 != op2(e21,e21)
| ~ spl8_2
| ~ spl8_8
| spl8_51
| ~ spl8_192 ),
inference(forward_demodulation,[],[f3512,f577]) ).
fof(f3519,plain,
( h1(op1(e12,e13)) != op2(h1(e12),e20)
| ~ spl8_2
| spl8_52 ),
inference(forward_demodulation,[],[f810,f577]) ).
fof(f3521,plain,
( op2(e21,e20) != h1(op1(e12,e13))
| ~ spl8_2
| ~ spl8_8
| spl8_52 ),
inference(forward_demodulation,[],[f3519,f606]) ).
fof(f3523,plain,
( op2(e21,e20) != h1(e11)
| ~ spl8_2
| ~ spl8_8
| spl8_52
| ~ spl8_261 ),
inference(forward_demodulation,[],[f3521,f1908]) ).
fof(f3524,plain,
( e22 != op2(e21,e20)
| ~ spl8_2
| ~ spl8_8
| spl8_52
| ~ spl8_60
| ~ spl8_261 ),
inference(forward_demodulation,[],[f3523,f843]) ).
fof(f3525,plain,
( $false
| ~ spl8_2
| ~ spl8_8
| spl8_52
| ~ spl8_60
| ~ spl8_204
| ~ spl8_261 ),
inference(forward_subsumption_resolution,[],[f3524,f1619]) ).
fof(f3526,plain,
( ~ spl8_2
| ~ spl8_8
| spl8_52
| ~ spl8_60
| ~ spl8_204
| ~ spl8_261 ),
inference(avatar_contradiction_clause,[],[f3525]) ).
fof(f3528,plain,
( h1(op1(e13,e10)) != op2(h1(e13),e23)
| spl8_53
| ~ spl8_58 ),
inference(forward_demodulation,[],[f814,f833]) ).
fof(f3530,plain,
( op2(e20,e23) != h1(op1(e13,e10))
| ~ spl8_2
| spl8_53
| ~ spl8_58 ),
inference(forward_demodulation,[],[f3528,f577]) ).
fof(f3532,plain,
( op2(e20,e23) != h1(e13)
| ~ spl8_2
| spl8_53
| ~ spl8_58
| ~ spl8_171 ),
inference(forward_demodulation,[],[f3530,f1425]) ).
fof(f3534,plain,
( e20 != op2(e20,e23)
| ~ spl8_2
| spl8_53
| ~ spl8_58
| ~ spl8_171 ),
inference(forward_demodulation,[],[f3532,f577]) ).
fof(f3535,plain,
( $false
| ~ spl8_2
| spl8_53
| ~ spl8_58
| ~ spl8_158
| ~ spl8_171 ),
inference(forward_subsumption_resolution,[],[f3534,f1349]) ).
fof(f3536,plain,
( ~ spl8_2
| spl8_53
| ~ spl8_58
| ~ spl8_158
| ~ spl8_171 ),
inference(avatar_contradiction_clause,[],[f3535]) ).
fof(f3538,plain,
( h1(op1(e13,e11)) != op2(h1(e13),e22)
| spl8_54
| ~ spl8_60 ),
inference(forward_demodulation,[],[f818,f843]) ).
fof(f3540,plain,
( op2(e20,e22) != h1(op1(e13,e11))
| ~ spl8_2
| spl8_54
| ~ spl8_60 ),
inference(forward_demodulation,[],[f3538,f577]) ).
fof(f3542,plain,
( op2(e20,e22) != h1(e11)
| ~ spl8_2
| spl8_54
| ~ spl8_60
| ~ spl8_252 ),
inference(forward_demodulation,[],[f3540,f1865]) ).
fof(f3544,plain,
( e22 != op2(e20,e22)
| ~ spl8_2
| spl8_54
| ~ spl8_60
| ~ spl8_252 ),
inference(forward_demodulation,[],[f3542,f843]) ).
fof(f3545,plain,
( $false
| ~ spl8_2
| spl8_54
| ~ spl8_60
| ~ spl8_202
| ~ spl8_252 ),
inference(forward_subsumption_resolution,[],[f3544,f1610]) ).
fof(f3546,plain,
( ~ spl8_2
| spl8_54
| ~ spl8_60
| ~ spl8_202
| ~ spl8_252 ),
inference(avatar_contradiction_clause,[],[f3545]) ).
fof(f3548,plain,
( h1(op1(e13,e12)) != op2(h1(e13),e21)
| ~ spl8_8
| spl8_55 ),
inference(forward_demodulation,[],[f822,f606]) ).
fof(f3550,plain,
( op2(e20,e21) != h1(op1(e13,e12))
| ~ spl8_2
| ~ spl8_8
| spl8_55 ),
inference(forward_demodulation,[],[f3548,f577]) ).
fof(f3552,plain,
( op2(e20,e21) != h1(e10)
| ~ spl8_2
| ~ spl8_8
| spl8_55
| ~ spl8_260 ),
inference(forward_demodulation,[],[f3550,f1903]) ).
fof(f3554,plain,
( e23 != op2(e20,e21)
| ~ spl8_2
| ~ spl8_8
| spl8_55
| ~ spl8_58
| ~ spl8_260 ),
inference(forward_demodulation,[],[f3552,f833]) ).
fof(f3555,plain,
( $false
| ~ spl8_2
| ~ spl8_8
| spl8_55
| ~ spl8_58
| ~ spl8_206
| ~ spl8_260 ),
inference(forward_subsumption_resolution,[],[f3554,f1628]) ).
fof(f3556,plain,
( ~ spl8_2
| ~ spl8_8
| spl8_55
| ~ spl8_58
| ~ spl8_206
| ~ spl8_260 ),
inference(avatar_contradiction_clause,[],[f3555]) ).
fof(f3558,plain,
( op2(e20,e20) != h1(op1(e13,e13))
| ~ spl8_2
| spl8_56 ),
inference(forward_demodulation,[],[f826,f577]) ).
fof(f3560,plain,
( op2(e20,e20) != h1(e12)
| ~ spl8_2
| spl8_56
| ~ spl8_182 ),
inference(forward_demodulation,[],[f3558,f1494]) ).
fof(f3562,plain,
( op2(e20,e20) != e21
| ~ spl8_2
| ~ spl8_8
| spl8_56
| ~ spl8_182 ),
inference(forward_demodulation,[],[f3560,f606]) ).
fof(f3564,plain,
( $false
| ~ spl8_2
| ~ spl8_8
| spl8_56
| ~ spl8_148
| ~ spl8_182 ),
inference(forward_subsumption_resolution,[],[f3562,f1279]) ).
fof(f3565,plain,
( ~ spl8_2
| ~ spl8_8
| spl8_56
| ~ spl8_148
| ~ spl8_182 ),
inference(avatar_contradiction_clause,[],[f3564]) ).
fof(f3579,plain,
( e21 != op2(e22,e22)
| ~ spl8_225 ),
inference(forward_demodulation,[],[f171,f1716]) ).
fof(f3580,plain,
( e20 != op2(e22,e22)
| ~ spl8_224 ),
inference(forward_demodulation,[],[f195,f1711]) ).
fof(f3602,plain,
( ~ spl8_142
| ~ spl8_224 ),
inference(avatar_split_clause,[],[f3580,f1709,f1240]) ).
fof(f3617,plain,
( ~ spl8_138
| ~ spl8_2
| ~ spl8_8
| spl8_51
| ~ spl8_192 ),
inference(avatar_split_clause,[],[f3514,f1552,f804,f605,f576,f1220]) ).
fof(f3623,plain,
( spl8_224
| ~ spl8_154 ),
inference(avatar_split_clause,[],[f3404,f1316,f1709]) ).
fof(f3629,plain,
( e22 != op2(e22,e20)
| ~ spl8_204 ),
inference(forward_demodulation,[],[f209,f1619]) ).
fof(f3647,plain,
( $false
| ~ spl8_22
| ~ spl8_105
| ~ spl8_148
| spl8_149 ),
inference(forward_subsumption_resolution,[],[f2012,f1285]) ).
fof(f3648,plain,
( ~ spl8_22
| ~ spl8_105
| ~ spl8_148
| spl8_149 ),
inference(avatar_contradiction_clause,[],[f3647]) ).
fof(f3654,plain,
( ~ spl8_146
| ~ spl8_8
| spl8_47
| ~ spl8_60
| ~ spl8_184 ),
inference(avatar_split_clause,[],[f3476,f1502,f842,f788,f605,f1268]) ).
fof(f3685,plain,
( ~ spl8_207
| ~ spl8_164 ),
inference(avatar_split_clause,[],[f3108,f1376,f1630]) ).
fof(f3690,plain,
( ~ spl8_195
| ~ spl8_224 ),
inference(avatar_split_clause,[],[f3376,f1709,f1577]) ).
fof(f3694,plain,
( ~ spl8_139
| ~ spl8_204 ),
inference(avatar_split_clause,[],[f3629,f1617,f1224]) ).
fof(f3717,plain,
( ~ spl8_143
| ~ spl8_2
| spl8_44
| ~ spl8_58
| ~ spl8_186 ),
inference(avatar_split_clause,[],[f3448,f1524,f832,f776,f576,f1248]) ).
fof(f3724,plain,
( ~ spl8_149
| ~ spl8_225 ),
inference(avatar_split_clause,[],[f3579,f1714,f1284]) ).
cnf(s1,plain,
( spl8_1
| ~ spl8_2 ),
inference(sat_conversion,[],[f579]) ).
cnf(s6,plain,
( ~ spl8_6
| ~ spl8_8 ),
inference(sat_conversion,[],[f608]) ).
cnf(s35,plain,
( ~ spl8_1
| spl8_6
| ~ spl8_41
| ~ spl8_42
| ~ spl8_43
| ~ spl8_44
| ~ spl8_45
| ~ spl8_46
| ~ spl8_47
| ~ spl8_48
| ~ spl8_49
| ~ spl8_50
| ~ spl8_51
| ~ spl8_52
| ~ spl8_53
| ~ spl8_54
| ~ spl8_55
| ~ spl8_56
| ~ spl8_58
| ~ spl8_60 ),
inference(sat_conversion,[],[f845]) ).
cnf(s97,plain,
spl8_136,
inference(sat_conversion,[],[f1211]) ).
cnf(s98,plain,
spl8_105,
inference(sat_conversion,[],[f1212]) ).
cnf(s100,plain,
spl8_2,
inference(sat_conversion,[],[f1214]) ).
cnf(s114,plain,
( spl8_137
| spl8_138
| spl8_142
| ~ spl8_143 ),
inference(sat_conversion,[],[f1256]) ).
cnf(s122,plain,
( spl8_145
| spl8_147
| spl8_148
| spl8_149 ),
inference(sat_conversion,[],[f1288]) ).
cnf(s124,plain,
( ~ spl8_145
| spl8_147
| spl8_148
| spl8_149 ),
inference(sat_conversion,[],[f1290]) ).
cnf(s154,plain,
( spl8_159
| spl8_161
| spl8_162
| spl8_164 ),
inference(sat_conversion,[],[f1380]) ).
cnf(s165,plain,
( ~ spl8_165
| spl8_166
| ~ spl8_167
| spl8_168 ),
inference(sat_conversion,[],[f1407]) ).
cnf(s166,plain,
( spl8_165
| spl8_166
| ~ spl8_167
| spl8_168 ),
inference(sat_conversion,[],[f1408]) ).
cnf(s169,plain,
( ~ spl8_165
| spl8_166
| spl8_168
| spl8_170 ),
inference(sat_conversion,[],[f1419]) ).
cnf(s170,plain,
( spl8_165
| spl8_166
| spl8_168
| spl8_170 ),
inference(sat_conversion,[],[f1420]) ).
cnf(s171,plain,
( ~ spl8_165
| spl8_168
| ~ spl8_169
| spl8_170 ),
inference(sat_conversion,[],[f1421]) ).
cnf(s172,plain,
( spl8_165
| spl8_168
| ~ spl8_169
| spl8_170 ),
inference(sat_conversion,[],[f1422]) ).
cnf(s181,plain,
( ~ spl8_172
| spl8_173
| ~ spl8_174
| spl8_175 ),
inference(sat_conversion,[],[f1451]) ).
cnf(s182,plain,
( spl8_173
| ~ spl8_174
| spl8_175
| spl8_176 ),
inference(sat_conversion,[],[f1456]) ).
cnf(s184,plain,
( ~ spl8_173
| ~ spl8_174
| spl8_175
| spl8_176 ),
inference(sat_conversion,[],[f1458]) ).
cnf(s186,plain,
( spl8_173
| spl8_175
| spl8_176
| spl8_177 ),
inference(sat_conversion,[],[f1464]) ).
cnf(s188,plain,
( ~ spl8_173
| spl8_175
| spl8_176
| spl8_177 ),
inference(sat_conversion,[],[f1466]) ).
cnf(s210,plain,
( spl8_180
| spl8_181
| spl8_183
| ~ spl8_185 ),
inference(sat_conversion,[],[f1520]) ).
cnf(s212,plain,
( spl8_181
| spl8_183
| ~ spl8_184
| ~ spl8_185 ),
inference(sat_conversion,[],[f1522]) ).
cnf(s218,plain,
( spl8_187
| spl8_189
| spl8_190
| spl8_192 ),
inference(sat_conversion,[],[f1556]) ).
cnf(s235,plain,
( spl8_162
| spl8_206
| spl8_207
| spl8_208 ),
inference(sat_conversion,[],[f1637]) ).
cnf(s241,plain,
( spl8_152
| spl8_204
| spl8_217
| spl8_218 ),
inference(sat_conversion,[],[f1683]) ).
cnf(s243,plain,
( spl8_159
| spl8_209
| spl8_220
| spl8_221 ),
inference(sat_conversion,[],[f1697]) ).
cnf(s245,plain,
( spl8_142
| spl8_194
| spl8_213
| spl8_223 ),
inference(sat_conversion,[],[f1707]) ).
cnf(s248,plain,
( spl8_149
| spl8_156
| spl8_197
| spl8_226 ),
inference(sat_conversion,[],[f1722]) ).
cnf(s249,plain,
( spl8_139
| spl8_146
| spl8_153
| spl8_160 ),
inference(sat_conversion,[],[f1723]) ).
cnf(s254,plain,
( spl8_140
| spl8_158
| spl8_212
| spl8_223 ),
inference(sat_conversion,[],[f1736]) ).
cnf(s255,plain,
( spl8_147
| spl8_200
| spl8_216
| spl8_226 ),
inference(sat_conversion,[],[f1737]) ).
cnf(s263,plain,
( spl8_151
| spl8_197
| spl8_202
| spl8_207 ),
inference(sat_conversion,[],[f1745]) ).
cnf(s273,plain,
( spl8_143
| spl8_195
| spl8_200
| spl8_205 ),
inference(sat_conversion,[],[f1755]) ).
cnf(s277,plain,
( spl8_165
| spl8_172
| spl8_179
| spl8_186 ),
inference(sat_conversion,[],[f1759]) ).
cnf(s278,plain,
( spl8_165
| spl8_229
| spl8_230
| spl8_231 ),
inference(sat_conversion,[],[f1772]) ).
cnf(s282,plain,
( spl8_167
| spl8_183
| spl8_240
| spl8_241 ),
inference(sat_conversion,[],[f1816]) ).
cnf(s287,plain,
( spl8_169
| spl8_173
| spl8_184
| spl8_191 ),
inference(sat_conversion,[],[f1857]) ).
cnf(s289,plain,
( spl8_180
| spl8_240
| spl8_253
| spl8_254 ),
inference(sat_conversion,[],[f1875]) ).
cnf(s290,plain,
( spl8_174
| spl8_180
| spl8_237
| spl8_255 ),
inference(sat_conversion,[],[f1880]) ).
cnf(s291,plain,
( spl8_187
| spl8_245
| spl8_256
| spl8_257 ),
inference(sat_conversion,[],[f1889]) ).
cnf(s292,plain,
( spl8_178
| spl8_187
| spl8_242
| spl8_258 ),
inference(sat_conversion,[],[f1894]) ).
cnf(s297,plain,
( spl8_167
| spl8_174
| spl8_181
| spl8_188 ),
inference(sat_conversion,[],[f1915]) ).
cnf(s298,plain,
( spl8_181
| spl8_238
| spl8_253
| spl8_263 ),
inference(sat_conversion,[],[f1920]) ).
cnf(s300,plain,
( spl8_185
| spl8_192
| spl8_243
| spl8_256 ),
inference(sat_conversion,[],[f1926]) ).
cnf(s303,plain,
( spl8_175
| spl8_236
| spl8_252
| spl8_262 ),
inference(sat_conversion,[],[f1929]) ).
cnf(s307,plain,
( spl8_171
| spl8_178
| spl8_185
| spl8_189 ),
inference(sat_conversion,[],[f1933]) ).
cnf(s323,plain,
( spl8_185
| spl8_260
| spl8_262
| spl8_263 ),
inference(sat_conversion,[],[f1949]) ).
cnf(s325,plain,
spl8_182,
inference(sat_conversion,[],[f1954]) ).
cnf(s326,plain,
spl8_154,
inference(sat_conversion,[],[f1955]) ).
cnf(s331,plain,
( ~ spl8_137
| ~ spl8_148 ),
inference(sat_conversion,[],[f1973]) ).
cnf(s338,plain,
( spl8_22
| ~ spl8_105
| ~ spl8_140
| ~ spl8_154 ),
inference(sat_conversion,[],[f2001]) ).
cnf(s356,plain,
( ~ spl8_154
| ~ spl8_161 ),
inference(sat_conversion,[],[f2078]) ).
cnf(s358,plain,
( spl8_37
| ~ spl8_136
| ~ spl8_148
| ~ spl8_162 ),
inference(sat_conversion,[],[f2087]) ).
cnf(s359,plain,
( ~ spl8_147
| ~ spl8_154 ),
inference(sat_conversion,[],[f2091]) ).
cnf(s360,plain,
( ~ spl8_37
| ~ spl8_136 ),
inference(sat_conversion,[],[f2109]) ).
cnf(s365,plain,
( ~ spl8_166
| ~ spl8_173 ),
inference(sat_conversion,[],[f2135]) ).
cnf(s367,plain,
( ~ spl8_165
| ~ spl8_176 ),
inference(sat_conversion,[],[f2143]) ).
cnf(s368,plain,
( ~ spl8_170
| ~ spl8_177 ),
inference(sat_conversion,[],[f2147]) ).
cnf(s370,plain,
( ~ spl8_168
| ~ spl8_182 ),
inference(sat_conversion,[],[f2156]) ).
cnf(s371,plain,
( ~ spl8_176
| ~ spl8_183 ),
inference(sat_conversion,[],[f2162]) ).
cnf(s373,plain,
( ~ spl8_173
| ~ spl8_187 ),
inference(sat_conversion,[],[f2170]) ).
cnf(s375,plain,
( ~ spl8_182
| ~ spl8_189 ),
inference(sat_conversion,[],[f2179]) ).
cnf(s377,plain,
( ~ spl8_176
| ~ spl8_190 ),
inference(sat_conversion,[],[f2187]) ).
cnf(s379,plain,
( ~ spl8_170
| ~ spl8_192 ),
inference(sat_conversion,[],[f2194]) ).
cnf(s381,plain,
( ~ spl8_175
| ~ spl8_182 ),
inference(sat_conversion,[],[f2202]) ).
cnf(s387,plain,
( ~ spl8_160
| ~ spl8_225 ),
inference(sat_conversion,[],[f2235]) ).
cnf(s399,plain,
( ~ spl8_138
| ~ spl8_159 ),
inference(sat_conversion,[],[f2284]) ).
cnf(s410,plain,
( spl8_22
| ~ spl8_105
| ~ spl8_138
| ~ spl8_152 ),
inference(sat_conversion,[],[f2334]) ).
cnf(s428,plain,
( spl8_37
| ~ spl8_136
| ~ spl8_156
| ~ spl8_220 ),
inference(sat_conversion,[],[f2434]) ).
cnf(s441,plain,
( ~ spl8_204
| ~ spl8_209 ),
inference(sat_conversion,[],[f2510]) ).
cnf(s448,plain,
( ~ spl8_224
| ~ spl8_226 ),
inference(sat_conversion,[],[f2548]) ).
cnf(s453,plain,
( ~ spl8_179
| ~ spl8_238 ),
inference(sat_conversion,[],[f2574]) ).
cnf(s458,plain,
( ~ spl8_229
| ~ spl8_240 ),
inference(sat_conversion,[],[f2595]) ).
cnf(s461,plain,
( ~ spl8_166
| ~ spl8_187 ),
inference(sat_conversion,[],[f2606]) ).
cnf(s462,plain,
( ~ spl8_165
| ~ spl8_183 ),
inference(sat_conversion,[],[f2610]) ).
cnf(s463,plain,
( ~ spl8_177
| ~ spl8_181 ),
inference(sat_conversion,[],[f2614]) ).
cnf(s467,plain,
( ~ spl8_171
| ~ spl8_231 ),
inference(sat_conversion,[],[f2635]) ).
cnf(s468,plain,
( ~ spl8_166
| ~ spl8_180 ),
inference(sat_conversion,[],[f2638]) ).
cnf(s496,plain,
( ~ spl8_184
| ~ spl8_256 ),
inference(sat_conversion,[],[f2768]) ).
cnf(s508,plain,
( ~ spl8_184
| ~ spl8_253 ),
inference(sat_conversion,[],[f2850]) ).
cnf(s509,plain,
( ~ spl8_240
| ~ spl8_245 ),
inference(sat_conversion,[],[f2854]) ).
cnf(s513,plain,
( ~ spl8_178
| ~ spl8_252 ),
inference(sat_conversion,[],[f2876]) ).
cnf(s516,plain,
( ~ spl8_238
| ~ spl8_243 ),
inference(sat_conversion,[],[f2888]) ).
cnf(s518,plain,
( ~ spl8_180
| ~ spl8_187 ),
inference(sat_conversion,[],[f2901]) ).
cnf(s524,plain,
( ~ spl8_188
| ~ spl8_261 ),
inference(sat_conversion,[],[f2948]) ).
cnf(s529,plain,
( spl8_8
| ~ spl8_148 ),
inference(sat_conversion,[],[f2999]) ).
cnf(s535,plain,
( ~ spl8_182
| ~ spl8_263 ),
inference(sat_conversion,[],[f3128]) ).
cnf(s536,plain,
( ~ spl8_182
| spl8_261 ),
inference(sat_conversion,[],[f3135]) ).
cnf(s538,plain,
( ~ spl8_182
| ~ spl8_241 ),
inference(sat_conversion,[],[f3139]) ).
cnf(s540,plain,
( ~ spl8_181
| ~ spl8_192 ),
inference(sat_conversion,[],[f3148]) ).
cnf(s544,plain,
( ~ spl8_191
| ~ spl8_261 ),
inference(sat_conversion,[],[f3152]) ).
cnf(s545,plain,
( ~ spl8_176
| ~ spl8_236 ),
inference(sat_conversion,[],[f3153]) ).
cnf(s546,plain,
( ~ spl8_237
| ~ spl8_238 ),
inference(sat_conversion,[],[f3154]) ).
cnf(s548,plain,
( ~ spl8_182
| ~ spl8_254 ),
inference(sat_conversion,[],[f3158]) ).
cnf(s549,plain,
( ~ spl8_182
| ~ spl8_255 ),
inference(sat_conversion,[],[f3159]) ).
cnf(s552,plain,
( ~ spl8_170
| ~ spl8_181 ),
inference(sat_conversion,[],[f3167]) ).
cnf(s554,plain,
( ~ spl8_240
| ~ spl8_253 ),
inference(sat_conversion,[],[f3169]) ).
cnf(s557,plain,
( ~ spl8_184
| ~ spl8_262 ),
inference(sat_conversion,[],[f3171]) ).
cnf(s560,plain,
( ~ spl8_169
| ~ spl8_176 ),
inference(sat_conversion,[],[f3175]) ).
cnf(s562,plain,
( ~ spl8_192
| ~ spl8_258 ),
inference(sat_conversion,[],[f3176]) ).
cnf(s567,plain,
( ~ spl8_154
| ~ spl8_223 ),
inference(sat_conversion,[],[f3276]) ).
cnf(s568,plain,
( ~ spl8_154
| spl8_225 ),
inference(sat_conversion,[],[f3281]) ).
cnf(s574,plain,
( ~ spl8_156
| ~ spl8_217 ),
inference(sat_conversion,[],[f3300]) ).
cnf(s577,plain,
( ~ spl8_138
| ~ spl8_213 ),
inference(sat_conversion,[],[f3303]) ).
cnf(s578,plain,
( ~ spl8_148
| ~ spl8_200 ),
inference(sat_conversion,[],[f3304]) ).
cnf(s579,plain,
( ~ spl8_138
| ~ spl8_212 ),
inference(sat_conversion,[],[f3305]) ).
cnf(s588,plain,
( ~ spl8_154
| ~ spl8_218 ),
inference(sat_conversion,[],[f3316]) ).
cnf(s590,plain,
( ~ spl8_154
| ~ spl8_205 ),
inference(sat_conversion,[],[f3320]) ).
cnf(s591,plain,
( ~ spl8_153
| ~ spl8_164 ),
inference(sat_conversion,[],[f3323]) ).
cnf(s592,plain,
( ~ spl8_158
| ~ spl8_208 ),
inference(sat_conversion,[],[f3325]) ).
cnf(s596,plain,
( ~ spl8_151
| ~ spl8_224 ),
inference(sat_conversion,[],[f3335]) ).
cnf(s598,plain,
( ~ spl8_148
| ~ spl8_197 ),
inference(sat_conversion,[],[f3338]) ).
cnf(s599,plain,
( spl8_60
| ~ spl8_148
| ~ spl8_204 ),
inference(sat_conversion,[],[f3407]) ).
cnf(s600,plain,
( spl8_58
| ~ spl8_148
| ~ spl8_206 ),
inference(sat_conversion,[],[f3413]) ).
cnf(s602,plain,
( ~ spl8_2
| spl8_42
| ~ spl8_58
| ~ spl8_60
| ~ spl8_224
| ~ spl8_242 ),
inference(sat_conversion,[],[f3422]) ).
cnf(s603,plain,
( spl8_41
| ~ spl8_58
| ~ spl8_60
| ~ spl8_154
| ~ spl8_176 ),
inference(sat_conversion,[],[f3430]) ).
cnf(s604,plain,
( ~ spl8_8
| spl8_43
| ~ spl8_58
| ~ spl8_216
| ~ spl8_238 ),
inference(sat_conversion,[],[f3440]) ).
cnf(s606,plain,
( ~ spl8_8
| spl8_45
| ~ spl8_58
| ~ spl8_60
| ~ spl8_225
| ~ spl8_240 ),
inference(sat_conversion,[],[f3460]) ).
cnf(s607,plain,
( spl8_46
| ~ spl8_58
| ~ spl8_60
| ~ spl8_164
| ~ spl8_166 ),
inference(sat_conversion,[],[f3469]) ).
cnf(s609,plain,
( ~ spl8_2
| spl8_48
| ~ spl8_60
| ~ spl8_194
| ~ spl8_257 ),
inference(sat_conversion,[],[f3488]) ).
cnf(s610,plain,
( ~ spl8_8
| spl8_49
| ~ spl8_58
| ~ spl8_221
| ~ spl8_230 ),
inference(sat_conversion,[],[f3498]) ).
cnf(s611,plain,
( ~ spl8_8
| spl8_50
| ~ spl8_60
| ~ spl8_156
| ~ spl8_174 ),
inference(sat_conversion,[],[f3508]) ).
cnf(s613,plain,
( ~ spl8_2
| ~ spl8_8
| spl8_52
| ~ spl8_60
| ~ spl8_204
| ~ spl8_261 ),
inference(sat_conversion,[],[f3526]) ).
cnf(s614,plain,
( ~ spl8_2
| spl8_53
| ~ spl8_58
| ~ spl8_158
| ~ spl8_171 ),
inference(sat_conversion,[],[f3536]) ).
cnf(s615,plain,
( ~ spl8_2
| spl8_54
| ~ spl8_60
| ~ spl8_202
| ~ spl8_252 ),
inference(sat_conversion,[],[f3546]) ).
cnf(s616,plain,
( ~ spl8_2
| ~ spl8_8
| spl8_55
| ~ spl8_58
| ~ spl8_206
| ~ spl8_260 ),
inference(sat_conversion,[],[f3556]) ).
cnf(s617,plain,
( ~ spl8_2
| ~ spl8_8
| spl8_56
| ~ spl8_148
| ~ spl8_182 ),
inference(sat_conversion,[],[f3565]) ).
cnf(s629,plain,
( ~ spl8_142
| ~ spl8_224 ),
inference(sat_conversion,[],[f3602]) ).
cnf(s632,plain,
( ~ spl8_2
| ~ spl8_8
| spl8_51
| ~ spl8_138
| ~ spl8_192 ),
inference(sat_conversion,[],[f3617]) ).
cnf(s640,plain,
( ~ spl8_154
| spl8_224 ),
inference(sat_conversion,[],[f3623]) ).
cnf(s653,plain,
( ~ spl8_22
| ~ spl8_105
| ~ spl8_148
| spl8_149 ),
inference(sat_conversion,[],[f3648]) ).
cnf(s656,plain,
( ~ spl8_8
| spl8_47
| ~ spl8_60
| ~ spl8_146
| ~ spl8_184 ),
inference(sat_conversion,[],[f3654]) ).
cnf(s676,plain,
( ~ spl8_164
| ~ spl8_207 ),
inference(sat_conversion,[],[f3685]) ).
cnf(s687,plain,
( ~ spl8_195
| ~ spl8_224 ),
inference(sat_conversion,[],[f3690]) ).
cnf(s692,plain,
( ~ spl8_139
| ~ spl8_204 ),
inference(sat_conversion,[],[f3694]) ).
cnf(s702,plain,
( ~ spl8_2
| spl8_44
| ~ spl8_58
| ~ spl8_143
| ~ spl8_186 ),
inference(sat_conversion,[],[f3717]) ).
cnf(s713,plain,
( ~ spl8_149
| ~ spl8_225 ),
inference(sat_conversion,[],[f3724]) ).
cnf(s717,plain,
spl8_224,
inference(rat,[],[s640,s326]) ).
cnf(s720,plain,
~ spl8_205,
inference(rat,[],[s590,s326]) ).
cnf(s721,plain,
~ spl8_218,
inference(rat,[],[s588,s326]) ).
cnf(s723,plain,
spl8_225,
inference(rat,[],[s568,s326]) ).
cnf(s724,plain,
~ spl8_223,
inference(rat,[],[s567,s326]) ).
cnf(s726,plain,
~ spl8_147,
inference(rat,[],[s359,s326]) ).
cnf(s727,plain,
~ spl8_161,
inference(rat,[],[s356,s326]) ).
cnf(s729,plain,
~ spl8_195,
inference(rat,[],[s687,s717]) ).
cnf(s730,plain,
~ spl8_142,
inference(rat,[],[s629,s717]) ).
cnf(s732,plain,
~ spl8_151,
inference(rat,[],[s596,s717]) ).
cnf(s733,plain,
~ spl8_226,
inference(rat,[],[s448,s717]) ).
cnf(s734,plain,
~ spl8_149,
inference(rat,[],[s713,s723]) ).
cnf(s738,plain,
~ spl8_160,
inference(rat,[],[s387,s723]) ).
cnf(s739,plain,
~ spl8_255,
inference(rat,[],[s549,s325]) ).
cnf(s740,plain,
~ spl8_254,
inference(rat,[],[s548,s325]) ).
cnf(s741,plain,
~ spl8_241,
inference(rat,[],[s538,s325]) ).
cnf(s742,plain,
spl8_261,
inference(rat,[],[s536,s325]) ).
cnf(s743,plain,
~ spl8_263,
inference(rat,[],[s535,s325]) ).
cnf(s745,plain,
~ spl8_175,
inference(rat,[],[s381,s325]) ).
cnf(s746,plain,
~ spl8_189,
inference(rat,[],[s375,s325]) ).
cnf(s747,plain,
~ spl8_168,
inference(rat,[],[s370,s325]) ).
cnf(s748,plain,
~ spl8_191,
inference(rat,[],[s544,s742]) ).
cnf(s750,plain,
~ spl8_188,
inference(rat,[],[s524,s742]) ).
cnf(s751,plain,
( spl8_185
| spl8_260
| spl8_262 ),
inference(rat,[],[s323,s743]) ).
cnf(s757,plain,
( spl8_171
| spl8_178
| spl8_185 ),
inference(rat,[],[s307,s746]) ).
cnf(s758,plain,
( spl8_236
| spl8_252
| spl8_262 ),
inference(rat,[],[s303,s745]) ).
cnf(s761,plain,
( spl8_181
| spl8_238
| spl8_253 ),
inference(rat,[],[s298,s743]) ).
cnf(s762,plain,
( spl8_167
| spl8_174
| spl8_181 ),
inference(rat,[],[s297,s750]) ).
cnf(s764,plain,
( spl8_174
| spl8_180
| spl8_237 ),
inference(rat,[],[s290,s739]) ).
cnf(s765,plain,
( spl8_180
| spl8_240
| spl8_253 ),
inference(rat,[],[s289,s740]) ).
cnf(s767,plain,
( spl8_169
| spl8_173
| spl8_184 ),
inference(rat,[],[s287,s748]) ).
cnf(s768,plain,
( spl8_167
| spl8_183
| spl8_240 ),
inference(rat,[],[s282,s741]) ).
cnf(s770,plain,
( spl8_143
| spl8_200 ),
inference(rat,[],[s273,s720,s729]) ).
cnf(s777,plain,
( spl8_197
| spl8_202
| spl8_207 ),
inference(rat,[],[s263,s732]) ).
cnf(s780,plain,
( spl8_200
| spl8_216 ),
inference(rat,[],[s255,s733,s726]) ).
cnf(s781,plain,
( spl8_140
| spl8_158
| spl8_212 ),
inference(rat,[],[s254,s724]) ).
cnf(s783,plain,
( spl8_139
| spl8_146
| spl8_153 ),
inference(rat,[],[s249,s738]) ).
cnf(s784,plain,
( spl8_156
| spl8_197 ),
inference(rat,[],[s248,s733,s734]) ).
cnf(s785,plain,
( spl8_194
| spl8_213 ),
inference(rat,[],[s245,s724,s730]) ).
cnf(s787,plain,
( spl8_152
| spl8_204
| spl8_217 ),
inference(rat,[],[s241,s721]) ).
cnf(s797,plain,
( spl8_187
| spl8_190
| spl8_192 ),
inference(rat,[],[s218,s746]) ).
cnf(s799,plain,
( ~ spl8_173
| spl8_176
| spl8_177 ),
inference(rat,[],[s188,s745]) ).
cnf(s801,plain,
( spl8_173
| spl8_176
| spl8_177 ),
inference(rat,[],[s186,s745]) ).
cnf(s803,plain,
( ~ spl8_173
| ~ spl8_174
| spl8_176 ),
inference(rat,[],[s184,s745]) ).
cnf(s805,plain,
( spl8_173
| ~ spl8_174
| spl8_176 ),
inference(rat,[],[s182,s745]) ).
cnf(s806,plain,
( ~ spl8_172
| spl8_173
| ~ spl8_174 ),
inference(rat,[],[s181,s745]) ).
cnf(s807,plain,
( spl8_165
| ~ spl8_169
| spl8_170 ),
inference(rat,[],[s172,s747]) ).
cnf(s808,plain,
( ~ spl8_165
| ~ spl8_169
| spl8_170 ),
inference(rat,[],[s171,s747]) ).
cnf(s809,plain,
( spl8_165
| spl8_166
| spl8_170 ),
inference(rat,[],[s170,s747]) ).
cnf(s810,plain,
( ~ spl8_165
| spl8_166
| spl8_170 ),
inference(rat,[],[s169,s747]) ).
cnf(s813,plain,
( spl8_165
| spl8_166
| ~ spl8_167 ),
inference(rat,[],[s166,s747]) ).
cnf(s814,plain,
( ~ spl8_165
| spl8_166
| ~ spl8_167 ),
inference(rat,[],[s165,s747]) ).
cnf(s817,plain,
( spl8_159
| spl8_162
| spl8_164 ),
inference(rat,[],[s154,s727]) ).
cnf(s823,plain,
( ~ spl8_145
| spl8_148 ),
inference(rat,[],[s124,s734,s726]) ).
cnf(s825,plain,
( spl8_145
| spl8_148 ),
inference(rat,[],[s122,s734,s726]) ).
cnf(s833,plain,
( spl8_137
| spl8_138
| ~ spl8_143 ),
inference(rat,[],[s114,s730]) ).
cnf(s840,plain,
~ spl8_37,
inference(rat,[],[s360,s97]) ).
cnf(s853,plain,
spl8_1,
inference(rat,[],[s1,s100]) ).
cnf(s854,plain,
spl8_148,
inference(rat,[],[s825,s823]) ).
cnf(s856,plain,
~ spl8_197,
inference(rat,[],[s598,s854]) ).
cnf(s857,plain,
~ spl8_200,
inference(rat,[],[s578,s854]) ).
cnf(s858,plain,
spl8_8,
inference(rat,[],[s529,s854]) ).
cnf(s860,plain,
~ spl8_137,
inference(rat,[],[s331,s854]) ).
cnf(s861,plain,
~ spl8_22,
inference(rat,[],[s653,s734,s98,s854]) ).
cnf(s862,plain,
~ spl8_162,
inference(rat,[],[s358,s840,s97,s854]) ).
cnf(s863,plain,
spl8_156,
inference(rat,[],[s784,s856]) ).
cnf(s864,plain,
spl8_143,
inference(rat,[],[s770,s857]) ).
cnf(s865,plain,
spl8_216,
inference(rat,[],[s780,s857]) ).
cnf(s866,plain,
spl8_56,
inference(rat,[],[s617,s325,s854,s100,s858]) ).
cnf(s867,plain,
~ spl8_6,
inference(rat,[],[s6,s858]) ).
cnf(s869,plain,
spl8_138,
inference(rat,[],[s833,s864,s860]) ).
cnf(s870,plain,
~ spl8_140,
inference(rat,[],[s338,s326,s98,s861]) ).
cnf(s871,plain,
~ spl8_217,
inference(rat,[],[s574,s863]) ).
cnf(s872,plain,
~ spl8_220,
inference(rat,[],[s428,s840,s97,s863]) ).
cnf(s875,plain,
~ spl8_212,
inference(rat,[],[s579,s869]) ).
cnf(s876,plain,
~ spl8_213,
inference(rat,[],[s577,s869]) ).
cnf(s879,plain,
~ spl8_159,
inference(rat,[],[s399,s869]) ).
cnf(s881,plain,
~ spl8_152,
inference(rat,[],[s410,s861,s98,s869]) ).
cnf(s882,plain,
spl8_158,
inference(rat,[],[s781,s875,s870]) ).
cnf(s883,plain,
spl8_204,
inference(rat,[],[s787,s881,s871]) ).
cnf(s884,plain,
spl8_194,
inference(rat,[],[s785,s876]) ).
cnf(s886,plain,
spl8_164,
inference(rat,[],[s817,s862,s879]) ).
cnf(s888,plain,
~ spl8_208,
inference(rat,[],[s592,s882]) ).
cnf(s889,plain,
~ spl8_139,
inference(rat,[],[s692,s883]) ).
cnf(s890,plain,
~ spl8_209,
inference(rat,[],[s441,s883]) ).
cnf(s891,plain,
spl8_60,
inference(rat,[],[s599,s854,s883]) ).
cnf(s892,plain,
~ spl8_207,
inference(rat,[],[s676,s886]) ).
cnf(s893,plain,
~ spl8_153,
inference(rat,[],[s591,s886]) ).
cnf(s897,plain,
spl8_221,
inference(rat,[],[s243,s879,s872,s890]) ).
cnf(s898,plain,
spl8_52,
inference(rat,[],[s613,s742,s883,s858,s100,s891]) ).
cnf(s899,plain,
spl8_206,
inference(rat,[],[s235,s888,s862,s892]) ).
cnf(s900,plain,
spl8_202,
inference(rat,[],[s777,s856,s892]) ).
cnf(s902,plain,
spl8_146,
inference(rat,[],[s783,s889,s893]) ).
cnf(s905,plain,
spl8_58,
inference(rat,[],[s600,s854,s899]) ).
cnf(s906,plain,
( spl8_165
| spl8_174
| spl8_166 ),
inference(rat,[],[s762,s552,s813,s809]) ).
cnf(s907,plain,
( ~ spl8_165
| spl8_166
| spl8_240 ),
inference(rat,[],[s768,s814,s462]) ).
cnf(s908,plain,
( ~ spl8_174
| spl8_176 ),
inference(rat,[],[s805,s803]) ).
cnf(s909,plain,
( spl8_166
| spl8_240
| spl8_174 ),
inference(rat,[],[s906,s907]) ).
cnf(s910,plain,
( ~ spl8_169
| spl8_170 ),
inference(rat,[],[s808,s807]) ).
cnf(s911,plain,
( spl8_240
| spl8_176 ),
inference(rat,[],[s910,s767,s368,s508,s801,s765,s365,s468,s909,s908]) ).
cnf(s912,plain,
( spl8_177
| spl8_176 ),
inference(rat,[],[s801,s799]) ).
cnf(s913,plain,
spl8_176,
inference(rat,[],[s810,s906,s468,s764,s546,s761,s368,s463,s912,s554,s911,s908]) ).
cnf(s914,plain,
~ spl8_169,
inference(rat,[],[s560,s913]) ).
cnf(s916,plain,
~ spl8_236,
inference(rat,[],[s545,s913]) ).
cnf(s917,plain,
~ spl8_190,
inference(rat,[],[s377,s913]) ).
cnf(s918,plain,
~ spl8_183,
inference(rat,[],[s371,s913]) ).
cnf(s919,plain,
~ spl8_165,
inference(rat,[],[s367,s913]) ).
cnf(s920,plain,
spl8_41,
inference(rat,[],[s603,s905,s326,s891,s913]) ).
cnf(s921,plain,
spl8_174,
inference(rat,[],[s761,s508,s540,s546,s767,s797,s764,s365,s461,s468,s906,s914,s917,s919]) ).
cnf(s923,plain,
spl8_50,
inference(rat,[],[s611,s891,s863,s858,s921]) ).
cnf(s924,plain,
spl8_166,
inference(rat,[],[s496,s300,s516,s767,s210,s761,s373,s518,s554,s797,s768,s379,s552,s813,s809,s914,s918,s917,s919]) ).
cnf(s925,plain,
~ spl8_180,
inference(rat,[],[s468,s924]) ).
cnf(s926,plain,
~ spl8_187,
inference(rat,[],[s461,s924]) ).
cnf(s927,plain,
~ spl8_173,
inference(rat,[],[s365,s924]) ).
cnf(s928,plain,
spl8_46,
inference(rat,[],[s607,s905,s886,s891,s924]) ).
cnf(s929,plain,
spl8_192,
inference(rat,[],[s797,s917,s926]) ).
cnf(s930,plain,
spl8_184,
inference(rat,[],[s767,s914,s927]) ).
cnf(s931,plain,
~ spl8_172,
inference(rat,[],[s806,s921,s927]) ).
cnf(s932,plain,
~ spl8_258,
inference(rat,[],[s562,s929]) ).
cnf(s934,plain,
~ spl8_181,
inference(rat,[],[s540,s929]) ).
cnf(s938,plain,
spl8_51,
inference(rat,[],[s632,s869,s858,s100,s929]) ).
cnf(s939,plain,
~ spl8_262,
inference(rat,[],[s557,s930]) ).
cnf(s941,plain,
~ spl8_253,
inference(rat,[],[s508,s930]) ).
cnf(s942,plain,
~ spl8_256,
inference(rat,[],[s496,s930]) ).
cnf(s943,plain,
spl8_47,
inference(rat,[],[s656,s902,s891,s858,s930]) ).
cnf(s944,plain,
~ spl8_185,
inference(rat,[],[s212,s934,s918,s930]) ).
cnf(s945,plain,
spl8_252,
inference(rat,[],[s758,s916,s939]) ).
cnf(s946,plain,
spl8_260,
inference(rat,[],[s751,s944,s939]) ).
cnf(s947,plain,
spl8_240,
inference(rat,[],[s765,s925,s941]) ).
cnf(s948,plain,
spl8_238,
inference(rat,[],[s761,s934,s941]) ).
cnf(s950,plain,
~ spl8_178,
inference(rat,[],[s513,s945]) ).
cnf(s951,plain,
spl8_54,
inference(rat,[],[s615,s900,s891,s100,s945]) ).
cnf(s952,plain,
spl8_55,
inference(rat,[],[s616,s905,s899,s858,s100,s946]) ).
cnf(s953,plain,
~ spl8_245,
inference(rat,[],[s509,s947]) ).
cnf(s954,plain,
~ spl8_229,
inference(rat,[],[s458,s947]) ).
cnf(s955,plain,
spl8_45,
inference(rat,[],[s606,s905,s723,s891,s858,s947]) ).
cnf(s956,plain,
~ spl8_179,
inference(rat,[],[s453,s948]) ).
cnf(s957,plain,
spl8_43,
inference(rat,[],[s604,s905,s865,s858,s948]) ).
cnf(s958,plain,
spl8_171,
inference(rat,[],[s757,s944,s950]) ).
cnf(s959,plain,
spl8_242,
inference(rat,[],[s292,s926,s932,s950]) ).
cnf(s960,plain,
spl8_257,
inference(rat,[],[s291,s926,s942,s953]) ).
cnf(s961,plain,
spl8_186,
inference(rat,[],[s277,s931,s919,s956]) ).
cnf(s962,plain,
~ spl8_231,
inference(rat,[],[s467,s958]) ).
cnf(s963,plain,
spl8_53,
inference(rat,[],[s614,s905,s882,s100,s958]) ).
cnf(s964,plain,
spl8_42,
inference(rat,[],[s602,s905,s717,s891,s100,s959]) ).
cnf(s966,plain,
spl8_48,
inference(rat,[],[s609,s891,s884,s100,s960]) ).
cnf(s970,plain,
spl8_44,
inference(rat,[],[s702,s905,s864,s100,s961]) ).
cnf(s971,plain,
spl8_230,
inference(rat,[],[s278,s919,s954,s962]) ).
cnf(s972,plain,
~ spl8_49,
inference(rat,[],[s35,s891,s905,s866,s952,s951,s963,s898,s938,s923,s964,s966,s943,s928,s955,s957,s920,s867,s853,s970]) ).
cnf(s976,plain,
$false,
inference(rat,[],[s610,s905,s897,s858,s971,s972]) ).
fof(f3750,plain,
$false,
inference(avatar_sat_refutation,[],[s976]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG117+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.09/0.16 % Computer : n001.cluster.edu
% 0.09/0.16 % Model : x86_64 x86_64
% 0.09/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.16 % Memory : 8046.5625MB
% 0.09/0.16 % OS : Linux 6.8.0-71-generic
% 0.09/0.16 % CPULimit : 300
% 0.09/0.16 % WCLimit : 300
% 0.09/0.16 % DateTime : Mon Sep 28 19:36:19 UTC 2026
% 0.09/0.16 % CPUTime :
% 0.09/0.16 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 Running first-order model finding
% 0.09/0.19 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.39/0.33 % (653354)Will run a generic schedule for satisfiability detection.
% 0.39/0.33 % (653362)dis+10_1_sil=32000:sp=arity:random_seed=897360610:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.39/0.33 % (653360)% WARNING: option uhcvi not known.
% 0.39/0.33 % (653360)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4199742347:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.39/0.33 % (653359)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2754550476_2999 on theBenchmark for (2999ds/0Mi)
% 0.39/0.33 % (653361)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3883134728:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.39/0.33 % (653363)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3247267974:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.39/0.33 % (653365)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3436695964:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.39/0.33 % (653364)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3150541803:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.39/0.33 % (653362)Instruction limit reached!
% 0.39/0.33 % (653362)------------------------------
% 0.39/0.33 % (653362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.39/0.33 % (653362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.39/0.33 % (653362)CaDiCaL version: 2.1.3
% 0.39/0.33 % (653362)Termination reason: Instruction limit
% 0.39/0.33 % (653362)Termination phase: Saturation
% 0.39/0.33 % (653362)Time elapsed: 0.028 s
% 0.39/0.33 % (653362)Peak memory usage: 12 MB
% 0.39/0.33 % (653362)Instructions burned: 105 (million)
% 0.39/0.33 % (653373)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3988489286:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.39/0.33 % Detected minimum model sizes of [8]
% 0.39/0.33 % Detected maximum model sizes of [max]
% 0.39/0.33 % TRYING [8]
% 0.39/0.33 % Detected minimum model sizes of [8]
% 0.39/0.33 % Detected maximum model sizes of [max]
% 0.39/0.33 % TRYING [8]
% 0.39/0.33 % (653363)Instruction limit reached!
% 0.39/0.33 % (653363)------------------------------
% 0.39/0.33 % (653363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.39/0.33 % (653363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.39/0.33 % (653363)CaDiCaL version: 2.1.3
% 0.39/0.33 % (653363)Termination reason: Instruction limit
% 0.39/0.33 % (653363)Termination phase: Saturation
% 0.39/0.33 % (653363)Time elapsed: 0.055 s
% 0.39/0.33 % (653363)Peak memory usage: 13 MB
% 0.39/0.33 % (653363)Instructions burned: 117 (million)
% 0.39/0.33 % (653364)Instruction limit reached!
% 0.39/0.33 % (653364)------------------------------
% 0.39/0.33 % (653364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.39/0.33 % (653364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.39/0.33 % (653364)CaDiCaL version: 2.1.3
% 0.39/0.33 % (653364)Termination reason: Instruction limit
% 0.39/0.33 % (653364)Termination phase: Saturation
% 0.39/0.33 % (653364)Time elapsed: 0.065 s
% 0.39/0.33 % (653364)Peak memory usage: 13 MB
% 0.39/0.33 % (653364)Instructions burned: 133 (million)
% 0.39/0.33 % (653360) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-653354-653360"...
% 0.39/0.33 % (653375)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2393558958:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.39/0.33 % (653376)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=379551413:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.39/0.33 % (653365)Instruction limit reached!
% 0.39/0.33 % (653365)------------------------------
% 0.39/0.33 % (653365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.39/0.33 % (653365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.39/0.33 % (653365)CaDiCaL version: 2.1.3
% 0.39/0.33 % (653365)Termination reason: Instruction limit
% 0.39/0.33 % (653365)Termination phase: Saturation
% 0.39/0.33 % (653365)Time elapsed: 0.087 s
% 0.39/0.33 % (653365)Peak memory usage: 14 MB
% 0.39/0.33 % (653365)Instructions burned: 160 (million)
% 0.39/0.33 % (653360)...printing done.
% 0.39/0.33 % (653360)Refutation found. Thanks to Tanya!
% 0.39/0.33 % SZS status Theorem for theBenchmark
% 0.39/0.33 % SZS output start Proof for theBenchmark
% See solution above
% 0.39/0.34 % (653360)------------------------------
% 0.39/0.34 % (653360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.39/0.34 % (653360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.39/0.34 % (653360)CaDiCaL version: 2.1.3
% 0.39/0.34 % (653360)Termination reason: Refutation
% 0.39/0.34 % (653360)Time elapsed: 0.088 s
% 0.39/0.34 % (653360)Peak memory usage: 14 MB
% 0.39/0.34 % (653360)Instructions burned: 173 (million)
% 0.39/0.34 % (653354)Success in time 0.135 s
% 0.39/0.34 % Vampire exiting
%------------------------------------------------------------------------------