%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG113+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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.74s 1.19s
% Output : Refutation 4.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 155
% Syntax : Number of formulae : 751 ( 182 unt; 141 def)
% Number of atoms : 3834 (2493 equ)
% Maximal formula atoms : 384 ( 5 avg)
% Number of connectives : 4963 (1880 ~;1996 |; 982 &)
% ( 105 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 143 ( 141 usr; 142 prp; 0-2 aty)
% Number of functors : 22 ( 22 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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
fof(f10,axiom,
( op1(e10,e10) = e10
& op1(e11,e11) = e11
& op1(e12,e12) = e12
& op1(e13,e13) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( op2(e20,e20) = e20
& op2(e21,e21) = e21
& op2(e22,e22) = e22
& op2(e23,e23) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e10 = op1(e12,e13)
& e11 = op1(op1(e12,e13),e13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e20 = op2(e22,e23)
& e21 = op2(op2(e22,e23),e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( h1(e12) = e20
& h1(e13) = e21
& h1(e10) = op2(e20,e21)
& h1(e11) = op2(op2(e20,e21),e21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
fof(f26,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 ) )
| ( h5(op1(e10,e10)) = op2(h5(e10),h5(e10))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& ( h5(e10) = e20
| h5(e11) = e20
| h5(e12) = e20
| h5(e13) = e20 )
& ( h5(e10) = e21
| h5(e11) = e21
| h5(e12) = e21
| h5(e13) = e21 )
& ( h5(e10) = e22
| h5(e11) = e22
| h5(e12) = e22
| h5(e13) = e22 )
& ( h5(e10) = e23
| h5(e11) = e23
| h5(e12) = e23
| h5(e13) = e23 ) )
| ( h6(op1(e10,e10)) = op2(h6(e10),h6(e10))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& ( h6(e10) = e20
| h6(e11) = e20
| h6(e12) = e20
| h6(e13) = e20 )
& ( h6(e10) = e21
| h6(e11) = e21
| h6(e12) = e21
| h6(e13) = e21 )
& ( h6(e10) = e22
| h6(e11) = e22
| h6(e12) = e22
| h6(e13) = e22 )
& ( h6(e10) = e23
| h6(e11) = e23
| h6(e12) = e23
| h6(e13) = e23 ) )
| ( h7(op1(e10,e10)) = op2(h7(e10),h7(e10))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& ( h7(e10) = e20
| h7(e11) = e20
| h7(e12) = e20
| h7(e13) = e20 )
& ( h7(e10) = e21
| h7(e11) = e21
| h7(e12) = e21
| h7(e13) = e21 )
& ( h7(e10) = e22
| h7(e11) = e22
| h7(e12) = e22
| h7(e13) = e22 )
& ( h7(e10) = e23
| h7(e11) = e23
| h7(e12) = e23
| h7(e13) = e23 ) )
| ( h8(op1(e10,e10)) = op2(h8(e10),h8(e10))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& ( h8(e10) = e20
| h8(e11) = e20
| h8(e12) = e20
| h8(e13) = e20 )
& ( h8(e10) = e21
| h8(e11) = e21
| h8(e12) = e21
| h8(e13) = e21 )
& ( h8(e10) = e22
| h8(e11) = e22
| h8(e12) = e22
| h8(e13) = e22 )
& ( h8(e10) = e23
| h8(e11) = e23
| h8(e12) = e23
| h8(e13) = e23 ) )
| ( h9(op1(e10,e10)) = op2(h9(e10),h9(e10))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& ( h9(e10) = e20
| h9(e11) = e20
| h9(e12) = e20
| h9(e13) = e20 )
& ( h9(e10) = e21
| h9(e11) = e21
| h9(e12) = e21
| h9(e13) = e21 )
& ( h9(e10) = e22
| h9(e11) = e22
| h9(e12) = e22
| h9(e13) = e22 )
& ( h9(e10) = e23
| h9(e11) = e23
| h9(e12) = e23
| h9(e13) = e23 ) )
| ( h10(op1(e10,e10)) = op2(h10(e10),h10(e10))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& ( h10(e10) = e20
| h10(e11) = e20
| h10(e12) = e20
| h10(e13) = e20 )
& ( h10(e10) = e21
| h10(e11) = e21
| h10(e12) = e21
| h10(e13) = e21 )
& ( h10(e10) = e22
| h10(e11) = e22
| h10(e12) = e22
| h10(e13) = e22 )
& ( h10(e10) = e23
| h10(e11) = e23
| h10(e12) = e23
| h10(e13) = e23 ) )
| ( h11(op1(e10,e10)) = op2(h11(e10),h11(e10))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& ( h11(e10) = e20
| h11(e11) = e20
| h11(e12) = e20
| h11(e13) = e20 )
& ( h11(e10) = e21
| h11(e11) = e21
| h11(e12) = e21
| h11(e13) = e21 )
& ( h11(e10) = e22
| h11(e11) = e22
| h11(e12) = e22
| h11(e13) = e22 )
& ( h11(e10) = e23
| h11(e11) = e23
| h11(e12) = e23
| h11(e13) = e23 ) )
| ( h12(op1(e10,e10)) = op2(h12(e10),h12(e10))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& ( h12(e10) = e20
| h12(e11) = e20
| h12(e12) = e20
| h12(e13) = e20 )
& ( h12(e10) = e21
| h12(e11) = e21
| h12(e12) = e21
| h12(e13) = e21 )
& ( h12(e10) = e22
| h12(e11) = e22
| h12(e12) = e22
| h12(e13) = e22 )
& ( h12(e10) = e23
| h12(e11) = e23
| h12(e12) = e23
| h12(e13) = e23 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f27,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 ) )
| ( h5(op1(e10,e10)) = op2(h5(e10),h5(e10))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& ( h5(e10) = e20
| h5(e11) = e20
| h5(e12) = e20
| h5(e13) = e20 )
& ( h5(e10) = e21
| h5(e11) = e21
| h5(e12) = e21
| h5(e13) = e21 )
& ( h5(e10) = e22
| h5(e11) = e22
| h5(e12) = e22
| h5(e13) = e22 )
& ( h5(e10) = e23
| h5(e11) = e23
| h5(e12) = e23
| h5(e13) = e23 ) )
| ( h6(op1(e10,e10)) = op2(h6(e10),h6(e10))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& ( h6(e10) = e20
| h6(e11) = e20
| h6(e12) = e20
| h6(e13) = e20 )
& ( h6(e10) = e21
| h6(e11) = e21
| h6(e12) = e21
| h6(e13) = e21 )
& ( h6(e10) = e22
| h6(e11) = e22
| h6(e12) = e22
| h6(e13) = e22 )
& ( h6(e10) = e23
| h6(e11) = e23
| h6(e12) = e23
| h6(e13) = e23 ) )
| ( h7(op1(e10,e10)) = op2(h7(e10),h7(e10))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& ( h7(e10) = e20
| h7(e11) = e20
| h7(e12) = e20
| h7(e13) = e20 )
& ( h7(e10) = e21
| h7(e11) = e21
| h7(e12) = e21
| h7(e13) = e21 )
& ( h7(e10) = e22
| h7(e11) = e22
| h7(e12) = e22
| h7(e13) = e22 )
& ( h7(e10) = e23
| h7(e11) = e23
| h7(e12) = e23
| h7(e13) = e23 ) )
| ( h8(op1(e10,e10)) = op2(h8(e10),h8(e10))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& ( h8(e10) = e20
| h8(e11) = e20
| h8(e12) = e20
| h8(e13) = e20 )
& ( h8(e10) = e21
| h8(e11) = e21
| h8(e12) = e21
| h8(e13) = e21 )
& ( h8(e10) = e22
| h8(e11) = e22
| h8(e12) = e22
| h8(e13) = e22 )
& ( h8(e10) = e23
| h8(e11) = e23
| h8(e12) = e23
| h8(e13) = e23 ) )
| ( h9(op1(e10,e10)) = op2(h9(e10),h9(e10))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& ( h9(e10) = e20
| h9(e11) = e20
| h9(e12) = e20
| h9(e13) = e20 )
& ( h9(e10) = e21
| h9(e11) = e21
| h9(e12) = e21
| h9(e13) = e21 )
& ( h9(e10) = e22
| h9(e11) = e22
| h9(e12) = e22
| h9(e13) = e22 )
& ( h9(e10) = e23
| h9(e11) = e23
| h9(e12) = e23
| h9(e13) = e23 ) )
| ( h10(op1(e10,e10)) = op2(h10(e10),h10(e10))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& ( h10(e10) = e20
| h10(e11) = e20
| h10(e12) = e20
| h10(e13) = e20 )
& ( h10(e10) = e21
| h10(e11) = e21
| h10(e12) = e21
| h10(e13) = e21 )
& ( h10(e10) = e22
| h10(e11) = e22
| h10(e12) = e22
| h10(e13) = e22 )
& ( h10(e10) = e23
| h10(e11) = e23
| h10(e12) = e23
| h10(e13) = e23 ) )
| ( h11(op1(e10,e10)) = op2(h11(e10),h11(e10))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& ( h11(e10) = e20
| h11(e11) = e20
| h11(e12) = e20
| h11(e13) = e20 )
& ( h11(e10) = e21
| h11(e11) = e21
| h11(e12) = e21
| h11(e13) = e21 )
& ( h11(e10) = e22
| h11(e11) = e22
| h11(e12) = e22
| h11(e13) = e22 )
& ( h11(e10) = e23
| h11(e11) = e23
| h11(e12) = e23
| h11(e13) = e23 ) )
| ( h12(op1(e10,e10)) = op2(h12(e10),h12(e10))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& ( h12(e10) = e20
| h12(e11) = e20
| h12(e12) = e20
| h12(e13) = e20 )
& ( h12(e10) = e21
| h12(e11) = e21
| h12(e12) = e21
| h12(e13) = e21 )
& ( h12(e10) = e22
| h12(e11) = e22
| h12(e12) = e22
| h12(e13) = e22 )
& ( h12(e10) = e23
| h12(e11) = e23
| h12(e12) = e23
| h12(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f28,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) ) )
& ( h5(op1(e10,e10)) != op2(h5(e10),h5(e10))
| h5(op1(e10,e11)) != op2(h5(e10),h5(e11))
| h5(op1(e10,e12)) != op2(h5(e10),h5(e12))
| h5(op1(e10,e13)) != op2(h5(e10),h5(e13))
| h5(op1(e11,e10)) != op2(h5(e11),h5(e10))
| h5(op1(e11,e11)) != op2(h5(e11),h5(e11))
| h5(op1(e11,e12)) != op2(h5(e11),h5(e12))
| h5(op1(e11,e13)) != op2(h5(e11),h5(e13))
| h5(op1(e12,e10)) != op2(h5(e12),h5(e10))
| h5(op1(e12,e11)) != op2(h5(e12),h5(e11))
| h5(op1(e12,e12)) != op2(h5(e12),h5(e12))
| h5(op1(e12,e13)) != op2(h5(e12),h5(e13))
| h5(op1(e13,e10)) != op2(h5(e13),h5(e10))
| h5(op1(e13,e11)) != op2(h5(e13),h5(e11))
| h5(op1(e13,e12)) != op2(h5(e13),h5(e12))
| h5(op1(e13,e13)) != op2(h5(e13),h5(e13))
| ( e20 != h5(e10)
& e20 != h5(e11)
& e20 != h5(e12)
& e20 != h5(e13) )
| ( e21 != h5(e10)
& e21 != h5(e11)
& e21 != h5(e12)
& e21 != h5(e13) )
| ( e22 != h5(e10)
& e22 != h5(e11)
& e22 != h5(e12)
& e22 != h5(e13) )
| ( e23 != h5(e10)
& e23 != h5(e11)
& e23 != h5(e12)
& e23 != h5(e13) ) )
& ( h6(op1(e10,e10)) != op2(h6(e10),h6(e10))
| h6(op1(e10,e11)) != op2(h6(e10),h6(e11))
| h6(op1(e10,e12)) != op2(h6(e10),h6(e12))
| h6(op1(e10,e13)) != op2(h6(e10),h6(e13))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| ( e20 != h6(e10)
& e20 != h6(e11)
& e20 != h6(e12)
& e20 != h6(e13) )
| ( e21 != h6(e10)
& e21 != h6(e11)
& e21 != h6(e12)
& e21 != h6(e13) )
| ( e22 != h6(e10)
& e22 != h6(e11)
& e22 != h6(e12)
& e22 != h6(e13) )
| ( e23 != h6(e10)
& e23 != h6(e11)
& e23 != h6(e12)
& e23 != h6(e13) ) )
& ( h7(op1(e10,e10)) != op2(h7(e10),h7(e10))
| h7(op1(e10,e11)) != op2(h7(e10),h7(e11))
| h7(op1(e10,e12)) != op2(h7(e10),h7(e12))
| h7(op1(e10,e13)) != op2(h7(e10),h7(e13))
| h7(op1(e11,e10)) != op2(h7(e11),h7(e10))
| h7(op1(e11,e11)) != op2(h7(e11),h7(e11))
| h7(op1(e11,e12)) != op2(h7(e11),h7(e12))
| h7(op1(e11,e13)) != op2(h7(e11),h7(e13))
| h7(op1(e12,e10)) != op2(h7(e12),h7(e10))
| h7(op1(e12,e11)) != op2(h7(e12),h7(e11))
| h7(op1(e12,e12)) != op2(h7(e12),h7(e12))
| h7(op1(e12,e13)) != op2(h7(e12),h7(e13))
| h7(op1(e13,e10)) != op2(h7(e13),h7(e10))
| h7(op1(e13,e11)) != op2(h7(e13),h7(e11))
| h7(op1(e13,e12)) != op2(h7(e13),h7(e12))
| h7(op1(e13,e13)) != op2(h7(e13),h7(e13))
| ( e20 != h7(e10)
& e20 != h7(e11)
& e20 != h7(e12)
& e20 != h7(e13) )
| ( e21 != h7(e10)
& e21 != h7(e11)
& e21 != h7(e12)
& e21 != h7(e13) )
| ( e22 != h7(e10)
& e22 != h7(e11)
& e22 != h7(e12)
& e22 != h7(e13) )
| ( e23 != h7(e10)
& e23 != h7(e11)
& e23 != h7(e12)
& e23 != h7(e13) ) )
& ( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h8(e11))
| h8(op1(e10,e12)) != op2(h8(e10),h8(e12))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e11,e10)) != op2(h8(e11),h8(e10))
| h8(op1(e11,e11)) != op2(h8(e11),h8(e11))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| ( e20 != h8(e10)
& e20 != h8(e11)
& e20 != h8(e12)
& e20 != h8(e13) )
| ( e21 != h8(e10)
& e21 != h8(e11)
& e21 != h8(e12)
& e21 != h8(e13) )
| ( e22 != h8(e10)
& e22 != h8(e11)
& e22 != h8(e12)
& e22 != h8(e13) )
| ( e23 != h8(e10)
& e23 != h8(e11)
& e23 != h8(e12)
& e23 != h8(e13) ) )
& ( h9(op1(e10,e10)) != op2(h9(e10),h9(e10))
| h9(op1(e10,e11)) != op2(h9(e10),h9(e11))
| h9(op1(e10,e12)) != op2(h9(e10),h9(e12))
| h9(op1(e10,e13)) != op2(h9(e10),h9(e13))
| h9(op1(e11,e10)) != op2(h9(e11),h9(e10))
| h9(op1(e11,e11)) != op2(h9(e11),h9(e11))
| h9(op1(e11,e12)) != op2(h9(e11),h9(e12))
| h9(op1(e11,e13)) != op2(h9(e11),h9(e13))
| h9(op1(e12,e10)) != op2(h9(e12),h9(e10))
| h9(op1(e12,e11)) != op2(h9(e12),h9(e11))
| h9(op1(e12,e12)) != op2(h9(e12),h9(e12))
| h9(op1(e12,e13)) != op2(h9(e12),h9(e13))
| h9(op1(e13,e10)) != op2(h9(e13),h9(e10))
| h9(op1(e13,e11)) != op2(h9(e13),h9(e11))
| h9(op1(e13,e12)) != op2(h9(e13),h9(e12))
| h9(op1(e13,e13)) != op2(h9(e13),h9(e13))
| ( e20 != h9(e10)
& e20 != h9(e11)
& e20 != h9(e12)
& e20 != h9(e13) )
| ( e21 != h9(e10)
& e21 != h9(e11)
& e21 != h9(e12)
& e21 != h9(e13) )
| ( e22 != h9(e10)
& e22 != h9(e11)
& e22 != h9(e12)
& e22 != h9(e13) )
| ( e23 != h9(e10)
& e23 != h9(e11)
& e23 != h9(e12)
& e23 != h9(e13) ) )
& ( h10(op1(e10,e10)) != op2(h10(e10),h10(e10))
| h10(op1(e10,e11)) != op2(h10(e10),h10(e11))
| h10(op1(e10,e12)) != op2(h10(e10),h10(e12))
| h10(op1(e10,e13)) != op2(h10(e10),h10(e13))
| h10(op1(e11,e10)) != op2(h10(e11),h10(e10))
| h10(op1(e11,e11)) != op2(h10(e11),h10(e11))
| h10(op1(e11,e12)) != op2(h10(e11),h10(e12))
| h10(op1(e11,e13)) != op2(h10(e11),h10(e13))
| h10(op1(e12,e10)) != op2(h10(e12),h10(e10))
| h10(op1(e12,e11)) != op2(h10(e12),h10(e11))
| h10(op1(e12,e12)) != op2(h10(e12),h10(e12))
| h10(op1(e12,e13)) != op2(h10(e12),h10(e13))
| h10(op1(e13,e10)) != op2(h10(e13),h10(e10))
| h10(op1(e13,e11)) != op2(h10(e13),h10(e11))
| h10(op1(e13,e12)) != op2(h10(e13),h10(e12))
| h10(op1(e13,e13)) != op2(h10(e13),h10(e13))
| ( e20 != h10(e10)
& e20 != h10(e11)
& e20 != h10(e12)
& e20 != h10(e13) )
| ( e21 != h10(e10)
& e21 != h10(e11)
& e21 != h10(e12)
& e21 != h10(e13) )
| ( e22 != h10(e10)
& e22 != h10(e11)
& e22 != h10(e12)
& e22 != h10(e13) )
| ( e23 != h10(e10)
& e23 != h10(e11)
& e23 != h10(e12)
& e23 != h10(e13) ) )
& ( h11(op1(e10,e10)) != op2(h11(e10),h11(e10))
| h11(op1(e10,e11)) != op2(h11(e10),h11(e11))
| h11(op1(e10,e12)) != op2(h11(e10),h11(e12))
| h11(op1(e10,e13)) != op2(h11(e10),h11(e13))
| h11(op1(e11,e10)) != op2(h11(e11),h11(e10))
| h11(op1(e11,e11)) != op2(h11(e11),h11(e11))
| h11(op1(e11,e12)) != op2(h11(e11),h11(e12))
| h11(op1(e11,e13)) != op2(h11(e11),h11(e13))
| h11(op1(e12,e10)) != op2(h11(e12),h11(e10))
| h11(op1(e12,e11)) != op2(h11(e12),h11(e11))
| h11(op1(e12,e12)) != op2(h11(e12),h11(e12))
| h11(op1(e12,e13)) != op2(h11(e12),h11(e13))
| h11(op1(e13,e10)) != op2(h11(e13),h11(e10))
| h11(op1(e13,e11)) != op2(h11(e13),h11(e11))
| h11(op1(e13,e12)) != op2(h11(e13),h11(e12))
| h11(op1(e13,e13)) != op2(h11(e13),h11(e13))
| ( e20 != h11(e10)
& e20 != h11(e11)
& e20 != h11(e12)
& e20 != h11(e13) )
| ( e21 != h11(e10)
& e21 != h11(e11)
& e21 != h11(e12)
& e21 != h11(e13) )
| ( e22 != h11(e10)
& e22 != h11(e11)
& e22 != h11(e12)
& e22 != h11(e13) )
| ( e23 != h11(e10)
& e23 != h11(e11)
& e23 != h11(e12)
& e23 != h11(e13) ) )
& ( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),h12(e11))
| h12(op1(e10,e12)) != op2(h12(e10),h12(e12))
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e11,e10)) != op2(h12(e11),h12(e10))
| h12(op1(e11,e11)) != op2(h12(e11),h12(e11))
| h12(op1(e11,e12)) != op2(h12(e11),h12(e12))
| h12(op1(e11,e13)) != op2(h12(e11),h12(e13))
| h12(op1(e12,e10)) != op2(h12(e12),h12(e10))
| h12(op1(e12,e11)) != op2(h12(e12),h12(e11))
| h12(op1(e12,e12)) != op2(h12(e12),h12(e12))
| h12(op1(e12,e13)) != op2(h12(e12),h12(e13))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e13,e11)) != op2(h12(e13),h12(e11))
| h12(op1(e13,e12)) != op2(h12(e13),h12(e12))
| h12(op1(e13,e13)) != op2(h12(e13),h12(e13))
| ( e20 != h12(e10)
& e20 != h12(e11)
& e20 != h12(e12)
& e20 != h12(e13) )
| ( e21 != h12(e10)
& e21 != h12(e11)
& e21 != h12(e12)
& e21 != h12(e13) )
| ( e22 != h12(e10)
& e22 != h12(e11)
& e22 != h12(e12)
& e22 != h12(e13) )
| ( e23 != h12(e10)
& e23 != h12(e11)
& e23 != h12(e12)
& e23 != h12(e13) ) ) ),
inference(ennf_transformation,[],[f27]) ).
fof(f29,definition,
( ( e23 != h12(e10)
& e23 != h12(e11)
& e23 != h12(e12)
& e23 != h12(e13) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f30,definition,
( ( e22 != h12(e10)
& e22 != h12(e11)
& e22 != h12(e12)
& e22 != h12(e13) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f31,definition,
( ( e21 != h12(e10)
& e21 != h12(e11)
& e21 != h12(e12)
& e21 != h12(e13) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f32,definition,
( ( e23 != h11(e10)
& e23 != h11(e11)
& e23 != h11(e12)
& e23 != h11(e13) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f33,definition,
( ( e22 != h11(e10)
& e22 != h11(e11)
& e22 != h11(e12)
& e22 != h11(e13) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f34,definition,
( ( e21 != h11(e10)
& e21 != h11(e11)
& e21 != h11(e12)
& e21 != h11(e13) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f35,definition,
( ( e23 != h10(e10)
& e23 != h10(e11)
& e23 != h10(e12)
& e23 != h10(e13) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f36,definition,
( ( e22 != h10(e10)
& e22 != h10(e11)
& e22 != h10(e12)
& e22 != h10(e13) )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f37,definition,
( ( e21 != h10(e10)
& e21 != h10(e11)
& e21 != h10(e12)
& e21 != h10(e13) )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f38,definition,
( ( e23 != h9(e10)
& e23 != h9(e11)
& e23 != h9(e12)
& e23 != h9(e13) )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f39,definition,
( ( e22 != h9(e10)
& e22 != h9(e11)
& e22 != h9(e12)
& e22 != h9(e13) )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f40,definition,
( ( e21 != h9(e10)
& e21 != h9(e11)
& e21 != h9(e12)
& e21 != h9(e13) )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f41,definition,
( ( e23 != h8(e10)
& e23 != h8(e11)
& e23 != h8(e12)
& e23 != h8(e13) )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f42,definition,
( ( e22 != h8(e10)
& e22 != h8(e11)
& e22 != h8(e12)
& e22 != h8(e13) )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f43,definition,
( ( e21 != h8(e10)
& e21 != h8(e11)
& e21 != h8(e12)
& e21 != h8(e13) )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f44,definition,
( ( e23 != h7(e10)
& e23 != h7(e11)
& e23 != h7(e12)
& e23 != h7(e13) )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f45,definition,
( ( e22 != h7(e10)
& e22 != h7(e11)
& e22 != h7(e12)
& e22 != h7(e13) )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f46,definition,
( ( e21 != h7(e10)
& e21 != h7(e11)
& e21 != h7(e12)
& e21 != h7(e13) )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f47,definition,
( ( e23 != h6(e10)
& e23 != h6(e11)
& e23 != h6(e12)
& e23 != h6(e13) )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f48,definition,
( ( e22 != h6(e10)
& e22 != h6(e11)
& e22 != h6(e12)
& e22 != h6(e13) )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f49,definition,
( ( e21 != h6(e10)
& e21 != h6(e11)
& e21 != h6(e12)
& e21 != h6(e13) )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f50,definition,
( ( e23 != h5(e10)
& e23 != h5(e11)
& e23 != h5(e12)
& e23 != h5(e13) )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f51,definition,
( ( e22 != h5(e10)
& e22 != h5(e11)
& e22 != h5(e12)
& e22 != h5(e13) )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f52,definition,
( ( e21 != h5(e10)
& e21 != h5(e11)
& e21 != h5(e12)
& e21 != h5(e13) )
| ~ sP23 ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f53,definition,
( ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) )
| ~ sP24 ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f54,definition,
( ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ~ sP25 ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f55,definition,
( ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ~ sP26 ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f56,definition,
( ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) )
| ~ sP27 ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f57,definition,
( ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ~ sP28 ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f58,definition,
( ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ~ sP29 ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f59,definition,
( ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) )
| ~ sP30 ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f60,definition,
( ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ~ sP31 ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f61,definition,
( ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ~ sP32 ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f62,definition,
( ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) )
| ~ sP33 ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f63,definition,
( ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ~ sP34 ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f64,definition,
( ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ~ sP35 ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f65,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) )
| sP35
| sP34
| sP33 )
& ( 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) )
| sP32
| sP31
| sP30 )
& ( 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) )
| sP29
| sP28
| sP27 )
& ( 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) )
| sP26
| sP25
| sP24 )
& ( h5(op1(e10,e10)) != op2(h5(e10),h5(e10))
| h5(op1(e10,e11)) != op2(h5(e10),h5(e11))
| h5(op1(e10,e12)) != op2(h5(e10),h5(e12))
| h5(op1(e10,e13)) != op2(h5(e10),h5(e13))
| h5(op1(e11,e10)) != op2(h5(e11),h5(e10))
| h5(op1(e11,e11)) != op2(h5(e11),h5(e11))
| h5(op1(e11,e12)) != op2(h5(e11),h5(e12))
| h5(op1(e11,e13)) != op2(h5(e11),h5(e13))
| h5(op1(e12,e10)) != op2(h5(e12),h5(e10))
| h5(op1(e12,e11)) != op2(h5(e12),h5(e11))
| h5(op1(e12,e12)) != op2(h5(e12),h5(e12))
| h5(op1(e12,e13)) != op2(h5(e12),h5(e13))
| h5(op1(e13,e10)) != op2(h5(e13),h5(e10))
| h5(op1(e13,e11)) != op2(h5(e13),h5(e11))
| h5(op1(e13,e12)) != op2(h5(e13),h5(e12))
| h5(op1(e13,e13)) != op2(h5(e13),h5(e13))
| ( e20 != h5(e10)
& e20 != h5(e11)
& e20 != h5(e12)
& e20 != h5(e13) )
| sP23
| sP22
| sP21 )
& ( h6(op1(e10,e10)) != op2(h6(e10),h6(e10))
| h6(op1(e10,e11)) != op2(h6(e10),h6(e11))
| h6(op1(e10,e12)) != op2(h6(e10),h6(e12))
| h6(op1(e10,e13)) != op2(h6(e10),h6(e13))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| ( e20 != h6(e10)
& e20 != h6(e11)
& e20 != h6(e12)
& e20 != h6(e13) )
| sP20
| sP19
| sP18 )
& ( h7(op1(e10,e10)) != op2(h7(e10),h7(e10))
| h7(op1(e10,e11)) != op2(h7(e10),h7(e11))
| h7(op1(e10,e12)) != op2(h7(e10),h7(e12))
| h7(op1(e10,e13)) != op2(h7(e10),h7(e13))
| h7(op1(e11,e10)) != op2(h7(e11),h7(e10))
| h7(op1(e11,e11)) != op2(h7(e11),h7(e11))
| h7(op1(e11,e12)) != op2(h7(e11),h7(e12))
| h7(op1(e11,e13)) != op2(h7(e11),h7(e13))
| h7(op1(e12,e10)) != op2(h7(e12),h7(e10))
| h7(op1(e12,e11)) != op2(h7(e12),h7(e11))
| h7(op1(e12,e12)) != op2(h7(e12),h7(e12))
| h7(op1(e12,e13)) != op2(h7(e12),h7(e13))
| h7(op1(e13,e10)) != op2(h7(e13),h7(e10))
| h7(op1(e13,e11)) != op2(h7(e13),h7(e11))
| h7(op1(e13,e12)) != op2(h7(e13),h7(e12))
| h7(op1(e13,e13)) != op2(h7(e13),h7(e13))
| ( e20 != h7(e10)
& e20 != h7(e11)
& e20 != h7(e12)
& e20 != h7(e13) )
| sP17
| sP16
| sP15 )
& ( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h8(e11))
| h8(op1(e10,e12)) != op2(h8(e10),h8(e12))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e11,e10)) != op2(h8(e11),h8(e10))
| h8(op1(e11,e11)) != op2(h8(e11),h8(e11))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| ( e20 != h8(e10)
& e20 != h8(e11)
& e20 != h8(e12)
& e20 != h8(e13) )
| sP14
| sP13
| sP12 )
& ( h9(op1(e10,e10)) != op2(h9(e10),h9(e10))
| h9(op1(e10,e11)) != op2(h9(e10),h9(e11))
| h9(op1(e10,e12)) != op2(h9(e10),h9(e12))
| h9(op1(e10,e13)) != op2(h9(e10),h9(e13))
| h9(op1(e11,e10)) != op2(h9(e11),h9(e10))
| h9(op1(e11,e11)) != op2(h9(e11),h9(e11))
| h9(op1(e11,e12)) != op2(h9(e11),h9(e12))
| h9(op1(e11,e13)) != op2(h9(e11),h9(e13))
| h9(op1(e12,e10)) != op2(h9(e12),h9(e10))
| h9(op1(e12,e11)) != op2(h9(e12),h9(e11))
| h9(op1(e12,e12)) != op2(h9(e12),h9(e12))
| h9(op1(e12,e13)) != op2(h9(e12),h9(e13))
| h9(op1(e13,e10)) != op2(h9(e13),h9(e10))
| h9(op1(e13,e11)) != op2(h9(e13),h9(e11))
| h9(op1(e13,e12)) != op2(h9(e13),h9(e12))
| h9(op1(e13,e13)) != op2(h9(e13),h9(e13))
| ( e20 != h9(e10)
& e20 != h9(e11)
& e20 != h9(e12)
& e20 != h9(e13) )
| sP11
| sP10
| sP9 )
& ( h10(op1(e10,e10)) != op2(h10(e10),h10(e10))
| h10(op1(e10,e11)) != op2(h10(e10),h10(e11))
| h10(op1(e10,e12)) != op2(h10(e10),h10(e12))
| h10(op1(e10,e13)) != op2(h10(e10),h10(e13))
| h10(op1(e11,e10)) != op2(h10(e11),h10(e10))
| h10(op1(e11,e11)) != op2(h10(e11),h10(e11))
| h10(op1(e11,e12)) != op2(h10(e11),h10(e12))
| h10(op1(e11,e13)) != op2(h10(e11),h10(e13))
| h10(op1(e12,e10)) != op2(h10(e12),h10(e10))
| h10(op1(e12,e11)) != op2(h10(e12),h10(e11))
| h10(op1(e12,e12)) != op2(h10(e12),h10(e12))
| h10(op1(e12,e13)) != op2(h10(e12),h10(e13))
| h10(op1(e13,e10)) != op2(h10(e13),h10(e10))
| h10(op1(e13,e11)) != op2(h10(e13),h10(e11))
| h10(op1(e13,e12)) != op2(h10(e13),h10(e12))
| h10(op1(e13,e13)) != op2(h10(e13),h10(e13))
| ( e20 != h10(e10)
& e20 != h10(e11)
& e20 != h10(e12)
& e20 != h10(e13) )
| sP8
| sP7
| sP6 )
& ( h11(op1(e10,e10)) != op2(h11(e10),h11(e10))
| h11(op1(e10,e11)) != op2(h11(e10),h11(e11))
| h11(op1(e10,e12)) != op2(h11(e10),h11(e12))
| h11(op1(e10,e13)) != op2(h11(e10),h11(e13))
| h11(op1(e11,e10)) != op2(h11(e11),h11(e10))
| h11(op1(e11,e11)) != op2(h11(e11),h11(e11))
| h11(op1(e11,e12)) != op2(h11(e11),h11(e12))
| h11(op1(e11,e13)) != op2(h11(e11),h11(e13))
| h11(op1(e12,e10)) != op2(h11(e12),h11(e10))
| h11(op1(e12,e11)) != op2(h11(e12),h11(e11))
| h11(op1(e12,e12)) != op2(h11(e12),h11(e12))
| h11(op1(e12,e13)) != op2(h11(e12),h11(e13))
| h11(op1(e13,e10)) != op2(h11(e13),h11(e10))
| h11(op1(e13,e11)) != op2(h11(e13),h11(e11))
| h11(op1(e13,e12)) != op2(h11(e13),h11(e12))
| h11(op1(e13,e13)) != op2(h11(e13),h11(e13))
| ( e20 != h11(e10)
& e20 != h11(e11)
& e20 != h11(e12)
& e20 != h11(e13) )
| sP5
| sP4
| sP3 )
& ( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),h12(e11))
| h12(op1(e10,e12)) != op2(h12(e10),h12(e12))
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e11,e10)) != op2(h12(e11),h12(e10))
| h12(op1(e11,e11)) != op2(h12(e11),h12(e11))
| h12(op1(e11,e12)) != op2(h12(e11),h12(e12))
| h12(op1(e11,e13)) != op2(h12(e11),h12(e13))
| h12(op1(e12,e10)) != op2(h12(e12),h12(e10))
| h12(op1(e12,e11)) != op2(h12(e12),h12(e11))
| h12(op1(e12,e12)) != op2(h12(e12),h12(e12))
| h12(op1(e12,e13)) != op2(h12(e12),h12(e13))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e13,e11)) != op2(h12(e13),h12(e11))
| h12(op1(e13,e12)) != op2(h12(e13),h12(e12))
| h12(op1(e13,e13)) != op2(h12(e13),h12(e13))
| ( e20 != h12(e10)
& e20 != h12(e11)
& e20 != h12(e12)
& e20 != h12(e13) )
| sP2
| sP1
| sP0 ) ),
inference(definition_folding,[],[f28,f64,f63,f62,f61,f60,f59,f58,f57,f56,f55,f54,f53,f52,f51,f50,f49,f48,f47,f46,f45,f44,f43,f42,f41,f40,f39,f38,f37,f36,f35,f34,f33,f32,f31,f30,f29]) ).
fof(f66,plain,
( ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ~ sP35 ),
inference(nnf_transformation,[],[f64]) ).
fof(f67,plain,
( ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ~ sP34 ),
inference(nnf_transformation,[],[f63]) ).
fof(f68,plain,
( ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) )
| ~ sP33 ),
inference(nnf_transformation,[],[f62]) ).
fof(f103,plain,
( e10 = op1(e13,e12)
| e11 = op1(e13,e12)
| e12 = op1(e13,e12)
| e13 = op1(e13,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f105,plain,
( e10 = op1(e13,e10)
| e11 = op1(e13,e10)
| e12 = op1(e13,e10)
| e13 = op1(e13,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f108,plain,
( e10 = op1(e12,e11)
| e11 = op1(e12,e11)
| e12 = op1(e12,e11)
| e13 = op1(e12,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f109,plain,
( e10 = op1(e12,e10)
| e11 = op1(e12,e10)
| e12 = op1(e12,e10)
| e13 = op1(e12,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f110,plain,
( e10 = op1(e11,e13)
| e11 = op1(e11,e13)
| e12 = op1(e11,e13)
| e13 = op1(e11,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f111,plain,
( e10 = op1(e11,e12)
| e11 = op1(e11,e12)
| e12 = op1(e11,e12)
| e13 = op1(e11,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f113,plain,
( e10 = op1(e11,e10)
| e11 = op1(e11,e10)
| e12 = op1(e11,e10)
| e13 = op1(e11,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f115,plain,
( e10 = op1(e10,e12)
| e11 = op1(e10,e12)
| e12 = op1(e10,e12)
| e13 = op1(e10,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f116,plain,
( e10 = op1(e10,e11)
| e11 = op1(e10,e11)
| e12 = op1(e10,e11)
| e13 = op1(e10,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f140,plain,
( e10 = op1(e10,e11)
| e10 = op1(e11,e11)
| e10 = op1(e12,e11)
| e10 = op1(e13,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f156,plain,
( e20 = op2(e22,e21)
| e21 = op2(e22,e21)
| e22 = op2(e22,e21)
| e23 = op2(e22,e21) ),
inference(cnf_transformation,[],[f3]) ).
fof(f158,plain,
( e20 = op2(e21,e23)
| e21 = op2(e21,e23)
| e22 = op2(e21,e23)
| e23 = op2(e21,e23) ),
inference(cnf_transformation,[],[f3]) ).
fof(f159,plain,
( e20 = op2(e21,e22)
| e21 = op2(e21,e22)
| e22 = op2(e21,e22)
| e23 = op2(e21,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f161,plain,
( e20 = op2(e21,e20)
| e21 = op2(e21,e20)
| e22 = op2(e21,e20)
| e23 = op2(e21,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f163,plain,
( e20 = op2(e20,e22)
| e21 = op2(e20,e22)
| e22 = op2(e20,e22)
| e23 = op2(e20,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f178,plain,
( e21 = op2(e20,e22)
| e21 = op2(e21,e22)
| e21 = op2(e22,e22)
| e21 = op2(e23,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f179,plain,
( e21 = op2(e22,e20)
| e21 = op2(e22,e21)
| e21 = op2(e22,e22)
| e21 = op2(e22,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f188,plain,
( e20 = op2(e20,e21)
| e20 = op2(e21,e21)
| e20 = op2(e22,e21)
| e20 = op2(e23,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f192,plain,
( op2(e20,e20) = e22
| e22 = op2(e21,e20)
| e22 = op2(e22,e20)
| e22 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f193,plain,
( op2(e20,e20) = e22
| e22 = op2(e20,e21)
| e22 = op2(e20,e22)
| e22 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f198,plain,
op1(e13,e12) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f201,plain,
op1(e13,e10) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f205,plain,
op1(e12,e11) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f206,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f207,plain,
op1(e12,e10) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f208,plain,
op1(e12,e10) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f211,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f212,plain,
op1(e11,e11) != op1(e11,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f213,plain,
op1(e11,e10) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f214,plain,
op1(e11,e10) != op1(e11,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f215,plain,
op1(e11,e10) != op1(e11,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f216,plain,
op1(e10,e12) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f217,plain,
op1(e10,e11) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f218,plain,
op1(e10,e11) != op1(e10,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f220,plain,
op1(e10,e10) != op1(e10,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f221,plain,
op1(e10,e10) != op1(e10,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f223,plain,
op1(e11,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f224,plain,
op1(e11,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f228,plain,
op1(e12,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f229,plain,
op1(e11,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f230,plain,
op1(e11,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f232,plain,
op1(e10,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f236,plain,
op1(e11,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f240,plain,
op1(e12,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f242,plain,
op1(e11,e10) != op1(e12,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f243,plain,
op1(e10,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f245,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f253,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f254,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f259,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f260,plain,
op2(e21,e21) != op2(e21,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f261,plain,
op2(e21,e20) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f263,plain,
op2(e21,e20) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f264,plain,
op2(e20,e22) != op2(e20,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f268,plain,
op2(e20,e20) != op2(e20,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f269,plain,
op2(e20,e20) != op2(e20,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f271,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f272,plain,
op2(e21,e23) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f278,plain,
op2(e21,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f280,plain,
op2(e20,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f281,plain,
op2(e20,e22) != op2(e21,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f284,plain,
op2(e21,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f293,plain,
op2(e20,e20) != op2(e21,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f299,plain,
e10 != e11,
inference(cnf_transformation,[],[f7]) ).
fof(f302,plain,
e21 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f304,plain,
e20 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f305,plain,
e20 != e21,
inference(cnf_transformation,[],[f8]) ).
fof(f322,plain,
e13 = op1(e13,e13),
inference(cnf_transformation,[],[f10]) ).
fof(f323,plain,
e12 = op1(e12,e12),
inference(cnf_transformation,[],[f10]) ).
fof(f324,plain,
e11 = op1(e11,e11),
inference(cnf_transformation,[],[f10]) ).
fof(f325,plain,
e10 = op1(e10,e10),
inference(cnf_transformation,[],[f10]) ).
fof(f326,plain,
e23 = op2(e23,e23),
inference(cnf_transformation,[],[f11]) ).
fof(f327,plain,
e22 = op2(e22,e22),
inference(cnf_transformation,[],[f11]) ).
fof(f328,plain,
e21 = op2(e21,e21),
inference(cnf_transformation,[],[f11]) ).
fof(f329,plain,
e20 = op2(e20,e20),
inference(cnf_transformation,[],[f11]) ).
fof(f330,plain,
e11 = op1(op1(e12,e13),e13),
inference(cnf_transformation,[],[f12]) ).
fof(f331,plain,
e10 = op1(e12,e13),
inference(cnf_transformation,[],[f12]) ).
fof(f332,plain,
e21 = op2(op2(e22,e23),e23),
inference(cnf_transformation,[],[f13]) ).
fof(f333,plain,
e20 = op2(e22,e23),
inference(cnf_transformation,[],[f13]) ).
fof(f334,plain,
h1(e11) = op2(op2(e20,e21),e21),
inference(cnf_transformation,[],[f14]) ).
fof(f335,plain,
op2(e20,e21) = h1(e10),
inference(cnf_transformation,[],[f14]) ).
fof(f336,plain,
e21 = h1(e13),
inference(cnf_transformation,[],[f14]) ).
fof(f337,plain,
e20 = h1(e12),
inference(cnf_transformation,[],[f14]) ).
fof(f382,plain,
( e21 != h1(e13)
| ~ sP35 ),
inference(cnf_transformation,[],[f66]) ).
fof(f389,plain,
( e22 != h1(e10)
| ~ sP34 ),
inference(cnf_transformation,[],[f67]) ).
fof(f392,plain,
( e23 != h1(e11)
| ~ sP33 ),
inference(cnf_transformation,[],[f68]) ).
fof(f571,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(e12)
| sP35
| sP34
| sP33 ),
inference(cnf_transformation,[],[f65]) ).
fof(f1631,definition,
( spl36_254
<=> sP33 ),
introduced(definition,[new_symbols(definition,[spl36_254])],[avatar_definition]) ).
fof(f1635,definition,
( spl36_255
<=> sP34 ),
introduced(definition,[new_symbols(definition,[spl36_255])],[avatar_definition]) ).
fof(f1639,definition,
( spl36_256
<=> sP35 ),
introduced(definition,[new_symbols(definition,[spl36_256])],[avatar_definition]) ).
fof(f1647,definition,
( spl36_258
<=> h1(op1(e13,e13)) = op2(h1(e13),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl36_258])],[avatar_definition]) ).
fof(f1649,plain,
( h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| spl36_258 ),
inference(avatar_component_clause,[],[f1647]) ).
fof(f1651,definition,
( spl36_259
<=> h1(op1(e13,e12)) = op2(h1(e13),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl36_259])],[avatar_definition]) ).
fof(f1653,plain,
( h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| spl36_259 ),
inference(avatar_component_clause,[],[f1651]) ).
fof(f1655,definition,
( spl36_260
<=> h1(op1(e13,e11)) = op2(h1(e13),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl36_260])],[avatar_definition]) ).
fof(f1657,plain,
( h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| spl36_260 ),
inference(avatar_component_clause,[],[f1655]) ).
fof(f1659,definition,
( spl36_261
<=> h1(op1(e13,e10)) = op2(h1(e13),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl36_261])],[avatar_definition]) ).
fof(f1661,plain,
( h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| spl36_261 ),
inference(avatar_component_clause,[],[f1659]) ).
fof(f1663,definition,
( spl36_262
<=> h1(op1(e12,e13)) = op2(h1(e12),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl36_262])],[avatar_definition]) ).
fof(f1665,plain,
( h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| spl36_262 ),
inference(avatar_component_clause,[],[f1663]) ).
fof(f1667,definition,
( spl36_263
<=> h1(op1(e12,e12)) = op2(h1(e12),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl36_263])],[avatar_definition]) ).
fof(f1669,plain,
( h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| spl36_263 ),
inference(avatar_component_clause,[],[f1667]) ).
fof(f1671,definition,
( spl36_264
<=> h1(op1(e12,e11)) = op2(h1(e12),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl36_264])],[avatar_definition]) ).
fof(f1673,plain,
( h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| spl36_264 ),
inference(avatar_component_clause,[],[f1671]) ).
fof(f1675,definition,
( spl36_265
<=> h1(op1(e12,e10)) = op2(h1(e12),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl36_265])],[avatar_definition]) ).
fof(f1677,plain,
( h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| spl36_265 ),
inference(avatar_component_clause,[],[f1675]) ).
fof(f1679,definition,
( spl36_266
<=> h1(op1(e11,e13)) = op2(h1(e11),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl36_266])],[avatar_definition]) ).
fof(f1681,plain,
( h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| spl36_266 ),
inference(avatar_component_clause,[],[f1679]) ).
fof(f1683,definition,
( spl36_267
<=> h1(op1(e11,e12)) = op2(h1(e11),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl36_267])],[avatar_definition]) ).
fof(f1685,plain,
( h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| spl36_267 ),
inference(avatar_component_clause,[],[f1683]) ).
fof(f1687,definition,
( spl36_268
<=> h1(op1(e11,e11)) = op2(h1(e11),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl36_268])],[avatar_definition]) ).
fof(f1689,plain,
( h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| spl36_268 ),
inference(avatar_component_clause,[],[f1687]) ).
fof(f1691,definition,
( spl36_269
<=> h1(op1(e11,e10)) = op2(h1(e11),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl36_269])],[avatar_definition]) ).
fof(f1693,plain,
( h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| spl36_269 ),
inference(avatar_component_clause,[],[f1691]) ).
fof(f1695,definition,
( spl36_270
<=> h1(op1(e10,e13)) = op2(h1(e10),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl36_270])],[avatar_definition]) ).
fof(f1697,plain,
( h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| spl36_270 ),
inference(avatar_component_clause,[],[f1695]) ).
fof(f1699,definition,
( spl36_271
<=> h1(op1(e10,e12)) = op2(h1(e10),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl36_271])],[avatar_definition]) ).
fof(f1701,plain,
( h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| spl36_271 ),
inference(avatar_component_clause,[],[f1699]) ).
fof(f1703,definition,
( spl36_272
<=> h1(op1(e10,e11)) = op2(h1(e10),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl36_272])],[avatar_definition]) ).
fof(f1705,plain,
( h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| spl36_272 ),
inference(avatar_component_clause,[],[f1703]) ).
fof(f1707,definition,
( spl36_273
<=> h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl36_273])],[avatar_definition]) ).
fof(f1709,plain,
( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| spl36_273 ),
inference(avatar_component_clause,[],[f1707]) ).
fof(f1712,definition,
( spl36_274
<=> e20 = h1(e12) ),
introduced(definition,[new_symbols(definition,[spl36_274])],[avatar_definition]) ).
fof(f1713,plain,
( e20 = h1(e12)
| ~ spl36_274 ),
inference(avatar_component_clause,[],[f1712]) ).
fof(f1715,plain,
( spl36_254
| spl36_255
| spl36_256
| ~ spl36_274
| ~ spl36_258
| ~ spl36_259
| ~ spl36_260
| ~ spl36_261
| ~ spl36_262
| ~ spl36_263
| ~ spl36_264
| ~ spl36_265
| ~ spl36_266
| ~ spl36_267
| ~ spl36_268
| ~ spl36_269
| ~ spl36_270
| ~ spl36_271
| ~ spl36_272
| ~ spl36_273 ),
inference(avatar_split_clause,[],[f571,f1707,f1703,f1699,f1695,f1691,f1687,f1683,f1679,f1675,f1671,f1667,f1663,f1659,f1655,f1651,f1647,f1712,f1639,f1635,f1631]) ).
fof(f2397,definition,
( spl36_411
<=> e23 = h1(e11) ),
introduced(definition,[new_symbols(definition,[spl36_411])],[avatar_definition]) ).
fof(f2398,plain,
( e23 = h1(e11)
| ~ spl36_411 ),
inference(avatar_component_clause,[],[f2397]) ).
fof(f2400,plain,
( ~ spl36_254
| ~ spl36_411 ),
inference(avatar_split_clause,[],[f392,f2397,f1631]) ).
fof(f2422,definition,
( spl36_416
<=> e22 = h1(e10) ),
introduced(definition,[new_symbols(definition,[spl36_416])],[avatar_definition]) ).
fof(f2423,plain,
( e22 = h1(e10)
| ~ spl36_416 ),
inference(avatar_component_clause,[],[f2422]) ).
fof(f2425,plain,
( ~ spl36_255
| ~ spl36_416 ),
inference(avatar_split_clause,[],[f389,f2422,f1635]) ).
fof(f2427,definition,
( spl36_417
<=> e21 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl36_417])],[avatar_definition]) ).
fof(f2428,plain,
( e21 = h1(e13)
| ~ spl36_417 ),
inference(avatar_component_clause,[],[f2427]) ).
fof(f2430,plain,
( ~ spl36_256
| ~ spl36_417 ),
inference(avatar_split_clause,[],[f382,f2427,f1639]) ).
fof(f2468,plain,
spl36_417,
inference(avatar_split_clause,[],[f336,f2427]) ).
fof(f2469,plain,
spl36_274,
inference(avatar_split_clause,[],[f337,f1712]) ).
fof(f2471,definition,
( spl36_421
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl36_421])],[avatar_definition]) ).
fof(f2473,plain,
( e23 = op2(e23,e23)
| ~ spl36_421 ),
inference(avatar_component_clause,[],[f2471]) ).
fof(f2479,definition,
( spl36_423
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl36_423])],[avatar_definition]) ).
fof(f2509,definition,
( spl36_430
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl36_430])],[avatar_definition]) ).
fof(f2511,plain,
( e22 = op2(e21,e23)
| ~ spl36_430 ),
inference(avatar_component_clause,[],[f2509]) ).
fof(f2513,definition,
( spl36_431
<=> e22 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl36_431])],[avatar_definition]) ).
fof(f2515,plain,
( e22 = op2(e20,e23)
| ~ spl36_431 ),
inference(avatar_component_clause,[],[f2513]) ).
fof(f2526,definition,
( spl36_434
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl36_434])],[avatar_definition]) ).
fof(f2528,plain,
( e22 = op2(e23,e20)
| ~ spl36_434 ),
inference(avatar_component_clause,[],[f2526]) ).
fof(f2535,definition,
( spl36_436
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl36_436])],[avatar_definition]) ).
fof(f2537,plain,
( e21 = op2(e22,e23)
| ~ spl36_436 ),
inference(avatar_component_clause,[],[f2535]) ).
fof(f2539,definition,
( spl36_437
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl36_437])],[avatar_definition]) ).
fof(f2543,definition,
( spl36_438
<=> e21 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl36_438])],[avatar_definition]) ).
fof(f2545,plain,
( e21 = op2(e20,e23)
| ~ spl36_438 ),
inference(avatar_component_clause,[],[f2543]) ).
fof(f2548,definition,
( spl36_439
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl36_439])],[avatar_definition]) ).
fof(f2550,plain,
( e21 = op2(e23,e22)
| ~ spl36_439 ),
inference(avatar_component_clause,[],[f2548]) ).
fof(f2565,definition,
( spl36_443
<=> e20 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl36_443])],[avatar_definition]) ).
fof(f2567,plain,
( e20 = op2(e22,e23)
| ~ spl36_443 ),
inference(avatar_component_clause,[],[f2565]) ).
fof(f2569,definition,
( spl36_444
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl36_444])],[avatar_definition]) ).
fof(f2582,definition,
( spl36_447
<=> e20 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl36_447])],[avatar_definition]) ).
fof(f2584,plain,
( e20 = op2(e23,e21)
| ~ spl36_447 ),
inference(avatar_component_clause,[],[f2582]) ).
fof(f2595,definition,
( spl36_450
<=> e23 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl36_450])],[avatar_definition]) ).
fof(f2599,definition,
( spl36_451
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl36_451])],[avatar_definition]) ).
fof(f2601,plain,
( e23 = op2(e20,e22)
| ~ spl36_451 ),
inference(avatar_component_clause,[],[f2599]) ).
fof(f2604,definition,
( spl36_452
<=> e23 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl36_452])],[avatar_definition]) ).
fof(f2606,plain,
( e23 = op2(e22,e21)
| ~ spl36_452 ),
inference(avatar_component_clause,[],[f2604]) ).
fof(f2613,definition,
( spl36_454
<=> e22 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl36_454])],[avatar_definition]) ).
fof(f2615,plain,
( e22 = op2(e22,e22)
| ~ spl36_454 ),
inference(avatar_component_clause,[],[f2613]) ).
fof(f2617,definition,
( spl36_455
<=> e22 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl36_455])],[avatar_definition]) ).
fof(f2621,definition,
( spl36_456
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl36_456])],[avatar_definition]) ).
fof(f2626,definition,
( spl36_457
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl36_457])],[avatar_definition]) ).
fof(f2630,definition,
( spl36_458
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl36_458])],[avatar_definition]) ).
fof(f2632,plain,
( e22 = op2(e22,e20)
| ~ spl36_458 ),
inference(avatar_component_clause,[],[f2630]) ).
fof(f2635,definition,
( spl36_459
<=> e21 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl36_459])],[avatar_definition]) ).
fof(f2637,plain,
( e21 = op2(e22,e22)
| ~ spl36_459 ),
inference(avatar_component_clause,[],[f2635]) ).
fof(f2639,definition,
( spl36_460
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl36_460])],[avatar_definition]) ).
fof(f2643,definition,
( spl36_461
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl36_461])],[avatar_definition]) ).
fof(f2646,plain,
( spl36_439
| spl36_459
| spl36_460
| spl36_461 ),
inference(avatar_split_clause,[],[f178,f2643,f2639,f2635,f2548]) ).
fof(f2648,definition,
( spl36_462
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl36_462])],[avatar_definition]) ).
fof(f2652,definition,
( spl36_463
<=> e21 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl36_463])],[avatar_definition]) ).
fof(f2654,plain,
( e21 = op2(e22,e20)
| ~ spl36_463 ),
inference(avatar_component_clause,[],[f2652]) ).
fof(f2655,plain,
( spl36_436
| spl36_459
| spl36_462
| spl36_463 ),
inference(avatar_split_clause,[],[f179,f2652,f2648,f2635,f2535]) ).
fof(f2661,definition,
( spl36_465
<=> e20 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl36_465])],[avatar_definition]) ).
fof(f2665,definition,
( spl36_466
<=> e20 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl36_466])],[avatar_definition]) ).
fof(f2670,definition,
( spl36_467
<=> e20 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl36_467])],[avatar_definition]) ).
fof(f2688,definition,
( spl36_471
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl36_471])],[avatar_definition]) ).
fof(f2697,definition,
( spl36_473
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl36_473])],[avatar_definition]) ).
fof(f2699,plain,
( e22 = op2(e20,e21)
| ~ spl36_473 ),
inference(avatar_component_clause,[],[f2697]) ).
fof(f2702,definition,
( spl36_474
<=> e22 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl36_474])],[avatar_definition]) ).
fof(f2707,definition,
( spl36_475
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl36_475])],[avatar_definition]) ).
fof(f2709,plain,
( e21 = op2(e21,e21)
| ~ spl36_475 ),
inference(avatar_component_clause,[],[f2707]) ).
fof(f2716,definition,
( spl36_477
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl36_477])],[avatar_definition]) ).
fof(f2721,definition,
( spl36_478
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl36_478])],[avatar_definition]) ).
fof(f2723,plain,
( e20 = op2(e21,e21)
| ~ spl36_478 ),
inference(avatar_component_clause,[],[f2721]) ).
fof(f2725,definition,
( spl36_479
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl36_479])],[avatar_definition]) ).
fof(f2728,plain,
( spl36_447
| spl36_467
| spl36_478
| spl36_479 ),
inference(avatar_split_clause,[],[f188,f2725,f2721,f2670,f2582]) ).
fof(f2730,definition,
( spl36_480
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl36_480])],[avatar_definition]) ).
fof(f2741,definition,
( spl36_482
<=> op2(e20,e20) = e22 ),
introduced(definition,[new_symbols(definition,[spl36_482])],[avatar_definition]) ).
fof(f2743,plain,
( op2(e20,e20) = e22
| ~ spl36_482 ),
inference(avatar_component_clause,[],[f2741]) ).
fof(f2744,plain,
( spl36_434
| spl36_458
| spl36_474
| spl36_482 ),
inference(avatar_split_clause,[],[f192,f2741,f2702,f2630,f2526]) ).
fof(f2745,plain,
( spl36_431
| spl36_456
| spl36_473
| spl36_482 ),
inference(avatar_split_clause,[],[f193,f2741,f2697,f2621,f2513]) ).
fof(f2753,definition,
( spl36_484
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl36_484])],[avatar_definition]) ).
fof(f2755,plain,
( e20 = op2(e20,e20)
| ~ spl36_484 ),
inference(avatar_component_clause,[],[f2753]) ).
fof(f2764,plain,
( spl36_452
| spl36_457
| spl36_462
| spl36_467 ),
inference(avatar_split_clause,[],[f156,f2670,f2648,f2626,f2604]) ).
fof(f2766,plain,
( spl36_423
| spl36_430
| spl36_437
| spl36_444 ),
inference(avatar_split_clause,[],[f158,f2569,f2539,f2509,f2479]) ).
fof(f2767,plain,
( spl36_450
| spl36_455
| spl36_460
| spl36_465 ),
inference(avatar_split_clause,[],[f159,f2661,f2639,f2617,f2595]) ).
fof(f2769,plain,
( spl36_471
| spl36_474
| spl36_477
| spl36_480 ),
inference(avatar_split_clause,[],[f161,f2730,f2716,f2702,f2688]) ).
fof(f2771,plain,
( spl36_451
| spl36_456
| spl36_461
| spl36_466 ),
inference(avatar_split_clause,[],[f163,f2665,f2643,f2621,f2599]) ).
fof(f2775,definition,
( spl36_485
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl36_485])],[avatar_definition]) ).
fof(f2777,plain,
( e13 = op1(e13,e13)
| ~ spl36_485 ),
inference(avatar_component_clause,[],[f2775]) ).
fof(f2783,definition,
( spl36_487
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl36_487])],[avatar_definition]) ).
fof(f2792,definition,
( spl36_489
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl36_489])],[avatar_definition]) ).
fof(f2800,definition,
( spl36_491
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl36_491])],[avatar_definition]) ).
fof(f2813,definition,
( spl36_494
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl36_494])],[avatar_definition]) ).
fof(f2815,plain,
( e12 = op1(e11,e13)
| ~ spl36_494 ),
inference(avatar_component_clause,[],[f2813]) ).
fof(f2822,definition,
( spl36_496
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl36_496])],[avatar_definition]) ).
fof(f2830,definition,
( spl36_498
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl36_498])],[avatar_definition]) ).
fof(f2832,plain,
( e12 = op1(e13,e10)
| ~ spl36_498 ),
inference(avatar_component_clause,[],[f2830]) ).
fof(f2843,definition,
( spl36_501
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl36_501])],[avatar_definition]) ).
fof(f2847,definition,
( spl36_502
<=> e11 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl36_502])],[avatar_definition]) ).
fof(f2849,plain,
( e11 = op1(e10,e13)
| ~ spl36_502 ),
inference(avatar_component_clause,[],[f2847]) ).
fof(f2852,definition,
( spl36_503
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl36_503])],[avatar_definition]) ).
fof(f2854,plain,
( e11 = op1(e13,e12)
| ~ spl36_503 ),
inference(avatar_component_clause,[],[f2852]) ).
fof(f2860,definition,
( spl36_505
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl36_505])],[avatar_definition]) ).
fof(f2869,definition,
( spl36_507
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl36_507])],[avatar_definition]) ).
fof(f2871,plain,
( e10 = op1(e12,e13)
| ~ spl36_507 ),
inference(avatar_component_clause,[],[f2869]) ).
fof(f2873,definition,
( spl36_508
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl36_508])],[avatar_definition]) ).
fof(f2882,definition,
( spl36_510
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl36_510])],[avatar_definition]) ).
fof(f2886,definition,
( spl36_511
<=> e10 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl36_511])],[avatar_definition]) ).
fof(f2888,plain,
( e10 = op1(e13,e11)
| ~ spl36_511 ),
inference(avatar_component_clause,[],[f2886]) ).
fof(f2890,definition,
( spl36_512
<=> e10 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl36_512])],[avatar_definition]) ).
fof(f2899,definition,
( spl36_514
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl36_514])],[avatar_definition]) ).
fof(f2903,definition,
( spl36_515
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl36_515])],[avatar_definition]) ).
fof(f2905,plain,
( e13 = op1(e10,e12)
| ~ spl36_515 ),
inference(avatar_component_clause,[],[f2903]) ).
fof(f2908,definition,
( spl36_516
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl36_516])],[avatar_definition]) ).
fof(f2910,plain,
( e13 = op1(e12,e11)
| ~ spl36_516 ),
inference(avatar_component_clause,[],[f2908]) ).
fof(f2912,definition,
( spl36_517
<=> e13 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl36_517])],[avatar_definition]) ).
fof(f2917,definition,
( spl36_518
<=> e12 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl36_518])],[avatar_definition]) ).
fof(f2919,plain,
( e12 = op1(e12,e12)
| ~ spl36_518 ),
inference(avatar_component_clause,[],[f2917]) ).
fof(f2921,definition,
( spl36_519
<=> e12 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl36_519])],[avatar_definition]) ).
fof(f2925,definition,
( spl36_520
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl36_520])],[avatar_definition]) ).
fof(f2930,definition,
( spl36_521
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl36_521])],[avatar_definition]) ).
fof(f2934,definition,
( spl36_522
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl36_522])],[avatar_definition]) ).
fof(f2943,definition,
( spl36_524
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl36_524])],[avatar_definition]) ).
fof(f2947,definition,
( spl36_525
<=> e11 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl36_525])],[avatar_definition]) ).
fof(f2952,definition,
( spl36_526
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl36_526])],[avatar_definition]) ).
fof(f2956,definition,
( spl36_527
<=> e11 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl36_527])],[avatar_definition]) ).
fof(f2958,plain,
( e11 = op1(e12,e10)
| ~ spl36_527 ),
inference(avatar_component_clause,[],[f2956]) ).
fof(f2965,definition,
( spl36_529
<=> e10 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl36_529])],[avatar_definition]) ).
fof(f2967,plain,
( e10 = op1(e11,e12)
| ~ spl36_529 ),
inference(avatar_component_clause,[],[f2965]) ).
fof(f2969,definition,
( spl36_530
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl36_530])],[avatar_definition]) ).
fof(f2974,definition,
( spl36_531
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl36_531])],[avatar_definition]) ).
fof(f2978,definition,
( spl36_532
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl36_532])],[avatar_definition]) ).
fof(f2987,definition,
( spl36_534
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl36_534])],[avatar_definition]) ).
fof(f2992,definition,
( spl36_535
<=> e13 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl36_535])],[avatar_definition]) ).
fof(f2994,plain,
( e13 = op1(e11,e10)
| ~ spl36_535 ),
inference(avatar_component_clause,[],[f2992]) ).
fof(f3001,definition,
( spl36_537
<=> e12 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl36_537])],[avatar_definition]) ).
fof(f3003,plain,
( e12 = op1(e10,e11)
| ~ spl36_537 ),
inference(avatar_component_clause,[],[f3001]) ).
fof(f3006,definition,
( spl36_538
<=> e12 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl36_538])],[avatar_definition]) ).
fof(f3011,definition,
( spl36_539
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl36_539])],[avatar_definition]) ).
fof(f3013,plain,
( e11 = op1(e11,e11)
| ~ spl36_539 ),
inference(avatar_component_clause,[],[f3011]) ).
fof(f3015,definition,
( spl36_540
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl36_540])],[avatar_definition]) ).
fof(f3020,definition,
( spl36_541
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl36_541])],[avatar_definition]) ).
fof(f3025,definition,
( spl36_542
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl36_542])],[avatar_definition]) ).
fof(f3027,plain,
( e10 = op1(e11,e11)
| ~ spl36_542 ),
inference(avatar_component_clause,[],[f3025]) ).
fof(f3029,definition,
( spl36_543
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl36_543])],[avatar_definition]) ).
fof(f3032,plain,
( spl36_511
| spl36_531
| spl36_542
| spl36_543 ),
inference(avatar_split_clause,[],[f140,f3029,f3025,f2974,f2886]) ).
fof(f3034,definition,
( spl36_544
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl36_544])],[avatar_definition]) ).
fof(f3057,definition,
( spl36_548
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl36_548])],[avatar_definition]) ).
fof(f3059,plain,
( e10 = op1(e10,e10)
| ~ spl36_548 ),
inference(avatar_component_clause,[],[f3057]) ).
fof(f3063,plain,
( spl36_489
| spl36_496
| spl36_503
| spl36_510 ),
inference(avatar_split_clause,[],[f103,f2882,f2852,f2822,f2792]) ).
fof(f3065,plain,
( spl36_491
| spl36_498
| spl36_505
| spl36_512 ),
inference(avatar_split_clause,[],[f105,f2890,f2860,f2830,f2800]) ).
fof(f3068,plain,
( spl36_516
| spl36_521
| spl36_526
| spl36_531 ),
inference(avatar_split_clause,[],[f108,f2974,f2952,f2930,f2908]) ).
fof(f3069,plain,
( spl36_517
| spl36_522
| spl36_527
| spl36_532 ),
inference(avatar_split_clause,[],[f109,f2978,f2956,f2934,f2912]) ).
fof(f3070,plain,
( spl36_487
| spl36_494
| spl36_501
| spl36_508 ),
inference(avatar_split_clause,[],[f110,f2873,f2843,f2813,f2783]) ).
fof(f3071,plain,
( spl36_514
| spl36_519
| spl36_524
| spl36_529 ),
inference(avatar_split_clause,[],[f111,f2965,f2943,f2921,f2899]) ).
fof(f3073,plain,
( spl36_535
| spl36_538
| spl36_541
| spl36_544 ),
inference(avatar_split_clause,[],[f113,f3034,f3020,f3006,f2992]) ).
fof(f3075,plain,
( spl36_515
| spl36_520
| spl36_525
| spl36_530 ),
inference(avatar_split_clause,[],[f115,f2969,f2947,f2925,f2903]) ).
fof(f3076,plain,
( spl36_534
| spl36_537
| spl36_540
| spl36_543 ),
inference(avatar_split_clause,[],[f116,f3029,f3015,f3001,f2987]) ).
fof(f3081,plain,
spl36_485,
inference(avatar_split_clause,[],[f322,f2775]) ).
fof(f3083,plain,
spl36_518,
inference(avatar_split_clause,[],[f323,f2917]) ).
fof(f3084,plain,
spl36_539,
inference(avatar_split_clause,[],[f324,f3011]) ).
fof(f3087,plain,
spl36_548,
inference(avatar_split_clause,[],[f325,f3057]) ).
fof(f3088,plain,
spl36_421,
inference(avatar_split_clause,[],[f326,f2471]) ).
fof(f3089,plain,
spl36_454,
inference(avatar_split_clause,[],[f327,f2613]) ).
fof(f3091,plain,
spl36_475,
inference(avatar_split_clause,[],[f328,f2707]) ).
fof(f3092,plain,
spl36_484,
inference(avatar_split_clause,[],[f329,f2753]) ).
fof(f3093,plain,
spl36_507,
inference(avatar_split_clause,[],[f331,f2869]) ).
fof(f3095,plain,
spl36_443,
inference(avatar_split_clause,[],[f333,f2565]) ).
fof(f3108,plain,
( e21 = e22
| ~ spl36_431
| ~ spl36_438 ),
inference(forward_demodulation,[],[f2545,f2515]) ).
fof(f3109,plain,
( $false
| ~ spl36_431
| ~ spl36_438 ),
inference(forward_subsumption_resolution,[],[f3108,f302]) ).
fof(f3110,plain,
( ~ spl36_431
| ~ spl36_438 ),
inference(avatar_contradiction_clause,[],[f3109]) ).
fof(f3119,plain,
( op2(e21,e21) != h1(op1(e13,e13))
| spl36_258
| ~ spl36_417 ),
inference(superposition,[],[f1649,f2428]) ).
fof(f3128,plain,
( e20 = e21
| ~ spl36_436
| ~ spl36_443 ),
inference(superposition,[],[f2567,f2537]) ).
fof(f3133,plain,
( $false
| ~ spl36_436
| ~ spl36_443 ),
inference(forward_subsumption_resolution,[],[f3128,f305]) ).
fof(f3134,plain,
( ~ spl36_436
| ~ spl36_443 ),
inference(avatar_contradiction_clause,[],[f3133]) ).
fof(f3243,plain,
( e21 = e22
| ~ spl36_454
| ~ spl36_459 ),
inference(forward_demodulation,[],[f2637,f2615]) ).
fof(f3244,plain,
( $false
| ~ spl36_454
| ~ spl36_459 ),
inference(forward_subsumption_resolution,[],[f3243,f302]) ).
fof(f3245,plain,
( ~ spl36_454
| ~ spl36_459 ),
inference(avatar_contradiction_clause,[],[f3244]) ).
fof(f3272,plain,
( e21 = e22
| ~ spl36_458
| ~ spl36_463 ),
inference(forward_demodulation,[],[f2654,f2632]) ).
fof(f3273,plain,
( $false
| ~ spl36_458
| ~ spl36_463 ),
inference(forward_subsumption_resolution,[],[f3272,f302]) ).
fof(f3274,plain,
( ~ spl36_458
| ~ spl36_463 ),
inference(avatar_contradiction_clause,[],[f3273]) ).
fof(f3327,plain,
( e20 = e21
| ~ spl36_475
| ~ spl36_478 ),
inference(superposition,[],[f2723,f2709]) ).
fof(f3333,plain,
( $false
| ~ spl36_475
| ~ spl36_478 ),
inference(forward_subsumption_resolution,[],[f3327,f305]) ).
fof(f3334,plain,
( ~ spl36_475
| ~ spl36_478 ),
inference(avatar_contradiction_clause,[],[f3333]) ).
fof(f3345,plain,
( e20 = e22
| ~ spl36_482
| ~ spl36_484 ),
inference(forward_demodulation,[],[f2755,f2743]) ).
fof(f3346,plain,
( $false
| ~ spl36_482
| ~ spl36_484 ),
inference(forward_subsumption_resolution,[],[f3345,f304]) ).
fof(f3347,plain,
( ~ spl36_482
| ~ spl36_484 ),
inference(avatar_contradiction_clause,[],[f3346]) ).
fof(f3371,plain,
( op2(e21,e21) != h1(e13)
| spl36_258
| ~ spl36_417
| ~ spl36_485 ),
inference(superposition,[],[f3119,f2777]) ).
fof(f3372,plain,
( e21 != op2(e21,e21)
| spl36_258
| ~ spl36_417
| ~ spl36_485 ),
inference(forward_demodulation,[],[f3371,f2428]) ).
fof(f3384,plain,
( $false
| spl36_258
| ~ spl36_417
| ~ spl36_475
| ~ spl36_485 ),
inference(forward_subsumption_resolution,[],[f3372,f2709]) ).
fof(f3385,plain,
( spl36_258
| ~ spl36_417
| ~ spl36_475
| ~ spl36_485 ),
inference(avatar_contradiction_clause,[],[f3384]) ).
fof(f3730,plain,
( e10 = e11
| ~ spl36_539
| ~ spl36_542 ),
inference(superposition,[],[f3027,f3013]) ).
fof(f3735,plain,
( $false
| ~ spl36_539
| ~ spl36_542 ),
inference(forward_subsumption_resolution,[],[f3730,f299]) ).
fof(f3736,plain,
( ~ spl36_539
| ~ spl36_542 ),
inference(avatar_contradiction_clause,[],[f3735]) ).
fof(f3750,plain,
( e22 = h1(e10)
| ~ spl36_473 ),
inference(forward_demodulation,[],[f335,f2699]) ).
fof(f3751,plain,
( spl36_416
| ~ spl36_473 ),
inference(avatar_split_clause,[],[f3750,f2697,f2422]) ).
fof(f3794,plain,
( e13 != op1(e13,e12)
| ~ spl36_485 ),
inference(forward_demodulation,[],[f198,f2777]) ).
fof(f3798,plain,
( h1(op1(e10,e11)) != op2(e22,h1(e11))
| spl36_272
| ~ spl36_416 ),
inference(superposition,[],[f1705,f2423]) ).
fof(f3799,plain,
( h1(e12) != op2(e22,h1(e11))
| spl36_272
| ~ spl36_416
| ~ spl36_537 ),
inference(forward_demodulation,[],[f3798,f3003]) ).
fof(f3800,plain,
( e20 != op2(e22,h1(e11))
| spl36_272
| ~ spl36_274
| ~ spl36_416
| ~ spl36_537 ),
inference(forward_demodulation,[],[f3799,f1713]) ).
fof(f3803,plain,
( e13 != op1(e13,e10)
| ~ spl36_485 ),
inference(forward_demodulation,[],[f201,f2777]) ).
fof(f3811,plain,
( e10 != op1(e12,e11)
| ~ spl36_507 ),
inference(forward_demodulation,[],[f205,f2871]) ).
fof(f3813,plain,
( e12 != op1(e12,e11)
| ~ spl36_518 ),
inference(forward_demodulation,[],[f206,f2919]) ).
fof(f3815,plain,
( e10 != op1(e12,e10)
| ~ spl36_507 ),
inference(forward_demodulation,[],[f207,f2871]) ).
fof(f3817,plain,
( e12 != op1(e12,e10)
| ~ spl36_518 ),
inference(forward_demodulation,[],[f208,f2919]) ).
fof(f3826,plain,
( e12 != op1(e11,e10)
| ~ spl36_494 ),
inference(forward_demodulation,[],[f213,f2815]) ).
fof(f3830,plain,
( e11 != op1(e11,e10)
| ~ spl36_539 ),
inference(forward_demodulation,[],[f215,f3013]) ).
fof(f3832,plain,
( e11 != op1(e10,e12)
| ~ spl36_502 ),
inference(forward_demodulation,[],[f216,f2849]) ).
fof(f3834,plain,
( e11 != op1(e10,e11)
| ~ spl36_502 ),
inference(forward_demodulation,[],[f217,f2849]) ).
fof(f3836,plain,
( e13 != op1(e10,e11)
| ~ spl36_515 ),
inference(forward_demodulation,[],[f218,f2905]) ).
fof(f3844,plain,
( e13 != op1(e11,e13)
| ~ spl36_485 ),
inference(forward_demodulation,[],[f223,f2777]) ).
fof(f3846,plain,
( e10 != op1(e11,e13)
| ~ spl36_507 ),
inference(forward_demodulation,[],[f224,f2871]) ).
fof(f3857,plain,
( e12 != op1(e11,e12)
| ~ spl36_518 ),
inference(forward_demodulation,[],[f230,f2919]) ).
fof(f3861,plain,
( e12 != op1(e10,e12)
| ~ spl36_518 ),
inference(forward_demodulation,[],[f232,f2919]) ).
fof(f3897,plain,
( e20 != op2(e22,e21)
| ~ spl36_443 ),
inference(forward_demodulation,[],[f253,f2567]) ).
fof(f3899,plain,
( e22 != op2(e22,e21)
| ~ spl36_454 ),
inference(forward_demodulation,[],[f254,f2615]) ).
fof(f3909,plain,
( e22 != op2(e21,e20)
| ~ spl36_430 ),
inference(forward_demodulation,[],[f261,f2511]) ).
fof(f3913,plain,
( e21 != op2(e21,e20)
| ~ spl36_475 ),
inference(forward_demodulation,[],[f263,f2709]) ).
fof(f3915,plain,
( e21 != op2(e20,e22)
| ~ spl36_438 ),
inference(forward_demodulation,[],[f264,f2545]) ).
fof(f3926,plain,
( e23 != op2(e21,e23)
| ~ spl36_421 ),
inference(forward_demodulation,[],[f271,f2473]) ).
fof(f3928,plain,
( e20 != op2(e21,e23)
| ~ spl36_443 ),
inference(forward_demodulation,[],[f272,f2567]) ).
fof(f3939,plain,
( e22 != op2(e21,e22)
| ~ spl36_454 ),
inference(forward_demodulation,[],[f278,f2615]) ).
fof(f3942,plain,
( e22 != op2(e20,e22)
| ~ spl36_454 ),
inference(forward_demodulation,[],[f280,f2615]) ).
fof(f3965,plain,
( e11 = op1(e10,e13)
| ~ spl36_507 ),
inference(forward_demodulation,[],[f330,f2871]) ).
fof(f3966,plain,
( e21 = op2(e20,e23)
| ~ spl36_443 ),
inference(forward_demodulation,[],[f332,f2567]) ).
fof(f3967,plain,
( op2(e22,e21) = h1(e11)
| ~ spl36_473 ),
inference(forward_demodulation,[],[f334,f2699]) ).
fof(f3968,plain,
( e23 = h1(e11)
| ~ spl36_452
| ~ spl36_473 ),
inference(forward_demodulation,[],[f3967,f2606]) ).
fof(f3969,plain,
( spl36_411
| ~ spl36_452
| ~ spl36_473 ),
inference(avatar_split_clause,[],[f3968,f2697,f2604,f2397]) ).
fof(f4037,plain,
( e21 != op2(e21,e22)
| ~ spl36_475 ),
inference(forward_demodulation,[],[f260,f2709]) ).
fof(f4040,plain,
( e23 != op2(e21,e22)
| ~ spl36_451 ),
inference(forward_demodulation,[],[f281,f2601]) ).
fof(f4042,plain,
( ~ spl36_455
| ~ spl36_454 ),
inference(avatar_split_clause,[],[f3939,f2613,f2617]) ).
fof(f4048,plain,
( ~ spl36_460
| ~ spl36_475 ),
inference(avatar_split_clause,[],[f4037,f2707,f2639]) ).
fof(f4050,plain,
( ~ spl36_450
| ~ spl36_451 ),
inference(avatar_split_clause,[],[f4040,f2599,f2595]) ).
fof(f4060,plain,
( ~ spl36_474
| ~ spl36_430 ),
inference(avatar_split_clause,[],[f3909,f2509,f2702]) ).
fof(f4061,plain,
( ~ spl36_477
| ~ spl36_475 ),
inference(avatar_split_clause,[],[f3913,f2707,f2716]) ).
fof(f4064,plain,
( e20 != op2(e21,e20)
| ~ spl36_484 ),
inference(forward_demodulation,[],[f293,f2755]) ).
fof(f4068,plain,
( ~ spl36_480
| ~ spl36_484 ),
inference(avatar_split_clause,[],[f4064,f2753,f2730]) ).
fof(f4116,plain,
( ~ spl36_540
| ~ spl36_502 ),
inference(avatar_split_clause,[],[f3834,f2847,f3015]) ).
fof(f4117,plain,
( e10 != op1(e10,e11)
| ~ spl36_548 ),
inference(forward_demodulation,[],[f221,f3059]) ).
fof(f4120,plain,
( ~ spl36_534
| ~ spl36_515 ),
inference(avatar_split_clause,[],[f3836,f2903,f2987]) ).
fof(f4121,plain,
( ~ spl36_532
| ~ spl36_507 ),
inference(avatar_split_clause,[],[f3815,f2869,f2978]) ).
fof(f4122,plain,
( ~ spl36_522
| ~ spl36_518 ),
inference(avatar_split_clause,[],[f3817,f2917,f2934]) ).
fof(f4124,plain,
( e13 != op1(e12,e10)
| ~ spl36_535 ),
inference(forward_demodulation,[],[f242,f2994]) ).
fof(f4126,plain,
( ~ spl36_531
| ~ spl36_507 ),
inference(avatar_split_clause,[],[f3811,f2869,f2974]) ).
fof(f4127,plain,
( ~ spl36_521
| ~ spl36_518 ),
inference(avatar_split_clause,[],[f3813,f2917,f2930]) ).
fof(f4129,plain,
( e11 != op1(e12,e11)
| ~ spl36_539 ),
inference(forward_demodulation,[],[f236,f3013]) ).
fof(f4135,plain,
( ~ spl36_543
| ~ spl36_548 ),
inference(avatar_split_clause,[],[f4117,f3057,f3029]) ).
fof(f4136,plain,
( ~ spl36_517
| ~ spl36_535 ),
inference(avatar_split_clause,[],[f4124,f2992,f2912]) ).
fof(f4138,plain,
( ~ spl36_526
| ~ spl36_539 ),
inference(avatar_split_clause,[],[f4129,f3011,f2952]) ).
fof(f4270,plain,
( e20 != op2(e22,e23)
| spl36_272
| ~ spl36_274
| ~ spl36_411
| ~ spl36_416
| ~ spl36_537 ),
inference(superposition,[],[f3800,f2398]) ).
fof(f4273,plain,
( $false
| spl36_272
| ~ spl36_274
| ~ spl36_411
| ~ spl36_416
| ~ spl36_443
| ~ spl36_537 ),
inference(forward_subsumption_resolution,[],[f4270,f2567]) ).
fof(f4274,plain,
( spl36_272
| ~ spl36_274
| ~ spl36_411
| ~ spl36_416
| ~ spl36_443
| ~ spl36_537 ),
inference(avatar_contradiction_clause,[],[f4273]) ).
fof(f4276,plain,
( h1(op1(e13,e12)) != op2(h1(e13),e20)
| spl36_259
| ~ spl36_274 ),
inference(forward_demodulation,[],[f1653,f1713]) ).
fof(f4278,plain,
( op2(e21,e20) != h1(op1(e13,e12))
| spl36_259
| ~ spl36_274
| ~ spl36_417 ),
inference(forward_demodulation,[],[f4276,f2428]) ).
fof(f4280,plain,
( op2(e21,e20) != h1(e11)
| spl36_259
| ~ spl36_274
| ~ spl36_417
| ~ spl36_503 ),
inference(forward_demodulation,[],[f4278,f2854]) ).
fof(f4282,plain,
( e23 != op2(e21,e20)
| spl36_259
| ~ spl36_274
| ~ spl36_411
| ~ spl36_417
| ~ spl36_503 ),
inference(forward_demodulation,[],[f4280,f2398]) ).
fof(f4283,plain,
( ~ spl36_471
| spl36_259
| ~ spl36_274
| ~ spl36_411
| ~ spl36_417
| ~ spl36_503 ),
inference(avatar_split_clause,[],[f4282,f2852,f2427,f2397,f1712,f1651,f2688]) ).
fof(f4285,plain,
( h1(op1(e13,e10)) != op2(h1(e13),e22)
| spl36_261
| ~ spl36_416 ),
inference(forward_demodulation,[],[f1661,f2423]) ).
fof(f4287,plain,
( op2(e21,e22) != h1(op1(e13,e10))
| spl36_261
| ~ spl36_416
| ~ spl36_417 ),
inference(forward_demodulation,[],[f4285,f2428]) ).
fof(f4289,plain,
( op2(e21,e22) != h1(e12)
| spl36_261
| ~ spl36_416
| ~ spl36_417
| ~ spl36_498 ),
inference(forward_demodulation,[],[f4287,f2832]) ).
fof(f4291,plain,
( e20 != op2(e21,e22)
| spl36_261
| ~ spl36_274
| ~ spl36_416
| ~ spl36_417
| ~ spl36_498 ),
inference(forward_demodulation,[],[f4289,f1713]) ).
fof(f4293,plain,
( ~ spl36_465
| spl36_261
| ~ spl36_274
| ~ spl36_416
| ~ spl36_417
| ~ spl36_498 ),
inference(avatar_split_clause,[],[f4291,f2830,f2427,f2422,f1712,f1659,f2661]) ).
fof(f4294,plain,
( h1(op1(e13,e11)) != op2(h1(e13),e23)
| spl36_260
| ~ spl36_411 ),
inference(forward_demodulation,[],[f1657,f2398]) ).
fof(f4296,plain,
( op2(e21,e23) != h1(op1(e13,e11))
| spl36_260
| ~ spl36_411
| ~ spl36_417 ),
inference(forward_demodulation,[],[f4294,f2428]) ).
fof(f4298,plain,
( op2(e21,e23) != h1(e10)
| spl36_260
| ~ spl36_411
| ~ spl36_417
| ~ spl36_511 ),
inference(forward_demodulation,[],[f4296,f2888]) ).
fof(f4300,plain,
( e22 != op2(e21,e23)
| spl36_260
| ~ spl36_411
| ~ spl36_416
| ~ spl36_417
| ~ spl36_511 ),
inference(forward_demodulation,[],[f4298,f2423]) ).
fof(f4302,plain,
( $false
| spl36_260
| ~ spl36_411
| ~ spl36_416
| ~ spl36_417
| ~ spl36_430
| ~ spl36_511 ),
inference(forward_subsumption_resolution,[],[f4300,f2511]) ).
fof(f4303,plain,
( spl36_260
| ~ spl36_411
| ~ spl36_416
| ~ spl36_417
| ~ spl36_430
| ~ spl36_511 ),
inference(avatar_contradiction_clause,[],[f4302]) ).
fof(f4306,plain,
( op2(e20,e20) != h1(op1(e12,e12))
| spl36_263
| ~ spl36_274 ),
inference(forward_demodulation,[],[f1669,f1713]) ).
fof(f4308,plain,
( op2(e20,e20) != h1(e12)
| spl36_263
| ~ spl36_274
| ~ spl36_518 ),
inference(forward_demodulation,[],[f4306,f2919]) ).
fof(f4310,plain,
( e20 != op2(e20,e20)
| spl36_263
| ~ spl36_274
| ~ spl36_518 ),
inference(forward_demodulation,[],[f4308,f1713]) ).
fof(f4312,plain,
( $false
| spl36_263
| ~ spl36_274
| ~ spl36_484
| ~ spl36_518 ),
inference(forward_subsumption_resolution,[],[f4310,f2755]) ).
fof(f4313,plain,
( spl36_263
| ~ spl36_274
| ~ spl36_484
| ~ spl36_518 ),
inference(avatar_contradiction_clause,[],[f4312]) ).
fof(f4314,plain,
( h1(op1(e12,e13)) != op2(h1(e12),e21)
| spl36_262
| ~ spl36_417 ),
inference(forward_demodulation,[],[f1665,f2428]) ).
fof(f4316,plain,
( op2(e20,e21) != h1(op1(e12,e13))
| spl36_262
| ~ spl36_274
| ~ spl36_417 ),
inference(forward_demodulation,[],[f4314,f1713]) ).
fof(f4318,plain,
( op2(e20,e21) != h1(e10)
| spl36_262
| ~ spl36_274
| ~ spl36_417
| ~ spl36_507 ),
inference(forward_demodulation,[],[f4316,f2871]) ).
fof(f4320,plain,
( e22 != op2(e20,e21)
| spl36_262
| ~ spl36_274
| ~ spl36_416
| ~ spl36_417
| ~ spl36_507 ),
inference(forward_demodulation,[],[f4318,f2423]) ).
fof(f4321,plain,
( $false
| spl36_262
| ~ spl36_274
| ~ spl36_416
| ~ spl36_417
| ~ spl36_473
| ~ spl36_507 ),
inference(forward_subsumption_resolution,[],[f4320,f2699]) ).
fof(f4322,plain,
( spl36_262
| ~ spl36_274
| ~ spl36_416
| ~ spl36_417
| ~ spl36_473
| ~ spl36_507 ),
inference(avatar_contradiction_clause,[],[f4321]) ).
fof(f4324,plain,
( h1(op1(e12,e10)) != op2(h1(e12),e22)
| spl36_265
| ~ spl36_416 ),
inference(forward_demodulation,[],[f1677,f2423]) ).
fof(f4326,plain,
( op2(e20,e22) != h1(op1(e12,e10))
| spl36_265
| ~ spl36_274
| ~ spl36_416 ),
inference(forward_demodulation,[],[f4324,f1713]) ).
fof(f4378,plain,
( op2(e22,e22) != h1(op1(e10,e10))
| spl36_273
| ~ spl36_416 ),
inference(forward_demodulation,[],[f1709,f2423]) ).
fof(f4388,plain,
( op2(e22,e22) != h1(e10)
| spl36_273
| ~ spl36_416
| ~ spl36_548 ),
inference(forward_demodulation,[],[f4378,f3059]) ).
fof(f4398,plain,
( e22 != op2(e22,e22)
| spl36_273
| ~ spl36_416
| ~ spl36_548 ),
inference(forward_demodulation,[],[f4388,f2423]) ).
fof(f4409,plain,
( $false
| spl36_273
| ~ spl36_416
| ~ spl36_454
| ~ spl36_548 ),
inference(forward_subsumption_resolution,[],[f4398,f2615]) ).
fof(f4410,plain,
( spl36_273
| ~ spl36_416
| ~ spl36_454
| ~ spl36_548 ),
inference(avatar_contradiction_clause,[],[f4409]) ).
fof(f4423,plain,
( h1(op1(e12,e11)) != op2(h1(e12),e23)
| spl36_264
| ~ spl36_411 ),
inference(forward_demodulation,[],[f1673,f2398]) ).
fof(f4428,plain,
( e11 != op1(e11,e12)
| ~ spl36_539 ),
inference(forward_demodulation,[],[f212,f3013]) ).
fof(f4429,plain,
( e13 != op1(e11,e12)
| ~ spl36_535 ),
inference(forward_demodulation,[],[f214,f2994]) ).
fof(f4431,plain,
( ~ spl36_519
| ~ spl36_518 ),
inference(avatar_split_clause,[],[f3857,f2917,f2921]) ).
fof(f4433,plain,
( ~ spl36_525
| ~ spl36_502 ),
inference(avatar_split_clause,[],[f3832,f2847,f2947]) ).
fof(f4434,plain,
( e10 != op1(e10,e12)
| ~ spl36_548 ),
inference(forward_demodulation,[],[f220,f3059]) ).
fof(f4436,plain,
( ~ spl36_520
| ~ spl36_518 ),
inference(avatar_split_clause,[],[f3861,f2917,f2925]) ).
fof(f4444,plain,
( op2(e20,e23) != h1(op1(e12,e11))
| spl36_264
| ~ spl36_274
| ~ spl36_411 ),
inference(forward_demodulation,[],[f4423,f1713]) ).
fof(f4448,plain,
( ~ spl36_524
| ~ spl36_539 ),
inference(avatar_split_clause,[],[f4428,f3011,f2943]) ).
fof(f4449,plain,
( ~ spl36_514
| ~ spl36_535 ),
inference(avatar_split_clause,[],[f4429,f2992,f2899]) ).
fof(f4450,plain,
( ~ spl36_530
| ~ spl36_548 ),
inference(avatar_split_clause,[],[f4434,f3057,f2969]) ).
fof(f4457,plain,
( op2(e20,e23) != h1(e13)
| spl36_264
| ~ spl36_274
| ~ spl36_411
| ~ spl36_516 ),
inference(forward_demodulation,[],[f4444,f2910]) ).
fof(f4462,plain,
( e21 != op2(e20,e23)
| spl36_264
| ~ spl36_274
| ~ spl36_411
| ~ spl36_417
| ~ spl36_516 ),
inference(forward_demodulation,[],[f4457,f2428]) ).
fof(f4465,plain,
( $false
| spl36_264
| ~ spl36_274
| ~ spl36_411
| ~ spl36_417
| ~ spl36_438
| ~ spl36_516 ),
inference(forward_subsumption_resolution,[],[f4462,f2545]) ).
fof(f4466,plain,
( spl36_264
| ~ spl36_274
| ~ spl36_411
| ~ spl36_417
| ~ spl36_438
| ~ spl36_516 ),
inference(avatar_contradiction_clause,[],[f4465]) ).
fof(f4472,plain,
( h1(op1(e11,e13)) != op2(h1(e11),e21)
| spl36_266
| ~ spl36_417 ),
inference(forward_demodulation,[],[f1681,f2428]) ).
fof(f4484,plain,
( op2(e23,e21) != h1(op1(e11,e13))
| spl36_266
| ~ spl36_411
| ~ spl36_417 ),
inference(forward_demodulation,[],[f4472,f2398]) ).
fof(f4490,plain,
( op2(e23,e21) != h1(e12)
| spl36_266
| ~ spl36_411
| ~ spl36_417
| ~ spl36_494 ),
inference(forward_demodulation,[],[f4484,f2815]) ).
fof(f4496,plain,
( e20 != op2(e23,e21)
| spl36_266
| ~ spl36_274
| ~ spl36_411
| ~ spl36_417
| ~ spl36_494 ),
inference(forward_demodulation,[],[f4490,f1713]) ).
fof(f4499,plain,
( $false
| spl36_266
| ~ spl36_274
| ~ spl36_411
| ~ spl36_417
| ~ spl36_447
| ~ spl36_494 ),
inference(forward_subsumption_resolution,[],[f4496,f2584]) ).
fof(f4500,plain,
( spl36_266
| ~ spl36_274
| ~ spl36_411
| ~ spl36_417
| ~ spl36_447
| ~ spl36_494 ),
inference(avatar_contradiction_clause,[],[f4499]) ).
fof(f4506,plain,
( h1(op1(e11,e12)) != op2(h1(e11),e20)
| spl36_267
| ~ spl36_274 ),
inference(forward_demodulation,[],[f1685,f1713]) ).
fof(f4512,plain,
( op2(e23,e20) != h1(op1(e11,e12))
| spl36_267
| ~ spl36_274
| ~ spl36_411 ),
inference(forward_demodulation,[],[f4506,f2398]) ).
fof(f4518,plain,
( e22 != h1(op1(e11,e12))
| spl36_267
| ~ spl36_274
| ~ spl36_411
| ~ spl36_434 ),
inference(forward_demodulation,[],[f4512,f2528]) ).
fof(f4560,plain,
( e22 != h1(e10)
| spl36_267
| ~ spl36_274
| ~ spl36_411
| ~ spl36_434
| ~ spl36_529 ),
inference(superposition,[],[f4518,f2967]) ).
fof(f4567,plain,
( $false
| spl36_267
| ~ spl36_274
| ~ spl36_411
| ~ spl36_416
| ~ spl36_434
| ~ spl36_529 ),
inference(forward_subsumption_resolution,[],[f4560,f2423]) ).
fof(f4568,plain,
( spl36_267
| ~ spl36_274
| ~ spl36_411
| ~ spl36_416
| ~ spl36_434
| ~ spl36_529 ),
inference(avatar_contradiction_clause,[],[f4567]) ).
fof(f4582,plain,
( op2(e23,e23) != h1(op1(e11,e11))
| spl36_268
| ~ spl36_411 ),
inference(forward_demodulation,[],[f1689,f2398]) ).
fof(f4592,plain,
( op2(e23,e23) != h1(e11)
| spl36_268
| ~ spl36_411
| ~ spl36_539 ),
inference(forward_demodulation,[],[f4582,f3013]) ).
fof(f4602,plain,
( e23 != op2(e23,e23)
| spl36_268
| ~ spl36_411
| ~ spl36_539 ),
inference(forward_demodulation,[],[f4592,f2398]) ).
fof(f4612,plain,
( $false
| spl36_268
| ~ spl36_411
| ~ spl36_421
| ~ spl36_539 ),
inference(forward_subsumption_resolution,[],[f4602,f2473]) ).
fof(f4613,plain,
( spl36_268
| ~ spl36_411
| ~ spl36_421
| ~ spl36_539 ),
inference(avatar_contradiction_clause,[],[f4612]) ).
fof(f4625,plain,
( h1(op1(e11,e10)) != op2(h1(e11),e22)
| spl36_269
| ~ spl36_416 ),
inference(forward_demodulation,[],[f1693,f2423]) ).
fof(f4633,plain,
( op2(e23,e22) != h1(op1(e11,e10))
| spl36_269
| ~ spl36_411
| ~ spl36_416 ),
inference(forward_demodulation,[],[f4625,f2398]) ).
fof(f4641,plain,
( op2(e23,e22) != h1(e13)
| spl36_269
| ~ spl36_411
| ~ spl36_416
| ~ spl36_535 ),
inference(forward_demodulation,[],[f4633,f2994]) ).
fof(f4648,plain,
( e21 != op2(e23,e22)
| spl36_269
| ~ spl36_411
| ~ spl36_416
| ~ spl36_417
| ~ spl36_535 ),
inference(forward_demodulation,[],[f4641,f2428]) ).
fof(f4653,plain,
( $false
| spl36_269
| ~ spl36_411
| ~ spl36_416
| ~ spl36_417
| ~ spl36_439
| ~ spl36_535 ),
inference(forward_subsumption_resolution,[],[f4648,f2550]) ).
fof(f4654,plain,
( spl36_269
| ~ spl36_411
| ~ spl36_416
| ~ spl36_417
| ~ spl36_439
| ~ spl36_535 ),
inference(avatar_contradiction_clause,[],[f4653]) ).
fof(f4659,plain,
( ~ spl36_538
| ~ spl36_494 ),
inference(avatar_split_clause,[],[f3826,f2813,f3006]) ).
fof(f4660,plain,
( ~ spl36_541
| ~ spl36_539 ),
inference(avatar_split_clause,[],[f3830,f3011,f3020]) ).
fof(f4662,plain,
( e10 != op1(e11,e10)
| ~ spl36_548 ),
inference(forward_demodulation,[],[f245,f3059]) ).
fof(f4674,plain,
( ~ spl36_544
| ~ spl36_548 ),
inference(avatar_split_clause,[],[f4662,f3057,f3034]) ).
fof(f4683,plain,
( h1(op1(e10,e13)) != op2(h1(e10),e21)
| spl36_270
| ~ spl36_417 ),
inference(forward_demodulation,[],[f1697,f2428]) ).
fof(f4689,plain,
( op2(e22,e21) != h1(op1(e10,e13))
| spl36_270
| ~ spl36_416
| ~ spl36_417 ),
inference(forward_demodulation,[],[f4683,f2423]) ).
fof(f4693,plain,
( op2(e22,e21) != h1(e11)
| spl36_270
| ~ spl36_416
| ~ spl36_417
| ~ spl36_502 ),
inference(forward_demodulation,[],[f4689,f2849]) ).
fof(f4694,plain,
( e23 != op2(e22,e21)
| spl36_270
| ~ spl36_411
| ~ spl36_416
| ~ spl36_417
| ~ spl36_502 ),
inference(forward_demodulation,[],[f4693,f2398]) ).
fof(f4698,plain,
( h1(op1(e10,e12)) != op2(h1(e10),e20)
| spl36_271
| ~ spl36_274 ),
inference(forward_demodulation,[],[f1701,f1713]) ).
fof(f4700,plain,
( op2(e22,e20) != h1(op1(e10,e12))
| spl36_271
| ~ spl36_274
| ~ spl36_416 ),
inference(forward_demodulation,[],[f4698,f2423]) ).
fof(f4702,plain,
( op2(e22,e20) != h1(e13)
| spl36_271
| ~ spl36_274
| ~ spl36_416
| ~ spl36_515 ),
inference(forward_demodulation,[],[f4700,f2905]) ).
fof(f4704,plain,
( e21 != op2(e22,e20)
| spl36_271
| ~ spl36_274
| ~ spl36_416
| ~ spl36_417
| ~ spl36_515 ),
inference(forward_demodulation,[],[f4702,f2428]) ).
fof(f4705,plain,
( $false
| spl36_271
| ~ spl36_274
| ~ spl36_416
| ~ spl36_417
| ~ spl36_463
| ~ spl36_515 ),
inference(forward_subsumption_resolution,[],[f4704,f2654]) ).
fof(f4706,plain,
( spl36_271
| ~ spl36_274
| ~ spl36_416
| ~ spl36_417
| ~ spl36_463
| ~ spl36_515 ),
inference(avatar_contradiction_clause,[],[f4705]) ).
fof(f4708,plain,
( e20 != op2(e20,e21)
| ~ spl36_484 ),
inference(forward_demodulation,[],[f269,f2755]) ).
fof(f4729,plain,
( spl36_438
| ~ spl36_443 ),
inference(avatar_split_clause,[],[f3966,f2565,f2543]) ).
fof(f4744,plain,
( e21 != op2(e21,e23)
| ~ spl36_475 ),
inference(forward_demodulation,[],[f259,f2709]) ).
fof(f4746,plain,
( ~ spl36_423
| ~ spl36_421 ),
inference(avatar_split_clause,[],[f3926,f2471,f2479]) ).
fof(f4747,plain,
( ~ spl36_444
| ~ spl36_443 ),
inference(avatar_split_clause,[],[f3928,f2565,f2569]) ).
fof(f4758,plain,
( ~ spl36_479
| ~ spl36_484 ),
inference(avatar_split_clause,[],[f4708,f2753,f2725]) ).
fof(f4771,plain,
( ~ spl36_437
| ~ spl36_475 ),
inference(avatar_split_clause,[],[f4744,f2707,f2539]) ).
fof(f4783,plain,
( op2(e20,e22) != h1(e11)
| spl36_265
| ~ spl36_274
| ~ spl36_416
| ~ spl36_527 ),
inference(forward_demodulation,[],[f4326,f2958]) ).
fof(f4803,plain,
( ~ spl36_461
| ~ spl36_438 ),
inference(avatar_split_clause,[],[f3915,f2543,f2643]) ).
fof(f4813,plain,
( e20 != op2(e20,e22)
| ~ spl36_484 ),
inference(forward_demodulation,[],[f268,f2755]) ).
fof(f4815,plain,
( ~ spl36_456
| ~ spl36_454 ),
inference(avatar_split_clause,[],[f3942,f2613,f2621]) ).
fof(f4828,plain,
( e23 != op2(e20,e22)
| spl36_265
| ~ spl36_274
| ~ spl36_411
| ~ spl36_416
| ~ spl36_527 ),
inference(forward_demodulation,[],[f4783,f2398]) ).
fof(f4836,plain,
( ~ spl36_466
| ~ spl36_484 ),
inference(avatar_split_clause,[],[f4813,f2753,f2665]) ).
fof(f4840,plain,
( ~ spl36_451
| spl36_265
| ~ spl36_274
| ~ spl36_411
| ~ spl36_416
| ~ spl36_527 ),
inference(avatar_split_clause,[],[f4828,f2956,f2422,f2397,f1712,f1675,f2599]) ).
fof(f4863,plain,
( ~ spl36_489
| ~ spl36_485 ),
inference(avatar_split_clause,[],[f3794,f2775,f2792]) ).
fof(f4865,plain,
( e12 != op1(e13,e12)
| ~ spl36_518 ),
inference(forward_demodulation,[],[f228,f2919]) ).
fof(f4866,plain,
( e10 != op1(e13,e12)
| ~ spl36_529 ),
inference(forward_demodulation,[],[f229,f2967]) ).
fof(f4876,plain,
( spl36_502
| ~ spl36_507 ),
inference(avatar_split_clause,[],[f3965,f2869,f2847]) ).
fof(f4878,plain,
( ~ spl36_491
| ~ spl36_485 ),
inference(avatar_split_clause,[],[f3803,f2775,f2800]) ).
fof(f4880,plain,
( e11 != op1(e13,e10)
| ~ spl36_527 ),
inference(forward_demodulation,[],[f240,f2958]) ).
fof(f4881,plain,
( e10 != op1(e13,e10)
| ~ spl36_548 ),
inference(forward_demodulation,[],[f243,f3059]) ).
fof(f4887,plain,
( e11 != op1(e11,e13)
| ~ spl36_539 ),
inference(forward_demodulation,[],[f211,f3013]) ).
fof(f4888,plain,
( ~ spl36_487
| ~ spl36_485 ),
inference(avatar_split_clause,[],[f3844,f2775,f2783]) ).
fof(f4889,plain,
( ~ spl36_508
| ~ spl36_507 ),
inference(avatar_split_clause,[],[f3846,f2869,f2873]) ).
fof(f4903,plain,
( ~ spl36_496
| ~ spl36_518 ),
inference(avatar_split_clause,[],[f4865,f2917,f2822]) ).
fof(f4904,plain,
( ~ spl36_510
| ~ spl36_529 ),
inference(avatar_split_clause,[],[f4866,f2965,f2882]) ).
fof(f4908,plain,
( ~ spl36_505
| ~ spl36_527 ),
inference(avatar_split_clause,[],[f4880,f2956,f2860]) ).
fof(f4909,plain,
( ~ spl36_512
| ~ spl36_548 ),
inference(avatar_split_clause,[],[f4881,f3057,f2890]) ).
fof(f4911,plain,
( ~ spl36_501
| ~ spl36_539 ),
inference(avatar_split_clause,[],[f4887,f3011,f2843]) ).
fof(f4941,plain,
( ~ spl36_452
| spl36_270
| ~ spl36_411
| ~ spl36_416
| ~ spl36_417
| ~ spl36_502 ),
inference(avatar_split_clause,[],[f4694,f2847,f2427,f2422,f2397,f1695,f2604]) ).
fof(f4973,plain,
( ~ spl36_467
| ~ spl36_443 ),
inference(avatar_split_clause,[],[f3897,f2565,f2670]) ).
fof(f4974,plain,
( ~ spl36_457
| ~ spl36_454 ),
inference(avatar_split_clause,[],[f3899,f2613,f2626]) ).
fof(f4975,plain,
( e21 != op2(e22,e21)
| ~ spl36_475 ),
inference(forward_demodulation,[],[f284,f2709]) ).
fof(f4989,plain,
( ~ spl36_462
| ~ spl36_475 ),
inference(avatar_split_clause,[],[f4975,f2707,f2648]) ).
cnf(s46,plain,
( spl36_254
| spl36_255
| spl36_256
| ~ spl36_258
| ~ spl36_259
| ~ spl36_260
| ~ spl36_261
| ~ spl36_262
| ~ spl36_263
| ~ spl36_264
| ~ spl36_265
| ~ spl36_266
| ~ spl36_267
| ~ spl36_268
| ~ spl36_269
| ~ spl36_270
| ~ spl36_271
| ~ spl36_272
| ~ spl36_273
| ~ spl36_274 ),
inference(sat_conversion,[],[f1715]) ).
cnf(s183,plain,
( ~ spl36_254
| ~ spl36_411 ),
inference(sat_conversion,[],[f2400]) ).
cnf(s188,plain,
( ~ spl36_255
| ~ spl36_416 ),
inference(sat_conversion,[],[f2425]) ).
cnf(s189,plain,
( ~ spl36_256
| ~ spl36_417 ),
inference(sat_conversion,[],[f2430]) ).
cnf(s215,plain,
spl36_417,
inference(sat_conversion,[],[f2468]) ).
cnf(s216,plain,
spl36_274,
inference(sat_conversion,[],[f2469]) ).
cnf(s229,plain,
( spl36_439
| spl36_459
| spl36_460
| spl36_461 ),
inference(sat_conversion,[],[f2646]) ).
cnf(s230,plain,
( spl36_436
| spl36_459
| spl36_462
| spl36_463 ),
inference(sat_conversion,[],[f2655]) ).
cnf(s239,plain,
( spl36_447
| spl36_467
| spl36_478
| spl36_479 ),
inference(sat_conversion,[],[f2728]) ).
cnf(s243,plain,
( spl36_434
| spl36_458
| spl36_474
| spl36_482 ),
inference(sat_conversion,[],[f2744]) ).
cnf(s244,plain,
( spl36_431
| spl36_456
| spl36_473
| spl36_482 ),
inference(sat_conversion,[],[f2745]) ).
cnf(s255,plain,
( spl36_452
| spl36_457
| spl36_462
| spl36_467 ),
inference(sat_conversion,[],[f2764]) ).
cnf(s257,plain,
( spl36_423
| spl36_430
| spl36_437
| spl36_444 ),
inference(sat_conversion,[],[f2766]) ).
cnf(s258,plain,
( spl36_450
| spl36_455
| spl36_460
| spl36_465 ),
inference(sat_conversion,[],[f2767]) ).
cnf(s260,plain,
( spl36_471
| spl36_474
| spl36_477
| spl36_480 ),
inference(sat_conversion,[],[f2769]) ).
cnf(s262,plain,
( spl36_451
| spl36_456
| spl36_461
| spl36_466 ),
inference(sat_conversion,[],[f2771]) ).
cnf(s287,plain,
( spl36_511
| spl36_531
| spl36_542
| spl36_543 ),
inference(sat_conversion,[],[f3032]) ).
cnf(s298,plain,
( spl36_489
| spl36_496
| spl36_503
| spl36_510 ),
inference(sat_conversion,[],[f3063]) ).
cnf(s300,plain,
( spl36_491
| spl36_498
| spl36_505
| spl36_512 ),
inference(sat_conversion,[],[f3065]) ).
cnf(s303,plain,
( spl36_516
| spl36_521
| spl36_526
| spl36_531 ),
inference(sat_conversion,[],[f3068]) ).
cnf(s304,plain,
( spl36_517
| spl36_522
| spl36_527
| spl36_532 ),
inference(sat_conversion,[],[f3069]) ).
cnf(s305,plain,
( spl36_487
| spl36_494
| spl36_501
| spl36_508 ),
inference(sat_conversion,[],[f3070]) ).
cnf(s306,plain,
( spl36_514
| spl36_519
| spl36_524
| spl36_529 ),
inference(sat_conversion,[],[f3071]) ).
cnf(s308,plain,
( spl36_535
| spl36_538
| spl36_541
| spl36_544 ),
inference(sat_conversion,[],[f3073]) ).
cnf(s310,plain,
( spl36_515
| spl36_520
| spl36_525
| spl36_530 ),
inference(sat_conversion,[],[f3075]) ).
cnf(s311,plain,
( spl36_534
| spl36_537
| spl36_540
| spl36_543 ),
inference(sat_conversion,[],[f3076]) ).
cnf(s313,plain,
spl36_485,
inference(sat_conversion,[],[f3081]) ).
cnf(s314,plain,
spl36_518,
inference(sat_conversion,[],[f3083]) ).
cnf(s315,plain,
spl36_539,
inference(sat_conversion,[],[f3084]) ).
cnf(s316,plain,
spl36_548,
inference(sat_conversion,[],[f3087]) ).
cnf(s317,plain,
spl36_421,
inference(sat_conversion,[],[f3088]) ).
cnf(s318,plain,
spl36_454,
inference(sat_conversion,[],[f3089]) ).
cnf(s319,plain,
spl36_475,
inference(sat_conversion,[],[f3091]) ).
cnf(s320,plain,
spl36_484,
inference(sat_conversion,[],[f3092]) ).
cnf(s321,plain,
spl36_507,
inference(sat_conversion,[],[f3093]) ).
cnf(s322,plain,
spl36_443,
inference(sat_conversion,[],[f3095]) ).
cnf(s325,plain,
( ~ spl36_431
| ~ spl36_438 ),
inference(sat_conversion,[],[f3110]) ).
cnf(s330,plain,
( ~ spl36_436
| ~ spl36_443 ),
inference(sat_conversion,[],[f3134]) ).
cnf(s356,plain,
( ~ spl36_454
| ~ spl36_459 ),
inference(sat_conversion,[],[f3245]) ).
cnf(s361,plain,
( ~ spl36_458
| ~ spl36_463 ),
inference(sat_conversion,[],[f3274]) ).
cnf(s373,plain,
( ~ spl36_475
| ~ spl36_478 ),
inference(sat_conversion,[],[f3334]) ).
cnf(s376,plain,
( ~ spl36_482
| ~ spl36_484 ),
inference(sat_conversion,[],[f3347]) ).
cnf(s381,plain,
( spl36_258
| ~ spl36_417
| ~ spl36_475
| ~ spl36_485 ),
inference(sat_conversion,[],[f3385]) ).
cnf(s443,plain,
( ~ spl36_539
| ~ spl36_542 ),
inference(sat_conversion,[],[f3736]) ).
cnf(s447,plain,
( spl36_416
| ~ spl36_473 ),
inference(sat_conversion,[],[f3751]) ).
cnf(s461,plain,
( spl36_411
| ~ spl36_452
| ~ spl36_473 ),
inference(sat_conversion,[],[f3969]) ).
cnf(s476,plain,
( ~ spl36_454
| ~ spl36_455 ),
inference(sat_conversion,[],[f4042]) ).
cnf(s480,plain,
( ~ spl36_460
| ~ spl36_475 ),
inference(sat_conversion,[],[f4048]) ).
cnf(s482,plain,
( ~ spl36_450
| ~ spl36_451 ),
inference(sat_conversion,[],[f4050]) ).
cnf(s485,plain,
( ~ spl36_430
| ~ spl36_474 ),
inference(sat_conversion,[],[f4060]) ).
cnf(s486,plain,
( ~ spl36_475
| ~ spl36_477 ),
inference(sat_conversion,[],[f4061]) ).
cnf(s490,plain,
( ~ spl36_480
| ~ spl36_484 ),
inference(sat_conversion,[],[f4068]) ).
cnf(s500,plain,
( ~ spl36_502
| ~ spl36_540 ),
inference(sat_conversion,[],[f4116]) ).
cnf(s503,plain,
( ~ spl36_515
| ~ spl36_534 ),
inference(sat_conversion,[],[f4120]) ).
cnf(s504,plain,
( ~ spl36_507
| ~ spl36_532 ),
inference(sat_conversion,[],[f4121]) ).
cnf(s505,plain,
( ~ spl36_518
| ~ spl36_522 ),
inference(sat_conversion,[],[f4122]) ).
cnf(s507,plain,
( ~ spl36_507
| ~ spl36_531 ),
inference(sat_conversion,[],[f4126]) ).
cnf(s508,plain,
( ~ spl36_518
| ~ spl36_521 ),
inference(sat_conversion,[],[f4127]) ).
cnf(s512,plain,
( ~ spl36_543
| ~ spl36_548 ),
inference(sat_conversion,[],[f4135]) ).
cnf(s513,plain,
( ~ spl36_517
| ~ spl36_535 ),
inference(sat_conversion,[],[f4136]) ).
cnf(s515,plain,
( ~ spl36_526
| ~ spl36_539 ),
inference(sat_conversion,[],[f4138]) ).
cnf(s534,plain,
( spl36_272
| ~ spl36_274
| ~ spl36_411
| ~ spl36_416
| ~ spl36_443
| ~ spl36_537 ),
inference(sat_conversion,[],[f4274]) ).
cnf(s535,plain,
( spl36_259
| ~ spl36_274
| ~ spl36_411
| ~ spl36_417
| ~ spl36_471
| ~ spl36_503 ),
inference(sat_conversion,[],[f4283]) ).
cnf(s537,plain,
( spl36_261
| ~ spl36_274
| ~ spl36_416
| ~ spl36_417
| ~ spl36_465
| ~ spl36_498 ),
inference(sat_conversion,[],[f4293]) ).
cnf(s538,plain,
( spl36_260
| ~ spl36_411
| ~ spl36_416
| ~ spl36_417
| ~ spl36_430
| ~ spl36_511 ),
inference(sat_conversion,[],[f4303]) ).
cnf(s540,plain,
( spl36_263
| ~ spl36_274
| ~ spl36_484
| ~ spl36_518 ),
inference(sat_conversion,[],[f4313]) ).
cnf(s541,plain,
( spl36_262
| ~ spl36_274
| ~ spl36_416
| ~ spl36_417
| ~ spl36_473
| ~ spl36_507 ),
inference(sat_conversion,[],[f4322]) ).
cnf(s549,plain,
( spl36_273
| ~ spl36_416
| ~ spl36_454
| ~ spl36_548 ),
inference(sat_conversion,[],[f4410]) ).
cnf(s555,plain,
( ~ spl36_518
| ~ spl36_519 ),
inference(sat_conversion,[],[f4431]) ).
cnf(s556,plain,
( ~ spl36_502
| ~ spl36_525 ),
inference(sat_conversion,[],[f4433]) ).
cnf(s558,plain,
( ~ spl36_518
| ~ spl36_520 ),
inference(sat_conversion,[],[f4436]) ).
cnf(s560,plain,
( ~ spl36_524
| ~ spl36_539 ),
inference(sat_conversion,[],[f4448]) ).
cnf(s561,plain,
( ~ spl36_514
| ~ spl36_535 ),
inference(sat_conversion,[],[f4449]) ).
cnf(s562,plain,
( ~ spl36_530
| ~ spl36_548 ),
inference(sat_conversion,[],[f4450]) ).
cnf(s564,plain,
( spl36_264
| ~ spl36_274
| ~ spl36_411
| ~ spl36_417
| ~ spl36_438
| ~ spl36_516 ),
inference(sat_conversion,[],[f4466]) ).
cnf(s569,plain,
( spl36_266
| ~ spl36_274
| ~ spl36_411
| ~ spl36_417
| ~ spl36_447
| ~ spl36_494 ),
inference(sat_conversion,[],[f4500]) ).
cnf(s575,plain,
( spl36_267
| ~ spl36_274
| ~ spl36_411
| ~ spl36_416
| ~ spl36_434
| ~ spl36_529 ),
inference(sat_conversion,[],[f4568]) ).
cnf(s579,plain,
( spl36_268
| ~ spl36_411
| ~ spl36_421
| ~ spl36_539 ),
inference(sat_conversion,[],[f4613]) ).
cnf(s585,plain,
( spl36_269
| ~ spl36_411
| ~ spl36_416
| ~ spl36_417
| ~ spl36_439
| ~ spl36_535 ),
inference(sat_conversion,[],[f4654]) ).
cnf(s586,plain,
( ~ spl36_494
| ~ spl36_538 ),
inference(sat_conversion,[],[f4659]) ).
cnf(s587,plain,
( ~ spl36_539
| ~ spl36_541 ),
inference(sat_conversion,[],[f4660]) ).
cnf(s591,plain,
( ~ spl36_544
| ~ spl36_548 ),
inference(sat_conversion,[],[f4674]) ).
cnf(s595,plain,
( spl36_271
| ~ spl36_274
| ~ spl36_416
| ~ spl36_417
| ~ spl36_463
| ~ spl36_515 ),
inference(sat_conversion,[],[f4706]) ).
cnf(s606,plain,
( spl36_438
| ~ spl36_443 ),
inference(sat_conversion,[],[f4729]) ).
cnf(s613,plain,
( ~ spl36_421
| ~ spl36_423 ),
inference(sat_conversion,[],[f4746]) ).
cnf(s614,plain,
( ~ spl36_443
| ~ spl36_444 ),
inference(sat_conversion,[],[f4747]) ).
cnf(s617,plain,
( ~ spl36_479
| ~ spl36_484 ),
inference(sat_conversion,[],[f4758]) ).
cnf(s630,plain,
( ~ spl36_437
| ~ spl36_475 ),
inference(sat_conversion,[],[f4771]) ).
cnf(s637,plain,
( ~ spl36_438
| ~ spl36_461 ),
inference(sat_conversion,[],[f4803]) ).
cnf(s643,plain,
( ~ spl36_454
| ~ spl36_456 ),
inference(sat_conversion,[],[f4815]) ).
cnf(s652,plain,
( ~ spl36_466
| ~ spl36_484 ),
inference(sat_conversion,[],[f4836]) ).
cnf(s654,plain,
( spl36_265
| ~ spl36_274
| ~ spl36_411
| ~ spl36_416
| ~ spl36_451
| ~ spl36_527 ),
inference(sat_conversion,[],[f4840]) ).
cnf(s659,plain,
( ~ spl36_485
| ~ spl36_489 ),
inference(sat_conversion,[],[f4863]) ).
cnf(s662,plain,
( spl36_502
| ~ spl36_507 ),
inference(sat_conversion,[],[f4876]) ).
cnf(s663,plain,
( ~ spl36_485
| ~ spl36_491 ),
inference(sat_conversion,[],[f4878]) ).
cnf(s665,plain,
( ~ spl36_485
| ~ spl36_487 ),
inference(sat_conversion,[],[f4888]) ).
cnf(s666,plain,
( ~ spl36_507
| ~ spl36_508 ),
inference(sat_conversion,[],[f4889]) ).
cnf(s670,plain,
( ~ spl36_496
| ~ spl36_518 ),
inference(sat_conversion,[],[f4903]) ).
cnf(s671,plain,
( ~ spl36_510
| ~ spl36_529 ),
inference(sat_conversion,[],[f4904]) ).
cnf(s675,plain,
( ~ spl36_505
| ~ spl36_527 ),
inference(sat_conversion,[],[f4908]) ).
cnf(s676,plain,
( ~ spl36_512
| ~ spl36_548 ),
inference(sat_conversion,[],[f4909]) ).
cnf(s678,plain,
( ~ spl36_501
| ~ spl36_539 ),
inference(sat_conversion,[],[f4911]) ).
cnf(s689,plain,
( spl36_270
| ~ spl36_411
| ~ spl36_416
| ~ spl36_417
| ~ spl36_452
| ~ spl36_502 ),
inference(sat_conversion,[],[f4941]) ).
cnf(s698,plain,
( ~ spl36_443
| ~ spl36_467 ),
inference(sat_conversion,[],[f4973]) ).
cnf(s699,plain,
( ~ spl36_454
| ~ spl36_457 ),
inference(sat_conversion,[],[f4974]) ).
cnf(s720,plain,
( ~ spl36_462
| ~ spl36_475 ),
inference(sat_conversion,[],[f4989]) ).
cnf(s721,plain,
~ spl36_467,
inference(rat,[],[s698,s322]) ).
cnf(s723,plain,
~ spl36_444,
inference(rat,[],[s614,s322]) ).
cnf(s724,plain,
spl36_438,
inference(rat,[],[s606,s322]) ).
cnf(s729,plain,
~ spl36_436,
inference(rat,[],[s330,s322]) ).
cnf(s731,plain,
~ spl36_461,
inference(rat,[],[s637,s724]) ).
cnf(s733,plain,
~ spl36_431,
inference(rat,[],[s325,s724]) ).
cnf(s734,plain,
~ spl36_508,
inference(rat,[],[s666,s321]) ).
cnf(s735,plain,
spl36_502,
inference(rat,[],[s662,s321]) ).
cnf(s737,plain,
~ spl36_531,
inference(rat,[],[s507,s321]) ).
cnf(s738,plain,
~ spl36_532,
inference(rat,[],[s504,s321]) ).
cnf(s741,plain,
~ spl36_525,
inference(rat,[],[s556,s735]) ).
cnf(s742,plain,
~ spl36_540,
inference(rat,[],[s500,s735]) ).
cnf(s745,plain,
~ spl36_466,
inference(rat,[],[s652,s320]) ).
cnf(s747,plain,
~ spl36_479,
inference(rat,[],[s617,s320]) ).
cnf(s748,plain,
~ spl36_480,
inference(rat,[],[s490,s320]) ).
cnf(s749,plain,
~ spl36_482,
inference(rat,[],[s376,s320]) ).
cnf(s750,plain,
~ spl36_462,
inference(rat,[],[s720,s319]) ).
cnf(s751,plain,
~ spl36_437,
inference(rat,[],[s630,s319]) ).
cnf(s752,plain,
~ spl36_477,
inference(rat,[],[s486,s319]) ).
cnf(s753,plain,
~ spl36_460,
inference(rat,[],[s480,s319]) ).
cnf(s754,plain,
~ spl36_478,
inference(rat,[],[s373,s319]) ).
cnf(s756,plain,
~ spl36_457,
inference(rat,[],[s699,s318]) ).
cnf(s757,plain,
~ spl36_456,
inference(rat,[],[s643,s318]) ).
cnf(s758,plain,
~ spl36_455,
inference(rat,[],[s476,s318]) ).
cnf(s759,plain,
~ spl36_459,
inference(rat,[],[s356,s318]) ).
cnf(s761,plain,
~ spl36_423,
inference(rat,[],[s613,s317]) ).
cnf(s768,plain,
~ spl36_512,
inference(rat,[],[s676,s316]) ).
cnf(s769,plain,
~ spl36_544,
inference(rat,[],[s591,s316]) ).
cnf(s770,plain,
~ spl36_530,
inference(rat,[],[s562,s316]) ).
cnf(s771,plain,
~ spl36_543,
inference(rat,[],[s512,s316]) ).
cnf(s773,plain,
~ spl36_501,
inference(rat,[],[s678,s315]) ).
cnf(s774,plain,
~ spl36_541,
inference(rat,[],[s587,s315]) ).
cnf(s775,plain,
~ spl36_524,
inference(rat,[],[s560,s315]) ).
cnf(s776,plain,
~ spl36_526,
inference(rat,[],[s515,s315]) ).
cnf(s777,plain,
~ spl36_542,
inference(rat,[],[s443,s315]) ).
cnf(s779,plain,
~ spl36_496,
inference(rat,[],[s670,s314]) ).
cnf(s780,plain,
~ spl36_520,
inference(rat,[],[s558,s314]) ).
cnf(s781,plain,
~ spl36_519,
inference(rat,[],[s555,s314]) ).
cnf(s782,plain,
~ spl36_521,
inference(rat,[],[s508,s314]) ).
cnf(s783,plain,
~ spl36_522,
inference(rat,[],[s505,s314]) ).
cnf(s787,plain,
~ spl36_487,
inference(rat,[],[s665,s313]) ).
cnf(s788,plain,
~ spl36_491,
inference(rat,[],[s663,s313]) ).
cnf(s790,plain,
~ spl36_489,
inference(rat,[],[s659,s313]) ).
cnf(s793,plain,
( spl36_534
| spl36_537 ),
inference(rat,[],[s311,s771,s742]) ).
cnf(s794,plain,
spl36_515,
inference(rat,[],[s310,s770,s741,s780]) ).
cnf(s795,plain,
~ spl36_534,
inference(rat,[],[s503,s794]) ).
cnf(s796,plain,
spl36_537,
inference(rat,[],[s793,s795]) ).
cnf(s797,plain,
( spl36_535
| spl36_538 ),
inference(rat,[],[s308,s769,s774]) ).
cnf(s798,plain,
( spl36_514
| spl36_529 ),
inference(rat,[],[s306,s775,s781]) ).
cnf(s799,plain,
spl36_494,
inference(rat,[],[s305,s734,s773,s787]) ).
cnf(s800,plain,
~ spl36_538,
inference(rat,[],[s586,s799]) ).
cnf(s801,plain,
spl36_535,
inference(rat,[],[s797,s800]) ).
cnf(s802,plain,
~ spl36_514,
inference(rat,[],[s561,s801]) ).
cnf(s803,plain,
~ spl36_517,
inference(rat,[],[s513,s801]) ).
cnf(s804,plain,
spl36_529,
inference(rat,[],[s798,s802]) ).
cnf(s805,plain,
~ spl36_510,
inference(rat,[],[s671,s804]) ).
cnf(s806,plain,
spl36_527,
inference(rat,[],[s304,s738,s783,s803]) ).
cnf(s807,plain,
~ spl36_505,
inference(rat,[],[s675,s806]) ).
cnf(s808,plain,
spl36_516,
inference(rat,[],[s303,s737,s776,s782]) ).
cnf(s809,plain,
spl36_498,
inference(rat,[],[s300,s768,s807,s788]) ).
cnf(s810,plain,
spl36_503,
inference(rat,[],[s298,s805,s779,s790]) ).
cnf(s811,plain,
spl36_511,
inference(rat,[],[s287,s771,s777,s737]) ).
cnf(s815,plain,
spl36_451,
inference(rat,[],[s262,s745,s731,s757]) ).
cnf(s816,plain,
~ spl36_450,
inference(rat,[],[s482,s815]) ).
cnf(s818,plain,
( spl36_471
| spl36_474 ),
inference(rat,[],[s260,s748,s752]) ).
cnf(s819,plain,
spl36_465,
inference(rat,[],[s258,s753,s758,s816]) ).
cnf(s823,plain,
spl36_430,
inference(rat,[],[s257,s723,s751,s761]) ).
cnf(s824,plain,
~ spl36_474,
inference(rat,[],[s485,s823]) ).
cnf(s827,plain,
spl36_471,
inference(rat,[],[s818,s824]) ).
cnf(s832,plain,
spl36_452,
inference(rat,[],[s255,s721,s750,s756]) ).
cnf(s837,plain,
spl36_473,
inference(rat,[],[s244,s749,s757,s733]) ).
cnf(s838,plain,
spl36_416,
inference(rat,[],[s447,s837]) ).
cnf(s840,plain,
spl36_411,
inference(rat,[],[s461,s832,s837]) ).
cnf(s841,plain,
spl36_273,
inference(rat,[],[s549,s316,s318,s838]) ).
cnf(s842,plain,
spl36_268,
inference(rat,[],[s579,s315,s317,s840]) ).
cnf(s843,plain,
( spl36_434
| spl36_458 ),
inference(rat,[],[s243,s749,s824]) ).
cnf(s844,plain,
spl36_447,
inference(rat,[],[s239,s747,s754,s721]) ).
cnf(s847,plain,
spl36_463,
inference(rat,[],[s230,s750,s759,s729]) ).
cnf(s849,plain,
~ spl36_458,
inference(rat,[],[s361,s847]) ).
cnf(s850,plain,
spl36_434,
inference(rat,[],[s843,s849]) ).
cnf(s855,plain,
spl36_439,
inference(rat,[],[s229,s731,s753,s759]) ).
cnf(s861,plain,
spl36_265,
inference(rat,[],[s654,s806,s815,s838,s840,s216]) ).
cnf(s862,plain,
spl36_267,
inference(rat,[],[s575,s804,s850,s838,s840,s216]) ).
cnf(s863,plain,
spl36_263,
inference(rat,[],[s540,s314,s320,s216]) ).
cnf(s864,plain,
spl36_272,
inference(rat,[],[s534,s796,s322,s838,s840,s216]) ).
cnf(s865,plain,
spl36_258,
inference(rat,[],[s381,s313,s319,s215]) ).
cnf(s866,plain,
spl36_270,
inference(rat,[],[s689,s735,s832,s840,s838,s215]) ).
cnf(s867,plain,
spl36_269,
inference(rat,[],[s585,s801,s855,s840,s838,s215]) ).
cnf(s868,plain,
spl36_260,
inference(rat,[],[s538,s811,s823,s840,s838,s215]) ).
cnf(s869,plain,
spl36_271,
inference(rat,[],[s595,s794,s847,s216,s838,s215]) ).
cnf(s870,plain,
spl36_266,
inference(rat,[],[s569,s799,s844,s216,s840,s215]) ).
cnf(s871,plain,
spl36_264,
inference(rat,[],[s564,s808,s724,s216,s840,s215]) ).
cnf(s872,plain,
spl36_262,
inference(rat,[],[s541,s321,s837,s216,s838,s215]) ).
cnf(s873,plain,
spl36_261,
inference(rat,[],[s537,s809,s819,s216,s838,s215]) ).
cnf(s874,plain,
spl36_259,
inference(rat,[],[s535,s810,s827,s216,s840,s215]) ).
cnf(s928,plain,
~ spl36_256,
inference(rat,[],[s189,s215]) ).
cnf(s929,plain,
~ spl36_255,
inference(rat,[],[s188,s838]) ).
cnf(s930,plain,
~ spl36_254,
inference(rat,[],[s183,s840]) ).
cnf(s962,plain,
$false,
inference(rat,[],[s46,s216,s841,s864,s869,s866,s867,s842,s862,s870,s861,s871,s863,s872,s873,s868,s874,s865,s928,s929,s930]) ).
fof(f4990,plain,
$false,
inference(avatar_sat_refutation,[],[s962]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG113+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n002.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 19:32:49 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.74/1.19 % (675102)Detected formulas, will run a generic FOF schedule.
% 3.74/1.19 % (675111)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2050197959:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.74/1.19 % (675111)Instruction limit reached!
% 3.74/1.19 % (675111)------------------------------
% 3.74/1.19 % (675111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.74/1.19 % (675111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.19 % (675111)CaDiCaL version: 2.1.3
% 3.74/1.19 % (675111)Termination reason: Instruction limit
% 3.74/1.19 % (675111)Termination phase: Saturation
% 3.74/1.19 % (675111)Time elapsed: 0.027 s
% 3.74/1.19 % (675111)Peak memory usage: 88 MB
% 3.74/1.19 % (675111)Instructions burned: 123 (million)
% 3.74/1.19 % (675109)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=3916326903:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.74/1.19 % (675108)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=3248077753:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.74/1.19 % (675113)dis-21_1_sil=8000:lcm=predicate:random_seed=214249445: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.74/1.19 % (675107)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=3702605419:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.74/1.19 % (675112)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2516655240:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.74/1.19 % (675110)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3019885568:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.74/1.19 % (675113)Refutation not found, incomplete strategy
% 3.74/1.19 % (675113)------------------------------
% 3.74/1.19 % (675113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.74/1.19 % (675113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.19 % (675113)CaDiCaL version: 2.1.3
% 3.74/1.19 % (675113)Termination reason: Refutation not found, incomplete strategy
% 3.74/1.19 % (675113)Time elapsed: 0.025 s
% 3.74/1.19 % (675113)Peak memory usage: 90 MB
% 3.74/1.19 % (675113)Instructions burned: 52 (million)
% 3.74/1.19 % (675110)Instruction limit reached!
% 3.74/1.19 % (675110)------------------------------
% 3.74/1.19 % (675110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.74/1.19 % (675110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.19 % (675110)CaDiCaL version: 2.1.3
% 3.74/1.19 % (675110)Termination reason: Instruction limit
% 3.74/1.19 % (675110)Termination phase: Saturation
% 3.74/1.19 % (675110)Time elapsed: 0.050 s
% 3.74/1.19 % (675110)Peak memory usage: 90 MB
% 3.74/1.19 % (675110)Instructions burned: 111 (million)
% 3.74/1.19 % (675112)First to succeed.
% 3.74/1.19 % (675112)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-675102"
% 3.74/1.19 % (675115)lrs+10_1_sil=8000:sp=occurrence:random_seed=762914203:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.74/1.19 % (675115)Also succeeded, but the first one will report.
% 3.74/1.19 % (675122)lrs+10_1_sil=32000:urr=on:br=off:random_seed=971623927:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.74/1.19 % (675113)------------------------------
% 3.74/1.19 % (675113)------------------------------
% 3.74/1.19 % (675122)Instruction limit reached!
% 3.74/1.19 % (675122)------------------------------
% 3.74/1.19 % (675122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.74/1.19 % (675122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.19 % (675122)CaDiCaL version: 2.1.3
% 3.74/1.19 % (675122)Termination reason: Instruction limit
% 3.74/1.19 % (675122)Termination phase: Saturation
% 3.74/1.19 % (675122)Time elapsed: 0.063 s
% 3.74/1.19 % (675122)Peak memory usage: 89 MB
% 3.74/1.19 % (675122)Instructions burned: 158 (million)
% 3.74/1.19 % (675112)Refutation found. Thanks to Tanya!
% 3.74/1.19 % SZS status Theorem for theBenchmark
% 3.74/1.19 % SZS output start Proof for theBenchmark
% See solution above
% 4.31/1.39 % (675112)------------------------------
% 4.31/1.39 % (675112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.39 % (675112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.39 % (675112)CaDiCaL version: 2.1.3
% 4.31/1.39 % (675112)Termination reason: Refutation
% 4.31/1.39 % (675112)Time elapsed: 0.086 s
% 4.31/1.39 % (675112)Peak memory usage: 92 MB
% 4.31/1.39 % (675112)Instructions burned: 178 (million)
% 4.31/1.39 % (675112)------------------------------
% 4.31/1.39 % (675112)------------------------------
% 4.31/1.39 % (675102)Success in time 0.54 s
% 4.31/1.39 % Vampire exiting
%------------------------------------------------------------------------------