%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG111+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 : n020.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:10 AM UTC 2026
% Result : Theorem 3.23s 1.15s
% Output : Refutation 3.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 138
% Syntax : Number of formulae : 801 ( 170 unt; 124 def)
% Number of atoms : 3284 (1784 equ)
% Maximal formula atoms : 128 ( 4 avg)
% Number of connectives : 4196 (1713 ~;1779 |; 592 &)
% ( 112 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 66 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 126 ( 124 usr; 125 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e10) = e11
| op1(e10,e10) = e12
| op1(e10,e10) = e13 )
& ( op1(e10,e11) = e10
| op1(e10,e11) = e11
| op1(e10,e11) = e12
| op1(e10,e11) = e13 )
& ( op1(e10,e12) = e10
| op1(e10,e12) = e11
| op1(e10,e12) = e12
| op1(e10,e12) = e13 )
& ( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e12
| op1(e10,e13) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 )
& ( op1(e11,e11) = e10
| op1(e11,e11) = e11
| op1(e11,e11) = e12
| op1(e11,e11) = e13 )
& ( op1(e11,e12) = e10
| op1(e11,e12) = e11
| op1(e11,e12) = e12
| op1(e11,e12) = e13 )
& ( op1(e11,e13) = e10
| op1(e11,e13) = e11
| op1(e11,e13) = e12
| op1(e11,e13) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e10) = e11
| op1(e12,e10) = e12
| op1(e12,e10) = e13 )
& ( op1(e12,e11) = e10
| op1(e12,e11) = e11
| op1(e12,e11) = e12
| op1(e12,e11) = e13 )
& ( op1(e12,e12) = e10
| op1(e12,e12) = e11
| op1(e12,e12) = e12
| op1(e12,e12) = e13 )
& ( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12
| op1(e12,e13) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e10) = e11
| op1(e13,e10) = e12
| op1(e13,e10) = e13 )
& ( op1(e13,e11) = e10
| op1(e13,e11) = e11
| op1(e13,e11) = e12
| op1(e13,e11) = e13 )
& ( op1(e13,e12) = e10
| op1(e13,e12) = e11
| op1(e13,e12) = e12
| op1(e13,e12) = e13 )
& ( op1(e13,e13) = e10
| op1(e13,e13) = e11
| op1(e13,e13) = e12
| op1(e13,e13) = e13 ) ),
file('/export/starexec/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(e10,e10) != e10 )
& ( op1(e10,e10) != e10
| op1(e11,e11) != e10 )
& ( op1(e10,e10) != e10
| op1(e12,e12) != e10 )
& ( op1(e10,e10) != e10
| op1(e13,e13) != e10 )
& ( op1(e10,e11) != e10
| op1(e10,e10) != e11 )
& ( op1(e10,e11) != e10
| op1(e11,e11) != e11 )
& ( op1(e10,e11) != e10
| op1(e12,e12) != e11 )
& ( op1(e10,e11) != e10
| op1(e13,e13) != e11 )
& ( op1(e10,e12) != e10
| op1(e10,e10) != e12 )
& ( op1(e10,e12) != e10
| op1(e11,e11) != e12 )
& ( op1(e10,e12) != e10
| op1(e12,e12) != e12 )
& ( op1(e10,e12) != e10
| op1(e13,e13) != e12 )
& ( op1(e10,e13) != e10
| op1(e10,e10) != e13 )
& ( op1(e10,e13) != e10
| op1(e11,e11) != e13 )
& ( op1(e10,e13) != e10
| op1(e12,e12) != e13 )
& ( op1(e10,e13) != e10
| op1(e13,e13) != e13 )
& ( op1(e11,e10) != e11
| op1(e10,e10) != e10 )
& ( op1(e11,e10) != e11
| op1(e11,e11) != e10 )
& ( op1(e11,e10) != e11
| op1(e12,e12) != e10 )
& ( op1(e11,e10) != e11
| op1(e13,e13) != e10 )
& ( op1(e11,e11) != e11
| op1(e10,e10) != e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) != e11 )
& ( op1(e11,e11) != e11
| op1(e12,e12) != e11 )
& ( op1(e11,e11) != e11
| op1(e13,e13) != e11 )
& ( op1(e11,e12) != e11
| op1(e10,e10) != e12 )
& ( op1(e11,e12) != e11
| op1(e11,e11) != e12 )
& ( op1(e11,e12) != e11
| op1(e12,e12) != e12 )
& ( op1(e11,e12) != e11
| op1(e13,e13) != e12 )
& ( op1(e11,e13) != e11
| op1(e10,e10) != e13 )
& ( op1(e11,e13) != e11
| op1(e11,e11) != e13 )
& ( op1(e11,e13) != e11
| op1(e12,e12) != e13 )
& ( op1(e11,e13) != e11
| op1(e13,e13) != e13 )
& ( op1(e12,e10) != e12
| op1(e10,e10) != e10 )
& ( op1(e12,e10) != e12
| op1(e11,e11) != e10 )
& ( op1(e12,e10) != e12
| op1(e12,e12) != e10 )
& ( op1(e12,e10) != e12
| op1(e13,e13) != e10 )
& ( op1(e12,e11) != e12
| op1(e10,e10) != e11 )
& ( op1(e12,e11) != e12
| op1(e11,e11) != e11 )
& ( op1(e12,e11) != e12
| op1(e12,e12) != e11 )
& ( op1(e12,e11) != e12
| op1(e13,e13) != e11 )
& ( op1(e12,e12) != e12
| op1(e10,e10) != e12 )
& ( op1(e12,e12) != e12
| op1(e11,e11) != e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) != e12 )
& ( op1(e12,e12) != e12
| op1(e13,e13) != e12 )
& ( op1(e12,e13) != e12
| op1(e10,e10) != e13 )
& ( op1(e12,e13) != e12
| op1(e11,e11) != e13 )
& ( op1(e12,e13) != e12
| op1(e12,e12) != e13 )
& ( op1(e12,e13) != e12
| op1(e13,e13) != e13 )
& ( op1(e13,e10) != e13
| op1(e10,e10) != e10 )
& ( op1(e13,e10) != e13
| op1(e11,e11) != e10 )
& ( op1(e13,e10) != e13
| op1(e12,e12) != e10 )
& ( op1(e13,e10) != e13
| op1(e13,e13) != e10 )
& ( op1(e13,e11) != e13
| op1(e10,e10) != e11 )
& ( op1(e13,e11) != e13
| op1(e11,e11) != e11 )
& ( op1(e13,e11) != e13
| op1(e12,e12) != e11 )
& ( op1(e13,e11) != e13
| op1(e13,e13) != e11 )
& ( op1(e13,e12) != e13
| op1(e10,e10) != e12 )
& ( op1(e13,e12) != e13
| op1(e11,e11) != e12 )
& ( op1(e13,e12) != e13
| op1(e12,e12) != e12 )
& ( op1(e13,e12) != e13
| op1(e13,e13) != e12 )
& ( op1(e13,e13) != e13
| op1(e10,e10) != e13 )
& ( op1(e13,e13) != e13
| op1(e11,e11) != e13 )
& ( op1(e13,e13) != e13
| op1(e12,e12) != e13 )
& ( op1(e13,e13) != e13
| op1(e13,e13) != e13 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( ( op2(e20,e20) != e20
| op2(e20,e20) != e20 )
& ( op2(e20,e20) != e20
| op2(e21,e21) != e20 )
& ( op2(e20,e20) != e20
| op2(e22,e22) != e20 )
& ( op2(e20,e20) != e20
| op2(e23,e23) != e20 )
& ( op2(e20,e21) != e20
| op2(e20,e20) != e21 )
& ( op2(e20,e21) != e20
| op2(e21,e21) != e21 )
& ( op2(e20,e21) != e20
| op2(e22,e22) != e21 )
& ( op2(e20,e21) != e20
| op2(e23,e23) != e21 )
& ( op2(e20,e22) != e20
| op2(e20,e20) != e22 )
& ( op2(e20,e22) != e20
| op2(e21,e21) != e22 )
& ( op2(e20,e22) != e20
| op2(e22,e22) != e22 )
& ( op2(e20,e22) != e20
| op2(e23,e23) != e22 )
& ( op2(e20,e23) != e20
| op2(e20,e20) != e23 )
& ( op2(e20,e23) != e20
| op2(e21,e21) != e23 )
& ( op2(e20,e23) != e20
| op2(e22,e22) != e23 )
& ( op2(e20,e23) != e20
| op2(e23,e23) != e23 )
& ( op2(e21,e20) != e21
| op2(e20,e20) != e20 )
& ( op2(e21,e20) != e21
| op2(e21,e21) != e20 )
& ( op2(e21,e20) != e21
| op2(e22,e22) != e20 )
& ( op2(e21,e20) != e21
| op2(e23,e23) != e20 )
& ( op2(e21,e21) != e21
| op2(e20,e20) != e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) != e21 )
& ( op2(e21,e21) != e21
| op2(e22,e22) != e21 )
& ( op2(e21,e21) != e21
| op2(e23,e23) != e21 )
& ( op2(e21,e22) != e21
| op2(e20,e20) != e22 )
& ( op2(e21,e22) != e21
| op2(e21,e21) != e22 )
& ( op2(e21,e22) != e21
| op2(e22,e22) != e22 )
& ( op2(e21,e22) != e21
| op2(e23,e23) != e22 )
& ( op2(e21,e23) != e21
| op2(e20,e20) != e23 )
& ( op2(e21,e23) != e21
| op2(e21,e21) != e23 )
& ( op2(e21,e23) != e21
| op2(e22,e22) != e23 )
& ( op2(e21,e23) != e21
| op2(e23,e23) != e23 )
& ( op2(e22,e20) != e22
| op2(e20,e20) != e20 )
& ( op2(e22,e20) != e22
| op2(e21,e21) != e20 )
& ( op2(e22,e20) != e22
| op2(e22,e22) != e20 )
& ( op2(e22,e20) != e22
| op2(e23,e23) != e20 )
& ( op2(e22,e21) != e22
| op2(e20,e20) != e21 )
& ( op2(e22,e21) != e22
| op2(e21,e21) != e21 )
& ( op2(e22,e21) != e22
| op2(e22,e22) != e21 )
& ( op2(e22,e21) != e22
| op2(e23,e23) != e21 )
& ( op2(e22,e22) != e22
| op2(e20,e20) != e22 )
& ( op2(e22,e22) != e22
| op2(e21,e21) != e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) != e22 )
& ( op2(e22,e22) != e22
| op2(e23,e23) != e22 )
& ( op2(e22,e23) != e22
| op2(e20,e20) != e23 )
& ( op2(e22,e23) != e22
| op2(e21,e21) != e23 )
& ( op2(e22,e23) != e22
| op2(e22,e22) != e23 )
& ( op2(e22,e23) != e22
| op2(e23,e23) != e23 )
& ( op2(e23,e20) != e23
| op2(e20,e20) != e20 )
& ( op2(e23,e20) != e23
| op2(e21,e21) != e20 )
& ( op2(e23,e20) != e23
| op2(e22,e22) != e20 )
& ( op2(e23,e20) != e23
| op2(e23,e23) != e20 )
& ( op2(e23,e21) != e23
| op2(e20,e20) != e21 )
& ( op2(e23,e21) != e23
| op2(e21,e21) != e21 )
& ( op2(e23,e21) != e23
| op2(e22,e22) != e21 )
& ( op2(e23,e21) != e23
| op2(e23,e23) != e21 )
& ( op2(e23,e22) != e23
| op2(e20,e20) != e22 )
& ( op2(e23,e22) != e23
| op2(e21,e21) != e22 )
& ( op2(e23,e22) != e23
| op2(e22,e22) != e22 )
& ( op2(e23,e22) != e23
| op2(e23,e23) != e22 )
& ( op2(e23,e23) != e23
| op2(e20,e20) != e23 )
& ( op2(e23,e23) != e23
| op2(e21,e21) != e23 )
& ( op2(e23,e23) != e23
| op2(e22,e22) != e23 )
& ( op2(e23,e23) != e23
| op2(e23,e23) != e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e10 = op1(e13,op1(e13,e13))
& e11 = op1(e13,e13)
& e12 = op1(op1(e13,op1(e13,e13)),op1(e13,e13)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e20 = op2(e23,op2(e23,e23))
& e21 = op2(e23,e23)
& e22 = op2(op2(e23,op2(e23,e23)),op2(e23,e23)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f15,axiom,
( h2(e13) = e21
& h2(e10) = op2(e21,op2(e21,e21))
& h2(e11) = op2(e21,e21)
& h2(e12) = op2(op2(e21,op2(e21,e21)),op2(e21,e21)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
fof(f18,conjecture,
( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f19,negated_conjecture,
~ ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f20,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) ) )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) ) )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) ) )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) ) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f21,definition,
( ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f22,definition,
( ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f25,definition,
( ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f26,definition,
( ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f27,definition,
( ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f29,definition,
( ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f30,definition,
( ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f31,definition,
( ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f32,definition,
( ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f33,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) )
| sP11
| sP10
| sP9 )
& ( 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) )
| sP8
| sP7
| sP6 )
& ( 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) )
| sP5
| sP4
| sP3 )
& ( 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) )
| sP2
| sP1
| sP0 ) ),
inference(definition_folding,[],[f20,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21]) ).
fof(f37,plain,
( ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ~ sP8 ),
inference(nnf_transformation,[],[f29]) ).
fof(f38,plain,
( ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ~ sP7 ),
inference(nnf_transformation,[],[f28]) ).
fof(f39,plain,
( ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) )
| ~ sP6 ),
inference(nnf_transformation,[],[f27]) ).
fof(f49,plain,
( e10 = op1(e13,e10)
| e11 = op1(e13,e10)
| e12 = op1(e13,e10)
| e13 = op1(e13,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f51,plain,
( e10 = op1(e12,e12)
| e11 = op1(e12,e12)
| e12 = op1(e12,e12)
| e13 = op1(e12,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f64,plain,
( e12 = op1(e10,e13)
| e12 = op1(e11,e13)
| e12 = op1(e12,e13)
| e12 = op1(e13,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f72,plain,
( e12 = op1(e10,e12)
| e12 = op1(e11,e12)
| e12 = op1(e12,e12)
| e12 = op1(e13,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f73,plain,
( e12 = op1(e12,e10)
| e12 = op1(e12,e11)
| e12 = op1(e12,e12)
| e12 = op1(e12,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f74,plain,
( e11 = op1(e10,e12)
| e11 = op1(e11,e12)
| e11 = op1(e12,e12)
| e11 = op1(e13,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f77,plain,
( e10 = op1(e12,e10)
| e10 = op1(e12,e11)
| e10 = op1(e12,e12)
| e10 = op1(e12,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f78,plain,
( e13 = op1(e10,e11)
| e13 = op1(e11,e11)
| e13 = op1(e12,e11)
| e13 = op1(e13,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f82,plain,
( e11 = op1(e10,e11)
| e11 = op1(e11,e11)
| e11 = op1(e12,e11)
| e11 = op1(e13,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f87,plain,
( op1(e10,e10) = e13
| e13 = op1(e10,e11)
| e13 = op1(e10,e12)
| e13 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f91,plain,
( op1(e10,e10) = e11
| e11 = op1(e10,e11)
| e11 = op1(e10,e12)
| e11 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f92,plain,
( e10 = op1(e10,e10)
| e10 = op1(e11,e10)
| e10 = op1(e12,e10)
| e10 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
( e10 = op1(e10,e10)
| e10 = op1(e10,e11)
| e10 = op1(e10,e12)
| e10 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f99,plain,
( e20 = op2(e22,e22)
| e21 = op2(e22,e22)
| e22 = op2(e22,e22)
| e23 = op2(e22,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f105,plain,
( e20 = op2(e21,e20)
| e21 = op2(e21,e20)
| e22 = op2(e21,e20)
| e23 = op2(e21,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f111,plain,
( e23 = op2(e23,e20)
| e23 = op2(e23,e21)
| e23 = op2(e23,e22)
| e23 = op2(e23,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f116,plain,
( e20 = op2(e20,e23)
| e20 = op2(e21,e23)
| e20 = op2(e22,e23)
| e20 = op2(e23,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f120,plain,
( e22 = op2(e20,e22)
| e22 = op2(e21,e22)
| e22 = op2(e22,e22)
| e22 = op2(e23,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f121,plain,
( e22 = op2(e22,e20)
| e22 = op2(e22,e21)
| e22 = op2(e22,e22)
| e22 = op2(e22,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f122,plain,
( e21 = op2(e20,e22)
| e21 = op2(e21,e22)
| e21 = op2(e22,e22)
| e21 = op2(e23,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f126,plain,
( e23 = op2(e20,e21)
| e23 = op2(e21,e21)
| e23 = op2(e22,e21)
| e23 = op2(e23,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f129,plain,
( e22 = op2(e21,e20)
| e22 = op2(e21,e21)
| e22 = op2(e21,e22)
| e22 = op2(e21,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f130,plain,
( e21 = op2(e20,e21)
| e21 = op2(e21,e21)
| e21 = op2(e22,e21)
| e21 = op2(e23,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f135,plain,
( op2(e20,e20) = e23
| e23 = op2(e20,e21)
| e23 = op2(e20,e22)
| e23 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f139,plain,
( op2(e20,e20) = e21
| e21 = op2(e20,e21)
| e21 = op2(e20,e22)
| e21 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f141,plain,
( e20 = op2(e20,e20)
| e20 = op2(e20,e21)
| e20 = op2(e20,e22)
| e20 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f142,plain,
op1(e13,e12) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f143,plain,
op1(e13,e11) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f145,plain,
op1(e13,e10) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f146,plain,
op1(e13,e10) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f147,plain,
op1(e13,e10) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f150,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f169,plain,
op1(e10,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f178,plain,
op1(e12,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f187,plain,
op1(e10,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f190,plain,
op2(e23,e22) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f191,plain,
op2(e23,e21) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f198,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f206,plain,
op2(e21,e20) != op2(e21,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f217,plain,
op2(e20,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f224,plain,
op2(e20,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f233,plain,
op2(e21,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f234,plain,
op2(e21,e20) != op2(e22,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f238,plain,
e12 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f239,plain,
e11 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f240,plain,
e11 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f241,plain,
e10 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f242,plain,
e10 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f243,plain,
e10 != e11,
inference(cnf_transformation,[],[f7]) ).
fof(f244,plain,
e22 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f245,plain,
e21 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f246,plain,
e21 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f247,plain,
e20 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f248,plain,
e20 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f249,plain,
e20 != e21,
inference(cnf_transformation,[],[f8]) ).
fof(f274,plain,
( e13 != op1(e13,e11)
| e11 != op1(e13,e13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f284,plain,
( e12 != op1(e12,e13)
| e13 != op1(e11,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f287,plain,
( e12 != op1(e12,e12)
| e12 != op1(e12,e12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f290,plain,
( e12 != op1(e12,e11)
| e11 != op1(e13,e13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f295,plain,
( e12 != op1(e12,e10)
| e10 != op1(e12,e12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f308,plain,
( e11 != op1(e11,e11)
| e11 != op1(e11,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f316,plain,
( e10 != op1(e10,e13)
| e13 != op1(e11,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f318,plain,
( e10 != op1(e10,e12)
| e12 != op1(e13,e13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f322,plain,
( e10 != op1(e10,e11)
| e11 != op1(e13,e13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f329,plain,
( e10 != op1(e10,e10)
| e10 != op1(e10,e10) ),
inference(cnf_transformation,[],[f10]) ).
fof(f330,plain,
( e23 != op2(e23,e23)
| e23 != op2(e23,e23) ),
inference(cnf_transformation,[],[f11]) ).
fof(f338,plain,
( e23 != op2(e23,e21)
| e21 != op2(e23,e23) ),
inference(cnf_transformation,[],[f11]) ).
fof(f348,plain,
( e22 != op2(e22,e23)
| e23 != op2(e21,e21) ),
inference(cnf_transformation,[],[f11]) ).
fof(f351,plain,
( e22 != op2(e22,e22)
| e22 != op2(e22,e22) ),
inference(cnf_transformation,[],[f11]) ).
fof(f354,plain,
( e22 != op2(e22,e21)
| e21 != op2(e23,e23) ),
inference(cnf_transformation,[],[f11]) ).
fof(f372,plain,
( e21 != op2(e21,e21)
| e21 != op2(e21,e21) ),
inference(cnf_transformation,[],[f11]) ).
fof(f380,plain,
( e20 != op2(e20,e23)
| e23 != op2(e21,e21) ),
inference(cnf_transformation,[],[f11]) ).
fof(f384,plain,
( e20 != op2(e20,e22)
| e22 != op2(e21,e21) ),
inference(cnf_transformation,[],[f11]) ).
fof(f386,plain,
( e20 != op2(e20,e21)
| e21 != op2(e23,e23) ),
inference(cnf_transformation,[],[f11]) ).
fof(f393,plain,
( e20 != op2(e20,e20)
| e20 != op2(e20,e20) ),
inference(cnf_transformation,[],[f11]) ).
fof(f394,plain,
e12 = op1(op1(e13,op1(e13,e13)),op1(e13,e13)),
inference(cnf_transformation,[],[f12]) ).
fof(f395,plain,
e11 = op1(e13,e13),
inference(cnf_transformation,[],[f12]) ).
fof(f396,plain,
e10 = op1(e13,op1(e13,e13)),
inference(cnf_transformation,[],[f12]) ).
fof(f397,plain,
e22 = op2(op2(e23,op2(e23,e23)),op2(e23,e23)),
inference(cnf_transformation,[],[f13]) ).
fof(f398,plain,
e21 = op2(e23,e23),
inference(cnf_transformation,[],[f13]) ).
fof(f399,plain,
e20 = op2(e23,op2(e23,e23)),
inference(cnf_transformation,[],[f13]) ).
fof(f404,plain,
h2(e12) = op2(op2(e21,op2(e21,e21)),op2(e21,e21)),
inference(cnf_transformation,[],[f15]) ).
fof(f405,plain,
op2(e21,e21) = h2(e11),
inference(cnf_transformation,[],[f15]) ).
fof(f406,plain,
h2(e10) = op2(e21,op2(e21,e21)),
inference(cnf_transformation,[],[f15]) ).
fof(f407,plain,
e21 = h2(e13),
inference(cnf_transformation,[],[f15]) ).
fof(f428,plain,
( e21 != h2(e13)
| ~ sP8 ),
inference(cnf_transformation,[],[f37]) ).
fof(f435,plain,
( e22 != h2(e10)
| ~ sP7 ),
inference(cnf_transformation,[],[f38]) ).
fof(f438,plain,
( e23 != h2(e11)
| ~ sP6 ),
inference(cnf_transformation,[],[f39]) ).
fof(f473,plain,
( 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(e12)
| sP8
| sP7
| sP6 ),
inference(cnf_transformation,[],[f33]) ).
fof(f480,plain,
e23 != op2(e23,e23),
inference(duplicate_literal_removal,[],[f330]) ).
fof(f481,plain,
e22 != op2(e22,e22),
inference(duplicate_literal_removal,[],[f351]) ).
fof(f482,plain,
e21 != op2(e21,e21),
inference(duplicate_literal_removal,[],[f372]) ).
fof(f483,plain,
e20 != op2(e20,e20),
inference(duplicate_literal_removal,[],[f393]) ).
fof(f485,plain,
e12 != op1(e12,e12),
inference(duplicate_literal_removal,[],[f287]) ).
fof(f486,plain,
e11 != op1(e11,e11),
inference(duplicate_literal_removal,[],[f308]) ).
fof(f487,plain,
e10 != op1(e10,e10),
inference(duplicate_literal_removal,[],[f329]) ).
fof(f681,definition,
( spl12_47
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl12_47])],[avatar_definition]) ).
fof(f685,definition,
( spl12_48
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl12_48])],[avatar_definition]) ).
fof(f689,definition,
( spl12_49
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl12_49])],[avatar_definition]) ).
fof(f697,definition,
( spl12_51
<=> h2(op1(e13,e13)) = op2(h2(e13),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_51])],[avatar_definition]) ).
fof(f698,plain,
( h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
| ~ spl12_51 ),
inference(avatar_component_clause,[],[f697]) ).
fof(f699,plain,
( h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| spl12_51 ),
inference(avatar_component_clause,[],[f697]) ).
fof(f701,definition,
( spl12_52
<=> h2(op1(e13,e12)) = op2(h2(e13),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_52])],[avatar_definition]) ).
fof(f703,plain,
( h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| spl12_52 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f705,definition,
( spl12_53
<=> h2(op1(e13,e11)) = op2(h2(e13),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_53])],[avatar_definition]) ).
fof(f707,plain,
( h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| spl12_53 ),
inference(avatar_component_clause,[],[f705]) ).
fof(f709,definition,
( spl12_54
<=> h2(op1(e13,e10)) = op2(h2(e13),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_54])],[avatar_definition]) ).
fof(f711,plain,
( h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| spl12_54 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f713,definition,
( spl12_55
<=> h2(op1(e12,e13)) = op2(h2(e12),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_55])],[avatar_definition]) ).
fof(f715,plain,
( h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| spl12_55 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f717,definition,
( spl12_56
<=> h2(op1(e12,e12)) = op2(h2(e12),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_56])],[avatar_definition]) ).
fof(f719,plain,
( h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| spl12_56 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f721,definition,
( spl12_57
<=> h2(op1(e12,e11)) = op2(h2(e12),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_57])],[avatar_definition]) ).
fof(f723,plain,
( h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| spl12_57 ),
inference(avatar_component_clause,[],[f721]) ).
fof(f725,definition,
( spl12_58
<=> h2(op1(e12,e10)) = op2(h2(e12),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_58])],[avatar_definition]) ).
fof(f727,plain,
( h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| spl12_58 ),
inference(avatar_component_clause,[],[f725]) ).
fof(f729,definition,
( spl12_59
<=> h2(op1(e11,e13)) = op2(h2(e11),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_59])],[avatar_definition]) ).
fof(f731,plain,
( h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| spl12_59 ),
inference(avatar_component_clause,[],[f729]) ).
fof(f733,definition,
( spl12_60
<=> h2(op1(e11,e12)) = op2(h2(e11),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_60])],[avatar_definition]) ).
fof(f735,plain,
( h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| spl12_60 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f737,definition,
( spl12_61
<=> h2(op1(e11,e11)) = op2(h2(e11),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_61])],[avatar_definition]) ).
fof(f739,plain,
( h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| spl12_61 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f741,definition,
( spl12_62
<=> h2(op1(e11,e10)) = op2(h2(e11),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_62])],[avatar_definition]) ).
fof(f743,plain,
( h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| spl12_62 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f745,definition,
( spl12_63
<=> h2(op1(e10,e13)) = op2(h2(e10),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl12_63])],[avatar_definition]) ).
fof(f747,plain,
( h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| spl12_63 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f749,definition,
( spl12_64
<=> h2(op1(e10,e12)) = op2(h2(e10),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl12_64])],[avatar_definition]) ).
fof(f751,plain,
( h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| spl12_64 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f753,definition,
( spl12_65
<=> h2(op1(e10,e11)) = op2(h2(e10),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl12_65])],[avatar_definition]) ).
fof(f755,plain,
( h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| spl12_65 ),
inference(avatar_component_clause,[],[f753]) ).
fof(f757,definition,
( spl12_66
<=> h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl12_66])],[avatar_definition]) ).
fof(f759,plain,
( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| spl12_66 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f762,definition,
( spl12_67
<=> e20 = h2(e12) ),
introduced(definition,[new_symbols(definition,[spl12_67])],[avatar_definition]) ).
fof(f763,plain,
( e20 = h2(e12)
| ~ spl12_67 ),
inference(avatar_component_clause,[],[f762]) ).
fof(f765,plain,
( spl12_47
| spl12_48
| spl12_49
| ~ spl12_67
| ~ spl12_51
| ~ spl12_52
| ~ spl12_53
| ~ spl12_54
| ~ spl12_55
| ~ spl12_56
| ~ spl12_57
| ~ spl12_58
| ~ spl12_59
| ~ spl12_60
| ~ spl12_61
| ~ spl12_62
| ~ spl12_63
| ~ spl12_64
| ~ spl12_65
| ~ spl12_66 ),
inference(avatar_split_clause,[],[f473,f757,f753,f749,f745,f741,f737,f733,f729,f725,f721,f717,f713,f709,f705,f701,f697,f762,f689,f685,f681]) ).
fof(f1003,definition,
( spl12_119
<=> e23 = h2(e11) ),
introduced(definition,[new_symbols(definition,[spl12_119])],[avatar_definition]) ).
fof(f1004,plain,
( e23 = h2(e11)
| ~ spl12_119 ),
inference(avatar_component_clause,[],[f1003]) ).
fof(f1006,plain,
( ~ spl12_47
| ~ spl12_119 ),
inference(avatar_split_clause,[],[f438,f1003,f681]) ).
fof(f1028,definition,
( spl12_124
<=> e22 = h2(e10) ),
introduced(definition,[new_symbols(definition,[spl12_124])],[avatar_definition]) ).
fof(f1029,plain,
( e22 = h2(e10)
| ~ spl12_124 ),
inference(avatar_component_clause,[],[f1028]) ).
fof(f1031,plain,
( ~ spl12_48
| ~ spl12_124 ),
inference(avatar_split_clause,[],[f435,f1028,f685]) ).
fof(f1033,definition,
( spl12_125
<=> e21 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl12_125])],[avatar_definition]) ).
fof(f1034,plain,
( e21 = h2(e13)
| ~ spl12_125 ),
inference(avatar_component_clause,[],[f1033]) ).
fof(f1036,plain,
( ~ spl12_49
| ~ spl12_125 ),
inference(avatar_split_clause,[],[f428,f1033,f689]) ).
fof(f1114,plain,
spl12_125,
inference(avatar_split_clause,[],[f407,f1033]) ).
fof(f1117,definition,
( spl12_141
<=> e23 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_141])],[avatar_definition]) ).
fof(f1121,definition,
( spl12_142
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_142])],[avatar_definition]) ).
fof(f1126,definition,
( spl12_143
<=> e23 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_143])],[avatar_definition]) ).
fof(f1127,plain,
( e23 = op2(e21,e21)
| ~ spl12_143 ),
inference(avatar_component_clause,[],[f1126]) ).
fof(f1131,definition,
( spl12_144
<=> op2(e20,e20) = e23 ),
introduced(definition,[new_symbols(definition,[spl12_144])],[avatar_definition]) ).
fof(f1132,plain,
( op2(e20,e20) = e23
| ~ spl12_144 ),
inference(avatar_component_clause,[],[f1131]) ).
fof(f1140,definition,
( spl12_146
<=> e23 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_146])],[avatar_definition]) ).
fof(f1141,plain,
( e23 = op2(e23,e22)
| ~ spl12_146 ),
inference(avatar_component_clause,[],[f1140]) ).
fof(f1145,definition,
( spl12_147
<=> e22 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_147])],[avatar_definition]) ).
fof(f1150,definition,
( spl12_148
<=> e22 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_148])],[avatar_definition]) ).
fof(f1160,definition,
( spl12_150
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_150])],[avatar_definition]) ).
fof(f1161,plain,
( e21 = op2(e23,e23)
| ~ spl12_150 ),
inference(avatar_component_clause,[],[f1160]) ).
fof(f1164,definition,
( spl12_151
<=> e23 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_151])],[avatar_definition]) ).
fof(f1167,plain,
( ~ spl12_150
| ~ spl12_151 ),
inference(avatar_split_clause,[],[f338,f1164,f1160]) ).
fof(f1169,definition,
( spl12_152
<=> e21 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_152])],[avatar_definition]) ).
fof(f1174,definition,
( spl12_153
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl12_153])],[avatar_definition]) ).
fof(f1179,definition,
( spl12_154
<=> op2(e20,e20) = e21 ),
introduced(definition,[new_symbols(definition,[spl12_154])],[avatar_definition]) ).
fof(f1180,plain,
( op2(e20,e20) = e21
| ~ spl12_154 ),
inference(avatar_component_clause,[],[f1179]) ).
fof(f1184,definition,
( spl12_155
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl12_155])],[avatar_definition]) ).
fof(f1185,plain,
( e20 = op2(e23,e23)
| ~ spl12_155 ),
inference(avatar_component_clause,[],[f1184]) ).
fof(f1188,definition,
( spl12_156
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_156])],[avatar_definition]) ).
fof(f1189,plain,
( e23 = op2(e23,e20)
| ~ spl12_156 ),
inference(avatar_component_clause,[],[f1188]) ).
fof(f1193,definition,
( spl12_157
<=> e20 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl12_157])],[avatar_definition]) ).
fof(f1203,definition,
( spl12_159
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl12_159])],[avatar_definition]) ).
fof(f1208,definition,
( spl12_160
<=> e22 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_160])],[avatar_definition]) ).
fof(f1213,plain,
( ~ spl12_143
| ~ spl12_160 ),
inference(avatar_split_clause,[],[f348,f1208,f1126]) ).
fof(f1216,plain,
~ spl12_147,
inference(avatar_split_clause,[],[f481,f1145]) ).
fof(f1220,definition,
( spl12_161
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_161])],[avatar_definition]) ).
fof(f1223,plain,
( ~ spl12_150
| ~ spl12_161 ),
inference(avatar_split_clause,[],[f354,f1220,f1160]) ).
fof(f1228,definition,
( spl12_162
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_162])],[avatar_definition]) ).
fof(f1229,plain,
( e22 = op2(e22,e20)
| ~ spl12_162 ),
inference(avatar_component_clause,[],[f1228]) ).
fof(f1244,definition,
( spl12_164
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_164])],[avatar_definition]) ).
fof(f1245,plain,
( e21 = op2(e21,e22)
| ~ spl12_164 ),
inference(avatar_component_clause,[],[f1244]) ).
fof(f1253,plain,
~ spl12_153,
inference(avatar_split_clause,[],[f482,f1174]) ).
fof(f1256,definition,
( spl12_165
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_165])],[avatar_definition]) ).
fof(f1264,definition,
( spl12_166
<=> e20 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_166])],[avatar_definition]) ).
fof(f1269,plain,
( ~ spl12_143
| ~ spl12_166 ),
inference(avatar_split_clause,[],[f380,f1264,f1126]) ).
fof(f1272,definition,
( spl12_167
<=> e20 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_167])],[avatar_definition]) ).
fof(f1273,plain,
( e20 = op2(e20,e22)
| ~ spl12_167 ),
inference(avatar_component_clause,[],[f1272]) ).
fof(f1277,plain,
( ~ spl12_148
| ~ spl12_167 ),
inference(avatar_split_clause,[],[f384,f1272,f1150]) ).
fof(f1280,definition,
( spl12_168
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_168])],[avatar_definition]) ).
fof(f1283,plain,
( ~ spl12_150
| ~ spl12_168 ),
inference(avatar_split_clause,[],[f386,f1280,f1160]) ).
fof(f1290,plain,
~ spl12_159,
inference(avatar_split_clause,[],[f483,f1203]) ).
fof(f1292,definition,
( spl12_169
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_169])],[avatar_definition]) ).
fof(f1293,plain,
( e13 = op1(e12,e12)
| ~ spl12_169 ),
inference(avatar_component_clause,[],[f1292]) ).
fof(f1301,definition,
( spl12_171
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_171])],[avatar_definition]) ).
fof(f1302,plain,
( e13 = op1(e11,e11)
| ~ spl12_171 ),
inference(avatar_component_clause,[],[f1301]) ).
fof(f1306,definition,
( spl12_172
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl12_172])],[avatar_definition]) ).
fof(f1311,definition,
( spl12_173
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_173])],[avatar_definition]) ).
fof(f1320,definition,
( spl12_175
<=> e12 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_175])],[avatar_definition]) ).
fof(f1335,definition,
( spl12_178
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_178])],[avatar_definition]) ).
fof(f1336,plain,
( e11 = op1(e13,e13)
| ~ spl12_178 ),
inference(avatar_component_clause,[],[f1335]) ).
fof(f1339,definition,
( spl12_179
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_179])],[avatar_definition]) ).
fof(f1342,plain,
( ~ spl12_178
| ~ spl12_179 ),
inference(avatar_split_clause,[],[f274,f1339,f1335]) ).
fof(f1344,definition,
( spl12_180
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_180])],[avatar_definition]) ).
fof(f1345,plain,
( e11 = op1(e12,e12)
| ~ spl12_180 ),
inference(avatar_component_clause,[],[f1344]) ).
fof(f1349,definition,
( spl12_181
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl12_181])],[avatar_definition]) ).
fof(f1354,definition,
( spl12_182
<=> op1(e10,e10) = e11 ),
introduced(definition,[new_symbols(definition,[spl12_182])],[avatar_definition]) ).
fof(f1355,plain,
( op1(e10,e10) = e11
| ~ spl12_182 ),
inference(avatar_component_clause,[],[f1354]) ).
fof(f1363,definition,
( spl12_184
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_184])],[avatar_definition]) ).
fof(f1364,plain,
( e13 = op1(e13,e10)
| ~ spl12_184 ),
inference(avatar_component_clause,[],[f1363]) ).
fof(f1368,definition,
( spl12_185
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl12_185])],[avatar_definition]) ).
fof(f1378,definition,
( spl12_187
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl12_187])],[avatar_definition]) ).
fof(f1383,definition,
( spl12_188
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_188])],[avatar_definition]) ).
fof(f1388,plain,
( ~ spl12_171
| ~ spl12_188 ),
inference(avatar_split_clause,[],[f284,f1383,f1301]) ).
fof(f1391,plain,
~ spl12_175,
inference(avatar_split_clause,[],[f485,f1320]) ).
fof(f1395,definition,
( spl12_189
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_189])],[avatar_definition]) ).
fof(f1398,plain,
( ~ spl12_178
| ~ spl12_189 ),
inference(avatar_split_clause,[],[f290,f1395,f1335]) ).
fof(f1403,definition,
( spl12_190
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_190])],[avatar_definition]) ).
fof(f1404,plain,
( e12 = op1(e12,e10)
| ~ spl12_190 ),
inference(avatar_component_clause,[],[f1403]) ).
fof(f1407,plain,
( ~ spl12_185
| ~ spl12_190 ),
inference(avatar_split_clause,[],[f295,f1403,f1368]) ).
fof(f1419,definition,
( spl12_192
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_192])],[avatar_definition]) ).
fof(f1420,plain,
( e11 = op1(e11,e12)
| ~ spl12_192 ),
inference(avatar_component_clause,[],[f1419]) ).
fof(f1428,plain,
~ spl12_181,
inference(avatar_split_clause,[],[f486,f1349]) ).
fof(f1439,definition,
( spl12_194
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_194])],[avatar_definition]) ).
fof(f1444,plain,
( ~ spl12_171
| ~ spl12_194 ),
inference(avatar_split_clause,[],[f316,f1439,f1301]) ).
fof(f1447,definition,
( spl12_195
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_195])],[avatar_definition]) ).
fof(f1448,plain,
( e10 = op1(e10,e12)
| ~ spl12_195 ),
inference(avatar_component_clause,[],[f1447]) ).
fof(f1450,plain,
( ~ spl12_173
| ~ spl12_195 ),
inference(avatar_split_clause,[],[f318,f1447,f1311]) ).
fof(f1455,definition,
( spl12_196
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_196])],[avatar_definition]) ).
fof(f1458,plain,
( ~ spl12_178
| ~ spl12_196 ),
inference(avatar_split_clause,[],[f322,f1455,f1335]) ).
fof(f1465,plain,
~ spl12_187,
inference(avatar_split_clause,[],[f487,f1378]) ).
fof(f1475,definition,
( spl12_199
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_199])],[avatar_definition]) ).
fof(f1477,plain,
( e23 = op2(e20,e23)
| ~ spl12_199 ),
inference(avatar_component_clause,[],[f1475]) ).
fof(f1479,plain,
( spl12_142
| spl12_146
| spl12_151
| spl12_156 ),
inference(avatar_split_clause,[],[f111,f1188,f1164,f1140,f1121]) ).
fof(f1481,definition,
( spl12_200
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_200])],[avatar_definition]) ).
fof(f1483,plain,
( e22 = op2(e21,e23)
| ~ spl12_200 ),
inference(avatar_component_clause,[],[f1481]) ).
fof(f1490,definition,
( spl12_202
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_202])],[avatar_definition]) ).
fof(f1492,plain,
( e22 = op2(e23,e22)
| ~ spl12_202 ),
inference(avatar_component_clause,[],[f1490]) ).
fof(f1507,definition,
( spl12_206
<=> e21 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl12_206])],[avatar_definition]) ).
fof(f1512,definition,
( spl12_207
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_207])],[avatar_definition]) ).
fof(f1516,definition,
( spl12_208
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_208])],[avatar_definition]) ).
fof(f1525,definition,
( spl12_210
<=> e20 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_210])],[avatar_definition]) ).
fof(f1527,plain,
( e20 = op2(e22,e23)
| ~ spl12_210 ),
inference(avatar_component_clause,[],[f1525]) ).
fof(f1529,definition,
( spl12_211
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_211])],[avatar_definition]) ).
fof(f1531,plain,
( e20 = op2(e21,e23)
| ~ spl12_211 ),
inference(avatar_component_clause,[],[f1529]) ).
fof(f1532,plain,
( spl12_155
| spl12_210
| spl12_211
| spl12_166 ),
inference(avatar_split_clause,[],[f116,f1264,f1529,f1525,f1184]) ).
fof(f1538,definition,
( spl12_213
<=> e20 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl12_213])],[avatar_definition]) ).
fof(f1540,plain,
( e20 = op2(e23,e21)
| ~ spl12_213 ),
inference(avatar_component_clause,[],[f1538]) ).
fof(f1551,definition,
( spl12_216
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_216])],[avatar_definition]) ).
fof(f1553,plain,
( e23 = op2(e20,e22)
| ~ spl12_216 ),
inference(avatar_component_clause,[],[f1551]) ).
fof(f1556,definition,
( spl12_217
<=> e23 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_217])],[avatar_definition]) ).
fof(f1558,plain,
( e23 = op2(e22,e21)
| ~ spl12_217 ),
inference(avatar_component_clause,[],[f1556]) ).
fof(f1565,definition,
( spl12_219
<=> e22 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl12_219])],[avatar_definition]) ).
fof(f1567,plain,
( e22 = op2(e21,e22)
| ~ spl12_219 ),
inference(avatar_component_clause,[],[f1565]) ).
fof(f1569,definition,
( spl12_220
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_220])],[avatar_definition]) ).
fof(f1571,plain,
( e22 = op2(e20,e22)
| ~ spl12_220 ),
inference(avatar_component_clause,[],[f1569]) ).
fof(f1572,plain,
( spl12_202
| spl12_147
| spl12_219
| spl12_220 ),
inference(avatar_split_clause,[],[f120,f1569,f1565,f1145,f1490]) ).
fof(f1573,plain,
( spl12_160
| spl12_147
| spl12_161
| spl12_162 ),
inference(avatar_split_clause,[],[f121,f1228,f1220,f1145,f1208]) ).
fof(f1575,definition,
( spl12_221
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl12_221])],[avatar_definition]) ).
fof(f1577,plain,
( e21 = op2(e20,e22)
| ~ spl12_221 ),
inference(avatar_component_clause,[],[f1575]) ).
fof(f1578,plain,
( spl12_207
| spl12_152
| spl12_164
| spl12_221 ),
inference(avatar_split_clause,[],[f122,f1575,f1244,f1169,f1512]) ).
fof(f1580,definition,
( spl12_222
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_222])],[avatar_definition]) ).
fof(f1582,plain,
( e21 = op2(e22,e21)
| ~ spl12_222 ),
inference(avatar_component_clause,[],[f1580]) ).
fof(f1603,definition,
( spl12_227
<=> e23 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_227])],[avatar_definition]) ).
fof(f1605,plain,
( e23 = op2(e20,e21)
| ~ spl12_227 ),
inference(avatar_component_clause,[],[f1603]) ).
fof(f1606,plain,
( spl12_151
| spl12_217
| spl12_143
| spl12_227 ),
inference(avatar_split_clause,[],[f126,f1603,f1126,f1556,f1164]) ).
fof(f1608,definition,
( spl12_228
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_228])],[avatar_definition]) ).
fof(f1613,definition,
( spl12_229
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_229])],[avatar_definition]) ).
fof(f1615,plain,
( e22 = op2(e20,e21)
| ~ spl12_229 ),
inference(avatar_component_clause,[],[f1613]) ).
fof(f1618,definition,
( spl12_230
<=> e22 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_230])],[avatar_definition]) ).
fof(f1621,plain,
( spl12_200
| spl12_219
| spl12_148
| spl12_230 ),
inference(avatar_split_clause,[],[f129,f1618,f1150,f1565,f1481]) ).
fof(f1623,definition,
( spl12_231
<=> e21 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl12_231])],[avatar_definition]) ).
fof(f1625,plain,
( e21 = op2(e20,e21)
| ~ spl12_231 ),
inference(avatar_component_clause,[],[f1623]) ).
fof(f1626,plain,
( spl12_208
| spl12_222
| spl12_153
| spl12_231 ),
inference(avatar_split_clause,[],[f130,f1623,f1174,f1580,f1516]) ).
fof(f1630,definition,
( spl12_232
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_232])],[avatar_definition]) ).
fof(f1635,plain,
( spl12_199
| spl12_216
| spl12_227
| spl12_144 ),
inference(avatar_split_clause,[],[f135,f1131,f1603,f1551,f1475]) ).
fof(f1639,plain,
( spl12_206
| spl12_221
| spl12_231
| spl12_154 ),
inference(avatar_split_clause,[],[f139,f1179,f1623,f1575,f1507]) ).
fof(f1641,plain,
( spl12_166
| spl12_167
| spl12_168
| spl12_159 ),
inference(avatar_split_clause,[],[f141,f1203,f1280,f1272,f1264]) ).
fof(f1647,plain,
( spl12_141
| spl12_147
| spl12_152
| spl12_157 ),
inference(avatar_split_clause,[],[f99,f1193,f1169,f1145,f1117]) ).
fof(f1653,plain,
( spl12_228
| spl12_230
| spl12_165
| spl12_232 ),
inference(avatar_split_clause,[],[f105,f1630,f1256,f1618,f1608]) ).
fof(f1667,definition,
( spl12_235
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_235])],[avatar_definition]) ).
fof(f1669,plain,
( e13 = op1(e10,e13)
| ~ spl12_235 ),
inference(avatar_component_clause,[],[f1667]) ).
fof(f1673,definition,
( spl12_236
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_236])],[avatar_definition]) ).
fof(f1675,plain,
( e12 = op1(e11,e13)
| ~ spl12_236 ),
inference(avatar_component_clause,[],[f1673]) ).
fof(f1677,definition,
( spl12_237
<=> e12 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_237])],[avatar_definition]) ).
fof(f1679,plain,
( e12 = op1(e10,e13)
| ~ spl12_237 ),
inference(avatar_component_clause,[],[f1677]) ).
fof(f1680,plain,
( spl12_173
| spl12_188
| spl12_236
| spl12_237 ),
inference(avatar_split_clause,[],[f64,f1677,f1673,f1383,f1311]) ).
fof(f1682,definition,
( spl12_238
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_238])],[avatar_definition]) ).
fof(f1684,plain,
( e12 = op1(e13,e12)
| ~ spl12_238 ),
inference(avatar_component_clause,[],[f1682]) ).
fof(f1690,definition,
( spl12_240
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_240])],[avatar_definition]) ).
fof(f1699,definition,
( spl12_242
<=> e11 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl12_242])],[avatar_definition]) ).
fof(f1704,definition,
( spl12_243
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_243])],[avatar_definition]) ).
fof(f1708,definition,
( spl12_244
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_244])],[avatar_definition]) ).
fof(f1712,definition,
( spl12_245
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_245])],[avatar_definition]) ).
fof(f1717,definition,
( spl12_246
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl12_246])],[avatar_definition]) ).
fof(f1719,plain,
( e10 = op1(e12,e13)
| ~ spl12_246 ),
inference(avatar_component_clause,[],[f1717]) ).
fof(f1730,definition,
( spl12_249
<=> e10 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl12_249])],[avatar_definition]) ).
fof(f1732,plain,
( e10 = op1(e13,e11)
| ~ spl12_249 ),
inference(avatar_component_clause,[],[f1730]) ).
fof(f1734,definition,
( spl12_250
<=> e10 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl12_250])],[avatar_definition]) ).
fof(f1743,definition,
( spl12_252
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_252])],[avatar_definition]) ).
fof(f1745,plain,
( e13 = op1(e10,e12)
| ~ spl12_252 ),
inference(avatar_component_clause,[],[f1743]) ).
fof(f1748,definition,
( spl12_253
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_253])],[avatar_definition]) ).
fof(f1750,plain,
( e13 = op1(e12,e11)
| ~ spl12_253 ),
inference(avatar_component_clause,[],[f1748]) ).
fof(f1757,definition,
( spl12_255
<=> e12 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl12_255])],[avatar_definition]) ).
fof(f1759,plain,
( e12 = op1(e11,e12)
| ~ spl12_255 ),
inference(avatar_component_clause,[],[f1757]) ).
fof(f1761,definition,
( spl12_256
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_256])],[avatar_definition]) ).
fof(f1763,plain,
( e12 = op1(e10,e12)
| ~ spl12_256 ),
inference(avatar_component_clause,[],[f1761]) ).
fof(f1764,plain,
( spl12_238
| spl12_175
| spl12_255
| spl12_256 ),
inference(avatar_split_clause,[],[f72,f1761,f1757,f1320,f1682]) ).
fof(f1765,plain,
( spl12_188
| spl12_175
| spl12_189
| spl12_190 ),
inference(avatar_split_clause,[],[f73,f1403,f1395,f1320,f1383]) ).
fof(f1767,definition,
( spl12_257
<=> e11 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl12_257])],[avatar_definition]) ).
fof(f1769,plain,
( e11 = op1(e10,e12)
| ~ spl12_257 ),
inference(avatar_component_clause,[],[f1767]) ).
fof(f1770,plain,
( spl12_243
| spl12_180
| spl12_192
| spl12_257 ),
inference(avatar_split_clause,[],[f74,f1767,f1419,f1344,f1704]) ).
fof(f1772,definition,
( spl12_258
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_258])],[avatar_definition]) ).
fof(f1774,plain,
( e11 = op1(e12,e11)
| ~ spl12_258 ),
inference(avatar_component_clause,[],[f1772]) ).
fof(f1786,definition,
( spl12_261
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl12_261])],[avatar_definition]) ).
fof(f1790,definition,
( spl12_262
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl12_262])],[avatar_definition]) ).
fof(f1792,plain,
( e10 = op1(e12,e10)
| ~ spl12_262 ),
inference(avatar_component_clause,[],[f1790]) ).
fof(f1793,plain,
( spl12_246
| spl12_185
| spl12_261
| spl12_262 ),
inference(avatar_split_clause,[],[f77,f1790,f1786,f1368,f1717]) ).
fof(f1795,definition,
( spl12_263
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_263])],[avatar_definition]) ).
fof(f1797,plain,
( e13 = op1(e10,e11)
| ~ spl12_263 ),
inference(avatar_component_clause,[],[f1795]) ).
fof(f1798,plain,
( spl12_179
| spl12_253
| spl12_171
| spl12_263 ),
inference(avatar_split_clause,[],[f78,f1795,f1301,f1748,f1339]) ).
fof(f1805,definition,
( spl12_265
<=> e12 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_265])],[avatar_definition]) ).
fof(f1807,plain,
( e12 = op1(e10,e11)
| ~ spl12_265 ),
inference(avatar_component_clause,[],[f1805]) ).
fof(f1815,definition,
( spl12_267
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl12_267])],[avatar_definition]) ).
fof(f1817,plain,
( e11 = op1(e10,e11)
| ~ spl12_267 ),
inference(avatar_component_clause,[],[f1815]) ).
fof(f1818,plain,
( spl12_244
| spl12_258
| spl12_181
| spl12_267 ),
inference(avatar_split_clause,[],[f82,f1815,f1349,f1772,f1708]) ).
fof(f1822,definition,
( spl12_268
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl12_268])],[avatar_definition]) ).
fof(f1824,plain,
( e10 = op1(e11,e10)
| ~ spl12_268 ),
inference(avatar_component_clause,[],[f1822]) ).
fof(f1827,plain,
( spl12_235
| spl12_252
| spl12_263
| spl12_172 ),
inference(avatar_split_clause,[],[f87,f1306,f1795,f1743,f1667]) ).
fof(f1831,plain,
( spl12_242
| spl12_257
| spl12_267
| spl12_182 ),
inference(avatar_split_clause,[],[f91,f1354,f1815,f1767,f1699]) ).
fof(f1832,plain,
( spl12_250
| spl12_262
| spl12_268
| spl12_187 ),
inference(avatar_split_clause,[],[f92,f1378,f1822,f1790,f1734]) ).
fof(f1833,plain,
( spl12_194
| spl12_195
| spl12_196
| spl12_187 ),
inference(avatar_split_clause,[],[f93,f1378,f1455,f1447,f1439]) ).
fof(f1837,plain,
( spl12_184
| spl12_240
| spl12_245
| spl12_250 ),
inference(avatar_split_clause,[],[f49,f1734,f1712,f1690,f1363]) ).
fof(f1839,plain,
( spl12_169
| spl12_175
| spl12_180
| spl12_185 ),
inference(avatar_split_clause,[],[f51,f1368,f1344,f1320,f1292]) ).
fof(f1852,plain,
spl12_178,
inference(avatar_split_clause,[],[f395,f1335]) ).
fof(f1853,plain,
spl12_150,
inference(avatar_split_clause,[],[f398,f1160]) ).
fof(f1854,plain,
~ spl12_142,
inference(avatar_split_clause,[],[f480,f1121]) ).
fof(f1855,plain,
( op2(e21,e21) != h2(op1(e13,e13))
| spl12_51
| ~ spl12_125 ),
inference(superposition,[],[f699,f1034]) ).
fof(f1874,plain,
( op2(e21,e21) != h2(e11)
| spl12_51
| ~ spl12_125
| ~ spl12_178 ),
inference(superposition,[],[f1855,f1336]) ).
fof(f2031,plain,
( e21 = e23
| ~ spl12_217
| ~ spl12_222 ),
inference(forward_demodulation,[],[f1582,f1558]) ).
fof(f2032,plain,
( $false
| ~ spl12_217
| ~ spl12_222 ),
inference(forward_subsumption_resolution,[],[f2031,f245]) ).
fof(f2033,plain,
( ~ spl12_217
| ~ spl12_222 ),
inference(avatar_contradiction_clause,[],[f2032]) ).
fof(f2086,plain,
( e22 = e23
| ~ spl12_146
| ~ spl12_202 ),
inference(superposition,[],[f1141,f1492]) ).
fof(f2090,plain,
( $false
| ~ spl12_146
| ~ spl12_202 ),
inference(forward_subsumption_resolution,[],[f2086,f244]) ).
fof(f2091,plain,
( ~ spl12_146
| ~ spl12_202 ),
inference(avatar_contradiction_clause,[],[f2090]) ).
fof(f2123,plain,
( e21 = e22
| ~ spl12_164
| ~ spl12_219 ),
inference(forward_demodulation,[],[f1567,f1245]) ).
fof(f2124,plain,
( $false
| ~ spl12_164
| ~ spl12_219 ),
inference(forward_subsumption_resolution,[],[f2123,f246]) ).
fof(f2125,plain,
( ~ spl12_164
| ~ spl12_219 ),
inference(avatar_contradiction_clause,[],[f2124]) ).
fof(f2141,plain,
( e20 = e21
| ~ spl12_150
| ~ spl12_155 ),
inference(superposition,[],[f1185,f1161]) ).
fof(f2146,plain,
( $false
| ~ spl12_150
| ~ spl12_155 ),
inference(forward_subsumption_resolution,[],[f2141,f249]) ).
fof(f2147,plain,
( ~ spl12_150
| ~ spl12_155 ),
inference(avatar_contradiction_clause,[],[f2146]) ).
fof(f2154,plain,
( e20 = e22
| ~ spl12_200
| ~ spl12_211 ),
inference(superposition,[],[f1531,f1483]) ).
fof(f2160,plain,
( $false
| ~ spl12_200
| ~ spl12_211 ),
inference(forward_subsumption_resolution,[],[f2154,f248]) ).
fof(f2161,plain,
( ~ spl12_200
| ~ spl12_211 ),
inference(avatar_contradiction_clause,[],[f2160]) ).
fof(f2164,plain,
( e20 = e21
| ~ spl12_167
| ~ spl12_221 ),
inference(forward_demodulation,[],[f1577,f1273]) ).
fof(f2167,plain,
( $false
| ~ spl12_167
| ~ spl12_221 ),
inference(forward_subsumption_resolution,[],[f2164,f249]) ).
fof(f2168,plain,
( ~ spl12_167
| ~ spl12_221 ),
inference(avatar_contradiction_clause,[],[f2167]) ).
fof(f2174,plain,
( e20 = e22
| ~ spl12_167
| ~ spl12_220 ),
inference(forward_demodulation,[],[f1571,f1273]) ).
fof(f2175,plain,
( $false
| ~ spl12_167
| ~ spl12_220 ),
inference(forward_subsumption_resolution,[],[f2174,f248]) ).
fof(f2176,plain,
( ~ spl12_167
| ~ spl12_220 ),
inference(avatar_contradiction_clause,[],[f2175]) ).
fof(f2204,plain,
( e22 = e23
| ~ spl12_227
| ~ spl12_229 ),
inference(forward_demodulation,[],[f1615,f1605]) ).
fof(f2205,plain,
( $false
| ~ spl12_227
| ~ spl12_229 ),
inference(forward_subsumption_resolution,[],[f2204,f244]) ).
fof(f2206,plain,
( ~ spl12_227
| ~ spl12_229 ),
inference(avatar_contradiction_clause,[],[f2205]) ).
fof(f2207,plain,
( e20 = e23
| ~ spl12_167
| ~ spl12_216 ),
inference(superposition,[],[f1553,f1273]) ).
fof(f2211,plain,
( $false
| ~ spl12_167
| ~ spl12_216 ),
inference(forward_subsumption_resolution,[],[f2207,f247]) ).
fof(f2212,plain,
( ~ spl12_167
| ~ spl12_216 ),
inference(avatar_contradiction_clause,[],[f2211]) ).
fof(f2214,plain,
( e21 = e23
| ~ spl12_144
| ~ spl12_154 ),
inference(superposition,[],[f1132,f1180]) ).
fof(f2220,plain,
( $false
| ~ spl12_144
| ~ spl12_154 ),
inference(forward_subsumption_resolution,[],[f2214,f245]) ).
fof(f2221,plain,
( ~ spl12_144
| ~ spl12_154 ),
inference(avatar_contradiction_clause,[],[f2220]) ).
fof(f2372,plain,
( e12 = e13
| ~ spl12_235
| ~ spl12_237 ),
inference(superposition,[],[f1669,f1679]) ).
fof(f2377,plain,
( $false
| ~ spl12_235
| ~ spl12_237 ),
inference(forward_subsumption_resolution,[],[f2372,f238]) ).
fof(f2378,plain,
( ~ spl12_235
| ~ spl12_237 ),
inference(avatar_contradiction_clause,[],[f2377]) ).
fof(f2455,plain,
( e10 = e13
| ~ spl12_195
| ~ spl12_252 ),
inference(superposition,[],[f1745,f1448]) ).
fof(f2459,plain,
( $false
| ~ spl12_195
| ~ spl12_252 ),
inference(forward_subsumption_resolution,[],[f2455,f241]) ).
fof(f2460,plain,
( ~ spl12_195
| ~ spl12_252 ),
inference(avatar_contradiction_clause,[],[f2459]) ).
fof(f2499,plain,
( e11 = e12
| ~ spl12_192
| ~ spl12_255 ),
inference(forward_demodulation,[],[f1759,f1420]) ).
fof(f2500,plain,
( $false
| ~ spl12_192
| ~ spl12_255 ),
inference(forward_subsumption_resolution,[],[f2499,f240]) ).
fof(f2501,plain,
( ~ spl12_192
| ~ spl12_255 ),
inference(avatar_contradiction_clause,[],[f2500]) ).
fof(f2544,plain,
( e11 = e13
| ~ spl12_253
| ~ spl12_258 ),
inference(forward_demodulation,[],[f1774,f1750]) ).
fof(f2545,plain,
( $false
| ~ spl12_253
| ~ spl12_258 ),
inference(forward_subsumption_resolution,[],[f2544,f239]) ).
fof(f2546,plain,
( ~ spl12_253
| ~ spl12_258 ),
inference(avatar_contradiction_clause,[],[f2545]) ).
fof(f2560,plain,
( e12 = e13
| ~ spl12_263
| ~ spl12_265 ),
inference(forward_demodulation,[],[f1807,f1797]) ).
fof(f2561,plain,
( $false
| ~ spl12_263
| ~ spl12_265 ),
inference(forward_subsumption_resolution,[],[f2560,f238]) ).
fof(f2562,plain,
( ~ spl12_263
| ~ spl12_265 ),
inference(avatar_contradiction_clause,[],[f2561]) ).
fof(f2598,plain,
( $false
| spl12_51
| ~ spl12_125
| ~ spl12_178 ),
inference(forward_subsumption_resolution,[],[f405,f1874]) ).
fof(f2599,plain,
( spl12_51
| ~ spl12_125
| ~ spl12_178 ),
inference(avatar_contradiction_clause,[],[f2598]) ).
fof(f2600,plain,
( op2(e21,e21) = h2(op1(e13,e13))
| ~ spl12_51
| ~ spl12_125 ),
inference(forward_demodulation,[],[f698,f1034]) ).
fof(f2601,plain,
( h2(op1(e13,e12)) != op2(e21,h2(e12))
| spl12_52
| ~ spl12_125 ),
inference(forward_demodulation,[],[f703,f1034]) ).
fof(f2603,plain,
( op2(e21,e21) = h2(e11)
| ~ spl12_51
| ~ spl12_125
| ~ spl12_178 ),
inference(forward_demodulation,[],[f2600,f1336]) ).
fof(f2604,plain,
( h2(e12) != op2(e21,h2(e12))
| spl12_52
| ~ spl12_125
| ~ spl12_238 ),
inference(forward_demodulation,[],[f2601,f1684]) ).
fof(f2623,plain,
( e11 != op1(e13,e12)
| ~ spl12_178 ),
inference(forward_demodulation,[],[f142,f1336]) ).
fof(f2625,plain,
( e11 != op1(e13,e11)
| ~ spl12_178 ),
inference(forward_demodulation,[],[f143,f1336]) ).
fof(f2629,plain,
( e11 != op1(e13,e10)
| ~ spl12_178 ),
inference(forward_demodulation,[],[f145,f1336]) ).
fof(f2631,plain,
( e12 != op1(e13,e10)
| ~ spl12_238 ),
inference(forward_demodulation,[],[f146,f1684]) ).
fof(f2633,plain,
( e10 != op1(e13,e10)
| ~ spl12_249 ),
inference(forward_demodulation,[],[f147,f1732]) ).
fof(f2637,plain,
( e11 != op1(e12,e11)
| ~ spl12_180 ),
inference(forward_demodulation,[],[f150,f1345]) ).
fof(f2668,plain,
( e11 != op1(e10,e13)
| ~ spl12_178 ),
inference(forward_demodulation,[],[f169,f1336]) ).
fof(f2683,plain,
( e10 != op1(e12,e11)
| ~ spl12_249 ),
inference(forward_demodulation,[],[f178,f1732]) ).
fof(f2697,plain,
( op1(e10,e10) != e13
| ~ spl12_184 ),
inference(forward_demodulation,[],[f187,f1364]) ).
fof(f2702,plain,
( e21 != op2(e23,e22)
| ~ spl12_150 ),
inference(forward_demodulation,[],[f190,f1161]) ).
fof(f2704,plain,
( e21 != op2(e23,e21)
| ~ spl12_150 ),
inference(forward_demodulation,[],[f191,f1161]) ).
fof(f2723,plain,
( e21 != op2(e21,e20)
| ~ spl12_164 ),
inference(forward_demodulation,[],[f206,f1245]) ).
fof(f2739,plain,
( e21 != op2(e20,e23)
| ~ spl12_150 ),
inference(forward_demodulation,[],[f217,f1161]) ).
fof(f2769,plain,
( e10 = op1(e13,e11)
| ~ spl12_178 ),
inference(forward_demodulation,[],[f396,f1336]) ).
fof(f2770,plain,
( e20 = op2(e23,e21)
| ~ spl12_150 ),
inference(forward_demodulation,[],[f399,f1161]) ).
fof(f2771,plain,
( spl12_213
| ~ spl12_150 ),
inference(avatar_split_clause,[],[f2770,f1160,f1538]) ).
fof(f2772,plain,
( ~ spl12_208
| ~ spl12_150 ),
inference(avatar_split_clause,[],[f2704,f1160,f1516]) ).
fof(f2773,plain,
( ~ spl12_206
| ~ spl12_150 ),
inference(avatar_split_clause,[],[f2739,f1160,f1507]) ).
fof(f2792,plain,
( e23 = h2(e11)
| ~ spl12_51
| ~ spl12_125
| ~ spl12_143
| ~ spl12_178 ),
inference(superposition,[],[f2603,f1127]) ).
fof(f2799,plain,
( spl12_119
| ~ spl12_51
| ~ spl12_125
| ~ spl12_143
| ~ spl12_178 ),
inference(avatar_split_clause,[],[f2792,f1335,f1126,f1033,f697,f1003]) ).
fof(f2852,plain,
( e21 = e22
| ~ spl12_229
| ~ spl12_231 ),
inference(superposition,[],[f1625,f1615]) ).
fof(f2858,plain,
( $false
| ~ spl12_229
| ~ spl12_231 ),
inference(forward_subsumption_resolution,[],[f2852,f246]) ).
fof(f2859,plain,
( ~ spl12_229
| ~ spl12_231 ),
inference(avatar_contradiction_clause,[],[f2858]) ).
fof(f2870,plain,
( ~ spl12_207
| ~ spl12_150 ),
inference(avatar_split_clause,[],[f2702,f1160,f1512]) ).
fof(f2883,plain,
( ~ spl12_165
| ~ spl12_164 ),
inference(avatar_split_clause,[],[f2723,f1244,f1256]) ).
fof(f2971,plain,
( e23 != op2(e21,e20)
| ~ spl12_156 ),
inference(forward_demodulation,[],[f233,f1189]) ).
fof(f2972,plain,
( e22 != op2(e21,e20)
| ~ spl12_162 ),
inference(forward_demodulation,[],[f234,f1229]) ).
fof(f2982,plain,
( h2(e10) = op2(e21,h2(e11))
| ~ spl12_51
| ~ spl12_125
| ~ spl12_178 ),
inference(forward_demodulation,[],[f406,f2603]) ).
fof(f2983,plain,
( op2(e21,e23) = h2(e10)
| ~ spl12_51
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178 ),
inference(forward_demodulation,[],[f2982,f1004]) ).
fof(f2984,plain,
( e22 = h2(e10)
| ~ spl12_51
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178
| ~ spl12_200 ),
inference(forward_demodulation,[],[f2983,f1483]) ).
fof(f2985,plain,
( spl12_124
| ~ spl12_51
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178
| ~ spl12_200 ),
inference(avatar_split_clause,[],[f2984,f1481,f1335,f1033,f1003,f697,f1028]) ).
fof(f2992,plain,
( e12 = op1(op1(e13,e11),e11)
| ~ spl12_178 ),
inference(forward_demodulation,[],[f394,f1336]) ).
fof(f2993,plain,
( e12 = op1(e10,e11)
| ~ spl12_178
| ~ spl12_249 ),
inference(forward_demodulation,[],[f2992,f1732]) ).
fof(f2998,plain,
( e11 = e12
| ~ spl12_178
| ~ spl12_249
| ~ spl12_267 ),
inference(forward_demodulation,[],[f2993,f1817]) ).
fof(f3001,plain,
( $false
| ~ spl12_178
| ~ spl12_249
| ~ spl12_267 ),
inference(forward_subsumption_resolution,[],[f2998,f240]) ).
fof(f3002,plain,
( ~ spl12_178
| ~ spl12_249
| ~ spl12_267 ),
inference(avatar_contradiction_clause,[],[f3001]) ).
fof(f3003,plain,
( e10 = e12
| ~ spl12_190
| ~ spl12_262 ),
inference(forward_demodulation,[],[f1404,f1792]) ).
fof(f3004,plain,
( spl12_265
| ~ spl12_178
| ~ spl12_249 ),
inference(avatar_split_clause,[],[f2993,f1730,f1335,f1805]) ).
fof(f3005,plain,
( ~ spl12_258
| ~ spl12_180 ),
inference(avatar_split_clause,[],[f2637,f1344,f1772]) ).
fof(f3007,plain,
( ~ spl12_261
| ~ spl12_249 ),
inference(avatar_split_clause,[],[f2683,f1730,f1786]) ).
fof(f3013,plain,
( ~ spl12_242
| ~ spl12_178 ),
inference(avatar_split_clause,[],[f2668,f1335,f1699]) ).
fof(f3022,plain,
( ~ spl12_172
| ~ spl12_184 ),
inference(avatar_split_clause,[],[f2697,f1363,f1306]) ).
fof(f3023,plain,
( $false
| ~ spl12_190
| ~ spl12_262 ),
inference(forward_subsumption_resolution,[],[f3003,f242]) ).
fof(f3024,plain,
( ~ spl12_190
| ~ spl12_262 ),
inference(avatar_contradiction_clause,[],[f3023]) ).
fof(f3033,plain,
( ~ spl12_243
| ~ spl12_178 ),
inference(avatar_split_clause,[],[f2623,f1335,f1704]) ).
fof(f3035,plain,
( ~ spl12_245
| ~ spl12_178 ),
inference(avatar_split_clause,[],[f2629,f1335,f1712]) ).
fof(f3036,plain,
( ~ spl12_250
| ~ spl12_249 ),
inference(avatar_split_clause,[],[f2633,f1730,f1734]) ).
fof(f3043,plain,
( ~ spl12_244
| ~ spl12_178 ),
inference(avatar_split_clause,[],[f2625,f1335,f1708]) ).
fof(f3044,plain,
( spl12_249
| ~ spl12_178 ),
inference(avatar_split_clause,[],[f2769,f1335,f1730]) ).
fof(f3096,plain,
( e10 = e12
| ~ spl12_195
| ~ spl12_256 ),
inference(forward_demodulation,[],[f1763,f1448]) ).
fof(f3097,plain,
( $false
| ~ spl12_195
| ~ spl12_256 ),
inference(forward_subsumption_resolution,[],[f3096,f242]) ).
fof(f3098,plain,
( ~ spl12_195
| ~ spl12_256 ),
inference(avatar_contradiction_clause,[],[f3097]) ).
fof(f3102,plain,
( ~ spl12_240
| ~ spl12_238 ),
inference(avatar_split_clause,[],[f2631,f1682,f1690]) ).
fof(f3116,plain,
( e10 = e11
| ~ spl12_195
| ~ spl12_257 ),
inference(forward_demodulation,[],[f1769,f1448]) ).
fof(f3117,plain,
( $false
| ~ spl12_195
| ~ spl12_257 ),
inference(forward_subsumption_resolution,[],[f3116,f243]) ).
fof(f3118,plain,
( ~ spl12_195
| ~ spl12_257 ),
inference(avatar_contradiction_clause,[],[f3117]) ).
fof(f3206,plain,
( e22 = op2(op2(e23,e21),e21)
| ~ spl12_150 ),
inference(forward_demodulation,[],[f397,f1161]) ).
fof(f3207,plain,
( e22 = op2(e20,e21)
| ~ spl12_150
| ~ spl12_213 ),
inference(forward_demodulation,[],[f3206,f1540]) ).
fof(f3213,plain,
( h2(e12) = op2(op2(e21,h2(e11)),h2(e11))
| ~ spl12_51
| ~ spl12_125
| ~ spl12_178 ),
inference(forward_demodulation,[],[f404,f2603]) ).
fof(f3214,plain,
( h2(e12) = op2(op2(e21,e23),e23)
| ~ spl12_51
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178 ),
inference(forward_demodulation,[],[f3213,f1004]) ).
fof(f3215,plain,
( op2(e22,e23) = h2(e12)
| ~ spl12_51
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178
| ~ spl12_200 ),
inference(forward_demodulation,[],[f3214,f1483]) ).
fof(f3216,plain,
( e20 = h2(e12)
| ~ spl12_51
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178
| ~ spl12_200
| ~ spl12_210 ),
inference(forward_demodulation,[],[f3215,f1527]) ).
fof(f3217,plain,
( spl12_67
| ~ spl12_51
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178
| ~ spl12_200
| ~ spl12_210 ),
inference(avatar_split_clause,[],[f3216,f1525,f1481,f1335,f1033,f1003,f697,f762]) ).
fof(f3218,plain,
( e20 != op2(e21,e20)
| spl12_52
| ~ spl12_67
| ~ spl12_125
| ~ spl12_238 ),
inference(superposition,[],[f2604,f763]) ).
fof(f3222,plain,
( h2(op1(e13,e10)) != op2(h2(e13),e22)
| spl12_54
| ~ spl12_124 ),
inference(forward_demodulation,[],[f711,f1029]) ).
fof(f3224,plain,
( op2(e21,e22) != h2(op1(e13,e10))
| spl12_54
| ~ spl12_124
| ~ spl12_125 ),
inference(forward_demodulation,[],[f3222,f1034]) ).
fof(f3226,plain,
( op2(e21,e22) != h2(e13)
| spl12_54
| ~ spl12_124
| ~ spl12_125
| ~ spl12_184 ),
inference(forward_demodulation,[],[f3224,f1364]) ).
fof(f3228,plain,
( e21 != op2(e21,e22)
| spl12_54
| ~ spl12_124
| ~ spl12_125
| ~ spl12_184 ),
inference(forward_demodulation,[],[f3226,f1034]) ).
fof(f3231,plain,
( h2(op1(e13,e11)) != op2(h2(e13),e23)
| spl12_53
| ~ spl12_119 ),
inference(forward_demodulation,[],[f707,f1004]) ).
fof(f3233,plain,
( op2(e21,e23) != h2(op1(e13,e11))
| spl12_53
| ~ spl12_119
| ~ spl12_125 ),
inference(forward_demodulation,[],[f3231,f1034]) ).
fof(f3235,plain,
( op2(e21,e23) != h2(e10)
| spl12_53
| ~ spl12_119
| ~ spl12_125
| ~ spl12_249 ),
inference(forward_demodulation,[],[f3233,f1732]) ).
fof(f3237,plain,
( e22 != op2(e21,e23)
| spl12_53
| ~ spl12_119
| ~ spl12_124
| ~ spl12_125
| ~ spl12_249 ),
inference(forward_demodulation,[],[f3235,f1029]) ).
fof(f3239,plain,
( $false
| spl12_53
| ~ spl12_119
| ~ spl12_124
| ~ spl12_125
| ~ spl12_200
| ~ spl12_249 ),
inference(forward_subsumption_resolution,[],[f3237,f1483]) ).
fof(f3240,plain,
( spl12_53
| ~ spl12_119
| ~ spl12_124
| ~ spl12_125
| ~ spl12_200
| ~ spl12_249 ),
inference(avatar_contradiction_clause,[],[f3239]) ).
fof(f3242,plain,
( op2(e20,e20) != h2(op1(e12,e12))
| spl12_56
| ~ spl12_67 ),
inference(forward_demodulation,[],[f719,f763]) ).
fof(f3244,plain,
( op2(e20,e20) != h2(e13)
| spl12_56
| ~ spl12_67
| ~ spl12_169 ),
inference(forward_demodulation,[],[f3242,f1293]) ).
fof(f3246,plain,
( op2(e20,e20) != e21
| spl12_56
| ~ spl12_67
| ~ spl12_125
| ~ spl12_169 ),
inference(forward_demodulation,[],[f3244,f1034]) ).
fof(f3248,plain,
( $false
| spl12_56
| ~ spl12_67
| ~ spl12_125
| ~ spl12_154
| ~ spl12_169 ),
inference(forward_subsumption_resolution,[],[f3246,f1180]) ).
fof(f3249,plain,
( spl12_56
| ~ spl12_67
| ~ spl12_125
| ~ spl12_154
| ~ spl12_169 ),
inference(avatar_contradiction_clause,[],[f3248]) ).
fof(f3250,plain,
( h2(op1(e12,e13)) != op2(h2(e12),e21)
| spl12_55
| ~ spl12_125 ),
inference(forward_demodulation,[],[f715,f1034]) ).
fof(f3252,plain,
( op2(e20,e21) != h2(op1(e12,e13))
| spl12_55
| ~ spl12_67
| ~ spl12_125 ),
inference(forward_demodulation,[],[f3250,f763]) ).
fof(f3254,plain,
( op2(e20,e21) != h2(e10)
| spl12_55
| ~ spl12_67
| ~ spl12_125
| ~ spl12_246 ),
inference(forward_demodulation,[],[f3252,f1719]) ).
fof(f3256,plain,
( e22 != op2(e20,e21)
| spl12_55
| ~ spl12_67
| ~ spl12_124
| ~ spl12_125
| ~ spl12_246 ),
inference(forward_demodulation,[],[f3254,f1029]) ).
fof(f3257,plain,
( $false
| spl12_55
| ~ spl12_67
| ~ spl12_124
| ~ spl12_125
| ~ spl12_229
| ~ spl12_246 ),
inference(forward_subsumption_resolution,[],[f3256,f1615]) ).
fof(f3258,plain,
( spl12_55
| ~ spl12_67
| ~ spl12_124
| ~ spl12_125
| ~ spl12_229
| ~ spl12_246 ),
inference(avatar_contradiction_clause,[],[f3257]) ).
fof(f3260,plain,
( h2(op1(e12,e10)) != op2(h2(e12),e22)
| spl12_58
| ~ spl12_124 ),
inference(forward_demodulation,[],[f727,f1029]) ).
fof(f3262,plain,
( op2(e20,e22) != h2(op1(e12,e10))
| spl12_58
| ~ spl12_67
| ~ spl12_124 ),
inference(forward_demodulation,[],[f3260,f763]) ).
fof(f3264,plain,
( op2(e20,e22) != h2(e12)
| spl12_58
| ~ spl12_67
| ~ spl12_124
| ~ spl12_190 ),
inference(forward_demodulation,[],[f3262,f1404]) ).
fof(f3266,plain,
( e20 != op2(e20,e22)
| spl12_58
| ~ spl12_67
| ~ spl12_124
| ~ spl12_190 ),
inference(forward_demodulation,[],[f3264,f763]) ).
fof(f3267,plain,
( $false
| spl12_58
| ~ spl12_67
| ~ spl12_124
| ~ spl12_167
| ~ spl12_190 ),
inference(forward_subsumption_resolution,[],[f3266,f1273]) ).
fof(f3268,plain,
( spl12_58
| ~ spl12_67
| ~ spl12_124
| ~ spl12_167
| ~ spl12_190 ),
inference(avatar_contradiction_clause,[],[f3267]) ).
fof(f3269,plain,
( h2(op1(e12,e11)) != op2(h2(e12),e23)
| spl12_57
| ~ spl12_119 ),
inference(forward_demodulation,[],[f723,f1004]) ).
fof(f3271,plain,
( op2(e20,e23) != h2(op1(e12,e11))
| spl12_57
| ~ spl12_67
| ~ spl12_119 ),
inference(forward_demodulation,[],[f3269,f763]) ).
fof(f3273,plain,
( op2(e20,e23) != h2(e11)
| spl12_57
| ~ spl12_67
| ~ spl12_119
| ~ spl12_258 ),
inference(forward_demodulation,[],[f3271,f1774]) ).
fof(f3275,plain,
( e23 != op2(e20,e23)
| spl12_57
| ~ spl12_67
| ~ spl12_119
| ~ spl12_258 ),
inference(forward_demodulation,[],[f3273,f1004]) ).
fof(f3277,plain,
( $false
| spl12_57
| ~ spl12_67
| ~ spl12_119
| ~ spl12_199
| ~ spl12_258 ),
inference(forward_subsumption_resolution,[],[f3275,f1477]) ).
fof(f3278,plain,
( spl12_57
| ~ spl12_67
| ~ spl12_119
| ~ spl12_199
| ~ spl12_258 ),
inference(avatar_contradiction_clause,[],[f3277]) ).
fof(f3280,plain,
( h2(op1(e11,e12)) != op2(h2(e11),e20)
| spl12_60
| ~ spl12_67 ),
inference(forward_demodulation,[],[f735,f763]) ).
fof(f3282,plain,
( op2(e23,e20) != h2(op1(e11,e12))
| spl12_60
| ~ spl12_67
| ~ spl12_119 ),
inference(forward_demodulation,[],[f3280,f1004]) ).
fof(f3284,plain,
( op2(e23,e20) != h2(e11)
| spl12_60
| ~ spl12_67
| ~ spl12_119
| ~ spl12_192 ),
inference(forward_demodulation,[],[f3282,f1420]) ).
fof(f3286,plain,
( e23 != op2(e23,e20)
| spl12_60
| ~ spl12_67
| ~ spl12_119
| ~ spl12_192 ),
inference(forward_demodulation,[],[f3284,f1004]) ).
fof(f3287,plain,
( $false
| spl12_60
| ~ spl12_67
| ~ spl12_119
| ~ spl12_156
| ~ spl12_192 ),
inference(forward_subsumption_resolution,[],[f3286,f1189]) ).
fof(f3288,plain,
( spl12_60
| ~ spl12_67
| ~ spl12_119
| ~ spl12_156
| ~ spl12_192 ),
inference(avatar_contradiction_clause,[],[f3287]) ).
fof(f3289,plain,
( h2(op1(e11,e13)) != op2(h2(e11),e21)
| spl12_59
| ~ spl12_125 ),
inference(forward_demodulation,[],[f731,f1034]) ).
fof(f3291,plain,
( op2(e23,e21) != h2(op1(e11,e13))
| spl12_59
| ~ spl12_119
| ~ spl12_125 ),
inference(forward_demodulation,[],[f3289,f1004]) ).
fof(f3293,plain,
( op2(e23,e21) != h2(e12)
| spl12_59
| ~ spl12_119
| ~ spl12_125
| ~ spl12_236 ),
inference(forward_demodulation,[],[f3291,f1675]) ).
fof(f3295,plain,
( e20 != op2(e23,e21)
| spl12_59
| ~ spl12_67
| ~ spl12_119
| ~ spl12_125
| ~ spl12_236 ),
inference(forward_demodulation,[],[f3293,f763]) ).
fof(f3297,plain,
( $false
| spl12_59
| ~ spl12_67
| ~ spl12_119
| ~ spl12_125
| ~ spl12_213
| ~ spl12_236 ),
inference(forward_subsumption_resolution,[],[f3295,f1540]) ).
fof(f3298,plain,
( spl12_59
| ~ spl12_67
| ~ spl12_119
| ~ spl12_125
| ~ spl12_213
| ~ spl12_236 ),
inference(avatar_contradiction_clause,[],[f3297]) ).
fof(f3300,plain,
( h2(op1(e11,e10)) != op2(h2(e11),e22)
| spl12_62
| ~ spl12_124 ),
inference(forward_demodulation,[],[f743,f1029]) ).
fof(f3302,plain,
( op2(e23,e22) != h2(op1(e11,e10))
| spl12_62
| ~ spl12_119
| ~ spl12_124 ),
inference(forward_demodulation,[],[f3300,f1004]) ).
fof(f3304,plain,
( op2(e23,e22) != h2(e10)
| spl12_62
| ~ spl12_119
| ~ spl12_124
| ~ spl12_268 ),
inference(forward_demodulation,[],[f3302,f1824]) ).
fof(f3306,plain,
( e22 != op2(e23,e22)
| spl12_62
| ~ spl12_119
| ~ spl12_124
| ~ spl12_268 ),
inference(forward_demodulation,[],[f3304,f1029]) ).
fof(f3307,plain,
( $false
| spl12_62
| ~ spl12_119
| ~ spl12_124
| ~ spl12_202
| ~ spl12_268 ),
inference(forward_subsumption_resolution,[],[f3306,f1492]) ).
fof(f3308,plain,
( spl12_62
| ~ spl12_119
| ~ spl12_124
| ~ spl12_202
| ~ spl12_268 ),
inference(avatar_contradiction_clause,[],[f3307]) ).
fof(f3309,plain,
( op2(e23,e23) != h2(op1(e11,e11))
| spl12_61
| ~ spl12_119 ),
inference(forward_demodulation,[],[f739,f1004]) ).
fof(f3311,plain,
( op2(e23,e23) != h2(e13)
| spl12_61
| ~ spl12_119
| ~ spl12_171 ),
inference(forward_demodulation,[],[f3309,f1302]) ).
fof(f3313,plain,
( e21 != op2(e23,e23)
| spl12_61
| ~ spl12_119
| ~ spl12_125
| ~ spl12_171 ),
inference(forward_demodulation,[],[f3311,f1034]) ).
fof(f3315,plain,
( $false
| spl12_61
| ~ spl12_119
| ~ spl12_125
| ~ spl12_150
| ~ spl12_171 ),
inference(forward_subsumption_resolution,[],[f3313,f1161]) ).
fof(f3316,plain,
( spl12_61
| ~ spl12_119
| ~ spl12_125
| ~ spl12_150
| ~ spl12_171 ),
inference(avatar_contradiction_clause,[],[f3315]) ).
fof(f3319,plain,
( h2(op1(e10,e12)) != op2(h2(e10),e20)
| spl12_64
| ~ spl12_67 ),
inference(forward_demodulation,[],[f751,f763]) ).
fof(f3321,plain,
( op2(e22,e20) != h2(op1(e10,e12))
| spl12_64
| ~ spl12_67
| ~ spl12_124 ),
inference(forward_demodulation,[],[f3319,f1029]) ).
fof(f3323,plain,
( op2(e22,e20) != h2(e10)
| spl12_64
| ~ spl12_67
| ~ spl12_124
| ~ spl12_195 ),
inference(forward_demodulation,[],[f3321,f1448]) ).
fof(f3324,plain,
( e22 != op2(e22,e20)
| spl12_64
| ~ spl12_67
| ~ spl12_124
| ~ spl12_195 ),
inference(forward_demodulation,[],[f3323,f1029]) ).
fof(f3325,plain,
( $false
| spl12_64
| ~ spl12_67
| ~ spl12_124
| ~ spl12_162
| ~ spl12_195 ),
inference(forward_subsumption_resolution,[],[f3324,f1229]) ).
fof(f3326,plain,
( spl12_64
| ~ spl12_67
| ~ spl12_124
| ~ spl12_162
| ~ spl12_195 ),
inference(avatar_contradiction_clause,[],[f3325]) ).
fof(f3327,plain,
( h2(op1(e10,e13)) != op2(h2(e10),e21)
| spl12_63
| ~ spl12_125 ),
inference(forward_demodulation,[],[f747,f1034]) ).
fof(f3329,plain,
( op2(e22,e21) != h2(op1(e10,e13))
| spl12_63
| ~ spl12_124
| ~ spl12_125 ),
inference(forward_demodulation,[],[f3327,f1029]) ).
fof(f3331,plain,
( op2(e22,e21) != h2(e13)
| spl12_63
| ~ spl12_124
| ~ spl12_125
| ~ spl12_235 ),
inference(forward_demodulation,[],[f3329,f1669]) ).
fof(f3333,plain,
( e21 != op2(e22,e21)
| spl12_63
| ~ spl12_124
| ~ spl12_125
| ~ spl12_235 ),
inference(forward_demodulation,[],[f3331,f1034]) ).
fof(f3335,plain,
( $false
| spl12_63
| ~ spl12_124
| ~ spl12_125
| ~ spl12_222
| ~ spl12_235 ),
inference(forward_subsumption_resolution,[],[f3333,f1582]) ).
fof(f3336,plain,
( spl12_63
| ~ spl12_124
| ~ spl12_125
| ~ spl12_222
| ~ spl12_235 ),
inference(avatar_contradiction_clause,[],[f3335]) ).
fof(f3338,plain,
( op2(e22,e22) != h2(op1(e10,e10))
| spl12_66
| ~ spl12_124 ),
inference(forward_demodulation,[],[f759,f1029]) ).
fof(f3340,plain,
( op2(e22,e22) != h2(e11)
| spl12_66
| ~ spl12_124
| ~ spl12_182 ),
inference(forward_demodulation,[],[f3338,f1355]) ).
fof(f3342,plain,
( e23 != op2(e22,e22)
| spl12_66
| ~ spl12_119
| ~ spl12_124
| ~ spl12_182 ),
inference(forward_demodulation,[],[f3340,f1004]) ).
fof(f3346,plain,
( h2(op1(e10,e11)) != op2(h2(e10),e23)
| spl12_65
| ~ spl12_119 ),
inference(forward_demodulation,[],[f755,f1004]) ).
fof(f3348,plain,
( op2(e22,e23) != h2(op1(e10,e11))
| spl12_65
| ~ spl12_119
| ~ spl12_124 ),
inference(forward_demodulation,[],[f3346,f1029]) ).
fof(f3350,plain,
( op2(e22,e23) != h2(e12)
| spl12_65
| ~ spl12_119
| ~ spl12_124
| ~ spl12_265 ),
inference(forward_demodulation,[],[f3348,f1807]) ).
fof(f3352,plain,
( e20 != op2(e22,e23)
| spl12_65
| ~ spl12_67
| ~ spl12_119
| ~ spl12_124
| ~ spl12_265 ),
inference(forward_demodulation,[],[f3350,f763]) ).
fof(f3353,plain,
( $false
| spl12_65
| ~ spl12_67
| ~ spl12_119
| ~ spl12_124
| ~ spl12_210
| ~ spl12_265 ),
inference(forward_subsumption_resolution,[],[f3352,f1527]) ).
fof(f3354,plain,
( spl12_65
| ~ spl12_67
| ~ spl12_119
| ~ spl12_124
| ~ spl12_210
| ~ spl12_265 ),
inference(avatar_contradiction_clause,[],[f3353]) ).
fof(f3358,plain,
( ~ spl12_232
| spl12_52
| ~ spl12_67
| ~ spl12_125
| ~ spl12_238 ),
inference(avatar_split_clause,[],[f3218,f1682,f1033,f762,f701,f1630]) ).
fof(f3362,plain,
( ~ spl12_228
| ~ spl12_156 ),
inference(avatar_split_clause,[],[f2971,f1188,f1608]) ).
fof(f3373,plain,
( ~ spl12_230
| ~ spl12_162 ),
inference(avatar_split_clause,[],[f2972,f1228,f1618]) ).
fof(f3381,plain,
( ~ spl12_141
| spl12_66
| ~ spl12_119
| ~ spl12_124
| ~ spl12_182 ),
inference(avatar_split_clause,[],[f3342,f1354,f1028,f1003,f757,f1117]) ).
fof(f3386,plain,
( e21 != op2(e22,e22)
| ~ spl12_222 ),
inference(forward_demodulation,[],[f198,f1582]) ).
fof(f3389,plain,
( e20 != op2(e22,e22)
| ~ spl12_167 ),
inference(forward_demodulation,[],[f224,f1273]) ).
fof(f3397,plain,
( ~ spl12_152
| ~ spl12_222 ),
inference(avatar_split_clause,[],[f3386,f1580,f1169]) ).
fof(f3399,plain,
( ~ spl12_157
| ~ spl12_167 ),
inference(avatar_split_clause,[],[f3389,f1272,f1193]) ).
fof(f3407,plain,
( ~ spl12_164
| spl12_54
| ~ spl12_124
| ~ spl12_125
| ~ spl12_184 ),
inference(avatar_split_clause,[],[f3228,f1363,f1033,f1028,f709,f1244]) ).
fof(f3422,plain,
( spl12_229
| ~ spl12_150
| ~ spl12_213 ),
inference(avatar_split_clause,[],[f3207,f1538,f1160,f1613]) ).
cnf(s10,plain,
( spl12_47
| spl12_48
| spl12_49
| ~ spl12_51
| ~ spl12_52
| ~ spl12_53
| ~ spl12_54
| ~ spl12_55
| ~ spl12_56
| ~ spl12_57
| ~ spl12_58
| ~ spl12_59
| ~ spl12_60
| ~ spl12_61
| ~ spl12_62
| ~ spl12_63
| ~ spl12_64
| ~ spl12_65
| ~ spl12_66
| ~ spl12_67 ),
inference(sat_conversion,[],[f765]) ).
cnf(s43,plain,
( ~ spl12_47
| ~ spl12_119 ),
inference(sat_conversion,[],[f1006]) ).
cnf(s48,plain,
( ~ spl12_48
| ~ spl12_124 ),
inference(sat_conversion,[],[f1031]) ).
cnf(s49,plain,
( ~ spl12_49
| ~ spl12_125 ),
inference(sat_conversion,[],[f1036]) ).
cnf(s67,plain,
spl12_125,
inference(sat_conversion,[],[f1114]) ).
cnf(s76,plain,
( ~ spl12_150
| ~ spl12_151 ),
inference(sat_conversion,[],[f1167]) ).
cnf(s86,plain,
( ~ spl12_143
| ~ spl12_160 ),
inference(sat_conversion,[],[f1213]) ).
cnf(s89,plain,
~ spl12_147,
inference(sat_conversion,[],[f1216]) ).
cnf(s92,plain,
( ~ spl12_150
| ~ spl12_161 ),
inference(sat_conversion,[],[f1223]) ).
cnf(s110,plain,
~ spl12_153,
inference(sat_conversion,[],[f1253]) ).
cnf(s118,plain,
( ~ spl12_143
| ~ spl12_166 ),
inference(sat_conversion,[],[f1269]) ).
cnf(s122,plain,
( ~ spl12_148
| ~ spl12_167 ),
inference(sat_conversion,[],[f1277]) ).
cnf(s124,plain,
( ~ spl12_150
| ~ spl12_168 ),
inference(sat_conversion,[],[f1283]) ).
cnf(s131,plain,
~ spl12_159,
inference(sat_conversion,[],[f1290]) ).
cnf(s139,plain,
( ~ spl12_178
| ~ spl12_179 ),
inference(sat_conversion,[],[f1342]) ).
cnf(s149,plain,
( ~ spl12_171
| ~ spl12_188 ),
inference(sat_conversion,[],[f1388]) ).
cnf(s152,plain,
~ spl12_175,
inference(sat_conversion,[],[f1391]) ).
cnf(s155,plain,
( ~ spl12_178
| ~ spl12_189 ),
inference(sat_conversion,[],[f1398]) ).
cnf(s160,plain,
( ~ spl12_185
| ~ spl12_190 ),
inference(sat_conversion,[],[f1407]) ).
cnf(s173,plain,
~ spl12_181,
inference(sat_conversion,[],[f1428]) ).
cnf(s181,plain,
( ~ spl12_171
| ~ spl12_194 ),
inference(sat_conversion,[],[f1444]) ).
cnf(s183,plain,
( ~ spl12_173
| ~ spl12_195 ),
inference(sat_conversion,[],[f1450]) ).
cnf(s187,plain,
( ~ spl12_178
| ~ spl12_196 ),
inference(sat_conversion,[],[f1458]) ).
cnf(s194,plain,
~ spl12_187,
inference(sat_conversion,[],[f1465]) ).
cnf(s196,plain,
( spl12_142
| spl12_146
| spl12_151
| spl12_156 ),
inference(sat_conversion,[],[f1479]) ).
cnf(s201,plain,
( spl12_155
| spl12_166
| spl12_210
| spl12_211 ),
inference(sat_conversion,[],[f1532]) ).
cnf(s205,plain,
( spl12_147
| spl12_202
| spl12_219
| spl12_220 ),
inference(sat_conversion,[],[f1572]) ).
cnf(s206,plain,
( spl12_147
| spl12_160
| spl12_161
| spl12_162 ),
inference(sat_conversion,[],[f1573]) ).
cnf(s207,plain,
( spl12_152
| spl12_164
| spl12_207
| spl12_221 ),
inference(sat_conversion,[],[f1578]) ).
cnf(s211,plain,
( spl12_143
| spl12_151
| spl12_217
| spl12_227 ),
inference(sat_conversion,[],[f1606]) ).
cnf(s214,plain,
( spl12_148
| spl12_200
| spl12_219
| spl12_230 ),
inference(sat_conversion,[],[f1621]) ).
cnf(s215,plain,
( spl12_153
| spl12_208
| spl12_222
| spl12_231 ),
inference(sat_conversion,[],[f1626]) ).
cnf(s220,plain,
( spl12_144
| spl12_199
| spl12_216
| spl12_227 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s224,plain,
( spl12_154
| spl12_206
| spl12_221
| spl12_231 ),
inference(sat_conversion,[],[f1639]) ).
cnf(s226,plain,
( spl12_159
| spl12_166
| spl12_167
| spl12_168 ),
inference(sat_conversion,[],[f1641]) ).
cnf(s232,plain,
( spl12_141
| spl12_147
| spl12_152
| spl12_157 ),
inference(sat_conversion,[],[f1647]) ).
cnf(s238,plain,
( spl12_165
| spl12_228
| spl12_230
| spl12_232 ),
inference(sat_conversion,[],[f1653]) ).
cnf(s245,plain,
( spl12_173
| spl12_188
| spl12_236
| spl12_237 ),
inference(sat_conversion,[],[f1680]) ).
cnf(s253,plain,
( spl12_175
| spl12_238
| spl12_255
| spl12_256 ),
inference(sat_conversion,[],[f1764]) ).
cnf(s254,plain,
( spl12_175
| spl12_188
| spl12_189
| spl12_190 ),
inference(sat_conversion,[],[f1765]) ).
cnf(s255,plain,
( spl12_180
| spl12_192
| spl12_243
| spl12_257 ),
inference(sat_conversion,[],[f1770]) ).
cnf(s258,plain,
( spl12_185
| spl12_246
| spl12_261
| spl12_262 ),
inference(sat_conversion,[],[f1793]) ).
cnf(s259,plain,
( spl12_171
| spl12_179
| spl12_253
| spl12_263 ),
inference(sat_conversion,[],[f1798]) ).
cnf(s263,plain,
( spl12_181
| spl12_244
| spl12_258
| spl12_267 ),
inference(sat_conversion,[],[f1818]) ).
cnf(s268,plain,
( spl12_172
| spl12_235
| spl12_252
| spl12_263 ),
inference(sat_conversion,[],[f1827]) ).
cnf(s272,plain,
( spl12_182
| spl12_242
| spl12_257
| spl12_267 ),
inference(sat_conversion,[],[f1831]) ).
cnf(s273,plain,
( spl12_187
| spl12_250
| spl12_262
| spl12_268 ),
inference(sat_conversion,[],[f1832]) ).
cnf(s274,plain,
( spl12_187
| spl12_194
| spl12_195
| spl12_196 ),
inference(sat_conversion,[],[f1833]) ).
cnf(s278,plain,
( spl12_184
| spl12_240
| spl12_245
| spl12_250 ),
inference(sat_conversion,[],[f1837]) ).
cnf(s280,plain,
( spl12_169
| spl12_175
| spl12_180
| spl12_185 ),
inference(sat_conversion,[],[f1839]) ).
cnf(s291,plain,
spl12_178,
inference(sat_conversion,[],[f1852]) ).
cnf(s292,plain,
spl12_150,
inference(sat_conversion,[],[f1853]) ).
cnf(s293,plain,
~ spl12_142,
inference(sat_conversion,[],[f1854]) ).
cnf(s326,plain,
( ~ spl12_217
| ~ spl12_222 ),
inference(sat_conversion,[],[f2033]) ).
cnf(s338,plain,
( ~ spl12_146
| ~ spl12_202 ),
inference(sat_conversion,[],[f2091]) ).
cnf(s344,plain,
( ~ spl12_164
| ~ spl12_219 ),
inference(sat_conversion,[],[f2125]) ).
cnf(s349,plain,
( ~ spl12_150
| ~ spl12_155 ),
inference(sat_conversion,[],[f2147]) ).
cnf(s352,plain,
( ~ spl12_200
| ~ spl12_211 ),
inference(sat_conversion,[],[f2161]) ).
cnf(s354,plain,
( ~ spl12_167
| ~ spl12_221 ),
inference(sat_conversion,[],[f2168]) ).
cnf(s355,plain,
( ~ spl12_167
| ~ spl12_220 ),
inference(sat_conversion,[],[f2176]) ).
cnf(s356,plain,
( ~ spl12_227
| ~ spl12_229 ),
inference(sat_conversion,[],[f2206]) ).
cnf(s358,plain,
( ~ spl12_167
| ~ spl12_216 ),
inference(sat_conversion,[],[f2212]) ).
cnf(s360,plain,
( ~ spl12_144
| ~ spl12_154 ),
inference(sat_conversion,[],[f2221]) ).
cnf(s381,plain,
( ~ spl12_235
| ~ spl12_237 ),
inference(sat_conversion,[],[f2378]) ).
cnf(s400,plain,
( ~ spl12_195
| ~ spl12_252 ),
inference(sat_conversion,[],[f2460]) ).
cnf(s406,plain,
( ~ spl12_192
| ~ spl12_255 ),
inference(sat_conversion,[],[f2501]) ).
cnf(s415,plain,
( ~ spl12_253
| ~ spl12_258 ),
inference(sat_conversion,[],[f2546]) ).
cnf(s418,plain,
( ~ spl12_263
| ~ spl12_265 ),
inference(sat_conversion,[],[f2562]) ).
cnf(s428,plain,
( spl12_51
| ~ spl12_125
| ~ spl12_178 ),
inference(sat_conversion,[],[f2599]) ).
cnf(s435,plain,
( ~ spl12_150
| spl12_213 ),
inference(sat_conversion,[],[f2771]) ).
cnf(s436,plain,
( ~ spl12_150
| ~ spl12_208 ),
inference(sat_conversion,[],[f2772]) ).
cnf(s437,plain,
( ~ spl12_150
| ~ spl12_206 ),
inference(sat_conversion,[],[f2773]) ).
cnf(s448,plain,
( ~ spl12_51
| spl12_119
| ~ spl12_125
| ~ spl12_143
| ~ spl12_178 ),
inference(sat_conversion,[],[f2799]) ).
cnf(s455,plain,
( ~ spl12_229
| ~ spl12_231 ),
inference(sat_conversion,[],[f2859]) ).
cnf(s458,plain,
( ~ spl12_150
| ~ spl12_207 ),
inference(sat_conversion,[],[f2870]) ).
cnf(s465,plain,
( ~ spl12_164
| ~ spl12_165 ),
inference(sat_conversion,[],[f2883]) ).
cnf(s472,plain,
( ~ spl12_51
| ~ spl12_119
| spl12_124
| ~ spl12_125
| ~ spl12_178
| ~ spl12_200 ),
inference(sat_conversion,[],[f2985]) ).
cnf(s477,plain,
( ~ spl12_178
| ~ spl12_249
| ~ spl12_267 ),
inference(sat_conversion,[],[f3002]) ).
cnf(s478,plain,
( ~ spl12_178
| ~ spl12_249
| spl12_265 ),
inference(sat_conversion,[],[f3004]) ).
cnf(s479,plain,
( ~ spl12_180
| ~ spl12_258 ),
inference(sat_conversion,[],[f3005]) ).
cnf(s480,plain,
( ~ spl12_249
| ~ spl12_261 ),
inference(sat_conversion,[],[f3007]) ).
cnf(s484,plain,
( ~ spl12_178
| ~ spl12_242 ),
inference(sat_conversion,[],[f3013]) ).
cnf(s490,plain,
( ~ spl12_172
| ~ spl12_184 ),
inference(sat_conversion,[],[f3022]) ).
cnf(s491,plain,
( ~ spl12_190
| ~ spl12_262 ),
inference(sat_conversion,[],[f3024]) ).
cnf(s496,plain,
( ~ spl12_178
| ~ spl12_243 ),
inference(sat_conversion,[],[f3033]) ).
cnf(s497,plain,
( ~ spl12_178
| ~ spl12_245 ),
inference(sat_conversion,[],[f3035]) ).
cnf(s498,plain,
( ~ spl12_249
| ~ spl12_250 ),
inference(sat_conversion,[],[f3036]) ).
cnf(s503,plain,
( ~ spl12_178
| ~ spl12_244 ),
inference(sat_conversion,[],[f3043]) ).
cnf(s504,plain,
( ~ spl12_178
| spl12_249 ),
inference(sat_conversion,[],[f3044]) ).
cnf(s513,plain,
( ~ spl12_195
| ~ spl12_256 ),
inference(sat_conversion,[],[f3098]) ).
cnf(s516,plain,
( ~ spl12_238
| ~ spl12_240 ),
inference(sat_conversion,[],[f3102]) ).
cnf(s517,plain,
( ~ spl12_195
| ~ spl12_257 ),
inference(sat_conversion,[],[f3118]) ).
cnf(s521,plain,
( ~ spl12_51
| spl12_67
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178
| ~ spl12_200
| ~ spl12_210 ),
inference(sat_conversion,[],[f3217]) ).
cnf(s524,plain,
( spl12_53
| ~ spl12_119
| ~ spl12_124
| ~ spl12_125
| ~ spl12_200
| ~ spl12_249 ),
inference(sat_conversion,[],[f3240]) ).
cnf(s525,plain,
( spl12_56
| ~ spl12_67
| ~ spl12_125
| ~ spl12_154
| ~ spl12_169 ),
inference(sat_conversion,[],[f3249]) ).
cnf(s526,plain,
( spl12_55
| ~ spl12_67
| ~ spl12_124
| ~ spl12_125
| ~ spl12_229
| ~ spl12_246 ),
inference(sat_conversion,[],[f3258]) ).
cnf(s527,plain,
( spl12_58
| ~ spl12_67
| ~ spl12_124
| ~ spl12_167
| ~ spl12_190 ),
inference(sat_conversion,[],[f3268]) ).
cnf(s528,plain,
( spl12_57
| ~ spl12_67
| ~ spl12_119
| ~ spl12_199
| ~ spl12_258 ),
inference(sat_conversion,[],[f3278]) ).
cnf(s529,plain,
( spl12_60
| ~ spl12_67
| ~ spl12_119
| ~ spl12_156
| ~ spl12_192 ),
inference(sat_conversion,[],[f3288]) ).
cnf(s530,plain,
( spl12_59
| ~ spl12_67
| ~ spl12_119
| ~ spl12_125
| ~ spl12_213
| ~ spl12_236 ),
inference(sat_conversion,[],[f3298]) ).
cnf(s531,plain,
( spl12_62
| ~ spl12_119
| ~ spl12_124
| ~ spl12_202
| ~ spl12_268 ),
inference(sat_conversion,[],[f3308]) ).
cnf(s532,plain,
( spl12_61
| ~ spl12_119
| ~ spl12_125
| ~ spl12_150
| ~ spl12_171 ),
inference(sat_conversion,[],[f3316]) ).
cnf(s533,plain,
( spl12_64
| ~ spl12_67
| ~ spl12_124
| ~ spl12_162
| ~ spl12_195 ),
inference(sat_conversion,[],[f3326]) ).
cnf(s534,plain,
( spl12_63
| ~ spl12_124
| ~ spl12_125
| ~ spl12_222
| ~ spl12_235 ),
inference(sat_conversion,[],[f3336]) ).
cnf(s536,plain,
( spl12_65
| ~ spl12_67
| ~ spl12_119
| ~ spl12_124
| ~ spl12_210
| ~ spl12_265 ),
inference(sat_conversion,[],[f3354]) ).
cnf(s537,plain,
( spl12_52
| ~ spl12_67
| ~ spl12_125
| ~ spl12_232
| ~ spl12_238 ),
inference(sat_conversion,[],[f3358]) ).
cnf(s539,plain,
( ~ spl12_156
| ~ spl12_228 ),
inference(sat_conversion,[],[f3362]) ).
cnf(s544,plain,
( ~ spl12_162
| ~ spl12_230 ),
inference(sat_conversion,[],[f3373]) ).
cnf(s546,plain,
( spl12_66
| ~ spl12_119
| ~ spl12_124
| ~ spl12_141
| ~ spl12_182 ),
inference(sat_conversion,[],[f3381]) ).
cnf(s550,plain,
( ~ spl12_152
| ~ spl12_222 ),
inference(sat_conversion,[],[f3397]) ).
cnf(s552,plain,
( ~ spl12_157
| ~ spl12_167 ),
inference(sat_conversion,[],[f3399]) ).
cnf(s558,plain,
( spl12_54
| ~ spl12_124
| ~ spl12_125
| ~ spl12_164
| ~ spl12_184 ),
inference(sat_conversion,[],[f3407]) ).
cnf(s568,plain,
( ~ spl12_150
| ~ spl12_213
| spl12_229 ),
inference(sat_conversion,[],[f3422]) ).
cnf(s590,plain,
~ spl12_207,
inference(rat,[],[s458,s292]) ).
cnf(s592,plain,
~ spl12_206,
inference(rat,[],[s437,s292]) ).
cnf(s593,plain,
~ spl12_208,
inference(rat,[],[s436,s292]) ).
cnf(s594,plain,
spl12_213,
inference(rat,[],[s435,s292]) ).
cnf(s596,plain,
~ spl12_155,
inference(rat,[],[s349,s292]) ).
cnf(s599,plain,
spl12_229,
inference(rat,[],[s568,s292,s594]) ).
cnf(s603,plain,
~ spl12_231,
inference(rat,[],[s455,s599]) ).
cnf(s604,plain,
~ spl12_227,
inference(rat,[],[s356,s599]) ).
cnf(s605,plain,
spl12_249,
inference(rat,[],[s504,s291]) ).
cnf(s606,plain,
~ spl12_244,
inference(rat,[],[s503,s291]) ).
cnf(s607,plain,
~ spl12_245,
inference(rat,[],[s497,s291]) ).
cnf(s608,plain,
~ spl12_243,
inference(rat,[],[s496,s291]) ).
cnf(s610,plain,
~ spl12_242,
inference(rat,[],[s484,s291]) ).
cnf(s613,plain,
~ spl12_250,
inference(rat,[],[s498,s605]) ).
cnf(s615,plain,
~ spl12_261,
inference(rat,[],[s480,s605]) ).
cnf(s616,plain,
spl12_265,
inference(rat,[],[s478,s291,s605]) ).
cnf(s617,plain,
~ spl12_267,
inference(rat,[],[s477,s291,s605]) ).
cnf(s618,plain,
~ spl12_263,
inference(rat,[],[s418,s616]) ).
cnf(s623,plain,
( spl12_184
| spl12_240 ),
inference(rat,[],[s278,s613,s607]) ).
cnf(s625,plain,
( spl12_187
| spl12_262
| spl12_268 ),
inference(rat,[],[s273,s613]) ).
cnf(s626,plain,
( spl12_182
| spl12_257 ),
inference(rat,[],[s272,s617,s610]) ).
cnf(s628,plain,
( spl12_172
| spl12_235
| spl12_252 ),
inference(rat,[],[s268,s618]) ).
cnf(s630,plain,
( spl12_181
| spl12_258 ),
inference(rat,[],[s263,s617,s606]) ).
cnf(s631,plain,
( spl12_171
| spl12_179
| spl12_253 ),
inference(rat,[],[s259,s618]) ).
cnf(s632,plain,
( spl12_185
| spl12_246
| spl12_262 ),
inference(rat,[],[s258,s615]) ).
cnf(s635,plain,
( spl12_180
| spl12_192
| spl12_257 ),
inference(rat,[],[s255,s608]) ).
cnf(s643,plain,
( spl12_154
| spl12_221 ),
inference(rat,[],[s224,s603,s592]) ).
cnf(s644,plain,
( spl12_144
| spl12_199
| spl12_216 ),
inference(rat,[],[s220,s604]) ).
cnf(s645,plain,
( spl12_153
| spl12_222 ),
inference(rat,[],[s215,s603,s593]) ).
cnf(s646,plain,
( spl12_143
| spl12_151
| spl12_217 ),
inference(rat,[],[s211,s604]) ).
cnf(s650,plain,
( spl12_152
| spl12_164
| spl12_221 ),
inference(rat,[],[s207,s590]) ).
cnf(s651,plain,
( spl12_166
| spl12_210
| spl12_211 ),
inference(rat,[],[s201,s596]) ).
cnf(s654,plain,
( spl12_146
| spl12_151
| spl12_156 ),
inference(rat,[],[s196,s293]) ).
cnf(s656,plain,
~ spl12_196,
inference(rat,[],[s187,s291]) ).
cnf(s657,plain,
spl12_258,
inference(rat,[],[s630,s173]) ).
cnf(s658,plain,
~ spl12_180,
inference(rat,[],[s479,s657]) ).
cnf(s659,plain,
~ spl12_253,
inference(rat,[],[s415,s657]) ).
cnf(s660,plain,
~ spl12_189,
inference(rat,[],[s155,s291]) ).
cnf(s661,plain,
~ spl12_179,
inference(rat,[],[s139,s291]) ).
cnf(s662,plain,
spl12_171,
inference(rat,[],[s631,s659,s661]) ).
cnf(s663,plain,
~ spl12_194,
inference(rat,[],[s181,s662]) ).
cnf(s665,plain,
~ spl12_188,
inference(rat,[],[s149,s662]) ).
cnf(s666,plain,
spl12_195,
inference(rat,[],[s274,s656,s194,s663]) ).
cnf(s667,plain,
spl12_190,
inference(rat,[],[s254,s152,s660,s665]) ).
cnf(s668,plain,
~ spl12_257,
inference(rat,[],[s517,s666]) ).
cnf(s669,plain,
~ spl12_256,
inference(rat,[],[s513,s666]) ).
cnf(s671,plain,
~ spl12_252,
inference(rat,[],[s400,s666]) ).
cnf(s674,plain,
~ spl12_173,
inference(rat,[],[s183,s666]) ).
cnf(s676,plain,
~ spl12_262,
inference(rat,[],[s491,s667]) ).
cnf(s677,plain,
~ spl12_185,
inference(rat,[],[s160,s667]) ).
cnf(s679,plain,
spl12_182,
inference(rat,[],[s626,s668]) ).
cnf(s680,plain,
spl12_192,
inference(rat,[],[s635,s658,s668]) ).
cnf(s681,plain,
spl12_268,
inference(rat,[],[s625,s194,s676]) ).
cnf(s682,plain,
spl12_246,
inference(rat,[],[s632,s676,s677]) ).
cnf(s683,plain,
spl12_169,
inference(rat,[],[s280,s152,s658,s677]) ).
cnf(s685,plain,
~ spl12_255,
inference(rat,[],[s406,s680]) ).
cnf(s688,plain,
spl12_238,
inference(rat,[],[s253,s669,s152,s685]) ).
cnf(s689,plain,
~ spl12_240,
inference(rat,[],[s516,s688]) ).
cnf(s691,plain,
spl12_184,
inference(rat,[],[s623,s689]) ).
cnf(s693,plain,
~ spl12_172,
inference(rat,[],[s490,s691]) ).
cnf(s694,plain,
spl12_235,
inference(rat,[],[s628,s671,s693]) ).
cnf(s695,plain,
~ spl12_237,
inference(rat,[],[s381,s694]) ).
cnf(s696,plain,
spl12_236,
inference(rat,[],[s245,s674,s665,s695]) ).
cnf(s699,plain,
~ spl12_168,
inference(rat,[],[s124,s292]) ).
cnf(s700,plain,
spl12_222,
inference(rat,[],[s645,s110]) ).
cnf(s701,plain,
~ spl12_152,
inference(rat,[],[s550,s700]) ).
cnf(s702,plain,
~ spl12_217,
inference(rat,[],[s326,s700]) ).
cnf(s703,plain,
~ spl12_161,
inference(rat,[],[s92,s292]) ).
cnf(s704,plain,
~ spl12_151,
inference(rat,[],[s76,s292]) ).
cnf(s705,plain,
spl12_143,
inference(rat,[],[s646,s702,s704]) ).
cnf(s707,plain,
~ spl12_166,
inference(rat,[],[s118,s705]) ).
cnf(s709,plain,
~ spl12_160,
inference(rat,[],[s86,s705]) ).
cnf(s710,plain,
spl12_167,
inference(rat,[],[s226,s699,s131,s707]) ).
cnf(s711,plain,
spl12_162,
inference(rat,[],[s206,s89,s703,s709]) ).
cnf(s712,plain,
~ spl12_157,
inference(rat,[],[s552,s710]) ).
cnf(s713,plain,
~ spl12_216,
inference(rat,[],[s358,s710]) ).
cnf(s714,plain,
~ spl12_220,
inference(rat,[],[s355,s710]) ).
cnf(s715,plain,
~ spl12_221,
inference(rat,[],[s354,s710]) ).
cnf(s717,plain,
~ spl12_148,
inference(rat,[],[s122,s710]) ).
cnf(s718,plain,
~ spl12_230,
inference(rat,[],[s544,s711]) ).
cnf(s723,plain,
spl12_141,
inference(rat,[],[s232,s89,s701,s712]) ).
cnf(s724,plain,
spl12_154,
inference(rat,[],[s643,s715]) ).
cnf(s725,plain,
spl12_164,
inference(rat,[],[s650,s701,s715]) ).
cnf(s730,plain,
~ spl12_144,
inference(rat,[],[s360,s724]) ).
cnf(s731,plain,
~ spl12_165,
inference(rat,[],[s465,s725]) ).
cnf(s732,plain,
~ spl12_219,
inference(rat,[],[s344,s725]) ).
cnf(s733,plain,
spl12_199,
inference(rat,[],[s644,s713,s730]) ).
cnf(s734,plain,
spl12_202,
inference(rat,[],[s205,s714,s89,s732]) ).
cnf(s735,plain,
spl12_200,
inference(rat,[],[s214,s718,s717,s732]) ).
cnf(s737,plain,
~ spl12_146,
inference(rat,[],[s338,s734]) ).
cnf(s738,plain,
~ spl12_211,
inference(rat,[],[s352,s735]) ).
cnf(s739,plain,
spl12_156,
inference(rat,[],[s654,s704,s737]) ).
cnf(s740,plain,
spl12_210,
inference(rat,[],[s651,s707,s738]) ).
cnf(s741,plain,
~ spl12_228,
inference(rat,[],[s539,s739]) ).
cnf(s746,plain,
spl12_232,
inference(rat,[],[s238,s731,s718,s741]) ).
cnf(s751,plain,
spl12_51,
inference(rat,[],[s428,s291,s67]) ).
cnf(s752,plain,
spl12_119,
inference(rat,[],[s448,s291,s705,s67,s751]) ).
cnf(s755,plain,
spl12_61,
inference(rat,[],[s532,s662,s292,s67,s752]) ).
cnf(s756,plain,
spl12_124,
inference(rat,[],[s472,s735,s291,s67,s751,s752]) ).
cnf(s757,plain,
spl12_67,
inference(rat,[],[s521,s740,s735,s291,s67,s751,s752]) ).
cnf(s758,plain,
spl12_54,
inference(rat,[],[s558,s691,s725,s67,s756]) ).
cnf(s759,plain,
spl12_63,
inference(rat,[],[s534,s694,s700,s67,s756]) ).
cnf(s760,plain,
spl12_66,
inference(rat,[],[s546,s679,s723,s752,s756]) ).
cnf(s761,plain,
spl12_62,
inference(rat,[],[s531,s681,s734,s752,s756]) ).
cnf(s762,plain,
spl12_53,
inference(rat,[],[s524,s605,s735,s67,s752,s756]) ).
cnf(s763,plain,
spl12_52,
inference(rat,[],[s537,s688,s746,s67,s757]) ).
cnf(s764,plain,
spl12_65,
inference(rat,[],[s536,s616,s740,s756,s752,s757]) ).
cnf(s765,plain,
spl12_64,
inference(rat,[],[s533,s666,s711,s756,s757]) ).
cnf(s766,plain,
spl12_59,
inference(rat,[],[s530,s696,s594,s67,s752,s757]) ).
cnf(s767,plain,
spl12_60,
inference(rat,[],[s529,s680,s739,s752,s757]) ).
cnf(s768,plain,
spl12_57,
inference(rat,[],[s528,s657,s733,s752,s757]) ).
cnf(s769,plain,
spl12_58,
inference(rat,[],[s527,s667,s710,s756,s757]) ).
cnf(s770,plain,
spl12_55,
inference(rat,[],[s526,s682,s599,s67,s756,s757]) ).
cnf(s771,plain,
spl12_56,
inference(rat,[],[s525,s683,s724,s67,s757]) ).
cnf(s774,plain,
~ spl12_49,
inference(rat,[],[s49,s67]) ).
cnf(s775,plain,
~ spl12_48,
inference(rat,[],[s48,s756]) ).
cnf(s776,plain,
~ spl12_47,
inference(rat,[],[s43,s752]) ).
cnf(s785,plain,
$false,
inference(rat,[],[s10,s757,s760,s764,s765,s759,s761,s755,s767,s766,s769,s768,s771,s770,s758,s762,s763,s751,s774,s775,s776]) ).
fof(f3463,plain,
$false,
inference(avatar_sat_refutation,[],[s785]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG111+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.10/0.21 % Computer : n020.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Mon Sep 28 19:30:20 UTC 2026
% 0.10/0.21 % CPUTime :
% 0.10/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.24 Running first-order theorem proving
% 0.10/0.24 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.23/1.15 % (452493)Detected formulas, will run a generic FOF schedule.
% 3.23/1.15 % (452500)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=3000464089:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.23/1.15 % (452498)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=1680716199:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.23/1.15 % (452502)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=458720324:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.23/1.15 % (452503)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=239999364:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.23/1.15 % (452499)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=3951503230:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.23/1.15 % (452501)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=268759080:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.23/1.15 % (452504)dis-21_1_sil=8000:lcm=predicate:random_seed=829839908: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.23/1.15 % (452504)Refutation not found, incomplete strategy
% 3.23/1.15 % (452504)------------------------------
% 3.23/1.15 % (452504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.15 % (452504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.15 % (452504)CaDiCaL version: 2.1.3
% 3.23/1.15 % (452504)Termination reason: Refutation not found, incomplete strategy
% 3.23/1.15 % (452504)Time elapsed: 0.018 s
% 3.23/1.15 % (452504)Peak memory usage: 89 MB
% 3.23/1.15 % (452504)Instructions burned: 37 (million)
% 3.23/1.15 % (452502)Instruction limit reached!
% 3.23/1.15 % (452502)------------------------------
% 3.23/1.15 % (452502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.15 % (452502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.15 % (452502)CaDiCaL version: 2.1.3
% 3.23/1.15 % (452502)Termination reason: Instruction limit
% 3.23/1.15 % (452502)Termination phase: Saturation
% 3.23/1.15 % (452502)Time elapsed: 0.048 s
% 3.23/1.15 % (452502)Peak memory usage: 88 MB
% 3.23/1.15 % (452502)Instructions burned: 120 (million)
% 3.23/1.15 % (452501)Instruction limit reached!
% 3.23/1.15 % (452501)------------------------------
% 3.23/1.15 % (452501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.15 % (452501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.15 % (452501)CaDiCaL version: 2.1.3
% 3.23/1.15 % (452501)Termination reason: Instruction limit
% 3.23/1.15 % (452501)Termination phase: Saturation
% 3.23/1.15 % (452501)Time elapsed: 0.049 s
% 3.23/1.15 % (452501)Peak memory usage: 90 MB
% 3.23/1.15 % (452501)Instructions burned: 109 (million)
% 3.23/1.15 % (452503)First to succeed.
% 3.23/1.15 % (452503)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-452493"
% 3.23/1.15 [W928 19:30:21.729257930 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.23/1.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.23/1.15 [W928 19:30:21.729282985 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.23/1.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.23/1.15 [W928 19:30:21.729303636 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.23/1.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.23/1.15 [W928 19:30:21.729313309 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.23/1.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.23/1.15 [W928 19:30:21.729327592 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.23/1.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.23/1.15 [W928 19:30:21.729335464 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.23/1.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.23/1.15 % (452513)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1312122203:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.23/1.15 % (452512)lrs+10_1_sil=8000:sp=occurrence:random_seed=926805725:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.23/1.15 % (452512)Also succeeded, but the first one will report.
% 3.23/1.15 % (452513)Also succeeded, but the first one will report.
% 3.23/1.15 % (452504)------------------------------
% 3.23/1.15 % (452504)------------------------------
% 3.23/1.15 % (452503)Refutation found. Thanks to Tanya!
% 3.23/1.15 % SZS status Theorem for theBenchmark
% 3.23/1.15 % SZS output start Proof for theBenchmark
% See solution above
% 3.96/1.34 % (452503)------------------------------
% 3.96/1.34 % (452503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.34 % (452503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.34 % (452503)CaDiCaL version: 2.1.3
% 3.96/1.34 % (452503)Termination reason: Refutation
% 3.96/1.34 % (452503)Time elapsed: 0.066 s
% 3.96/1.34 % (452503)Peak memory usage: 91 MB
% 3.96/1.34 % (452503)Instructions burned: 130 (million)
% 3.96/1.34 % (452503)------------------------------
% 3.96/1.34 % (452503)------------------------------
% 3.96/1.34 % (452493)Success in time 0.479 s
% 3.96/1.34 % Vampire exiting
%------------------------------------------------------------------------------