%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:11:26 AM UTC 2026
% Result : Theorem 3.70s 1.16s
% Output : Refutation 4.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 174
% Syntax : Number of formulae : 1105 ( 160 unt; 160 def)
% Number of atoms : 3955 (1818 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 4719 (1869 ~;2161 |; 549 &)
% ( 140 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 162 ( 160 usr; 161 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(f18,conjecture,
( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f19,negated_conjecture,
~ ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f20,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) ) )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) ) )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) ) )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) ) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f21,definition,
( ( op1(e13,e13) = e13
& op1(e13,e13) != e13 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f22,definition,
( ( op1(e13,e13) = e12
& op1(e13,e12) != e13 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( op1(e13,e13) = e11
& op1(e13,e11) != e13 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( op1(e13,e13) = e10
& op1(e13,e10) != e13 )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f25,plain,
( ( ( op1(e10,e10) = e10
& op1(e10,e10) != e10 )
| ( op1(e11,e11) = e10
& op1(e11,e10) != e11 )
| ( op1(e12,e12) = e10
& op1(e12,e10) != e12 )
| sP3 )
& ( ( op1(e10,e10) = e11
& op1(e10,e11) != e10 )
| ( op1(e11,e11) = e11
& op1(e11,e11) != e11 )
| ( op1(e12,e12) = e11
& op1(e12,e11) != e12 )
| sP2 )
& ( ( op1(e10,e10) = e12
& op1(e10,e12) != e10 )
| ( op1(e11,e11) = e12
& op1(e11,e12) != e11 )
| ( op1(e12,e12) = e12
& op1(e12,e12) != e12 )
| sP1 )
& ( ( op1(e10,e10) = e13
& op1(e10,e13) != e10 )
| ( op1(e11,e11) = e13
& op1(e11,e13) != e11 )
| ( op1(e12,e12) = e13
& op1(e12,e13) != e12 )
| sP0 ) ),
inference(definition_folding,[],[f10,f24,f23,f22,f21]) ).
fof(f26,definition,
( ( op2(e23,e23) = e23
& op2(e23,e23) != e23 )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f27,definition,
( ( op2(e23,e23) = e22
& op2(e23,e22) != e23 )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( op2(e23,e23) = e21
& op2(e23,e21) != e23 )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f29,definition,
( ( op2(e23,e23) = e20
& op2(e23,e20) != e23 )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f30,plain,
( ( ( op2(e20,e20) = e20
& op2(e20,e20) != e20 )
| ( op2(e21,e21) = e20
& op2(e21,e20) != e21 )
| ( op2(e22,e22) = e20
& op2(e22,e20) != e22 )
| sP7 )
& ( ( op2(e20,e20) = e21
& op2(e20,e21) != e20 )
| ( op2(e21,e21) = e21
& op2(e21,e21) != e21 )
| ( op2(e22,e22) = e21
& op2(e22,e21) != e22 )
| sP6 )
& ( ( op2(e20,e20) = e22
& op2(e20,e22) != e20 )
| ( op2(e21,e21) = e22
& op2(e21,e22) != e21 )
| ( op2(e22,e22) = e22
& op2(e22,e22) != e22 )
| sP5 )
& ( ( op2(e20,e20) = e23
& op2(e20,e23) != e20 )
| ( op2(e21,e21) = e23
& op2(e21,e23) != e21 )
| ( op2(e22,e22) = e23
& op2(e22,e23) != e22 )
| sP4 ) ),
inference(definition_folding,[],[f11,f29,f28,f27,f26]) ).
fof(f31,definition,
( ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f32,definition,
( ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f33,definition,
( ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f34,definition,
( ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f35,definition,
( ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f36,definition,
( ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f37,definition,
( ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f38,definition,
( ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f39,definition,
( ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f40,definition,
( ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f41,definition,
( ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f42,definition,
( ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f43,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) )
| sP19
| sP18
| sP17 )
& ( 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) )
| sP16
| sP15
| sP14 )
& ( 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) )
| sP13
| sP12
| sP11 )
& ( 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) )
| sP10
| sP9
| sP8 ) ),
inference(definition_folding,[],[f20,f42,f41,f40,f39,f38,f37,f36,f35,f34,f33,f32,f31]) ).
fof(f44,plain,
( ( op1(e13,e13) = e10
& op1(e13,e10) != e13 )
| ~ sP3 ),
inference(nnf_transformation,[],[f24]) ).
fof(f45,plain,
( ( op1(e13,e13) = e11
& op1(e13,e11) != e13 )
| ~ sP2 ),
inference(nnf_transformation,[],[f23]) ).
fof(f47,plain,
( ( op1(e13,e13) = e13
& op1(e13,e13) != e13 )
| ~ sP0 ),
inference(nnf_transformation,[],[f21]) ).
fof(f48,plain,
( ( op2(e23,e23) = e20
& op2(e23,e20) != e23 )
| ~ sP7 ),
inference(nnf_transformation,[],[f29]) ).
fof(f49,plain,
( ( op2(e23,e23) = e21
& op2(e23,e21) != e23 )
| ~ sP6 ),
inference(nnf_transformation,[],[f28]) ).
fof(f50,plain,
( ( op2(e23,e23) = e22
& op2(e23,e22) != e23 )
| ~ sP5 ),
inference(nnf_transformation,[],[f27]) ).
fof(f51,plain,
( ( op2(e23,e23) = e23
& op2(e23,e23) != e23 )
| ~ sP4 ),
inference(nnf_transformation,[],[f26]) ).
fof(f52,plain,
( ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ~ sP19 ),
inference(nnf_transformation,[],[f42]) ).
fof(f53,plain,
( ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ~ sP18 ),
inference(nnf_transformation,[],[f41]) ).
fof(f54,plain,
( ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) )
| ~ sP17 ),
inference(nnf_transformation,[],[f40]) ).
fof(f66,plain,
( e10 = op1(e13,e11)
| e11 = op1(e13,e11)
| e12 = op1(e13,e11)
| e13 = op1(e13,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f70,plain,
( e10 = op1(e12,e11)
| e11 = op1(e12,e11)
| e12 = op1(e12,e11)
| e13 = op1(e12,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f76,plain,
( e10 = op1(e10,e13)
| e11 = op1(e10,e13)
| e12 = op1(e10,e13)
| e13 = op1(e10,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f78,plain,
( e10 = op1(e10,e11)
| e11 = op1(e10,e11)
| e12 = op1(e10,e11)
| e13 = op1(e10,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f80,plain,
( e13 = op1(e10,e13)
| e13 = op1(e11,e13)
| e13 = op1(e12,e13)
| e13 = op1(e13,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f85,plain,
( e11 = op1(e13,e10)
| e11 = op1(e13,e11)
| e11 = op1(e13,e12)
| e11 = op1(e13,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f86,plain,
( e10 = op1(e10,e13)
| e10 = op1(e11,e13)
| e10 = op1(e12,e13)
| e10 = op1(e13,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f90,plain,
( e12 = op1(e10,e12)
| e12 = op1(e11,e12)
| e12 = op1(e12,e12)
| e12 = op1(e13,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f91,plain,
( e12 = op1(e12,e10)
| e12 = op1(e12,e11)
| e12 = op1(e12,e12)
| e12 = op1(e12,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f97,plain,
( e13 = op1(e11,e10)
| e13 = op1(e11,e11)
| e13 = op1(e11,e12)
| e13 = op1(e11,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f99,plain,
( e12 = op1(e11,e10)
| e12 = op1(e11,e11)
| e12 = op1(e11,e12)
| e12 = op1(e11,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f100,plain,
( e11 = op1(e10,e11)
| e11 = op1(e11,e11)
| e11 = op1(e12,e11)
| e11 = op1(e13,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f101,plain,
( e11 = op1(e11,e10)
| e11 = op1(e11,e11)
| e11 = op1(e11,e12)
| e11 = op1(e11,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f102,plain,
( e10 = op1(e10,e11)
| e10 = op1(e11,e11)
| e10 = op1(e12,e11)
| e10 = op1(e13,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f104,plain,
( op1(e10,e10) = e13
| e13 = op1(e11,e10)
| e13 = op1(e12,e10)
| e13 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f105,plain,
( op1(e10,e10) = e13
| e13 = op1(e10,e11)
| e13 = op1(e10,e12)
| e13 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f106,plain,
( op1(e10,e10) = e12
| e12 = op1(e11,e10)
| e12 = op1(e12,e10)
| e12 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f107,plain,
( op1(e10,e10) = e12
| e12 = op1(e10,e11)
| e12 = op1(e10,e12)
| e12 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f110,plain,
( e10 = op1(e10,e10)
| e10 = op1(e11,e10)
| e10 = op1(e12,e10)
| e10 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f118,plain,
( e20 = op2(e22,e21)
| e21 = op2(e22,e21)
| e22 = op2(e22,e21)
| e23 = op2(e22,e21) ),
inference(cnf_transformation,[],[f3]) ).
fof(f123,plain,
( e20 = op2(e21,e20)
| e21 = op2(e21,e20)
| e22 = op2(e21,e20)
| e23 = op2(e21,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f126,plain,
( e20 = op2(e20,e21)
| e21 = op2(e20,e21)
| e22 = op2(e20,e21)
| e23 = op2(e20,e21) ),
inference(cnf_transformation,[],[f3]) ).
fof(f128,plain,
( e23 = op2(e20,e23)
| e23 = op2(e21,e23)
| e23 = op2(e22,e23)
| e23 = op2(e23,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f129,plain,
( e23 = op2(e23,e20)
| e23 = op2(e23,e21)
| e23 = op2(e23,e22)
| e23 = op2(e23,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f134,plain,
( e20 = op2(e20,e23)
| e20 = op2(e21,e23)
| e20 = op2(e22,e23)
| e20 = op2(e23,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f135,plain,
( e20 = op2(e23,e20)
| e20 = op2(e23,e21)
| e20 = op2(e23,e22)
| e20 = op2(e23,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f138,plain,
( e22 = op2(e20,e22)
| e22 = op2(e21,e22)
| e22 = op2(e22,e22)
| e22 = op2(e23,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f143,plain,
( e20 = op2(e22,e20)
| e20 = op2(e22,e21)
| e20 = op2(e22,e22)
| e20 = op2(e22,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f144,plain,
( e23 = op2(e20,e21)
| e23 = op2(e21,e21)
| e23 = op2(e22,e21)
| e23 = op2(e23,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f148,plain,
( e21 = op2(e20,e21)
| e21 = op2(e21,e21)
| e21 = op2(e22,e21)
| e21 = op2(e23,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f149,plain,
( e21 = op2(e21,e20)
| e21 = op2(e21,e21)
| e21 = op2(e21,e22)
| e21 = op2(e21,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f154,plain,
( op2(e20,e20) = e22
| e22 = op2(e21,e20)
| e22 = op2(e22,e20)
| e22 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f155,plain,
( op2(e20,e20) = e22
| e22 = op2(e20,e21)
| e22 = op2(e20,e22)
| e22 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f160,plain,
op1(e13,e12) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f161,plain,
op1(e13,e11) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
op1(e13,e11) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
op1(e13,e10) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f166,plain,
op1(e12,e12) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
op1(e12,e11) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f170,plain,
op1(e12,e10) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f171,plain,
op1(e12,e10) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f177,plain,
op1(e11,e10) != op1(e11,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f179,plain,
op1(e10,e11) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f180,plain,
op1(e10,e11) != op1(e10,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f181,plain,
op1(e10,e10) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f185,plain,
op1(e11,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f187,plain,
op1(e10,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f188,plain,
op1(e10,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f189,plain,
op1(e10,e13) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f192,plain,
op1(e11,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f197,plain,
op1(e11,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f199,plain,
op1(e10,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f207,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f211,plain,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f214,plain,
op2(e22,e22) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f215,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f216,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f221,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f225,plain,
op2(e21,e20) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f227,plain,
op2(e20,e21) != op2(e20,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f228,plain,
op2(e20,e21) != op2(e20,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f231,plain,
op2(e20,e20) != op2(e20,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f235,plain,
op2(e20,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f238,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f246,plain,
op2(e21,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f248,plain,
op2(e20,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f251,plain,
op2(e21,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f256,plain,
e12 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f257,plain,
e11 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f258,plain,
e11 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f259,plain,
e10 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f260,plain,
e10 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f261,plain,
e10 != e11,
inference(cnf_transformation,[],[f7]) ).
fof(f262,plain,
e22 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f263,plain,
e21 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f264,plain,
e21 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f265,plain,
e20 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f266,plain,
e20 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f267,plain,
e20 != e21,
inference(cnf_transformation,[],[f8]) ).
fof(f285,plain,
( e10 = op1(e13,e13)
| ~ sP3 ),
inference(cnf_transformation,[],[f44]) ).
fof(f287,plain,
( e11 = op1(e13,e13)
| ~ sP2 ),
inference(cnf_transformation,[],[f45]) ).
fof(f291,plain,
( e13 = op1(e13,e13)
| ~ sP0 ),
inference(cnf_transformation,[],[f47]) ).
fof(f295,plain,
( e10 != op1(e10,e13)
| e13 = op1(e11,e11)
| e13 = op1(e12,e12)
| sP0 ),
inference(cnf_transformation,[],[f25]) ).
fof(f299,plain,
( op1(e10,e10) = e13
| e13 = op1(e11,e11)
| e13 = op1(e12,e12)
| sP0 ),
inference(cnf_transformation,[],[f25]) ).
fof(f311,plain,
( e10 != op1(e10,e11)
| e11 = op1(e11,e11)
| e11 = op1(e12,e12)
| sP2 ),
inference(cnf_transformation,[],[f25]) ).
fof(f313,plain,
( op1(e10,e10) = e11
| e11 != op1(e11,e11)
| e11 = op1(e12,e12)
| sP2 ),
inference(cnf_transformation,[],[f25]) ).
fof(f315,plain,
( op1(e10,e10) = e11
| e11 = op1(e11,e11)
| e11 = op1(e12,e12)
| sP2 ),
inference(cnf_transformation,[],[f25]) ).
fof(f322,plain,
( e10 = op1(e10,e10)
| e10 = op1(e11,e11)
| e12 != op1(e12,e10)
| sP3 ),
inference(cnf_transformation,[],[f25]) ).
fof(f323,plain,
( e10 = op1(e10,e10)
| e10 = op1(e11,e11)
| e10 = op1(e12,e12)
| sP3 ),
inference(cnf_transformation,[],[f25]) ).
fof(f325,plain,
( e20 = op2(e23,e23)
| ~ sP7 ),
inference(cnf_transformation,[],[f48]) ).
fof(f327,plain,
( e21 = op2(e23,e23)
| ~ sP6 ),
inference(cnf_transformation,[],[f49]) ).
fof(f328,plain,
( e23 != op2(e23,e22)
| ~ sP5 ),
inference(cnf_transformation,[],[f50]) ).
fof(f331,plain,
( e23 = op2(e23,e23)
| ~ sP4 ),
inference(cnf_transformation,[],[f51]) ).
fof(f337,plain,
( op2(e20,e20) = e23
| e21 != op2(e21,e23)
| e23 = op2(e22,e22)
| sP4 ),
inference(cnf_transformation,[],[f30]) ).
fof(f339,plain,
( op2(e20,e20) = e23
| e23 = op2(e21,e21)
| e23 = op2(e22,e22)
| sP4 ),
inference(cnf_transformation,[],[f30]) ).
fof(f346,plain,
( op2(e20,e20) = e22
| e22 = op2(e21,e21)
| e22 != op2(e22,e22)
| sP5 ),
inference(cnf_transformation,[],[f30]) ).
fof(f351,plain,
( e20 != op2(e20,e21)
| e21 = op2(e21,e21)
| e21 = op2(e22,e22)
| sP6 ),
inference(cnf_transformation,[],[f30]) ).
fof(f353,plain,
( op2(e20,e20) = e21
| e21 != op2(e21,e21)
| e21 = op2(e22,e22)
| sP6 ),
inference(cnf_transformation,[],[f30]) ).
fof(f355,plain,
( op2(e20,e20) = e21
| e21 = op2(e21,e21)
| e21 = op2(e22,e22)
| sP6 ),
inference(cnf_transformation,[],[f30]) ).
fof(f361,plain,
( e20 = op2(e20,e20)
| e21 != op2(e21,e20)
| e20 = op2(e22,e22)
| sP7 ),
inference(cnf_transformation,[],[f30]) ).
fof(f362,plain,
( e20 = op2(e20,e20)
| e20 = op2(e21,e21)
| e22 != op2(e22,e20)
| sP7 ),
inference(cnf_transformation,[],[f30]) ).
fof(f363,plain,
( e20 = op2(e20,e20)
| e20 = op2(e21,e21)
| e20 = op2(e22,e22)
| sP7 ),
inference(cnf_transformation,[],[f30]) ).
fof(f364,plain,
e12 = op1(e13,e13),
inference(cnf_transformation,[],[f12]) ).
fof(f365,plain,
e11 = op1(op1(e13,e13),e13),
inference(cnf_transformation,[],[f12]) ).
fof(f366,plain,
e10 = op1(e13,op1(e13,e13)),
inference(cnf_transformation,[],[f12]) ).
fof(f367,plain,
e22 = op2(e23,e23),
inference(cnf_transformation,[],[f13]) ).
fof(f368,plain,
e21 = op2(op2(e23,e23),e23),
inference(cnf_transformation,[],[f13]) ).
fof(f370,plain,
op2(e20,e20) = h1(e12),
inference(cnf_transformation,[],[f14]) ).
fof(f371,plain,
h1(e11) = op2(op2(e20,e20),e20),
inference(cnf_transformation,[],[f14]) ).
fof(f372,plain,
h1(e10) = op2(e20,op2(e20,e20)),
inference(cnf_transformation,[],[f14]) ).
fof(f373,plain,
e20 = h1(e13),
inference(cnf_transformation,[],[f14]) ).
fof(f387,plain,
( e21 != h1(e12)
| ~ sP19 ),
inference(cnf_transformation,[],[f52]) ).
fof(f392,plain,
( e22 != h1(e11)
| ~ sP18 ),
inference(cnf_transformation,[],[f53]) ).
fof(f397,plain,
( e23 != h1(e10)
| ~ sP17 ),
inference(cnf_transformation,[],[f54]) ).
fof(f446,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(e13)
| sP19
| sP18
| sP17 ),
inference(cnf_transformation,[],[f43]) ).
fof(f739,definition,
( spl20_70
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl20_70])],[avatar_definition]) ).
fof(f743,definition,
( spl20_71
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl20_71])],[avatar_definition]) ).
fof(f747,definition,
( spl20_72
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl20_72])],[avatar_definition]) ).
fof(f751,definition,
( spl20_73
<=> e20 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl20_73])],[avatar_definition]) ).
fof(f752,plain,
( e20 = h1(e13)
| ~ spl20_73 ),
inference(avatar_component_clause,[],[f751]) ).
fof(f755,definition,
( spl20_74
<=> h1(op1(e13,e13)) = op2(h1(e13),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl20_74])],[avatar_definition]) ).
fof(f757,plain,
( h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| spl20_74 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f759,definition,
( spl20_75
<=> h1(op1(e13,e12)) = op2(h1(e13),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl20_75])],[avatar_definition]) ).
fof(f761,plain,
( h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| spl20_75 ),
inference(avatar_component_clause,[],[f759]) ).
fof(f763,definition,
( spl20_76
<=> h1(op1(e13,e11)) = op2(h1(e13),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl20_76])],[avatar_definition]) ).
fof(f765,plain,
( h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| spl20_76 ),
inference(avatar_component_clause,[],[f763]) ).
fof(f767,definition,
( spl20_77
<=> h1(op1(e13,e10)) = op2(h1(e13),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl20_77])],[avatar_definition]) ).
fof(f769,plain,
( h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| spl20_77 ),
inference(avatar_component_clause,[],[f767]) ).
fof(f771,definition,
( spl20_78
<=> h1(op1(e12,e13)) = op2(h1(e12),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl20_78])],[avatar_definition]) ).
fof(f773,plain,
( h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| spl20_78 ),
inference(avatar_component_clause,[],[f771]) ).
fof(f775,definition,
( spl20_79
<=> h1(op1(e12,e12)) = op2(h1(e12),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl20_79])],[avatar_definition]) ).
fof(f777,plain,
( h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| spl20_79 ),
inference(avatar_component_clause,[],[f775]) ).
fof(f779,definition,
( spl20_80
<=> h1(op1(e12,e11)) = op2(h1(e12),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl20_80])],[avatar_definition]) ).
fof(f781,plain,
( h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| spl20_80 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f783,definition,
( spl20_81
<=> h1(op1(e12,e10)) = op2(h1(e12),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl20_81])],[avatar_definition]) ).
fof(f785,plain,
( h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| spl20_81 ),
inference(avatar_component_clause,[],[f783]) ).
fof(f787,definition,
( spl20_82
<=> h1(op1(e11,e13)) = op2(h1(e11),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl20_82])],[avatar_definition]) ).
fof(f789,plain,
( h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| spl20_82 ),
inference(avatar_component_clause,[],[f787]) ).
fof(f791,definition,
( spl20_83
<=> h1(op1(e11,e12)) = op2(h1(e11),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl20_83])],[avatar_definition]) ).
fof(f793,plain,
( h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| spl20_83 ),
inference(avatar_component_clause,[],[f791]) ).
fof(f795,definition,
( spl20_84
<=> h1(op1(e11,e11)) = op2(h1(e11),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl20_84])],[avatar_definition]) ).
fof(f797,plain,
( h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| spl20_84 ),
inference(avatar_component_clause,[],[f795]) ).
fof(f799,definition,
( spl20_85
<=> h1(op1(e11,e10)) = op2(h1(e11),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl20_85])],[avatar_definition]) ).
fof(f801,plain,
( h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| spl20_85 ),
inference(avatar_component_clause,[],[f799]) ).
fof(f803,definition,
( spl20_86
<=> h1(op1(e10,e13)) = op2(h1(e10),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl20_86])],[avatar_definition]) ).
fof(f805,plain,
( h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| spl20_86 ),
inference(avatar_component_clause,[],[f803]) ).
fof(f807,definition,
( spl20_87
<=> h1(op1(e10,e12)) = op2(h1(e10),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl20_87])],[avatar_definition]) ).
fof(f809,plain,
( h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| spl20_87 ),
inference(avatar_component_clause,[],[f807]) ).
fof(f811,definition,
( spl20_88
<=> h1(op1(e10,e11)) = op2(h1(e10),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl20_88])],[avatar_definition]) ).
fof(f813,plain,
( h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| spl20_88 ),
inference(avatar_component_clause,[],[f811]) ).
fof(f815,definition,
( spl20_89
<=> h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl20_89])],[avatar_definition]) ).
fof(f817,plain,
( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| spl20_89 ),
inference(avatar_component_clause,[],[f815]) ).
fof(f818,plain,
( spl20_70
| spl20_71
| spl20_72
| ~ spl20_73
| ~ spl20_74
| ~ spl20_75
| ~ spl20_76
| ~ spl20_77
| ~ spl20_78
| ~ spl20_79
| ~ spl20_80
| ~ spl20_81
| ~ spl20_82
| ~ spl20_83
| ~ spl20_84
| ~ spl20_85
| ~ spl20_86
| ~ spl20_87
| ~ spl20_88
| ~ spl20_89 ),
inference(avatar_split_clause,[],[f446,f815,f811,f807,f803,f799,f795,f791,f787,f783,f779,f775,f771,f767,f763,f759,f755,f751,f747,f743,f739]) ).
fof(f1030,definition,
( spl20_132
<=> e23 = h1(e10) ),
introduced(definition,[new_symbols(definition,[spl20_132])],[avatar_definition]) ).
fof(f1031,plain,
( e23 = h1(e10)
| ~ spl20_132 ),
inference(avatar_component_clause,[],[f1030]) ).
fof(f1033,plain,
( ~ spl20_70
| ~ spl20_132 ),
inference(avatar_split_clause,[],[f397,f1030,f739]) ).
fof(f1045,definition,
( spl20_135
<=> e22 = h1(e11) ),
introduced(definition,[new_symbols(definition,[spl20_135])],[avatar_definition]) ).
fof(f1046,plain,
( e22 = h1(e11)
| ~ spl20_135 ),
inference(avatar_component_clause,[],[f1045]) ).
fof(f1048,plain,
( ~ spl20_71
| ~ spl20_135 ),
inference(avatar_split_clause,[],[f392,f1045,f743]) ).
fof(f1060,definition,
( spl20_138
<=> e21 = h1(e12) ),
introduced(definition,[new_symbols(definition,[spl20_138])],[avatar_definition]) ).
fof(f1061,plain,
( e21 = h1(e12)
| ~ spl20_138 ),
inference(avatar_component_clause,[],[f1060]) ).
fof(f1063,plain,
( ~ spl20_72
| ~ spl20_138 ),
inference(avatar_split_clause,[],[f387,f1060,f747]) ).
fof(f1077,plain,
spl20_73,
inference(avatar_split_clause,[],[f373,f751]) ).
fof(f1079,definition,
( spl20_141
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl20_141])],[avatar_definition]) ).
fof(f1087,definition,
( spl20_143
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl20_143])],[avatar_definition]) ).
fof(f1088,plain,
( e21 = op2(e21,e23)
| ~ spl20_143 ),
inference(avatar_component_clause,[],[f1087]) ).
fof(f1091,definition,
( spl20_144
<=> e20 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl20_144])],[avatar_definition]) ).
fof(f1092,plain,
( e20 = op2(e20,e23)
| ~ spl20_144 ),
inference(avatar_component_clause,[],[f1091]) ).
fof(f1096,definition,
( spl20_145
<=> e23 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl20_145])],[avatar_definition]) ).
fof(f1098,plain,
( e23 = op2(e22,e22)
| ~ spl20_145 ),
inference(avatar_component_clause,[],[f1096]) ).
fof(f1101,definition,
( spl20_146
<=> e23 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl20_146])],[avatar_definition]) ).
fof(f1103,plain,
( e23 = op2(e21,e21)
| ~ spl20_146 ),
inference(avatar_component_clause,[],[f1101]) ).
fof(f1107,definition,
( spl20_147
<=> op2(e20,e20) = e23 ),
introduced(definition,[new_symbols(definition,[spl20_147])],[avatar_definition]) ).
fof(f1109,plain,
( op2(e20,e20) = e23
| ~ spl20_147 ),
inference(avatar_component_clause,[],[f1107]) ).
fof(f1111,plain,
( spl20_141
| spl20_145
| ~ spl20_143
| spl20_147 ),
inference(avatar_split_clause,[],[f337,f1107,f1087,f1096,f1079]) ).
fof(f1113,plain,
( spl20_141
| spl20_145
| spl20_146
| spl20_147 ),
inference(avatar_split_clause,[],[f339,f1107,f1101,f1096,f1079]) ).
fof(f1115,definition,
( spl20_148
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl20_148])],[avatar_definition]) ).
fof(f1119,definition,
( spl20_149
<=> e22 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl20_149])],[avatar_definition]) ).
fof(f1123,definition,
( spl20_150
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl20_150])],[avatar_definition]) ).
fof(f1124,plain,
( e21 = op2(e21,e22)
| ~ spl20_150 ),
inference(avatar_component_clause,[],[f1123]) ).
fof(f1133,definition,
( spl20_152
<=> e22 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl20_152])],[avatar_definition]) ).
fof(f1135,plain,
( e22 = op2(e21,e21)
| ~ spl20_152 ),
inference(avatar_component_clause,[],[f1133]) ).
fof(f1139,definition,
( spl20_153
<=> op2(e20,e20) = e22 ),
introduced(definition,[new_symbols(definition,[spl20_153])],[avatar_definition]) ).
fof(f1141,plain,
( op2(e20,e20) = e22
| ~ spl20_153 ),
inference(avatar_component_clause,[],[f1139]) ).
fof(f1144,plain,
( spl20_148
| ~ spl20_149
| spl20_152
| spl20_153 ),
inference(avatar_split_clause,[],[f346,f1139,f1133,f1119,f1115]) ).
fof(f1147,definition,
( spl20_154
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl20_154])],[avatar_definition]) ).
fof(f1151,definition,
( spl20_155
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl20_155])],[avatar_definition]) ).
fof(f1152,plain,
( e22 = op2(e22,e21)
| ~ spl20_155 ),
inference(avatar_component_clause,[],[f1151]) ).
fof(f1155,definition,
( spl20_156
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl20_156])],[avatar_definition]) ).
fof(f1156,plain,
( e21 = op2(e21,e21)
| ~ spl20_156 ),
inference(avatar_component_clause,[],[f1155]) ).
fof(f1159,definition,
( spl20_157
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl20_157])],[avatar_definition]) ).
fof(f1164,definition,
( spl20_158
<=> e21 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl20_158])],[avatar_definition]) ).
fof(f1169,plain,
( spl20_154
| spl20_158
| spl20_156
| ~ spl20_157 ),
inference(avatar_split_clause,[],[f351,f1159,f1155,f1164,f1147]) ).
fof(f1171,definition,
( spl20_159
<=> op2(e20,e20) = e21 ),
introduced(definition,[new_symbols(definition,[spl20_159])],[avatar_definition]) ).
fof(f1173,plain,
( op2(e20,e20) = e21
| ~ spl20_159 ),
inference(avatar_component_clause,[],[f1171]) ).
fof(f1175,plain,
( spl20_154
| spl20_158
| ~ spl20_156
| spl20_159 ),
inference(avatar_split_clause,[],[f353,f1171,f1155,f1164,f1147]) ).
fof(f1177,plain,
( spl20_154
| spl20_158
| spl20_156
| spl20_159 ),
inference(avatar_split_clause,[],[f355,f1171,f1155,f1164,f1147]) ).
fof(f1179,definition,
( spl20_160
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl20_160])],[avatar_definition]) ).
fof(f1183,definition,
( spl20_161
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl20_161])],[avatar_definition]) ).
fof(f1187,definition,
( spl20_162
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl20_162])],[avatar_definition]) ).
fof(f1188,plain,
( e21 = op2(e21,e20)
| ~ spl20_162 ),
inference(avatar_component_clause,[],[f1187]) ).
fof(f1191,definition,
( spl20_163
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl20_163])],[avatar_definition]) ).
fof(f1192,plain,
( e20 = op2(e20,e20)
| ~ spl20_163 ),
inference(avatar_component_clause,[],[f1191]) ).
fof(f1196,definition,
( spl20_164
<=> e20 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl20_164])],[avatar_definition]) ).
fof(f1198,plain,
( e20 = op2(e22,e22)
| ~ spl20_164 ),
inference(avatar_component_clause,[],[f1196]) ).
fof(f1201,definition,
( spl20_165
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl20_165])],[avatar_definition]) ).
fof(f1203,plain,
( e20 = op2(e21,e21)
| ~ spl20_165 ),
inference(avatar_component_clause,[],[f1201]) ).
fof(f1207,plain,
( spl20_160
| spl20_164
| ~ spl20_162
| spl20_163 ),
inference(avatar_split_clause,[],[f361,f1191,f1187,f1196,f1179]) ).
fof(f1208,plain,
( spl20_160
| ~ spl20_161
| spl20_165
| spl20_163 ),
inference(avatar_split_clause,[],[f362,f1191,f1201,f1183,f1179]) ).
fof(f1209,plain,
( spl20_160
| spl20_164
| spl20_165
| spl20_163 ),
inference(avatar_split_clause,[],[f363,f1191,f1201,f1196,f1179]) ).
fof(f1211,definition,
( spl20_166
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl20_166])],[avatar_definition]) ).
fof(f1212,plain,
( e23 = op2(e23,e23)
| ~ spl20_166 ),
inference(avatar_component_clause,[],[f1211]) ).
fof(f1215,plain,
( ~ spl20_141
| spl20_166 ),
inference(avatar_split_clause,[],[f331,f1211,f1079]) ).
fof(f1217,definition,
( spl20_167
<=> e23 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl20_167])],[avatar_definition]) ).
fof(f1218,plain,
( e23 = op2(e23,e22)
| ~ spl20_167 ),
inference(avatar_component_clause,[],[f1217]) ).
fof(f1220,plain,
( ~ spl20_148
| ~ spl20_167 ),
inference(avatar_split_clause,[],[f328,f1217,f1115]) ).
fof(f1222,definition,
( spl20_168
<=> e22 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl20_168])],[avatar_definition]) ).
fof(f1224,plain,
( e22 = op2(e23,e23)
| ~ spl20_168 ),
inference(avatar_component_clause,[],[f1222]) ).
fof(f1227,definition,
( spl20_169
<=> e23 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl20_169])],[avatar_definition]) ).
fof(f1228,plain,
( e23 = op2(e23,e21)
| ~ spl20_169 ),
inference(avatar_component_clause,[],[f1227]) ).
fof(f1232,definition,
( spl20_170
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl20_170])],[avatar_definition]) ).
fof(f1234,plain,
( e21 = op2(e23,e23)
| ~ spl20_170 ),
inference(avatar_component_clause,[],[f1232]) ).
fof(f1235,plain,
( ~ spl20_154
| spl20_170 ),
inference(avatar_split_clause,[],[f327,f1232,f1147]) ).
fof(f1237,definition,
( spl20_171
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl20_171])],[avatar_definition]) ).
fof(f1238,plain,
( e23 = op2(e23,e20)
| ~ spl20_171 ),
inference(avatar_component_clause,[],[f1237]) ).
fof(f1242,definition,
( spl20_172
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl20_172])],[avatar_definition]) ).
fof(f1244,plain,
( e20 = op2(e23,e23)
| ~ spl20_172 ),
inference(avatar_component_clause,[],[f1242]) ).
fof(f1245,plain,
( ~ spl20_160
| spl20_172 ),
inference(avatar_split_clause,[],[f325,f1242,f1179]) ).
fof(f1247,definition,
( spl20_173
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl20_173])],[avatar_definition]) ).
fof(f1251,definition,
( spl20_174
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl20_174])],[avatar_definition]) ).
fof(f1252,plain,
( e12 = op1(e12,e13)
| ~ spl20_174 ),
inference(avatar_component_clause,[],[f1251]) ).
fof(f1255,definition,
( spl20_175
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl20_175])],[avatar_definition]) ).
fof(f1256,plain,
( e11 = op1(e11,e13)
| ~ spl20_175 ),
inference(avatar_component_clause,[],[f1255]) ).
fof(f1259,definition,
( spl20_176
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl20_176])],[avatar_definition]) ).
fof(f1260,plain,
( e10 = op1(e10,e13)
| ~ spl20_176 ),
inference(avatar_component_clause,[],[f1259]) ).
fof(f1264,definition,
( spl20_177
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl20_177])],[avatar_definition]) ).
fof(f1266,plain,
( e13 = op1(e12,e12)
| ~ spl20_177 ),
inference(avatar_component_clause,[],[f1264]) ).
fof(f1269,definition,
( spl20_178
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl20_178])],[avatar_definition]) ).
fof(f1271,plain,
( e13 = op1(e11,e11)
| ~ spl20_178 ),
inference(avatar_component_clause,[],[f1269]) ).
fof(f1273,plain,
( spl20_173
| spl20_177
| spl20_178
| ~ spl20_176 ),
inference(avatar_split_clause,[],[f295,f1259,f1269,f1264,f1247]) ).
fof(f1275,definition,
( spl20_179
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl20_179])],[avatar_definition]) ).
fof(f1277,plain,
( op1(e10,e10) = e13
| ~ spl20_179 ),
inference(avatar_component_clause,[],[f1275]) ).
fof(f1281,plain,
( spl20_173
| spl20_177
| spl20_178
| spl20_179 ),
inference(avatar_split_clause,[],[f299,f1275,f1269,f1264,f1247]) ).
fof(f1287,definition,
( spl20_181
<=> e12 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl20_181])],[avatar_definition]) ).
fof(f1288,plain,
( e12 = op1(e12,e12)
| ~ spl20_181 ),
inference(avatar_component_clause,[],[f1287]) ).
fof(f1291,definition,
( spl20_182
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl20_182])],[avatar_definition]) ).
fof(f1292,plain,
( e11 = op1(e11,e12)
| ~ spl20_182 ),
inference(avatar_component_clause,[],[f1291]) ).
fof(f1301,definition,
( spl20_184
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl20_184])],[avatar_definition]) ).
fof(f1303,plain,
( e12 = op1(e11,e11)
| ~ spl20_184 ),
inference(avatar_component_clause,[],[f1301]) ).
fof(f1307,definition,
( spl20_185
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[spl20_185])],[avatar_definition]) ).
fof(f1309,plain,
( op1(e10,e10) = e12
| ~ spl20_185 ),
inference(avatar_component_clause,[],[f1307]) ).
fof(f1315,definition,
( spl20_186
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl20_186])],[avatar_definition]) ).
fof(f1319,definition,
( spl20_187
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl20_187])],[avatar_definition]) ).
fof(f1320,plain,
( e12 = op1(e12,e11)
| ~ spl20_187 ),
inference(avatar_component_clause,[],[f1319]) ).
fof(f1323,definition,
( spl20_188
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl20_188])],[avatar_definition]) ).
fof(f1324,plain,
( e11 = op1(e11,e11)
| ~ spl20_188 ),
inference(avatar_component_clause,[],[f1323]) ).
fof(f1327,definition,
( spl20_189
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl20_189])],[avatar_definition]) ).
fof(f1332,definition,
( spl20_190
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl20_190])],[avatar_definition]) ).
fof(f1337,plain,
( spl20_186
| spl20_190
| spl20_188
| ~ spl20_189 ),
inference(avatar_split_clause,[],[f311,f1327,f1323,f1332,f1315]) ).
fof(f1339,definition,
( spl20_191
<=> op1(e10,e10) = e11 ),
introduced(definition,[new_symbols(definition,[spl20_191])],[avatar_definition]) ).
fof(f1341,plain,
( op1(e10,e10) = e11
| ~ spl20_191 ),
inference(avatar_component_clause,[],[f1339]) ).
fof(f1343,plain,
( spl20_186
| spl20_190
| ~ spl20_188
| spl20_191 ),
inference(avatar_split_clause,[],[f313,f1339,f1323,f1332,f1315]) ).
fof(f1345,plain,
( spl20_186
| spl20_190
| spl20_188
| spl20_191 ),
inference(avatar_split_clause,[],[f315,f1339,f1323,f1332,f1315]) ).
fof(f1347,definition,
( spl20_192
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl20_192])],[avatar_definition]) ).
fof(f1351,definition,
( spl20_193
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl20_193])],[avatar_definition]) ).
fof(f1352,plain,
( e12 = op1(e12,e10)
| ~ spl20_193 ),
inference(avatar_component_clause,[],[f1351]) ).
fof(f1355,definition,
( spl20_194
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl20_194])],[avatar_definition]) ).
fof(f1359,definition,
( spl20_195
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl20_195])],[avatar_definition]) ).
fof(f1360,plain,
( e10 = op1(e10,e10)
| ~ spl20_195 ),
inference(avatar_component_clause,[],[f1359]) ).
fof(f1364,definition,
( spl20_196
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl20_196])],[avatar_definition]) ).
fof(f1366,plain,
( e10 = op1(e12,e12)
| ~ spl20_196 ),
inference(avatar_component_clause,[],[f1364]) ).
fof(f1369,definition,
( spl20_197
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl20_197])],[avatar_definition]) ).
fof(f1371,plain,
( e10 = op1(e11,e11)
| ~ spl20_197 ),
inference(avatar_component_clause,[],[f1369]) ).
fof(f1376,plain,
( spl20_192
| ~ spl20_193
| spl20_197
| spl20_195 ),
inference(avatar_split_clause,[],[f322,f1359,f1369,f1351,f1347]) ).
fof(f1377,plain,
( spl20_192
| spl20_196
| spl20_197
| spl20_195 ),
inference(avatar_split_clause,[],[f323,f1359,f1369,f1364,f1347]) ).
fof(f1379,definition,
( spl20_198
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl20_198])],[avatar_definition]) ).
fof(f1380,plain,
( e13 = op1(e13,e13)
| ~ spl20_198 ),
inference(avatar_component_clause,[],[f1379]) ).
fof(f1383,plain,
( ~ spl20_173
| spl20_198 ),
inference(avatar_split_clause,[],[f291,f1379,f1247]) ).
fof(f1390,definition,
( spl20_200
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl20_200])],[avatar_definition]) ).
fof(f1392,plain,
( e12 = op1(e13,e13)
| ~ spl20_200 ),
inference(avatar_component_clause,[],[f1390]) ).
fof(f1395,definition,
( spl20_201
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl20_201])],[avatar_definition]) ).
fof(f1396,plain,
( e13 = op1(e13,e11)
| ~ spl20_201 ),
inference(avatar_component_clause,[],[f1395]) ).
fof(f1400,definition,
( spl20_202
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl20_202])],[avatar_definition]) ).
fof(f1402,plain,
( e11 = op1(e13,e13)
| ~ spl20_202 ),
inference(avatar_component_clause,[],[f1400]) ).
fof(f1403,plain,
( ~ spl20_186
| spl20_202 ),
inference(avatar_split_clause,[],[f287,f1400,f1315]) ).
fof(f1405,definition,
( spl20_203
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl20_203])],[avatar_definition]) ).
fof(f1406,plain,
( e13 = op1(e13,e10)
| ~ spl20_203 ),
inference(avatar_component_clause,[],[f1405]) ).
fof(f1410,definition,
( spl20_204
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl20_204])],[avatar_definition]) ).
fof(f1413,plain,
( ~ spl20_192
| spl20_204 ),
inference(avatar_split_clause,[],[f285,f1410,f1347]) ).
fof(f1415,definition,
( spl20_205
<=> e23 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl20_205])],[avatar_definition]) ).
fof(f1417,plain,
( e23 = op2(e22,e23)
| ~ spl20_205 ),
inference(avatar_component_clause,[],[f1415]) ).
fof(f1419,definition,
( spl20_206
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl20_206])],[avatar_definition]) ).
fof(f1421,plain,
( e23 = op2(e21,e23)
| ~ spl20_206 ),
inference(avatar_component_clause,[],[f1419]) ).
fof(f1423,definition,
( spl20_207
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl20_207])],[avatar_definition]) ).
fof(f1425,plain,
( e23 = op2(e20,e23)
| ~ spl20_207 ),
inference(avatar_component_clause,[],[f1423]) ).
fof(f1426,plain,
( spl20_166
| spl20_205
| spl20_206
| spl20_207 ),
inference(avatar_split_clause,[],[f128,f1423,f1419,f1415,f1211]) ).
fof(f1427,plain,
( spl20_166
| spl20_167
| spl20_169
| spl20_171 ),
inference(avatar_split_clause,[],[f129,f1237,f1227,f1217,f1211]) ).
fof(f1433,definition,
( spl20_209
<=> e22 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl20_209])],[avatar_definition]) ).
fof(f1438,definition,
( spl20_210
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl20_210])],[avatar_definition]) ).
fof(f1440,plain,
( e22 = op2(e23,e22)
| ~ spl20_210 ),
inference(avatar_component_clause,[],[f1438]) ).
fof(f1446,definition,
( spl20_212
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl20_212])],[avatar_definition]) ).
fof(f1451,definition,
( spl20_213
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl20_213])],[avatar_definition]) ).
fof(f1453,plain,
( e21 = op2(e22,e23)
| ~ spl20_213 ),
inference(avatar_component_clause,[],[f1451]) ).
fof(f1464,definition,
( spl20_216
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl20_216])],[avatar_definition]) ).
fof(f1466,plain,
( e21 = op2(e23,e21)
| ~ spl20_216 ),
inference(avatar_component_clause,[],[f1464]) ).
fof(f1473,definition,
( spl20_218
<=> e20 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl20_218])],[avatar_definition]) ).
fof(f1475,plain,
( e20 = op2(e22,e23)
| ~ spl20_218 ),
inference(avatar_component_clause,[],[f1473]) ).
fof(f1477,definition,
( spl20_219
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl20_219])],[avatar_definition]) ).
fof(f1480,plain,
( spl20_172
| spl20_218
| spl20_219
| spl20_144 ),
inference(avatar_split_clause,[],[f134,f1091,f1477,f1473,f1242]) ).
fof(f1482,definition,
( spl20_220
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl20_220])],[avatar_definition]) ).
fof(f1484,plain,
( e20 = op2(e23,e22)
| ~ spl20_220 ),
inference(avatar_component_clause,[],[f1482]) ).
fof(f1486,definition,
( spl20_221
<=> e20 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl20_221])],[avatar_definition]) ).
fof(f1488,plain,
( e20 = op2(e23,e21)
| ~ spl20_221 ),
inference(avatar_component_clause,[],[f1486]) ).
fof(f1490,definition,
( spl20_222
<=> e20 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl20_222])],[avatar_definition]) ).
fof(f1492,plain,
( e20 = op2(e23,e20)
| ~ spl20_222 ),
inference(avatar_component_clause,[],[f1490]) ).
fof(f1493,plain,
( spl20_172
| spl20_220
| spl20_221
| spl20_222 ),
inference(avatar_split_clause,[],[f135,f1490,f1486,f1482,f1242]) ).
fof(f1504,definition,
( spl20_225
<=> e23 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl20_225])],[avatar_definition]) ).
fof(f1513,definition,
( spl20_227
<=> e22 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl20_227])],[avatar_definition]) ).
fof(f1515,plain,
( e22 = op2(e21,e22)
| ~ spl20_227 ),
inference(avatar_component_clause,[],[f1513]) ).
fof(f1517,definition,
( spl20_228
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl20_228])],[avatar_definition]) ).
fof(f1519,plain,
( e22 = op2(e20,e22)
| ~ spl20_228 ),
inference(avatar_component_clause,[],[f1517]) ).
fof(f1520,plain,
( spl20_210
| spl20_149
| spl20_227
| spl20_228 ),
inference(avatar_split_clause,[],[f138,f1517,f1513,f1119,f1438]) ).
fof(f1528,definition,
( spl20_230
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl20_230])],[avatar_definition]) ).
fof(f1542,definition,
( spl20_233
<=> e20 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl20_233])],[avatar_definition]) ).
fof(f1546,definition,
( spl20_234
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl20_234])],[avatar_definition]) ).
fof(f1548,plain,
( e20 = op2(e22,e20)
| ~ spl20_234 ),
inference(avatar_component_clause,[],[f1546]) ).
fof(f1549,plain,
( spl20_218
| spl20_164
| spl20_233
| spl20_234 ),
inference(avatar_split_clause,[],[f143,f1546,f1542,f1196,f1473]) ).
fof(f1551,definition,
( spl20_235
<=> e23 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl20_235])],[avatar_definition]) ).
fof(f1553,plain,
( e23 = op2(e20,e21)
| ~ spl20_235 ),
inference(avatar_component_clause,[],[f1551]) ).
fof(f1554,plain,
( spl20_169
| spl20_225
| spl20_146
| spl20_235 ),
inference(avatar_split_clause,[],[f144,f1551,f1101,f1504,f1227]) ).
fof(f1556,definition,
( spl20_236
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl20_236])],[avatar_definition]) ).
fof(f1558,plain,
( e23 = op2(e21,e20)
| ~ spl20_236 ),
inference(avatar_component_clause,[],[f1556]) ).
fof(f1561,definition,
( spl20_237
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl20_237])],[avatar_definition]) ).
fof(f1566,definition,
( spl20_238
<=> e22 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl20_238])],[avatar_definition]) ).
fof(f1568,plain,
( e22 = op2(e21,e20)
| ~ spl20_238 ),
inference(avatar_component_clause,[],[f1566]) ).
fof(f1571,definition,
( spl20_239
<=> e21 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl20_239])],[avatar_definition]) ).
fof(f1574,plain,
( spl20_216
| spl20_230
| spl20_156
| spl20_239 ),
inference(avatar_split_clause,[],[f148,f1571,f1155,f1528,f1464]) ).
fof(f1575,plain,
( spl20_143
| spl20_150
| spl20_156
| spl20_162 ),
inference(avatar_split_clause,[],[f149,f1187,f1155,f1123,f1087]) ).
fof(f1578,definition,
( spl20_240
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl20_240])],[avatar_definition]) ).
fof(f1584,plain,
( spl20_212
| spl20_161
| spl20_238
| spl20_153 ),
inference(avatar_split_clause,[],[f154,f1139,f1566,f1183,f1446]) ).
fof(f1585,plain,
( spl20_209
| spl20_228
| spl20_237
| spl20_153 ),
inference(avatar_split_clause,[],[f155,f1139,f1561,f1517,f1433]) ).
fof(f1596,plain,
( spl20_225
| spl20_155
| spl20_230
| spl20_233 ),
inference(avatar_split_clause,[],[f118,f1542,f1528,f1151,f1504]) ).
fof(f1601,plain,
( spl20_236
| spl20_238
| spl20_162
| spl20_240 ),
inference(avatar_split_clause,[],[f123,f1578,f1187,f1566,f1556]) ).
fof(f1604,plain,
( spl20_235
| spl20_237
| spl20_239
| spl20_157 ),
inference(avatar_split_clause,[],[f126,f1159,f1571,f1561,f1551]) ).
fof(f1607,definition,
( spl20_241
<=> e13 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl20_241])],[avatar_definition]) ).
fof(f1609,plain,
( e13 = op1(e12,e13)
| ~ spl20_241 ),
inference(avatar_component_clause,[],[f1607]) ).
fof(f1611,definition,
( spl20_242
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl20_242])],[avatar_definition]) ).
fof(f1613,plain,
( e13 = op1(e11,e13)
| ~ spl20_242 ),
inference(avatar_component_clause,[],[f1611]) ).
fof(f1615,definition,
( spl20_243
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl20_243])],[avatar_definition]) ).
fof(f1617,plain,
( e13 = op1(e10,e13)
| ~ spl20_243 ),
inference(avatar_component_clause,[],[f1615]) ).
fof(f1618,plain,
( spl20_198
| spl20_241
| spl20_242
| spl20_243 ),
inference(avatar_split_clause,[],[f80,f1615,f1611,f1607,f1379]) ).
fof(f1621,definition,
( spl20_244
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl20_244])],[avatar_definition]) ).
fof(f1625,definition,
( spl20_245
<=> e12 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl20_245])],[avatar_definition]) ).
fof(f1630,definition,
( spl20_246
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl20_246])],[avatar_definition]) ).
fof(f1632,plain,
( e12 = op1(e13,e12)
| ~ spl20_246 ),
inference(avatar_component_clause,[],[f1630]) ).
fof(f1634,definition,
( spl20_247
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl20_247])],[avatar_definition]) ).
fof(f1638,definition,
( spl20_248
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl20_248])],[avatar_definition]) ).
fof(f1640,plain,
( e12 = op1(e13,e10)
| ~ spl20_248 ),
inference(avatar_component_clause,[],[f1638]) ).
fof(f1643,definition,
( spl20_249
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl20_249])],[avatar_definition]) ).
fof(f1645,plain,
( e11 = op1(e12,e13)
| ~ spl20_249 ),
inference(avatar_component_clause,[],[f1643]) ).
fof(f1647,definition,
( spl20_250
<=> e11 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl20_250])],[avatar_definition]) ).
fof(f1652,definition,
( spl20_251
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl20_251])],[avatar_definition]) ).
fof(f1654,plain,
( e11 = op1(e13,e12)
| ~ spl20_251 ),
inference(avatar_component_clause,[],[f1652]) ).
fof(f1656,definition,
( spl20_252
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl20_252])],[avatar_definition]) ).
fof(f1658,plain,
( e11 = op1(e13,e11)
| ~ spl20_252 ),
inference(avatar_component_clause,[],[f1656]) ).
fof(f1660,definition,
( spl20_253
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl20_253])],[avatar_definition]) ).
fof(f1662,plain,
( e11 = op1(e13,e10)
| ~ spl20_253 ),
inference(avatar_component_clause,[],[f1660]) ).
fof(f1663,plain,
( spl20_202
| spl20_251
| spl20_252
| spl20_253 ),
inference(avatar_split_clause,[],[f85,f1660,f1656,f1652,f1400]) ).
fof(f1665,definition,
( spl20_254
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl20_254])],[avatar_definition]) ).
fof(f1667,plain,
( e10 = op1(e12,e13)
| ~ spl20_254 ),
inference(avatar_component_clause,[],[f1665]) ).
fof(f1669,definition,
( spl20_255
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl20_255])],[avatar_definition]) ).
fof(f1671,plain,
( e10 = op1(e11,e13)
| ~ spl20_255 ),
inference(avatar_component_clause,[],[f1669]) ).
fof(f1672,plain,
( spl20_204
| spl20_254
| spl20_255
| spl20_176 ),
inference(avatar_split_clause,[],[f86,f1259,f1669,f1665,f1410]) ).
fof(f1674,definition,
( spl20_256
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl20_256])],[avatar_definition]) ).
fof(f1676,plain,
( e10 = op1(e13,e12)
| ~ spl20_256 ),
inference(avatar_component_clause,[],[f1674]) ).
fof(f1678,definition,
( spl20_257
<=> e10 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl20_257])],[avatar_definition]) ).
fof(f1682,definition,
( spl20_258
<=> e10 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl20_258])],[avatar_definition]) ).
fof(f1687,definition,
( spl20_259
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl20_259])],[avatar_definition]) ).
fof(f1691,definition,
( spl20_260
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl20_260])],[avatar_definition]) ).
fof(f1693,plain,
( e13 = op1(e10,e12)
| ~ spl20_260 ),
inference(avatar_component_clause,[],[f1691]) ).
fof(f1696,definition,
( spl20_261
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl20_261])],[avatar_definition]) ).
fof(f1700,definition,
( spl20_262
<=> e13 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl20_262])],[avatar_definition]) ).
fof(f1705,definition,
( spl20_263
<=> e12 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl20_263])],[avatar_definition]) ).
fof(f1707,plain,
( e12 = op1(e11,e12)
| ~ spl20_263 ),
inference(avatar_component_clause,[],[f1705]) ).
fof(f1709,definition,
( spl20_264
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl20_264])],[avatar_definition]) ).
fof(f1711,plain,
( e12 = op1(e10,e12)
| ~ spl20_264 ),
inference(avatar_component_clause,[],[f1709]) ).
fof(f1712,plain,
( spl20_246
| spl20_181
| spl20_263
| spl20_264 ),
inference(avatar_split_clause,[],[f90,f1709,f1705,f1287,f1630]) ).
fof(f1713,plain,
( spl20_174
| spl20_181
| spl20_187
| spl20_193 ),
inference(avatar_split_clause,[],[f91,f1351,f1319,f1287,f1251]) ).
fof(f1720,definition,
( spl20_266
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl20_266])],[avatar_definition]) ).
fof(f1722,plain,
( e11 = op1(e12,e11)
| ~ spl20_266 ),
inference(avatar_component_clause,[],[f1720]) ).
fof(f1734,definition,
( spl20_269
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl20_269])],[avatar_definition]) ).
fof(f1736,plain,
( e10 = op1(e12,e11)
| ~ spl20_269 ),
inference(avatar_component_clause,[],[f1734]) ).
fof(f1738,definition,
( spl20_270
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl20_270])],[avatar_definition]) ).
fof(f1740,plain,
( e10 = op1(e12,e10)
| ~ spl20_270 ),
inference(avatar_component_clause,[],[f1738]) ).
fof(f1743,definition,
( spl20_271
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl20_271])],[avatar_definition]) ).
fof(f1745,plain,
( e13 = op1(e10,e11)
| ~ spl20_271 ),
inference(avatar_component_clause,[],[f1743]) ).
fof(f1748,definition,
( spl20_272
<=> e13 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl20_272])],[avatar_definition]) ).
fof(f1750,plain,
( e13 = op1(e11,e10)
| ~ spl20_272 ),
inference(avatar_component_clause,[],[f1748]) ).
fof(f1751,plain,
( spl20_242
| spl20_259
| spl20_178
| spl20_272 ),
inference(avatar_split_clause,[],[f97,f1748,f1269,f1687,f1611]) ).
fof(f1753,definition,
( spl20_273
<=> e12 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl20_273])],[avatar_definition]) ).
fof(f1755,plain,
( e12 = op1(e10,e11)
| ~ spl20_273 ),
inference(avatar_component_clause,[],[f1753]) ).
fof(f1758,definition,
( spl20_274
<=> e12 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl20_274])],[avatar_definition]) ).
fof(f1760,plain,
( e12 = op1(e11,e10)
| ~ spl20_274 ),
inference(avatar_component_clause,[],[f1758]) ).
fof(f1761,plain,
( spl20_244
| spl20_263
| spl20_184
| spl20_274 ),
inference(avatar_split_clause,[],[f99,f1758,f1301,f1705,f1621]) ).
fof(f1763,definition,
( spl20_275
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl20_275])],[avatar_definition]) ).
fof(f1765,plain,
( e11 = op1(e10,e11)
| ~ spl20_275 ),
inference(avatar_component_clause,[],[f1763]) ).
fof(f1766,plain,
( spl20_252
| spl20_266
| spl20_188
| spl20_275 ),
inference(avatar_split_clause,[],[f100,f1763,f1323,f1720,f1656]) ).
fof(f1767,plain,
( spl20_175
| spl20_182
| spl20_188
| spl20_194 ),
inference(avatar_split_clause,[],[f101,f1355,f1323,f1291,f1255]) ).
fof(f1768,plain,
( spl20_257
| spl20_269
| spl20_197
| spl20_189 ),
inference(avatar_split_clause,[],[f102,f1327,f1369,f1734,f1678]) ).
fof(f1770,definition,
( spl20_276
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl20_276])],[avatar_definition]) ).
fof(f1772,plain,
( e10 = op1(e11,e10)
| ~ spl20_276 ),
inference(avatar_component_clause,[],[f1770]) ).
fof(f1774,plain,
( spl20_203
| spl20_262
| spl20_272
| spl20_179 ),
inference(avatar_split_clause,[],[f104,f1275,f1748,f1700,f1405]) ).
fof(f1775,plain,
( spl20_243
| spl20_260
| spl20_271
| spl20_179 ),
inference(avatar_split_clause,[],[f105,f1275,f1743,f1691,f1615]) ).
fof(f1776,plain,
( spl20_248
| spl20_193
| spl20_274
| spl20_185 ),
inference(avatar_split_clause,[],[f106,f1307,f1758,f1351,f1638]) ).
fof(f1777,plain,
( spl20_245
| spl20_264
| spl20_273
| spl20_185 ),
inference(avatar_split_clause,[],[f107,f1307,f1753,f1709,f1625]) ).
fof(f1780,plain,
( spl20_258
| spl20_270
| spl20_276
| spl20_195 ),
inference(avatar_split_clause,[],[f110,f1359,f1770,f1738,f1682]) ).
fof(f1784,plain,
( spl20_201
| spl20_247
| spl20_252
| spl20_257 ),
inference(avatar_split_clause,[],[f66,f1678,f1656,f1634,f1395]) ).
fof(f1788,plain,
( spl20_261
| spl20_187
| spl20_266
| spl20_269 ),
inference(avatar_split_clause,[],[f70,f1734,f1720,f1319,f1696]) ).
fof(f1794,plain,
( spl20_243
| spl20_245
| spl20_250
| spl20_176 ),
inference(avatar_split_clause,[],[f76,f1259,f1647,f1625,f1615]) ).
fof(f1796,plain,
( spl20_271
| spl20_273
| spl20_275
| spl20_189 ),
inference(avatar_split_clause,[],[f78,f1327,f1763,f1753,f1743]) ).
fof(f1798,plain,
( op2(e20,e20) != h1(op1(e13,e13))
| ~ spl20_73
| spl20_74 ),
inference(forward_demodulation,[],[f757,f752]) ).
fof(f1800,plain,
spl20_200,
inference(avatar_split_clause,[],[f364,f1390]) ).
fof(f1801,plain,
spl20_168,
inference(avatar_split_clause,[],[f367,f1222]) ).
fof(f1803,plain,
( e21 = e23
| ~ spl20_146
| ~ spl20_156 ),
inference(superposition,[],[f1156,f1103]) ).
fof(f1807,plain,
( $false
| ~ spl20_146
| ~ spl20_156 ),
inference(forward_subsumption_resolution,[],[f1803,f263]) ).
fof(f1808,plain,
( ~ spl20_146
| ~ spl20_156 ),
inference(avatar_contradiction_clause,[],[f1807]) ).
fof(f1810,plain,
( e21 = e23
| ~ spl20_147
| ~ spl20_159 ),
inference(superposition,[],[f1173,f1109]) ).
fof(f1814,plain,
( $false
| ~ spl20_147
| ~ spl20_159 ),
inference(forward_subsumption_resolution,[],[f1810,f263]) ).
fof(f1815,plain,
( ~ spl20_147
| ~ spl20_159 ),
inference(avatar_contradiction_clause,[],[f1814]) ).
fof(f1824,plain,
( e20 = e23
| ~ spl20_145
| ~ spl20_164 ),
inference(superposition,[],[f1198,f1098]) ).
fof(f1828,plain,
( $false
| ~ spl20_145
| ~ spl20_164 ),
inference(forward_subsumption_resolution,[],[f1824,f265]) ).
fof(f1829,plain,
( ~ spl20_145
| ~ spl20_164 ),
inference(avatar_contradiction_clause,[],[f1828]) ).
fof(f1831,plain,
( e20 = e23
| ~ spl20_146
| ~ spl20_165 ),
inference(superposition,[],[f1203,f1103]) ).
fof(f1835,plain,
( $false
| ~ spl20_146
| ~ spl20_165 ),
inference(forward_subsumption_resolution,[],[f1831,f265]) ).
fof(f1836,plain,
( ~ spl20_146
| ~ spl20_165 ),
inference(avatar_contradiction_clause,[],[f1835]) ).
fof(f1849,plain,
( e11 = e13
| ~ spl20_179
| ~ spl20_191 ),
inference(superposition,[],[f1341,f1277]) ).
fof(f1853,plain,
( $false
| ~ spl20_179
| ~ spl20_191 ),
inference(forward_subsumption_resolution,[],[f1849,f257]) ).
fof(f1854,plain,
( ~ spl20_179
| ~ spl20_191 ),
inference(avatar_contradiction_clause,[],[f1853]) ).
fof(f1856,plain,
( e10 = e11
| ~ spl20_191
| ~ spl20_195 ),
inference(superposition,[],[f1360,f1341]) ).
fof(f1860,plain,
( $false
| ~ spl20_191
| ~ spl20_195 ),
inference(forward_subsumption_resolution,[],[f1856,f261]) ).
fof(f1861,plain,
( ~ spl20_191
| ~ spl20_195 ),
inference(avatar_contradiction_clause,[],[f1860]) ).
fof(f1870,plain,
( e10 = e13
| ~ spl20_177
| ~ spl20_196 ),
inference(superposition,[],[f1366,f1266]) ).
fof(f1874,plain,
( $false
| ~ spl20_177
| ~ spl20_196 ),
inference(forward_subsumption_resolution,[],[f1870,f259]) ).
fof(f1875,plain,
( ~ spl20_177
| ~ spl20_196 ),
inference(avatar_contradiction_clause,[],[f1874]) ).
fof(f1877,plain,
( e10 = e11
| ~ spl20_188
| ~ spl20_197 ),
inference(superposition,[],[f1371,f1324]) ).
fof(f1881,plain,
( $false
| ~ spl20_188
| ~ spl20_197 ),
inference(forward_subsumption_resolution,[],[f1877,f261]) ).
fof(f1882,plain,
( ~ spl20_188
| ~ spl20_197 ),
inference(avatar_contradiction_clause,[],[f1881]) ).
fof(f1916,plain,
( e21 = e23
| ~ spl20_205
| ~ spl20_213 ),
inference(forward_demodulation,[],[f1417,f1453]) ).
fof(f1918,plain,
( $false
| ~ spl20_205
| ~ spl20_213 ),
inference(forward_subsumption_resolution,[],[f1916,f263]) ).
fof(f1919,plain,
( ~ spl20_205
| ~ spl20_213 ),
inference(avatar_contradiction_clause,[],[f1918]) ).
fof(f1959,plain,
( e22 = e23
| ~ spl20_146
| ~ spl20_152 ),
inference(superposition,[],[f1135,f1103]) ).
fof(f1963,plain,
( $false
| ~ spl20_146
| ~ spl20_152 ),
inference(forward_subsumption_resolution,[],[f1959,f262]) ).
fof(f1964,plain,
( ~ spl20_146
| ~ spl20_152 ),
inference(avatar_contradiction_clause,[],[f1963]) ).
fof(f2004,plain,
( e20 = e21
| ~ spl20_213
| ~ spl20_218 ),
inference(forward_demodulation,[],[f1453,f1475]) ).
fof(f2006,plain,
( $false
| ~ spl20_213
| ~ spl20_218 ),
inference(forward_subsumption_resolution,[],[f2004,f267]) ).
fof(f2007,plain,
( ~ spl20_213
| ~ spl20_218 ),
inference(avatar_contradiction_clause,[],[f2006]) ).
fof(f2049,plain,
( e21 = e23
| ~ spl20_169
| ~ spl20_216 ),
inference(forward_demodulation,[],[f1228,f1466]) ).
fof(f2053,plain,
( $false
| ~ spl20_169
| ~ spl20_216 ),
inference(forward_subsumption_resolution,[],[f2049,f263]) ).
fof(f2054,plain,
( ~ spl20_169
| ~ spl20_216 ),
inference(avatar_contradiction_clause,[],[f2053]) ).
fof(f2106,plain,
( e20 = e21
| ~ spl20_216
| ~ spl20_221 ),
inference(forward_demodulation,[],[f1466,f1488]) ).
fof(f2109,plain,
( $false
| ~ spl20_216
| ~ spl20_221 ),
inference(forward_subsumption_resolution,[],[f2106,f267]) ).
fof(f2110,plain,
( ~ spl20_216
| ~ spl20_221 ),
inference(avatar_contradiction_clause,[],[f2109]) ).
fof(f2131,plain,
( e21 = e22
| ~ spl20_162
| ~ spl20_238 ),
inference(forward_demodulation,[],[f1568,f1188]) ).
fof(f2133,plain,
( $false
| ~ spl20_162
| ~ spl20_238 ),
inference(forward_subsumption_resolution,[],[f2131,f264]) ).
fof(f2134,plain,
( ~ spl20_162
| ~ spl20_238 ),
inference(avatar_contradiction_clause,[],[f2133]) ).
fof(f2191,plain,
( e10 = e12
| ~ spl20_193
| ~ spl20_270 ),
inference(superposition,[],[f1352,f1740]) ).
fof(f2192,plain,
( $false
| ~ spl20_193
| ~ spl20_270 ),
inference(forward_subsumption_resolution,[],[f2191,f260]) ).
fof(f2193,plain,
( ~ spl20_193
| ~ spl20_270 ),
inference(avatar_contradiction_clause,[],[f2192]) ).
fof(f2205,plain,
( e10 = e11
| ~ spl20_249
| ~ spl20_254 ),
inference(superposition,[],[f1667,f1645]) ).
fof(f2211,plain,
( $false
| ~ spl20_249
| ~ spl20_254 ),
inference(forward_subsumption_resolution,[],[f2205,f261]) ).
fof(f2212,plain,
( ~ spl20_249
| ~ spl20_254 ),
inference(avatar_contradiction_clause,[],[f2211]) ).
fof(f2214,plain,
( e10 = e13
| ~ spl20_178
| ~ spl20_197 ),
inference(forward_demodulation,[],[f1271,f1371]) ).
fof(f2218,plain,
( $false
| ~ spl20_178
| ~ spl20_197 ),
inference(forward_subsumption_resolution,[],[f2214,f259]) ).
fof(f2219,plain,
( ~ spl20_178
| ~ spl20_197 ),
inference(avatar_contradiction_clause,[],[f2218]) ).
fof(f2226,plain,
( e12 = e13
| ~ spl20_177
| ~ spl20_181 ),
inference(superposition,[],[f1288,f1266]) ).
fof(f2230,plain,
( $false
| ~ spl20_177
| ~ spl20_181 ),
inference(forward_subsumption_resolution,[],[f2226,f256]) ).
fof(f2231,plain,
( ~ spl20_177
| ~ spl20_181 ),
inference(avatar_contradiction_clause,[],[f2230]) ).
fof(f2233,plain,
( e11 = e13
| ~ spl20_241
| ~ spl20_249 ),
inference(forward_demodulation,[],[f1609,f1645]) ).
fof(f2235,plain,
( $false
| ~ spl20_241
| ~ spl20_249 ),
inference(forward_subsumption_resolution,[],[f2233,f257]) ).
fof(f2236,plain,
( ~ spl20_241
| ~ spl20_249 ),
inference(avatar_contradiction_clause,[],[f2235]) ).
fof(f2282,plain,
( e11 = e12
| ~ spl20_185
| ~ spl20_191 ),
inference(superposition,[],[f1341,f1309]) ).
fof(f2287,plain,
( $false
| ~ spl20_185
| ~ spl20_191 ),
inference(forward_subsumption_resolution,[],[f2282,f258]) ).
fof(f2288,plain,
( ~ spl20_185
| ~ spl20_191 ),
inference(avatar_contradiction_clause,[],[f2287]) ).
fof(f2308,plain,
( e10 = e13
| ~ spl20_272
| ~ spl20_276 ),
inference(superposition,[],[f1772,f1750]) ).
fof(f2313,plain,
( $false
| ~ spl20_272
| ~ spl20_276 ),
inference(forward_subsumption_resolution,[],[f2308,f259]) ).
fof(f2314,plain,
( ~ spl20_272
| ~ spl20_276 ),
inference(avatar_contradiction_clause,[],[f2313]) ).
fof(f2345,plain,
( e12 != op1(e13,e13)
| ~ spl20_246 ),
inference(forward_demodulation,[],[f160,f1632]) ).
fof(f2346,plain,
( ~ spl20_200
| ~ spl20_246 ),
inference(avatar_split_clause,[],[f2345,f1630,f1390]) ).
fof(f2350,plain,
( e11 = e12
| ~ spl20_182
| ~ spl20_263 ),
inference(forward_demodulation,[],[f1707,f1292]) ).
fof(f2352,plain,
( $false
| ~ spl20_182
| ~ spl20_263 ),
inference(forward_subsumption_resolution,[],[f2350,f258]) ).
fof(f2353,plain,
( ~ spl20_182
| ~ spl20_263 ),
inference(avatar_contradiction_clause,[],[f2352]) ).
fof(f2361,plain,
( e11 = e13
| ~ spl20_175
| ~ spl20_242 ),
inference(superposition,[],[f1256,f1613]) ).
fof(f2365,plain,
( $false
| ~ spl20_175
| ~ spl20_242 ),
inference(forward_subsumption_resolution,[],[f2361,f257]) ).
fof(f2366,plain,
( ~ spl20_175
| ~ spl20_242 ),
inference(avatar_contradiction_clause,[],[f2365]) ).
fof(f2381,plain,
( e10 = e11
| ~ spl20_251
| ~ spl20_256 ),
inference(superposition,[],[f1676,f1654]) ).
fof(f2386,plain,
( $false
| ~ spl20_251
| ~ spl20_256 ),
inference(forward_subsumption_resolution,[],[f2381,f261]) ).
fof(f2387,plain,
( ~ spl20_251
| ~ spl20_256 ),
inference(avatar_contradiction_clause,[],[f2386]) ).
fof(f2425,plain,
( e10 = e12
| ~ spl20_187
| ~ spl20_269 ),
inference(superposition,[],[f1736,f1320]) ).
fof(f2430,plain,
( $false
| ~ spl20_187
| ~ spl20_269 ),
inference(forward_subsumption_resolution,[],[f2425,f260]) ).
fof(f2431,plain,
( ~ spl20_187
| ~ spl20_269 ),
inference(avatar_contradiction_clause,[],[f2430]) ).
fof(f2449,plain,
( e10 = e13
| ~ spl20_176
| ~ spl20_243 ),
inference(superposition,[],[f1260,f1617]) ).
fof(f2453,plain,
( $false
| ~ spl20_176
| ~ spl20_243 ),
inference(forward_subsumption_resolution,[],[f2449,f259]) ).
fof(f2454,plain,
( ~ spl20_176
| ~ spl20_243 ),
inference(avatar_contradiction_clause,[],[f2453]) ).
fof(f2460,plain,
( e12 = e13
| ~ spl20_260
| ~ spl20_264 ),
inference(superposition,[],[f1693,f1711]) ).
fof(f2462,plain,
( $false
| ~ spl20_260
| ~ spl20_264 ),
inference(forward_subsumption_resolution,[],[f2460,f256]) ).
fof(f2463,plain,
( ~ spl20_260
| ~ spl20_264 ),
inference(avatar_contradiction_clause,[],[f2462]) ).
fof(f2478,plain,
( e12 = e13
| ~ spl20_272
| ~ spl20_274 ),
inference(superposition,[],[f1760,f1750]) ).
fof(f2483,plain,
( $false
| ~ spl20_272
| ~ spl20_274 ),
inference(forward_subsumption_resolution,[],[f2478,f256]) ).
fof(f2484,plain,
( ~ spl20_272
| ~ spl20_274 ),
inference(avatar_contradiction_clause,[],[f2483]) ).
fof(f2491,plain,
( e22 = e23
| ~ spl20_166
| ~ spl20_168 ),
inference(superposition,[],[f1224,f1212]) ).
fof(f2495,plain,
( $false
| ~ spl20_166
| ~ spl20_168 ),
inference(forward_subsumption_resolution,[],[f2491,f262]) ).
fof(f2496,plain,
( ~ spl20_166
| ~ spl20_168 ),
inference(avatar_contradiction_clause,[],[f2495]) ).
fof(f2498,plain,
( e20 = e23
| ~ spl20_171
| ~ spl20_222 ),
inference(forward_demodulation,[],[f1238,f1492]) ).
fof(f2505,plain,
( $false
| ~ spl20_171
| ~ spl20_222 ),
inference(forward_subsumption_resolution,[],[f2498,f265]) ).
fof(f2506,plain,
( ~ spl20_171
| ~ spl20_222 ),
inference(avatar_contradiction_clause,[],[f2505]) ).
fof(f2522,plain,
( e21 = e23
| ~ spl20_143
| ~ spl20_206 ),
inference(forward_demodulation,[],[f1421,f1088]) ).
fof(f2523,plain,
( $false
| ~ spl20_143
| ~ spl20_206 ),
inference(forward_subsumption_resolution,[],[f2522,f263]) ).
fof(f2524,plain,
( ~ spl20_143
| ~ spl20_206 ),
inference(avatar_contradiction_clause,[],[f2523]) ).
fof(f2526,plain,
( e22 = e23
| ~ spl20_167
| ~ spl20_210 ),
inference(forward_demodulation,[],[f1218,f1440]) ).
fof(f2529,plain,
( $false
| ~ spl20_167
| ~ spl20_210 ),
inference(forward_subsumption_resolution,[],[f2526,f262]) ).
fof(f2530,plain,
( ~ spl20_167
| ~ spl20_210 ),
inference(avatar_contradiction_clause,[],[f2529]) ).
fof(f2631,plain,
( e21 = e22
| ~ spl20_168
| ~ spl20_170 ),
inference(superposition,[],[f1234,f1224]) ).
fof(f2635,plain,
( $false
| ~ spl20_168
| ~ spl20_170 ),
inference(forward_subsumption_resolution,[],[f2631,f264]) ).
fof(f2636,plain,
( ~ spl20_168
| ~ spl20_170 ),
inference(avatar_contradiction_clause,[],[f2635]) ).
fof(f2642,plain,
( e10 = e11
| ~ spl20_175
| ~ spl20_255 ),
inference(forward_demodulation,[],[f1256,f1671]) ).
fof(f2644,plain,
( $false
| ~ spl20_175
| ~ spl20_255 ),
inference(forward_subsumption_resolution,[],[f2642,f261]) ).
fof(f2645,plain,
( ~ spl20_175
| ~ spl20_255 ),
inference(avatar_contradiction_clause,[],[f2644]) ).
fof(f2660,plain,
( e11 = e12
| ~ spl20_273
| ~ spl20_275 ),
inference(superposition,[],[f1765,f1755]) ).
fof(f2666,plain,
( $false
| ~ spl20_273
| ~ spl20_275 ),
inference(forward_subsumption_resolution,[],[f2660,f258]) ).
fof(f2667,plain,
( ~ spl20_273
| ~ spl20_275 ),
inference(avatar_contradiction_clause,[],[f2666]) ).
fof(f2693,plain,
( e11 = e12
| ~ spl20_248
| ~ spl20_253 ),
inference(superposition,[],[f1662,f1640]) ).
fof(f2697,plain,
( $false
| ~ spl20_248
| ~ spl20_253 ),
inference(forward_subsumption_resolution,[],[f2693,f258]) ).
fof(f2698,plain,
( ~ spl20_248
| ~ spl20_253 ),
inference(avatar_contradiction_clause,[],[f2697]) ).
fof(f2704,plain,
( e10 != op1(e13,e13)
| ~ spl20_256 ),
inference(forward_demodulation,[],[f160,f1676]) ).
fof(f2705,plain,
( ~ spl20_204
| ~ spl20_256 ),
inference(avatar_split_clause,[],[f2704,f1674,f1410]) ).
fof(f2725,plain,
( e11 = e13
| ~ spl20_271
| ~ spl20_275 ),
inference(superposition,[],[f1765,f1745]) ).
fof(f2730,plain,
( $false
| ~ spl20_271
| ~ spl20_275 ),
inference(forward_subsumption_resolution,[],[f2725,f257]) ).
fof(f2731,plain,
( ~ spl20_271
| ~ spl20_275 ),
inference(avatar_contradiction_clause,[],[f2730]) ).
fof(f2732,plain,
( e10 = e12
| ~ spl20_184
| ~ spl20_197 ),
inference(forward_demodulation,[],[f1303,f1371]) ).
fof(f2734,plain,
( $false
| ~ spl20_184
| ~ spl20_197 ),
inference(forward_subsumption_resolution,[],[f2732,f260]) ).
fof(f2735,plain,
( ~ spl20_184
| ~ spl20_197 ),
inference(avatar_contradiction_clause,[],[f2734]) ).
fof(f2780,plain,
( e20 = e22
| ~ spl20_168
| ~ spl20_172 ),
inference(superposition,[],[f1244,f1224]) ).
fof(f2784,plain,
( $false
| ~ spl20_168
| ~ spl20_172 ),
inference(forward_subsumption_resolution,[],[f2780,f266]) ).
fof(f2785,plain,
( ~ spl20_168
| ~ spl20_172 ),
inference(avatar_contradiction_clause,[],[f2784]) ).
fof(f2797,plain,
( e20 = e21
| ~ spl20_156
| ~ spl20_165 ),
inference(superposition,[],[f1203,f1156]) ).
fof(f2803,plain,
( $false
| ~ spl20_156
| ~ spl20_165 ),
inference(forward_subsumption_resolution,[],[f2797,f267]) ).
fof(f2804,plain,
( ~ spl20_156
| ~ spl20_165 ),
inference(avatar_contradiction_clause,[],[f2803]) ).
fof(f2853,plain,
( e21 = e22
| ~ spl20_153
| ~ spl20_159 ),
inference(forward_demodulation,[],[f1141,f1173]) ).
fof(f2856,plain,
( $false
| ~ spl20_153
| ~ spl20_159 ),
inference(forward_subsumption_resolution,[],[f2853,f264]) ).
fof(f2857,plain,
( ~ spl20_153
| ~ spl20_159 ),
inference(avatar_contradiction_clause,[],[f2856]) ).
fof(f2859,plain,
( e20 = e21
| ~ spl20_159
| ~ spl20_163 ),
inference(superposition,[],[f1192,f1173]) ).
fof(f2864,plain,
( $false
| ~ spl20_159
| ~ spl20_163 ),
inference(forward_subsumption_resolution,[],[f2859,f267]) ).
fof(f2865,plain,
( ~ spl20_159
| ~ spl20_163 ),
inference(avatar_contradiction_clause,[],[f2864]) ).
fof(f2869,plain,
( e21 = e22
| ~ spl20_150
| ~ spl20_227 ),
inference(forward_demodulation,[],[f1515,f1124]) ).
fof(f2875,plain,
( $false
| ~ spl20_150
| ~ spl20_227 ),
inference(forward_subsumption_resolution,[],[f2869,f264]) ).
fof(f2876,plain,
( ~ spl20_150
| ~ spl20_227 ),
inference(avatar_contradiction_clause,[],[f2875]) ).
fof(f2933,plain,
( e21 = h1(e12)
| ~ spl20_159 ),
inference(forward_demodulation,[],[f370,f1173]) ).
fof(f2934,plain,
( spl20_138
| ~ spl20_159 ),
inference(avatar_split_clause,[],[f2933,f1171,f1060]) ).
fof(f2949,plain,
( e10 != op1(e13,e11)
| ~ spl20_256 ),
inference(forward_demodulation,[],[f162,f1676]) ).
fof(f2981,plain,
( e10 != op1(e13,e10)
| ~ spl20_256 ),
inference(forward_demodulation,[],[f164,f1676]) ).
fof(f3108,plain,
( e12 = e13
| ~ spl20_198
| ~ spl20_200 ),
inference(superposition,[],[f1392,f1380]) ).
fof(f3110,plain,
( e12 != op1(e13,e11)
| ~ spl20_200 ),
inference(superposition,[],[f161,f1392]) ).
fof(f3112,plain,
( op2(e20,e20) != h1(e12)
| ~ spl20_73
| spl20_74
| ~ spl20_200 ),
inference(superposition,[],[f1798,f1392]) ).
fof(f3113,plain,
( op2(e20,e20) != e21
| ~ spl20_73
| spl20_74
| ~ spl20_138
| ~ spl20_200 ),
inference(forward_demodulation,[],[f3112,f1061]) ).
fof(f3119,plain,
( $false
| ~ spl20_198
| ~ spl20_200 ),
inference(forward_subsumption_resolution,[],[f3108,f256]) ).
fof(f3120,plain,
( ~ spl20_198
| ~ spl20_200 ),
inference(avatar_contradiction_clause,[],[f3119]) ).
fof(f3121,plain,
( $false
| ~ spl20_73
| spl20_74
| ~ spl20_138
| ~ spl20_159
| ~ spl20_200 ),
inference(forward_subsumption_resolution,[],[f3113,f1173]) ).
fof(f3122,plain,
( ~ spl20_73
| spl20_74
| ~ spl20_138
| ~ spl20_159
| ~ spl20_200 ),
inference(avatar_contradiction_clause,[],[f3121]) ).
fof(f3128,plain,
( h1(op1(e10,e12)) != op2(h1(e10),e21)
| spl20_87
| ~ spl20_138 ),
inference(forward_demodulation,[],[f809,f1061]) ).
fof(f3130,plain,
( ~ spl20_247
| ~ spl20_200 ),
inference(avatar_split_clause,[],[f3110,f1390,f1634]) ).
fof(f3159,plain,
( e13 != op1(e12,e11)
| ~ spl20_177 ),
inference(forward_demodulation,[],[f168,f1266]) ).
fof(f3162,plain,
( e13 != op1(e12,e10)
| ~ spl20_177 ),
inference(forward_demodulation,[],[f170,f1266]) ).
fof(f3172,plain,
( e10 != op1(e11,e10)
| ~ spl20_197 ),
inference(forward_demodulation,[],[f177,f1371]) ).
fof(f3175,plain,
( e13 != op1(e10,e11)
| ~ spl20_243 ),
inference(forward_demodulation,[],[f179,f1617]) ).
fof(f3177,plain,
( op1(e10,e10) != e13
| ~ spl20_243 ),
inference(forward_demodulation,[],[f181,f1617]) ).
fof(f3182,plain,
( e12 != op1(e11,e13)
| ~ spl20_200 ),
inference(forward_demodulation,[],[f185,f1392]) ).
fof(f3186,plain,
( e12 != op1(e10,e13)
| ~ spl20_200 ),
inference(forward_demodulation,[],[f187,f1392]) ).
fof(f3194,plain,
( e13 != op1(e11,e12)
| ~ spl20_177 ),
inference(forward_demodulation,[],[f192,f1266]) ).
fof(f3201,plain,
( e13 != op1(e11,e11)
| ~ spl20_201 ),
inference(forward_demodulation,[],[f197,f1396]) ).
fof(f3220,plain,
( e22 != op2(e23,e20)
| ~ spl20_168 ),
inference(forward_demodulation,[],[f211,f1224]) ).
fof(f3228,plain,
( e23 != op2(e22,e21)
| ~ spl20_145 ),
inference(forward_demodulation,[],[f216,f1098]) ).
fof(f3242,plain,
( e20 != op2(e21,e20)
| ~ spl20_165 ),
inference(forward_demodulation,[],[f225,f1203]) ).
fof(f3245,plain,
( e23 != op2(e20,e21)
| ~ spl20_207 ),
inference(forward_demodulation,[],[f227,f1425]) ).
fof(f3257,plain,
( e22 != op2(e20,e23)
| ~ spl20_168 ),
inference(forward_demodulation,[],[f235,f1224]) ).
fof(f3290,plain,
( e11 = op1(e12,e13)
| ~ spl20_200 ),
inference(forward_demodulation,[],[f365,f1392]) ).
fof(f3298,plain,
( e11 != op1(e11,e10)
| ~ spl20_191 ),
inference(forward_demodulation,[],[f207,f1341]) ).
fof(f3300,plain,
( e11 != op1(e12,e13)
| ~ spl20_266 ),
inference(forward_demodulation,[],[f167,f1722]) ).
fof(f3302,plain,
( spl20_249
| ~ spl20_200 ),
inference(avatar_split_clause,[],[f3290,f1390,f1643]) ).
fof(f3307,plain,
( ~ spl20_178
| ~ spl20_201 ),
inference(avatar_split_clause,[],[f3201,f1395,f1269]) ).
fof(f3311,plain,
( ~ spl20_244
| ~ spl20_200 ),
inference(avatar_split_clause,[],[f3182,f1390,f1621]) ).
fof(f3312,plain,
( e13 != op1(e11,e13)
| ~ spl20_243 ),
inference(forward_demodulation,[],[f189,f1617]) ).
fof(f3314,plain,
( ~ spl20_194
| ~ spl20_191 ),
inference(avatar_split_clause,[],[f3298,f1339,f1355]) ).
fof(f3316,plain,
( ~ spl20_249
| ~ spl20_266 ),
inference(avatar_split_clause,[],[f3300,f1720,f1643]) ).
fof(f3321,plain,
( ~ spl20_245
| ~ spl20_200 ),
inference(avatar_split_clause,[],[f3186,f1390,f1625]) ).
fof(f3325,plain,
( ~ spl20_242
| ~ spl20_243 ),
inference(avatar_split_clause,[],[f3312,f1615,f1611]) ).
fof(f3326,plain,
( ~ spl20_271
| ~ spl20_243 ),
inference(avatar_split_clause,[],[f3175,f1615,f1743]) ).
fof(f3328,plain,
( ~ spl20_258
| ~ spl20_256 ),
inference(avatar_split_clause,[],[f2981,f1674,f1682]) ).
fof(f3330,plain,
( ~ spl20_257
| ~ spl20_256 ),
inference(avatar_split_clause,[],[f2949,f1674,f1678]) ).
fof(f3339,plain,
( e10 = e12
| ~ spl20_181
| ~ spl20_196 ),
inference(superposition,[],[f1366,f1288]) ).
fof(f3344,plain,
( $false
| ~ spl20_181
| ~ spl20_196 ),
inference(forward_subsumption_resolution,[],[f3339,f260]) ).
fof(f3345,plain,
( ~ spl20_181
| ~ spl20_196 ),
inference(avatar_contradiction_clause,[],[f3344]) ).
fof(f3346,plain,
( ~ spl20_261
| ~ spl20_177 ),
inference(avatar_split_clause,[],[f3159,f1264,f1696]) ).
fof(f3347,plain,
( ~ spl20_262
| ~ spl20_177 ),
inference(avatar_split_clause,[],[f3162,f1264,f1700]) ).
fof(f3348,plain,
( ~ spl20_259
| ~ spl20_177 ),
inference(avatar_split_clause,[],[f3194,f1264,f1687]) ).
fof(f3349,plain,
( ~ spl20_276
| ~ spl20_197 ),
inference(avatar_split_clause,[],[f3172,f1369,f1770]) ).
fof(f3382,plain,
( h1(e12) != op2(h1(e10),e21)
| spl20_87
| ~ spl20_138
| ~ spl20_264 ),
inference(superposition,[],[f3128,f1711]) ).
fof(f3384,plain,
( e21 != op2(h1(e10),e21)
| spl20_87
| ~ spl20_138
| ~ spl20_264 ),
inference(forward_demodulation,[],[f3382,f1061]) ).
fof(f3410,plain,
( e11 = e12
| ~ spl20_200
| ~ spl20_202 ),
inference(superposition,[],[f1402,f1392]) ).
fof(f3417,plain,
( $false
| ~ spl20_200
| ~ spl20_202 ),
inference(forward_subsumption_resolution,[],[f3410,f258]) ).
fof(f3418,plain,
( ~ spl20_200
| ~ spl20_202 ),
inference(avatar_contradiction_clause,[],[f3417]) ).
fof(f3423,plain,
( e11 != op1(e12,e12)
| ~ spl20_249 ),
inference(forward_demodulation,[],[f166,f1645]) ).
fof(f3442,plain,
( e12 != op1(e10,e11)
| ~ spl20_264 ),
inference(forward_demodulation,[],[f180,f1711]) ).
fof(f3449,plain,
( e11 != op1(e10,e13)
| ~ spl20_249 ),
inference(forward_demodulation,[],[f188,f1645]) ).
fof(f3465,plain,
( e11 != op1(e11,e11)
| ~ spl20_252 ),
inference(forward_demodulation,[],[f197,f1658]) ).
fof(f3467,plain,
( e11 != op1(e10,e11)
| ~ spl20_252 ),
inference(forward_demodulation,[],[f199,f1658]) ).
fof(f3480,plain,
( e10 = op1(e13,e12)
| ~ spl20_200 ),
inference(forward_demodulation,[],[f366,f1392]) ).
fof(f3481,plain,
( e21 = op2(e22,e23)
| ~ spl20_168 ),
inference(forward_demodulation,[],[f368,f1224]) ).
fof(f3484,plain,
( e21 != op2(e20,e21)
| ~ spl20_159 ),
inference(forward_demodulation,[],[f231,f1173]) ).
fof(f3485,plain,
( ~ spl20_235
| ~ spl20_207 ),
inference(avatar_split_clause,[],[f3245,f1423,f1551]) ).
fof(f3486,plain,
( e20 != op2(e22,e21)
| ~ spl20_165 ),
inference(forward_demodulation,[],[f246,f1203]) ).
fof(f3489,plain,
( e23 != op2(e23,e20)
| ~ spl20_236 ),
inference(forward_demodulation,[],[f251,f1558]) ).
fof(f3494,plain,
( e23 != op2(e23,e22)
| ~ spl20_145 ),
inference(forward_demodulation,[],[f238,f1098]) ).
fof(f3495,plain,
( spl20_213
| ~ spl20_168 ),
inference(avatar_split_clause,[],[f3481,f1222,f1451]) ).
fof(f3496,plain,
( ~ spl20_212
| ~ spl20_168 ),
inference(avatar_split_clause,[],[f3220,f1222,f1446]) ).
fof(f3502,plain,
( e20 != op2(e21,e23)
| ~ spl20_165 ),
inference(forward_demodulation,[],[f221,f1203]) ).
fof(f3506,plain,
( ~ spl20_239
| ~ spl20_159 ),
inference(avatar_split_clause,[],[f3484,f1171,f1571]) ).
fof(f3507,plain,
( ~ spl20_233
| ~ spl20_165 ),
inference(avatar_split_clause,[],[f3486,f1201,f1542]) ).
fof(f3509,plain,
( ~ spl20_171
| ~ spl20_236 ),
inference(avatar_split_clause,[],[f3489,f1556,f1237]) ).
fof(f3510,plain,
( ~ spl20_167
| ~ spl20_145 ),
inference(avatar_split_clause,[],[f3494,f1096,f1217]) ).
fof(f3514,plain,
( ~ spl20_219
| ~ spl20_165 ),
inference(avatar_split_clause,[],[f3502,f1201,f1477]) ).
fof(f3517,plain,
( ~ spl20_240
| ~ spl20_165 ),
inference(avatar_split_clause,[],[f3242,f1201,f1578]) ).
fof(f3520,plain,
( ~ spl20_209
| ~ spl20_168 ),
inference(avatar_split_clause,[],[f3257,f1222,f1433]) ).
fof(f3563,plain,
( e21 != op2(e22,e21)
| ~ spl20_213 ),
inference(forward_demodulation,[],[f215,f1453]) ).
fof(f3572,plain,
( e22 != op2(e20,e21)
| ~ spl20_228 ),
inference(forward_demodulation,[],[f228,f1519]) ).
fof(f3588,plain,
( e22 != op2(e20,e21)
| ~ spl20_155 ),
inference(forward_demodulation,[],[f248,f1152]) ).
fof(f3595,plain,
( op2(e21,e20) = h1(e11)
| ~ spl20_159 ),
inference(forward_demodulation,[],[f371,f1173]) ).
fof(f3596,plain,
( e22 = h1(e11)
| ~ spl20_159
| ~ spl20_238 ),
inference(forward_demodulation,[],[f3595,f1568]) ).
fof(f3597,plain,
( spl20_135
| ~ spl20_159
| ~ spl20_238 ),
inference(avatar_split_clause,[],[f3596,f1566,f1171,f1045]) ).
fof(f3598,plain,
( op2(e20,e21) = h1(e10)
| ~ spl20_159 ),
inference(forward_demodulation,[],[f372,f1173]) ).
fof(f3599,plain,
( e23 = h1(e10)
| ~ spl20_159
| ~ spl20_235 ),
inference(forward_demodulation,[],[f3598,f1553]) ).
fof(f3600,plain,
( spl20_132
| ~ spl20_159
| ~ spl20_235 ),
inference(avatar_split_clause,[],[f3599,f1551,f1171,f1030]) ).
fof(f3601,plain,
( e21 != op2(e23,e21)
| spl20_87
| ~ spl20_132
| ~ spl20_138
| ~ spl20_264 ),
inference(superposition,[],[f3384,f1031]) ).
fof(f3602,plain,
( $false
| spl20_87
| ~ spl20_132
| ~ spl20_138
| ~ spl20_216
| ~ spl20_264 ),
inference(forward_subsumption_resolution,[],[f3601,f1466]) ).
fof(f3603,plain,
( spl20_87
| ~ spl20_132
| ~ spl20_138
| ~ spl20_216
| ~ spl20_264 ),
inference(avatar_contradiction_clause,[],[f3602]) ).
fof(f3604,plain,
( h1(op1(e13,e12)) != op2(h1(e13),e21)
| spl20_75
| ~ spl20_138 ),
inference(forward_demodulation,[],[f761,f1061]) ).
fof(f3606,plain,
( op2(e20,e21) != h1(op1(e13,e12))
| ~ spl20_73
| spl20_75
| ~ spl20_138 ),
inference(forward_demodulation,[],[f3604,f752]) ).
fof(f3608,plain,
( op2(e20,e21) != h1(e10)
| ~ spl20_73
| spl20_75
| ~ spl20_138
| ~ spl20_256 ),
inference(forward_demodulation,[],[f3606,f1676]) ).
fof(f3610,plain,
( e23 != op2(e20,e21)
| ~ spl20_73
| spl20_75
| ~ spl20_132
| ~ spl20_138
| ~ spl20_256 ),
inference(forward_demodulation,[],[f3608,f1031]) ).
fof(f3612,plain,
( $false
| ~ spl20_73
| spl20_75
| ~ spl20_132
| ~ spl20_138
| ~ spl20_235
| ~ spl20_256 ),
inference(forward_subsumption_resolution,[],[f3610,f1553]) ).
fof(f3613,plain,
( ~ spl20_73
| spl20_75
| ~ spl20_132
| ~ spl20_138
| ~ spl20_235
| ~ spl20_256 ),
inference(avatar_contradiction_clause,[],[f3612]) ).
fof(f3615,plain,
( h1(op1(e13,e11)) != op2(e20,h1(e11))
| ~ spl20_73
| spl20_76 ),
inference(forward_demodulation,[],[f765,f752]) ).
fof(f3617,plain,
( h1(e11) != op2(e20,h1(e11))
| ~ spl20_73
| spl20_76
| ~ spl20_252 ),
inference(forward_demodulation,[],[f3615,f1658]) ).
fof(f3620,plain,
( e22 != op2(e20,e22)
| ~ spl20_73
| spl20_76
| ~ spl20_135
| ~ spl20_252 ),
inference(superposition,[],[f3617,f1046]) ).
fof(f3624,plain,
( h1(op1(e13,e10)) != op2(h1(e13),e23)
| spl20_77
| ~ spl20_132 ),
inference(forward_demodulation,[],[f769,f1031]) ).
fof(f3626,plain,
( op2(e20,e23) != h1(op1(e13,e10))
| ~ spl20_73
| spl20_77
| ~ spl20_132 ),
inference(forward_demodulation,[],[f3624,f752]) ).
fof(f3628,plain,
( op2(e20,e23) != h1(e13)
| ~ spl20_73
| spl20_77
| ~ spl20_132
| ~ spl20_203 ),
inference(forward_demodulation,[],[f3626,f1406]) ).
fof(f3630,plain,
( e20 != op2(e20,e23)
| ~ spl20_73
| spl20_77
| ~ spl20_132
| ~ spl20_203 ),
inference(forward_demodulation,[],[f3628,f752]) ).
fof(f3631,plain,
( $false
| ~ spl20_73
| spl20_77
| ~ spl20_132
| ~ spl20_144
| ~ spl20_203 ),
inference(forward_subsumption_resolution,[],[f3630,f1092]) ).
fof(f3632,plain,
( ~ spl20_73
| spl20_77
| ~ spl20_132
| ~ spl20_144
| ~ spl20_203 ),
inference(avatar_contradiction_clause,[],[f3631]) ).
fof(f3634,plain,
( h1(op1(e12,e13)) != op2(h1(e12),e20)
| ~ spl20_73
| spl20_78 ),
inference(forward_demodulation,[],[f773,f752]) ).
fof(f3636,plain,
( op2(e21,e20) != h1(op1(e12,e13))
| ~ spl20_73
| spl20_78
| ~ spl20_138 ),
inference(forward_demodulation,[],[f3634,f1061]) ).
fof(f3638,plain,
( op2(e21,e20) != h1(e11)
| ~ spl20_73
| spl20_78
| ~ spl20_138
| ~ spl20_249 ),
inference(forward_demodulation,[],[f3636,f1645]) ).
fof(f3640,plain,
( e22 != op2(e21,e20)
| ~ spl20_73
| spl20_78
| ~ spl20_135
| ~ spl20_138
| ~ spl20_249 ),
inference(forward_demodulation,[],[f3638,f1046]) ).
fof(f3641,plain,
( $false
| ~ spl20_73
| spl20_78
| ~ spl20_135
| ~ spl20_138
| ~ spl20_238
| ~ spl20_249 ),
inference(forward_subsumption_resolution,[],[f3640,f1568]) ).
fof(f3642,plain,
( ~ spl20_73
| spl20_78
| ~ spl20_135
| ~ spl20_138
| ~ spl20_238
| ~ spl20_249 ),
inference(avatar_contradiction_clause,[],[f3641]) ).
fof(f3644,plain,
( op2(e21,e21) != h1(op1(e12,e12))
| spl20_79
| ~ spl20_138 ),
inference(forward_demodulation,[],[f777,f1061]) ).
fof(f3646,plain,
( op2(e21,e21) != h1(e13)
| spl20_79
| ~ spl20_138
| ~ spl20_177 ),
inference(forward_demodulation,[],[f3644,f1266]) ).
fof(f3648,plain,
( e20 != op2(e21,e21)
| ~ spl20_73
| spl20_79
| ~ spl20_138
| ~ spl20_177 ),
inference(forward_demodulation,[],[f3646,f752]) ).
fof(f3650,plain,
( $false
| ~ spl20_73
| spl20_79
| ~ spl20_138
| ~ spl20_165
| ~ spl20_177 ),
inference(forward_subsumption_resolution,[],[f3648,f1203]) ).
fof(f3651,plain,
( ~ spl20_73
| spl20_79
| ~ spl20_138
| ~ spl20_165
| ~ spl20_177 ),
inference(avatar_contradiction_clause,[],[f3650]) ).
fof(f3653,plain,
( h1(op1(e12,e11)) != op2(h1(e12),e22)
| spl20_80
| ~ spl20_135 ),
inference(forward_demodulation,[],[f781,f1046]) ).
fof(f3655,plain,
( op2(e21,e22) != h1(op1(e12,e11))
| spl20_80
| ~ spl20_135
| ~ spl20_138 ),
inference(forward_demodulation,[],[f3653,f1061]) ).
fof(f3657,plain,
( op2(e21,e22) != h1(e12)
| spl20_80
| ~ spl20_135
| ~ spl20_138
| ~ spl20_187 ),
inference(forward_demodulation,[],[f3655,f1320]) ).
fof(f3658,plain,
( e21 != op2(e21,e22)
| spl20_80
| ~ spl20_135
| ~ spl20_138
| ~ spl20_187 ),
inference(forward_demodulation,[],[f3657,f1061]) ).
fof(f3659,plain,
( $false
| spl20_80
| ~ spl20_135
| ~ spl20_138
| ~ spl20_150
| ~ spl20_187 ),
inference(forward_subsumption_resolution,[],[f3658,f1124]) ).
fof(f3660,plain,
( spl20_80
| ~ spl20_135
| ~ spl20_138
| ~ spl20_150
| ~ spl20_187 ),
inference(avatar_contradiction_clause,[],[f3659]) ).
fof(f3662,plain,
( h1(op1(e12,e10)) != op2(h1(e12),e23)
| spl20_81
| ~ spl20_132 ),
inference(forward_demodulation,[],[f785,f1031]) ).
fof(f3664,plain,
( op2(e21,e23) != h1(op1(e12,e10))
| spl20_81
| ~ spl20_132
| ~ spl20_138 ),
inference(forward_demodulation,[],[f3662,f1061]) ).
fof(f3666,plain,
( op2(e21,e23) != h1(e10)
| spl20_81
| ~ spl20_132
| ~ spl20_138
| ~ spl20_270 ),
inference(forward_demodulation,[],[f3664,f1740]) ).
fof(f3668,plain,
( e23 != op2(e21,e23)
| spl20_81
| ~ spl20_132
| ~ spl20_138
| ~ spl20_270 ),
inference(forward_demodulation,[],[f3666,f1031]) ).
fof(f3669,plain,
( $false
| spl20_81
| ~ spl20_132
| ~ spl20_138
| ~ spl20_206
| ~ spl20_270 ),
inference(forward_subsumption_resolution,[],[f3668,f1421]) ).
fof(f3670,plain,
( spl20_81
| ~ spl20_132
| ~ spl20_138
| ~ spl20_206
| ~ spl20_270 ),
inference(avatar_contradiction_clause,[],[f3669]) ).
fof(f3672,plain,
( h1(op1(e11,e13)) != op2(h1(e11),e20)
| ~ spl20_73
| spl20_82 ),
inference(forward_demodulation,[],[f789,f752]) ).
fof(f3674,plain,
( op2(e22,e20) != h1(op1(e11,e13))
| ~ spl20_73
| spl20_82
| ~ spl20_135 ),
inference(forward_demodulation,[],[f3672,f1046]) ).
fof(f3676,plain,
( op2(e22,e20) != h1(e13)
| ~ spl20_73
| spl20_82
| ~ spl20_135
| ~ spl20_242 ),
inference(forward_demodulation,[],[f3674,f1613]) ).
fof(f3678,plain,
( e20 != op2(e22,e20)
| ~ spl20_73
| spl20_82
| ~ spl20_135
| ~ spl20_242 ),
inference(forward_demodulation,[],[f3676,f752]) ).
fof(f3679,plain,
( $false
| ~ spl20_73
| spl20_82
| ~ spl20_135
| ~ spl20_234
| ~ spl20_242 ),
inference(forward_subsumption_resolution,[],[f3678,f1548]) ).
fof(f3680,plain,
( ~ spl20_73
| spl20_82
| ~ spl20_135
| ~ spl20_234
| ~ spl20_242 ),
inference(avatar_contradiction_clause,[],[f3679]) ).
fof(f3682,plain,
( h1(op1(e11,e12)) != op2(h1(e11),e21)
| spl20_83
| ~ spl20_138 ),
inference(forward_demodulation,[],[f793,f1061]) ).
fof(f3684,plain,
( op2(e22,e21) != h1(op1(e11,e12))
| spl20_83
| ~ spl20_135
| ~ spl20_138 ),
inference(forward_demodulation,[],[f3682,f1046]) ).
fof(f3686,plain,
( op2(e22,e21) != h1(e11)
| spl20_83
| ~ spl20_135
| ~ spl20_138
| ~ spl20_182 ),
inference(forward_demodulation,[],[f3684,f1292]) ).
fof(f3688,plain,
( e22 != op2(e22,e21)
| spl20_83
| ~ spl20_135
| ~ spl20_138
| ~ spl20_182 ),
inference(forward_demodulation,[],[f3686,f1046]) ).
fof(f3692,plain,
( op2(e22,e22) != h1(op1(e11,e11))
| spl20_84
| ~ spl20_135 ),
inference(forward_demodulation,[],[f797,f1046]) ).
fof(f3694,plain,
( op2(e22,e22) != h1(e10)
| spl20_84
| ~ spl20_135
| ~ spl20_197 ),
inference(forward_demodulation,[],[f3692,f1371]) ).
fof(f3696,plain,
( e23 != op2(e22,e22)
| spl20_84
| ~ spl20_132
| ~ spl20_135
| ~ spl20_197 ),
inference(forward_demodulation,[],[f3694,f1031]) ).
fof(f3698,plain,
( $false
| spl20_84
| ~ spl20_132
| ~ spl20_135
| ~ spl20_145
| ~ spl20_197 ),
inference(forward_subsumption_resolution,[],[f3696,f1098]) ).
fof(f3699,plain,
( spl20_84
| ~ spl20_132
| ~ spl20_135
| ~ spl20_145
| ~ spl20_197 ),
inference(avatar_contradiction_clause,[],[f3698]) ).
fof(f3701,plain,
( h1(op1(e11,e10)) != op2(h1(e11),e23)
| spl20_85
| ~ spl20_132 ),
inference(forward_demodulation,[],[f801,f1031]) ).
fof(f3703,plain,
( op2(e22,e23) != h1(op1(e11,e10))
| spl20_85
| ~ spl20_132
| ~ spl20_135 ),
inference(forward_demodulation,[],[f3701,f1046]) ).
fof(f3705,plain,
( op2(e22,e23) != h1(e12)
| spl20_85
| ~ spl20_132
| ~ spl20_135
| ~ spl20_274 ),
inference(forward_demodulation,[],[f3703,f1760]) ).
fof(f3706,plain,
( e21 != op2(e22,e23)
| spl20_85
| ~ spl20_132
| ~ spl20_135
| ~ spl20_138
| ~ spl20_274 ),
inference(forward_demodulation,[],[f3705,f1061]) ).
fof(f3707,plain,
( $false
| spl20_85
| ~ spl20_132
| ~ spl20_135
| ~ spl20_138
| ~ spl20_213
| ~ spl20_274 ),
inference(forward_subsumption_resolution,[],[f3706,f1453]) ).
fof(f3708,plain,
( spl20_85
| ~ spl20_132
| ~ spl20_135
| ~ spl20_138
| ~ spl20_213
| ~ spl20_274 ),
inference(avatar_contradiction_clause,[],[f3707]) ).
fof(f3710,plain,
( h1(op1(e10,e13)) != op2(h1(e10),e20)
| ~ spl20_73
| spl20_86 ),
inference(forward_demodulation,[],[f805,f752]) ).
fof(f3712,plain,
( op2(e23,e20) != h1(op1(e10,e13))
| ~ spl20_73
| spl20_86
| ~ spl20_132 ),
inference(forward_demodulation,[],[f3710,f1031]) ).
fof(f3714,plain,
( op2(e23,e20) != h1(e10)
| ~ spl20_73
| spl20_86
| ~ spl20_132
| ~ spl20_176 ),
inference(forward_demodulation,[],[f3712,f1260]) ).
fof(f3716,plain,
( e23 != op2(e23,e20)
| ~ spl20_73
| spl20_86
| ~ spl20_132
| ~ spl20_176 ),
inference(forward_demodulation,[],[f3714,f1031]) ).
fof(f3717,plain,
( $false
| ~ spl20_73
| spl20_86
| ~ spl20_132
| ~ spl20_171
| ~ spl20_176 ),
inference(forward_subsumption_resolution,[],[f3716,f1238]) ).
fof(f3718,plain,
( ~ spl20_73
| spl20_86
| ~ spl20_132
| ~ spl20_171
| ~ spl20_176 ),
inference(avatar_contradiction_clause,[],[f3717]) ).
fof(f3720,plain,
( h1(op1(e10,e11)) != op2(h1(e10),e22)
| spl20_88
| ~ spl20_135 ),
inference(forward_demodulation,[],[f813,f1046]) ).
fof(f3722,plain,
( op2(e23,e22) != h1(op1(e10,e11))
| spl20_88
| ~ spl20_132
| ~ spl20_135 ),
inference(forward_demodulation,[],[f3720,f1031]) ).
fof(f3724,plain,
( op2(e23,e22) != h1(e13)
| spl20_88
| ~ spl20_132
| ~ spl20_135
| ~ spl20_271 ),
inference(forward_demodulation,[],[f3722,f1745]) ).
fof(f3726,plain,
( e20 != op2(e23,e22)
| ~ spl20_73
| spl20_88
| ~ spl20_132
| ~ spl20_135
| ~ spl20_271 ),
inference(forward_demodulation,[],[f3724,f752]) ).
fof(f3727,plain,
( $false
| ~ spl20_73
| spl20_88
| ~ spl20_132
| ~ spl20_135
| ~ spl20_220
| ~ spl20_271 ),
inference(forward_subsumption_resolution,[],[f3726,f1484]) ).
fof(f3728,plain,
( ~ spl20_73
| spl20_88
| ~ spl20_132
| ~ spl20_135
| ~ spl20_220
| ~ spl20_271 ),
inference(avatar_contradiction_clause,[],[f3727]) ).
fof(f3730,plain,
( op2(e23,e23) != h1(op1(e10,e10))
| spl20_89
| ~ spl20_132 ),
inference(forward_demodulation,[],[f817,f1031]) ).
fof(f3732,plain,
( op2(e23,e23) != h1(e11)
| spl20_89
| ~ spl20_132
| ~ spl20_191 ),
inference(forward_demodulation,[],[f3730,f1341]) ).
fof(f3734,plain,
( e22 != op2(e23,e23)
| spl20_89
| ~ spl20_132
| ~ spl20_135
| ~ spl20_191 ),
inference(forward_demodulation,[],[f3732,f1046]) ).
fof(f3736,plain,
( $false
| spl20_89
| ~ spl20_132
| ~ spl20_135
| ~ spl20_168
| ~ spl20_191 ),
inference(forward_subsumption_resolution,[],[f3734,f1224]) ).
fof(f3737,plain,
( spl20_89
| ~ spl20_132
| ~ spl20_135
| ~ spl20_168
| ~ spl20_191 ),
inference(avatar_contradiction_clause,[],[f3736]) ).
fof(f3744,plain,
( ~ spl20_225
| ~ spl20_145 ),
inference(avatar_split_clause,[],[f3228,f1096,f1504]) ).
fof(f3746,plain,
( ~ spl20_230
| ~ spl20_213 ),
inference(avatar_split_clause,[],[f3563,f1451,f1528]) ).
fof(f3769,plain,
( ~ spl20_228
| ~ spl20_73
| spl20_76
| ~ spl20_135
| ~ spl20_252 ),
inference(avatar_split_clause,[],[f3620,f1656,f1045,f763,f751,f1517]) ).
fof(f3773,plain,
( ~ spl20_155
| spl20_83
| ~ spl20_135
| ~ spl20_138
| ~ spl20_182 ),
inference(avatar_split_clause,[],[f3688,f1291,f1060,f1045,f791,f1151]) ).
fof(f3780,plain,
( e23 != op2(e21,e21)
| ~ spl20_206 ),
inference(forward_demodulation,[],[f221,f1421]) ).
fof(f3784,plain,
( e21 != op2(e22,e22)
| ~ spl20_213 ),
inference(forward_demodulation,[],[f214,f1453]) ).
fof(f3785,plain,
( e20 != op2(e22,e22)
| ~ spl20_220 ),
inference(forward_demodulation,[],[f238,f1484]) ).
fof(f3793,plain,
( ~ spl20_146
| ~ spl20_206 ),
inference(avatar_split_clause,[],[f3780,f1419,f1101]) ).
fof(f3796,plain,
( ~ spl20_158
| ~ spl20_213 ),
inference(avatar_split_clause,[],[f3784,f1451,f1164]) ).
fof(f3797,plain,
( ~ spl20_164
| ~ spl20_220 ),
inference(avatar_split_clause,[],[f3785,f1482,f1196]) ).
fof(f3821,plain,
( ~ spl20_237
| ~ spl20_155 ),
inference(avatar_split_clause,[],[f3588,f1151,f1561]) ).
fof(f3825,plain,
( e11 = e12
| ~ spl20_174
| ~ spl20_249 ),
inference(forward_demodulation,[],[f1252,f1645]) ).
fof(f3826,plain,
( ~ spl20_237
| ~ spl20_228 ),
inference(avatar_split_clause,[],[f3572,f1517,f1561]) ).
fof(f3829,plain,
( ~ spl20_179
| ~ spl20_243 ),
inference(avatar_split_clause,[],[f3177,f1615,f1275]) ).
fof(f3833,plain,
( ~ spl20_273
| ~ spl20_264 ),
inference(avatar_split_clause,[],[f3442,f1709,f1753]) ).
fof(f3834,plain,
( ~ spl20_275
| ~ spl20_252 ),
inference(avatar_split_clause,[],[f3467,f1656,f1763]) ).
fof(f3838,plain,
( spl20_256
| ~ spl20_200 ),
inference(avatar_split_clause,[],[f3480,f1390,f1674]) ).
fof(f3844,plain,
( ~ spl20_188
| ~ spl20_252 ),
inference(avatar_split_clause,[],[f3465,f1656,f1323]) ).
fof(f3845,plain,
( e10 != op1(e12,e11)
| ~ spl20_270 ),
inference(forward_demodulation,[],[f171,f1740]) ).
fof(f3849,plain,
( ~ spl20_190
| ~ spl20_249 ),
inference(avatar_split_clause,[],[f3423,f1643,f1332]) ).
fof(f3854,plain,
( ~ spl20_250
| ~ spl20_249 ),
inference(avatar_split_clause,[],[f3449,f1643,f1647]) ).
fof(f3867,plain,
( $false
| ~ spl20_174
| ~ spl20_249 ),
inference(forward_subsumption_resolution,[],[f3825,f258]) ).
fof(f3868,plain,
( ~ spl20_174
| ~ spl20_249 ),
inference(avatar_contradiction_clause,[],[f3867]) ).
fof(f3869,plain,
( ~ spl20_269
| ~ spl20_270 ),
inference(avatar_split_clause,[],[f3845,f1738,f1734]) ).
cnf(s13,plain,
( spl20_70
| spl20_71
| spl20_72
| ~ spl20_73
| ~ spl20_74
| ~ spl20_75
| ~ spl20_76
| ~ spl20_77
| ~ spl20_78
| ~ spl20_79
| ~ spl20_80
| ~ spl20_81
| ~ spl20_82
| ~ spl20_83
| ~ spl20_84
| ~ spl20_85
| ~ spl20_86
| ~ spl20_87
| ~ spl20_88
| ~ spl20_89 ),
inference(sat_conversion,[],[f818]) ).
cnf(s56,plain,
( ~ spl20_70
| ~ spl20_132 ),
inference(sat_conversion,[],[f1033]) ).
cnf(s59,plain,
( ~ spl20_71
| ~ spl20_135 ),
inference(sat_conversion,[],[f1048]) ).
cnf(s62,plain,
( ~ spl20_72
| ~ spl20_138 ),
inference(sat_conversion,[],[f1063]) ).
cnf(s68,plain,
spl20_73,
inference(sat_conversion,[],[f1077]) ).
cnf(s74,plain,
( spl20_141
| ~ spl20_143
| spl20_145
| spl20_147 ),
inference(sat_conversion,[],[f1111]) ).
cnf(s76,plain,
( spl20_141
| spl20_145
| spl20_146
| spl20_147 ),
inference(sat_conversion,[],[f1113]) ).
cnf(s83,plain,
( spl20_148
| ~ spl20_149
| spl20_152
| spl20_153 ),
inference(sat_conversion,[],[f1144]) ).
cnf(s88,plain,
( spl20_154
| spl20_156
| ~ spl20_157
| spl20_158 ),
inference(sat_conversion,[],[f1169]) ).
cnf(s90,plain,
( spl20_154
| ~ spl20_156
| spl20_158
| spl20_159 ),
inference(sat_conversion,[],[f1175]) ).
cnf(s92,plain,
( spl20_154
| spl20_156
| spl20_158
| spl20_159 ),
inference(sat_conversion,[],[f1177]) ).
cnf(s98,plain,
( spl20_160
| ~ spl20_162
| spl20_163
| spl20_164 ),
inference(sat_conversion,[],[f1207]) ).
cnf(s99,plain,
( spl20_160
| ~ spl20_161
| spl20_163
| spl20_165 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s100,plain,
( spl20_160
| spl20_163
| spl20_164
| spl20_165 ),
inference(sat_conversion,[],[f1209]) ).
cnf(s102,plain,
( ~ spl20_141
| spl20_166 ),
inference(sat_conversion,[],[f1215]) ).
cnf(s103,plain,
( ~ spl20_148
| ~ spl20_167 ),
inference(sat_conversion,[],[f1220]) ).
cnf(s106,plain,
( ~ spl20_154
| spl20_170 ),
inference(sat_conversion,[],[f1235]) ).
cnf(s108,plain,
( ~ spl20_160
| spl20_172 ),
inference(sat_conversion,[],[f1245]) ).
cnf(s112,plain,
( spl20_173
| ~ spl20_176
| spl20_177
| spl20_178 ),
inference(sat_conversion,[],[f1273]) ).
cnf(s116,plain,
( spl20_173
| spl20_177
| spl20_178
| spl20_179 ),
inference(sat_conversion,[],[f1281]) ).
cnf(s128,plain,
( spl20_186
| spl20_188
| ~ spl20_189
| spl20_190 ),
inference(sat_conversion,[],[f1337]) ).
cnf(s130,plain,
( spl20_186
| ~ spl20_188
| spl20_190
| spl20_191 ),
inference(sat_conversion,[],[f1343]) ).
cnf(s132,plain,
( spl20_186
| spl20_188
| spl20_190
| spl20_191 ),
inference(sat_conversion,[],[f1345]) ).
cnf(s139,plain,
( spl20_192
| ~ spl20_193
| spl20_195
| spl20_197 ),
inference(sat_conversion,[],[f1376]) ).
cnf(s140,plain,
( spl20_192
| spl20_195
| spl20_196
| spl20_197 ),
inference(sat_conversion,[],[f1377]) ).
cnf(s142,plain,
( ~ spl20_173
| spl20_198 ),
inference(sat_conversion,[],[f1383]) ).
cnf(s146,plain,
( ~ spl20_186
| spl20_202 ),
inference(sat_conversion,[],[f1403]) ).
cnf(s148,plain,
( ~ spl20_192
| spl20_204 ),
inference(sat_conversion,[],[f1413]) ).
cnf(s149,plain,
( spl20_166
| spl20_205
| spl20_206
| spl20_207 ),
inference(sat_conversion,[],[f1426]) ).
cnf(s150,plain,
( spl20_166
| spl20_167
| spl20_169
| spl20_171 ),
inference(sat_conversion,[],[f1427]) ).
cnf(s155,plain,
( spl20_144
| spl20_172
| spl20_218
| spl20_219 ),
inference(sat_conversion,[],[f1480]) ).
cnf(s156,plain,
( spl20_172
| spl20_220
| spl20_221
| spl20_222 ),
inference(sat_conversion,[],[f1493]) ).
cnf(s159,plain,
( spl20_149
| spl20_210
| spl20_227
| spl20_228 ),
inference(sat_conversion,[],[f1520]) ).
cnf(s164,plain,
( spl20_164
| spl20_218
| spl20_233
| spl20_234 ),
inference(sat_conversion,[],[f1549]) ).
cnf(s165,plain,
( spl20_146
| spl20_169
| spl20_225
| spl20_235 ),
inference(sat_conversion,[],[f1554]) ).
cnf(s169,plain,
( spl20_156
| spl20_216
| spl20_230
| spl20_239 ),
inference(sat_conversion,[],[f1574]) ).
cnf(s170,plain,
( spl20_143
| spl20_150
| spl20_156
| spl20_162 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s175,plain,
( spl20_153
| spl20_161
| spl20_212
| spl20_238 ),
inference(sat_conversion,[],[f1584]) ).
cnf(s176,plain,
( spl20_153
| spl20_209
| spl20_228
| spl20_237 ),
inference(sat_conversion,[],[f1585]) ).
cnf(s187,plain,
( spl20_155
| spl20_225
| spl20_230
| spl20_233 ),
inference(sat_conversion,[],[f1596]) ).
cnf(s192,plain,
( spl20_162
| spl20_236
| spl20_238
| spl20_240 ),
inference(sat_conversion,[],[f1601]) ).
cnf(s195,plain,
( spl20_157
| spl20_235
| spl20_237
| spl20_239 ),
inference(sat_conversion,[],[f1604]) ).
cnf(s197,plain,
( spl20_198
| spl20_241
| spl20_242
| spl20_243 ),
inference(sat_conversion,[],[f1618]) ).
cnf(s202,plain,
( spl20_202
| spl20_251
| spl20_252
| spl20_253 ),
inference(sat_conversion,[],[f1663]) ).
cnf(s203,plain,
( spl20_176
| spl20_204
| spl20_254
| spl20_255 ),
inference(sat_conversion,[],[f1672]) ).
cnf(s207,plain,
( spl20_181
| spl20_246
| spl20_263
| spl20_264 ),
inference(sat_conversion,[],[f1712]) ).
cnf(s208,plain,
( spl20_174
| spl20_181
| spl20_187
| spl20_193 ),
inference(sat_conversion,[],[f1713]) ).
cnf(s214,plain,
( spl20_178
| spl20_242
| spl20_259
| spl20_272 ),
inference(sat_conversion,[],[f1751]) ).
cnf(s216,plain,
( spl20_184
| spl20_244
| spl20_263
| spl20_274 ),
inference(sat_conversion,[],[f1761]) ).
cnf(s217,plain,
( spl20_188
| spl20_252
| spl20_266
| spl20_275 ),
inference(sat_conversion,[],[f1766]) ).
cnf(s218,plain,
( spl20_175
| spl20_182
| spl20_188
| spl20_194 ),
inference(sat_conversion,[],[f1767]) ).
cnf(s219,plain,
( spl20_189
| spl20_197
| spl20_257
| spl20_269 ),
inference(sat_conversion,[],[f1768]) ).
cnf(s221,plain,
( spl20_179
| spl20_203
| spl20_262
| spl20_272 ),
inference(sat_conversion,[],[f1774]) ).
cnf(s222,plain,
( spl20_179
| spl20_243
| spl20_260
| spl20_271 ),
inference(sat_conversion,[],[f1775]) ).
cnf(s223,plain,
( spl20_185
| spl20_193
| spl20_248
| spl20_274 ),
inference(sat_conversion,[],[f1776]) ).
cnf(s224,plain,
( spl20_185
| spl20_245
| spl20_264
| spl20_273 ),
inference(sat_conversion,[],[f1777]) ).
cnf(s227,plain,
( spl20_195
| spl20_258
| spl20_270
| spl20_276 ),
inference(sat_conversion,[],[f1780]) ).
cnf(s231,plain,
( spl20_201
| spl20_247
| spl20_252
| spl20_257 ),
inference(sat_conversion,[],[f1784]) ).
cnf(s235,plain,
( spl20_187
| spl20_261
| spl20_266
| spl20_269 ),
inference(sat_conversion,[],[f1788]) ).
cnf(s241,plain,
( spl20_176
| spl20_243
| spl20_245
| spl20_250 ),
inference(sat_conversion,[],[f1794]) ).
cnf(s243,plain,
( spl20_189
| spl20_271
| spl20_273
| spl20_275 ),
inference(sat_conversion,[],[f1796]) ).
cnf(s245,plain,
spl20_200,
inference(sat_conversion,[],[f1800]) ).
cnf(s246,plain,
spl20_168,
inference(sat_conversion,[],[f1801]) ).
cnf(s248,plain,
( ~ spl20_146
| ~ spl20_156 ),
inference(sat_conversion,[],[f1808]) ).
cnf(s250,plain,
( ~ spl20_147
| ~ spl20_159 ),
inference(sat_conversion,[],[f1815]) ).
cnf(s254,plain,
( ~ spl20_145
| ~ spl20_164 ),
inference(sat_conversion,[],[f1829]) ).
cnf(s256,plain,
( ~ spl20_146
| ~ spl20_165 ),
inference(sat_conversion,[],[f1836]) ).
cnf(s261,plain,
( ~ spl20_179
| ~ spl20_191 ),
inference(sat_conversion,[],[f1854]) ).
cnf(s263,plain,
( ~ spl20_191
| ~ spl20_195 ),
inference(sat_conversion,[],[f1861]) ).
cnf(s266,plain,
( ~ spl20_177
| ~ spl20_196 ),
inference(sat_conversion,[],[f1875]) ).
cnf(s268,plain,
( ~ spl20_188
| ~ spl20_197 ),
inference(sat_conversion,[],[f1882]) ).
cnf(s277,plain,
( ~ spl20_205
| ~ spl20_213 ),
inference(sat_conversion,[],[f1919]) ).
cnf(s288,plain,
( ~ spl20_146
| ~ spl20_152 ),
inference(sat_conversion,[],[f1964]) ).
cnf(s299,plain,
( ~ spl20_213
| ~ spl20_218 ),
inference(sat_conversion,[],[f2007]) ).
cnf(s309,plain,
( ~ spl20_169
| ~ spl20_216 ),
inference(sat_conversion,[],[f2054]) ).
cnf(s320,plain,
( ~ spl20_216
| ~ spl20_221 ),
inference(sat_conversion,[],[f2110]) ).
cnf(s324,plain,
( ~ spl20_162
| ~ spl20_238 ),
inference(sat_conversion,[],[f2134]) ).
cnf(s335,plain,
( ~ spl20_193
| ~ spl20_270 ),
inference(sat_conversion,[],[f2193]) ).
cnf(s340,plain,
( ~ spl20_249
| ~ spl20_254 ),
inference(sat_conversion,[],[f2212]) ).
cnf(s341,plain,
( ~ spl20_178
| ~ spl20_197 ),
inference(sat_conversion,[],[f2219]) ).
cnf(s345,plain,
( ~ spl20_177
| ~ spl20_181 ),
inference(sat_conversion,[],[f2231]) ).
cnf(s346,plain,
( ~ spl20_241
| ~ spl20_249 ),
inference(sat_conversion,[],[f2236]) ).
cnf(s356,plain,
( ~ spl20_185
| ~ spl20_191 ),
inference(sat_conversion,[],[f2288]) ).
cnf(s361,plain,
( ~ spl20_272
| ~ spl20_276 ),
inference(sat_conversion,[],[f2314]) ).
cnf(s370,plain,
( ~ spl20_200
| ~ spl20_246 ),
inference(sat_conversion,[],[f2346]) ).
cnf(s372,plain,
( ~ spl20_182
| ~ spl20_263 ),
inference(sat_conversion,[],[f2353]) ).
cnf(s376,plain,
( ~ spl20_175
| ~ spl20_242 ),
inference(sat_conversion,[],[f2366]) ).
cnf(s380,plain,
( ~ spl20_251
| ~ spl20_256 ),
inference(sat_conversion,[],[f2387]) ).
cnf(s387,plain,
( ~ spl20_187
| ~ spl20_269 ),
inference(sat_conversion,[],[f2431]) ).
cnf(s393,plain,
( ~ spl20_176
| ~ spl20_243 ),
inference(sat_conversion,[],[f2454]) ).
cnf(s394,plain,
( ~ spl20_260
| ~ spl20_264 ),
inference(sat_conversion,[],[f2463]) ).
cnf(s397,plain,
( ~ spl20_272
| ~ spl20_274 ),
inference(sat_conversion,[],[f2484]) ).
cnf(s400,plain,
( ~ spl20_166
| ~ spl20_168 ),
inference(sat_conversion,[],[f2496]) ).
cnf(s401,plain,
( ~ spl20_171
| ~ spl20_222 ),
inference(sat_conversion,[],[f2506]) ).
cnf(s410,plain,
( ~ spl20_143
| ~ spl20_206 ),
inference(sat_conversion,[],[f2524]) ).
cnf(s412,plain,
( ~ spl20_167
| ~ spl20_210 ),
inference(sat_conversion,[],[f2530]) ).
cnf(s428,plain,
( ~ spl20_168
| ~ spl20_170 ),
inference(sat_conversion,[],[f2636]) ).
cnf(s431,plain,
( ~ spl20_175
| ~ spl20_255 ),
inference(sat_conversion,[],[f2645]) ).
cnf(s433,plain,
( ~ spl20_273
| ~ spl20_275 ),
inference(sat_conversion,[],[f2667]) ).
cnf(s438,plain,
( ~ spl20_248
| ~ spl20_253 ),
inference(sat_conversion,[],[f2698]) ).
cnf(s439,plain,
( ~ spl20_204
| ~ spl20_256 ),
inference(sat_conversion,[],[f2705]) ).
cnf(s444,plain,
( ~ spl20_271
| ~ spl20_275 ),
inference(sat_conversion,[],[f2731]) ).
cnf(s445,plain,
( ~ spl20_184
| ~ spl20_197 ),
inference(sat_conversion,[],[f2735]) ).
cnf(s454,plain,
( ~ spl20_168
| ~ spl20_172 ),
inference(sat_conversion,[],[f2785]) ).
cnf(s459,plain,
( ~ spl20_156
| ~ spl20_165 ),
inference(sat_conversion,[],[f2804]) ).
cnf(s469,plain,
( ~ spl20_153
| ~ spl20_159 ),
inference(sat_conversion,[],[f2857]) ).
cnf(s471,plain,
( ~ spl20_159
| ~ spl20_163 ),
inference(sat_conversion,[],[f2865]) ).
cnf(s474,plain,
( ~ spl20_150
| ~ spl20_227 ),
inference(sat_conversion,[],[f2876]) ).
cnf(s481,plain,
( spl20_138
| ~ spl20_159 ),
inference(sat_conversion,[],[f2934]) ).
cnf(s505,plain,
( ~ spl20_198
| ~ spl20_200 ),
inference(sat_conversion,[],[f3120]) ).
cnf(s506,plain,
( ~ spl20_73
| spl20_74
| ~ spl20_138
| ~ spl20_159
| ~ spl20_200 ),
inference(sat_conversion,[],[f3122]) ).
cnf(s510,plain,
( ~ spl20_200
| ~ spl20_247 ),
inference(sat_conversion,[],[f3130]) ).
cnf(s513,plain,
( ~ spl20_200
| spl20_249 ),
inference(sat_conversion,[],[f3302]) ).
cnf(s516,plain,
( ~ spl20_178
| ~ spl20_201 ),
inference(sat_conversion,[],[f3307]) ).
cnf(s518,plain,
( ~ spl20_200
| ~ spl20_244 ),
inference(sat_conversion,[],[f3311]) ).
cnf(s519,plain,
( ~ spl20_191
| ~ spl20_194 ),
inference(sat_conversion,[],[f3314]) ).
cnf(s521,plain,
( ~ spl20_249
| ~ spl20_266 ),
inference(sat_conversion,[],[f3316]) ).
cnf(s526,plain,
( ~ spl20_200
| ~ spl20_245 ),
inference(sat_conversion,[],[f3321]) ).
cnf(s529,plain,
( ~ spl20_242
| ~ spl20_243 ),
inference(sat_conversion,[],[f3325]) ).
cnf(s530,plain,
( ~ spl20_243
| ~ spl20_271 ),
inference(sat_conversion,[],[f3326]) ).
cnf(s531,plain,
( ~ spl20_256
| ~ spl20_258 ),
inference(sat_conversion,[],[f3328]) ).
cnf(s532,plain,
( ~ spl20_256
| ~ spl20_257 ),
inference(sat_conversion,[],[f3330]) ).
cnf(s535,plain,
( ~ spl20_181
| ~ spl20_196 ),
inference(sat_conversion,[],[f3345]) ).
cnf(s536,plain,
( ~ spl20_177
| ~ spl20_261 ),
inference(sat_conversion,[],[f3346]) ).
cnf(s537,plain,
( ~ spl20_177
| ~ spl20_262 ),
inference(sat_conversion,[],[f3347]) ).
cnf(s538,plain,
( ~ spl20_177
| ~ spl20_259 ),
inference(sat_conversion,[],[f3348]) ).
cnf(s541,plain,
( ~ spl20_197
| ~ spl20_276 ),
inference(sat_conversion,[],[f3349]) ).
cnf(s546,plain,
( ~ spl20_200
| ~ spl20_202 ),
inference(sat_conversion,[],[f3418]) ).
cnf(s548,plain,
( ~ spl20_207
| ~ spl20_235 ),
inference(sat_conversion,[],[f3485]) ).
cnf(s549,plain,
( ~ spl20_168
| spl20_213 ),
inference(sat_conversion,[],[f3495]) ).
cnf(s550,plain,
( ~ spl20_168
| ~ spl20_212 ),
inference(sat_conversion,[],[f3496]) ).
cnf(s553,plain,
( ~ spl20_159
| ~ spl20_239 ),
inference(sat_conversion,[],[f3506]) ).
cnf(s554,plain,
( ~ spl20_165
| ~ spl20_233 ),
inference(sat_conversion,[],[f3507]) ).
cnf(s556,plain,
( ~ spl20_171
| ~ spl20_236 ),
inference(sat_conversion,[],[f3509]) ).
cnf(s557,plain,
( ~ spl20_145
| ~ spl20_167 ),
inference(sat_conversion,[],[f3510]) ).
cnf(s561,plain,
( ~ spl20_165
| ~ spl20_219 ),
inference(sat_conversion,[],[f3514]) ).
cnf(s564,plain,
( ~ spl20_165
| ~ spl20_240 ),
inference(sat_conversion,[],[f3517]) ).
cnf(s565,plain,
( ~ spl20_168
| ~ spl20_209 ),
inference(sat_conversion,[],[f3520]) ).
cnf(s568,plain,
( spl20_135
| ~ spl20_159
| ~ spl20_238 ),
inference(sat_conversion,[],[f3597]) ).
cnf(s569,plain,
( spl20_132
| ~ spl20_159
| ~ spl20_235 ),
inference(sat_conversion,[],[f3600]) ).
cnf(s570,plain,
( spl20_87
| ~ spl20_132
| ~ spl20_138
| ~ spl20_216
| ~ spl20_264 ),
inference(sat_conversion,[],[f3603]) ).
cnf(s571,plain,
( ~ spl20_73
| spl20_75
| ~ spl20_132
| ~ spl20_138
| ~ spl20_235
| ~ spl20_256 ),
inference(sat_conversion,[],[f3613]) ).
cnf(s573,plain,
( ~ spl20_73
| spl20_77
| ~ spl20_132
| ~ spl20_144
| ~ spl20_203 ),
inference(sat_conversion,[],[f3632]) ).
cnf(s574,plain,
( ~ spl20_73
| spl20_78
| ~ spl20_135
| ~ spl20_138
| ~ spl20_238
| ~ spl20_249 ),
inference(sat_conversion,[],[f3642]) ).
cnf(s575,plain,
( ~ spl20_73
| spl20_79
| ~ spl20_138
| ~ spl20_165
| ~ spl20_177 ),
inference(sat_conversion,[],[f3651]) ).
cnf(s576,plain,
( spl20_80
| ~ spl20_135
| ~ spl20_138
| ~ spl20_150
| ~ spl20_187 ),
inference(sat_conversion,[],[f3660]) ).
cnf(s577,plain,
( spl20_81
| ~ spl20_132
| ~ spl20_138
| ~ spl20_206
| ~ spl20_270 ),
inference(sat_conversion,[],[f3670]) ).
cnf(s578,plain,
( ~ spl20_73
| spl20_82
| ~ spl20_135
| ~ spl20_234
| ~ spl20_242 ),
inference(sat_conversion,[],[f3680]) ).
cnf(s580,plain,
( spl20_84
| ~ spl20_132
| ~ spl20_135
| ~ spl20_145
| ~ spl20_197 ),
inference(sat_conversion,[],[f3699]) ).
cnf(s581,plain,
( spl20_85
| ~ spl20_132
| ~ spl20_135
| ~ spl20_138
| ~ spl20_213
| ~ spl20_274 ),
inference(sat_conversion,[],[f3708]) ).
cnf(s582,plain,
( ~ spl20_73
| spl20_86
| ~ spl20_132
| ~ spl20_171
| ~ spl20_176 ),
inference(sat_conversion,[],[f3718]) ).
cnf(s583,plain,
( ~ spl20_73
| spl20_88
| ~ spl20_132
| ~ spl20_135
| ~ spl20_220
| ~ spl20_271 ),
inference(sat_conversion,[],[f3728]) ).
cnf(s584,plain,
( spl20_89
| ~ spl20_132
| ~ spl20_135
| ~ spl20_168
| ~ spl20_191 ),
inference(sat_conversion,[],[f3737]) ).
cnf(s588,plain,
( ~ spl20_145
| ~ spl20_225 ),
inference(sat_conversion,[],[f3744]) ).
cnf(s590,plain,
( ~ spl20_213
| ~ spl20_230 ),
inference(sat_conversion,[],[f3746]) ).
cnf(s595,plain,
( ~ spl20_73
| spl20_76
| ~ spl20_135
| ~ spl20_228
| ~ spl20_252 ),
inference(sat_conversion,[],[f3769]) ).
cnf(s596,plain,
( spl20_83
| ~ spl20_135
| ~ spl20_138
| ~ spl20_155
| ~ spl20_182 ),
inference(sat_conversion,[],[f3773]) ).
cnf(s603,plain,
( ~ spl20_146
| ~ spl20_206 ),
inference(sat_conversion,[],[f3793]) ).
cnf(s606,plain,
( ~ spl20_158
| ~ spl20_213 ),
inference(sat_conversion,[],[f3796]) ).
cnf(s607,plain,
( ~ spl20_164
| ~ spl20_220 ),
inference(sat_conversion,[],[f3797]) ).
cnf(s619,plain,
( ~ spl20_155
| ~ spl20_237 ),
inference(sat_conversion,[],[f3821]) ).
cnf(s622,plain,
( ~ spl20_228
| ~ spl20_237 ),
inference(sat_conversion,[],[f3826]) ).
cnf(s625,plain,
( ~ spl20_179
| ~ spl20_243 ),
inference(sat_conversion,[],[f3829]) ).
cnf(s630,plain,
( ~ spl20_264
| ~ spl20_273 ),
inference(sat_conversion,[],[f3833]) ).
cnf(s631,plain,
( ~ spl20_252
| ~ spl20_275 ),
inference(sat_conversion,[],[f3834]) ).
cnf(s632,plain,
( ~ spl20_200
| spl20_256 ),
inference(sat_conversion,[],[f3838]) ).
cnf(s636,plain,
( ~ spl20_188
| ~ spl20_252 ),
inference(sat_conversion,[],[f3844]) ).
cnf(s640,plain,
( ~ spl20_190
| ~ spl20_249 ),
inference(sat_conversion,[],[f3849]) ).
cnf(s641,plain,
( ~ spl20_249
| ~ spl20_250 ),
inference(sat_conversion,[],[f3854]) ).
cnf(s642,plain,
( ~ spl20_174
| ~ spl20_249 ),
inference(sat_conversion,[],[f3868]) ).
cnf(s643,plain,
( ~ spl20_269
| ~ spl20_270 ),
inference(sat_conversion,[],[f3869]) ).
cnf(s654,plain,
~ spl20_209,
inference(rat,[],[s565,s246]) ).
cnf(s656,plain,
~ spl20_212,
inference(rat,[],[s550,s246]) ).
cnf(s657,plain,
spl20_213,
inference(rat,[],[s549,s246]) ).
cnf(s658,plain,
~ spl20_172,
inference(rat,[],[s454,s246]) ).
cnf(s659,plain,
~ spl20_170,
inference(rat,[],[s428,s246]) ).
cnf(s662,plain,
~ spl20_166,
inference(rat,[],[s400,s246]) ).
cnf(s663,plain,
~ spl20_158,
inference(rat,[],[s606,s657]) ).
cnf(s664,plain,
~ spl20_230,
inference(rat,[],[s590,s657]) ).
cnf(s665,plain,
~ spl20_218,
inference(rat,[],[s299,s657]) ).
cnf(s666,plain,
~ spl20_205,
inference(rat,[],[s277,s657]) ).
cnf(s668,plain,
spl20_256,
inference(rat,[],[s632,s245]) ).
cnf(s669,plain,
~ spl20_202,
inference(rat,[],[s546,s245]) ).
cnf(s670,plain,
~ spl20_245,
inference(rat,[],[s526,s245]) ).
cnf(s671,plain,
~ spl20_244,
inference(rat,[],[s518,s245]) ).
cnf(s672,plain,
spl20_249,
inference(rat,[],[s513,s245]) ).
cnf(s673,plain,
~ spl20_247,
inference(rat,[],[s510,s245]) ).
cnf(s674,plain,
~ spl20_198,
inference(rat,[],[s505,s245]) ).
cnf(s675,plain,
~ spl20_246,
inference(rat,[],[s370,s245]) ).
cnf(s676,plain,
~ spl20_257,
inference(rat,[],[s532,s668]) ).
cnf(s677,plain,
~ spl20_258,
inference(rat,[],[s531,s668]) ).
cnf(s678,plain,
~ spl20_204,
inference(rat,[],[s439,s668]) ).
cnf(s679,plain,
~ spl20_251,
inference(rat,[],[s380,s668]) ).
cnf(s680,plain,
~ spl20_174,
inference(rat,[],[s642,s672]) ).
cnf(s681,plain,
~ spl20_250,
inference(rat,[],[s641,s672]) ).
cnf(s682,plain,
~ spl20_190,
inference(rat,[],[s640,s672]) ).
cnf(s683,plain,
~ spl20_266,
inference(rat,[],[s521,s672]) ).
cnf(s684,plain,
~ spl20_241,
inference(rat,[],[s346,s672]) ).
cnf(s685,plain,
~ spl20_254,
inference(rat,[],[s340,s672]) ).
cnf(s686,plain,
( spl20_176
| spl20_243 ),
inference(rat,[],[s241,s681,s670]) ).
cnf(s688,plain,
( spl20_187
| spl20_261
| spl20_269 ),
inference(rat,[],[s235,s683]) ).
cnf(s691,plain,
( spl20_201
| spl20_252 ),
inference(rat,[],[s231,s676,s673]) ).
cnf(s692,plain,
( spl20_195
| spl20_270
| spl20_276 ),
inference(rat,[],[s227,s677]) ).
cnf(s694,plain,
( spl20_185
| spl20_264
| spl20_273 ),
inference(rat,[],[s224,s670]) ).
cnf(s695,plain,
( spl20_189
| spl20_197
| spl20_269 ),
inference(rat,[],[s219,s676]) ).
cnf(s696,plain,
( spl20_188
| spl20_252
| spl20_275 ),
inference(rat,[],[s217,s683]) ).
cnf(s697,plain,
( spl20_184
| spl20_263
| spl20_274 ),
inference(rat,[],[s216,s671]) ).
cnf(s701,plain,
( spl20_181
| spl20_187
| spl20_193 ),
inference(rat,[],[s208,s680]) ).
cnf(s702,plain,
( spl20_181
| spl20_263
| spl20_264 ),
inference(rat,[],[s207,s675]) ).
cnf(s704,plain,
( spl20_176
| spl20_255 ),
inference(rat,[],[s203,s685,s678]) ).
cnf(s705,plain,
( spl20_252
| spl20_253 ),
inference(rat,[],[s202,s679,s669]) ).
cnf(s707,plain,
( spl20_242
| spl20_243 ),
inference(rat,[],[s197,s684,s674]) ).
cnf(s710,plain,
( spl20_155
| spl20_225
| spl20_233 ),
inference(rat,[],[s187,s664]) ).
cnf(s713,plain,
( spl20_153
| spl20_228
| spl20_237 ),
inference(rat,[],[s176,s654]) ).
cnf(s714,plain,
( spl20_153
| spl20_161
| spl20_238 ),
inference(rat,[],[s175,s656]) ).
cnf(s715,plain,
( spl20_156
| spl20_216
| spl20_239 ),
inference(rat,[],[s169,s664]) ).
cnf(s717,plain,
( spl20_164
| spl20_233
| spl20_234 ),
inference(rat,[],[s164,s665]) ).
cnf(s720,plain,
( spl20_220
| spl20_221
| spl20_222 ),
inference(rat,[],[s156,s658]) ).
cnf(s721,plain,
( spl20_144
| spl20_219 ),
inference(rat,[],[s155,s665,s658]) ).
cnf(s723,plain,
( spl20_167
| spl20_169
| spl20_171 ),
inference(rat,[],[s150,s662]) ).
cnf(s724,plain,
( spl20_206
| spl20_207 ),
inference(rat,[],[s149,s666,s662]) ).
cnf(s725,plain,
~ spl20_192,
inference(rat,[],[s148,s678]) ).
cnf(s726,plain,
~ spl20_186,
inference(rat,[],[s146,s669]) ).
cnf(s727,plain,
~ spl20_173,
inference(rat,[],[s142,s674]) ).
cnf(s728,plain,
( spl20_195
| spl20_196
| spl20_197 ),
inference(rat,[],[s140,s725]) ).
cnf(s729,plain,
( ~ spl20_193
| spl20_195
| spl20_197 ),
inference(rat,[],[s139,s725]) ).
cnf(s736,plain,
( spl20_188
| spl20_191 ),
inference(rat,[],[s132,s682,s726]) ).
cnf(s738,plain,
( ~ spl20_188
| spl20_191 ),
inference(rat,[],[s130,s682,s726]) ).
cnf(s740,plain,
( spl20_188
| ~ spl20_189 ),
inference(rat,[],[s128,s682,s726]) ).
cnf(s744,plain,
( spl20_177
| spl20_178
| spl20_179 ),
inference(rat,[],[s116,s727]) ).
cnf(s746,plain,
( ~ spl20_176
| spl20_177
| spl20_178 ),
inference(rat,[],[s112,s727]) ).
cnf(s748,plain,
~ spl20_160,
inference(rat,[],[s108,s658]) ).
cnf(s749,plain,
~ spl20_154,
inference(rat,[],[s106,s659]) ).
cnf(s750,plain,
~ spl20_141,
inference(rat,[],[s102,s662]) ).
cnf(s751,plain,
( spl20_163
| spl20_164
| spl20_165 ),
inference(rat,[],[s100,s748]) ).
cnf(s752,plain,
( ~ spl20_161
| spl20_163
| spl20_165 ),
inference(rat,[],[s99,s748]) ).
cnf(s753,plain,
( ~ spl20_162
| spl20_163
| spl20_164 ),
inference(rat,[],[s98,s748]) ).
cnf(s759,plain,
( spl20_156
| spl20_159 ),
inference(rat,[],[s92,s663,s749]) ).
cnf(s761,plain,
( ~ spl20_156
| spl20_159 ),
inference(rat,[],[s90,s663,s749]) ).
cnf(s763,plain,
( spl20_156
| ~ spl20_157 ),
inference(rat,[],[s88,s663,s749]) ).
cnf(s767,plain,
( spl20_145
| spl20_146
| spl20_147 ),
inference(rat,[],[s76,s750]) ).
cnf(s769,plain,
( ~ spl20_143
| spl20_145
| spl20_147 ),
inference(rat,[],[s74,s750]) ).
cnf(s779,plain,
( spl20_70
| spl20_71
| spl20_72
| ~ spl20_74
| ~ spl20_75
| ~ spl20_76
| ~ spl20_77
| ~ spl20_78
| ~ spl20_79
| ~ spl20_80
| ~ spl20_81
| ~ spl20_82
| ~ spl20_83
| ~ spl20_84
| ~ spl20_85
| ~ spl20_86
| ~ spl20_87
| ~ spl20_88
| ~ spl20_89 ),
inference(rat,[],[s13,s68]) ).
cnf(s792,plain,
( ~ spl20_159
| spl20_74 ),
inference(rat,[],[s506,s481,s68,s245]) ).
cnf(s793,plain,
spl20_159,
inference(rat,[],[s761,s759]) ).
cnf(s797,plain,
~ spl20_239,
inference(rat,[],[s553,s793]) ).
cnf(s798,plain,
spl20_138,
inference(rat,[],[s481,s793]) ).
cnf(s799,plain,
~ spl20_163,
inference(rat,[],[s471,s793]) ).
cnf(s800,plain,
~ spl20_153,
inference(rat,[],[s469,s793]) ).
cnf(s801,plain,
~ spl20_147,
inference(rat,[],[s250,s793]) ).
cnf(s802,plain,
spl20_74,
inference(rat,[],[s792,s793]) ).
cnf(s804,plain,
spl20_165,
inference(rat,[],[s83,s159,s103,s412,s723,s401,s622,s720,s195,s309,s320,s548,s474,s715,s763,s724,s170,s248,s288,s603,s324,s769,s767,s714,s254,s607,s752,s751,s800,s797,s801,s799]) ).
cnf(s805,plain,
~ spl20_72,
inference(rat,[],[s62,s798]) ).
cnf(s806,plain,
~ spl20_240,
inference(rat,[],[s564,s804]) ).
cnf(s807,plain,
~ spl20_219,
inference(rat,[],[s561,s804]) ).
cnf(s809,plain,
~ spl20_233,
inference(rat,[],[s554,s804]) ).
cnf(s810,plain,
~ spl20_156,
inference(rat,[],[s459,s804]) ).
cnf(s813,plain,
~ spl20_146,
inference(rat,[],[s256,s804]) ).
cnf(s815,plain,
spl20_144,
inference(rat,[],[s721,s807]) ).
cnf(s817,plain,
spl20_216,
inference(rat,[],[s715,s797,s810]) ).
cnf(s819,plain,
spl20_145,
inference(rat,[],[s767,s801,s813]) ).
cnf(s821,plain,
~ spl20_221,
inference(rat,[],[s320,s817]) ).
cnf(s822,plain,
~ spl20_169,
inference(rat,[],[s309,s817]) ).
cnf(s825,plain,
~ spl20_225,
inference(rat,[],[s588,s819]) ).
cnf(s826,plain,
~ spl20_167,
inference(rat,[],[s557,s819]) ).
cnf(s829,plain,
~ spl20_164,
inference(rat,[],[s254,s819]) ).
cnf(s830,plain,
spl20_155,
inference(rat,[],[s710,s809,s825]) ).
cnf(s831,plain,
spl20_235,
inference(rat,[],[s165,s822,s813,s825]) ).
cnf(s832,plain,
spl20_171,
inference(rat,[],[s723,s822,s826]) ).
cnf(s833,plain,
spl20_234,
inference(rat,[],[s717,s809,s829]) ).
cnf(s834,plain,
~ spl20_162,
inference(rat,[],[s753,s799,s829]) ).
cnf(s835,plain,
~ spl20_237,
inference(rat,[],[s619,s830]) ).
cnf(s836,plain,
~ spl20_207,
inference(rat,[],[s548,s831]) ).
cnf(s837,plain,
spl20_132,
inference(rat,[],[s569,s793,s831]) ).
cnf(s838,plain,
~ spl20_236,
inference(rat,[],[s556,s832]) ).
cnf(s840,plain,
~ spl20_222,
inference(rat,[],[s401,s832]) ).
cnf(s842,plain,
spl20_228,
inference(rat,[],[s713,s800,s835]) ).
cnf(s843,plain,
spl20_206,
inference(rat,[],[s724,s836]) ).
cnf(s844,plain,
spl20_75,
inference(rat,[],[s571,s668,s831,s798,s68,s837]) ).
cnf(s845,plain,
~ spl20_70,
inference(rat,[],[s56,s837]) ).
cnf(s846,plain,
spl20_238,
inference(rat,[],[s192,s806,s834,s838]) ).
cnf(s847,plain,
spl20_220,
inference(rat,[],[s720,s821,s840]) ).
cnf(s849,plain,
~ spl20_143,
inference(rat,[],[s410,s843]) ).
cnf(s850,plain,
spl20_135,
inference(rat,[],[s568,s793,s846]) ).
cnf(s853,plain,
spl20_150,
inference(rat,[],[s170,s834,s810,s849]) ).
cnf(s854,plain,
spl20_78,
inference(rat,[],[s574,s672,s846,s798,s68,s850]) ).
cnf(s855,plain,
~ spl20_71,
inference(rat,[],[s59,s850]) ).
cnf(s858,plain,
( spl20_177
| spl20_178 ),
inference(rat,[],[s686,s625,s746,s744]) ).
cnf(s859,plain,
spl20_191,
inference(rat,[],[s738,s736]) ).
cnf(s861,plain,
~ spl20_185,
inference(rat,[],[s356,s859]) ).
cnf(s862,plain,
~ spl20_195,
inference(rat,[],[s263,s859]) ).
cnf(s863,plain,
spl20_89,
inference(rat,[],[s584,s850,s246,s837,s859]) ).
cnf(s864,plain,
( ~ spl20_272
| spl20_248 ),
inference(rat,[],[s335,s692,s223,s361,s397,s862,s861]) ).
cnf(s865,plain,
~ spl20_194,
inference(rat,[],[s519,s859]) ).
cnf(s866,plain,
~ spl20_179,
inference(rat,[],[s261,s859]) ).
cnf(s867,plain,
spl20_252,
inference(rat,[],[s394,s694,s222,s433,s444,s529,s696,s214,s268,s864,s728,s266,s538,s858,s438,s516,s705,s691,s861,s866,s862]) ).
cnf(s868,plain,
~ spl20_188,
inference(rat,[],[s636,s867]) ).
cnf(s870,plain,
~ spl20_275,
inference(rat,[],[s631,s867]) ).
cnf(s871,plain,
spl20_76,
inference(rat,[],[s595,s850,s842,s68,s867]) ).
cnf(s872,plain,
~ spl20_189,
inference(rat,[],[s740,s868]) ).
cnf(s873,plain,
( ~ spl20_243
| spl20_181 ),
inference(rat,[],[s372,s218,s702,s431,s630,s704,s243,s393,s530,s868,s865,s872,s870]) ).
cnf(s874,plain,
~ spl20_177,
inference(rat,[],[s779,s583,s573,s243,s221,s570,s630,s581,s397,s702,s697,s596,s372,s218,s578,s376,s582,s707,s686,s873,s576,s688,s577,s643,s692,s580,s445,s541,s728,s575,s266,s345,s536,s537,s845,s855,s805,s802,s844,s854,s871,s863,s68,s837,s847,s850,s815,s872,s870,s866,s798,s817,s657,s830,s868,s865,s833,s832,s853,s843,s862,s819,s804]) ).
cnf(s875,plain,
spl20_178,
inference(rat,[],[s858,s874]) ).
cnf(s879,plain,
~ spl20_197,
inference(rat,[],[s341,s875]) ).
cnf(s881,plain,
spl20_196,
inference(rat,[],[s728,s862,s879]) ).
cnf(s882,plain,
spl20_269,
inference(rat,[],[s695,s872,s879]) ).
cnf(s883,plain,
~ spl20_193,
inference(rat,[],[s729,s862,s879]) ).
cnf(s889,plain,
~ spl20_181,
inference(rat,[],[s535,s881]) ).
cnf(s891,plain,
~ spl20_187,
inference(rat,[],[s387,s882]) ).
cnf(s892,plain,
$false,
inference(rat,[],[s701,s889,s891,s883]) ).
fof(f3881,plain,
$false,
inference(avatar_sat_refutation,[],[s892]) ).
%------------------------------------------------------------------------------
%----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 THM
% 0.08/0.18 % Computer : n003.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 19:32:13 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.70/1.16 % (1899490)Detected formulas, will run a generic FOF schedule.
% 3.70/1.16 % (1899497)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1310799153:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.70/1.16 % (1899496)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1541698395:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.70/1.16 % (1899495)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3408939936:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.70/1.16 % (1899501)dis-21_1_sil=8000:lcm=predicate:random_seed=47787439:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.70/1.16 % (1899498)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1360577084:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.70/1.16 % (1899499)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1641538459:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.70/1.16 % (1899500)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1941598547:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.70/1.16 % (1899501)Refutation not found, incomplete strategy
% 3.70/1.16 % (1899501)------------------------------
% 3.70/1.16 % (1899501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.70/1.16 % (1899501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/1.16 % (1899501)CaDiCaL version: 2.1.3
% 3.70/1.16 % (1899501)Termination reason: Refutation not found, incomplete strategy
% 3.70/1.16 % (1899501)Time elapsed: 0.017 s
% 3.70/1.16 % (1899501)Peak memory usage: 89 MB
% 3.70/1.16 % (1899501)Instructions burned: 33 (million)
% 3.70/1.16 % (1899499)Instruction limit reached!
% 3.70/1.16 % (1899499)------------------------------
% 3.70/1.16 % (1899499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.70/1.16 % (1899499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/1.16 % (1899499)CaDiCaL version: 2.1.3
% 3.70/1.16 % (1899499)Termination reason: Instruction limit
% 3.70/1.16 % (1899499)Termination phase: Saturation
% 3.70/1.16 % (1899499)Time elapsed: 0.049 s
% 3.70/1.16 % (1899499)Peak memory usage: 88 MB
% 3.70/1.16 % (1899499)Instructions burned: 119 (million)
% 3.70/1.16 % (1899498)Instruction limit reached!
% 3.70/1.16 % (1899498)------------------------------
% 3.70/1.16 % (1899498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.70/1.16 % (1899498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/1.16 % (1899498)CaDiCaL version: 2.1.3
% 3.70/1.16 % (1899498)Termination reason: Instruction limit
% 3.70/1.16 % (1899498)Termination phase: Saturation
% 3.70/1.16 % (1899498)Time elapsed: 0.050 s
% 3.70/1.16 % (1899498)Peak memory usage: 90 MB
% 3.70/1.16 % (1899498)Instructions burned: 110 (million)
% 3.70/1.16 % (1899500)First to succeed.
% 3.70/1.16 % (1899500)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1899490"
% 3.70/1.16 [W928 19:32:14.313513302 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.70/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.70/1.16 [W928 19:32:14.313550289 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.70/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.70/1.16 [W928 19:32:14.313570515 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.70/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.70/1.16 [W928 19:32:14.313577525 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.70/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.70/1.16 [W928 19:32:14.313590834 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.70/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.70/1.16 [W928 19:32:14.313609530 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.70/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.70/1.16 % (1899510)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3456805843:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.70/1.16 % (1899509)lrs+10_1_sil=8000:sp=occurrence:random_seed=2371869060:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.70/1.16 % (1899501)------------------------------
% 3.70/1.16 % (1899501)------------------------------
% 3.70/1.16 % (1899509)Also succeeded, but the first one will report.
% 3.70/1.16 % (1899510)Instruction limit reached!
% 3.70/1.16 % (1899510)------------------------------
% 3.70/1.16 % (1899510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.70/1.16 % (1899510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/1.16 % (1899510)CaDiCaL version: 2.1.3
% 3.70/1.16 % (1899510)Termination reason: Instruction limit
% 3.70/1.16 % (1899510)Termination phase: Saturation
% 3.70/1.16 % (1899510)Time elapsed: 0.078 s
% 3.70/1.16 % (1899510)Peak memory usage: 90 MB
% 3.70/1.16 % (1899510)Instructions burned: 157 (million)
% 3.70/1.16 % (1899500)Refutation found. Thanks to Tanya!
% 3.70/1.16 % SZS status Theorem for theBenchmark
% 3.70/1.16 % SZS output start Proof for theBenchmark
% See solution above
% 4.13/1.35 % (1899500)------------------------------
% 4.13/1.35 % (1899500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.13/1.35 % (1899500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/1.35 % (1899500)CaDiCaL version: 2.1.3
% 4.13/1.35 % (1899500)Termination reason: Refutation
% 4.13/1.35 % (1899500)Time elapsed: 0.086 s
% 4.13/1.35 % (1899500)Peak memory usage: 91 MB
% 4.13/1.35 % (1899500)Instructions burned: 166 (million)
% 4.13/1.35 % (1899500)------------------------------
% 4.13/1.35 % (1899500)------------------------------
% 4.13/1.35 % (1899490)Success in time 0.503 s
% 4.13/1.35 % Vampire exiting
%------------------------------------------------------------------------------