%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG111+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:22:47 AM UTC 2026
% Result : Theorem 0.19s 0.37s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 140
% Syntax : Number of formulae : 817 ( 172 unt; 126 def)
% Number of atoms : 3319 (1796 equ)
% Maximal formula atoms : 128 ( 4 avg)
% Number of connectives : 4236 (1734 ~;1796 |; 592 &)
% ( 114 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 66 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 128 ( 126 usr; 127 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e10) = e11
| op1(e10,e10) = e12
| op1(e10,e10) = e13 )
& ( op1(e10,e11) = e10
| op1(e10,e11) = e11
| op1(e10,e11) = e12
| op1(e10,e11) = e13 )
& ( op1(e10,e12) = e10
| op1(e10,e12) = e11
| op1(e10,e12) = e12
| op1(e10,e12) = e13 )
& ( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e12
| op1(e10,e13) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 )
& ( op1(e11,e11) = e10
| op1(e11,e11) = e11
| op1(e11,e11) = e12
| op1(e11,e11) = e13 )
& ( op1(e11,e12) = e10
| op1(e11,e12) = e11
| op1(e11,e12) = e12
| op1(e11,e12) = e13 )
& ( op1(e11,e13) = e10
| op1(e11,e13) = e11
| op1(e11,e13) = e12
| op1(e11,e13) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e10) = e11
| op1(e12,e10) = e12
| op1(e12,e10) = e13 )
& ( op1(e12,e11) = e10
| op1(e12,e11) = e11
| op1(e12,e11) = e12
| op1(e12,e11) = e13 )
& ( op1(e12,e12) = e10
| op1(e12,e12) = e11
| op1(e12,e12) = e12
| op1(e12,e12) = e13 )
& ( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12
| op1(e12,e13) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e10) = e11
| op1(e13,e10) = e12
| op1(e13,e10) = e13 )
& ( op1(e13,e11) = e10
| op1(e13,e11) = e11
| op1(e13,e11) = e12
| op1(e13,e11) = e13 )
& ( op1(e13,e12) = e10
| op1(e13,e12) = e11
| op1(e13,e12) = e12
| op1(e13,e12) = e13 )
& ( op1(e13,e13) = e10
| op1(e13,e13) = e11
| op1(e13,e13) = e12
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e11) = e10
| op1(e10,e12) = e10
| op1(e10,e13) = e10 )
& ( op1(e10,e10) = e10
| op1(e11,e10) = e10
| op1(e12,e10) = e10
| op1(e13,e10) = e10 )
& ( op1(e10,e10) = e11
| op1(e10,e11) = e11
| op1(e10,e12) = e11
| op1(e10,e13) = e11 )
& ( op1(e10,e10) = e11
| op1(e11,e10) = e11
| op1(e12,e10) = e11
| op1(e13,e10) = e11 )
& ( op1(e10,e10) = e12
| op1(e10,e11) = e12
| op1(e10,e12) = e12
| op1(e10,e13) = e12 )
& ( op1(e10,e10) = e12
| op1(e11,e10) = e12
| op1(e12,e10) = e12
| op1(e13,e10) = e12 )
& ( op1(e10,e10) = e13
| op1(e10,e11) = e13
| op1(e10,e12) = e13
| op1(e10,e13) = e13 )
& ( op1(e10,e10) = e13
| op1(e11,e10) = e13
| op1(e12,e10) = e13
| op1(e13,e10) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e11) = e10
| op1(e11,e12) = e10
| op1(e11,e13) = e10 )
& ( op1(e10,e11) = e10
| op1(e11,e11) = e10
| op1(e12,e11) = e10
| op1(e13,e11) = e10 )
& ( op1(e11,e10) = e11
| op1(e11,e11) = e11
| op1(e11,e12) = e11
| op1(e11,e13) = e11 )
& ( op1(e10,e11) = e11
| op1(e11,e11) = e11
| op1(e12,e11) = e11
| op1(e13,e11) = e11 )
& ( op1(e11,e10) = e12
| op1(e11,e11) = e12
| op1(e11,e12) = e12
| op1(e11,e13) = e12 )
& ( op1(e10,e11) = e12
| op1(e11,e11) = e12
| op1(e12,e11) = e12
| op1(e13,e11) = e12 )
& ( op1(e11,e10) = e13
| op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e11,e13) = e13 )
& ( op1(e10,e11) = e13
| op1(e11,e11) = e13
| op1(e12,e11) = e13
| op1(e13,e11) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e11) = e10
| op1(e12,e12) = e10
| op1(e12,e13) = e10 )
& ( op1(e10,e12) = e10
| op1(e11,e12) = e10
| op1(e12,e12) = e10
| op1(e13,e12) = e10 )
& ( op1(e12,e10) = e11
| op1(e12,e11) = e11
| op1(e12,e12) = e11
| op1(e12,e13) = e11 )
& ( op1(e10,e12) = e11
| op1(e11,e12) = e11
| op1(e12,e12) = e11
| op1(e13,e12) = e11 )
& ( op1(e12,e10) = e12
| op1(e12,e11) = e12
| op1(e12,e12) = e12
| op1(e12,e13) = e12 )
& ( op1(e10,e12) = e12
| op1(e11,e12) = e12
| op1(e12,e12) = e12
| op1(e13,e12) = e12 )
& ( op1(e12,e10) = e13
| op1(e12,e11) = e13
| op1(e12,e12) = e13
| op1(e12,e13) = e13 )
& ( op1(e10,e12) = e13
| op1(e11,e12) = e13
| op1(e12,e12) = e13
| op1(e13,e12) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10 )
& ( op1(e10,e13) = e10
| op1(e11,e13) = e10
| op1(e12,e13) = e10
| op1(e13,e13) = e10 )
& ( op1(e13,e10) = e11
| op1(e13,e11) = e11
| op1(e13,e12) = e11
| op1(e13,e13) = e11 )
& ( op1(e10,e13) = e11
| op1(e11,e13) = e11
| op1(e12,e13) = e11
| op1(e13,e13) = e11 )
& ( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12
| op1(e13,e13) = e12 )
& ( op1(e10,e13) = e12
| op1(e11,e13) = e12
| op1(e12,e13) = e12
| op1(e13,e13) = e12 )
& ( op1(e13,e10) = e13
| op1(e13,e11) = e13
| op1(e13,e12) = e13
| op1(e13,e13) = e13 )
& ( op1(e10,e13) = e13
| op1(e11,e13) = e13
| op1(e12,e13) = e13
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e20) = e21
| op2(e20,e20) = e22
| op2(e20,e20) = e23 )
& ( op2(e20,e21) = e20
| op2(e20,e21) = e21
| op2(e20,e21) = e22
| op2(e20,e21) = e23 )
& ( op2(e20,e22) = e20
| op2(e20,e22) = e21
| op2(e20,e22) = e22
| op2(e20,e22) = e23 )
& ( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22
| op2(e20,e23) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e20) = e21
| op2(e21,e20) = e22
| op2(e21,e20) = e23 )
& ( op2(e21,e21) = e20
| op2(e21,e21) = e21
| op2(e21,e21) = e22
| op2(e21,e21) = e23 )
& ( op2(e21,e22) = e20
| op2(e21,e22) = e21
| op2(e21,e22) = e22
| op2(e21,e22) = e23 )
& ( op2(e21,e23) = e20
| op2(e21,e23) = e21
| op2(e21,e23) = e22
| op2(e21,e23) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e20) = e21
| op2(e22,e20) = e22
| op2(e22,e20) = e23 )
& ( op2(e22,e21) = e20
| op2(e22,e21) = e21
| op2(e22,e21) = e22
| op2(e22,e21) = e23 )
& ( op2(e22,e22) = e20
| op2(e22,e22) = e21
| op2(e22,e22) = e22
| op2(e22,e22) = e23 )
& ( op2(e22,e23) = e20
| op2(e22,e23) = e21
| op2(e22,e23) = e22
| op2(e22,e23) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e20) = e21
| op2(e23,e20) = e22
| op2(e23,e20) = e23 )
& ( op2(e23,e21) = e20
| op2(e23,e21) = e21
| op2(e23,e21) = e22
| op2(e23,e21) = e23 )
& ( op2(e23,e22) = e20
| op2(e23,e22) = e21
| op2(e23,e22) = e22
| op2(e23,e22) = e23 )
& ( op2(e23,e23) = e20
| op2(e23,e23) = e21
| op2(e23,e23) = e22
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e22) = e20
| op2(e20,e23) = e20 )
& ( op2(e20,e20) = e20
| op2(e21,e20) = e20
| op2(e22,e20) = e20
| op2(e23,e20) = e20 )
& ( op2(e20,e20) = e21
| op2(e20,e21) = e21
| op2(e20,e22) = e21
| op2(e20,e23) = e21 )
& ( op2(e20,e20) = e21
| op2(e21,e20) = e21
| op2(e22,e20) = e21
| op2(e23,e20) = e21 )
& ( op2(e20,e20) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 )
& ( op2(e20,e20) = e22
| op2(e21,e20) = e22
| op2(e22,e20) = e22
| op2(e23,e20) = e22 )
& ( op2(e20,e20) = e23
| op2(e20,e21) = e23
| op2(e20,e22) = e23
| op2(e20,e23) = e23 )
& ( op2(e20,e20) = e23
| op2(e21,e20) = e23
| op2(e22,e20) = e23
| op2(e23,e20) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e21) = e20
| op2(e21,e22) = e20
| op2(e21,e23) = e20 )
& ( op2(e20,e21) = e20
| op2(e21,e21) = e20
| op2(e22,e21) = e20
| op2(e23,e21) = e20 )
& ( op2(e21,e20) = e21
| op2(e21,e21) = e21
| op2(e21,e22) = e21
| op2(e21,e23) = e21 )
& ( op2(e20,e21) = e21
| op2(e21,e21) = e21
| op2(e22,e21) = e21
| op2(e23,e21) = e21 )
& ( op2(e21,e20) = e22
| op2(e21,e21) = e22
| op2(e21,e22) = e22
| op2(e21,e23) = e22 )
& ( op2(e20,e21) = e22
| op2(e21,e21) = e22
| op2(e22,e21) = e22
| op2(e23,e21) = e22 )
& ( op2(e21,e20) = e23
| op2(e21,e21) = e23
| op2(e21,e22) = e23
| op2(e21,e23) = e23 )
& ( op2(e20,e21) = e23
| op2(e21,e21) = e23
| op2(e22,e21) = e23
| op2(e23,e21) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e21) = e20
| op2(e22,e22) = e20
| op2(e22,e23) = e20 )
& ( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e22,e22) = e20
| op2(e23,e22) = e20 )
& ( op2(e22,e20) = e21
| op2(e22,e21) = e21
| op2(e22,e22) = e21
| op2(e22,e23) = e21 )
& ( op2(e20,e22) = e21
| op2(e21,e22) = e21
| op2(e22,e22) = e21
| op2(e23,e22) = e21 )
& ( op2(e22,e20) = e22
| op2(e22,e21) = e22
| op2(e22,e22) = e22
| op2(e22,e23) = e22 )
& ( op2(e20,e22) = e22
| op2(e21,e22) = e22
| op2(e22,e22) = e22
| op2(e23,e22) = e22 )
& ( op2(e22,e20) = e23
| op2(e22,e21) = e23
| op2(e22,e22) = e23
| op2(e22,e23) = e23 )
& ( op2(e20,e22) = e23
| op2(e21,e22) = e23
| op2(e22,e22) = e23
| op2(e23,e22) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e23) = e20 )
& ( op2(e20,e23) = e20
| op2(e21,e23) = e20
| op2(e22,e23) = e20
| op2(e23,e23) = e20 )
& ( op2(e23,e20) = e21
| op2(e23,e21) = e21
| op2(e23,e22) = e21
| op2(e23,e23) = e21 )
& ( op2(e20,e23) = e21
| op2(e21,e23) = e21
| op2(e22,e23) = e21
| op2(e23,e23) = e21 )
& ( op2(e23,e20) = e22
| op2(e23,e21) = e22
| op2(e23,e22) = e22
| op2(e23,e23) = e22 )
& ( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22
| op2(e23,e23) = e22 )
& ( op2(e23,e20) = e23
| op2(e23,e21) = e23
| op2(e23,e22) = e23
| op2(e23,e23) = e23 )
& ( op2(e20,e23) = e23
| op2(e21,e23) = e23
| op2(e22,e23) = e23
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op1(e10,e10) != op1(e11,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e12,e10) != op1(e13,e10)
& op1(e10,e11) != op1(e11,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e12,e11) != op1(e13,e11)
& op1(e10,e12) != op1(e11,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e12,e12) != op1(e13,e12)
& op1(e10,e13) != op1(e11,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e12,e13) != op1(e13,e13)
& op1(e10,e10) != op1(e10,e11)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e12) != op1(e10,e13)
& op1(e11,e10) != op1(e11,e11)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e12) != op1(e11,e13)
& op1(e12,e10) != op1(e12,e11)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e12) != op1(e12,e13)
& op1(e13,e10) != op1(e13,e11)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e12) != op1(e13,e13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( op2(e20,e20) != op2(e21,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e22,e20) != op2(e23,e20)
& op2(e20,e21) != op2(e21,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e22,e21) != op2(e23,e21)
& op2(e20,e22) != op2(e21,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e22,e22) != op2(e23,e22)
& op2(e20,e23) != op2(e21,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e22,e23) != op2(e23,e23)
& op2(e20,e20) != op2(e20,e21)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e22) != op2(e20,e23)
& op2(e21,e20) != op2(e21,e21)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e22) != op2(e21,e23)
& op2(e22,e20) != op2(e22,e21)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e22) != op2(e22,e23)
& op2(e23,e20) != op2(e23,e21)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e22) != op2(e23,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f10,axiom,
( ( op1(e10,e10) != e10
| op1(e10,e10) != e10 )
& ( op1(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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f19,negated_conjecture,
~ ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f20,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) ) )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) ) )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) ) )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) ) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f21,definition,
( ( 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(f51,plain,
( e10 = op1(e12,e12)
| e11 = op1(e12,e12)
| e12 = op1(e12,e12)
| e13 = op1(e12,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f54,plain,
( e10 = op1(e11,e13)
| e11 = op1(e11,e13)
| e12 = op1(e11,e13)
| e13 = op1(e11,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f63,plain,
( e13 = op1(e13,e10)
| e13 = op1(e13,e11)
| e13 = op1(e13,e12)
| e13 = op1(e13,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f68,plain,
( e10 = op1(e10,e13)
| e10 = op1(e11,e13)
| e10 = op1(e12,e13)
| e10 = 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(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(f95,plain,
( e20 = op2(e23,e22)
| e21 = op2(e23,e22)
| e22 = op2(e23,e22)
| e23 = op2(e23,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f110,plain,
( e23 = op2(e20,e23)
| e23 = op2(e21,e23)
| e23 = op2(e22,e23)
| e23 = op2(e23,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f111,plain,
( e23 = op2(e23,e20)
| e23 = op2(e23,e21)
| e23 = op2(e23,e22)
| e23 = op2(e23,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f119,plain,
( e23 = op2(e22,e20)
| e23 = op2(e22,e21)
| e23 = op2(e22,e22)
| e23 = op2(e22,e23) ),
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(f125,plain,
( e20 = op2(e22,e20)
| e20 = op2(e22,e21)
| e20 = op2(e22,e22)
| e20 = op2(e22,e23) ),
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(f131,plain,
( e21 = op2(e21,e20)
| e21 = op2(e21,e21)
| e21 = op2(e21,e22)
| e21 = op2(e21,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(f140,plain,
( e20 = op2(e20,e20)
| e20 = op2(e21,e20)
| e20 = op2(e22,e20)
| e20 = op2(e23,e20) ),
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(f150,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f155,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f157,plain,
op1(e11,e10) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f169,plain,
op1(e10,e13) != op1(e13,e13),
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(f192,plain,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f195,plain,
op2(e23,e20) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f203,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f215,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f217,plain,
op2(e20,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f220,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f226,plain,
op2(e22,e21) != op2(e23,e21),
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(f266,plain,
( e13 != op1(e13,e13)
| e13 != op1(e13,e13) ),
inference(cnf_transformation,[],[f10]) ).
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(f294,plain,
( e12 != op1(e12,e10)
| e10 != op1(e13,e13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f295,plain,
( e12 != op1(e12,e10)
| e10 != op1(e12,e12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f300,plain,
( e11 != op1(e11,e13)
| e13 != op1(e11,e11) ),
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(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(f359,plain,
( e22 != op2(e22,e20)
| e20 != op2(e22,e22) ),
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(f484,plain,
e13 != op1(e13,e13),
inference(duplicate_literal_removal,[],[f266]) ).
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(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(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(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(f1232,plain,
( ~ spl12_157
| ~ spl12_162 ),
inference(avatar_split_clause,[],[f359,f1228,f1193]) ).
fof(f1236,definition,
( spl12_163
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_163])],[avatar_definition]) ).
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(f1257,plain,
( e21 = op2(e21,e20)
| ~ spl12_165 ),
inference(avatar_component_clause,[],[f1256]) ).
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(f1296,definition,
( spl12_170
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_170])],[avatar_definition]) ).
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(f1307,plain,
( op1(e10,e10) = e13
| ~ spl12_172 ),
inference(avatar_component_clause,[],[f1306]) ).
fof(f1315,definition,
( spl12_174
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl12_174])],[avatar_definition]) ).
fof(f1316,plain,
( e13 = op1(e13,e12)
| ~ spl12_174 ),
inference(avatar_component_clause,[],[f1315]) ).
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(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(f1359,definition,
( spl12_183
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl12_183])],[avatar_definition]) ).
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(f1406,plain,
( ~ spl12_183
| ~ spl12_190 ),
inference(avatar_split_clause,[],[f294,f1403,f1359]) ).
fof(f1407,plain,
( ~ spl12_185
| ~ spl12_190 ),
inference(avatar_split_clause,[],[f295,f1403,f1368]) ).
fof(f1411,definition,
( spl12_191
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_191])],[avatar_definition]) ).
fof(f1416,plain,
( ~ spl12_171
| ~ spl12_191 ),
inference(avatar_split_clause,[],[f300,f1411,f1301]) ).
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(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(f1467,definition,
( spl12_197
<=> e23 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl12_197])],[avatar_definition]) ).
fof(f1469,plain,
( e23 = op2(e22,e23)
| ~ spl12_197 ),
inference(avatar_component_clause,[],[f1467]) ).
fof(f1471,definition,
( spl12_198
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl12_198])],[avatar_definition]) ).
fof(f1473,plain,
( e23 = op2(e21,e23)
| ~ spl12_198 ),
inference(avatar_component_clause,[],[f1471]) ).
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(f1478,plain,
( spl12_142
| spl12_197
| spl12_198
| spl12_199 ),
inference(avatar_split_clause,[],[f110,f1475,f1471,f1467,f1121]) ).
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(f1534,definition,
( spl12_212
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl12_212])],[avatar_definition]) ).
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(f1542,definition,
( spl12_214
<=> e20 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl12_214])],[avatar_definition]) ).
fof(f1544,plain,
( e20 = op2(e23,e20)
| ~ spl12_214 ),
inference(avatar_component_clause,[],[f1542]) ).
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(f1560,definition,
( spl12_218
<=> e23 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_218])],[avatar_definition]) ).
fof(f1562,plain,
( e23 = op2(e22,e20)
| ~ spl12_218 ),
inference(avatar_component_clause,[],[f1560]) ).
fof(f1563,plain,
( spl12_197
| spl12_141
| spl12_217
| spl12_218 ),
inference(avatar_split_clause,[],[f119,f1560,f1556,f1117,f1467]) ).
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(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(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(f1594,definition,
( spl12_225
<=> e20 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl12_225])],[avatar_definition]) ).
fof(f1598,definition,
( spl12_226
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl12_226])],[avatar_definition]) ).
fof(f1600,plain,
( e20 = op2(e22,e20)
| ~ spl12_226 ),
inference(avatar_component_clause,[],[f1598]) ).
fof(f1601,plain,
( spl12_210
| spl12_157
| spl12_225
| spl12_226 ),
inference(avatar_split_clause,[],[f125,f1598,f1594,f1193,f1525]) ).
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(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(f1620,plain,
( e22 = op2(e21,e20)
| ~ spl12_230 ),
inference(avatar_component_clause,[],[f1618]) ).
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(f1627,plain,
( spl12_163
| spl12_164
| spl12_153
| spl12_165 ),
inference(avatar_split_clause,[],[f131,f1256,f1174,f1244,f1236]) ).
fof(f1630,definition,
( spl12_232
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl12_232])],[avatar_definition]) ).
fof(f1632,plain,
( e20 = op2(e21,e20)
| ~ spl12_232 ),
inference(avatar_component_clause,[],[f1630]) ).
fof(f1639,plain,
( spl12_206
| spl12_221
| spl12_231
| spl12_154 ),
inference(avatar_split_clause,[],[f139,f1179,f1623,f1575,f1507]) ).
fof(f1640,plain,
( spl12_214
| spl12_226
| spl12_232
| spl12_159 ),
inference(avatar_split_clause,[],[f140,f1203,f1630,f1598,f1542]) ).
fof(f1641,plain,
( spl12_166
| spl12_167
| spl12_168
| spl12_159 ),
inference(avatar_split_clause,[],[f141,f1203,f1280,f1272,f1264]) ).
fof(f1643,plain,
( spl12_146
| spl12_202
| spl12_207
| spl12_212 ),
inference(avatar_split_clause,[],[f95,f1534,f1512,f1490,f1140]) ).
fof(f1663,definition,
( spl12_234
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_234])],[avatar_definition]) ).
fof(f1665,plain,
( e13 = op1(e11,e13)
| ~ spl12_234 ),
inference(avatar_component_clause,[],[f1663]) ).
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(f1671,plain,
( spl12_170
| spl12_174
| spl12_179
| spl12_184 ),
inference(avatar_split_clause,[],[f63,f1363,f1339,f1315,f1296]) ).
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(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(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(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(f1721,definition,
( spl12_247
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl12_247])],[avatar_definition]) ).
fof(f1724,plain,
( spl12_183
| spl12_246
| spl12_247
| spl12_194 ),
inference(avatar_split_clause,[],[f68,f1439,f1721,f1717,f1359]) ).
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(f1736,plain,
( e10 = op1(e13,e10)
| ~ spl12_250 ),
inference(avatar_component_clause,[],[f1734]) ).
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(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(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(f1839,plain,
( spl12_169
| spl12_175
| spl12_180
| spl12_185 ),
inference(avatar_split_clause,[],[f51,f1368,f1344,f1320,f1292]) ).
fof(f1842,plain,
( spl12_234
| spl12_236
| spl12_191
| spl12_247 ),
inference(avatar_split_clause,[],[f54,f1721,f1411,f1673,f1663]) ).
fof(f1852,plain,
( op2(e21,e21) != h2(op1(e13,e13))
| spl12_51
| ~ spl12_125 ),
inference(superposition,[],[f699,f1034]) ).
fof(f1853,plain,
spl12_178,
inference(avatar_split_clause,[],[f395,f1335]) ).
fof(f1854,plain,
spl12_150,
inference(avatar_split_clause,[],[f398,f1160]) ).
fof(f1855,plain,
~ spl12_142,
inference(avatar_split_clause,[],[f480,f1121]) ).
fof(f1856,plain,
~ spl12_170,
inference(avatar_split_clause,[],[f484,f1296]) ).
fof(f1874,plain,
( op2(e21,e21) != h2(e11)
| spl12_51
| ~ spl12_125
| ~ spl12_178 ),
inference(superposition,[],[f1852,f1336]) ).
fof(f2036,plain,
( e21 = e23
| ~ spl12_217
| ~ spl12_222 ),
inference(superposition,[],[f1582,f1558]) ).
fof(f2041,plain,
( $false
| ~ spl12_217
| ~ spl12_222 ),
inference(forward_subsumption_resolution,[],[f2036,f245]) ).
fof(f2042,plain,
( ~ spl12_217
| ~ spl12_222 ),
inference(avatar_contradiction_clause,[],[f2041]) ).
fof(f2048,plain,
( e22 = e23
| ~ spl12_162
| ~ spl12_218 ),
inference(forward_demodulation,[],[f1562,f1229]) ).
fof(f2049,plain,
( $false
| ~ spl12_162
| ~ spl12_218 ),
inference(forward_subsumption_resolution,[],[f2048,f244]) ).
fof(f2050,plain,
( ~ spl12_162
| ~ spl12_218 ),
inference(avatar_contradiction_clause,[],[f2049]) ).
fof(f2076,plain,
( e20 = e22
| ~ spl12_162
| ~ spl12_226 ),
inference(superposition,[],[f1600,f1229]) ).
fof(f2080,plain,
( $false
| ~ spl12_162
| ~ spl12_226 ),
inference(forward_subsumption_resolution,[],[f2076,f248]) ).
fof(f2081,plain,
( ~ spl12_162
| ~ spl12_226 ),
inference(avatar_contradiction_clause,[],[f2080]) ).
fof(f2154,plain,
( e22 = e23
| ~ spl12_227
| ~ spl12_229 ),
inference(superposition,[],[f1615,f1605]) ).
fof(f2159,plain,
( $false
| ~ spl12_227
| ~ spl12_229 ),
inference(forward_subsumption_resolution,[],[f2154,f244]) ).
fof(f2160,plain,
( ~ spl12_227
| ~ spl12_229 ),
inference(avatar_contradiction_clause,[],[f2159]) ).
fof(f2163,plain,
( e20 = e22
| ~ spl12_230
| ~ spl12_232 ),
inference(superposition,[],[f1632,f1620]) ).
fof(f2168,plain,
( $false
| ~ spl12_230
| ~ spl12_232 ),
inference(forward_subsumption_resolution,[],[f2163,f248]) ).
fof(f2169,plain,
( ~ spl12_230
| ~ spl12_232 ),
inference(avatar_contradiction_clause,[],[f2168]) ).
fof(f2192,plain,
( e11 = e13
| ~ spl12_172
| ~ spl12_182 ),
inference(superposition,[],[f1355,f1307]) ).
fof(f2196,plain,
( $false
| ~ spl12_172
| ~ spl12_182 ),
inference(forward_subsumption_resolution,[],[f2192,f239]) ).
fof(f2197,plain,
( ~ spl12_172
| ~ spl12_182 ),
inference(avatar_contradiction_clause,[],[f2196]) ).
fof(f2238,plain,
( e10 = e11
| ~ spl12_195
| ~ spl12_257 ),
inference(forward_demodulation,[],[f1769,f1448]) ).
fof(f2239,plain,
( $false
| ~ spl12_195
| ~ spl12_257 ),
inference(forward_subsumption_resolution,[],[f2238,f243]) ).
fof(f2240,plain,
( ~ spl12_195
| ~ spl12_257 ),
inference(avatar_contradiction_clause,[],[f2239]) ).
fof(f2270,plain,
( e10 = e13
| ~ spl12_184
| ~ spl12_250 ),
inference(superposition,[],[f1736,f1364]) ).
fof(f2274,plain,
( $false
| ~ spl12_184
| ~ spl12_250 ),
inference(forward_subsumption_resolution,[],[f2270,f241]) ).
fof(f2275,plain,
( ~ spl12_184
| ~ spl12_250 ),
inference(avatar_contradiction_clause,[],[f2274]) ).
fof(f2278,plain,
( e10 = e13
| ~ spl12_195
| ~ spl12_252 ),
inference(forward_demodulation,[],[f1745,f1448]) ).
fof(f2279,plain,
( $false
| ~ spl12_195
| ~ spl12_252 ),
inference(forward_subsumption_resolution,[],[f2278,f241]) ).
fof(f2280,plain,
( ~ spl12_195
| ~ spl12_252 ),
inference(avatar_contradiction_clause,[],[f2279]) ).
fof(f2291,plain,
( e12 = e13
| ~ spl12_174
| ~ spl12_238 ),
inference(superposition,[],[f1684,f1316]) ).
fof(f2295,plain,
( $false
| ~ spl12_174
| ~ spl12_238 ),
inference(forward_subsumption_resolution,[],[f2291,f238]) ).
fof(f2296,plain,
( ~ spl12_174
| ~ spl12_238 ),
inference(avatar_contradiction_clause,[],[f2295]) ).
fof(f2303,plain,
( e11 = e13
| ~ spl12_253
| ~ spl12_258 ),
inference(superposition,[],[f1774,f1750]) ).
fof(f2308,plain,
( $false
| ~ spl12_253
| ~ spl12_258 ),
inference(forward_subsumption_resolution,[],[f2303,f239]) ).
fof(f2309,plain,
( ~ spl12_253
| ~ spl12_258 ),
inference(avatar_contradiction_clause,[],[f2308]) ).
fof(f2353,plain,
( e11 = e12
| ~ spl12_192
| ~ spl12_255 ),
inference(superposition,[],[f1420,f1759]) ).
fof(f2358,plain,
( $false
| ~ spl12_192
| ~ spl12_255 ),
inference(forward_subsumption_resolution,[],[f2353,f240]) ).
fof(f2359,plain,
( ~ spl12_192
| ~ spl12_255 ),
inference(avatar_contradiction_clause,[],[f2358]) ).
fof(f2361,plain,
( e10 = e12
| ~ spl12_195
| ~ spl12_256 ),
inference(forward_demodulation,[],[f1763,f1448]) ).
fof(f2362,plain,
( $false
| ~ spl12_195
| ~ spl12_256 ),
inference(forward_subsumption_resolution,[],[f2361,f242]) ).
fof(f2363,plain,
( ~ spl12_195
| ~ spl12_256 ),
inference(avatar_contradiction_clause,[],[f2362]) ).
fof(f2493,plain,
( e10 = e12
| ~ spl12_190
| ~ spl12_262 ),
inference(superposition,[],[f1792,f1404]) ).
fof(f2499,plain,
( $false
| ~ spl12_190
| ~ spl12_262 ),
inference(forward_subsumption_resolution,[],[f2493,f242]) ).
fof(f2500,plain,
( ~ spl12_190
| ~ spl12_262 ),
inference(avatar_contradiction_clause,[],[f2499]) ).
fof(f2510,plain,
( e12 = e13
| ~ spl12_263
| ~ spl12_265 ),
inference(superposition,[],[f1807,f1797]) ).
fof(f2515,plain,
( $false
| ~ spl12_263
| ~ spl12_265 ),
inference(forward_subsumption_resolution,[],[f2510,f238]) ).
fof(f2516,plain,
( ~ spl12_263
| ~ spl12_265 ),
inference(avatar_contradiction_clause,[],[f2515]) ).
fof(f2522,plain,
( e11 = e12
| ~ spl12_265
| ~ spl12_267 ),
inference(superposition,[],[f1817,f1807]) ).
fof(f2527,plain,
( $false
| ~ spl12_265
| ~ spl12_267 ),
inference(forward_subsumption_resolution,[],[f2522,f240]) ).
fof(f2528,plain,
( ~ spl12_265
| ~ spl12_267 ),
inference(avatar_contradiction_clause,[],[f2527]) ).
fof(f2623,plain,
( $false
| spl12_51
| ~ spl12_125
| ~ spl12_178 ),
inference(forward_subsumption_resolution,[],[f405,f1874]) ).
fof(f2624,plain,
( spl12_51
| ~ spl12_125
| ~ spl12_178 ),
inference(avatar_contradiction_clause,[],[f2623]) ).
fof(f2625,plain,
( op2(e21,e21) = h2(op1(e13,e13))
| ~ spl12_51
| ~ spl12_125 ),
inference(forward_demodulation,[],[f698,f1034]) ).
fof(f2626,plain,
( h2(op1(e13,e12)) != op2(e21,h2(e12))
| spl12_52
| ~ spl12_125 ),
inference(forward_demodulation,[],[f703,f1034]) ).
fof(f2628,plain,
( op2(e21,e21) = h2(e11)
| ~ spl12_51
| ~ spl12_125
| ~ spl12_178 ),
inference(forward_demodulation,[],[f2625,f1336]) ).
fof(f2647,plain,
( e11 != op1(e13,e12)
| ~ spl12_178 ),
inference(forward_demodulation,[],[f142,f1336]) ).
fof(f2649,plain,
( e11 != op1(e13,e11)
| ~ spl12_178 ),
inference(forward_demodulation,[],[f143,f1336]) ).
fof(f2665,plain,
( e13 != op1(e11,e11)
| ~ spl12_234 ),
inference(forward_demodulation,[],[f155,f1665]) ).
fof(f2684,plain,
( e11 != op1(e10,e13)
| ~ spl12_178 ),
inference(forward_demodulation,[],[f169,f1336]) ).
fof(f2716,plain,
( e21 != op2(e23,e22)
| ~ spl12_150 ),
inference(forward_demodulation,[],[f190,f1161]) ).
fof(f2718,plain,
( e21 != op2(e23,e21)
| ~ spl12_150 ),
inference(forward_demodulation,[],[f191,f1161]) ).
fof(f2736,plain,
( e23 != op2(e21,e21)
| ~ spl12_198 ),
inference(forward_demodulation,[],[f203,f1473]) ).
fof(f2753,plain,
( e21 != op2(e21,e23)
| ~ spl12_150 ),
inference(forward_demodulation,[],[f215,f1161]) ).
fof(f2757,plain,
( e21 != op2(e20,e23)
| ~ spl12_150 ),
inference(forward_demodulation,[],[f217,f1161]) ).
fof(f2763,plain,
( e23 != op2(e22,e22)
| ~ spl12_146 ),
inference(forward_demodulation,[],[f220,f1141]) ).
fof(f2790,plain,
( e10 = op1(e13,e11)
| ~ spl12_178 ),
inference(forward_demodulation,[],[f396,f1336]) ).
fof(f2791,plain,
( spl12_249
| ~ spl12_178 ),
inference(avatar_split_clause,[],[f2790,f1335,f1730]) ).
fof(f2800,plain,
( ~ spl12_244
| ~ spl12_178 ),
inference(avatar_split_clause,[],[f2649,f1335,f1708]) ).
fof(f2804,plain,
( ~ spl12_242
| ~ spl12_178 ),
inference(avatar_split_clause,[],[f2684,f1335,f1699]) ).
fof(f2806,plain,
( e11 != op1(e12,e12)
| ~ spl12_258 ),
inference(forward_demodulation,[],[f150,f1774]) ).
fof(f2808,plain,
( ~ spl12_243
| ~ spl12_178 ),
inference(avatar_split_clause,[],[f2647,f1335,f1704]) ).
fof(f2886,plain,
( e20 = op2(e23,e21)
| ~ spl12_150 ),
inference(forward_demodulation,[],[f399,f1161]) ).
fof(f2887,plain,
( spl12_213
| ~ spl12_150 ),
inference(avatar_split_clause,[],[f2886,f1160,f1538]) ).
fof(f2889,plain,
( e21 = e22
| ~ spl12_164
| ~ spl12_219 ),
inference(forward_demodulation,[],[f1567,f1245]) ).
fof(f2897,plain,
( ~ spl12_208
| ~ spl12_150 ),
inference(avatar_split_clause,[],[f2718,f1160,f1516]) ).
fof(f2898,plain,
( e20 != op2(e23,e21)
| ~ spl12_214 ),
inference(forward_demodulation,[],[f195,f1544]) ).
fof(f2902,plain,
( $false
| ~ spl12_164
| ~ spl12_219 ),
inference(forward_subsumption_resolution,[],[f2889,f246]) ).
fof(f2903,plain,
( ~ spl12_164
| ~ spl12_219 ),
inference(avatar_contradiction_clause,[],[f2902]) ).
fof(f2908,plain,
( ~ spl12_213
| ~ spl12_214 ),
inference(avatar_split_clause,[],[f2898,f1542,f1538]) ).
fof(f2912,plain,
( ~ spl12_206
| ~ spl12_150 ),
inference(avatar_split_clause,[],[f2757,f1160,f1507]) ).
fof(f2923,plain,
( ~ spl12_143
| ~ spl12_198 ),
inference(avatar_split_clause,[],[f2736,f1471,f1126]) ).
fof(f2930,plain,
( ~ spl12_163
| ~ spl12_150 ),
inference(avatar_split_clause,[],[f2753,f1160,f1236]) ).
fof(f2936,plain,
( e23 = h2(e11)
| ~ spl12_51
| ~ spl12_125
| ~ spl12_143
| ~ spl12_178 ),
inference(superposition,[],[f2628,f1127]) ).
fof(f2943,plain,
( spl12_119
| ~ spl12_51
| ~ spl12_125
| ~ spl12_143
| ~ spl12_178 ),
inference(avatar_split_clause,[],[f2936,f1335,f1126,f1033,f697,f1003]) ).
fof(f3000,plain,
( e21 = e22
| ~ spl12_229
| ~ spl12_231 ),
inference(superposition,[],[f1625,f1615]) ).
fof(f3006,plain,
( $false
| ~ spl12_229
| ~ spl12_231 ),
inference(forward_subsumption_resolution,[],[f3000,f246]) ).
fof(f3007,plain,
( ~ spl12_229
| ~ spl12_231 ),
inference(avatar_contradiction_clause,[],[f3006]) ).
fof(f3017,plain,
( ~ spl12_141
| ~ spl12_146 ),
inference(avatar_split_clause,[],[f2763,f1140,f1117]) ).
fof(f3021,plain,
( e20 = e21
| ~ spl12_167
| ~ spl12_221 ),
inference(forward_demodulation,[],[f1577,f1273]) ).
fof(f3022,plain,
( ~ spl12_207
| ~ spl12_150 ),
inference(avatar_split_clause,[],[f2716,f1160,f1512]) ).
fof(f3023,plain,
( e20 != op2(e23,e22)
| ~ spl12_213 ),
inference(forward_demodulation,[],[f192,f1540]) ).
fof(f3027,plain,
( $false
| ~ spl12_167
| ~ spl12_221 ),
inference(forward_subsumption_resolution,[],[f3021,f249]) ).
fof(f3028,plain,
( ~ spl12_167
| ~ spl12_221 ),
inference(avatar_contradiction_clause,[],[f3027]) ).
fof(f3029,plain,
( ~ spl12_212
| ~ spl12_213 ),
inference(avatar_split_clause,[],[f3023,f1538,f1534]) ).
fof(f3124,plain,
( e20 != op2(e22,e21)
| ~ spl12_213 ),
inference(forward_demodulation,[],[f226,f1540]) ).
fof(f3150,plain,
( h2(e10) = op2(e21,h2(e11))
| ~ spl12_51
| ~ spl12_125
| ~ spl12_178 ),
inference(forward_demodulation,[],[f406,f2628]) ).
fof(f3151,plain,
( op2(e21,e23) = h2(e10)
| ~ spl12_51
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178 ),
inference(forward_demodulation,[],[f3150,f1004]) ).
fof(f3152,plain,
( e22 = h2(e10)
| ~ spl12_51
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178
| ~ spl12_200 ),
inference(forward_demodulation,[],[f3151,f1483]) ).
fof(f3153,plain,
( spl12_124
| ~ spl12_51
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178
| ~ spl12_200 ),
inference(avatar_split_clause,[],[f3152,f1481,f1335,f1033,f1003,f697,f1028]) ).
fof(f3160,plain,
( e12 = op1(op1(e13,e11),e11)
| ~ spl12_178 ),
inference(forward_demodulation,[],[f394,f1336]) ).
fof(f3161,plain,
( e12 = op1(e10,e11)
| ~ spl12_178
| ~ spl12_249 ),
inference(forward_demodulation,[],[f3160,f1732]) ).
fof(f3162,plain,
( e22 = op2(op2(e23,e21),e21)
| ~ spl12_150 ),
inference(forward_demodulation,[],[f397,f1161]) ).
fof(f3163,plain,
( e22 = op2(e20,e21)
| ~ spl12_150
| ~ spl12_213 ),
inference(forward_demodulation,[],[f3162,f1540]) ).
fof(f3173,plain,
( h2(e12) = op2(op2(e21,h2(e11)),h2(e11))
| ~ spl12_51
| ~ spl12_125
| ~ spl12_178 ),
inference(forward_demodulation,[],[f404,f2628]) ).
fof(f3174,plain,
( h2(e12) = op2(op2(e21,e23),e23)
| ~ spl12_51
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178 ),
inference(forward_demodulation,[],[f3173,f1004]) ).
fof(f3175,plain,
( op2(e22,e23) = h2(e12)
| ~ spl12_51
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178
| ~ spl12_200 ),
inference(forward_demodulation,[],[f3174,f1483]) ).
fof(f3176,plain,
( e20 = h2(e12)
| ~ spl12_51
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178
| ~ spl12_200
| ~ spl12_210 ),
inference(forward_demodulation,[],[f3175,f1527]) ).
fof(f3177,plain,
( spl12_67
| ~ spl12_51
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178
| ~ spl12_200
| ~ spl12_210 ),
inference(avatar_split_clause,[],[f3176,f1525,f1481,f1335,f1033,f1003,f697,f762]) ).
fof(f3178,plain,
( op2(e21,e20) != h2(op1(e13,e12))
| spl12_52
| ~ spl12_67
| ~ spl12_125 ),
inference(superposition,[],[f2626,f763]) ).
fof(f3179,plain,
( op2(e21,e20) != h2(e12)
| spl12_52
| ~ spl12_67
| ~ spl12_125
| ~ spl12_238 ),
inference(forward_demodulation,[],[f3178,f1684]) ).
fof(f3180,plain,
( e20 != op2(e21,e20)
| spl12_52
| ~ spl12_67
| ~ spl12_125
| ~ spl12_238 ),
inference(forward_demodulation,[],[f3179,f763]) ).
fof(f3181,plain,
( $false
| spl12_52
| ~ spl12_67
| ~ spl12_125
| ~ spl12_232
| ~ spl12_238 ),
inference(forward_subsumption_resolution,[],[f3180,f1632]) ).
fof(f3182,plain,
( spl12_52
| ~ spl12_67
| ~ spl12_125
| ~ spl12_232
| ~ spl12_238 ),
inference(avatar_contradiction_clause,[],[f3181]) ).
fof(f3184,plain,
( h2(op1(e13,e10)) != op2(h2(e13),e22)
| spl12_54
| ~ spl12_124 ),
inference(forward_demodulation,[],[f711,f1029]) ).
fof(f3186,plain,
( op2(e21,e22) != h2(op1(e13,e10))
| spl12_54
| ~ spl12_124
| ~ spl12_125 ),
inference(forward_demodulation,[],[f3184,f1034]) ).
fof(f3188,plain,
( op2(e21,e22) != h2(e13)
| spl12_54
| ~ spl12_124
| ~ spl12_125
| ~ spl12_184 ),
inference(forward_demodulation,[],[f3186,f1364]) ).
fof(f3190,plain,
( e21 != op2(e21,e22)
| spl12_54
| ~ spl12_124
| ~ spl12_125
| ~ spl12_184 ),
inference(forward_demodulation,[],[f3188,f1034]) ).
fof(f3191,plain,
( $false
| spl12_54
| ~ spl12_124
| ~ spl12_125
| ~ spl12_164
| ~ spl12_184 ),
inference(forward_subsumption_resolution,[],[f3190,f1245]) ).
fof(f3192,plain,
( spl12_54
| ~ spl12_124
| ~ spl12_125
| ~ spl12_164
| ~ spl12_184 ),
inference(avatar_contradiction_clause,[],[f3191]) ).
fof(f3193,plain,
( h2(op1(e13,e11)) != op2(h2(e13),e23)
| spl12_53
| ~ spl12_119 ),
inference(forward_demodulation,[],[f707,f1004]) ).
fof(f3195,plain,
( op2(e21,e23) != h2(op1(e13,e11))
| spl12_53
| ~ spl12_119
| ~ spl12_125 ),
inference(forward_demodulation,[],[f3193,f1034]) ).
fof(f3197,plain,
( op2(e21,e23) != h2(e10)
| spl12_53
| ~ spl12_119
| ~ spl12_125
| ~ spl12_249 ),
inference(forward_demodulation,[],[f3195,f1732]) ).
fof(f3199,plain,
( e22 != op2(e21,e23)
| spl12_53
| ~ spl12_119
| ~ spl12_124
| ~ spl12_125
| ~ spl12_249 ),
inference(forward_demodulation,[],[f3197,f1029]) ).
fof(f3201,plain,
( $false
| spl12_53
| ~ spl12_119
| ~ spl12_124
| ~ spl12_125
| ~ spl12_200
| ~ spl12_249 ),
inference(forward_subsumption_resolution,[],[f3199,f1483]) ).
fof(f3202,plain,
( spl12_53
| ~ spl12_119
| ~ spl12_124
| ~ spl12_125
| ~ spl12_200
| ~ spl12_249 ),
inference(avatar_contradiction_clause,[],[f3201]) ).
fof(f3204,plain,
( op2(e20,e20) != h2(op1(e12,e12))
| spl12_56
| ~ spl12_67 ),
inference(forward_demodulation,[],[f719,f763]) ).
fof(f3206,plain,
( op2(e20,e20) != h2(e13)
| spl12_56
| ~ spl12_67
| ~ spl12_169 ),
inference(forward_demodulation,[],[f3204,f1293]) ).
fof(f3208,plain,
( op2(e20,e20) != e21
| spl12_56
| ~ spl12_67
| ~ spl12_125
| ~ spl12_169 ),
inference(forward_demodulation,[],[f3206,f1034]) ).
fof(f3210,plain,
( $false
| spl12_56
| ~ spl12_67
| ~ spl12_125
| ~ spl12_154
| ~ spl12_169 ),
inference(forward_subsumption_resolution,[],[f3208,f1180]) ).
fof(f3211,plain,
( spl12_56
| ~ spl12_67
| ~ spl12_125
| ~ spl12_154
| ~ spl12_169 ),
inference(avatar_contradiction_clause,[],[f3210]) ).
fof(f3212,plain,
( h2(op1(e12,e13)) != op2(h2(e12),e21)
| spl12_55
| ~ spl12_125 ),
inference(forward_demodulation,[],[f715,f1034]) ).
fof(f3214,plain,
( op2(e20,e21) != h2(op1(e12,e13))
| spl12_55
| ~ spl12_67
| ~ spl12_125 ),
inference(forward_demodulation,[],[f3212,f763]) ).
fof(f3216,plain,
( op2(e20,e21) != h2(e10)
| spl12_55
| ~ spl12_67
| ~ spl12_125
| ~ spl12_246 ),
inference(forward_demodulation,[],[f3214,f1719]) ).
fof(f3218,plain,
( e22 != op2(e20,e21)
| spl12_55
| ~ spl12_67
| ~ spl12_124
| ~ spl12_125
| ~ spl12_246 ),
inference(forward_demodulation,[],[f3216,f1029]) ).
fof(f3219,plain,
( $false
| spl12_55
| ~ spl12_67
| ~ spl12_124
| ~ spl12_125
| ~ spl12_229
| ~ spl12_246 ),
inference(forward_subsumption_resolution,[],[f3218,f1615]) ).
fof(f3220,plain,
( spl12_55
| ~ spl12_67
| ~ spl12_124
| ~ spl12_125
| ~ spl12_229
| ~ spl12_246 ),
inference(avatar_contradiction_clause,[],[f3219]) ).
fof(f3222,plain,
( h2(op1(e12,e10)) != op2(h2(e12),e22)
| spl12_58
| ~ spl12_124 ),
inference(forward_demodulation,[],[f727,f1029]) ).
fof(f3224,plain,
( op2(e20,e22) != h2(op1(e12,e10))
| spl12_58
| ~ spl12_67
| ~ spl12_124 ),
inference(forward_demodulation,[],[f3222,f763]) ).
fof(f3226,plain,
( op2(e20,e22) != h2(e12)
| spl12_58
| ~ spl12_67
| ~ spl12_124
| ~ spl12_190 ),
inference(forward_demodulation,[],[f3224,f1404]) ).
fof(f3228,plain,
( e20 != op2(e20,e22)
| spl12_58
| ~ spl12_67
| ~ spl12_124
| ~ spl12_190 ),
inference(forward_demodulation,[],[f3226,f763]) ).
fof(f3229,plain,
( $false
| spl12_58
| ~ spl12_67
| ~ spl12_124
| ~ spl12_167
| ~ spl12_190 ),
inference(forward_subsumption_resolution,[],[f3228,f1273]) ).
fof(f3230,plain,
( spl12_58
| ~ spl12_67
| ~ spl12_124
| ~ spl12_167
| ~ spl12_190 ),
inference(avatar_contradiction_clause,[],[f3229]) ).
fof(f3231,plain,
( h2(op1(e12,e11)) != op2(h2(e12),e23)
| spl12_57
| ~ spl12_119 ),
inference(forward_demodulation,[],[f723,f1004]) ).
fof(f3233,plain,
( op2(e20,e23) != h2(op1(e12,e11))
| spl12_57
| ~ spl12_67
| ~ spl12_119 ),
inference(forward_demodulation,[],[f3231,f763]) ).
fof(f3235,plain,
( op2(e20,e23) != h2(e11)
| spl12_57
| ~ spl12_67
| ~ spl12_119
| ~ spl12_258 ),
inference(forward_demodulation,[],[f3233,f1774]) ).
fof(f3237,plain,
( e23 != op2(e20,e23)
| spl12_57
| ~ spl12_67
| ~ spl12_119
| ~ spl12_258 ),
inference(forward_demodulation,[],[f3235,f1004]) ).
fof(f3239,plain,
( $false
| spl12_57
| ~ spl12_67
| ~ spl12_119
| ~ spl12_199
| ~ spl12_258 ),
inference(forward_subsumption_resolution,[],[f3237,f1477]) ).
fof(f3240,plain,
( spl12_57
| ~ spl12_67
| ~ spl12_119
| ~ spl12_199
| ~ spl12_258 ),
inference(avatar_contradiction_clause,[],[f3239]) ).
fof(f3242,plain,
( h2(op1(e11,e12)) != op2(h2(e11),e20)
| spl12_60
| ~ spl12_67 ),
inference(forward_demodulation,[],[f735,f763]) ).
fof(f3244,plain,
( op2(e23,e20) != h2(op1(e11,e12))
| spl12_60
| ~ spl12_67
| ~ spl12_119 ),
inference(forward_demodulation,[],[f3242,f1004]) ).
fof(f3246,plain,
( op2(e23,e20) != h2(e11)
| spl12_60
| ~ spl12_67
| ~ spl12_119
| ~ spl12_192 ),
inference(forward_demodulation,[],[f3244,f1420]) ).
fof(f3248,plain,
( e23 != op2(e23,e20)
| spl12_60
| ~ spl12_67
| ~ spl12_119
| ~ spl12_192 ),
inference(forward_demodulation,[],[f3246,f1004]) ).
fof(f3249,plain,
( $false
| spl12_60
| ~ spl12_67
| ~ spl12_119
| ~ spl12_156
| ~ spl12_192 ),
inference(forward_subsumption_resolution,[],[f3248,f1189]) ).
fof(f3250,plain,
( spl12_60
| ~ spl12_67
| ~ spl12_119
| ~ spl12_156
| ~ spl12_192 ),
inference(avatar_contradiction_clause,[],[f3249]) ).
fof(f3251,plain,
( h2(op1(e11,e13)) != op2(h2(e11),e21)
| spl12_59
| ~ spl12_125 ),
inference(forward_demodulation,[],[f731,f1034]) ).
fof(f3253,plain,
( op2(e23,e21) != h2(op1(e11,e13))
| spl12_59
| ~ spl12_119
| ~ spl12_125 ),
inference(forward_demodulation,[],[f3251,f1004]) ).
fof(f3255,plain,
( op2(e23,e21) != h2(e12)
| spl12_59
| ~ spl12_119
| ~ spl12_125
| ~ spl12_236 ),
inference(forward_demodulation,[],[f3253,f1675]) ).
fof(f3257,plain,
( e20 != op2(e23,e21)
| spl12_59
| ~ spl12_67
| ~ spl12_119
| ~ spl12_125
| ~ spl12_236 ),
inference(forward_demodulation,[],[f3255,f763]) ).
fof(f3259,plain,
( $false
| spl12_59
| ~ spl12_67
| ~ spl12_119
| ~ spl12_125
| ~ spl12_213
| ~ spl12_236 ),
inference(forward_subsumption_resolution,[],[f3257,f1540]) ).
fof(f3260,plain,
( spl12_59
| ~ spl12_67
| ~ spl12_119
| ~ spl12_125
| ~ spl12_213
| ~ spl12_236 ),
inference(avatar_contradiction_clause,[],[f3259]) ).
fof(f3262,plain,
( h2(op1(e11,e10)) != op2(h2(e11),e22)
| spl12_62
| ~ spl12_124 ),
inference(forward_demodulation,[],[f743,f1029]) ).
fof(f3264,plain,
( op2(e23,e22) != h2(op1(e11,e10))
| spl12_62
| ~ spl12_119
| ~ spl12_124 ),
inference(forward_demodulation,[],[f3262,f1004]) ).
fof(f3266,plain,
( op2(e23,e22) != h2(e10)
| spl12_62
| ~ spl12_119
| ~ spl12_124
| ~ spl12_268 ),
inference(forward_demodulation,[],[f3264,f1824]) ).
fof(f3268,plain,
( e22 != op2(e23,e22)
| spl12_62
| ~ spl12_119
| ~ spl12_124
| ~ spl12_268 ),
inference(forward_demodulation,[],[f3266,f1029]) ).
fof(f3269,plain,
( $false
| spl12_62
| ~ spl12_119
| ~ spl12_124
| ~ spl12_202
| ~ spl12_268 ),
inference(forward_subsumption_resolution,[],[f3268,f1492]) ).
fof(f3270,plain,
( spl12_62
| ~ spl12_119
| ~ spl12_124
| ~ spl12_202
| ~ spl12_268 ),
inference(avatar_contradiction_clause,[],[f3269]) ).
fof(f3271,plain,
( op2(e23,e23) != h2(op1(e11,e11))
| spl12_61
| ~ spl12_119 ),
inference(forward_demodulation,[],[f739,f1004]) ).
fof(f3273,plain,
( op2(e23,e23) != h2(e13)
| spl12_61
| ~ spl12_119
| ~ spl12_171 ),
inference(forward_demodulation,[],[f3271,f1302]) ).
fof(f3275,plain,
( e21 != op2(e23,e23)
| spl12_61
| ~ spl12_119
| ~ spl12_125
| ~ spl12_171 ),
inference(forward_demodulation,[],[f3273,f1034]) ).
fof(f3277,plain,
( $false
| spl12_61
| ~ spl12_119
| ~ spl12_125
| ~ spl12_150
| ~ spl12_171 ),
inference(forward_subsumption_resolution,[],[f3275,f1161]) ).
fof(f3278,plain,
( spl12_61
| ~ spl12_119
| ~ spl12_125
| ~ spl12_150
| ~ spl12_171 ),
inference(avatar_contradiction_clause,[],[f3277]) ).
fof(f3281,plain,
( h2(op1(e10,e12)) != op2(h2(e10),e20)
| spl12_64
| ~ spl12_67 ),
inference(forward_demodulation,[],[f751,f763]) ).
fof(f3283,plain,
( op2(e22,e20) != h2(op1(e10,e12))
| spl12_64
| ~ spl12_67
| ~ spl12_124 ),
inference(forward_demodulation,[],[f3281,f1029]) ).
fof(f3285,plain,
( op2(e22,e20) != h2(e10)
| spl12_64
| ~ spl12_67
| ~ spl12_124
| ~ spl12_195 ),
inference(forward_demodulation,[],[f3283,f1448]) ).
fof(f3286,plain,
( e22 != op2(e22,e20)
| spl12_64
| ~ spl12_67
| ~ spl12_124
| ~ spl12_195 ),
inference(forward_demodulation,[],[f3285,f1029]) ).
fof(f3287,plain,
( $false
| spl12_64
| ~ spl12_67
| ~ spl12_124
| ~ spl12_162
| ~ spl12_195 ),
inference(forward_subsumption_resolution,[],[f3286,f1229]) ).
fof(f3288,plain,
( spl12_64
| ~ spl12_67
| ~ spl12_124
| ~ spl12_162
| ~ spl12_195 ),
inference(avatar_contradiction_clause,[],[f3287]) ).
fof(f3289,plain,
( h2(op1(e10,e13)) != op2(h2(e10),e21)
| spl12_63
| ~ spl12_125 ),
inference(forward_demodulation,[],[f747,f1034]) ).
fof(f3291,plain,
( op2(e22,e21) != h2(op1(e10,e13))
| spl12_63
| ~ spl12_124
| ~ spl12_125 ),
inference(forward_demodulation,[],[f3289,f1029]) ).
fof(f3293,plain,
( op2(e22,e21) != h2(e13)
| spl12_63
| ~ spl12_124
| ~ spl12_125
| ~ spl12_235 ),
inference(forward_demodulation,[],[f3291,f1669]) ).
fof(f3295,plain,
( e21 != op2(e22,e21)
| spl12_63
| ~ spl12_124
| ~ spl12_125
| ~ spl12_235 ),
inference(forward_demodulation,[],[f3293,f1034]) ).
fof(f3300,plain,
( op2(e22,e22) != h2(op1(e10,e10))
| spl12_66
| ~ spl12_124 ),
inference(forward_demodulation,[],[f759,f1029]) ).
fof(f3302,plain,
( op2(e22,e22) != h2(e11)
| spl12_66
| ~ spl12_124
| ~ spl12_182 ),
inference(forward_demodulation,[],[f3300,f1355]) ).
fof(f3304,plain,
( e23 != op2(e22,e22)
| spl12_66
| ~ spl12_119
| ~ spl12_124
| ~ spl12_182 ),
inference(forward_demodulation,[],[f3302,f1004]) ).
fof(f3308,plain,
( h2(op1(e10,e11)) != op2(h2(e10),e23)
| spl12_65
| ~ spl12_119 ),
inference(forward_demodulation,[],[f755,f1004]) ).
fof(f3310,plain,
( op2(e22,e23) != h2(op1(e10,e11))
| spl12_65
| ~ spl12_119
| ~ spl12_124 ),
inference(forward_demodulation,[],[f3308,f1029]) ).
fof(f3312,plain,
( op2(e22,e23) != h2(e12)
| spl12_65
| ~ spl12_119
| ~ spl12_124
| ~ spl12_265 ),
inference(forward_demodulation,[],[f3310,f1807]) ).
fof(f3314,plain,
( e20 != op2(e22,e23)
| spl12_65
| ~ spl12_67
| ~ spl12_119
| ~ spl12_124
| ~ spl12_265 ),
inference(forward_demodulation,[],[f3312,f763]) ).
fof(f3315,plain,
( $false
| spl12_65
| ~ spl12_67
| ~ spl12_119
| ~ spl12_124
| ~ spl12_210
| ~ spl12_265 ),
inference(forward_subsumption_resolution,[],[f3314,f1527]) ).
fof(f3316,plain,
( spl12_65
| ~ spl12_67
| ~ spl12_119
| ~ spl12_124
| ~ spl12_210
| ~ spl12_265 ),
inference(avatar_contradiction_clause,[],[f3315]) ).
fof(f3320,plain,
( ~ spl12_222
| spl12_63
| ~ spl12_124
| ~ spl12_125
| ~ spl12_235 ),
inference(avatar_split_clause,[],[f3295,f1667,f1033,f1028,f745,f1580]) ).
fof(f3324,plain,
( e20 = e21
| ~ spl12_165
| ~ spl12_232 ),
inference(forward_demodulation,[],[f1257,f1632]) ).
fof(f3329,plain,
( spl12_229
| ~ spl12_150
| ~ spl12_213 ),
inference(avatar_split_clause,[],[f3163,f1538,f1160,f1613]) ).
fof(f3334,plain,
( ~ spl12_225
| ~ spl12_213 ),
inference(avatar_split_clause,[],[f3124,f1538,f1594]) ).
fof(f3366,plain,
( $false
| ~ spl12_165
| ~ spl12_232 ),
inference(forward_subsumption_resolution,[],[f3324,f249]) ).
fof(f3367,plain,
( ~ spl12_165
| ~ spl12_232 ),
inference(avatar_contradiction_clause,[],[f3366]) ).
fof(f3389,plain,
( ~ spl12_141
| spl12_66
| ~ spl12_119
| ~ spl12_124
| ~ spl12_182 ),
inference(avatar_split_clause,[],[f3304,f1354,f1028,f1003,f757,f1117]) ).
fof(f3402,plain,
( e20 = e23
| ~ spl12_197
| ~ spl12_210 ),
inference(forward_demodulation,[],[f1469,f1527]) ).
fof(f3416,plain,
( $false
| ~ spl12_197
| ~ spl12_210 ),
inference(forward_subsumption_resolution,[],[f3402,f247]) ).
fof(f3417,plain,
( ~ spl12_197
| ~ spl12_210 ),
inference(avatar_contradiction_clause,[],[f3416]) ).
fof(f3436,plain,
( ~ spl12_171
| ~ spl12_234 ),
inference(avatar_split_clause,[],[f2665,f1663,f1301]) ).
fof(f3438,plain,
( spl12_265
| ~ spl12_178
| ~ spl12_249 ),
inference(avatar_split_clause,[],[f3161,f1730,f1335,f1805]) ).
fof(f3441,plain,
( e10 != op1(e11,e13)
| ~ spl12_268 ),
inference(forward_demodulation,[],[f157,f1824]) ).
fof(f3449,plain,
( ~ spl12_180
| ~ spl12_258 ),
inference(avatar_split_clause,[],[f2806,f1772,f1344]) ).
fof(f3459,plain,
( ~ spl12_247
| ~ spl12_268 ),
inference(avatar_split_clause,[],[f3441,f1822,f1721]) ).
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(s97,plain,
( ~ spl12_157
| ~ spl12_162 ),
inference(sat_conversion,[],[f1232]) ).
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(s159,plain,
( ~ spl12_183
| ~ spl12_190 ),
inference(sat_conversion,[],[f1406]) ).
cnf(s160,plain,
( ~ spl12_185
| ~ spl12_190 ),
inference(sat_conversion,[],[f1407]) ).
cnf(s165,plain,
( ~ spl12_171
| ~ spl12_191 ),
inference(sat_conversion,[],[f1416]) ).
cnf(s173,plain,
~ spl12_181,
inference(sat_conversion,[],[f1428]) ).
cnf(s181,plain,
( ~ spl12_171
| ~ spl12_194 ),
inference(sat_conversion,[],[f1444]) ).
cnf(s187,plain,
( ~ spl12_178
| ~ spl12_196 ),
inference(sat_conversion,[],[f1458]) ).
cnf(s194,plain,
~ spl12_187,
inference(sat_conversion,[],[f1465]) ).
cnf(s195,plain,
( spl12_142
| spl12_197
| spl12_198
| spl12_199 ),
inference(sat_conversion,[],[f1478]) ).
cnf(s196,plain,
( spl12_142
| spl12_146
| spl12_151
| spl12_156 ),
inference(sat_conversion,[],[f1479]) ).
cnf(s204,plain,
( spl12_141
| spl12_197
| spl12_217
| spl12_218 ),
inference(sat_conversion,[],[f1563]) ).
cnf(s206,plain,
( spl12_147
| spl12_160
| spl12_161
| spl12_162 ),
inference(sat_conversion,[],[f1573]) ).
cnf(s210,plain,
( spl12_157
| spl12_210
| spl12_225
| spl12_226 ),
inference(sat_conversion,[],[f1601]) ).
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(s216,plain,
( spl12_153
| spl12_163
| spl12_164
| spl12_165 ),
inference(sat_conversion,[],[f1627]) ).
cnf(s224,plain,
( spl12_154
| spl12_206
| spl12_221
| spl12_231 ),
inference(sat_conversion,[],[f1639]) ).
cnf(s225,plain,
( spl12_159
| spl12_214
| spl12_226
| spl12_232 ),
inference(sat_conversion,[],[f1640]) ).
cnf(s226,plain,
( spl12_159
| spl12_166
| spl12_167
| spl12_168 ),
inference(sat_conversion,[],[f1641]) ).
cnf(s228,plain,
( spl12_146
| spl12_202
| spl12_207
| spl12_212 ),
inference(sat_conversion,[],[f1643]) ).
cnf(s244,plain,
( spl12_170
| spl12_174
| spl12_179
| spl12_184 ),
inference(sat_conversion,[],[f1671]) ).
cnf(s249,plain,
( spl12_183
| spl12_194
| spl12_246
| spl12_247 ),
inference(sat_conversion,[],[f1724]) ).
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(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(s280,plain,
( spl12_169
| spl12_175
| spl12_180
| spl12_185 ),
inference(sat_conversion,[],[f1839]) ).
cnf(s283,plain,
( spl12_191
| spl12_234
| spl12_236
| spl12_247 ),
inference(sat_conversion,[],[f1842]) ).
cnf(s291,plain,
spl12_178,
inference(sat_conversion,[],[f1853]) ).
cnf(s292,plain,
spl12_150,
inference(sat_conversion,[],[f1854]) ).
cnf(s293,plain,
~ spl12_142,
inference(sat_conversion,[],[f1855]) ).
cnf(s294,plain,
~ spl12_170,
inference(sat_conversion,[],[f1856]) ).
cnf(s329,plain,
( ~ spl12_217
| ~ spl12_222 ),
inference(sat_conversion,[],[f2042]) ).
cnf(s331,plain,
( ~ spl12_162
| ~ spl12_218 ),
inference(sat_conversion,[],[f2050]) ).
cnf(s337,plain,
( ~ spl12_162
| ~ spl12_226 ),
inference(sat_conversion,[],[f2081]) ).
cnf(s351,plain,
( ~ spl12_227
| ~ spl12_229 ),
inference(sat_conversion,[],[f2160]) ).
cnf(s353,plain,
( ~ spl12_230
| ~ spl12_232 ),
inference(sat_conversion,[],[f2169]) ).
cnf(s359,plain,
( ~ spl12_172
| ~ spl12_182 ),
inference(sat_conversion,[],[f2197]) ).
cnf(s369,plain,
( ~ spl12_195
| ~ spl12_257 ),
inference(sat_conversion,[],[f2240]) ).
cnf(s377,plain,
( ~ spl12_184
| ~ spl12_250 ),
inference(sat_conversion,[],[f2275]) ).
cnf(s378,plain,
( ~ spl12_195
| ~ spl12_252 ),
inference(sat_conversion,[],[f2280]) ).
cnf(s382,plain,
( ~ spl12_174
| ~ spl12_238 ),
inference(sat_conversion,[],[f2296]) ).
cnf(s384,plain,
( ~ spl12_253
| ~ spl12_258 ),
inference(sat_conversion,[],[f2309]) ).
cnf(s394,plain,
( ~ spl12_192
| ~ spl12_255 ),
inference(sat_conversion,[],[f2359]) ).
cnf(s395,plain,
( ~ spl12_195
| ~ spl12_256 ),
inference(sat_conversion,[],[f2363]) ).
cnf(s416,plain,
( ~ spl12_190
| ~ spl12_262 ),
inference(sat_conversion,[],[f2500]) ).
cnf(s419,plain,
( ~ spl12_263
| ~ spl12_265 ),
inference(sat_conversion,[],[f2516]) ).
cnf(s422,plain,
( ~ spl12_265
| ~ spl12_267 ),
inference(sat_conversion,[],[f2528]) ).
cnf(s438,plain,
( spl12_51
| ~ spl12_125
| ~ spl12_178 ),
inference(sat_conversion,[],[f2624]) ).
cnf(s445,plain,
( ~ spl12_178
| spl12_249 ),
inference(sat_conversion,[],[f2791]) ).
cnf(s449,plain,
( ~ spl12_178
| ~ spl12_244 ),
inference(sat_conversion,[],[f2800]) ).
cnf(s450,plain,
( ~ spl12_178
| ~ spl12_242 ),
inference(sat_conversion,[],[f2804]) ).
cnf(s451,plain,
( ~ spl12_178
| ~ spl12_243 ),
inference(sat_conversion,[],[f2808]) ).
cnf(s458,plain,
( ~ spl12_150
| spl12_213 ),
inference(sat_conversion,[],[f2887]) ).
cnf(s462,plain,
( ~ spl12_150
| ~ spl12_208 ),
inference(sat_conversion,[],[f2897]) ).
cnf(s464,plain,
( ~ spl12_164
| ~ spl12_219 ),
inference(sat_conversion,[],[f2903]) ).
cnf(s469,plain,
( ~ spl12_213
| ~ spl12_214 ),
inference(sat_conversion,[],[f2908]) ).
cnf(s473,plain,
( ~ spl12_150
| ~ spl12_206 ),
inference(sat_conversion,[],[f2912]) ).
cnf(s478,plain,
( ~ spl12_143
| ~ spl12_198 ),
inference(sat_conversion,[],[f2923]) ).
cnf(s485,plain,
( ~ spl12_150
| ~ spl12_163 ),
inference(sat_conversion,[],[f2930]) ).
cnf(s489,plain,
( ~ spl12_51
| spl12_119
| ~ spl12_125
| ~ spl12_143
| ~ spl12_178 ),
inference(sat_conversion,[],[f2943]) ).
cnf(s498,plain,
( ~ spl12_229
| ~ spl12_231 ),
inference(sat_conversion,[],[f3007]) ).
cnf(s503,plain,
( ~ spl12_141
| ~ spl12_146 ),
inference(sat_conversion,[],[f3017]) ).
cnf(s504,plain,
( ~ spl12_150
| ~ spl12_207 ),
inference(sat_conversion,[],[f3022]) ).
cnf(s505,plain,
( ~ spl12_167
| ~ spl12_221 ),
inference(sat_conversion,[],[f3028]) ).
cnf(s506,plain,
( ~ spl12_212
| ~ spl12_213 ),
inference(sat_conversion,[],[f3029]) ).
cnf(s518,plain,
( ~ spl12_51
| ~ spl12_119
| spl12_124
| ~ spl12_125
| ~ spl12_178
| ~ spl12_200 ),
inference(sat_conversion,[],[f3153]) ).
cnf(s522,plain,
( ~ spl12_51
| spl12_67
| ~ spl12_119
| ~ spl12_125
| ~ spl12_178
| ~ spl12_200
| ~ spl12_210 ),
inference(sat_conversion,[],[f3177]) ).
cnf(s523,plain,
( spl12_52
| ~ spl12_67
| ~ spl12_125
| ~ spl12_232
| ~ spl12_238 ),
inference(sat_conversion,[],[f3182]) ).
cnf(s524,plain,
( spl12_54
| ~ spl12_124
| ~ spl12_125
| ~ spl12_164
| ~ spl12_184 ),
inference(sat_conversion,[],[f3192]) ).
cnf(s525,plain,
( spl12_53
| ~ spl12_119
| ~ spl12_124
| ~ spl12_125
| ~ spl12_200
| ~ spl12_249 ),
inference(sat_conversion,[],[f3202]) ).
cnf(s526,plain,
( spl12_56
| ~ spl12_67
| ~ spl12_125
| ~ spl12_154
| ~ spl12_169 ),
inference(sat_conversion,[],[f3211]) ).
cnf(s527,plain,
( spl12_55
| ~ spl12_67
| ~ spl12_124
| ~ spl12_125
| ~ spl12_229
| ~ spl12_246 ),
inference(sat_conversion,[],[f3220]) ).
cnf(s528,plain,
( spl12_58
| ~ spl12_67
| ~ spl12_124
| ~ spl12_167
| ~ spl12_190 ),
inference(sat_conversion,[],[f3230]) ).
cnf(s529,plain,
( spl12_57
| ~ spl12_67
| ~ spl12_119
| ~ spl12_199
| ~ spl12_258 ),
inference(sat_conversion,[],[f3240]) ).
cnf(s530,plain,
( spl12_60
| ~ spl12_67
| ~ spl12_119
| ~ spl12_156
| ~ spl12_192 ),
inference(sat_conversion,[],[f3250]) ).
cnf(s531,plain,
( spl12_59
| ~ spl12_67
| ~ spl12_119
| ~ spl12_125
| ~ spl12_213
| ~ spl12_236 ),
inference(sat_conversion,[],[f3260]) ).
cnf(s532,plain,
( spl12_62
| ~ spl12_119
| ~ spl12_124
| ~ spl12_202
| ~ spl12_268 ),
inference(sat_conversion,[],[f3270]) ).
cnf(s533,plain,
( spl12_61
| ~ spl12_119
| ~ spl12_125
| ~ spl12_150
| ~ spl12_171 ),
inference(sat_conversion,[],[f3278]) ).
cnf(s534,plain,
( spl12_64
| ~ spl12_67
| ~ spl12_124
| ~ spl12_162
| ~ spl12_195 ),
inference(sat_conversion,[],[f3288]) ).
cnf(s537,plain,
( spl12_65
| ~ spl12_67
| ~ spl12_119
| ~ spl12_124
| ~ spl12_210
| ~ spl12_265 ),
inference(sat_conversion,[],[f3316]) ).
cnf(s538,plain,
( spl12_63
| ~ spl12_124
| ~ spl12_125
| ~ spl12_222
| ~ spl12_235 ),
inference(sat_conversion,[],[f3320]) ).
cnf(s542,plain,
( ~ spl12_150
| ~ spl12_213
| spl12_229 ),
inference(sat_conversion,[],[f3329]) ).
cnf(s546,plain,
( ~ spl12_213
| ~ spl12_225 ),
inference(sat_conversion,[],[f3334]) ).
cnf(s562,plain,
( ~ spl12_165
| ~ spl12_232 ),
inference(sat_conversion,[],[f3367]) ).
cnf(s573,plain,
( spl12_66
| ~ spl12_119
| ~ spl12_124
| ~ spl12_141
| ~ spl12_182 ),
inference(sat_conversion,[],[f3389]) ).
cnf(s591,plain,
( ~ spl12_197
| ~ spl12_210 ),
inference(sat_conversion,[],[f3417]) ).
cnf(s603,plain,
( ~ spl12_171
| ~ spl12_234 ),
inference(sat_conversion,[],[f3436]) ).
cnf(s605,plain,
( ~ spl12_178
| ~ spl12_249
| spl12_265 ),
inference(sat_conversion,[],[f3438]) ).
cnf(s607,plain,
( ~ spl12_180
| ~ spl12_258 ),
inference(sat_conversion,[],[f3449]) ).
cnf(s611,plain,
( ~ spl12_247
| ~ spl12_268 ),
inference(sat_conversion,[],[f3459]) ).
cnf(s617,plain,
~ spl12_207,
inference(rat,[],[s504,s292]) ).
cnf(s618,plain,
~ spl12_163,
inference(rat,[],[s485,s292]) ).
cnf(s620,plain,
~ spl12_206,
inference(rat,[],[s473,s292]) ).
cnf(s622,plain,
~ spl12_208,
inference(rat,[],[s462,s292]) ).
cnf(s623,plain,
spl12_213,
inference(rat,[],[s458,s292]) ).
cnf(s626,plain,
~ spl12_225,
inference(rat,[],[s546,s623]) ).
cnf(s627,plain,
spl12_229,
inference(rat,[],[s542,s292,s623]) ).
cnf(s628,plain,
~ spl12_212,
inference(rat,[],[s506,s623]) ).
cnf(s630,plain,
~ spl12_214,
inference(rat,[],[s469,s623]) ).
cnf(s633,plain,
~ spl12_231,
inference(rat,[],[s498,s627]) ).
cnf(s634,plain,
~ spl12_227,
inference(rat,[],[s351,s627]) ).
cnf(s636,plain,
~ spl12_243,
inference(rat,[],[s451,s291]) ).
cnf(s637,plain,
~ spl12_242,
inference(rat,[],[s450,s291]) ).
cnf(s638,plain,
~ spl12_244,
inference(rat,[],[s449,s291]) ).
cnf(s640,plain,
spl12_249,
inference(rat,[],[s445,s291]) ).
cnf(s642,plain,
spl12_265,
inference(rat,[],[s605,s291,s640]) ).
cnf(s644,plain,
~ spl12_267,
inference(rat,[],[s422,s642]) ).
cnf(s645,plain,
~ spl12_263,
inference(rat,[],[s419,s642]) ).
cnf(s650,plain,
( spl12_182
| spl12_257 ),
inference(rat,[],[s272,s644,s637]) ).
cnf(s652,plain,
( spl12_172
| spl12_235
| spl12_252 ),
inference(rat,[],[s268,s645]) ).
cnf(s654,plain,
( spl12_181
| spl12_258 ),
inference(rat,[],[s263,s644,s638]) ).
cnf(s655,plain,
( spl12_171
| spl12_179
| spl12_253 ),
inference(rat,[],[s259,s645]) ).
cnf(s656,plain,
( spl12_180
| spl12_192
| spl12_257 ),
inference(rat,[],[s255,s636]) ).
cnf(s658,plain,
( spl12_174
| spl12_179
| spl12_184 ),
inference(rat,[],[s244,s294]) ).
cnf(s666,plain,
( spl12_146
| spl12_202 ),
inference(rat,[],[s228,s628,s617]) ).
cnf(s667,plain,
( spl12_159
| spl12_226
| spl12_232 ),
inference(rat,[],[s225,s630]) ).
cnf(s668,plain,
( spl12_154
| spl12_221 ),
inference(rat,[],[s224,s633,s620]) ).
cnf(s672,plain,
( spl12_153
| spl12_164
| spl12_165 ),
inference(rat,[],[s216,s618]) ).
cnf(s673,plain,
( spl12_153
| spl12_222 ),
inference(rat,[],[s215,s633,s622]) ).
cnf(s674,plain,
( spl12_143
| spl12_151
| spl12_217 ),
inference(rat,[],[s211,s634]) ).
cnf(s675,plain,
( spl12_157
| spl12_210
| spl12_226 ),
inference(rat,[],[s210,s626]) ).
cnf(s681,plain,
( spl12_146
| spl12_151
| spl12_156 ),
inference(rat,[],[s196,s293]) ).
cnf(s682,plain,
( spl12_197
| spl12_198
| spl12_199 ),
inference(rat,[],[s195,s293]) ).
cnf(s683,plain,
~ spl12_196,
inference(rat,[],[s187,s291]) ).
cnf(s684,plain,
spl12_258,
inference(rat,[],[s654,s173]) ).
cnf(s685,plain,
~ spl12_180,
inference(rat,[],[s607,s684]) ).
cnf(s686,plain,
~ spl12_253,
inference(rat,[],[s384,s684]) ).
cnf(s687,plain,
~ spl12_189,
inference(rat,[],[s155,s291]) ).
cnf(s688,plain,
~ spl12_179,
inference(rat,[],[s139,s291]) ).
cnf(s689,plain,
spl12_171,
inference(rat,[],[s655,s686,s688]) ).
cnf(s690,plain,
~ spl12_234,
inference(rat,[],[s603,s689]) ).
cnf(s691,plain,
~ spl12_194,
inference(rat,[],[s181,s689]) ).
cnf(s692,plain,
~ spl12_191,
inference(rat,[],[s165,s689]) ).
cnf(s693,plain,
~ spl12_188,
inference(rat,[],[s149,s689]) ).
cnf(s694,plain,
spl12_195,
inference(rat,[],[s274,s683,s194,s691]) ).
cnf(s695,plain,
spl12_190,
inference(rat,[],[s254,s152,s687,s693]) ).
cnf(s696,plain,
~ spl12_256,
inference(rat,[],[s395,s694]) ).
cnf(s697,plain,
~ spl12_252,
inference(rat,[],[s378,s694]) ).
cnf(s698,plain,
~ spl12_257,
inference(rat,[],[s369,s694]) ).
cnf(s702,plain,
~ spl12_262,
inference(rat,[],[s416,s695]) ).
cnf(s705,plain,
~ spl12_185,
inference(rat,[],[s160,s695]) ).
cnf(s706,plain,
~ spl12_183,
inference(rat,[],[s159,s695]) ).
cnf(s707,plain,
spl12_182,
inference(rat,[],[s650,s698]) ).
cnf(s708,plain,
spl12_192,
inference(rat,[],[s656,s685,s698]) ).
cnf(s709,plain,
spl12_169,
inference(rat,[],[s280,s152,s685,s705]) ).
cnf(s710,plain,
~ spl12_172,
inference(rat,[],[s359,s707]) ).
cnf(s712,plain,
~ spl12_255,
inference(rat,[],[s394,s708]) ).
cnf(s713,plain,
spl12_235,
inference(rat,[],[s652,s697,s710]) ).
cnf(s714,plain,
spl12_238,
inference(rat,[],[s253,s696,s152,s712]) ).
cnf(s715,plain,
~ spl12_174,
inference(rat,[],[s382,s714]) ).
cnf(s717,plain,
spl12_184,
inference(rat,[],[s658,s688,s715]) ).
cnf(s719,plain,
~ spl12_250,
inference(rat,[],[s377,s717]) ).
cnf(s720,plain,
spl12_268,
inference(rat,[],[s273,s702,s194,s719]) ).
cnf(s721,plain,
~ spl12_247,
inference(rat,[],[s611,s720]) ).
cnf(s724,plain,
spl12_236,
inference(rat,[],[s283,s692,s690,s721]) ).
cnf(s725,plain,
spl12_246,
inference(rat,[],[s249,s706,s691,s721]) ).
cnf(s728,plain,
~ spl12_168,
inference(rat,[],[s124,s292]) ).
cnf(s729,plain,
spl12_222,
inference(rat,[],[s673,s110]) ).
cnf(s730,plain,
~ spl12_217,
inference(rat,[],[s329,s729]) ).
cnf(s731,plain,
~ spl12_161,
inference(rat,[],[s92,s292]) ).
cnf(s732,plain,
~ spl12_151,
inference(rat,[],[s76,s292]) ).
cnf(s733,plain,
spl12_143,
inference(rat,[],[s674,s730,s732]) ).
cnf(s734,plain,
~ spl12_198,
inference(rat,[],[s478,s733]) ).
cnf(s735,plain,
~ spl12_166,
inference(rat,[],[s118,s733]) ).
cnf(s736,plain,
~ spl12_160,
inference(rat,[],[s86,s733]) ).
cnf(s737,plain,
spl12_167,
inference(rat,[],[s226,s728,s131,s735]) ).
cnf(s738,plain,
spl12_162,
inference(rat,[],[s206,s89,s731,s736]) ).
cnf(s739,plain,
~ spl12_221,
inference(rat,[],[s505,s737]) ).
cnf(s741,plain,
~ spl12_148,
inference(rat,[],[s122,s737]) ).
cnf(s743,plain,
~ spl12_226,
inference(rat,[],[s337,s738]) ).
cnf(s744,plain,
~ spl12_218,
inference(rat,[],[s331,s738]) ).
cnf(s745,plain,
~ spl12_157,
inference(rat,[],[s97,s738]) ).
cnf(s747,plain,
spl12_154,
inference(rat,[],[s668,s739]) ).
cnf(s748,plain,
spl12_232,
inference(rat,[],[s667,s131,s743]) ).
cnf(s750,plain,
spl12_210,
inference(rat,[],[s675,s743,s745]) ).
cnf(s754,plain,
~ spl12_165,
inference(rat,[],[s562,s748]) ).
cnf(s755,plain,
~ spl12_230,
inference(rat,[],[s353,s748]) ).
cnf(s756,plain,
~ spl12_197,
inference(rat,[],[s591,s750]) ).
cnf(s758,plain,
spl12_164,
inference(rat,[],[s672,s110,s754]) ).
cnf(s759,plain,
spl12_141,
inference(rat,[],[s204,s744,s730,s756]) ).
cnf(s760,plain,
spl12_199,
inference(rat,[],[s682,s734,s756]) ).
cnf(s761,plain,
~ spl12_219,
inference(rat,[],[s464,s758]) ).
cnf(s766,plain,
~ spl12_146,
inference(rat,[],[s503,s759]) ).
cnf(s769,plain,
spl12_200,
inference(rat,[],[s214,s755,s741,s761]) ).
cnf(s770,plain,
spl12_202,
inference(rat,[],[s666,s766]) ).
cnf(s771,plain,
spl12_156,
inference(rat,[],[s681,s732,s766]) ).
cnf(s779,plain,
spl12_51,
inference(rat,[],[s438,s291,s67]) ).
cnf(s780,plain,
spl12_119,
inference(rat,[],[s489,s291,s733,s67,s779]) ).
cnf(s782,plain,
spl12_61,
inference(rat,[],[s533,s689,s292,s67,s780]) ).
cnf(s783,plain,
spl12_124,
inference(rat,[],[s518,s769,s291,s67,s779,s780]) ).
cnf(s784,plain,
spl12_67,
inference(rat,[],[s522,s750,s769,s291,s67,s779,s780]) ).
cnf(s785,plain,
spl12_63,
inference(rat,[],[s538,s713,s729,s67,s783]) ).
cnf(s786,plain,
spl12_54,
inference(rat,[],[s524,s717,s758,s67,s783]) ).
cnf(s787,plain,
spl12_66,
inference(rat,[],[s573,s707,s759,s780,s783]) ).
cnf(s788,plain,
spl12_62,
inference(rat,[],[s532,s720,s770,s780,s783]) ).
cnf(s789,plain,
spl12_53,
inference(rat,[],[s525,s640,s769,s67,s780,s783]) ).
cnf(s790,plain,
spl12_65,
inference(rat,[],[s537,s642,s750,s783,s780,s784]) ).
cnf(s791,plain,
spl12_64,
inference(rat,[],[s534,s694,s738,s783,s784]) ).
cnf(s792,plain,
spl12_59,
inference(rat,[],[s531,s724,s623,s67,s780,s784]) ).
cnf(s793,plain,
spl12_60,
inference(rat,[],[s530,s708,s771,s780,s784]) ).
cnf(s794,plain,
spl12_57,
inference(rat,[],[s529,s684,s760,s780,s784]) ).
cnf(s795,plain,
spl12_58,
inference(rat,[],[s528,s695,s737,s783,s784]) ).
cnf(s796,plain,
spl12_55,
inference(rat,[],[s527,s725,s627,s67,s783,s784]) ).
cnf(s797,plain,
spl12_56,
inference(rat,[],[s526,s709,s747,s67,s784]) ).
cnf(s798,plain,
spl12_52,
inference(rat,[],[s523,s714,s748,s67,s784]) ).
cnf(s801,plain,
~ spl12_49,
inference(rat,[],[s49,s67]) ).
cnf(s802,plain,
~ spl12_48,
inference(rat,[],[s48,s783]) ).
cnf(s803,plain,
~ spl12_47,
inference(rat,[],[s43,s780]) ).
cnf(s812,plain,
$false,
inference(rat,[],[s10,s784,s787,s790,s791,s785,s788,s782,s793,s792,s795,s794,s797,s796,s786,s789,s798,s779,s801,s802,s803]) ).
fof(f3464,plain,
$false,
inference(avatar_sat_refutation,[],[s812]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG111+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 % Computer : n007.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Mon Sep 28 19:27:41 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24 Running first-order model finding
% 0.09/0.24 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.37 % (2732784)Will run a generic schedule for satisfiability detection.
% 0.19/0.37 % (2732794)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2317845738:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.37 % (2732790)% WARNING: option uhcvi not known.
% 0.19/0.37 % (2732789)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2862543269_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.37 % (2732790)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2210770820:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.37 % (2732791)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2005792921:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.37 % (2732792)dis+10_1_sil=32000:sp=arity:random_seed=1220314535:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.37 % (2732793)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1252809001:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.37 % (2732795)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2028307512:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.37 % (2732794)Instruction limit reached!
% 0.19/0.37 % (2732794)------------------------------
% 0.19/0.37 % (2732794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.37 % (2732794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.37 % (2732794)CaDiCaL version: 2.1.3
% 0.19/0.37 % (2732794)Termination reason: Instruction limit
% 0.19/0.37 % (2732794)Termination phase: Saturation
% 0.19/0.37 % (2732794)Time elapsed: 0.034 s
% 0.19/0.37 % (2732794)Peak memory usage: 13 MB
% 0.19/0.37 % (2732794)Instructions burned: 132 (million)
% 0.19/0.37 % Detected minimum model sizes of [8]
% 0.19/0.37 % Detected maximum model sizes of [max]
% 0.19/0.37 % TRYING [8]
% 0.19/0.37 % (2732803)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2285967453:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.19/0.37 % (2732792) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2732784-2732792"...
% 0.19/0.37 % (2732793) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2732784-2732793"...
% 0.19/0.37 % Detected minimum model sizes of [8]
% 0.19/0.37 % Detected maximum model sizes of [max]
% 0.19/0.37 % TRYING [8]
% 0.19/0.37 % (2732792)...printing done.
% 0.19/0.37 % (2732790) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2732784-2732790"...
% 0.19/0.37 % (2732793)...printing done.
% 0.19/0.37 % (2732792)Refutation found. Thanks to Tanya!
% 0.19/0.37 % SZS status Theorem for theBenchmark
% 0.19/0.37 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.37 % (2732792)------------------------------
% 0.19/0.37 % (2732792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.37 % (2732792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.37 % (2732792)CaDiCaL version: 2.1.3
% 0.19/0.37 % (2732792)Termination reason: Refutation
% 0.19/0.37 % (2732792)Time elapsed: 0.063 s
% 0.19/0.37 % (2732792)Peak memory usage: 14 MB
% 0.19/0.37 % (2732792)Instructions burned: 127 (million)
% 0.19/0.37 % (2732784)Success in time 0.117 s
% 0.19/0.37 % Vampire exiting
%------------------------------------------------------------------------------