%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG114+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 : n004.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:11 AM UTC 2026
% Result : Theorem 3.18s 1.11s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 155
% Syntax : Number of formulae : 892 ( 174 unt; 141 def)
% Number of atoms : 3346 (1675 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 4033 (1579 ~;1784 |; 549 &)
% ( 121 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 143 ( 141 usr; 142 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(e10,e10) != e11 )
| ( op1(e12,e12) = e10
& op1(e10,e10) != e12 )
| ( op1(e13,e13) = e10
& op1(e10,e10) != e13 ) )
& ( ( op1(e10,e10) = e11
& op1(e11,e11) != e10 )
| ( op1(e11,e11) = e11
& op1(e11,e11) != e11 )
| ( op1(e12,e12) = e11
& op1(e11,e11) != e12 )
| ( op1(e13,e13) = e11
& op1(e11,e11) != e13 ) )
& ( ( op1(e10,e10) = e12
& op1(e12,e12) != e10 )
| ( op1(e11,e11) = e12
& op1(e12,e12) != e11 )
| ( op1(e12,e12) = e12
& op1(e12,e12) != e12 )
| ( op1(e13,e13) = e12
& op1(e12,e12) != e13 ) )
& ( ( op1(e10,e10) = e13
& op1(e13,e13) != e10 )
| ( op1(e11,e11) = e13
& op1(e13,e13) != e11 )
| ( op1(e12,e12) = e13
& op1(e13,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(e20,e20) != e21 )
| ( op2(e22,e22) = e20
& op2(e20,e20) != e22 )
| ( op2(e23,e23) = e20
& op2(e20,e20) != e23 ) )
& ( ( op2(e20,e20) = e21
& op2(e21,e21) != e20 )
| ( op2(e21,e21) = e21
& op2(e21,e21) != e21 )
| ( op2(e22,e22) = e21
& op2(e21,e21) != e22 )
| ( op2(e23,e23) = e21
& op2(e21,e21) != e23 ) )
& ( ( op2(e20,e20) = e22
& op2(e22,e22) != e20 )
| ( op2(e21,e21) = e22
& op2(e22,e22) != e21 )
| ( op2(e22,e22) = e22
& op2(e22,e22) != e22 )
| ( op2(e23,e23) = e22
& op2(e22,e22) != e23 ) )
& ( ( op2(e20,e20) = e23
& op2(e23,e23) != e20 )
| ( op2(e21,e21) = e23
& op2(e23,e23) != e21 )
| ( op2(e22,e22) = e23
& op2(e23,e23) != e22 )
| ( op2(e23,e23) = e23
& op2(e23,e23) != e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e10 = op1(op1(e12,e12),e12)
& e11 = op1(op1(e12,e12),op1(e12,e12))
& e13 = op1(e12,e12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e20 = op2(op2(e22,e22),e22)
& e21 = op2(op2(e22,e22),op2(e22,e22))
& e23 = op2(e22,e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f16,axiom,
( h3(e12) = e22
& h3(e10) = op2(op2(e22,e22),e22)
& h3(e11) = op2(op2(e22,e22),op2(e22,e22))
& h3(e13) = op2(e22,e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f18,conjecture,
( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f19,negated_conjecture,
~ ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f20,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) ) )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) ) )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) ) )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) ) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f21,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(e12,e12) != e13 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( op1(e13,e13) = e11
& op1(e11,e11) != e13 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( op1(e13,e13) = e10
& op1(e10,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(e10,e10) != e11 )
| ( op1(e12,e12) = e10
& op1(e10,e10) != e12 )
| sP3 )
& ( ( op1(e10,e10) = e11
& op1(e11,e11) != e10 )
| ( op1(e11,e11) = e11
& op1(e11,e11) != e11 )
| ( op1(e12,e12) = e11
& op1(e11,e11) != e12 )
| sP2 )
& ( ( op1(e10,e10) = e12
& op1(e12,e12) != e10 )
| ( op1(e11,e11) = e12
& op1(e12,e12) != e11 )
| ( op1(e12,e12) = e12
& op1(e12,e12) != e12 )
| sP1 )
& ( ( op1(e10,e10) = e13
& op1(e13,e13) != e10 )
| ( op1(e11,e11) = e13
& op1(e13,e13) != e11 )
| ( op1(e12,e12) = e13
& op1(e13,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(e22,e22) != e23 )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( op2(e23,e23) = e21
& op2(e21,e21) != e23 )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f29,definition,
( ( op2(e23,e23) = e20
& op2(e20,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(e20,e20) != e21 )
| ( op2(e22,e22) = e20
& op2(e20,e20) != e22 )
| sP7 )
& ( ( op2(e20,e20) = e21
& op2(e21,e21) != e20 )
| ( op2(e21,e21) = e21
& op2(e21,e21) != e21 )
| ( op2(e22,e22) = e21
& op2(e21,e21) != e22 )
| sP6 )
& ( ( op2(e20,e20) = e22
& op2(e22,e22) != e20 )
| ( op2(e21,e21) = e22
& op2(e22,e22) != e21 )
| ( op2(e22,e22) = e22
& op2(e22,e22) != e22 )
| sP5 )
& ( ( op2(e20,e20) = e23
& op2(e23,e23) != e20 )
| ( op2(e21,e21) = e23
& op2(e23,e23) != e21 )
| ( op2(e22,e22) = e23
& op2(e23,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(e10,e10) != e13 )
| ~ sP3 ),
inference(nnf_transformation,[],[f24]) ).
fof(f46,plain,
( ( op1(e13,e13) = e12
& op1(e12,e12) != e13 )
| ~ sP1 ),
inference(nnf_transformation,[],[f22]) ).
fof(f47,plain,
( ( op1(e13,e13) = e13
& op1(e13,e13) != e13 )
| ~ sP0 ),
inference(nnf_transformation,[],[f21]) ).
fof(f48,plain,
( ( op2(e23,e23) = e20
& op2(e20,e20) != e23 )
| ~ sP7 ),
inference(nnf_transformation,[],[f29]) ).
fof(f49,plain,
( ( op2(e23,e23) = e21
& op2(e21,e21) != e23 )
| ~ sP6 ),
inference(nnf_transformation,[],[f28]) ).
fof(f50,plain,
( ( op2(e23,e23) = e22
& op2(e22,e22) != e23 )
| ~ sP5 ),
inference(nnf_transformation,[],[f27]) ).
fof(f51,plain,
( ( op2(e23,e23) = e23
& op2(e23,e23) != e23 )
| ~ sP4 ),
inference(nnf_transformation,[],[f26]) ).
fof(f58,plain,
( ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ~ sP13 ),
inference(nnf_transformation,[],[f36]) ).
fof(f59,plain,
( ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ~ sP12 ),
inference(nnf_transformation,[],[f35]) ).
fof(f60,plain,
( ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) )
| ~ sP11 ),
inference(nnf_transformation,[],[f34]) ).
fof(f67,plain,
( e10 = op1(e13,e10)
| e11 = op1(e13,e10)
| e12 = op1(e13,e10)
| e13 = op1(e13,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f72,plain,
( e10 = op1(e11,e13)
| e11 = op1(e11,e13)
| e12 = op1(e11,e13)
| e13 = op1(e11,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f82,plain,
( e12 = op1(e10,e13)
| e12 = op1(e11,e13)
| e12 = op1(e12,e13)
| e12 = op1(e13,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f83,plain,
( e12 = op1(e13,e10)
| e12 = op1(e13,e11)
| e12 = op1(e13,e12)
| e12 = 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(f92,plain,
( e11 = op1(e10,e12)
| e11 = op1(e11,e12)
| e11 = op1(e12,e12)
| e11 = op1(e13,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
( e11 = op1(e12,e10)
| e11 = op1(e12,e11)
| e11 = op1(e12,e12)
| e11 = op1(e12,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f96,plain,
( e13 = op1(e10,e11)
| e13 = op1(e11,e11)
| e13 = op1(e12,e11)
| e13 = 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(f110,plain,
( e10 = op1(e10,e10)
| e10 = op1(e11,e10)
| e10 = op1(e12,e10)
| e10 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f111,plain,
( e10 = op1(e10,e10)
| e10 = op1(e10,e11)
| e10 = op1(e10,e12)
| e10 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f115,plain,
( e20 = op2(e23,e20)
| e21 = op2(e23,e20)
| e22 = op2(e23,e20)
| e23 = op2(e23,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f116,plain,
( e20 = op2(e22,e23)
| e21 = op2(e22,e23)
| e22 = op2(e22,e23)
| e23 = op2(e22,e23) ),
inference(cnf_transformation,[],[f3]) ).
fof(f121,plain,
( e20 = op2(e21,e22)
| e21 = op2(e21,e22)
| e22 = op2(e21,e22)
| e23 = op2(e21,e22) ),
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(f131,plain,
( e22 = op2(e23,e20)
| e22 = op2(e23,e21)
| e22 = op2(e23,e22)
| e22 = op2(e23,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f140,plain,
( e21 = op2(e20,e22)
| e21 = op2(e21,e22)
| e21 = op2(e22,e22)
| e21 = op2(e23,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f141,plain,
( e21 = op2(e22,e20)
| e21 = op2(e22,e21)
| e21 = op2(e22,e22)
| e21 = 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(f145,plain,
( e23 = op2(e21,e20)
| e23 = op2(e21,e21)
| e23 = op2(e21,e22)
| e23 = op2(e21,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f158,plain,
( e20 = op2(e20,e20)
| e20 = op2(e21,e20)
| e20 = op2(e22,e20)
| e20 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f159,plain,
( e20 = op2(e20,e20)
| e20 = op2(e20,e21)
| e20 = op2(e20,e22)
| e20 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f160,plain,
op1(e13,e12) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f163,plain,
op1(e13,e10) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
op1(e13,e10) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f172,plain,
op1(e11,e12) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f173,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f177,plain,
op1(e11,e10) != op1(e11,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f182,plain,
op1(e10,e10) != op1(e10,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f184,plain,
op1(e12,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f185,plain,
op1(e11,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f193,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f201,plain,
op1(e10,e11) != op1(e11,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f205,plain,
op1(e10,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f208,plain,
op2(e23,e22) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f211,plain,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f212,plain,
op2(e23,e20) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f213,plain,
op2(e23,e20) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f214,plain,
op2(e22,e22) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f216,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f224,plain,
op2(e21,e20) != op2(e21,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f225,plain,
op2(e21,e20) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f232,plain,
op2(e22,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f236,plain,
op2(e20,e23) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f239,plain,
op2(e21,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f240,plain,
op2(e21,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f241,plain,
op2(e20,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f249,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f251,plain,
op2(e21,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f253,plain,
op2(e20,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f255,plain,
op2(e20,e20) != op2(e21,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(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(f288,plain,
( e13 != op1(e12,e12)
| ~ sP1 ),
inference(cnf_transformation,[],[f46]) ).
fof(f291,plain,
( e13 = op1(e13,e13)
| ~ sP0 ),
inference(cnf_transformation,[],[f47]) ).
fof(f296,plain,
( op1(e10,e10) = e13
| e11 != op1(e13,e13)
| e12 != op1(e13,e13)
| sP0 ),
inference(cnf_transformation,[],[f25]) ).
fof(f307,plain,
( op1(e10,e10) = e12
| e12 = op1(e11,e11)
| e12 = op1(e12,e12)
| sP1 ),
inference(cnf_transformation,[],[f25]) ).
fof(f319,plain,
( e10 != op1(e10,e10)
| e10 = op1(e11,e11)
| e10 = op1(e12,e12)
| 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(f326,plain,
( e23 != op2(e21,e21)
| ~ sP6 ),
inference(cnf_transformation,[],[f49]) ).
fof(f327,plain,
( e21 = op2(e23,e23)
| ~ sP6 ),
inference(cnf_transformation,[],[f49]) ).
fof(f328,plain,
( e23 != op2(e22,e22)
| ~ sP5 ),
inference(cnf_transformation,[],[f50]) ).
fof(f331,plain,
( e23 = op2(e23,e23)
| ~ sP4 ),
inference(cnf_transformation,[],[f51]) ).
fof(f338,plain,
( op2(e20,e20) = e23
| e23 = op2(e21,e21)
| e22 != op2(e23,e23)
| 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(f347,plain,
( op2(e20,e20) = e22
| e22 = op2(e21,e21)
| e22 = op2(e22,e22)
| sP5 ),
inference(cnf_transformation,[],[f30]) ).
fof(f349,plain,
( e20 != op2(e21,e21)
| e21 != op2(e21,e21)
| e21 = op2(e22,e22)
| sP6 ),
inference(cnf_transformation,[],[f30]) ).
fof(f351,plain,
( e20 != op2(e21,e21)
| e21 = op2(e21,e21)
| e21 = op2(e22,e22)
| sP6 ),
inference(cnf_transformation,[],[f30]) ).
fof(f359,plain,
( e20 != op2(e20,e20)
| e20 = op2(e21,e21)
| e20 = op2(e22,e22)
| 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,
e13 = op1(e12,e12),
inference(cnf_transformation,[],[f12]) ).
fof(f365,plain,
e11 = op1(op1(e12,e12),op1(e12,e12)),
inference(cnf_transformation,[],[f12]) ).
fof(f366,plain,
e10 = op1(op1(e12,e12),e12),
inference(cnf_transformation,[],[f12]) ).
fof(f367,plain,
e23 = op2(e22,e22),
inference(cnf_transformation,[],[f13]) ).
fof(f369,plain,
e20 = op2(op2(e22,e22),e22),
inference(cnf_transformation,[],[f13]) ).
fof(f378,plain,
op2(e22,e22) = h3(e13),
inference(cnf_transformation,[],[f16]) ).
fof(f379,plain,
op2(op2(e22,e22),op2(e22,e22)) = h3(e11),
inference(cnf_transformation,[],[f16]) ).
fof(f380,plain,
op2(op2(e22,e22),e22) = h3(e10),
inference(cnf_transformation,[],[f16]) ).
fof(f381,plain,
e22 = h3(e12),
inference(cnf_transformation,[],[f16]) ).
fof(f412,plain,
( e21 != h3(e11)
| ~ sP13 ),
inference(cnf_transformation,[],[f58]) ).
fof(f415,plain,
( e22 != h3(e12)
| ~ sP12 ),
inference(cnf_transformation,[],[f59]) ).
fof(f418,plain,
( e23 != h3(e13)
| ~ sP11 ),
inference(cnf_transformation,[],[f60]) ).
fof(f441,plain,
( 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)
| sP13
| sP12
| sP11 ),
inference(cnf_transformation,[],[f43]) ).
fof(f547,definition,
( spl20_24
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl20_24])],[avatar_definition]) ).
fof(f551,definition,
( spl20_25
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl20_25])],[avatar_definition]) ).
fof(f555,definition,
( spl20_26
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl20_26])],[avatar_definition]) ).
fof(f563,definition,
( spl20_28
<=> h3(op1(e13,e13)) = op2(h3(e13),h3(e13)) ),
introduced(definition,[new_symbols(definition,[spl20_28])],[avatar_definition]) ).
fof(f565,plain,
( h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| spl20_28 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f567,definition,
( spl20_29
<=> h3(op1(e13,e12)) = op2(h3(e13),h3(e12)) ),
introduced(definition,[new_symbols(definition,[spl20_29])],[avatar_definition]) ).
fof(f569,plain,
( h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| spl20_29 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f571,definition,
( spl20_30
<=> h3(op1(e13,e11)) = op2(h3(e13),h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl20_30])],[avatar_definition]) ).
fof(f573,plain,
( h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| spl20_30 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f575,definition,
( spl20_31
<=> h3(op1(e13,e10)) = op2(h3(e13),h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl20_31])],[avatar_definition]) ).
fof(f577,plain,
( h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| spl20_31 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f579,definition,
( spl20_32
<=> h3(op1(e12,e13)) = op2(h3(e12),h3(e13)) ),
introduced(definition,[new_symbols(definition,[spl20_32])],[avatar_definition]) ).
fof(f581,plain,
( h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| spl20_32 ),
inference(avatar_component_clause,[],[f579]) ).
fof(f583,definition,
( spl20_33
<=> h3(op1(e12,e12)) = op2(h3(e12),h3(e12)) ),
introduced(definition,[new_symbols(definition,[spl20_33])],[avatar_definition]) ).
fof(f585,plain,
( h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| spl20_33 ),
inference(avatar_component_clause,[],[f583]) ).
fof(f587,definition,
( spl20_34
<=> h3(op1(e12,e11)) = op2(h3(e12),h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl20_34])],[avatar_definition]) ).
fof(f589,plain,
( h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| spl20_34 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f591,definition,
( spl20_35
<=> h3(op1(e12,e10)) = op2(h3(e12),h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl20_35])],[avatar_definition]) ).
fof(f593,plain,
( h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| spl20_35 ),
inference(avatar_component_clause,[],[f591]) ).
fof(f595,definition,
( spl20_36
<=> h3(op1(e11,e13)) = op2(h3(e11),h3(e13)) ),
introduced(definition,[new_symbols(definition,[spl20_36])],[avatar_definition]) ).
fof(f597,plain,
( h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| spl20_36 ),
inference(avatar_component_clause,[],[f595]) ).
fof(f599,definition,
( spl20_37
<=> h3(op1(e11,e12)) = op2(h3(e11),h3(e12)) ),
introduced(definition,[new_symbols(definition,[spl20_37])],[avatar_definition]) ).
fof(f601,plain,
( h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| spl20_37 ),
inference(avatar_component_clause,[],[f599]) ).
fof(f603,definition,
( spl20_38
<=> h3(op1(e11,e11)) = op2(h3(e11),h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl20_38])],[avatar_definition]) ).
fof(f605,plain,
( h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| spl20_38 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f607,definition,
( spl20_39
<=> h3(op1(e11,e10)) = op2(h3(e11),h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl20_39])],[avatar_definition]) ).
fof(f609,plain,
( h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| spl20_39 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f611,definition,
( spl20_40
<=> h3(op1(e10,e13)) = op2(h3(e10),h3(e13)) ),
introduced(definition,[new_symbols(definition,[spl20_40])],[avatar_definition]) ).
fof(f613,plain,
( h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| spl20_40 ),
inference(avatar_component_clause,[],[f611]) ).
fof(f615,definition,
( spl20_41
<=> h3(op1(e10,e12)) = op2(h3(e10),h3(e12)) ),
introduced(definition,[new_symbols(definition,[spl20_41])],[avatar_definition]) ).
fof(f617,plain,
( h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| spl20_41 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f619,definition,
( spl20_42
<=> h3(op1(e10,e11)) = op2(h3(e10),h3(e11)) ),
introduced(definition,[new_symbols(definition,[spl20_42])],[avatar_definition]) ).
fof(f621,plain,
( h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| spl20_42 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f623,definition,
( spl20_43
<=> h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) ),
introduced(definition,[new_symbols(definition,[spl20_43])],[avatar_definition]) ).
fof(f625,plain,
( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| spl20_43 ),
inference(avatar_component_clause,[],[f623]) ).
fof(f638,definition,
( spl20_46
<=> e20 = h3(e10) ),
introduced(definition,[new_symbols(definition,[spl20_46])],[avatar_definition]) ).
fof(f639,plain,
( e20 = h3(e10)
| ~ spl20_46 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f641,plain,
( spl20_24
| spl20_25
| spl20_26
| ~ spl20_46
| ~ spl20_28
| ~ spl20_29
| ~ spl20_30
| ~ spl20_31
| ~ spl20_32
| ~ spl20_33
| ~ spl20_34
| ~ spl20_35
| ~ spl20_36
| ~ spl20_37
| ~ spl20_38
| ~ spl20_39
| ~ spl20_40
| ~ spl20_41
| ~ spl20_42
| ~ spl20_43 ),
inference(avatar_split_clause,[],[f441,f623,f619,f615,f611,f607,f603,f599,f595,f591,f587,f583,f579,f575,f571,f567,f563,f638,f555,f551,f547]) ).
fof(f895,definition,
( spl20_105
<=> e23 = h3(e13) ),
introduced(definition,[new_symbols(definition,[spl20_105])],[avatar_definition]) ).
fof(f896,plain,
( e23 = h3(e13)
| ~ spl20_105 ),
inference(avatar_component_clause,[],[f895]) ).
fof(f898,plain,
( ~ spl20_24
| ~ spl20_105 ),
inference(avatar_split_clause,[],[f418,f895,f547]) ).
fof(f920,definition,
( spl20_110
<=> e22 = h3(e12) ),
introduced(definition,[new_symbols(definition,[spl20_110])],[avatar_definition]) ).
fof(f921,plain,
( e22 = h3(e12)
| ~ spl20_110 ),
inference(avatar_component_clause,[],[f920]) ).
fof(f923,plain,
( ~ spl20_25
| ~ spl20_110 ),
inference(avatar_split_clause,[],[f415,f920,f551]) ).
fof(f945,definition,
( spl20_115
<=> e21 = h3(e11) ),
introduced(definition,[new_symbols(definition,[spl20_115])],[avatar_definition]) ).
fof(f946,plain,
( e21 = h3(e11)
| ~ spl20_115 ),
inference(avatar_component_clause,[],[f945]) ).
fof(f948,plain,
( ~ spl20_26
| ~ spl20_115 ),
inference(avatar_split_clause,[],[f412,f945,f555]) ).
fof(f1075,plain,
spl20_110,
inference(avatar_split_clause,[],[f381,f920]) ).
fof(f1079,definition,
( spl20_141
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl20_141])],[avatar_definition]) ).
fof(f1083,definition,
( spl20_142
<=> e22 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl20_142])],[avatar_definition]) ).
fof(f1087,definition,
( spl20_143
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl20_143])],[avatar_definition]) ).
fof(f1088,plain,
( e21 = op2(e23,e23)
| ~ spl20_143 ),
inference(avatar_component_clause,[],[f1087]) ).
fof(f1091,definition,
( spl20_144
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl20_144])],[avatar_definition]) ).
fof(f1092,plain,
( e20 = op2(e23,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(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(f1112,plain,
( spl20_141
| ~ spl20_142
| spl20_146
| spl20_147 ),
inference(avatar_split_clause,[],[f338,f1107,f1101,f1083,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(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl20_150])],[avatar_definition]) ).
fof(f1124,plain,
( e21 = op2(e22,e22)
| ~ spl20_150 ),
inference(avatar_component_clause,[],[f1123]) ).
fof(f1127,definition,
( spl20_151
<=> e20 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl20_151])],[avatar_definition]) ).
fof(f1128,plain,
( e20 = op2(e22,e22)
| ~ spl20_151 ),
inference(avatar_component_clause,[],[f1127]) ).
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(f1145,plain,
( spl20_148
| spl20_149
| spl20_152
| spl20_153 ),
inference(avatar_split_clause,[],[f347,f1139,f1133,f1119,f1115]) ).
fof(f1147,definition,
( spl20_154
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl20_154])],[avatar_definition]) ).
fof(f1151,definition,
( spl20_155
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl20_155])],[avatar_definition]) ).
fof(f1155,definition,
( spl20_156
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl20_156])],[avatar_definition]) ).
fof(f1156,plain,
( e20 = op2(e21,e21)
| ~ spl20_156 ),
inference(avatar_component_clause,[],[f1155]) ).
fof(f1159,plain,
( spl20_154
| spl20_150
| ~ spl20_155
| ~ spl20_156 ),
inference(avatar_split_clause,[],[f349,f1155,f1151,f1123,f1147]) ).
fof(f1161,plain,
( spl20_154
| spl20_150
| spl20_155
| ~ spl20_156 ),
inference(avatar_split_clause,[],[f351,f1155,f1151,f1123,f1147]) ).
fof(f1171,definition,
( spl20_158
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl20_158])],[avatar_definition]) ).
fof(f1175,definition,
( spl20_159
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl20_159])],[avatar_definition]) ).
fof(f1176,plain,
( e20 = op2(e20,e20)
| ~ spl20_159 ),
inference(avatar_component_clause,[],[f1175]) ).
fof(f1181,plain,
( spl20_158
| spl20_151
| spl20_156
| ~ spl20_159 ),
inference(avatar_split_clause,[],[f359,f1175,f1155,f1127,f1171]) ).
fof(f1185,plain,
( spl20_158
| spl20_151
| spl20_156
| spl20_159 ),
inference(avatar_split_clause,[],[f363,f1175,f1155,f1127,f1171]) ).
fof(f1187,definition,
( spl20_160
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl20_160])],[avatar_definition]) ).
fof(f1188,plain,
( e23 = op2(e23,e23)
| ~ spl20_160 ),
inference(avatar_component_clause,[],[f1187]) ).
fof(f1191,plain,
( ~ spl20_141
| spl20_160 ),
inference(avatar_split_clause,[],[f331,f1187,f1079]) ).
fof(f1192,plain,
( ~ spl20_148
| ~ spl20_145 ),
inference(avatar_split_clause,[],[f328,f1096,f1115]) ).
fof(f1194,plain,
( ~ spl20_154
| ~ spl20_146 ),
inference(avatar_split_clause,[],[f326,f1101,f1147]) ).
fof(f1195,plain,
( ~ spl20_154
| spl20_143 ),
inference(avatar_split_clause,[],[f327,f1087,f1147]) ).
fof(f1197,plain,
( ~ spl20_158
| spl20_144 ),
inference(avatar_split_clause,[],[f325,f1091,f1171]) ).
fof(f1199,definition,
( spl20_161
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl20_161])],[avatar_definition]) ).
fof(f1203,definition,
( spl20_162
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl20_162])],[avatar_definition]) ).
fof(f1207,definition,
( spl20_163
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl20_163])],[avatar_definition]) ).
fof(f1208,plain,
( e11 = op1(e13,e13)
| ~ spl20_163 ),
inference(avatar_component_clause,[],[f1207]) ).
fof(f1211,definition,
( spl20_164
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl20_164])],[avatar_definition]) ).
fof(f1216,definition,
( spl20_165
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl20_165])],[avatar_definition]) ).
fof(f1218,plain,
( e13 = op1(e12,e12)
| ~ spl20_165 ),
inference(avatar_component_clause,[],[f1216]) ).
fof(f1221,definition,
( spl20_166
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl20_166])],[avatar_definition]) ).
fof(f1223,plain,
( e13 = op1(e11,e11)
| ~ spl20_166 ),
inference(avatar_component_clause,[],[f1221]) ).
fof(f1227,definition,
( spl20_167
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl20_167])],[avatar_definition]) ).
fof(f1229,plain,
( op1(e10,e10) = e13
| ~ spl20_167 ),
inference(avatar_component_clause,[],[f1227]) ).
fof(f1230,plain,
( spl20_161
| ~ spl20_162
| ~ spl20_163
| spl20_167 ),
inference(avatar_split_clause,[],[f296,f1227,f1207,f1203,f1199]) ).
fof(f1235,definition,
( spl20_168
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl20_168])],[avatar_definition]) ).
fof(f1239,definition,
( spl20_169
<=> e12 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl20_169])],[avatar_definition]) ).
fof(f1240,plain,
( e12 = op1(e12,e12)
| ~ spl20_169 ),
inference(avatar_component_clause,[],[f1239]) ).
fof(f1243,definition,
( spl20_170
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl20_170])],[avatar_definition]) ).
fof(f1244,plain,
( e11 = op1(e12,e12)
| ~ spl20_170 ),
inference(avatar_component_clause,[],[f1243]) ).
fof(f1247,definition,
( spl20_171
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl20_171])],[avatar_definition]) ).
fof(f1248,plain,
( e10 = op1(e12,e12)
| ~ spl20_171 ),
inference(avatar_component_clause,[],[f1247]) ).
fof(f1253,definition,
( spl20_172
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl20_172])],[avatar_definition]) ).
fof(f1255,plain,
( e12 = op1(e11,e11)
| ~ spl20_172 ),
inference(avatar_component_clause,[],[f1253]) ).
fof(f1259,definition,
( spl20_173
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[spl20_173])],[avatar_definition]) ).
fof(f1261,plain,
( op1(e10,e10) = e12
| ~ spl20_173 ),
inference(avatar_component_clause,[],[f1259]) ).
fof(f1265,plain,
( spl20_168
| spl20_169
| spl20_172
| spl20_173 ),
inference(avatar_split_clause,[],[f307,f1259,f1253,f1239,f1235]) ).
fof(f1271,definition,
( spl20_175
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl20_175])],[avatar_definition]) ).
fof(f1272,plain,
( e11 = op1(e11,e11)
| ~ spl20_175 ),
inference(avatar_component_clause,[],[f1271]) ).
fof(f1275,definition,
( spl20_176
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl20_176])],[avatar_definition]) ).
fof(f1276,plain,
( e10 = op1(e11,e11)
| ~ spl20_176 ),
inference(avatar_component_clause,[],[f1275]) ).
fof(f1291,definition,
( spl20_178
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl20_178])],[avatar_definition]) ).
fof(f1295,definition,
( spl20_179
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl20_179])],[avatar_definition]) ).
fof(f1296,plain,
( e10 = op1(e10,e10)
| ~ spl20_179 ),
inference(avatar_component_clause,[],[f1295]) ).
fof(f1301,plain,
( spl20_178
| spl20_171
| spl20_176
| ~ spl20_179 ),
inference(avatar_split_clause,[],[f319,f1295,f1275,f1247,f1291]) ).
fof(f1305,plain,
( spl20_178
| spl20_171
| spl20_176
| spl20_179 ),
inference(avatar_split_clause,[],[f323,f1295,f1275,f1247,f1291]) ).
fof(f1307,definition,
( spl20_180
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl20_180])],[avatar_definition]) ).
fof(f1308,plain,
( e13 = op1(e13,e13)
| ~ spl20_180 ),
inference(avatar_component_clause,[],[f1307]) ).
fof(f1311,plain,
( ~ spl20_161
| spl20_180 ),
inference(avatar_split_clause,[],[f291,f1307,f1199]) ).
fof(f1312,plain,
( ~ spl20_168
| ~ spl20_165 ),
inference(avatar_split_clause,[],[f288,f1216,f1235]) ).
fof(f1317,plain,
( ~ spl20_178
| spl20_164 ),
inference(avatar_split_clause,[],[f285,f1211,f1291]) ).
fof(f1319,definition,
( spl20_181
<=> e23 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl20_181])],[avatar_definition]) ).
fof(f1323,definition,
( spl20_182
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl20_182])],[avatar_definition]) ).
fof(f1336,definition,
( spl20_185
<=> e23 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl20_185])],[avatar_definition]) ).
fof(f1338,plain,
( e23 = op2(e23,e21)
| ~ spl20_185 ),
inference(avatar_component_clause,[],[f1336]) ).
fof(f1340,definition,
( spl20_186
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl20_186])],[avatar_definition]) ).
fof(f1342,plain,
( e23 = op2(e23,e20)
| ~ spl20_186 ),
inference(avatar_component_clause,[],[f1340]) ).
fof(f1345,definition,
( spl20_187
<=> e22 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl20_187])],[avatar_definition]) ).
fof(f1358,definition,
( spl20_190
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl20_190])],[avatar_definition]) ).
fof(f1360,plain,
( e22 = op2(e23,e22)
| ~ spl20_190 ),
inference(avatar_component_clause,[],[f1358]) ).
fof(f1362,definition,
( spl20_191
<=> e22 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl20_191])],[avatar_definition]) ).
fof(f1364,plain,
( e22 = op2(e23,e21)
| ~ spl20_191 ),
inference(avatar_component_clause,[],[f1362]) ).
fof(f1366,definition,
( spl20_192
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl20_192])],[avatar_definition]) ).
fof(f1369,plain,
( spl20_142
| spl20_190
| spl20_191
| spl20_192 ),
inference(avatar_split_clause,[],[f131,f1366,f1362,f1358,f1083]) ).
fof(f1371,definition,
( spl20_193
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl20_193])],[avatar_definition]) ).
fof(f1384,definition,
( spl20_196
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl20_196])],[avatar_definition]) ).
fof(f1386,plain,
( e21 = op2(e23,e22)
| ~ spl20_196 ),
inference(avatar_component_clause,[],[f1384]) ).
fof(f1392,definition,
( spl20_198
<=> e21 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl20_198])],[avatar_definition]) ).
fof(f1397,definition,
( spl20_199
<=> e20 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl20_199])],[avatar_definition]) ).
fof(f1405,definition,
( spl20_201
<=> e20 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl20_201])],[avatar_definition]) ).
fof(f1407,plain,
( e20 = op2(e20,e23)
| ~ spl20_201 ),
inference(avatar_component_clause,[],[f1405]) ).
fof(f1410,definition,
( spl20_202
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl20_202])],[avatar_definition]) ).
fof(f1412,plain,
( e20 = op2(e23,e22)
| ~ spl20_202 ),
inference(avatar_component_clause,[],[f1410]) ).
fof(f1418,definition,
( spl20_204
<=> e20 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl20_204])],[avatar_definition]) ).
fof(f1423,definition,
( spl20_205
<=> e23 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl20_205])],[avatar_definition]) ).
fof(f1432,definition,
( spl20_207
<=> e23 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl20_207])],[avatar_definition]) ).
fof(f1441,definition,
( spl20_209
<=> e22 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl20_209])],[avatar_definition]) ).
fof(f1459,definition,
( spl20_213
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl20_213])],[avatar_definition]) ).
fof(f1463,definition,
( spl20_214
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl20_214])],[avatar_definition]) ).
fof(f1465,plain,
( e21 = op2(e20,e22)
| ~ spl20_214 ),
inference(avatar_component_clause,[],[f1463]) ).
fof(f1466,plain,
( spl20_196
| spl20_150
| spl20_213
| spl20_214 ),
inference(avatar_split_clause,[],[f140,f1463,f1459,f1123,f1384]) ).
fof(f1468,definition,
( spl20_215
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl20_215])],[avatar_definition]) ).
fof(f1472,definition,
( spl20_216
<=> e21 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl20_216])],[avatar_definition]) ).
fof(f1474,plain,
( e21 = op2(e22,e20)
| ~ spl20_216 ),
inference(avatar_component_clause,[],[f1472]) ).
fof(f1475,plain,
( spl20_193
| spl20_150
| spl20_215
| spl20_216 ),
inference(avatar_split_clause,[],[f141,f1472,f1468,f1123,f1371]) ).
fof(f1477,definition,
( spl20_217
<=> e20 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl20_217])],[avatar_definition]) ).
fof(f1479,plain,
( e20 = op2(e21,e22)
| ~ spl20_217 ),
inference(avatar_component_clause,[],[f1477]) ).
fof(f1481,definition,
( spl20_218
<=> e20 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl20_218])],[avatar_definition]) ).
fof(f1490,definition,
( spl20_220
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl20_220])],[avatar_definition]) ).
fof(f1492,plain,
( e20 = op2(e22,e20)
| ~ spl20_220 ),
inference(avatar_component_clause,[],[f1490]) ).
fof(f1495,definition,
( spl20_221
<=> e23 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl20_221])],[avatar_definition]) ).
fof(f1498,plain,
( spl20_185
| spl20_207
| spl20_146
| spl20_221 ),
inference(avatar_split_clause,[],[f144,f1495,f1101,f1432,f1336]) ).
fof(f1500,definition,
( spl20_222
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl20_222])],[avatar_definition]) ).
fof(f1502,plain,
( e23 = op2(e21,e20)
| ~ spl20_222 ),
inference(avatar_component_clause,[],[f1500]) ).
fof(f1503,plain,
( spl20_182
| spl20_205
| spl20_146
| spl20_222 ),
inference(avatar_split_clause,[],[f145,f1500,f1101,f1423,f1323]) ).
fof(f1510,definition,
( spl20_224
<=> e22 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl20_224])],[avatar_definition]) ).
fof(f1520,definition,
( spl20_226
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl20_226])],[avatar_definition]) ).
fof(f1522,plain,
( e21 = op2(e21,e20)
| ~ spl20_226 ),
inference(avatar_component_clause,[],[f1520]) ).
fof(f1525,definition,
( spl20_227
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl20_227])],[avatar_definition]) ).
fof(f1530,definition,
( spl20_228
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl20_228])],[avatar_definition]) ).
fof(f1540,plain,
( spl20_204
| spl20_220
| spl20_228
| spl20_159 ),
inference(avatar_split_clause,[],[f158,f1175,f1530,f1490,f1418]) ).
fof(f1541,plain,
( spl20_201
| spl20_218
| spl20_227
| spl20_159 ),
inference(avatar_split_clause,[],[f159,f1175,f1525,f1481,f1405]) ).
fof(f1545,plain,
( spl20_186
| spl20_192
| spl20_198
| spl20_204 ),
inference(avatar_split_clause,[],[f115,f1418,f1392,f1366,f1340]) ).
fof(f1546,plain,
( spl20_181
| spl20_187
| spl20_193
| spl20_199 ),
inference(avatar_split_clause,[],[f116,f1397,f1371,f1345,f1319]) ).
fof(f1551,plain,
( spl20_205
| spl20_209
| spl20_213
| spl20_217 ),
inference(avatar_split_clause,[],[f121,f1477,f1459,f1441,f1423]) ).
fof(f1553,plain,
( spl20_222
| spl20_224
| spl20_226
| spl20_228 ),
inference(avatar_split_clause,[],[f123,f1530,f1520,f1510,f1500]) ).
fof(f1563,definition,
( spl20_230
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl20_230])],[avatar_definition]) ).
fof(f1565,plain,
( e13 = op1(e11,e13)
| ~ spl20_230 ),
inference(avatar_component_clause,[],[f1563]) ).
fof(f1576,definition,
( spl20_233
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl20_233])],[avatar_definition]) ).
fof(f1578,plain,
( e13 = op1(e13,e11)
| ~ spl20_233 ),
inference(avatar_component_clause,[],[f1576]) ).
fof(f1580,definition,
( spl20_234
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl20_234])],[avatar_definition]) ).
fof(f1582,plain,
( e13 = op1(e13,e10)
| ~ spl20_234 ),
inference(avatar_component_clause,[],[f1580]) ).
fof(f1585,definition,
( spl20_235
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl20_235])],[avatar_definition]) ).
fof(f1587,plain,
( e12 = op1(e12,e13)
| ~ spl20_235 ),
inference(avatar_component_clause,[],[f1585]) ).
fof(f1589,definition,
( spl20_236
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl20_236])],[avatar_definition]) ).
fof(f1593,definition,
( spl20_237
<=> e12 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl20_237])],[avatar_definition]) ).
fof(f1595,plain,
( e12 = op1(e10,e13)
| ~ spl20_237 ),
inference(avatar_component_clause,[],[f1593]) ).
fof(f1596,plain,
( spl20_162
| spl20_235
| spl20_236
| spl20_237 ),
inference(avatar_split_clause,[],[f82,f1593,f1589,f1585,f1203]) ).
fof(f1598,definition,
( spl20_238
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl20_238])],[avatar_definition]) ).
fof(f1600,plain,
( e12 = op1(e13,e12)
| ~ spl20_238 ),
inference(avatar_component_clause,[],[f1598]) ).
fof(f1602,definition,
( spl20_239
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl20_239])],[avatar_definition]) ).
fof(f1604,plain,
( e12 = op1(e13,e11)
| ~ spl20_239 ),
inference(avatar_component_clause,[],[f1602]) ).
fof(f1606,definition,
( spl20_240
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl20_240])],[avatar_definition]) ).
fof(f1609,plain,
( spl20_162
| spl20_238
| spl20_239
| spl20_240 ),
inference(avatar_split_clause,[],[f83,f1606,f1602,f1598,f1203]) ).
fof(f1611,definition,
( spl20_241
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl20_241])],[avatar_definition]) ).
fof(f1615,definition,
( spl20_242
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl20_242])],[avatar_definition]) ).
fof(f1624,definition,
( spl20_244
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl20_244])],[avatar_definition]) ).
fof(f1626,plain,
( e11 = op1(e13,e12)
| ~ spl20_244 ),
inference(avatar_component_clause,[],[f1624]) ).
fof(f1632,definition,
( spl20_246
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl20_246])],[avatar_definition]) ).
fof(f1641,definition,
( spl20_248
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl20_248])],[avatar_definition]) ).
fof(f1645,definition,
( spl20_249
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl20_249])],[avatar_definition]) ).
fof(f1647,plain,
( e10 = op1(e10,e13)
| ~ spl20_249 ),
inference(avatar_component_clause,[],[f1645]) ).
fof(f1650,definition,
( spl20_250
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl20_250])],[avatar_definition]) ).
fof(f1652,plain,
( e10 = op1(e13,e12)
| ~ spl20_250 ),
inference(avatar_component_clause,[],[f1650]) ).
fof(f1658,definition,
( spl20_252
<=> e10 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl20_252])],[avatar_definition]) ).
fof(f1672,definition,
( spl20_255
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl20_255])],[avatar_definition]) ).
fof(f1681,definition,
( spl20_257
<=> e12 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl20_257])],[avatar_definition]) ).
fof(f1683,plain,
( e12 = op1(e11,e12)
| ~ spl20_257 ),
inference(avatar_component_clause,[],[f1681]) ).
fof(f1685,definition,
( spl20_258
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl20_258])],[avatar_definition]) ).
fof(f1688,plain,
( spl20_238
| spl20_169
| spl20_257
| spl20_258 ),
inference(avatar_split_clause,[],[f90,f1685,f1681,f1239,f1598]) ).
fof(f1699,definition,
( spl20_261
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl20_261])],[avatar_definition]) ).
fof(f1701,plain,
( e11 = op1(e11,e12)
| ~ spl20_261 ),
inference(avatar_component_clause,[],[f1699]) ).
fof(f1703,definition,
( spl20_262
<=> e11 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl20_262])],[avatar_definition]) ).
fof(f1705,plain,
( e11 = op1(e10,e12)
| ~ spl20_262 ),
inference(avatar_component_clause,[],[f1703]) ).
fof(f1706,plain,
( spl20_244
| spl20_170
| spl20_261
| spl20_262 ),
inference(avatar_split_clause,[],[f92,f1703,f1699,f1243,f1624]) ).
fof(f1708,definition,
( spl20_263
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl20_263])],[avatar_definition]) ).
fof(f1710,plain,
( e11 = op1(e12,e11)
| ~ spl20_263 ),
inference(avatar_component_clause,[],[f1708]) ).
fof(f1712,definition,
( spl20_264
<=> e11 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl20_264])],[avatar_definition]) ).
fof(f1714,plain,
( e11 = op1(e12,e10)
| ~ spl20_264 ),
inference(avatar_component_clause,[],[f1712]) ).
fof(f1715,plain,
( spl20_241
| spl20_170
| spl20_263
| spl20_264 ),
inference(avatar_split_clause,[],[f93,f1712,f1708,f1243,f1611]) ).
fof(f1721,definition,
( spl20_266
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl20_266])],[avatar_definition]) ).
fof(f1730,definition,
( spl20_268
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl20_268])],[avatar_definition]) ).
fof(f1732,plain,
( e10 = op1(e12,e10)
| ~ spl20_268 ),
inference(avatar_component_clause,[],[f1730]) ).
fof(f1735,definition,
( spl20_269
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl20_269])],[avatar_definition]) ).
fof(f1737,plain,
( e13 = op1(e10,e11)
| ~ spl20_269 ),
inference(avatar_component_clause,[],[f1735]) ).
fof(f1738,plain,
( spl20_233
| spl20_255
| spl20_166
| spl20_269 ),
inference(avatar_split_clause,[],[f96,f1735,f1221,f1672,f1576]) ).
fof(f1760,definition,
( spl20_274
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl20_274])],[avatar_definition]) ).
fof(f1762,plain,
( e11 = op1(e11,e10)
| ~ spl20_274 ),
inference(avatar_component_clause,[],[f1760]) ).
fof(f1763,plain,
( spl20_242
| spl20_261
| spl20_175
| spl20_274 ),
inference(avatar_split_clause,[],[f101,f1760,f1271,f1699,f1615]) ).
fof(f1765,definition,
( spl20_275
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl20_275])],[avatar_definition]) ).
fof(f1770,definition,
( spl20_276
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl20_276])],[avatar_definition]) ).
fof(f1780,plain,
( spl20_252
| spl20_268
| spl20_276
| spl20_179 ),
inference(avatar_split_clause,[],[f110,f1295,f1770,f1730,f1658]) ).
fof(f1781,plain,
( spl20_249
| spl20_266
| spl20_275
| spl20_179 ),
inference(avatar_split_clause,[],[f111,f1295,f1765,f1721,f1645]) ).
fof(f1785,plain,
( spl20_234
| spl20_240
| spl20_246
| spl20_252 ),
inference(avatar_split_clause,[],[f67,f1658,f1632,f1606,f1580]) ).
fof(f1790,plain,
( spl20_230
| spl20_236
| spl20_242
| spl20_248 ),
inference(avatar_split_clause,[],[f72,f1641,f1615,f1589,f1563]) ).
fof(f1798,plain,
spl20_165,
inference(avatar_split_clause,[],[f364,f1216]) ).
fof(f1799,plain,
spl20_145,
inference(avatar_split_clause,[],[f367,f1096]) ).
fof(f1811,plain,
( e20 = e23
| ~ spl20_145
| ~ spl20_151 ),
inference(superposition,[],[f1128,f1098]) ).
fof(f1815,plain,
( $false
| ~ spl20_145
| ~ spl20_151 ),
inference(forward_subsumption_resolution,[],[f1811,f265]) ).
fof(f1816,plain,
( ~ spl20_145
| ~ spl20_151 ),
inference(avatar_contradiction_clause,[],[f1815]) ).
fof(f1853,plain,
( e10 = e13
| ~ spl20_165
| ~ spl20_171 ),
inference(superposition,[],[f1248,f1218]) ).
fof(f1857,plain,
( $false
| ~ spl20_165
| ~ spl20_171 ),
inference(forward_subsumption_resolution,[],[f1853,f259]) ).
fof(f1858,plain,
( ~ spl20_165
| ~ spl20_171 ),
inference(avatar_contradiction_clause,[],[f1857]) ).
fof(f1867,plain,
( e10 = e11
| ~ spl20_175
| ~ spl20_176 ),
inference(superposition,[],[f1276,f1272]) ).
fof(f1873,plain,
( $false
| ~ spl20_175
| ~ spl20_176 ),
inference(forward_subsumption_resolution,[],[f1867,f261]) ).
fof(f1874,plain,
( ~ spl20_175
| ~ spl20_176 ),
inference(avatar_contradiction_clause,[],[f1873]) ).
fof(f1877,plain,
( e10 = e12
| ~ spl20_173
| ~ spl20_179 ),
inference(forward_demodulation,[],[f1296,f1261]) ).
fof(f1878,plain,
( $false
| ~ spl20_173
| ~ spl20_179 ),
inference(forward_subsumption_resolution,[],[f1877,f260]) ).
fof(f1879,plain,
( ~ spl20_173
| ~ spl20_179 ),
inference(avatar_contradiction_clause,[],[f1878]) ).
fof(f1880,plain,
( e10 = e12
| ~ spl20_172
| ~ spl20_176 ),
inference(superposition,[],[f1255,f1276]) ).
fof(f1885,plain,
( $false
| ~ spl20_172
| ~ spl20_176 ),
inference(forward_subsumption_resolution,[],[f1880,f260]) ).
fof(f1886,plain,
( ~ spl20_172
| ~ spl20_176 ),
inference(avatar_contradiction_clause,[],[f1885]) ).
fof(f2009,plain,
( e20 = e21
| ~ spl20_196
| ~ spl20_202 ),
inference(superposition,[],[f1412,f1386]) ).
fof(f2014,plain,
( $false
| ~ spl20_196
| ~ spl20_202 ),
inference(forward_subsumption_resolution,[],[f2009,f267]) ).
fof(f2015,plain,
( ~ spl20_196
| ~ spl20_202 ),
inference(avatar_contradiction_clause,[],[f2014]) ).
fof(f2176,plain,
( e20 = e22
| ~ spl20_190
| ~ spl20_202 ),
inference(superposition,[],[f1360,f1412]) ).
fof(f2181,plain,
( $false
| ~ spl20_190
| ~ spl20_202 ),
inference(forward_subsumption_resolution,[],[f2176,f266]) ).
fof(f2182,plain,
( ~ spl20_190
| ~ spl20_202 ),
inference(avatar_contradiction_clause,[],[f2181]) ).
fof(f2260,plain,
( e12 = e13
| ~ spl20_233
| ~ spl20_239 ),
inference(superposition,[],[f1604,f1578]) ).
fof(f2264,plain,
( $false
| ~ spl20_233
| ~ spl20_239 ),
inference(forward_subsumption_resolution,[],[f2260,f256]) ).
fof(f2265,plain,
( ~ spl20_233
| ~ spl20_239 ),
inference(avatar_contradiction_clause,[],[f2264]) ).
fof(f2293,plain,
( e10 = e11
| ~ spl20_244
| ~ spl20_250 ),
inference(superposition,[],[f1652,f1626]) ).
fof(f2298,plain,
( $false
| ~ spl20_244
| ~ spl20_250 ),
inference(forward_subsumption_resolution,[],[f2293,f261]) ).
fof(f2299,plain,
( ~ spl20_244
| ~ spl20_250 ),
inference(avatar_contradiction_clause,[],[f2298]) ).
fof(f2321,plain,
( e12 = e13
| ~ spl20_167
| ~ spl20_173 ),
inference(forward_demodulation,[],[f1229,f1261]) ).
fof(f2322,plain,
( $false
| ~ spl20_167
| ~ spl20_173 ),
inference(forward_subsumption_resolution,[],[f2321,f256]) ).
fof(f2323,plain,
( ~ spl20_167
| ~ spl20_173 ),
inference(avatar_contradiction_clause,[],[f2322]) ).
fof(f2324,plain,
( e10 = e13
| ~ spl20_166
| ~ spl20_176 ),
inference(forward_demodulation,[],[f1223,f1276]) ).
fof(f2327,plain,
( $false
| ~ spl20_166
| ~ spl20_176 ),
inference(forward_subsumption_resolution,[],[f2324,f259]) ).
fof(f2328,plain,
( ~ spl20_166
| ~ spl20_176 ),
inference(avatar_contradiction_clause,[],[f2327]) ).
fof(f2335,plain,
( e11 = e13
| ~ spl20_165
| ~ spl20_170 ),
inference(superposition,[],[f1244,f1218]) ).
fof(f2339,plain,
( $false
| ~ spl20_165
| ~ spl20_170 ),
inference(forward_subsumption_resolution,[],[f2335,f257]) ).
fof(f2340,plain,
( ~ spl20_165
| ~ spl20_170 ),
inference(avatar_contradiction_clause,[],[f2339]) ).
fof(f2410,plain,
( e10 = e12
| ~ spl20_237
| ~ spl20_249 ),
inference(forward_demodulation,[],[f1647,f1595]) ).
fof(f2411,plain,
( $false
| ~ spl20_237
| ~ spl20_249 ),
inference(forward_subsumption_resolution,[],[f2410,f260]) ).
fof(f2412,plain,
( ~ spl20_237
| ~ spl20_249 ),
inference(avatar_contradiction_clause,[],[f2411]) ).
fof(f2447,plain,
( e10 = e11
| ~ spl20_264
| ~ spl20_268 ),
inference(superposition,[],[f1732,f1714]) ).
fof(f2453,plain,
( $false
| ~ spl20_264
| ~ spl20_268 ),
inference(forward_subsumption_resolution,[],[f2447,f261]) ).
fof(f2454,plain,
( ~ spl20_264
| ~ spl20_268 ),
inference(avatar_contradiction_clause,[],[f2453]) ).
fof(f2540,plain,
( e11 = e12
| ~ spl20_257
| ~ spl20_261 ),
inference(forward_demodulation,[],[f1701,f1683]) ).
fof(f2543,plain,
( $false
| ~ spl20_257
| ~ spl20_261 ),
inference(forward_subsumption_resolution,[],[f2540,f258]) ).
fof(f2544,plain,
( ~ spl20_257
| ~ spl20_261 ),
inference(avatar_contradiction_clause,[],[f2543]) ).
fof(f2587,plain,
( e12 = e13
| ~ spl20_165
| ~ spl20_169 ),
inference(superposition,[],[f1240,f1218]) ).
fof(f2591,plain,
( $false
| ~ spl20_165
| ~ spl20_169 ),
inference(forward_subsumption_resolution,[],[f2587,f256]) ).
fof(f2592,plain,
( ~ spl20_165
| ~ spl20_169 ),
inference(avatar_contradiction_clause,[],[f2591]) ).
fof(f2607,plain,
( e10 = e12
| ~ spl20_238
| ~ spl20_250 ),
inference(forward_demodulation,[],[f1652,f1600]) ).
fof(f2608,plain,
( $false
| ~ spl20_238
| ~ spl20_250 ),
inference(forward_subsumption_resolution,[],[f2607,f260]) ).
fof(f2609,plain,
( ~ spl20_238
| ~ spl20_250 ),
inference(avatar_contradiction_clause,[],[f2608]) ).
fof(f2708,plain,
( e23 = h3(e13)
| ~ spl20_145 ),
inference(forward_demodulation,[],[f378,f1098]) ).
fof(f2709,plain,
( spl20_105
| ~ spl20_145 ),
inference(avatar_split_clause,[],[f2708,f1096,f895]) ).
fof(f2719,plain,
( e11 != op1(e13,e10)
| ~ spl20_163 ),
inference(forward_demodulation,[],[f163,f1208]) ).
fof(f2721,plain,
( e10 != op1(e13,e10)
| ~ spl20_250 ),
inference(forward_demodulation,[],[f164,f1652]) ).
fof(f2728,plain,
( e13 != op1(e12,e11)
| ~ spl20_165 ),
inference(forward_demodulation,[],[f168,f1218]) ).
fof(f2740,plain,
( e10 != op1(e11,e10)
| ~ spl20_176 ),
inference(forward_demodulation,[],[f177,f1276]) ).
fof(f2754,plain,
( e11 != op1(e12,e13)
| ~ spl20_163 ),
inference(forward_demodulation,[],[f184,f1208]) ).
fof(f2756,plain,
( e11 != op1(e11,e13)
| ~ spl20_163 ),
inference(forward_demodulation,[],[f185,f1208]) ).
fof(f2769,plain,
( e10 != op1(e10,e12)
| ~ spl20_250 ),
inference(forward_demodulation,[],[f193,f1652]) ).
fof(f2782,plain,
( e10 != op1(e10,e11)
| ~ spl20_176 ),
inference(forward_demodulation,[],[f201,f1276]) ).
fof(f2794,plain,
( e20 != op2(e23,e22)
| ~ spl20_144 ),
inference(forward_demodulation,[],[f208,f1092]) ).
fof(f2804,plain,
( e23 != op2(e23,e20)
| ~ spl20_185 ),
inference(forward_demodulation,[],[f213,f1338]) ).
fof(f2808,plain,
( e23 != op2(e22,e21)
| ~ spl20_145 ),
inference(forward_demodulation,[],[f216,f1098]) ).
fof(f2846,plain,
( e23 != op2(e21,e22)
| ~ spl20_145 ),
inference(forward_demodulation,[],[f240,f1098]) ).
fof(f2872,plain,
( e10 = op1(e13,e12)
| ~ spl20_165 ),
inference(forward_demodulation,[],[f366,f1218]) ).
fof(f2873,plain,
( e20 = op2(e23,e22)
| ~ spl20_145 ),
inference(forward_demodulation,[],[f369,f1098]) ).
fof(f2874,plain,
( spl20_202
| ~ spl20_145 ),
inference(avatar_split_clause,[],[f2873,f1096,f1410]) ).
fof(f2875,plain,
( e20 = e22
| ~ spl20_152
| ~ spl20_156 ),
inference(forward_demodulation,[],[f1156,f1135]) ).
fof(f2877,plain,
( e20 = e21
| ~ spl20_216
| ~ spl20_220 ),
inference(forward_demodulation,[],[f1474,f1492]) ).
fof(f2881,plain,
( e20 != op2(e23,e22)
| ~ spl20_217 ),
inference(forward_demodulation,[],[f239,f1479]) ).
fof(f2892,plain,
( $false
| ~ spl20_152
| ~ spl20_156 ),
inference(forward_subsumption_resolution,[],[f2875,f266]) ).
fof(f2893,plain,
( ~ spl20_152
| ~ spl20_156 ),
inference(avatar_contradiction_clause,[],[f2892]) ).
fof(f2896,plain,
( $false
| ~ spl20_216
| ~ spl20_220 ),
inference(forward_subsumption_resolution,[],[f2877,f267]) ).
fof(f2897,plain,
( ~ spl20_216
| ~ spl20_220 ),
inference(avatar_contradiction_clause,[],[f2896]) ).
fof(f2898,plain,
( ~ spl20_202
| ~ spl20_217 ),
inference(avatar_split_clause,[],[f2881,f1477,f1410]) ).
fof(f2911,plain,
( ~ spl20_202
| ~ spl20_144 ),
inference(avatar_split_clause,[],[f2794,f1091,f1410]) ).
fof(f2919,plain,
( e23 != op2(e23,e20)
| ~ spl20_222 ),
inference(forward_demodulation,[],[f251,f1502]) ).
fof(f2933,plain,
( e21 = e23
| ~ spl20_145
| ~ spl20_150 ),
inference(superposition,[],[f1124,f1098]) ).
fof(f2937,plain,
( $false
| ~ spl20_145
| ~ spl20_150 ),
inference(forward_subsumption_resolution,[],[f2933,f263]) ).
fof(f2938,plain,
( ~ spl20_145
| ~ spl20_150 ),
inference(avatar_contradiction_clause,[],[f2937]) ).
fof(f2974,plain,
( e22 != op2(e21,e20)
| ~ spl20_153 ),
inference(forward_demodulation,[],[f255,f1141]) ).
fof(f2976,plain,
( e20 != op2(e21,e20)
| ~ spl20_156 ),
inference(forward_demodulation,[],[f225,f1156]) ).
fof(f2980,plain,
( ~ spl20_224
| ~ spl20_153 ),
inference(avatar_split_clause,[],[f2974,f1139,f1510]) ).
fof(f2982,plain,
( ~ spl20_228
| ~ spl20_156 ),
inference(avatar_split_clause,[],[f2976,f1155,f1530]) ).
fof(f3030,plain,
( e21 != op2(e23,e20)
| ~ spl20_143 ),
inference(forward_demodulation,[],[f211,f1088]) ).
fof(f3032,plain,
( e21 = e23
| ~ spl20_143
| ~ spl20_160 ),
inference(forward_demodulation,[],[f1188,f1088]) ).
fof(f3033,plain,
( $false
| ~ spl20_143
| ~ spl20_160 ),
inference(forward_subsumption_resolution,[],[f3032,f263]) ).
fof(f3034,plain,
( ~ spl20_143
| ~ spl20_160 ),
inference(avatar_contradiction_clause,[],[f3033]) ).
fof(f3036,plain,
( e20 != op2(e23,e20)
| ~ spl20_202 ),
inference(forward_demodulation,[],[f212,f1412]) ).
fof(f3059,plain,
( e20 != op2(e20,e22)
| ~ spl20_202 ),
inference(forward_demodulation,[],[f241,f1412]) ).
fof(f3065,plain,
( e20 != op2(e20,e21)
| ~ spl20_156 ),
inference(forward_demodulation,[],[f249,f1156]) ).
fof(f3075,plain,
( op2(e23,e22) = h3(e10)
| ~ spl20_145 ),
inference(forward_demodulation,[],[f380,f1098]) ).
fof(f3076,plain,
( e20 = h3(e10)
| ~ spl20_145
| ~ spl20_202 ),
inference(forward_demodulation,[],[f3075,f1412]) ).
fof(f3077,plain,
( spl20_46
| ~ spl20_145
| ~ spl20_202 ),
inference(avatar_split_clause,[],[f3076,f1410,f1096,f638]) ).
fof(f3086,plain,
( e11 = op1(e13,e13)
| ~ spl20_165 ),
inference(forward_demodulation,[],[f365,f1218]) ).
fof(f3125,plain,
( op2(e23,e23) = h3(e11)
| ~ spl20_145 ),
inference(forward_demodulation,[],[f379,f1098]) ).
fof(f3126,plain,
( e21 = h3(e11)
| ~ spl20_143
| ~ spl20_145 ),
inference(forward_demodulation,[],[f3125,f1088]) ).
fof(f3127,plain,
( spl20_115
| ~ spl20_143
| ~ spl20_145 ),
inference(avatar_split_clause,[],[f3126,f1096,f1087,f945]) ).
fof(f3129,plain,
( h3(op1(e12,e11)) != op2(h3(e12),e21)
| spl20_34
| ~ spl20_115 ),
inference(superposition,[],[f589,f946]) ).
fof(f3130,plain,
( op2(e22,e21) != h3(op1(e12,e11))
| spl20_34
| ~ spl20_110
| ~ spl20_115 ),
inference(forward_demodulation,[],[f3129,f921]) ).
fof(f3133,plain,
( op2(e22,e21) != h3(e11)
| spl20_34
| ~ spl20_110
| ~ spl20_115
| ~ spl20_263 ),
inference(forward_demodulation,[],[f3130,f1710]) ).
fof(f3134,plain,
( e21 != op2(e22,e21)
| spl20_34
| ~ spl20_110
| ~ spl20_115
| ~ spl20_263 ),
inference(forward_demodulation,[],[f3133,f946]) ).
fof(f3137,plain,
( op2(e23,e23) != h3(op1(e13,e13))
| spl20_28
| ~ spl20_105 ),
inference(forward_demodulation,[],[f565,f896]) ).
fof(f3139,plain,
( op2(e23,e23) != h3(e11)
| spl20_28
| ~ spl20_105
| ~ spl20_163 ),
inference(forward_demodulation,[],[f3137,f1208]) ).
fof(f3141,plain,
( e21 != op2(e23,e23)
| spl20_28
| ~ spl20_105
| ~ spl20_115
| ~ spl20_163 ),
inference(forward_demodulation,[],[f3139,f946]) ).
fof(f3143,plain,
( $false
| spl20_28
| ~ spl20_105
| ~ spl20_115
| ~ spl20_143
| ~ spl20_163 ),
inference(forward_subsumption_resolution,[],[f3141,f1088]) ).
fof(f3144,plain,
( spl20_28
| ~ spl20_105
| ~ spl20_115
| ~ spl20_143
| ~ spl20_163 ),
inference(avatar_contradiction_clause,[],[f3143]) ).
fof(f3147,plain,
( h3(op1(e13,e11)) != op2(h3(e13),e21)
| spl20_30
| ~ spl20_115 ),
inference(forward_demodulation,[],[f573,f946]) ).
fof(f3149,plain,
( op2(e23,e21) != h3(op1(e13,e11))
| spl20_30
| ~ spl20_105
| ~ spl20_115 ),
inference(forward_demodulation,[],[f3147,f896]) ).
fof(f3151,plain,
( op2(e23,e21) != h3(e12)
| spl20_30
| ~ spl20_105
| ~ spl20_115
| ~ spl20_239 ),
inference(forward_demodulation,[],[f3149,f1604]) ).
fof(f3152,plain,
( e22 != op2(e23,e21)
| spl20_30
| ~ spl20_105
| ~ spl20_110
| ~ spl20_115
| ~ spl20_239 ),
inference(forward_demodulation,[],[f3151,f921]) ).
fof(f3153,plain,
( $false
| spl20_30
| ~ spl20_105
| ~ spl20_110
| ~ spl20_115
| ~ spl20_191
| ~ spl20_239 ),
inference(forward_subsumption_resolution,[],[f3152,f1364]) ).
fof(f3154,plain,
( spl20_30
| ~ spl20_105
| ~ spl20_110
| ~ spl20_115
| ~ spl20_191
| ~ spl20_239 ),
inference(avatar_contradiction_clause,[],[f3153]) ).
fof(f3155,plain,
( h3(op1(e13,e12)) != op2(h3(e13),e22)
| spl20_29
| ~ spl20_110 ),
inference(forward_demodulation,[],[f569,f921]) ).
fof(f3157,plain,
( op2(e23,e22) != h3(op1(e13,e12))
| spl20_29
| ~ spl20_105
| ~ spl20_110 ),
inference(forward_demodulation,[],[f3155,f896]) ).
fof(f3159,plain,
( op2(e23,e22) != h3(e10)
| spl20_29
| ~ spl20_105
| ~ spl20_110
| ~ spl20_250 ),
inference(forward_demodulation,[],[f3157,f1652]) ).
fof(f3161,plain,
( e20 != op2(e23,e22)
| spl20_29
| ~ spl20_46
| ~ spl20_105
| ~ spl20_110
| ~ spl20_250 ),
inference(forward_demodulation,[],[f3159,f639]) ).
fof(f3163,plain,
( $false
| spl20_29
| ~ spl20_46
| ~ spl20_105
| ~ spl20_110
| ~ spl20_202
| ~ spl20_250 ),
inference(forward_subsumption_resolution,[],[f3161,f1412]) ).
fof(f3164,plain,
( spl20_29
| ~ spl20_46
| ~ spl20_105
| ~ spl20_110
| ~ spl20_202
| ~ spl20_250 ),
inference(avatar_contradiction_clause,[],[f3163]) ).
fof(f3166,plain,
( h3(op1(e12,e13)) != op2(h3(e12),e23)
| spl20_32
| ~ spl20_105 ),
inference(forward_demodulation,[],[f581,f896]) ).
fof(f3168,plain,
( op2(e22,e23) != h3(op1(e12,e13))
| spl20_32
| ~ spl20_105
| ~ spl20_110 ),
inference(forward_demodulation,[],[f3166,f921]) ).
fof(f3170,plain,
( op2(e22,e23) != h3(e12)
| spl20_32
| ~ spl20_105
| ~ spl20_110
| ~ spl20_235 ),
inference(forward_demodulation,[],[f3168,f1587]) ).
fof(f3172,plain,
( e22 != op2(e22,e23)
| spl20_32
| ~ spl20_105
| ~ spl20_110
| ~ spl20_235 ),
inference(forward_demodulation,[],[f3170,f921]) ).
fof(f3175,plain,
( h3(op1(e13,e10)) != op2(h3(e13),e20)
| spl20_31
| ~ spl20_46 ),
inference(forward_demodulation,[],[f577,f639]) ).
fof(f3177,plain,
( op2(e23,e20) != h3(op1(e13,e10))
| spl20_31
| ~ spl20_46
| ~ spl20_105 ),
inference(forward_demodulation,[],[f3175,f896]) ).
fof(f3179,plain,
( op2(e23,e20) != h3(e13)
| spl20_31
| ~ spl20_46
| ~ spl20_105
| ~ spl20_234 ),
inference(forward_demodulation,[],[f3177,f1582]) ).
fof(f3181,plain,
( e23 != op2(e23,e20)
| spl20_31
| ~ spl20_46
| ~ spl20_105
| ~ spl20_234 ),
inference(forward_demodulation,[],[f3179,f896]) ).
fof(f3183,plain,
( $false
| spl20_31
| ~ spl20_46
| ~ spl20_105
| ~ spl20_186
| ~ spl20_234 ),
inference(forward_subsumption_resolution,[],[f3181,f1342]) ).
fof(f3184,plain,
( spl20_31
| ~ spl20_46
| ~ spl20_105
| ~ spl20_186
| ~ spl20_234 ),
inference(avatar_contradiction_clause,[],[f3183]) ).
fof(f3186,plain,
( h3(op1(e12,e10)) != op2(h3(e12),e20)
| spl20_35
| ~ spl20_46 ),
inference(forward_demodulation,[],[f593,f639]) ).
fof(f3188,plain,
( op2(e22,e20) != h3(op1(e12,e10))
| spl20_35
| ~ spl20_46
| ~ spl20_110 ),
inference(forward_demodulation,[],[f3186,f921]) ).
fof(f3190,plain,
( op2(e22,e20) != h3(e10)
| spl20_35
| ~ spl20_46
| ~ spl20_110
| ~ spl20_268 ),
inference(forward_demodulation,[],[f3188,f1732]) ).
fof(f3192,plain,
( e20 != op2(e22,e20)
| spl20_35
| ~ spl20_46
| ~ spl20_110
| ~ spl20_268 ),
inference(forward_demodulation,[],[f3190,f639]) ).
fof(f3195,plain,
( op2(e22,e22) != h3(op1(e12,e12))
| spl20_33
| ~ spl20_110 ),
inference(forward_demodulation,[],[f585,f921]) ).
fof(f3197,plain,
( op2(e22,e22) != h3(e13)
| spl20_33
| ~ spl20_110
| ~ spl20_165 ),
inference(forward_demodulation,[],[f3195,f1218]) ).
fof(f3199,plain,
( e23 != op2(e22,e22)
| spl20_33
| ~ spl20_105
| ~ spl20_110
| ~ spl20_165 ),
inference(forward_demodulation,[],[f3197,f896]) ).
fof(f3201,plain,
( $false
| spl20_33
| ~ spl20_105
| ~ spl20_110
| ~ spl20_145
| ~ spl20_165 ),
inference(forward_subsumption_resolution,[],[f3199,f1098]) ).
fof(f3202,plain,
( spl20_33
| ~ spl20_105
| ~ spl20_110
| ~ spl20_145
| ~ spl20_165 ),
inference(avatar_contradiction_clause,[],[f3201]) ).
fof(f3205,plain,
( h3(op1(e11,e13)) != op2(h3(e11),e23)
| spl20_36
| ~ spl20_105 ),
inference(forward_demodulation,[],[f597,f896]) ).
fof(f3207,plain,
( op2(e21,e23) != h3(op1(e11,e13))
| spl20_36
| ~ spl20_105
| ~ spl20_115 ),
inference(forward_demodulation,[],[f3205,f946]) ).
fof(f3209,plain,
( op2(e21,e23) != h3(e13)
| spl20_36
| ~ spl20_105
| ~ spl20_115
| ~ spl20_230 ),
inference(forward_demodulation,[],[f3207,f1565]) ).
fof(f3210,plain,
( e23 != op2(e21,e23)
| spl20_36
| ~ spl20_105
| ~ spl20_115
| ~ spl20_230 ),
inference(forward_demodulation,[],[f3209,f896]) ).
fof(f3214,plain,
( op2(e21,e21) != h3(op1(e11,e11))
| spl20_38
| ~ spl20_115 ),
inference(forward_demodulation,[],[f605,f946]) ).
fof(f3216,plain,
( op2(e21,e21) != h3(e10)
| spl20_38
| ~ spl20_115
| ~ spl20_176 ),
inference(forward_demodulation,[],[f3214,f1276]) ).
fof(f3218,plain,
( e20 != op2(e21,e21)
| spl20_38
| ~ spl20_46
| ~ spl20_115
| ~ spl20_176 ),
inference(forward_demodulation,[],[f3216,f639]) ).
fof(f3220,plain,
( $false
| spl20_38
| ~ spl20_46
| ~ spl20_115
| ~ spl20_156
| ~ spl20_176 ),
inference(forward_subsumption_resolution,[],[f3218,f1156]) ).
fof(f3221,plain,
( spl20_38
| ~ spl20_46
| ~ spl20_115
| ~ spl20_156
| ~ spl20_176 ),
inference(avatar_contradiction_clause,[],[f3220]) ).
fof(f3222,plain,
( h3(op1(e11,e12)) != op2(h3(e11),e22)
| spl20_37
| ~ spl20_110 ),
inference(forward_demodulation,[],[f601,f921]) ).
fof(f3224,plain,
( op2(e21,e22) != h3(op1(e11,e12))
| spl20_37
| ~ spl20_110
| ~ spl20_115 ),
inference(forward_demodulation,[],[f3222,f946]) ).
fof(f3226,plain,
( op2(e21,e22) != h3(e12)
| spl20_37
| ~ spl20_110
| ~ spl20_115
| ~ spl20_257 ),
inference(forward_demodulation,[],[f3224,f1683]) ).
fof(f3228,plain,
( e22 != op2(e21,e22)
| spl20_37
| ~ spl20_110
| ~ spl20_115
| ~ spl20_257 ),
inference(forward_demodulation,[],[f3226,f921]) ).
fof(f3232,plain,
( h3(op1(e10,e13)) != op2(h3(e10),e23)
| spl20_40
| ~ spl20_105 ),
inference(forward_demodulation,[],[f613,f896]) ).
fof(f3234,plain,
( op2(e20,e23) != h3(op1(e10,e13))
| spl20_40
| ~ spl20_46
| ~ spl20_105 ),
inference(forward_demodulation,[],[f3232,f639]) ).
fof(f3236,plain,
( op2(e20,e23) != h3(e10)
| spl20_40
| ~ spl20_46
| ~ spl20_105
| ~ spl20_249 ),
inference(forward_demodulation,[],[f3234,f1647]) ).
fof(f3238,plain,
( e20 != op2(e20,e23)
| spl20_40
| ~ spl20_46
| ~ spl20_105
| ~ spl20_249 ),
inference(forward_demodulation,[],[f3236,f639]) ).
fof(f3241,plain,
( h3(op1(e11,e10)) != op2(h3(e11),e20)
| spl20_39
| ~ spl20_46 ),
inference(forward_demodulation,[],[f609,f639]) ).
fof(f3243,plain,
( op2(e21,e20) != h3(op1(e11,e10))
| spl20_39
| ~ spl20_46
| ~ spl20_115 ),
inference(forward_demodulation,[],[f3241,f946]) ).
fof(f3245,plain,
( op2(e21,e20) != h3(e11)
| spl20_39
| ~ spl20_46
| ~ spl20_115
| ~ spl20_274 ),
inference(forward_demodulation,[],[f3243,f1762]) ).
fof(f3247,plain,
( e21 != op2(e21,e20)
| spl20_39
| ~ spl20_46
| ~ spl20_115
| ~ spl20_274 ),
inference(forward_demodulation,[],[f3245,f946]) ).
fof(f3249,plain,
( $false
| spl20_39
| ~ spl20_46
| ~ spl20_115
| ~ spl20_226
| ~ spl20_274 ),
inference(forward_subsumption_resolution,[],[f3247,f1522]) ).
fof(f3250,plain,
( spl20_39
| ~ spl20_46
| ~ spl20_115
| ~ spl20_226
| ~ spl20_274 ),
inference(avatar_contradiction_clause,[],[f3249]) ).
fof(f3252,plain,
( h3(op1(e10,e11)) != op2(h3(e10),e21)
| spl20_42
| ~ spl20_115 ),
inference(forward_demodulation,[],[f621,f946]) ).
fof(f3254,plain,
( op2(e20,e21) != h3(op1(e10,e11))
| spl20_42
| ~ spl20_46
| ~ spl20_115 ),
inference(forward_demodulation,[],[f3252,f639]) ).
fof(f3256,plain,
( op2(e20,e21) != h3(e13)
| spl20_42
| ~ spl20_46
| ~ spl20_115
| ~ spl20_269 ),
inference(forward_demodulation,[],[f3254,f1737]) ).
fof(f3258,plain,
( e23 != op2(e20,e21)
| spl20_42
| ~ spl20_46
| ~ spl20_105
| ~ spl20_115
| ~ spl20_269 ),
inference(forward_demodulation,[],[f3256,f896]) ).
fof(f3261,plain,
( h3(op1(e10,e12)) != op2(h3(e10),e22)
| spl20_41
| ~ spl20_110 ),
inference(forward_demodulation,[],[f617,f921]) ).
fof(f3263,plain,
( op2(e20,e22) != h3(op1(e10,e12))
| spl20_41
| ~ spl20_46
| ~ spl20_110 ),
inference(forward_demodulation,[],[f3261,f639]) ).
fof(f3265,plain,
( op2(e20,e22) != h3(e11)
| spl20_41
| ~ spl20_46
| ~ spl20_110
| ~ spl20_262 ),
inference(forward_demodulation,[],[f3263,f1705]) ).
fof(f3267,plain,
( e21 != op2(e20,e22)
| spl20_41
| ~ spl20_46
| ~ spl20_110
| ~ spl20_115
| ~ spl20_262 ),
inference(forward_demodulation,[],[f3265,f946]) ).
fof(f3269,plain,
( $false
| spl20_41
| ~ spl20_46
| ~ spl20_110
| ~ spl20_115
| ~ spl20_214
| ~ spl20_262 ),
inference(forward_subsumption_resolution,[],[f3267,f1465]) ).
fof(f3270,plain,
( spl20_41
| ~ spl20_46
| ~ spl20_110
| ~ spl20_115
| ~ spl20_214
| ~ spl20_262 ),
inference(avatar_contradiction_clause,[],[f3269]) ).
fof(f3272,plain,
( op2(e20,e20) != h3(op1(e10,e10))
| spl20_43
| ~ spl20_46 ),
inference(forward_demodulation,[],[f625,f639]) ).
fof(f3274,plain,
( op2(e20,e20) != h3(e12)
| spl20_43
| ~ spl20_46
| ~ spl20_173 ),
inference(forward_demodulation,[],[f3272,f1261]) ).
fof(f3276,plain,
( op2(e20,e20) != e22
| spl20_43
| ~ spl20_46
| ~ spl20_110
| ~ spl20_173 ),
inference(forward_demodulation,[],[f3274,f921]) ).
fof(f3278,plain,
( $false
| spl20_43
| ~ spl20_46
| ~ spl20_110
| ~ spl20_153
| ~ spl20_173 ),
inference(forward_subsumption_resolution,[],[f3276,f1141]) ).
fof(f3279,plain,
( spl20_43
| ~ spl20_46
| ~ spl20_110
| ~ spl20_153
| ~ spl20_173 ),
inference(avatar_contradiction_clause,[],[f3278]) ).
fof(f3284,plain,
( ~ spl20_221
| spl20_42
| ~ spl20_46
| ~ spl20_105
| ~ spl20_115
| ~ spl20_269 ),
inference(avatar_split_clause,[],[f3258,f1735,f945,f895,f638,f619,f1495]) ).
fof(f3294,plain,
( ~ spl20_227
| ~ spl20_156 ),
inference(avatar_split_clause,[],[f3065,f1155,f1525]) ).
fof(f3317,plain,
( ~ spl20_215
| spl20_34
| ~ spl20_110
| ~ spl20_115
| ~ spl20_263 ),
inference(avatar_split_clause,[],[f3134,f1708,f945,f920,f587,f1468]) ).
fof(f3333,plain,
( ~ spl20_207
| ~ spl20_145 ),
inference(avatar_split_clause,[],[f2808,f1096,f1432]) ).
fof(f3360,plain,
( ~ spl20_182
| spl20_36
| ~ spl20_105
| ~ spl20_115
| ~ spl20_230 ),
inference(avatar_split_clause,[],[f3210,f1563,f945,f895,f595,f1323]) ).
fof(f3368,plain,
( e21 != op2(e21,e22)
| ~ spl20_226 ),
inference(forward_demodulation,[],[f224,f1522]) ).
fof(f3372,plain,
( ~ spl20_205
| ~ spl20_145 ),
inference(avatar_split_clause,[],[f2846,f1096,f1423]) ).
fof(f3373,plain,
( e23 != op2(e22,e23)
| ~ spl20_145 ),
inference(forward_demodulation,[],[f214,f1098]) ).
fof(f3374,plain,
( e20 != op2(e22,e23)
| ~ spl20_201 ),
inference(forward_demodulation,[],[f236,f1407]) ).
fof(f3375,plain,
( e21 != op2(e22,e23)
| ~ spl20_143 ),
inference(forward_demodulation,[],[f232,f1088]) ).
fof(f3388,plain,
( ~ spl20_213
| ~ spl20_226 ),
inference(avatar_split_clause,[],[f3368,f1520,f1459]) ).
fof(f3391,plain,
( ~ spl20_181
| ~ spl20_145 ),
inference(avatar_split_clause,[],[f3373,f1096,f1319]) ).
fof(f3392,plain,
( ~ spl20_199
| ~ spl20_201 ),
inference(avatar_split_clause,[],[f3374,f1405,f1397]) ).
fof(f3393,plain,
( ~ spl20_193
| ~ spl20_143 ),
inference(avatar_split_clause,[],[f3375,f1087,f1371]) ).
fof(f3406,plain,
( ~ spl20_187
| spl20_32
| ~ spl20_105
| ~ spl20_110
| ~ spl20_235 ),
inference(avatar_split_clause,[],[f3172,f1585,f920,f895,f579,f1345]) ).
fof(f3442,plain,
( ~ spl20_201
| spl20_40
| ~ spl20_46
| ~ spl20_105
| ~ spl20_249 ),
inference(avatar_split_clause,[],[f3238,f1645,f895,f638,f611,f1405]) ).
fof(f3443,plain,
( e22 = e23
| ~ spl20_147
| ~ spl20_153 ),
inference(forward_demodulation,[],[f1109,f1141]) ).
fof(f3449,plain,
( $false
| ~ spl20_147
| ~ spl20_153 ),
inference(forward_subsumption_resolution,[],[f3443,f262]) ).
fof(f3450,plain,
( ~ spl20_147
| ~ spl20_153 ),
inference(avatar_contradiction_clause,[],[f3449]) ).
fof(f3466,plain,
( ~ spl20_220
| spl20_35
| ~ spl20_46
| ~ spl20_110
| ~ spl20_268 ),
inference(avatar_split_clause,[],[f3192,f1730,f920,f638,f591,f1490]) ).
fof(f3476,plain,
( ~ spl20_209
| spl20_37
| ~ spl20_110
| ~ spl20_115
| ~ spl20_257 ),
inference(avatar_split_clause,[],[f3228,f1681,f945,f920,f599,f1441]) ).
fof(f3489,plain,
( e20 = e22
| ~ spl20_153
| ~ spl20_159 ),
inference(forward_demodulation,[],[f1176,f1141]) ).
fof(f3494,plain,
( ~ spl20_186
| ~ spl20_185 ),
inference(avatar_split_clause,[],[f2804,f1336,f1340]) ).
fof(f3501,plain,
( ~ spl20_186
| ~ spl20_222 ),
inference(avatar_split_clause,[],[f2919,f1500,f1340]) ).
fof(f3505,plain,
( ~ spl20_218
| ~ spl20_202 ),
inference(avatar_split_clause,[],[f3059,f1410,f1481]) ).
fof(f3511,plain,
( ~ spl20_198
| ~ spl20_143 ),
inference(avatar_split_clause,[],[f3030,f1087,f1392]) ).
fof(f3512,plain,
( ~ spl20_204
| ~ spl20_202 ),
inference(avatar_split_clause,[],[f3036,f1410,f1418]) ).
fof(f3513,plain,
( e22 != op2(e23,e20)
| ~ spl20_153 ),
inference(forward_demodulation,[],[f253,f1141]) ).
fof(f3542,plain,
( $false
| ~ spl20_153
| ~ spl20_159 ),
inference(forward_subsumption_resolution,[],[f3489,f266]) ).
fof(f3543,plain,
( ~ spl20_153
| ~ spl20_159 ),
inference(avatar_contradiction_clause,[],[f3542]) ).
fof(f3545,plain,
( ~ spl20_192
| ~ spl20_153 ),
inference(avatar_split_clause,[],[f3513,f1139,f1366]) ).
fof(f3602,plain,
( e11 = e13
| ~ spl20_163
| ~ spl20_180 ),
inference(forward_demodulation,[],[f1308,f1208]) ).
fof(f3618,plain,
( e12 != op1(e11,e13)
| ~ spl20_257 ),
inference(forward_demodulation,[],[f172,f1683]) ).
fof(f3619,plain,
( e10 != op1(e11,e13)
| ~ spl20_176 ),
inference(forward_demodulation,[],[f173,f1276]) ).
fof(f3621,plain,
( ~ spl20_242
| ~ spl20_163 ),
inference(avatar_split_clause,[],[f2756,f1207,f1615]) ).
fof(f3652,plain,
( $false
| ~ spl20_163
| ~ spl20_180 ),
inference(forward_subsumption_resolution,[],[f3602,f257]) ).
fof(f3653,plain,
( ~ spl20_163
| ~ spl20_180 ),
inference(avatar_contradiction_clause,[],[f3652]) ).
fof(f3656,plain,
( ~ spl20_236
| ~ spl20_257 ),
inference(avatar_split_clause,[],[f3618,f1681,f1589]) ).
fof(f3657,plain,
( ~ spl20_248
| ~ spl20_176 ),
inference(avatar_split_clause,[],[f3619,f1275,f1641]) ).
fof(f3695,plain,
( ~ spl20_246
| ~ spl20_163 ),
inference(avatar_split_clause,[],[f2719,f1207,f1632]) ).
fof(f3696,plain,
( ~ spl20_252
| ~ spl20_250 ),
inference(avatar_split_clause,[],[f2721,f1650,f1658]) ).
fof(f3700,plain,
( e12 != op1(e13,e10)
| ~ spl20_173 ),
inference(forward_demodulation,[],[f205,f1261]) ).
fof(f3709,plain,
( ~ spl20_240
| ~ spl20_173 ),
inference(avatar_split_clause,[],[f3700,f1259,f1606]) ).
fof(f3726,plain,
( e10 != op1(e13,e13)
| ~ spl20_250 ),
inference(forward_demodulation,[],[f160,f1652]) ).
fof(f3729,plain,
( spl20_163
| ~ spl20_165 ),
inference(avatar_split_clause,[],[f3086,f1216,f1207]) ).
fof(f3737,plain,
( ~ spl20_164
| ~ spl20_250 ),
inference(avatar_split_clause,[],[f3726,f1650,f1211]) ).
fof(f3752,plain,
( ~ spl20_276
| ~ spl20_176 ),
inference(avatar_split_clause,[],[f2740,f1275,f1770]) ).
fof(f3754,plain,
( ~ spl20_275
| ~ spl20_176 ),
inference(avatar_split_clause,[],[f2782,f1275,f1765]) ).
fof(f3768,plain,
( ~ spl20_255
| ~ spl20_165 ),
inference(avatar_split_clause,[],[f2728,f1216,f1672]) ).
fof(f3769,plain,
( e12 != op1(e10,e12)
| ~ spl20_173 ),
inference(forward_demodulation,[],[f182,f1261]) ).
fof(f3770,plain,
( ~ spl20_266
| ~ spl20_250 ),
inference(avatar_split_clause,[],[f2769,f1650,f1721]) ).
fof(f3778,plain,
( ~ spl20_258
| ~ spl20_173 ),
inference(avatar_split_clause,[],[f3769,f1259,f1685]) ).
fof(f3782,plain,
( spl20_250
| ~ spl20_165 ),
inference(avatar_split_clause,[],[f2872,f1216,f1650]) ).
fof(f3786,plain,
( ~ spl20_241
| ~ spl20_163 ),
inference(avatar_split_clause,[],[f2754,f1207,f1611]) ).
cnf(s8,plain,
( spl20_24
| spl20_25
| spl20_26
| ~ spl20_28
| ~ spl20_29
| ~ spl20_30
| ~ spl20_31
| ~ spl20_32
| ~ spl20_33
| ~ spl20_34
| ~ spl20_35
| ~ spl20_36
| ~ spl20_37
| ~ spl20_38
| ~ spl20_39
| ~ spl20_40
| ~ spl20_41
| ~ spl20_42
| ~ spl20_43
| ~ spl20_46 ),
inference(sat_conversion,[],[f641]) ).
cnf(s29,plain,
( ~ spl20_24
| ~ spl20_105 ),
inference(sat_conversion,[],[f898]) ).
cnf(s34,plain,
( ~ spl20_25
| ~ spl20_110 ),
inference(sat_conversion,[],[f923]) ).
cnf(s39,plain,
( ~ spl20_26
| ~ spl20_115 ),
inference(sat_conversion,[],[f948]) ).
cnf(s66,plain,
spl20_110,
inference(sat_conversion,[],[f1075]) ).
cnf(s75,plain,
( spl20_141
| ~ spl20_142
| spl20_146
| spl20_147 ),
inference(sat_conversion,[],[f1112]) ).
cnf(s83,plain,
( spl20_148
| ~ spl20_149
| spl20_152
| spl20_153 ),
inference(sat_conversion,[],[f1144]) ).
cnf(s84,plain,
( spl20_148
| spl20_149
| spl20_152
| spl20_153 ),
inference(sat_conversion,[],[f1145]) ).
cnf(s86,plain,
( spl20_150
| spl20_154
| ~ spl20_155
| ~ spl20_156 ),
inference(sat_conversion,[],[f1159]) ).
cnf(s88,plain,
( spl20_150
| spl20_154
| spl20_155
| ~ spl20_156 ),
inference(sat_conversion,[],[f1161]) ).
cnf(s96,plain,
( spl20_151
| spl20_156
| spl20_158
| ~ spl20_159 ),
inference(sat_conversion,[],[f1181]) ).
cnf(s100,plain,
( spl20_151
| spl20_156
| spl20_158
| spl20_159 ),
inference(sat_conversion,[],[f1185]) ).
cnf(s102,plain,
( ~ spl20_141
| spl20_160 ),
inference(sat_conversion,[],[f1191]) ).
cnf(s103,plain,
( ~ spl20_145
| ~ spl20_148 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s105,plain,
( ~ spl20_146
| ~ spl20_154 ),
inference(sat_conversion,[],[f1194]) ).
cnf(s106,plain,
( spl20_143
| ~ spl20_154 ),
inference(sat_conversion,[],[f1195]) ).
cnf(s108,plain,
( spl20_144
| ~ spl20_158 ),
inference(sat_conversion,[],[f1197]) ).
cnf(s113,plain,
( spl20_161
| ~ spl20_162
| ~ spl20_163
| spl20_167 ),
inference(sat_conversion,[],[f1230]) ).
cnf(s124,plain,
( spl20_168
| spl20_169
| spl20_172
| spl20_173 ),
inference(sat_conversion,[],[f1265]) ).
cnf(s136,plain,
( spl20_171
| spl20_176
| spl20_178
| ~ spl20_179 ),
inference(sat_conversion,[],[f1301]) ).
cnf(s140,plain,
( spl20_171
| spl20_176
| spl20_178
| spl20_179 ),
inference(sat_conversion,[],[f1305]) ).
cnf(s142,plain,
( ~ spl20_161
| spl20_180 ),
inference(sat_conversion,[],[f1311]) ).
cnf(s143,plain,
( ~ spl20_165
| ~ spl20_168 ),
inference(sat_conversion,[],[f1312]) ).
cnf(s148,plain,
( spl20_164
| ~ spl20_178 ),
inference(sat_conversion,[],[f1317]) ).
cnf(s152,plain,
( spl20_142
| spl20_190
| spl20_191
| spl20_192 ),
inference(sat_conversion,[],[f1369]) ).
cnf(s161,plain,
( spl20_150
| spl20_196
| spl20_213
| spl20_214 ),
inference(sat_conversion,[],[f1466]) ).
cnf(s162,plain,
( spl20_150
| spl20_193
| spl20_215
| spl20_216 ),
inference(sat_conversion,[],[f1475]) ).
cnf(s165,plain,
( spl20_146
| spl20_185
| spl20_207
| spl20_221 ),
inference(sat_conversion,[],[f1498]) ).
cnf(s166,plain,
( spl20_146
| spl20_182
| spl20_205
| spl20_222 ),
inference(sat_conversion,[],[f1503]) ).
cnf(s179,plain,
( spl20_159
| spl20_204
| spl20_220
| spl20_228 ),
inference(sat_conversion,[],[f1540]) ).
cnf(s180,plain,
( spl20_159
| spl20_201
| spl20_218
| spl20_227 ),
inference(sat_conversion,[],[f1541]) ).
cnf(s184,plain,
( spl20_186
| spl20_192
| spl20_198
| spl20_204 ),
inference(sat_conversion,[],[f1545]) ).
cnf(s185,plain,
( spl20_181
| spl20_187
| spl20_193
| spl20_199 ),
inference(sat_conversion,[],[f1546]) ).
cnf(s190,plain,
( spl20_205
| spl20_209
| spl20_213
| spl20_217 ),
inference(sat_conversion,[],[f1551]) ).
cnf(s192,plain,
( spl20_222
| spl20_224
| spl20_226
| spl20_228 ),
inference(sat_conversion,[],[f1553]) ).
cnf(s199,plain,
( spl20_162
| spl20_235
| spl20_236
| spl20_237 ),
inference(sat_conversion,[],[f1596]) ).
cnf(s200,plain,
( spl20_162
| spl20_238
| spl20_239
| spl20_240 ),
inference(sat_conversion,[],[f1609]) ).
cnf(s207,plain,
( spl20_169
| spl20_238
| spl20_257
| spl20_258 ),
inference(sat_conversion,[],[f1688]) ).
cnf(s209,plain,
( spl20_170
| spl20_244
| spl20_261
| spl20_262 ),
inference(sat_conversion,[],[f1706]) ).
cnf(s210,plain,
( spl20_170
| spl20_241
| spl20_263
| spl20_264 ),
inference(sat_conversion,[],[f1715]) ).
cnf(s213,plain,
( spl20_166
| spl20_233
| spl20_255
| spl20_269 ),
inference(sat_conversion,[],[f1738]) ).
cnf(s218,plain,
( spl20_175
| spl20_242
| spl20_261
| spl20_274 ),
inference(sat_conversion,[],[f1763]) ).
cnf(s227,plain,
( spl20_179
| spl20_252
| spl20_268
| spl20_276 ),
inference(sat_conversion,[],[f1780]) ).
cnf(s228,plain,
( spl20_179
| spl20_249
| spl20_266
| spl20_275 ),
inference(sat_conversion,[],[f1781]) ).
cnf(s232,plain,
( spl20_234
| spl20_240
| spl20_246
| spl20_252 ),
inference(sat_conversion,[],[f1785]) ).
cnf(s237,plain,
( spl20_230
| spl20_236
| spl20_242
| spl20_248 ),
inference(sat_conversion,[],[f1790]) ).
cnf(s245,plain,
spl20_165,
inference(sat_conversion,[],[f1798]) ).
cnf(s246,plain,
spl20_145,
inference(sat_conversion,[],[f1799]) ).
cnf(s250,plain,
( ~ spl20_145
| ~ spl20_151 ),
inference(sat_conversion,[],[f1816]) ).
cnf(s258,plain,
( ~ spl20_165
| ~ spl20_171 ),
inference(sat_conversion,[],[f1858]) ).
cnf(s261,plain,
( ~ spl20_175
| ~ spl20_176 ),
inference(sat_conversion,[],[f1874]) ).
cnf(s262,plain,
( ~ spl20_173
| ~ spl20_179 ),
inference(sat_conversion,[],[f1879]) ).
cnf(s264,plain,
( ~ spl20_172
| ~ spl20_176 ),
inference(sat_conversion,[],[f1886]) ).
cnf(s295,plain,
( ~ spl20_196
| ~ spl20_202 ),
inference(sat_conversion,[],[f2015]) ).
cnf(s330,plain,
( ~ spl20_190
| ~ spl20_202 ),
inference(sat_conversion,[],[f2182]) ).
cnf(s347,plain,
( ~ spl20_233
| ~ spl20_239 ),
inference(sat_conversion,[],[f2265]) ).
cnf(s354,plain,
( ~ spl20_244
| ~ spl20_250 ),
inference(sat_conversion,[],[f2299]) ).
cnf(s360,plain,
( ~ spl20_167
| ~ spl20_173 ),
inference(sat_conversion,[],[f2323]) ).
cnf(s361,plain,
( ~ spl20_166
| ~ spl20_176 ),
inference(sat_conversion,[],[f2328]) ).
cnf(s364,plain,
( ~ spl20_165
| ~ spl20_170 ),
inference(sat_conversion,[],[f2340]) ).
cnf(s381,plain,
( ~ spl20_237
| ~ spl20_249 ),
inference(sat_conversion,[],[f2412]) ).
cnf(s389,plain,
( ~ spl20_264
| ~ spl20_268 ),
inference(sat_conversion,[],[f2454]) ).
cnf(s406,plain,
( ~ spl20_257
| ~ spl20_261 ),
inference(sat_conversion,[],[f2544]) ).
cnf(s415,plain,
( ~ spl20_165
| ~ spl20_169 ),
inference(sat_conversion,[],[f2592]) ).
cnf(s416,plain,
( ~ spl20_238
| ~ spl20_250 ),
inference(sat_conversion,[],[f2609]) ).
cnf(s437,plain,
( spl20_105
| ~ spl20_145 ),
inference(sat_conversion,[],[f2709]) ).
cnf(s439,plain,
( ~ spl20_145
| spl20_202 ),
inference(sat_conversion,[],[f2874]) ).
cnf(s442,plain,
( ~ spl20_152
| ~ spl20_156 ),
inference(sat_conversion,[],[f2893]) ).
cnf(s444,plain,
( ~ spl20_216
| ~ spl20_220 ),
inference(sat_conversion,[],[f2897]) ).
cnf(s445,plain,
( ~ spl20_202
| ~ spl20_217 ),
inference(sat_conversion,[],[f2898]) ).
cnf(s456,plain,
( ~ spl20_144
| ~ spl20_202 ),
inference(sat_conversion,[],[f2911]) ).
cnf(s469,plain,
( ~ spl20_145
| ~ spl20_150 ),
inference(sat_conversion,[],[f2938]) ).
cnf(s474,plain,
( ~ spl20_153
| ~ spl20_224 ),
inference(sat_conversion,[],[f2980]) ).
cnf(s476,plain,
( ~ spl20_156
| ~ spl20_228 ),
inference(sat_conversion,[],[f2982]) ).
cnf(s485,plain,
( ~ spl20_143
| ~ spl20_160 ),
inference(sat_conversion,[],[f3034]) ).
cnf(s488,plain,
( spl20_46
| ~ spl20_145
| ~ spl20_202 ),
inference(sat_conversion,[],[f3077]) ).
cnf(s497,plain,
( spl20_115
| ~ spl20_143
| ~ spl20_145 ),
inference(sat_conversion,[],[f3127]) ).
cnf(s500,plain,
( spl20_28
| ~ spl20_105
| ~ spl20_115
| ~ spl20_143
| ~ spl20_163 ),
inference(sat_conversion,[],[f3144]) ).
cnf(s501,plain,
( spl20_30
| ~ spl20_105
| ~ spl20_110
| ~ spl20_115
| ~ spl20_191
| ~ spl20_239 ),
inference(sat_conversion,[],[f3154]) ).
cnf(s502,plain,
( spl20_29
| ~ spl20_46
| ~ spl20_105
| ~ spl20_110
| ~ spl20_202
| ~ spl20_250 ),
inference(sat_conversion,[],[f3164]) ).
cnf(s504,plain,
( spl20_31
| ~ spl20_46
| ~ spl20_105
| ~ spl20_186
| ~ spl20_234 ),
inference(sat_conversion,[],[f3184]) ).
cnf(s506,plain,
( spl20_33
| ~ spl20_105
| ~ spl20_110
| ~ spl20_145
| ~ spl20_165 ),
inference(sat_conversion,[],[f3202]) ).
cnf(s508,plain,
( spl20_38
| ~ spl20_46
| ~ spl20_115
| ~ spl20_156
| ~ spl20_176 ),
inference(sat_conversion,[],[f3221]) ).
cnf(s511,plain,
( spl20_39
| ~ spl20_46
| ~ spl20_115
| ~ spl20_226
| ~ spl20_274 ),
inference(sat_conversion,[],[f3250]) ).
cnf(s513,plain,
( spl20_41
| ~ spl20_46
| ~ spl20_110
| ~ spl20_115
| ~ spl20_214
| ~ spl20_262 ),
inference(sat_conversion,[],[f3270]) ).
cnf(s514,plain,
( spl20_43
| ~ spl20_46
| ~ spl20_110
| ~ spl20_153
| ~ spl20_173 ),
inference(sat_conversion,[],[f3279]) ).
cnf(s515,plain,
( spl20_42
| ~ spl20_46
| ~ spl20_105
| ~ spl20_115
| ~ spl20_221
| ~ spl20_269 ),
inference(sat_conversion,[],[f3284]) ).
cnf(s520,plain,
( ~ spl20_156
| ~ spl20_227 ),
inference(sat_conversion,[],[f3294]) ).
cnf(s530,plain,
( spl20_34
| ~ spl20_110
| ~ spl20_115
| ~ spl20_215
| ~ spl20_263 ),
inference(sat_conversion,[],[f3317]) ).
cnf(s534,plain,
( ~ spl20_145
| ~ spl20_207 ),
inference(sat_conversion,[],[f3333]) ).
cnf(s549,plain,
( spl20_36
| ~ spl20_105
| ~ spl20_115
| ~ spl20_182
| ~ spl20_230 ),
inference(sat_conversion,[],[f3360]) ).
cnf(s554,plain,
( ~ spl20_145
| ~ spl20_205 ),
inference(sat_conversion,[],[f3372]) ).
cnf(s557,plain,
( ~ spl20_213
| ~ spl20_226 ),
inference(sat_conversion,[],[f3388]) ).
cnf(s560,plain,
( ~ spl20_145
| ~ spl20_181 ),
inference(sat_conversion,[],[f3391]) ).
cnf(s561,plain,
( ~ spl20_199
| ~ spl20_201 ),
inference(sat_conversion,[],[f3392]) ).
cnf(s562,plain,
( ~ spl20_143
| ~ spl20_193 ),
inference(sat_conversion,[],[f3393]) ).
cnf(s572,plain,
( spl20_32
| ~ spl20_105
| ~ spl20_110
| ~ spl20_187
| ~ spl20_235 ),
inference(sat_conversion,[],[f3406]) ).
cnf(s585,plain,
( spl20_40
| ~ spl20_46
| ~ spl20_105
| ~ spl20_201
| ~ spl20_249 ),
inference(sat_conversion,[],[f3442]) ).
cnf(s588,plain,
( ~ spl20_147
| ~ spl20_153 ),
inference(sat_conversion,[],[f3450]) ).
cnf(s599,plain,
( spl20_35
| ~ spl20_46
| ~ spl20_110
| ~ spl20_220
| ~ spl20_268 ),
inference(sat_conversion,[],[f3466]) ).
cnf(s604,plain,
( spl20_37
| ~ spl20_110
| ~ spl20_115
| ~ spl20_209
| ~ spl20_257 ),
inference(sat_conversion,[],[f3476]) ).
cnf(s612,plain,
( ~ spl20_185
| ~ spl20_186 ),
inference(sat_conversion,[],[f3494]) ).
cnf(s616,plain,
( ~ spl20_186
| ~ spl20_222 ),
inference(sat_conversion,[],[f3501]) ).
cnf(s619,plain,
( ~ spl20_202
| ~ spl20_218 ),
inference(sat_conversion,[],[f3505]) ).
cnf(s624,plain,
( ~ spl20_143
| ~ spl20_198 ),
inference(sat_conversion,[],[f3511]) ).
cnf(s625,plain,
( ~ spl20_202
| ~ spl20_204 ),
inference(sat_conversion,[],[f3512]) ).
cnf(s632,plain,
( ~ spl20_153
| ~ spl20_159 ),
inference(sat_conversion,[],[f3543]) ).
cnf(s634,plain,
( ~ spl20_153
| ~ spl20_192 ),
inference(sat_conversion,[],[f3545]) ).
cnf(s709,plain,
( ~ spl20_163
| ~ spl20_242 ),
inference(sat_conversion,[],[f3621]) ).
cnf(s716,plain,
( ~ spl20_163
| ~ spl20_180 ),
inference(sat_conversion,[],[f3653]) ).
cnf(s718,plain,
( ~ spl20_236
| ~ spl20_257 ),
inference(sat_conversion,[],[f3656]) ).
cnf(s719,plain,
( ~ spl20_176
| ~ spl20_248 ),
inference(sat_conversion,[],[f3657]) ).
cnf(s753,plain,
( ~ spl20_163
| ~ spl20_246 ),
inference(sat_conversion,[],[f3695]) ).
cnf(s754,plain,
( ~ spl20_250
| ~ spl20_252 ),
inference(sat_conversion,[],[f3696]) ).
cnf(s760,plain,
( ~ spl20_173
| ~ spl20_240 ),
inference(sat_conversion,[],[f3709]) ).
cnf(s768,plain,
( spl20_163
| ~ spl20_165 ),
inference(sat_conversion,[],[f3729]) ).
cnf(s772,plain,
( ~ spl20_164
| ~ spl20_250 ),
inference(sat_conversion,[],[f3737]) ).
cnf(s778,plain,
( ~ spl20_176
| ~ spl20_276 ),
inference(sat_conversion,[],[f3752]) ).
cnf(s780,plain,
( ~ spl20_176
| ~ spl20_275 ),
inference(sat_conversion,[],[f3754]) ).
cnf(s794,plain,
( ~ spl20_165
| ~ spl20_255 ),
inference(sat_conversion,[],[f3768]) ).
cnf(s795,plain,
( ~ spl20_250
| ~ spl20_266 ),
inference(sat_conversion,[],[f3770]) ).
cnf(s801,plain,
( ~ spl20_173
| ~ spl20_258 ),
inference(sat_conversion,[],[f3778]) ).
cnf(s803,plain,
( ~ spl20_165
| spl20_250 ),
inference(sat_conversion,[],[f3782]) ).
cnf(s805,plain,
( ~ spl20_163
| ~ spl20_241 ),
inference(sat_conversion,[],[f3786]) ).
cnf(s808,plain,
~ spl20_181,
inference(rat,[],[s560,s246]) ).
cnf(s809,plain,
~ spl20_205,
inference(rat,[],[s554,s246]) ).
cnf(s810,plain,
~ spl20_207,
inference(rat,[],[s534,s246]) ).
cnf(s811,plain,
~ spl20_150,
inference(rat,[],[s469,s246]) ).
cnf(s812,plain,
spl20_202,
inference(rat,[],[s439,s246]) ).
cnf(s813,plain,
spl20_105,
inference(rat,[],[s437,s246]) ).
cnf(s814,plain,
~ spl20_151,
inference(rat,[],[s250,s246]) ).
cnf(s815,plain,
~ spl20_204,
inference(rat,[],[s625,s812]) ).
cnf(s817,plain,
~ spl20_218,
inference(rat,[],[s619,s812]) ).
cnf(s818,plain,
~ spl20_144,
inference(rat,[],[s456,s812]) ).
cnf(s819,plain,
~ spl20_217,
inference(rat,[],[s445,s812]) ).
cnf(s820,plain,
~ spl20_190,
inference(rat,[],[s330,s812]) ).
cnf(s822,plain,
~ spl20_196,
inference(rat,[],[s295,s812]) ).
cnf(s823,plain,
spl20_46,
inference(rat,[],[s488,s246,s812]) ).
cnf(s826,plain,
spl20_250,
inference(rat,[],[s803,s245]) ).
cnf(s828,plain,
~ spl20_255,
inference(rat,[],[s794,s245]) ).
cnf(s830,plain,
spl20_163,
inference(rat,[],[s768,s245]) ).
cnf(s831,plain,
~ spl20_169,
inference(rat,[],[s415,s245]) ).
cnf(s832,plain,
~ spl20_170,
inference(rat,[],[s364,s245]) ).
cnf(s833,plain,
~ spl20_171,
inference(rat,[],[s258,s245]) ).
cnf(s835,plain,
~ spl20_266,
inference(rat,[],[s795,s826]) ).
cnf(s836,plain,
~ spl20_164,
inference(rat,[],[s772,s826]) ).
cnf(s837,plain,
~ spl20_252,
inference(rat,[],[s754,s826]) ).
cnf(s838,plain,
~ spl20_238,
inference(rat,[],[s416,s826]) ).
cnf(s839,plain,
~ spl20_244,
inference(rat,[],[s354,s826]) ).
cnf(s840,plain,
~ spl20_241,
inference(rat,[],[s805,s830]) ).
cnf(s843,plain,
~ spl20_246,
inference(rat,[],[s753,s830]) ).
cnf(s844,plain,
~ spl20_180,
inference(rat,[],[s716,s830]) ).
cnf(s845,plain,
~ spl20_242,
inference(rat,[],[s709,s830]) ).
cnf(s849,plain,
( spl20_230
| spl20_236
| spl20_248 ),
inference(rat,[],[s237,s845]) ).
cnf(s853,plain,
( spl20_234
| spl20_240 ),
inference(rat,[],[s232,s837,s843]) ).
cnf(s855,plain,
( spl20_179
| spl20_249
| spl20_275 ),
inference(rat,[],[s228,s835]) ).
cnf(s856,plain,
( spl20_179
| spl20_268
| spl20_276 ),
inference(rat,[],[s227,s837]) ).
cnf(s861,plain,
( spl20_175
| spl20_261
| spl20_274 ),
inference(rat,[],[s218,s845]) ).
cnf(s864,plain,
( spl20_166
| spl20_233
| spl20_269 ),
inference(rat,[],[s213,s828]) ).
cnf(s866,plain,
( spl20_263
| spl20_264 ),
inference(rat,[],[s210,s840,s832]) ).
cnf(s867,plain,
( spl20_261
| spl20_262 ),
inference(rat,[],[s209,s839,s832]) ).
cnf(s869,plain,
( spl20_257
| spl20_258 ),
inference(rat,[],[s207,s838,s831]) ).
cnf(s871,plain,
( spl20_162
| spl20_239
| spl20_240 ),
inference(rat,[],[s200,s838]) ).
cnf(s875,plain,
( spl20_209
| spl20_213 ),
inference(rat,[],[s190,s819,s809]) ).
cnf(s877,plain,
( spl20_187
| spl20_193
| spl20_199 ),
inference(rat,[],[s185,s808]) ).
cnf(s878,plain,
( spl20_186
| spl20_192
| spl20_198 ),
inference(rat,[],[s184,s815]) ).
cnf(s881,plain,
( spl20_159
| spl20_201
| spl20_227 ),
inference(rat,[],[s180,s817]) ).
cnf(s882,plain,
( spl20_159
| spl20_220
| spl20_228 ),
inference(rat,[],[s179,s815]) ).
cnf(s885,plain,
( spl20_146
| spl20_182
| spl20_222 ),
inference(rat,[],[s166,s809]) ).
cnf(s886,plain,
( spl20_146
| spl20_185
| spl20_221 ),
inference(rat,[],[s165,s810]) ).
cnf(s888,plain,
( spl20_193
| spl20_215
| spl20_216 ),
inference(rat,[],[s162,s811]) ).
cnf(s889,plain,
( spl20_213
| spl20_214 ),
inference(rat,[],[s161,s822,s811]) ).
cnf(s893,plain,
( spl20_142
| spl20_191
| spl20_192 ),
inference(rat,[],[s152,s820]) ).
cnf(s896,plain,
~ spl20_178,
inference(rat,[],[s148,s836]) ).
cnf(s897,plain,
~ spl20_168,
inference(rat,[],[s143,s245]) ).
cnf(s898,plain,
~ spl20_161,
inference(rat,[],[s142,s844]) ).
cnf(s899,plain,
( spl20_176
| spl20_179 ),
inference(rat,[],[s140,s896,s833]) ).
cnf(s903,plain,
( spl20_176
| ~ spl20_179 ),
inference(rat,[],[s136,s896,s833]) ).
cnf(s911,plain,
( spl20_172
| spl20_173 ),
inference(rat,[],[s124,s831,s897]) ).
cnf(s913,plain,
( ~ spl20_162
| spl20_167 ),
inference(rat,[],[s113,s830,s898]) ).
cnf(s914,plain,
~ spl20_158,
inference(rat,[],[s108,s818]) ).
cnf(s915,plain,
~ spl20_148,
inference(rat,[],[s103,s246]) ).
cnf(s916,plain,
( spl20_156
| spl20_159 ),
inference(rat,[],[s100,s914,s814]) ).
cnf(s920,plain,
( spl20_156
| ~ spl20_159 ),
inference(rat,[],[s96,s914,s814]) ).
cnf(s926,plain,
( spl20_154
| spl20_155
| ~ spl20_156 ),
inference(rat,[],[s88,s811]) ).
cnf(s927,plain,
( spl20_154
| ~ spl20_155
| ~ spl20_156 ),
inference(rat,[],[s86,s811]) ).
cnf(s928,plain,
( spl20_149
| spl20_152
| spl20_153 ),
inference(rat,[],[s84,s915]) ).
cnf(s929,plain,
( ~ spl20_149
| spl20_152
| spl20_153 ),
inference(rat,[],[s83,s915]) ).
cnf(s930,plain,
spl20_33,
inference(rat,[],[s506,s245,s246,s813,s66]) ).
cnf(s931,plain,
spl20_29,
inference(rat,[],[s502,s826,s812,s823,s813,s66]) ).
cnf(s933,plain,
~ spl20_25,
inference(rat,[],[s34,s66]) ).
cnf(s934,plain,
~ spl20_24,
inference(rat,[],[s29,s813]) ).
cnf(s941,plain,
( spl20_26
| ~ spl20_28
| ~ spl20_30
| ~ spl20_31
| ~ spl20_32
| ~ spl20_34
| ~ spl20_35
| ~ spl20_36
| ~ spl20_37
| ~ spl20_38
| ~ spl20_39
| ~ spl20_40
| ~ spl20_41
| ~ spl20_42
| ~ spl20_43 ),
inference(rat,[],[s8,s823,s930,s931,s933,s934]) ).
cnf(s948,plain,
spl20_156,
inference(rat,[],[s920,s916]) ).
cnf(s951,plain,
~ spl20_227,
inference(rat,[],[s520,s948]) ).
cnf(s953,plain,
~ spl20_228,
inference(rat,[],[s476,s948]) ).
cnf(s954,plain,
~ spl20_152,
inference(rat,[],[s442,s948]) ).
cnf(s956,plain,
spl20_154,
inference(rat,[],[s927,s926,s948]) ).
cnf(s957,plain,
spl20_143,
inference(rat,[],[s106,s956]) ).
cnf(s958,plain,
~ spl20_146,
inference(rat,[],[s105,s956]) ).
cnf(s959,plain,
~ spl20_198,
inference(rat,[],[s624,s957]) ).
cnf(s962,plain,
~ spl20_193,
inference(rat,[],[s562,s957]) ).
cnf(s963,plain,
spl20_115,
inference(rat,[],[s497,s246,s957]) ).
cnf(s964,plain,
~ spl20_160,
inference(rat,[],[s485,s957]) ).
cnf(s967,plain,
spl20_28,
inference(rat,[],[s500,s830,s957,s813,s963]) ).
cnf(s968,plain,
~ spl20_26,
inference(rat,[],[s39,s963]) ).
cnf(s969,plain,
~ spl20_141,
inference(rat,[],[s102,s964]) ).
cnf(s971,plain,
spl20_176,
inference(rat,[],[s903,s899]) ).
cnf(s972,plain,
~ spl20_275,
inference(rat,[],[s780,s971]) ).
cnf(s973,plain,
~ spl20_276,
inference(rat,[],[s778,s971]) ).
cnf(s974,plain,
~ spl20_248,
inference(rat,[],[s719,s971]) ).
cnf(s975,plain,
~ spl20_166,
inference(rat,[],[s361,s971]) ).
cnf(s976,plain,
~ spl20_172,
inference(rat,[],[s264,s971]) ).
cnf(s977,plain,
~ spl20_175,
inference(rat,[],[s261,s971]) ).
cnf(s978,plain,
spl20_38,
inference(rat,[],[s508,s963,s948,s823,s971]) ).
cnf(s979,plain,
spl20_173,
inference(rat,[],[s911,s976]) ).
cnf(s981,plain,
~ spl20_258,
inference(rat,[],[s801,s979]) ).
cnf(s985,plain,
~ spl20_240,
inference(rat,[],[s760,s979]) ).
cnf(s986,plain,
~ spl20_167,
inference(rat,[],[s360,s979]) ).
cnf(s987,plain,
~ spl20_179,
inference(rat,[],[s262,s979]) ).
cnf(s988,plain,
spl20_257,
inference(rat,[],[s869,s981]) ).
cnf(s989,plain,
spl20_234,
inference(rat,[],[s853,s985]) ).
cnf(s990,plain,
~ spl20_162,
inference(rat,[],[s913,s986]) ).
cnf(s991,plain,
spl20_249,
inference(rat,[],[s855,s972,s987]) ).
cnf(s992,plain,
spl20_268,
inference(rat,[],[s856,s973,s987]) ).
cnf(s993,plain,
~ spl20_236,
inference(rat,[],[s718,s988]) ).
cnf(s994,plain,
~ spl20_261,
inference(rat,[],[s406,s988]) ).
cnf(s996,plain,
spl20_239,
inference(rat,[],[s871,s985,s990]) ).
cnf(s998,plain,
~ spl20_237,
inference(rat,[],[s381,s991]) ).
cnf(s1000,plain,
~ spl20_264,
inference(rat,[],[s389,s992]) ).
cnf(s1001,plain,
spl20_230,
inference(rat,[],[s849,s974,s993]) ).
cnf(s1002,plain,
spl20_274,
inference(rat,[],[s861,s977,s994]) ).
cnf(s1003,plain,
spl20_262,
inference(rat,[],[s867,s994]) ).
cnf(s1005,plain,
~ spl20_233,
inference(rat,[],[s347,s996]) ).
cnf(s1006,plain,
spl20_235,
inference(rat,[],[s199,s990,s993,s998]) ).
cnf(s1007,plain,
spl20_263,
inference(rat,[],[s866,s1000]) ).
cnf(s1010,plain,
spl20_269,
inference(rat,[],[s864,s975,s1005]) ).
cnf(s1015,plain,
spl20_153,
inference(rat,[],[s929,s928,s954]) ).
cnf(s1016,plain,
~ spl20_192,
inference(rat,[],[s634,s1015]) ).
cnf(s1017,plain,
~ spl20_159,
inference(rat,[],[s632,s1015]) ).
cnf(s1018,plain,
~ spl20_147,
inference(rat,[],[s588,s1015]) ).
cnf(s1023,plain,
~ spl20_224,
inference(rat,[],[s474,s1015]) ).
cnf(s1026,plain,
spl20_43,
inference(rat,[],[s514,s979,s66,s823,s1015]) ).
cnf(s1027,plain,
spl20_186,
inference(rat,[],[s878,s959,s1016]) ).
cnf(s1028,plain,
spl20_201,
inference(rat,[],[s881,s951,s1017]) ).
cnf(s1029,plain,
spl20_220,
inference(rat,[],[s882,s953,s1017]) ).
cnf(s1030,plain,
~ spl20_142,
inference(rat,[],[s75,s969,s958,s1018]) ).
cnf(s1037,plain,
~ spl20_222,
inference(rat,[],[s616,s1027]) ).
cnf(s1038,plain,
~ spl20_185,
inference(rat,[],[s612,s1027]) ).
cnf(s1039,plain,
spl20_31,
inference(rat,[],[s504,s989,s823,s813,s1027]) ).
cnf(s1040,plain,
~ spl20_199,
inference(rat,[],[s561,s1028]) ).
cnf(s1042,plain,
spl20_40,
inference(rat,[],[s585,s991,s823,s813,s1028]) ).
cnf(s1043,plain,
~ spl20_216,
inference(rat,[],[s444,s1029]) ).
cnf(s1046,plain,
spl20_35,
inference(rat,[],[s599,s992,s66,s823,s1029]) ).
cnf(s1048,plain,
spl20_191,
inference(rat,[],[s893,s1016,s1030]) ).
cnf(s1049,plain,
spl20_226,
inference(rat,[],[s192,s953,s1023,s1037]) ).
cnf(s1050,plain,
spl20_182,
inference(rat,[],[s885,s958,s1037]) ).
cnf(s1051,plain,
spl20_221,
inference(rat,[],[s886,s958,s1038]) ).
cnf(s1052,plain,
spl20_187,
inference(rat,[],[s877,s962,s1040]) ).
cnf(s1054,plain,
spl20_215,
inference(rat,[],[s888,s962,s1043]) ).
cnf(s1056,plain,
spl20_30,
inference(rat,[],[s501,s996,s963,s66,s813,s1048]) ).
cnf(s1057,plain,
~ spl20_213,
inference(rat,[],[s557,s1049]) ).
cnf(s1058,plain,
spl20_39,
inference(rat,[],[s511,s1002,s963,s823,s1049]) ).
cnf(s1060,plain,
spl20_36,
inference(rat,[],[s549,s1001,s963,s813,s1050]) ).
cnf(s1064,plain,
spl20_42,
inference(rat,[],[s515,s1010,s963,s823,s813,s1051]) ).
cnf(s1065,plain,
spl20_32,
inference(rat,[],[s572,s1006,s66,s813,s1052]) ).
cnf(s1067,plain,
spl20_34,
inference(rat,[],[s530,s1007,s963,s66,s1054]) ).
cnf(s1068,plain,
spl20_209,
inference(rat,[],[s875,s1057]) ).
cnf(s1069,plain,
spl20_214,
inference(rat,[],[s889,s1057]) ).
cnf(s1072,plain,
spl20_37,
inference(rat,[],[s604,s988,s963,s66,s1068]) ).
cnf(s1074,plain,
spl20_41,
inference(rat,[],[s513,s1003,s963,s66,s823,s1069]) ).
cnf(s1075,plain,
$false,
inference(rat,[],[s941,s1026,s1064,s1065,s1042,s1058,s978,s1056,s1060,s1046,s1067,s1039,s967,s968,s1074,s1072]) ).
fof(f3789,plain,
$false,
inference(avatar_sat_refutation,[],[s1075]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG114+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.16 % Computer : n004.cluster.edu
% 0.08/0.16 % Model : x86_64 x86_64
% 0.08/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.16 % Memory : 8046.5625MB
% 0.08/0.16 % OS : Linux 6.8.0-71-generic
% 0.08/0.16 % CPULimit : 300
% 0.08/0.16 % WCLimit : 300
% 0.08/0.16 % DateTime : Mon Sep 28 19:30:22 UTC 2026
% 0.08/0.16 % CPUTime :
% 0.08/0.16 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 Running first-order theorem proving
% 0.08/0.19 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.18/1.11 % (674092)Detected formulas, will run a generic FOF schedule.
% 3.18/1.11 % (674100)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4258185359:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.18/1.11 % (674102)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2505449025:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.18/1.11 % (674101)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=845176465:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.18/1.11 % (674098)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=135656742:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.18/1.11 % (674097)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=2328925214:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.18/1.11 % (674099)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=3037169182:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.18/1.11 % (674100)Instruction limit reached!
% 3.18/1.11 % (674100)------------------------------
% 3.18/1.11 % (674100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.18/1.11 % (674100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.18/1.11 % (674100)CaDiCaL version: 2.1.3
% 3.18/1.11 % (674100)Termination reason: Instruction limit
% 3.18/1.11 % (674100)Termination phase: Saturation
% 3.18/1.11 % (674100)Time elapsed: 0.028 s
% 3.18/1.11 % (674100)Peak memory usage: 90 MB
% 3.18/1.11 % (674100)Instructions burned: 112 (million)
% 3.18/1.11 % (674103)dis-21_1_sil=8000:lcm=predicate:random_seed=3969859733: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.18/1.11 % (674103)Refutation not found, incomplete strategy
% 3.18/1.11 % (674103)------------------------------
% 3.18/1.11 % (674103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.18/1.11 % (674103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.18/1.11 % (674103)CaDiCaL version: 2.1.3
% 3.18/1.11 % (674103)Termination reason: Refutation not found, incomplete strategy
% 3.18/1.11 % (674103)Time elapsed: 0.017 s
% 3.18/1.11 % (674103)Peak memory usage: 89 MB
% 3.18/1.11 % (674103)Instructions burned: 33 (million)
% 3.18/1.11 % (674101)Instruction limit reached!
% 3.18/1.11 % (674101)------------------------------
% 3.18/1.11 % (674101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.18/1.11 % (674101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.18/1.11 % (674101)CaDiCaL version: 2.1.3
% 3.18/1.11 % (674101)Termination reason: Instruction limit
% 3.18/1.11 % (674101)Termination phase: Saturation
% 3.18/1.11 % (674101)Time elapsed: 0.051 s
% 3.18/1.11 % (674101)Peak memory usage: 88 MB
% 3.18/1.11 % (674101)Instructions burned: 122 (million)
% 3.18/1.11 % (674102)First to succeed.
% 3.18/1.11 % (674102)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-674092"
% 3.18/1.11 % (674110)lrs+10_1_sil=8000:sp=occurrence:random_seed=3457737934:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.18/1.11 % (674110)Also succeeded, but the first one will report.
% 3.18/1.11 % (674112)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3349476140:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 3.18/1.11 % (674112)Also succeeded, but the first one will report.
% 3.18/1.11 % (674103)------------------------------
% 3.18/1.11 % (674103)------------------------------
% 3.18/1.11 % (674102)Refutation found. Thanks to Tanya!
% 3.18/1.11 % SZS status Theorem for theBenchmark
% 3.18/1.11 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/1.30 % (674102)------------------------------
% 0.16/1.30 % (674102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/1.30 % (674102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/1.30 % (674102)CaDiCaL version: 2.1.3
% 0.16/1.30 % (674102)Termination reason: Refutation
% 0.16/1.30 % (674102)Time elapsed: 0.075 s
% 0.16/1.30 % (674102)Peak memory usage: 91 MB
% 0.16/1.30 % (674102)Instructions burned: 145 (million)
% 0.16/1.30 % (674102)------------------------------
% 0.16/1.30 % (674102)------------------------------
% 0.16/1.30 % (674092)Success in time 0.481 s
% 0.16/1.30 % Vampire exiting
%------------------------------------------------------------------------------