%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG114+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 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.20s 0.35s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 136
% Syntax : Number of formulae : 915 ( 168 unt; 122 def)
% Number of atoms : 3203 (1474 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 3753 (1465 ~;1734 |; 432 &)
% ( 122 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 126 ( 124 usr; 125 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e11) = e10
| op1(e10,e12) = e10
| op1(e10,e13) = e10 )
& ( op1(e10,e10) = e10
| op1(e11,e10) = e10
| op1(e12,e10) = e10
| op1(e13,e10) = e10 )
& ( op1(e10,e10) = e11
| op1(e10,e11) = e11
| op1(e10,e12) = e11
| op1(e10,e13) = e11 )
& ( op1(e10,e10) = e11
| op1(e11,e10) = e11
| op1(e12,e10) = e11
| op1(e13,e10) = e11 )
& ( op1(e10,e10) = e12
| op1(e10,e11) = e12
| op1(e10,e12) = e12
| op1(e10,e13) = e12 )
& ( op1(e10,e10) = e12
| op1(e11,e10) = e12
| op1(e12,e10) = e12
| op1(e13,e10) = e12 )
& ( op1(e10,e10) = e13
| op1(e10,e11) = e13
| op1(e10,e12) = e13
| op1(e10,e13) = e13 )
& ( op1(e10,e10) = e13
| op1(e11,e10) = e13
| op1(e12,e10) = e13
| op1(e13,e10) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e11) = e10
| op1(e11,e12) = e10
| op1(e11,e13) = e10 )
& ( op1(e10,e11) = e10
| op1(e11,e11) = e10
| op1(e12,e11) = e10
| op1(e13,e11) = e10 )
& ( op1(e11,e10) = e11
| op1(e11,e11) = e11
| op1(e11,e12) = e11
| op1(e11,e13) = e11 )
& ( op1(e10,e11) = e11
| op1(e11,e11) = e11
| op1(e12,e11) = e11
| op1(e13,e11) = e11 )
& ( op1(e11,e10) = e12
| op1(e11,e11) = e12
| op1(e11,e12) = e12
| op1(e11,e13) = e12 )
& ( op1(e10,e11) = e12
| op1(e11,e11) = e12
| op1(e12,e11) = e12
| op1(e13,e11) = e12 )
& ( op1(e11,e10) = e13
| op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e11,e13) = e13 )
& ( op1(e10,e11) = e13
| op1(e11,e11) = e13
| op1(e12,e11) = e13
| op1(e13,e11) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e11) = e10
| op1(e12,e12) = e10
| op1(e12,e13) = e10 )
& ( op1(e10,e12) = e10
| op1(e11,e12) = e10
| op1(e12,e12) = e10
| op1(e13,e12) = e10 )
& ( op1(e12,e10) = e11
| op1(e12,e11) = e11
| op1(e12,e12) = e11
| op1(e12,e13) = e11 )
& ( op1(e10,e12) = e11
| op1(e11,e12) = e11
| op1(e12,e12) = e11
| op1(e13,e12) = e11 )
& ( op1(e12,e10) = e12
| op1(e12,e11) = e12
| op1(e12,e12) = e12
| op1(e12,e13) = e12 )
& ( op1(e10,e12) = e12
| op1(e11,e12) = e12
| op1(e12,e12) = e12
| op1(e13,e12) = e12 )
& ( op1(e12,e10) = e13
| op1(e12,e11) = e13
| op1(e12,e12) = e13
| op1(e12,e13) = e13 )
& ( op1(e10,e12) = e13
| op1(e11,e12) = e13
| op1(e12,e12) = e13
| op1(e13,e12) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10 )
& ( op1(e10,e13) = e10
| op1(e11,e13) = e10
| op1(e12,e13) = e10
| op1(e13,e13) = e10 )
& ( op1(e13,e10) = e11
| op1(e13,e11) = e11
| op1(e13,e12) = e11
| op1(e13,e13) = e11 )
& ( op1(e10,e13) = e11
| op1(e11,e13) = e11
| op1(e12,e13) = e11
| op1(e13,e13) = e11 )
& ( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12
| op1(e13,e13) = e12 )
& ( op1(e10,e13) = e12
| op1(e11,e13) = e12
| op1(e12,e13) = e12
| op1(e13,e13) = e12 )
& ( op1(e13,e10) = e13
| op1(e13,e11) = e13
| op1(e13,e12) = e13
| op1(e13,e13) = e13 )
& ( op1(e10,e13) = e13
| op1(e11,e13) = e13
| op1(e12,e13) = e13
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e20) = e21
| op2(e20,e20) = e22
| op2(e20,e20) = e23 )
& ( op2(e20,e21) = e20
| op2(e20,e21) = e21
| op2(e20,e21) = e22
| op2(e20,e21) = e23 )
& ( op2(e20,e22) = e20
| op2(e20,e22) = e21
| op2(e20,e22) = e22
| op2(e20,e22) = e23 )
& ( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22
| op2(e20,e23) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e20) = e21
| op2(e21,e20) = e22
| op2(e21,e20) = e23 )
& ( op2(e21,e21) = e20
| op2(e21,e21) = e21
| op2(e21,e21) = e22
| op2(e21,e21) = e23 )
& ( op2(e21,e22) = e20
| op2(e21,e22) = e21
| op2(e21,e22) = e22
| op2(e21,e22) = e23 )
& ( op2(e21,e23) = e20
| op2(e21,e23) = e21
| op2(e21,e23) = e22
| op2(e21,e23) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e20) = e21
| op2(e22,e20) = e22
| op2(e22,e20) = e23 )
& ( op2(e22,e21) = e20
| op2(e22,e21) = e21
| op2(e22,e21) = e22
| op2(e22,e21) = e23 )
& ( op2(e22,e22) = e20
| op2(e22,e22) = e21
| op2(e22,e22) = e22
| op2(e22,e22) = e23 )
& ( op2(e22,e23) = e20
| op2(e22,e23) = e21
| op2(e22,e23) = e22
| op2(e22,e23) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e20) = e21
| op2(e23,e20) = e22
| op2(e23,e20) = e23 )
& ( op2(e23,e21) = e20
| op2(e23,e21) = e21
| op2(e23,e21) = e22
| op2(e23,e21) = e23 )
& ( op2(e23,e22) = e20
| op2(e23,e22) = e21
| op2(e23,e22) = e22
| op2(e23,e22) = e23 )
& ( op2(e23,e23) = e20
| op2(e23,e23) = e21
| op2(e23,e23) = e22
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e22) = e20
| op2(e20,e23) = e20 )
& ( op2(e20,e20) = e20
| op2(e21,e20) = e20
| op2(e22,e20) = e20
| op2(e23,e20) = e20 )
& ( op2(e20,e20) = e21
| op2(e20,e21) = e21
| op2(e20,e22) = e21
| op2(e20,e23) = e21 )
& ( op2(e20,e20) = e21
| op2(e21,e20) = e21
| op2(e22,e20) = e21
| op2(e23,e20) = e21 )
& ( op2(e20,e20) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 )
& ( op2(e20,e20) = e22
| op2(e21,e20) = e22
| op2(e22,e20) = e22
| op2(e23,e20) = e22 )
& ( op2(e20,e20) = e23
| op2(e20,e21) = e23
| op2(e20,e22) = e23
| op2(e20,e23) = e23 )
& ( op2(e20,e20) = e23
| op2(e21,e20) = e23
| op2(e22,e20) = e23
| op2(e23,e20) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e21) = e20
| op2(e21,e22) = e20
| op2(e21,e23) = e20 )
& ( op2(e20,e21) = e20
| op2(e21,e21) = e20
| op2(e22,e21) = e20
| op2(e23,e21) = e20 )
& ( op2(e21,e20) = e21
| op2(e21,e21) = e21
| op2(e21,e22) = e21
| op2(e21,e23) = e21 )
& ( op2(e20,e21) = e21
| op2(e21,e21) = e21
| op2(e22,e21) = e21
| op2(e23,e21) = e21 )
& ( op2(e21,e20) = e22
| op2(e21,e21) = e22
| op2(e21,e22) = e22
| op2(e21,e23) = e22 )
& ( op2(e20,e21) = e22
| op2(e21,e21) = e22
| op2(e22,e21) = e22
| op2(e23,e21) = e22 )
& ( op2(e21,e20) = e23
| op2(e21,e21) = e23
| op2(e21,e22) = e23
| op2(e21,e23) = e23 )
& ( op2(e20,e21) = e23
| op2(e21,e21) = e23
| op2(e22,e21) = e23
| op2(e23,e21) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e21) = e20
| op2(e22,e22) = e20
| op2(e22,e23) = e20 )
& ( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e22,e22) = e20
| op2(e23,e22) = e20 )
& ( op2(e22,e20) = e21
| op2(e22,e21) = e21
| op2(e22,e22) = e21
| op2(e22,e23) = e21 )
& ( op2(e20,e22) = e21
| op2(e21,e22) = e21
| op2(e22,e22) = e21
| op2(e23,e22) = e21 )
& ( op2(e22,e20) = e22
| op2(e22,e21) = e22
| op2(e22,e22) = e22
| op2(e22,e23) = e22 )
& ( op2(e20,e22) = e22
| op2(e21,e22) = e22
| op2(e22,e22) = e22
| op2(e23,e22) = e22 )
& ( op2(e22,e20) = e23
| op2(e22,e21) = e23
| op2(e22,e22) = e23
| op2(e22,e23) = e23 )
& ( op2(e20,e22) = e23
| op2(e21,e22) = e23
| op2(e22,e22) = e23
| op2(e23,e22) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e23) = e20 )
& ( op2(e20,e23) = e20
| op2(e21,e23) = e20
| op2(e22,e23) = e20
| op2(e23,e23) = e20 )
& ( op2(e23,e20) = e21
| op2(e23,e21) = e21
| op2(e23,e22) = e21
| op2(e23,e23) = e21 )
& ( op2(e20,e23) = e21
| op2(e21,e23) = e21
| op2(e22,e23) = e21
| op2(e23,e23) = e21 )
& ( op2(e23,e20) = e22
| op2(e23,e21) = e22
| op2(e23,e22) = e22
| op2(e23,e23) = e22 )
& ( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22
| op2(e23,e23) = e22 )
& ( op2(e23,e20) = e23
| op2(e23,e21) = e23
| op2(e23,e22) = e23
| op2(e23,e23) = e23 )
& ( op2(e20,e23) = e23
| op2(e21,e23) = e23
| op2(e22,e23) = e23
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op1(e10,e10) != op1(e11,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e12,e10) != op1(e13,e10)
& op1(e10,e11) != op1(e11,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e12,e11) != op1(e13,e11)
& op1(e10,e12) != op1(e11,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e12,e12) != op1(e13,e12)
& op1(e10,e13) != op1(e11,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e12,e13) != op1(e13,e13)
& op1(e10,e10) != op1(e10,e11)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e12) != op1(e10,e13)
& op1(e11,e10) != op1(e11,e11)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e12) != op1(e11,e13)
& op1(e12,e10) != op1(e12,e11)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e12) != op1(e12,e13)
& op1(e13,e10) != op1(e13,e11)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e12) != op1(e13,e13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( op2(e20,e20) != op2(e21,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e22,e20) != op2(e23,e20)
& op2(e20,e21) != op2(e21,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e22,e21) != op2(e23,e21)
& op2(e20,e22) != op2(e21,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e22,e22) != op2(e23,e22)
& op2(e20,e23) != op2(e21,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e22,e23) != op2(e23,e23)
& op2(e20,e20) != op2(e20,e21)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e22) != op2(e20,e23)
& op2(e21,e20) != op2(e21,e21)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e22) != op2(e21,e23)
& op2(e22,e20) != op2(e22,e21)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e22) != op2(e22,e23)
& op2(e23,e20) != op2(e23,e21)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e22) != op2(e23,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f10,axiom,
( ( ( op1(e10,e10) = e10
& op1(e10,e10) != e10 )
| ( op1(e11,e11) = e10
& op1(e10,e10) != e11 )
| ( op1(e12,e12) = e10
& op1(e10,e10) != e12 )
| ( op1(e13,e13) = e10
& op1(e10,e10) != e13 ) )
& ( ( op1(e10,e10) = e11
& op1(e11,e11) != e10 )
| ( op1(e11,e11) = e11
& op1(e11,e11) != e11 )
| ( op1(e12,e12) = e11
& op1(e11,e11) != e12 )
| ( op1(e13,e13) = e11
& op1(e11,e11) != e13 ) )
& ( ( op1(e10,e10) = e12
& op1(e12,e12) != e10 )
| ( op1(e11,e11) = e12
& op1(e12,e12) != e11 )
| ( op1(e12,e12) = e12
& op1(e12,e12) != e12 )
| ( op1(e13,e13) = e12
& op1(e12,e12) != e13 ) )
& ( ( op1(e10,e10) = e13
& op1(e13,e13) != e10 )
| ( op1(e11,e11) = e13
& op1(e13,e13) != e11 )
| ( op1(e12,e12) = e13
& op1(e13,e13) != e12 )
| ( op1(e13,e13) = e13
& op1(e13,e13) != e13 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( ( ( op2(e20,e20) = e20
& op2(e20,e20) != e20 )
| ( op2(e21,e21) = e20
& op2(e20,e20) != e21 )
| ( op2(e22,e22) = e20
& op2(e20,e20) != e22 )
| ( op2(e23,e23) = e20
& op2(e20,e20) != e23 ) )
& ( ( op2(e20,e20) = e21
& op2(e21,e21) != e20 )
| ( op2(e21,e21) = e21
& op2(e21,e21) != e21 )
| ( op2(e22,e22) = e21
& op2(e21,e21) != e22 )
| ( op2(e23,e23) = e21
& op2(e21,e21) != e23 ) )
& ( ( op2(e20,e20) = e22
& op2(e22,e22) != e20 )
| ( op2(e21,e21) = e22
& op2(e22,e22) != e21 )
| ( op2(e22,e22) = e22
& op2(e22,e22) != e22 )
| ( op2(e23,e23) = e22
& op2(e22,e22) != e23 ) )
& ( ( op2(e20,e20) = e23
& op2(e23,e23) != e20 )
| ( op2(e21,e21) = e23
& op2(e23,e23) != e21 )
| ( op2(e22,e22) = e23
& op2(e23,e23) != e22 )
| ( op2(e23,e23) = e23
& op2(e23,e23) != e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e10 = op1(op1(e12,e12),e12)
& e11 = op1(op1(e12,e12),op1(e12,e12))
& e13 = op1(e12,e12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e20 = op2(op2(e22,e22),e22)
& e21 = op2(op2(e22,e22),op2(e22,e22))
& e23 = op2(e22,e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f15,axiom,
( h2(e12) = e21
& h2(e10) = op2(op2(e21,e21),e21)
& h2(e11) = op2(op2(e21,e21),op2(e21,e21))
& h2(e13) = op2(e21,e21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
fof(f17,axiom,
( h4(e12) = e23
& h4(e10) = op2(op2(e23,e23),e23)
& h4(e11) = op2(op2(e23,e23),op2(e23,e23))
& h4(e13) = op2(e23,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
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(f37,plain,
( e10 = op1(e10,e13)
| e10 = op1(e10,e12)
| e10 = op1(e10,e11)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f38,plain,
( e10 = op1(e13,e10)
| e10 = op1(e12,e10)
| e10 = op1(e11,e10)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f39,plain,
( e11 = op1(e10,e13)
| e11 = op1(e10,e12)
| e11 = op1(e10,e11)
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[],[f2]) ).
fof(f40,plain,
( e11 = op1(e13,e10)
| e11 = op1(e12,e10)
| e11 = op1(e11,e10)
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[],[f2]) ).
fof(f43,plain,
( e13 = op1(e10,e13)
| e13 = op1(e10,e12)
| e13 = op1(e10,e11)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f2]) ).
fof(f44,plain,
( e13 = op1(e13,e10)
| e13 = op1(e12,e10)
| e13 = op1(e11,e10)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f2]) ).
fof(f47,plain,
( e11 = op1(e11,e13)
| e11 = op1(e11,e12)
| e11 = op1(e11,e11)
| e11 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f48,plain,
( e11 = op1(e13,e11)
| e11 = op1(e12,e11)
| e11 = op1(e11,e11)
| e11 = op1(e10,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f51,plain,
( e13 = op1(e11,e13)
| e13 = op1(e11,e12)
| e13 = op1(e11,e11)
| e13 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f52,plain,
( e13 = op1(e13,e11)
| e13 = op1(e12,e11)
| e13 = op1(e11,e11)
| e13 = op1(e10,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f53,plain,
( e10 = op1(e12,e13)
| e10 = op1(e12,e12)
| e10 = op1(e12,e11)
| e10 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f56,plain,
( e11 = op1(e13,e12)
| e11 = op1(e12,e12)
| e11 = op1(e11,e12)
| e11 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f58,plain,
( e12 = op1(e13,e12)
| e12 = op1(e12,e12)
| e12 = op1(e11,e12)
| e12 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f65,plain,
( e12 = op1(e13,e13)
| e12 = op1(e13,e12)
| e12 = op1(e13,e11)
| e12 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f66,plain,
( e12 = op1(e13,e13)
| e12 = op1(e12,e13)
| e12 = op1(e11,e13)
| e12 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f68,plain,
( e13 = op1(e13,e13)
| e13 = op1(e12,e13)
| e13 = op1(e11,e13)
| e13 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f71,plain,
( e23 = op2(e20,e22)
| e22 = op2(e20,e22)
| e21 = op2(e20,e22)
| e20 = op2(e20,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f81,plain,
( e23 = op2(e23,e20)
| e22 = op2(e23,e20)
| e21 = op2(e23,e20)
| e20 = op2(e23,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f85,plain,
( e20 = op2(e20,e23)
| e20 = op2(e20,e22)
| e20 = op2(e20,e21)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f86,plain,
( e20 = op2(e23,e20)
| e20 = op2(e22,e20)
| e20 = op2(e21,e20)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f88,plain,
( e21 = op2(e23,e20)
| e21 = op2(e22,e20)
| e21 = op2(e21,e20)
| op2(e20,e20) = e21 ),
inference(cnf_transformation,[],[f4]) ).
fof(f91,plain,
( e23 = op2(e20,e23)
| e23 = op2(e20,e22)
| e23 = op2(e20,e21)
| op2(e20,e20) = e23 ),
inference(cnf_transformation,[],[f4]) ).
fof(f98,plain,
( e22 = op2(e23,e21)
| e22 = op2(e22,e21)
| e22 = op2(e21,e21)
| e22 = op2(e20,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f99,plain,
( e23 = op2(e21,e23)
| e23 = op2(e21,e22)
| e23 = op2(e21,e21)
| e23 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f103,plain,
( e21 = op2(e22,e23)
| e21 = op2(e22,e22)
| e21 = op2(e22,e21)
| e21 = op2(e22,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f105,plain,
( e22 = op2(e22,e23)
| e22 = op2(e22,e22)
| e22 = op2(e22,e21)
| e22 = op2(e22,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f106,plain,
( e22 = op2(e23,e22)
| e22 = op2(e22,e22)
| e22 = op2(e21,e22)
| e22 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f117,plain,
op1(e13,e12) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f123,plain,
op1(e12,e12) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f125,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f127,plain,
op1(e12,e10) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f132,plain,
op1(e11,e10) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f138,plain,
op1(e10,e10) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f146,plain,
op1(e10,e13) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f149,plain,
op1(e11,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f151,plain,
op1(e10,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f155,plain,
op1(e11,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f168,plain,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f169,plain,
op2(e23,e20) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f182,plain,
op2(e21,e20) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f187,plain,
op2(e20,e20) != op2(e20,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f188,plain,
op2(e20,e20) != op2(e20,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f189,plain,
op2(e22,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f197,plain,
op2(e21,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f198,plain,
op2(e20,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f199,plain,
op2(e20,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f203,plain,
op2(e21,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f206,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f208,plain,
op2(e21,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f210,plain,
op2(e20,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f213,plain,
e12 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f214,plain,
e11 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f215,plain,
e11 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f216,plain,
e10 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f217,plain,
e10 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f218,plain,
e10 != e11,
inference(cnf_transformation,[],[f7]) ).
fof(f219,plain,
e22 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f220,plain,
e21 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f221,plain,
e21 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f222,plain,
e20 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f223,plain,
e20 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f224,plain,
e20 != e21,
inference(cnf_transformation,[],[f8]) ).
fof(f245,plain,
( e10 = op1(e13,e13)
| e10 = op1(e12,e12)
| e10 = op1(e11,e11)
| e10 != op1(e10,e10) ),
inference(cnf_transformation,[],[f10]) ).
fof(f246,plain,
( e10 = op1(e13,e13)
| e10 = op1(e12,e12)
| e10 = op1(e11,e11)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f10]) ).
fof(f261,plain,
( e11 = op1(e13,e13)
| e11 = op1(e12,e12)
| e11 = op1(e11,e11)
| e10 != op1(e11,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f269,plain,
( e13 != op1(e11,e11)
| e11 = op1(e12,e12)
| e11 = op1(e11,e11)
| e10 != op1(e11,e11) ),
inference(cnf_transformation,[],[f10]) ).
fof(f286,plain,
( e13 != op1(e12,e12)
| e12 = op1(e12,e12)
| e12 = op1(e11,e11)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f10]) ).
fof(f292,plain,
( e13 = op1(e13,e13)
| e12 != op1(e13,e13)
| e11 != op1(e13,e13)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f10]) ).
fof(f309,plain,
( e20 = op2(e23,e23)
| e20 = op2(e22,e22)
| e20 = op2(e21,e21)
| e20 != op2(e20,e20) ),
inference(cnf_transformation,[],[f11]) ).
fof(f310,plain,
( e20 = op2(e23,e23)
| e20 = op2(e22,e22)
| e20 = op2(e21,e21)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f11]) ).
fof(f334,plain,
( e23 != op2(e21,e21)
| e21 = op2(e22,e22)
| e21 = op2(e21,e21)
| op2(e20,e20) = e21 ),
inference(cnf_transformation,[],[f11]) ).
fof(f350,plain,
( e23 != op2(e22,e22)
| e22 = op2(e22,e22)
| e22 = op2(e21,e21)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f11]) ).
fof(f369,plain,
e13 = op1(e12,e12),
inference(cnf_transformation,[],[f12]) ).
fof(f371,plain,
e10 = op1(op1(e12,e12),e12),
inference(cnf_transformation,[],[f12]) ).
fof(f372,plain,
e23 = op2(e22,e22),
inference(cnf_transformation,[],[f13]) ).
fof(f373,plain,
e21 = op2(op2(e22,e22),op2(e22,e22)),
inference(cnf_transformation,[],[f13]) ).
fof(f374,plain,
e20 = op2(op2(e22,e22),e22),
inference(cnf_transformation,[],[f13]) ).
fof(f379,plain,
op2(e21,e21) = h2(e13),
inference(cnf_transformation,[],[f15]) ).
fof(f380,plain,
h2(e11) = op2(op2(e21,e21),op2(e21,e21)),
inference(cnf_transformation,[],[f15]) ).
fof(f381,plain,
h2(e10) = op2(op2(e21,e21),e21),
inference(cnf_transformation,[],[f15]) ).
fof(f382,plain,
e21 = h2(e12),
inference(cnf_transformation,[],[f15]) ).
fof(f390,plain,
e23 = h4(e12),
inference(cnf_transformation,[],[f17]) ).
fof(f399,plain,
( e20 != h2(e13)
| ~ sP5 ),
inference(cnf_transformation,[],[f20]) ).
fof(f404,plain,
( e21 != h2(e12)
| ~ sP4 ),
inference(cnf_transformation,[],[f20]) ).
fof(f441,plain,
( e23 != h2(e10)
| e22 != h2(e11)
| sP4
| sP5
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(cnf_transformation,[],[f20]) ).
fof(f516,plain,
( e23 != h2(e10)
| e22 != h2(e11)
| sP4
| ~ sP5
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(consistent_polarity_flipping,[],[f441]) ).
fof(f526,plain,
( e20 != h2(e13)
| sP5 ),
inference(consistent_polarity_flipping,[],[f399]) ).
fof(f576,definition,
( spl8_11
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl8_11])],[avatar_definition]) ).
fof(f580,definition,
( spl8_12
<=> e20 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl8_12])],[avatar_definition]) ).
fof(f581,plain,
( e20 = h2(e13)
| ~ spl8_12 ),
inference(avatar_component_clause,[],[f580]) ).
fof(f583,plain,
( spl8_11
| ~ spl8_12 ),
inference(avatar_split_clause,[],[f526,f580,f576]) ).
fof(f600,definition,
( spl8_16
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl8_16])],[avatar_definition]) ).
fof(f609,definition,
( spl8_18
<=> e21 = h2(e12) ),
introduced(definition,[new_symbols(definition,[spl8_18])],[avatar_definition]) ).
fof(f610,plain,
( e21 = h2(e12)
| ~ spl8_18 ),
inference(avatar_component_clause,[],[f609]) ).
fof(f612,plain,
( ~ spl8_16
| ~ spl8_18 ),
inference(avatar_split_clause,[],[f404,f609,f600]) ).
fof(f681,definition,
( spl8_33
<=> e20 = h4(e12) ),
introduced(definition,[new_symbols(definition,[spl8_33])],[avatar_definition]) ).
fof(f682,plain,
( e20 = h4(e12)
| ~ spl8_33 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f683,plain,
( e20 != h4(e12)
| spl8_33 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f832,definition,
( spl8_65
<=> h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_65])],[avatar_definition]) ).
fof(f834,plain,
( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| spl8_65 ),
inference(avatar_component_clause,[],[f832]) ).
fof(f836,definition,
( spl8_66
<=> h2(op1(e10,e11)) = op2(h2(e10),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_66])],[avatar_definition]) ).
fof(f838,plain,
( h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| spl8_66 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f840,definition,
( spl8_67
<=> h2(op1(e10,e12)) = op2(h2(e10),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_67])],[avatar_definition]) ).
fof(f842,plain,
( h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| spl8_67 ),
inference(avatar_component_clause,[],[f840]) ).
fof(f844,definition,
( spl8_68
<=> h2(op1(e10,e13)) = op2(h2(e10),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_68])],[avatar_definition]) ).
fof(f846,plain,
( h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| spl8_68 ),
inference(avatar_component_clause,[],[f844]) ).
fof(f848,definition,
( spl8_69
<=> h2(op1(e11,e10)) = op2(h2(e11),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_69])],[avatar_definition]) ).
fof(f850,plain,
( h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| spl8_69 ),
inference(avatar_component_clause,[],[f848]) ).
fof(f852,definition,
( spl8_70
<=> h2(op1(e11,e11)) = op2(h2(e11),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_70])],[avatar_definition]) ).
fof(f854,plain,
( h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| spl8_70 ),
inference(avatar_component_clause,[],[f852]) ).
fof(f856,definition,
( spl8_71
<=> h2(op1(e11,e12)) = op2(h2(e11),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_71])],[avatar_definition]) ).
fof(f858,plain,
( h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| spl8_71 ),
inference(avatar_component_clause,[],[f856]) ).
fof(f860,definition,
( spl8_72
<=> h2(op1(e11,e13)) = op2(h2(e11),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_72])],[avatar_definition]) ).
fof(f862,plain,
( h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| spl8_72 ),
inference(avatar_component_clause,[],[f860]) ).
fof(f864,definition,
( spl8_73
<=> h2(op1(e12,e10)) = op2(h2(e12),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_73])],[avatar_definition]) ).
fof(f866,plain,
( h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| spl8_73 ),
inference(avatar_component_clause,[],[f864]) ).
fof(f868,definition,
( spl8_74
<=> h2(op1(e12,e11)) = op2(h2(e12),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_74])],[avatar_definition]) ).
fof(f870,plain,
( h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| spl8_74 ),
inference(avatar_component_clause,[],[f868]) ).
fof(f872,definition,
( spl8_75
<=> h2(op1(e12,e12)) = op2(h2(e12),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_75])],[avatar_definition]) ).
fof(f874,plain,
( h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| spl8_75 ),
inference(avatar_component_clause,[],[f872]) ).
fof(f876,definition,
( spl8_76
<=> h2(op1(e12,e13)) = op2(h2(e12),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_76])],[avatar_definition]) ).
fof(f878,plain,
( h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| spl8_76 ),
inference(avatar_component_clause,[],[f876]) ).
fof(f880,definition,
( spl8_77
<=> h2(op1(e13,e10)) = op2(h2(e13),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_77])],[avatar_definition]) ).
fof(f882,plain,
( h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| spl8_77 ),
inference(avatar_component_clause,[],[f880]) ).
fof(f884,definition,
( spl8_78
<=> h2(op1(e13,e11)) = op2(h2(e13),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_78])],[avatar_definition]) ).
fof(f886,plain,
( h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| spl8_78 ),
inference(avatar_component_clause,[],[f884]) ).
fof(f888,definition,
( spl8_79
<=> h2(op1(e13,e12)) = op2(h2(e13),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_79])],[avatar_definition]) ).
fof(f890,plain,
( h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| spl8_79 ),
inference(avatar_component_clause,[],[f888]) ).
fof(f892,definition,
( spl8_80
<=> h2(op1(e13,e13)) = op2(h2(e13),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_80])],[avatar_definition]) ).
fof(f894,plain,
( h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| spl8_80 ),
inference(avatar_component_clause,[],[f892]) ).
fof(f900,definition,
( spl8_82
<=> e23 = h2(e10) ),
introduced(definition,[new_symbols(definition,[spl8_82])],[avatar_definition]) ).
fof(f901,plain,
( e23 = h2(e10)
| ~ spl8_82 ),
inference(avatar_component_clause,[],[f900]) ).
fof(f910,definition,
( spl8_84
<=> e22 = h2(e11) ),
introduced(definition,[new_symbols(definition,[spl8_84])],[avatar_definition]) ).
fof(f911,plain,
( e22 = h2(e11)
| ~ spl8_84 ),
inference(avatar_component_clause,[],[f910]) ).
fof(f913,plain,
( ~ spl8_65
| ~ spl8_66
| ~ spl8_67
| ~ spl8_68
| ~ spl8_69
| ~ spl8_70
| ~ spl8_71
| ~ spl8_72
| ~ spl8_73
| ~ spl8_74
| ~ spl8_75
| ~ spl8_76
| ~ spl8_77
| ~ spl8_78
| ~ spl8_79
| ~ spl8_80
| ~ spl8_11
| spl8_16
| ~ spl8_84
| ~ spl8_82 ),
inference(avatar_split_clause,[],[f516,f900,f910,f600,f576,f892,f888,f884,f880,f876,f872,f868,f864,f860,f856,f852,f848,f844,f840,f836,f832]) ).
fof(f1152,definition,
( spl8_135
<=> e23 = h4(e12) ),
introduced(definition,[new_symbols(definition,[spl8_135])],[avatar_definition]) ).
fof(f1153,plain,
( e23 = h4(e12)
| ~ spl8_135 ),
inference(avatar_component_clause,[],[f1152]) ).
fof(f1167,plain,
spl8_135,
inference(avatar_split_clause,[],[f390,f1152]) ).
fof(f1169,plain,
spl8_18,
inference(avatar_split_clause,[],[f382,f609]) ).
fof(f1172,definition,
( spl8_137
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl8_137])],[avatar_definition]) ).
fof(f1173,plain,
( e20 = op2(e20,e20)
| ~ spl8_137 ),
inference(avatar_component_clause,[],[f1172]) ).
fof(f1176,definition,
( spl8_138
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_138])],[avatar_definition]) ).
fof(f1178,plain,
( e20 = op2(e21,e21)
| ~ spl8_138 ),
inference(avatar_component_clause,[],[f1176]) ).
fof(f1180,definition,
( spl8_139
<=> op2(e20,e20) = e22 ),
introduced(definition,[new_symbols(definition,[spl8_139])],[avatar_definition]) ).
fof(f1181,plain,
( op2(e20,e20) = e22
| ~ spl8_139 ),
inference(avatar_component_clause,[],[f1180]) ).
fof(f1184,definition,
( spl8_140
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl8_140])],[avatar_definition]) ).
fof(f1186,plain,
( e20 = op2(e23,e23)
| ~ spl8_140 ),
inference(avatar_component_clause,[],[f1184]) ).
fof(f1190,definition,
( spl8_141
<=> op2(e20,e20) = e21 ),
introduced(definition,[new_symbols(definition,[spl8_141])],[avatar_definition]) ).
fof(f1191,plain,
( op2(e20,e20) = e21
| ~ spl8_141 ),
inference(avatar_component_clause,[],[f1190]) ).
fof(f1196,definition,
( spl8_142
<=> e20 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl8_142])],[avatar_definition]) ).
fof(f1198,plain,
( e20 = op2(e22,e22)
| ~ spl8_142 ),
inference(avatar_component_clause,[],[f1196]) ).
fof(f1199,plain,
( ~ spl8_137
| spl8_138
| spl8_142
| spl8_140 ),
inference(avatar_split_clause,[],[f309,f1184,f1196,f1176,f1172]) ).
fof(f1200,plain,
( spl8_137
| spl8_138
| spl8_142
| spl8_140 ),
inference(avatar_split_clause,[],[f310,f1184,f1196,f1176,f1172]) ).
fof(f1204,definition,
( spl8_143
<=> op2(e20,e20) = e23 ),
introduced(definition,[new_symbols(definition,[spl8_143])],[avatar_definition]) ).
fof(f1205,plain,
( op2(e20,e20) = e23
| ~ spl8_143 ),
inference(avatar_component_clause,[],[f1204]) ).
fof(f1216,definition,
( spl8_144
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_144])],[avatar_definition]) ).
fof(f1220,definition,
( spl8_145
<=> e22 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_145])],[avatar_definition]) ).
fof(f1221,plain,
( e22 = op2(e21,e21)
| ~ spl8_145 ),
inference(avatar_component_clause,[],[f1220]) ).
fof(f1224,definition,
( spl8_146
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl8_146])],[avatar_definition]) ).
fof(f1226,plain,
( e21 = op2(e23,e23)
| ~ spl8_146 ),
inference(avatar_component_clause,[],[f1224]) ).
fof(f1232,definition,
( spl8_147
<=> e21 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl8_147])],[avatar_definition]) ).
fof(f1234,plain,
( e21 = op2(e22,e22)
| ~ spl8_147 ),
inference(avatar_component_clause,[],[f1232]) ).
fof(f1240,definition,
( spl8_148
<=> e23 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_148])],[avatar_definition]) ).
fof(f1248,plain,
( spl8_141
| spl8_144
| spl8_147
| ~ spl8_148 ),
inference(avatar_split_clause,[],[f334,f1240,f1232,f1216,f1190]) ).
fof(f1252,definition,
( spl8_149
<=> e22 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl8_149])],[avatar_definition]) ).
fof(f1253,plain,
( e22 = op2(e22,e22)
| ~ spl8_149 ),
inference(avatar_component_clause,[],[f1252]) ).
fof(f1268,definition,
( spl8_151
<=> e23 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl8_151])],[avatar_definition]) ).
fof(f1269,plain,
( e23 = op2(e22,e22)
| ~ spl8_151 ),
inference(avatar_component_clause,[],[f1268]) ).
fof(f1276,plain,
( spl8_139
| spl8_145
| spl8_149
| ~ spl8_151 ),
inference(avatar_split_clause,[],[f350,f1268,f1252,f1220,f1180]) ).
fof(f1300,definition,
( spl8_153
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl8_153])],[avatar_definition]) ).
fof(f1301,plain,
( e10 = op1(e10,e10)
| ~ spl8_153 ),
inference(avatar_component_clause,[],[f1300]) ).
fof(f1304,definition,
( spl8_154
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_154])],[avatar_definition]) ).
fof(f1306,plain,
( e10 = op1(e11,e11)
| ~ spl8_154 ),
inference(avatar_component_clause,[],[f1304]) ).
fof(f1308,definition,
( spl8_155
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[spl8_155])],[avatar_definition]) ).
fof(f1309,plain,
( op1(e10,e10) = e12
| ~ spl8_155 ),
inference(avatar_component_clause,[],[f1308]) ).
fof(f1312,definition,
( spl8_156
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_156])],[avatar_definition]) ).
fof(f1314,plain,
( e10 = op1(e13,e13)
| ~ spl8_156 ),
inference(avatar_component_clause,[],[f1312]) ).
fof(f1318,definition,
( spl8_157
<=> op1(e10,e10) = e11 ),
introduced(definition,[new_symbols(definition,[spl8_157])],[avatar_definition]) ).
fof(f1319,plain,
( op1(e10,e10) = e11
| ~ spl8_157 ),
inference(avatar_component_clause,[],[f1318]) ).
fof(f1324,definition,
( spl8_158
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl8_158])],[avatar_definition]) ).
fof(f1326,plain,
( e10 = op1(e12,e12)
| ~ spl8_158 ),
inference(avatar_component_clause,[],[f1324]) ).
fof(f1327,plain,
( ~ spl8_153
| spl8_154
| spl8_158
| spl8_156 ),
inference(avatar_split_clause,[],[f245,f1312,f1324,f1304,f1300]) ).
fof(f1328,plain,
( spl8_153
| spl8_154
| spl8_158
| spl8_156 ),
inference(avatar_split_clause,[],[f246,f1312,f1324,f1304,f1300]) ).
fof(f1332,definition,
( spl8_159
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl8_159])],[avatar_definition]) ).
fof(f1333,plain,
( op1(e10,e10) = e13
| ~ spl8_159 ),
inference(avatar_component_clause,[],[f1332]) ).
fof(f1344,definition,
( spl8_160
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_160])],[avatar_definition]) ).
fof(f1346,plain,
( e11 = op1(e11,e11)
| ~ spl8_160 ),
inference(avatar_component_clause,[],[f1344]) ).
fof(f1348,definition,
( spl8_161
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_161])],[avatar_definition]) ).
fof(f1349,plain,
( e12 = op1(e11,e11)
| ~ spl8_161 ),
inference(avatar_component_clause,[],[f1348]) ).
fof(f1352,definition,
( spl8_162
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_162])],[avatar_definition]) ).
fof(f1354,plain,
( e11 = op1(e13,e13)
| ~ spl8_162 ),
inference(avatar_component_clause,[],[f1352]) ).
fof(f1360,definition,
( spl8_163
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl8_163])],[avatar_definition]) ).
fof(f1362,plain,
( e11 = op1(e12,e12)
| ~ spl8_163 ),
inference(avatar_component_clause,[],[f1360]) ).
fof(f1363,plain,
( ~ spl8_154
| spl8_160
| spl8_163
| spl8_162 ),
inference(avatar_split_clause,[],[f261,f1352,f1360,f1344,f1304]) ).
fof(f1368,definition,
( spl8_164
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_164])],[avatar_definition]) ).
fof(f1375,plain,
( ~ spl8_154
| spl8_160
| spl8_163
| ~ spl8_164 ),
inference(avatar_split_clause,[],[f269,f1368,f1360,f1344,f1304]) ).
fof(f1380,definition,
( spl8_165
<=> e12 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl8_165])],[avatar_definition]) ).
fof(f1381,plain,
( e12 = op1(e12,e12)
| ~ spl8_165 ),
inference(avatar_component_clause,[],[f1380]) ).
fof(f1384,definition,
( spl8_166
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_166])],[avatar_definition]) ).
fof(f1396,definition,
( spl8_167
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl8_167])],[avatar_definition]) ).
fof(f1397,plain,
( e13 = op1(e12,e12)
| ~ spl8_167 ),
inference(avatar_component_clause,[],[f1396]) ).
fof(f1404,plain,
( spl8_155
| spl8_161
| spl8_165
| ~ spl8_167 ),
inference(avatar_split_clause,[],[f286,f1396,f1380,f1348,f1308]) ).
fof(f1408,definition,
( spl8_168
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_168])],[avatar_definition]) ).
fof(f1410,plain,
( e13 = op1(e13,e13)
| ~ spl8_168 ),
inference(avatar_component_clause,[],[f1408]) ).
fof(f1414,plain,
( spl8_159
| ~ spl8_162
| ~ spl8_166
| spl8_168 ),
inference(avatar_split_clause,[],[f292,f1408,f1384,f1352,f1332]) ).
fof(f1428,definition,
( spl8_169
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl8_169])],[avatar_definition]) ).
fof(f1432,definition,
( spl8_170
<=> e20 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_170])],[avatar_definition]) ).
fof(f1436,definition,
( spl8_171
<=> e20 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl8_171])],[avatar_definition]) ).
fof(f1438,plain,
( e20 = op2(e20,e23)
| ~ spl8_171 ),
inference(avatar_component_clause,[],[f1436]) ).
fof(f1439,plain,
( spl8_137
| spl8_169
| spl8_170
| spl8_171 ),
inference(avatar_split_clause,[],[f85,f1436,f1432,f1428,f1172]) ).
fof(f1441,definition,
( spl8_172
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl8_172])],[avatar_definition]) ).
fof(f1445,definition,
( spl8_173
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_173])],[avatar_definition]) ).
fof(f1447,plain,
( e20 = op2(e22,e20)
| ~ spl8_173 ),
inference(avatar_component_clause,[],[f1445]) ).
fof(f1449,definition,
( spl8_174
<=> e20 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_174])],[avatar_definition]) ).
fof(f1452,plain,
( spl8_137
| spl8_172
| spl8_173
| spl8_174 ),
inference(avatar_split_clause,[],[f86,f1449,f1445,f1441,f1172]) ).
fof(f1458,definition,
( spl8_176
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_176])],[avatar_definition]) ).
fof(f1467,definition,
( spl8_178
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl8_178])],[avatar_definition]) ).
fof(f1471,definition,
( spl8_179
<=> e21 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_179])],[avatar_definition]) ).
fof(f1473,plain,
( e21 = op2(e22,e20)
| ~ spl8_179 ),
inference(avatar_component_clause,[],[f1471]) ).
fof(f1475,definition,
( spl8_180
<=> e21 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_180])],[avatar_definition]) ).
fof(f1478,plain,
( spl8_141
| spl8_178
| spl8_179
| spl8_180 ),
inference(avatar_split_clause,[],[f88,f1475,f1471,f1467,f1190]) ).
fof(f1480,definition,
( spl8_181
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl8_181])],[avatar_definition]) ).
fof(f1484,definition,
( spl8_182
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_182])],[avatar_definition]) ).
fof(f1497,definition,
( spl8_185
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_185])],[avatar_definition]) ).
fof(f1499,plain,
( e22 = op2(e22,e20)
| ~ spl8_185 ),
inference(avatar_component_clause,[],[f1497]) ).
fof(f1501,definition,
( spl8_186
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_186])],[avatar_definition]) ).
fof(f1506,definition,
( spl8_187
<=> e23 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl8_187])],[avatar_definition]) ).
fof(f1508,plain,
( e23 = op2(e20,e21)
| ~ spl8_187 ),
inference(avatar_component_clause,[],[f1506]) ).
fof(f1510,definition,
( spl8_188
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_188])],[avatar_definition]) ).
fof(f1514,definition,
( spl8_189
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl8_189])],[avatar_definition]) ).
fof(f1516,plain,
( e23 = op2(e20,e23)
| ~ spl8_189 ),
inference(avatar_component_clause,[],[f1514]) ).
fof(f1517,plain,
( spl8_143
| spl8_187
| spl8_188
| spl8_189 ),
inference(avatar_split_clause,[],[f91,f1514,f1510,f1506,f1204]) ).
fof(f1519,definition,
( spl8_190
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl8_190])],[avatar_definition]) ).
fof(f1527,definition,
( spl8_192
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_192])],[avatar_definition]) ).
fof(f1529,plain,
( e23 = op2(e23,e20)
| ~ spl8_192 ),
inference(avatar_component_clause,[],[f1527]) ).
fof(f1559,definition,
( spl8_199
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl8_199])],[avatar_definition]) ).
fof(f1561,plain,
( e21 = op2(e22,e21)
| ~ spl8_199 ),
inference(avatar_component_clause,[],[f1559]) ).
fof(f1568,definition,
( spl8_201
<=> e22 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl8_201])],[avatar_definition]) ).
fof(f1577,definition,
( spl8_203
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl8_203])],[avatar_definition]) ).
fof(f1579,plain,
( e22 = op2(e22,e21)
| ~ spl8_203 ),
inference(avatar_component_clause,[],[f1577]) ).
fof(f1581,definition,
( spl8_204
<=> e22 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl8_204])],[avatar_definition]) ).
fof(f1583,plain,
( e22 = op2(e23,e21)
| ~ spl8_204 ),
inference(avatar_component_clause,[],[f1581]) ).
fof(f1584,plain,
( spl8_181
| spl8_145
| spl8_203
| spl8_204 ),
inference(avatar_split_clause,[],[f98,f1581,f1577,f1220,f1480]) ).
fof(f1586,definition,
( spl8_205
<=> e23 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl8_205])],[avatar_definition]) ).
fof(f1590,definition,
( spl8_206
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_206])],[avatar_definition]) ).
fof(f1593,plain,
( spl8_190
| spl8_148
| spl8_205
| spl8_206 ),
inference(avatar_split_clause,[],[f99,f1590,f1586,f1240,f1519]) ).
fof(f1609,definition,
( spl8_210
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_210])],[avatar_definition]) ).
fof(f1611,plain,
( e20 = op2(e23,e22)
| ~ spl8_210 ),
inference(avatar_component_clause,[],[f1609]) ).
fof(f1614,definition,
( spl8_211
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl8_211])],[avatar_definition]) ).
fof(f1617,plain,
( spl8_179
| spl8_199
| spl8_147
| spl8_211 ),
inference(avatar_split_clause,[],[f103,f1614,f1232,f1559,f1471]) ).
fof(f1624,definition,
( spl8_213
<=> e22 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl8_213])],[avatar_definition]) ).
fof(f1626,plain,
( e22 = op2(e22,e23)
| ~ spl8_213 ),
inference(avatar_component_clause,[],[f1624]) ).
fof(f1627,plain,
( spl8_185
| spl8_203
| spl8_149
| spl8_213 ),
inference(avatar_split_clause,[],[f105,f1624,f1252,f1577,f1497]) ).
fof(f1629,definition,
( spl8_214
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_214])],[avatar_definition]) ).
fof(f1632,plain,
( spl8_182
| spl8_201
| spl8_149
| spl8_214 ),
inference(avatar_split_clause,[],[f106,f1629,f1252,f1568,f1484]) ).
fof(f1653,plain,
( spl8_170
| spl8_176
| spl8_182
| spl8_188 ),
inference(avatar_split_clause,[],[f71,f1510,f1484,f1458,f1432]) ).
fof(f1663,plain,
( spl8_174
| spl8_180
| spl8_186
| spl8_192 ),
inference(avatar_split_clause,[],[f81,f1527,f1501,f1475,f1449]) ).
fof(f1668,definition,
( spl8_217
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl8_217])],[avatar_definition]) ).
fof(f1670,plain,
( e10 = op1(e10,e11)
| ~ spl8_217 ),
inference(avatar_component_clause,[],[f1668]) ).
fof(f1672,definition,
( spl8_218
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_218])],[avatar_definition]) ).
fof(f1674,plain,
( e10 = op1(e10,e12)
| ~ spl8_218 ),
inference(avatar_component_clause,[],[f1672]) ).
fof(f1676,definition,
( spl8_219
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl8_219])],[avatar_definition]) ).
fof(f1678,plain,
( e10 = op1(e10,e13)
| ~ spl8_219 ),
inference(avatar_component_clause,[],[f1676]) ).
fof(f1679,plain,
( spl8_153
| spl8_217
| spl8_218
| spl8_219 ),
inference(avatar_split_clause,[],[f37,f1676,f1672,f1668,f1300]) ).
fof(f1681,definition,
( spl8_220
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_220])],[avatar_definition]) ).
fof(f1683,plain,
( e10 = op1(e11,e10)
| ~ spl8_220 ),
inference(avatar_component_clause,[],[f1681]) ).
fof(f1685,definition,
( spl8_221
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl8_221])],[avatar_definition]) ).
fof(f1687,plain,
( e10 = op1(e12,e10)
| ~ spl8_221 ),
inference(avatar_component_clause,[],[f1685]) ).
fof(f1689,definition,
( spl8_222
<=> e10 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_222])],[avatar_definition]) ).
fof(f1691,plain,
( e10 = op1(e13,e10)
| ~ spl8_222 ),
inference(avatar_component_clause,[],[f1689]) ).
fof(f1692,plain,
( spl8_153
| spl8_220
| spl8_221
| spl8_222 ),
inference(avatar_split_clause,[],[f38,f1689,f1685,f1681,f1300]) ).
fof(f1694,definition,
( spl8_223
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl8_223])],[avatar_definition]) ).
fof(f1696,plain,
( e11 = op1(e10,e11)
| ~ spl8_223 ),
inference(avatar_component_clause,[],[f1694]) ).
fof(f1698,definition,
( spl8_224
<=> e11 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_224])],[avatar_definition]) ).
fof(f1700,plain,
( e11 = op1(e10,e12)
| ~ spl8_224 ),
inference(avatar_component_clause,[],[f1698]) ).
fof(f1702,definition,
( spl8_225
<=> e11 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl8_225])],[avatar_definition]) ).
fof(f1704,plain,
( e11 = op1(e10,e13)
| ~ spl8_225 ),
inference(avatar_component_clause,[],[f1702]) ).
fof(f1705,plain,
( spl8_157
| spl8_223
| spl8_224
| spl8_225 ),
inference(avatar_split_clause,[],[f39,f1702,f1698,f1694,f1318]) ).
fof(f1707,definition,
( spl8_226
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_226])],[avatar_definition]) ).
fof(f1709,plain,
( e11 = op1(e11,e10)
| ~ spl8_226 ),
inference(avatar_component_clause,[],[f1707]) ).
fof(f1711,definition,
( spl8_227
<=> e11 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl8_227])],[avatar_definition]) ).
fof(f1713,plain,
( e11 = op1(e12,e10)
| ~ spl8_227 ),
inference(avatar_component_clause,[],[f1711]) ).
fof(f1715,definition,
( spl8_228
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_228])],[avatar_definition]) ).
fof(f1717,plain,
( e11 = op1(e13,e10)
| ~ spl8_228 ),
inference(avatar_component_clause,[],[f1715]) ).
fof(f1718,plain,
( spl8_157
| spl8_226
| spl8_227
| spl8_228 ),
inference(avatar_split_clause,[],[f40,f1715,f1711,f1707,f1318]) ).
fof(f1724,definition,
( spl8_230
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_230])],[avatar_definition]) ).
fof(f1726,plain,
( e12 = op1(e10,e12)
| ~ spl8_230 ),
inference(avatar_component_clause,[],[f1724]) ).
fof(f1728,definition,
( spl8_231
<=> e12 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl8_231])],[avatar_definition]) ).
fof(f1730,plain,
( e12 = op1(e10,e13)
| ~ spl8_231 ),
inference(avatar_component_clause,[],[f1728]) ).
fof(f1741,definition,
( spl8_234
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_234])],[avatar_definition]) ).
fof(f1743,plain,
( e12 = op1(e13,e10)
| ~ spl8_234 ),
inference(avatar_component_clause,[],[f1741]) ).
fof(f1746,definition,
( spl8_235
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl8_235])],[avatar_definition]) ).
fof(f1748,plain,
( e13 = op1(e10,e11)
| ~ spl8_235 ),
inference(avatar_component_clause,[],[f1746]) ).
fof(f1750,definition,
( spl8_236
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_236])],[avatar_definition]) ).
fof(f1754,definition,
( spl8_237
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl8_237])],[avatar_definition]) ).
fof(f1756,plain,
( e13 = op1(e10,e13)
| ~ spl8_237 ),
inference(avatar_component_clause,[],[f1754]) ).
fof(f1757,plain,
( spl8_159
| spl8_235
| spl8_236
| spl8_237 ),
inference(avatar_split_clause,[],[f43,f1754,f1750,f1746,f1332]) ).
fof(f1759,definition,
( spl8_238
<=> e13 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_238])],[avatar_definition]) ).
fof(f1761,plain,
( e13 = op1(e11,e10)
| ~ spl8_238 ),
inference(avatar_component_clause,[],[f1759]) ).
fof(f1763,definition,
( spl8_239
<=> e13 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl8_239])],[avatar_definition]) ).
fof(f1767,definition,
( spl8_240
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_240])],[avatar_definition]) ).
fof(f1769,plain,
( e13 = op1(e13,e10)
| ~ spl8_240 ),
inference(avatar_component_clause,[],[f1767]) ).
fof(f1770,plain,
( spl8_159
| spl8_238
| spl8_239
| spl8_240 ),
inference(avatar_split_clause,[],[f44,f1767,f1763,f1759,f1332]) ).
fof(f1781,definition,
( spl8_243
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_243])],[avatar_definition]) ).
fof(f1783,plain,
( e10 = op1(e12,e11)
| ~ spl8_243 ),
inference(avatar_component_clause,[],[f1781]) ).
fof(f1790,definition,
( spl8_245
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl8_245])],[avatar_definition]) ).
fof(f1792,plain,
( e11 = op1(e11,e12)
| ~ spl8_245 ),
inference(avatar_component_clause,[],[f1790]) ).
fof(f1794,definition,
( spl8_246
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_246])],[avatar_definition]) ).
fof(f1796,plain,
( e11 = op1(e11,e13)
| ~ spl8_246 ),
inference(avatar_component_clause,[],[f1794]) ).
fof(f1797,plain,
( spl8_226
| spl8_160
| spl8_245
| spl8_246 ),
inference(avatar_split_clause,[],[f47,f1794,f1790,f1344,f1707]) ).
fof(f1799,definition,
( spl8_247
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_247])],[avatar_definition]) ).
fof(f1801,plain,
( e11 = op1(e12,e11)
| ~ spl8_247 ),
inference(avatar_component_clause,[],[f1799]) ).
fof(f1803,definition,
( spl8_248
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_248])],[avatar_definition]) ).
fof(f1805,plain,
( e11 = op1(e13,e11)
| ~ spl8_248 ),
inference(avatar_component_clause,[],[f1803]) ).
fof(f1806,plain,
( spl8_223
| spl8_160
| spl8_247
| spl8_248 ),
inference(avatar_split_clause,[],[f48,f1803,f1799,f1344,f1694]) ).
fof(f1808,definition,
( spl8_249
<=> e12 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl8_249])],[avatar_definition]) ).
fof(f1810,plain,
( e12 = op1(e11,e12)
| ~ spl8_249 ),
inference(avatar_component_clause,[],[f1808]) ).
fof(f1812,definition,
( spl8_250
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_250])],[avatar_definition]) ).
fof(f1814,plain,
( e12 = op1(e11,e13)
| ~ spl8_250 ),
inference(avatar_component_clause,[],[f1812]) ).
fof(f1821,definition,
( spl8_252
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_252])],[avatar_definition]) ).
fof(f1823,plain,
( e12 = op1(e13,e11)
| ~ spl8_252 ),
inference(avatar_component_clause,[],[f1821]) ).
fof(f1826,definition,
( spl8_253
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl8_253])],[avatar_definition]) ).
fof(f1830,definition,
( spl8_254
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_254])],[avatar_definition]) ).
fof(f1832,plain,
( e13 = op1(e11,e13)
| ~ spl8_254 ),
inference(avatar_component_clause,[],[f1830]) ).
fof(f1833,plain,
( spl8_238
| spl8_164
| spl8_253
| spl8_254 ),
inference(avatar_split_clause,[],[f51,f1830,f1826,f1368,f1759]) ).
fof(f1835,definition,
( spl8_255
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_255])],[avatar_definition]) ).
fof(f1839,definition,
( spl8_256
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_256])],[avatar_definition]) ).
fof(f1841,plain,
( e13 = op1(e13,e11)
| ~ spl8_256 ),
inference(avatar_component_clause,[],[f1839]) ).
fof(f1842,plain,
( spl8_235
| spl8_164
| spl8_255
| spl8_256 ),
inference(avatar_split_clause,[],[f52,f1839,f1835,f1368,f1746]) ).
fof(f1844,definition,
( spl8_257
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl8_257])],[avatar_definition]) ).
fof(f1846,plain,
( e10 = op1(e12,e13)
| ~ spl8_257 ),
inference(avatar_component_clause,[],[f1844]) ).
fof(f1847,plain,
( spl8_221
| spl8_243
| spl8_158
| spl8_257 ),
inference(avatar_split_clause,[],[f53,f1844,f1324,f1781,f1685]) ).
fof(f1849,definition,
( spl8_258
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_258])],[avatar_definition]) ).
fof(f1851,plain,
( e10 = op1(e13,e12)
| ~ spl8_258 ),
inference(avatar_component_clause,[],[f1849]) ).
fof(f1859,definition,
( spl8_260
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_260])],[avatar_definition]) ).
fof(f1861,plain,
( e11 = op1(e13,e12)
| ~ spl8_260 ),
inference(avatar_component_clause,[],[f1859]) ).
fof(f1862,plain,
( spl8_224
| spl8_245
| spl8_163
| spl8_260 ),
inference(avatar_split_clause,[],[f56,f1859,f1360,f1790,f1698]) ).
fof(f1864,definition,
( spl8_261
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl8_261])],[avatar_definition]) ).
fof(f1866,plain,
( e12 = op1(e12,e13)
| ~ spl8_261 ),
inference(avatar_component_clause,[],[f1864]) ).
fof(f1869,definition,
( spl8_262
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_262])],[avatar_definition]) ).
fof(f1871,plain,
( e12 = op1(e13,e12)
| ~ spl8_262 ),
inference(avatar_component_clause,[],[f1869]) ).
fof(f1872,plain,
( spl8_230
| spl8_249
| spl8_165
| spl8_262 ),
inference(avatar_split_clause,[],[f58,f1869,f1380,f1808,f1724]) ).
fof(f1874,definition,
( spl8_263
<=> e13 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl8_263])],[avatar_definition]) ).
fof(f1887,plain,
( spl8_234
| spl8_252
| spl8_262
| spl8_166 ),
inference(avatar_split_clause,[],[f65,f1384,f1869,f1821,f1741]) ).
fof(f1888,plain,
( spl8_231
| spl8_250
| spl8_261
| spl8_166 ),
inference(avatar_split_clause,[],[f66,f1384,f1864,f1812,f1728]) ).
fof(f1890,plain,
( spl8_237
| spl8_254
| spl8_263
| spl8_168 ),
inference(avatar_split_clause,[],[f68,f1408,f1874,f1830,f1754]) ).
fof(f1908,plain,
( e20 != e23
| spl8_33
| ~ spl8_135 ),
inference(superposition,[],[f683,f1153]) ).
fof(f1909,plain,
( h2(op1(e12,e11)) != op2(e21,h2(e11))
| ~ spl8_18
| spl8_74 ),
inference(forward_demodulation,[],[f870,f610]) ).
fof(f1910,plain,
spl8_167,
inference(avatar_split_clause,[],[f369,f1396]) ).
fof(f1911,plain,
spl8_151,
inference(avatar_split_clause,[],[f372,f1268]) ).
fof(f1942,plain,
( e20 = e23
| ~ spl8_142
| ~ spl8_151 ),
inference(superposition,[],[f1269,f1198]) ).
fof(f1947,plain,
( $false
| spl8_33
| ~ spl8_135
| ~ spl8_142
| ~ spl8_151 ),
inference(forward_subsumption_resolution,[],[f1942,f1908]) ).
fof(f1948,plain,
( spl8_33
| ~ spl8_135
| ~ spl8_142
| ~ spl8_151 ),
inference(avatar_contradiction_clause,[],[f1947]) ).
fof(f1949,plain,
( e20 = e23
| ~ spl8_33
| ~ spl8_135 ),
inference(forward_demodulation,[],[f682,f1153]) ).
fof(f1961,plain,
( e20 != e23
| spl8_33
| ~ spl8_135 ),
inference(forward_demodulation,[],[f683,f1153]) ).
fof(f2001,plain,
( e10 = e13
| ~ spl8_158
| ~ spl8_167 ),
inference(forward_demodulation,[],[f1397,f1326]) ).
fof(f2002,plain,
( $false
| ~ spl8_158
| ~ spl8_167 ),
inference(forward_subsumption_resolution,[],[f2001,f216]) ).
fof(f2003,plain,
( ~ spl8_158
| ~ spl8_167 ),
inference(avatar_contradiction_clause,[],[f2002]) ).
fof(f2072,plain,
( e20 = e21
| ~ spl8_173
| ~ spl8_179 ),
inference(superposition,[],[f1447,f1473]) ).
fof(f2076,plain,
( $false
| ~ spl8_173
| ~ spl8_179 ),
inference(forward_subsumption_resolution,[],[f2072,f224]) ).
fof(f2077,plain,
( ~ spl8_173
| ~ spl8_179 ),
inference(avatar_contradiction_clause,[],[f2076]) ).
fof(f2145,plain,
( e21 = e22
| ~ spl8_199
| ~ spl8_203 ),
inference(superposition,[],[f1579,f1561]) ).
fof(f2150,plain,
( $false
| ~ spl8_199
| ~ spl8_203 ),
inference(forward_subsumption_resolution,[],[f2145,f221]) ).
fof(f2151,plain,
( ~ spl8_199
| ~ spl8_203 ),
inference(avatar_contradiction_clause,[],[f2150]) ).
fof(f2248,plain,
( e20 = e22
| ~ spl8_173
| ~ spl8_185 ),
inference(superposition,[],[f1499,f1447]) ).
fof(f2252,plain,
( $false
| ~ spl8_173
| ~ spl8_185 ),
inference(forward_subsumption_resolution,[],[f2248,f223]) ).
fof(f2253,plain,
( ~ spl8_173
| ~ spl8_185 ),
inference(avatar_contradiction_clause,[],[f2252]) ).
fof(f2260,plain,
( e22 = e23
| ~ spl8_149
| ~ spl8_151 ),
inference(superposition,[],[f1253,f1269]) ).
fof(f2264,plain,
( $false
| ~ spl8_149
| ~ spl8_151 ),
inference(forward_subsumption_resolution,[],[f2260,f219]) ).
fof(f2265,plain,
( ~ spl8_149
| ~ spl8_151 ),
inference(avatar_contradiction_clause,[],[f2264]) ).
fof(f2269,plain,
( e20 = e23
| ~ spl8_171
| ~ spl8_189 ),
inference(superposition,[],[f1516,f1438]) ).
fof(f2274,plain,
( $false
| spl8_33
| ~ spl8_135
| ~ spl8_171
| ~ spl8_189 ),
inference(forward_subsumption_resolution,[],[f2269,f1961]) ).
fof(f2275,plain,
( spl8_33
| ~ spl8_135
| ~ spl8_171
| ~ spl8_189 ),
inference(avatar_contradiction_clause,[],[f2274]) ).
fof(f2368,plain,
( e20 = e22
| ~ spl8_138
| ~ spl8_145 ),
inference(forward_demodulation,[],[f1178,f1221]) ).
fof(f2369,plain,
( e20 = e21
| ~ spl8_140
| ~ spl8_146 ),
inference(forward_demodulation,[],[f1226,f1186]) ).
fof(f2372,plain,
( $false
| ~ spl8_138
| ~ spl8_145 ),
inference(forward_subsumption_resolution,[],[f2368,f223]) ).
fof(f2373,plain,
( ~ spl8_138
| ~ spl8_145 ),
inference(avatar_contradiction_clause,[],[f2372]) ).
fof(f2374,plain,
( $false
| ~ spl8_140
| ~ spl8_146 ),
inference(forward_subsumption_resolution,[],[f2369,f224]) ).
fof(f2375,plain,
( ~ spl8_140
| ~ spl8_146 ),
inference(avatar_contradiction_clause,[],[f2374]) ).
fof(f2378,plain,
( e21 = e23
| ~ spl8_147
| ~ spl8_151 ),
inference(forward_demodulation,[],[f1234,f1269]) ).
fof(f2380,plain,
( $false
| ~ spl8_147
| ~ spl8_151 ),
inference(forward_subsumption_resolution,[],[f2378,f220]) ).
fof(f2381,plain,
( ~ spl8_147
| ~ spl8_151 ),
inference(avatar_contradiction_clause,[],[f2380]) ).
fof(f2464,plain,
( e10 = e13
| ~ spl8_217
| ~ spl8_235 ),
inference(forward_demodulation,[],[f1748,f1670]) ).
fof(f2465,plain,
( $false
| ~ spl8_217
| ~ spl8_235 ),
inference(forward_subsumption_resolution,[],[f2464,f216]) ).
fof(f2466,plain,
( ~ spl8_217
| ~ spl8_235 ),
inference(avatar_contradiction_clause,[],[f2465]) ).
fof(f2483,plain,
( e11 = e12
| ~ spl8_224
| ~ spl8_230 ),
inference(superposition,[],[f1726,f1700]) ).
fof(f2487,plain,
( $false
| ~ spl8_224
| ~ spl8_230 ),
inference(forward_subsumption_resolution,[],[f2483,f215]) ).
fof(f2488,plain,
( ~ spl8_224
| ~ spl8_230 ),
inference(avatar_contradiction_clause,[],[f2487]) ).
fof(f2495,plain,
( e10 = e11
| ~ spl8_221
| ~ spl8_227 ),
inference(superposition,[],[f1713,f1687]) ).
fof(f2496,plain,
( $false
| ~ spl8_221
| ~ spl8_227 ),
inference(forward_subsumption_resolution,[],[f2495,f218]) ).
fof(f2497,plain,
( ~ spl8_221
| ~ spl8_227 ),
inference(avatar_contradiction_clause,[],[f2496]) ).
fof(f2523,plain,
( e11 = e12
| ~ spl8_248
| ~ spl8_252 ),
inference(superposition,[],[f1823,f1805]) ).
fof(f2528,plain,
( $false
| ~ spl8_248
| ~ spl8_252 ),
inference(forward_subsumption_resolution,[],[f2523,f215]) ).
fof(f2529,plain,
( ~ spl8_248
| ~ spl8_252 ),
inference(avatar_contradiction_clause,[],[f2528]) ).
fof(f2535,plain,
( h2(e11) != op2(e21,h2(e11))
| ~ spl8_18
| spl8_74
| ~ spl8_247 ),
inference(superposition,[],[f1909,f1801]) ).
fof(f2546,plain,
( e11 = e13
| ~ spl8_246
| ~ spl8_254 ),
inference(forward_demodulation,[],[f1832,f1796]) ).
fof(f2547,plain,
( $false
| ~ spl8_246
| ~ spl8_254 ),
inference(forward_subsumption_resolution,[],[f2546,f214]) ).
fof(f2548,plain,
( ~ spl8_246
| ~ spl8_254 ),
inference(avatar_contradiction_clause,[],[f2547]) ).
fof(f2549,plain,
( e10 = e12
| ~ spl8_154
| ~ spl8_161 ),
inference(forward_demodulation,[],[f1306,f1349]) ).
fof(f2551,plain,
( $false
| ~ spl8_154
| ~ spl8_161 ),
inference(forward_subsumption_resolution,[],[f2549,f217]) ).
fof(f2552,plain,
( ~ spl8_154
| ~ spl8_161 ),
inference(avatar_contradiction_clause,[],[f2551]) ).
fof(f2560,plain,
( e10 = e12
| ~ spl8_222
| ~ spl8_234 ),
inference(superposition,[],[f1743,f1691]) ).
fof(f2564,plain,
( $false
| ~ spl8_222
| ~ spl8_234 ),
inference(forward_subsumption_resolution,[],[f2560,f217]) ).
fof(f2565,plain,
( ~ spl8_222
| ~ spl8_234 ),
inference(avatar_contradiction_clause,[],[f2564]) ).
fof(f2587,plain,
( e12 = e13
| ~ spl8_252
| ~ spl8_256 ),
inference(forward_demodulation,[],[f1841,f1823]) ).
fof(f2588,plain,
( $false
| ~ spl8_252
| ~ spl8_256 ),
inference(forward_subsumption_resolution,[],[f2587,f213]) ).
fof(f2589,plain,
( ~ spl8_252
| ~ spl8_256 ),
inference(avatar_contradiction_clause,[],[f2588]) ).
fof(f2599,plain,
( e10 = e11
| ~ spl8_258
| ~ spl8_260 ),
inference(forward_demodulation,[],[f1861,f1851]) ).
fof(f2600,plain,
( $false
| ~ spl8_258
| ~ spl8_260 ),
inference(forward_subsumption_resolution,[],[f2599,f218]) ).
fof(f2601,plain,
( ~ spl8_258
| ~ spl8_260 ),
inference(avatar_contradiction_clause,[],[f2600]) ).
fof(f2668,plain,
( e10 = e12
| ~ spl8_218
| ~ spl8_230 ),
inference(superposition,[],[f1674,f1726]) ).
fof(f2670,plain,
( $false
| ~ spl8_218
| ~ spl8_230 ),
inference(forward_subsumption_resolution,[],[f2668,f217]) ).
fof(f2671,plain,
( ~ spl8_218
| ~ spl8_230 ),
inference(avatar_contradiction_clause,[],[f2670]) ).
fof(f2674,plain,
( e11 = e13
| ~ spl8_226
| ~ spl8_238 ),
inference(superposition,[],[f1709,f1761]) ).
fof(f2680,plain,
( $false
| ~ spl8_226
| ~ spl8_238 ),
inference(forward_subsumption_resolution,[],[f2674,f214]) ).
fof(f2681,plain,
( ~ spl8_226
| ~ spl8_238 ),
inference(avatar_contradiction_clause,[],[f2680]) ).
fof(f2717,plain,
( e10 = e13
| ~ spl8_220
| ~ spl8_238 ),
inference(forward_demodulation,[],[f1761,f1683]) ).
fof(f2718,plain,
( $false
| ~ spl8_220
| ~ spl8_238 ),
inference(forward_subsumption_resolution,[],[f2717,f216]) ).
fof(f2719,plain,
( ~ spl8_220
| ~ spl8_238 ),
inference(avatar_contradiction_clause,[],[f2718]) ).
fof(f2721,plain,
( e12 = e13
| ~ spl8_234
| ~ spl8_240 ),
inference(forward_demodulation,[],[f1769,f1743]) ).
fof(f2722,plain,
( $false
| ~ spl8_234
| ~ spl8_240 ),
inference(forward_subsumption_resolution,[],[f2721,f213]) ).
fof(f2723,plain,
( ~ spl8_234
| ~ spl8_240 ),
inference(avatar_contradiction_clause,[],[f2722]) ).
fof(f2736,plain,
( e10 = e13
| ~ spl8_219
| ~ spl8_237 ),
inference(forward_demodulation,[],[f1756,f1678]) ).
fof(f2737,plain,
( $false
| ~ spl8_219
| ~ spl8_237 ),
inference(forward_subsumption_resolution,[],[f2736,f216]) ).
fof(f2738,plain,
( ~ spl8_219
| ~ spl8_237 ),
inference(avatar_contradiction_clause,[],[f2737]) ).
fof(f2763,plain,
( e11 = e12
| ~ spl8_228
| ~ spl8_234 ),
inference(forward_demodulation,[],[f1717,f1743]) ).
fof(f2764,plain,
( e12 = e13
| ~ spl8_250
| ~ spl8_254 ),
inference(forward_demodulation,[],[f1832,f1814]) ).
fof(f2765,plain,
( $false
| ~ spl8_228
| ~ spl8_234 ),
inference(forward_subsumption_resolution,[],[f2763,f215]) ).
fof(f2766,plain,
( ~ spl8_228
| ~ spl8_234 ),
inference(avatar_contradiction_clause,[],[f2765]) ).
fof(f2767,plain,
( $false
| ~ spl8_250
| ~ spl8_254 ),
inference(forward_subsumption_resolution,[],[f2764,f213]) ).
fof(f2768,plain,
( ~ spl8_250
| ~ spl8_254 ),
inference(avatar_contradiction_clause,[],[f2767]) ).
fof(f2821,plain,
( e10 = e11
| ~ spl8_219
| ~ spl8_225 ),
inference(superposition,[],[f1678,f1704]) ).
fof(f2825,plain,
( $false
| ~ spl8_219
| ~ spl8_225 ),
inference(forward_subsumption_resolution,[],[f2821,f218]) ).
fof(f2826,plain,
( ~ spl8_219
| ~ spl8_225 ),
inference(avatar_contradiction_clause,[],[f2825]) ).
fof(f2839,plain,
( e10 = e11
| ~ spl8_218
| ~ spl8_224 ),
inference(superposition,[],[f1674,f1700]) ).
fof(f2844,plain,
( $false
| ~ spl8_218
| ~ spl8_224 ),
inference(forward_subsumption_resolution,[],[f2839,f218]) ).
fof(f2845,plain,
( ~ spl8_218
| ~ spl8_224 ),
inference(avatar_contradiction_clause,[],[f2844]) ).
fof(f2871,plain,
( e10 = e12
| ~ spl8_257
| ~ spl8_261 ),
inference(superposition,[],[f1866,f1846]) ).
fof(f2875,plain,
( $false
| ~ spl8_257
| ~ spl8_261 ),
inference(forward_subsumption_resolution,[],[f2871,f217]) ).
fof(f2876,plain,
( ~ spl8_257
| ~ spl8_261 ),
inference(avatar_contradiction_clause,[],[f2875]) ).
fof(f2893,plain,
( e12 = e13
| ~ spl8_165
| ~ spl8_167 ),
inference(superposition,[],[f1381,f1397]) ).
fof(f2899,plain,
( $false
| ~ spl8_165
| ~ spl8_167 ),
inference(forward_subsumption_resolution,[],[f2893,f213]) ).
fof(f2900,plain,
( ~ spl8_165
| ~ spl8_167 ),
inference(avatar_contradiction_clause,[],[f2899]) ).
fof(f2902,plain,
( e11 = e13
| ~ spl8_223
| ~ spl8_235 ),
inference(superposition,[],[f1696,f1748]) ).
fof(f2908,plain,
( $false
| ~ spl8_223
| ~ spl8_235 ),
inference(forward_subsumption_resolution,[],[f2902,f214]) ).
fof(f2909,plain,
( ~ spl8_223
| ~ spl8_235 ),
inference(avatar_contradiction_clause,[],[f2908]) ).
fof(f2916,plain,
( e11 = e12
| ~ spl8_245
| ~ spl8_249 ),
inference(superposition,[],[f1810,f1792]) ).
fof(f2921,plain,
( $false
| ~ spl8_245
| ~ spl8_249 ),
inference(forward_subsumption_resolution,[],[f2916,f215]) ).
fof(f2922,plain,
( ~ spl8_245
| ~ spl8_249 ),
inference(avatar_contradiction_clause,[],[f2921]) ).
fof(f2945,plain,
( e20 = h2(e13)
| ~ spl8_138 ),
inference(forward_demodulation,[],[f379,f1178]) ).
fof(f2948,plain,
( spl8_12
| ~ spl8_138 ),
inference(avatar_split_clause,[],[f2945,f1176,f580]) ).
fof(f2954,plain,
( e10 != op1(e13,e12)
| ~ spl8_156 ),
inference(forward_demodulation,[],[f117,f1314]) ).
fof(f2963,plain,
( e13 != op1(e12,e11)
| ~ spl8_167 ),
inference(forward_demodulation,[],[f125,f1397]) ).
fof(f2966,plain,
( e13 != op1(e12,e10)
| ~ spl8_167 ),
inference(forward_demodulation,[],[f127,f1397]) ).
fof(f2975,plain,
( e13 != op1(e11,e10)
| ~ spl8_254 ),
inference(forward_demodulation,[],[f132,f1832]) ).
fof(f2983,plain,
( op1(e10,e10) != e12
| ~ spl8_231 ),
inference(forward_demodulation,[],[f138,f1730]) ).
fof(f2992,plain,
( e13 != op1(e10,e13)
| ~ spl8_254 ),
inference(forward_demodulation,[],[f146,f1832]) ).
fof(f2996,plain,
( e13 != op1(e11,e12)
| ~ spl8_167 ),
inference(forward_demodulation,[],[f149,f1397]) ).
fof(f2999,plain,
( e13 != op1(e10,e12)
| ~ spl8_167 ),
inference(forward_demodulation,[],[f151,f1397]) ).
fof(f3007,plain,
( e10 != op1(e11,e11)
| ~ spl8_243 ),
inference(forward_demodulation,[],[f155,f1783]) ).
fof(f3025,plain,
( e21 != op2(e23,e20)
| ~ spl8_146 ),
inference(forward_demodulation,[],[f168,f1226]) ).
fof(f3026,plain,
( e20 != op2(e23,e20)
| ~ spl8_210 ),
inference(forward_demodulation,[],[f169,f1611]) ).
fof(f3040,plain,
( e20 != op2(e21,e20)
| ~ spl8_138 ),
inference(forward_demodulation,[],[f182,f1178]) ).
fof(f3049,plain,
( e21 != op2(e22,e23)
| ~ spl8_146 ),
inference(forward_demodulation,[],[f189,f1226]) ).
fof(f3060,plain,
( e23 != op2(e21,e22)
| ~ spl8_151 ),
inference(forward_demodulation,[],[f197,f1269]) ).
fof(f3062,plain,
( e20 != op2(e20,e22)
| ~ spl8_210 ),
inference(forward_demodulation,[],[f198,f1611]) ).
fof(f3063,plain,
( e23 != op2(e20,e22)
| ~ spl8_151 ),
inference(forward_demodulation,[],[f199,f1269]) ).
fof(f3067,plain,
( e21 != op2(e21,e21)
| ~ spl8_199 ),
inference(forward_demodulation,[],[f203,f1561]) ).
fof(f3071,plain,
( e20 != op2(e20,e21)
| ~ spl8_138 ),
inference(forward_demodulation,[],[f206,f1178]) ).
fof(f3073,plain,
( e23 != op2(e21,e20)
| ~ spl8_192 ),
inference(forward_demodulation,[],[f208,f1529]) ).
fof(f3080,plain,
( e10 = op1(e13,e12)
| ~ spl8_167 ),
inference(forward_demodulation,[],[f371,f1397]) ).
fof(f3085,plain,
( e10 = e12
| ~ spl8_167
| ~ spl8_262 ),
inference(forward_demodulation,[],[f3080,f1871]) ).
fof(f3088,plain,
( $false
| ~ spl8_167
| ~ spl8_262 ),
inference(forward_subsumption_resolution,[],[f3085,f217]) ).
fof(f3089,plain,
( ~ spl8_167
| ~ spl8_262 ),
inference(avatar_contradiction_clause,[],[f3088]) ).
fof(f3091,plain,
( spl8_258
| ~ spl8_167 ),
inference(avatar_split_clause,[],[f3080,f1396,f1849]) ).
fof(f3092,plain,
( e13 != op1(e12,e13)
| ~ spl8_167 ),
inference(forward_demodulation,[],[f123,f1397]) ).
fof(f3093,plain,
( ~ spl8_253
| ~ spl8_167 ),
inference(avatar_split_clause,[],[f2996,f1396,f1826]) ).
fof(f3094,plain,
( ~ spl8_255
| ~ spl8_167 ),
inference(avatar_split_clause,[],[f2963,f1396,f1835]) ).
fof(f3095,plain,
( ~ spl8_239
| ~ spl8_167 ),
inference(avatar_split_clause,[],[f2966,f1396,f1763]) ).
fof(f3096,plain,
( ~ spl8_236
| ~ spl8_167 ),
inference(avatar_split_clause,[],[f2999,f1396,f1750]) ).
fof(f3098,plain,
( ~ spl8_263
| ~ spl8_167 ),
inference(avatar_split_clause,[],[f3092,f1396,f1874]) ).
fof(f3101,plain,
( e12 = e13
| ~ spl8_155
| ~ spl8_159 ),
inference(forward_demodulation,[],[f1333,f1309]) ).
fof(f3102,plain,
( $false
| ~ spl8_155
| ~ spl8_159 ),
inference(forward_subsumption_resolution,[],[f3101,f213]) ).
fof(f3103,plain,
( ~ spl8_155
| ~ spl8_159 ),
inference(avatar_contradiction_clause,[],[f3102]) ).
fof(f3105,plain,
( e10 = e11
| ~ spl8_154
| ~ spl8_160 ),
inference(forward_demodulation,[],[f1346,f1306]) ).
fof(f3107,plain,
( $false
| ~ spl8_154
| ~ spl8_160 ),
inference(forward_subsumption_resolution,[],[f3105,f218]) ).
fof(f3108,plain,
( ~ spl8_154
| ~ spl8_160 ),
inference(avatar_contradiction_clause,[],[f3107]) ).
fof(f3109,plain,
( ~ spl8_258
| ~ spl8_156 ),
inference(avatar_split_clause,[],[f2954,f1312,f1849]) ).
fof(f3113,plain,
( e11 = e12
| ~ spl8_155
| ~ spl8_157 ),
inference(forward_demodulation,[],[f1319,f1309]) ).
fof(f3117,plain,
( ~ spl8_154
| ~ spl8_243 ),
inference(avatar_split_clause,[],[f3007,f1781,f1304]) ).
fof(f3121,plain,
( ~ spl8_238
| ~ spl8_254 ),
inference(avatar_split_clause,[],[f2975,f1830,f1759]) ).
fof(f3123,plain,
( ~ spl8_237
| ~ spl8_254 ),
inference(avatar_split_clause,[],[f2992,f1830,f1754]) ).
fof(f3128,plain,
( $false
| ~ spl8_155
| ~ spl8_157 ),
inference(forward_subsumption_resolution,[],[f3113,f215]) ).
fof(f3129,plain,
( ~ spl8_155
| ~ spl8_157 ),
inference(avatar_contradiction_clause,[],[f3128]) ).
fof(f3133,plain,
( e11 = e13
| ~ spl8_163
| ~ spl8_167 ),
inference(superposition,[],[f1362,f1397]) ).
fof(f3139,plain,
( $false
| ~ spl8_163
| ~ spl8_167 ),
inference(forward_subsumption_resolution,[],[f3133,f214]) ).
fof(f3140,plain,
( ~ spl8_163
| ~ spl8_167 ),
inference(avatar_contradiction_clause,[],[f3139]) ).
fof(f3141,plain,
( e10 = e12
| ~ spl8_153
| ~ spl8_155 ),
inference(forward_demodulation,[],[f1301,f1309]) ).
fof(f3143,plain,
( $false
| ~ spl8_155
| ~ spl8_231 ),
inference(forward_subsumption_resolution,[],[f2983,f1309]) ).
fof(f3144,plain,
( ~ spl8_155
| ~ spl8_231 ),
inference(avatar_contradiction_clause,[],[f3143]) ).
fof(f3148,plain,
( $false
| ~ spl8_153
| ~ spl8_155 ),
inference(forward_subsumption_resolution,[],[f3141,f217]) ).
fof(f3149,plain,
( ~ spl8_153
| ~ spl8_155 ),
inference(avatar_contradiction_clause,[],[f3148]) ).
fof(f3154,plain,
( e11 = e13
| ~ spl8_162
| ~ spl8_168 ),
inference(forward_demodulation,[],[f1410,f1354]) ).
fof(f3155,plain,
( $false
| ~ spl8_162
| ~ spl8_168 ),
inference(forward_subsumption_resolution,[],[f3154,f214]) ).
fof(f3156,plain,
( ~ spl8_162
| ~ spl8_168 ),
inference(avatar_contradiction_clause,[],[f3155]) ).
fof(f3251,plain,
( e20 = op2(e23,e22)
| ~ spl8_151 ),
inference(forward_demodulation,[],[f374,f1269]) ).
fof(f3258,plain,
( op2(e20,e21) = h2(e10)
| ~ spl8_138 ),
inference(forward_demodulation,[],[f381,f1178]) ).
fof(f3259,plain,
( e23 = h2(e10)
| ~ spl8_138
| ~ spl8_187 ),
inference(forward_demodulation,[],[f3258,f1508]) ).
fof(f3260,plain,
( spl8_82
| ~ spl8_138
| ~ spl8_187 ),
inference(avatar_split_clause,[],[f3259,f1506,f1176,f900]) ).
fof(f3284,plain,
( e21 = op2(e23,e23)
| ~ spl8_151 ),
inference(forward_demodulation,[],[f373,f1269]) ).
fof(f3293,plain,
( op2(e20,e20) = h2(e11)
| ~ spl8_138 ),
inference(forward_demodulation,[],[f380,f1178]) ).
fof(f3294,plain,
( e22 = h2(e11)
| ~ spl8_138
| ~ spl8_139 ),
inference(forward_demodulation,[],[f3293,f1181]) ).
fof(f3295,plain,
( spl8_84
| ~ spl8_138
| ~ spl8_139 ),
inference(avatar_split_clause,[],[f3294,f1180,f1176,f910]) ).
fof(f3296,plain,
( e22 != op2(e21,e22)
| ~ spl8_18
| spl8_74
| ~ spl8_84
| ~ spl8_247 ),
inference(superposition,[],[f2535,f911]) ).
fof(f3300,plain,
( op2(e23,e23) != h2(op1(e10,e10))
| spl8_65
| ~ spl8_82 ),
inference(forward_demodulation,[],[f834,f901]) ).
fof(f3302,plain,
( op2(e23,e23) != h2(e12)
| spl8_65
| ~ spl8_82
| ~ spl8_155 ),
inference(forward_demodulation,[],[f3300,f1309]) ).
fof(f3304,plain,
( e21 != op2(e23,e23)
| ~ spl8_18
| spl8_65
| ~ spl8_82
| ~ spl8_155 ),
inference(forward_demodulation,[],[f3302,f610]) ).
fof(f3306,plain,
( $false
| ~ spl8_18
| spl8_65
| ~ spl8_82
| ~ spl8_146
| ~ spl8_155 ),
inference(forward_subsumption_resolution,[],[f3304,f1226]) ).
fof(f3307,plain,
( ~ spl8_18
| spl8_65
| ~ spl8_82
| ~ spl8_146
| ~ spl8_155 ),
inference(avatar_contradiction_clause,[],[f3306]) ).
fof(f3310,plain,
( h2(op1(e10,e11)) != op2(h2(e10),e22)
| spl8_66
| ~ spl8_84 ),
inference(forward_demodulation,[],[f838,f911]) ).
fof(f3312,plain,
( op2(e23,e22) != h2(op1(e10,e11))
| spl8_66
| ~ spl8_82
| ~ spl8_84 ),
inference(forward_demodulation,[],[f3310,f901]) ).
fof(f3314,plain,
( op2(e23,e22) != h2(e13)
| spl8_66
| ~ spl8_82
| ~ spl8_84
| ~ spl8_235 ),
inference(forward_demodulation,[],[f3312,f1748]) ).
fof(f3315,plain,
( e20 != op2(e23,e22)
| ~ spl8_12
| spl8_66
| ~ spl8_82
| ~ spl8_84
| ~ spl8_235 ),
inference(forward_demodulation,[],[f3314,f581]) ).
fof(f3316,plain,
( $false
| ~ spl8_12
| spl8_66
| ~ spl8_82
| ~ spl8_84
| ~ spl8_210
| ~ spl8_235 ),
inference(forward_subsumption_resolution,[],[f3315,f1611]) ).
fof(f3317,plain,
( ~ spl8_12
| spl8_66
| ~ spl8_82
| ~ spl8_84
| ~ spl8_210
| ~ spl8_235 ),
inference(avatar_contradiction_clause,[],[f3316]) ).
fof(f3319,plain,
( h2(op1(e10,e12)) != op2(h2(e10),e21)
| ~ spl8_18
| spl8_67 ),
inference(forward_demodulation,[],[f842,f610]) ).
fof(f3321,plain,
( op2(e23,e21) != h2(op1(e10,e12))
| ~ spl8_18
| spl8_67
| ~ spl8_82 ),
inference(forward_demodulation,[],[f3319,f901]) ).
fof(f3323,plain,
( op2(e23,e21) != h2(e11)
| ~ spl8_18
| spl8_67
| ~ spl8_82
| ~ spl8_224 ),
inference(forward_demodulation,[],[f3321,f1700]) ).
fof(f3325,plain,
( e22 != op2(e23,e21)
| ~ spl8_18
| spl8_67
| ~ spl8_82
| ~ spl8_84
| ~ spl8_224 ),
inference(forward_demodulation,[],[f3323,f911]) ).
fof(f3329,plain,
( h2(op1(e10,e13)) != op2(h2(e10),e20)
| ~ spl8_12
| spl8_68 ),
inference(forward_demodulation,[],[f846,f581]) ).
fof(f3331,plain,
( op2(e23,e20) != h2(op1(e10,e13))
| ~ spl8_12
| spl8_68
| ~ spl8_82 ),
inference(forward_demodulation,[],[f3329,f901]) ).
fof(f3333,plain,
( op2(e23,e20) != h2(e10)
| ~ spl8_12
| spl8_68
| ~ spl8_82
| ~ spl8_219 ),
inference(forward_demodulation,[],[f3331,f1678]) ).
fof(f3335,plain,
( e23 != op2(e23,e20)
| ~ spl8_12
| spl8_68
| ~ spl8_82
| ~ spl8_219 ),
inference(forward_demodulation,[],[f3333,f901]) ).
fof(f3339,plain,
( h2(op1(e11,e10)) != op2(h2(e11),e23)
| spl8_69
| ~ spl8_82 ),
inference(forward_demodulation,[],[f850,f901]) ).
fof(f3341,plain,
( op2(e22,e23) != h2(op1(e11,e10))
| spl8_69
| ~ spl8_82
| ~ spl8_84 ),
inference(forward_demodulation,[],[f3339,f911]) ).
fof(f3343,plain,
( op2(e22,e23) != h2(e11)
| spl8_69
| ~ spl8_82
| ~ spl8_84
| ~ spl8_226 ),
inference(forward_demodulation,[],[f3341,f1709]) ).
fof(f3345,plain,
( e22 != op2(e22,e23)
| spl8_69
| ~ spl8_82
| ~ spl8_84
| ~ spl8_226 ),
inference(forward_demodulation,[],[f3343,f911]) ).
fof(f3346,plain,
( $false
| spl8_69
| ~ spl8_82
| ~ spl8_84
| ~ spl8_213
| ~ spl8_226 ),
inference(forward_subsumption_resolution,[],[f3345,f1626]) ).
fof(f3347,plain,
( spl8_69
| ~ spl8_82
| ~ spl8_84
| ~ spl8_213
| ~ spl8_226 ),
inference(avatar_contradiction_clause,[],[f3346]) ).
fof(f3349,plain,
( op2(e22,e22) != h2(op1(e11,e11))
| spl8_70
| ~ spl8_84 ),
inference(forward_demodulation,[],[f854,f911]) ).
fof(f3351,plain,
( op2(e22,e22) != h2(e10)
| spl8_70
| ~ spl8_84
| ~ spl8_154 ),
inference(forward_demodulation,[],[f3349,f1306]) ).
fof(f3358,plain,
( h2(op1(e11,e12)) != op2(h2(e11),e21)
| ~ spl8_18
| spl8_71 ),
inference(forward_demodulation,[],[f858,f610]) ).
fof(f3360,plain,
( op2(e22,e21) != h2(op1(e11,e12))
| ~ spl8_18
| spl8_71
| ~ spl8_84 ),
inference(forward_demodulation,[],[f3358,f911]) ).
fof(f3362,plain,
( op2(e22,e21) != h2(e12)
| ~ spl8_18
| spl8_71
| ~ spl8_84
| ~ spl8_249 ),
inference(forward_demodulation,[],[f3360,f1810]) ).
fof(f3363,plain,
( e21 != op2(e22,e21)
| ~ spl8_18
| spl8_71
| ~ spl8_84
| ~ spl8_249 ),
inference(forward_demodulation,[],[f3362,f610]) ).
fof(f3367,plain,
( h2(op1(e11,e13)) != op2(h2(e11),e20)
| ~ spl8_12
| spl8_72 ),
inference(forward_demodulation,[],[f862,f581]) ).
fof(f3369,plain,
( op2(e22,e20) != h2(op1(e11,e13))
| ~ spl8_12
| spl8_72
| ~ spl8_84 ),
inference(forward_demodulation,[],[f3367,f911]) ).
fof(f3371,plain,
( op2(e22,e20) != h2(e13)
| ~ spl8_12
| spl8_72
| ~ spl8_84
| ~ spl8_254 ),
inference(forward_demodulation,[],[f3369,f1832]) ).
fof(f3373,plain,
( e20 != op2(e22,e20)
| ~ spl8_12
| spl8_72
| ~ spl8_84
| ~ spl8_254 ),
inference(forward_demodulation,[],[f3371,f581]) ).
fof(f3377,plain,
( h2(op1(e12,e10)) != op2(h2(e12),e23)
| spl8_73
| ~ spl8_82 ),
inference(forward_demodulation,[],[f866,f901]) ).
fof(f3379,plain,
( op2(e21,e23) != h2(op1(e12,e10))
| ~ spl8_18
| spl8_73
| ~ spl8_82 ),
inference(forward_demodulation,[],[f3377,f610]) ).
fof(f3381,plain,
( op2(e21,e23) != h2(e10)
| ~ spl8_18
| spl8_73
| ~ spl8_82
| ~ spl8_221 ),
inference(forward_demodulation,[],[f3379,f1687]) ).
fof(f3383,plain,
( e23 != op2(e21,e23)
| ~ spl8_18
| spl8_73
| ~ spl8_82
| ~ spl8_221 ),
inference(forward_demodulation,[],[f3381,f901]) ).
fof(f3387,plain,
( op2(e21,e21) != h2(op1(e12,e12))
| ~ spl8_18
| spl8_75 ),
inference(forward_demodulation,[],[f874,f610]) ).
fof(f3389,plain,
( op2(e21,e21) != h2(e13)
| ~ spl8_18
| spl8_75
| ~ spl8_167 ),
inference(forward_demodulation,[],[f3387,f1397]) ).
fof(f3391,plain,
( e20 != op2(e21,e21)
| ~ spl8_12
| ~ spl8_18
| spl8_75
| ~ spl8_167 ),
inference(forward_demodulation,[],[f3389,f581]) ).
fof(f3393,plain,
( $false
| ~ spl8_12
| ~ spl8_18
| spl8_75
| ~ spl8_138
| ~ spl8_167 ),
inference(forward_subsumption_resolution,[],[f3391,f1178]) ).
fof(f3394,plain,
( ~ spl8_12
| ~ spl8_18
| spl8_75
| ~ spl8_138
| ~ spl8_167 ),
inference(avatar_contradiction_clause,[],[f3393]) ).
fof(f3396,plain,
( h2(op1(e12,e13)) != op2(h2(e12),e20)
| ~ spl8_12
| spl8_76 ),
inference(forward_demodulation,[],[f878,f581]) ).
fof(f3398,plain,
( op2(e21,e20) != h2(op1(e12,e13))
| ~ spl8_12
| ~ spl8_18
| spl8_76 ),
inference(forward_demodulation,[],[f3396,f610]) ).
fof(f3400,plain,
( op2(e21,e20) != h2(e12)
| ~ spl8_12
| ~ spl8_18
| spl8_76
| ~ spl8_261 ),
inference(forward_demodulation,[],[f3398,f1866]) ).
fof(f3401,plain,
( e21 != op2(e21,e20)
| ~ spl8_12
| ~ spl8_18
| spl8_76
| ~ spl8_261 ),
inference(forward_demodulation,[],[f3400,f610]) ).
fof(f3405,plain,
( h2(op1(e13,e10)) != op2(h2(e13),e23)
| spl8_77
| ~ spl8_82 ),
inference(forward_demodulation,[],[f882,f901]) ).
fof(f3407,plain,
( op2(e20,e23) != h2(op1(e13,e10))
| ~ spl8_12
| spl8_77
| ~ spl8_82 ),
inference(forward_demodulation,[],[f3405,f581]) ).
fof(f3409,plain,
( op2(e20,e23) != h2(e13)
| ~ spl8_12
| spl8_77
| ~ spl8_82
| ~ spl8_240 ),
inference(forward_demodulation,[],[f3407,f1769]) ).
fof(f3411,plain,
( e20 != op2(e20,e23)
| ~ spl8_12
| spl8_77
| ~ spl8_82
| ~ spl8_240 ),
inference(forward_demodulation,[],[f3409,f581]) ).
fof(f3415,plain,
( h2(op1(e13,e11)) != op2(h2(e13),e22)
| spl8_78
| ~ spl8_84 ),
inference(forward_demodulation,[],[f886,f911]) ).
fof(f3417,plain,
( op2(e20,e22) != h2(op1(e13,e11))
| ~ spl8_12
| spl8_78
| ~ spl8_84 ),
inference(forward_demodulation,[],[f3415,f581]) ).
fof(f3419,plain,
( op2(e20,e22) != h2(e12)
| ~ spl8_12
| spl8_78
| ~ spl8_84
| ~ spl8_252 ),
inference(forward_demodulation,[],[f3417,f1823]) ).
fof(f3421,plain,
( e21 != op2(e20,e22)
| ~ spl8_12
| ~ spl8_18
| spl8_78
| ~ spl8_84
| ~ spl8_252 ),
inference(forward_demodulation,[],[f3419,f610]) ).
fof(f3425,plain,
( h2(op1(e13,e12)) != op2(h2(e13),e21)
| ~ spl8_18
| spl8_79 ),
inference(forward_demodulation,[],[f890,f610]) ).
fof(f3427,plain,
( op2(e20,e21) != h2(op1(e13,e12))
| ~ spl8_12
| ~ spl8_18
| spl8_79 ),
inference(forward_demodulation,[],[f3425,f581]) ).
fof(f3429,plain,
( op2(e20,e21) != h2(e10)
| ~ spl8_12
| ~ spl8_18
| spl8_79
| ~ spl8_258 ),
inference(forward_demodulation,[],[f3427,f1851]) ).
fof(f3431,plain,
( e23 != op2(e20,e21)
| ~ spl8_12
| ~ spl8_18
| spl8_79
| ~ spl8_82
| ~ spl8_258 ),
inference(forward_demodulation,[],[f3429,f901]) ).
fof(f3432,plain,
( $false
| ~ spl8_12
| ~ spl8_18
| spl8_79
| ~ spl8_82
| ~ spl8_187
| ~ spl8_258 ),
inference(forward_subsumption_resolution,[],[f3431,f1508]) ).
fof(f3433,plain,
( ~ spl8_12
| ~ spl8_18
| spl8_79
| ~ spl8_82
| ~ spl8_187
| ~ spl8_258 ),
inference(avatar_contradiction_clause,[],[f3432]) ).
fof(f3435,plain,
( op2(e20,e20) != h2(op1(e13,e13))
| ~ spl8_12
| spl8_80 ),
inference(forward_demodulation,[],[f894,f581]) ).
fof(f3437,plain,
( op2(e20,e20) != h2(e11)
| ~ spl8_12
| spl8_80
| ~ spl8_162 ),
inference(forward_demodulation,[],[f3435,f1354]) ).
fof(f3439,plain,
( op2(e20,e20) != e22
| ~ spl8_12
| spl8_80
| ~ spl8_84
| ~ spl8_162 ),
inference(forward_demodulation,[],[f3437,f911]) ).
fof(f3441,plain,
( $false
| ~ spl8_12
| spl8_80
| ~ spl8_84
| ~ spl8_139
| ~ spl8_162 ),
inference(forward_subsumption_resolution,[],[f3439,f1181]) ).
fof(f3442,plain,
( ~ spl8_12
| spl8_80
| ~ spl8_84
| ~ spl8_139
| ~ spl8_162 ),
inference(avatar_contradiction_clause,[],[f3441]) ).
fof(f3446,plain,
( ~ spl8_192
| ~ spl8_12
| spl8_68
| ~ spl8_82
| ~ spl8_219 ),
inference(avatar_split_clause,[],[f3335,f1676,f900,f844,f580,f1527]) ).
fof(f3455,plain,
( e22 != op2(e23,e20)
| ~ spl8_139 ),
inference(forward_demodulation,[],[f210,f1181]) ).
fof(f3456,plain,
( ~ spl8_180
| ~ spl8_146 ),
inference(avatar_split_clause,[],[f3025,f1224,f1475]) ).
fof(f3471,plain,
( ~ spl8_206
| ~ spl8_18
| spl8_73
| ~ spl8_82
| ~ spl8_221 ),
inference(avatar_split_clause,[],[f3383,f1685,f900,f864,f609,f1590]) ).
fof(f3475,plain,
( ~ spl8_178
| ~ spl8_12
| ~ spl8_18
| spl8_76
| ~ spl8_261 ),
inference(avatar_split_clause,[],[f3401,f1864,f876,f609,f580,f1467]) ).
fof(f3476,plain,
( e21 = e22
| ~ spl8_139
| ~ spl8_141 ),
inference(forward_demodulation,[],[f1191,f1181]) ).
fof(f3478,plain,
( e22 != op2(e23,e22)
| ~ spl8_204 ),
inference(forward_demodulation,[],[f167,f1583]) ).
fof(f3480,plain,
( spl8_210
| ~ spl8_151 ),
inference(avatar_split_clause,[],[f3251,f1268,f1609]) ).
fof(f3483,plain,
( ~ spl8_205
| ~ spl8_151 ),
inference(avatar_split_clause,[],[f3060,f1268,f1586]) ).
fof(f3485,plain,
( e22 != op2(e20,e21)
| ~ spl8_139 ),
inference(forward_demodulation,[],[f188,f1181]) ).
fof(f3487,plain,
( e22 != op2(e20,e22)
| ~ spl8_139 ),
inference(forward_demodulation,[],[f187,f1181]) ).
fof(f3495,plain,
( spl8_146
| ~ spl8_151 ),
inference(avatar_split_clause,[],[f3284,f1268,f1224]) ).
fof(f3499,plain,
( ~ spl8_144
| ~ spl8_199 ),
inference(avatar_split_clause,[],[f3067,f1559,f1216]) ).
fof(f3509,plain,
( $false
| ~ spl8_139
| ~ spl8_141 ),
inference(forward_subsumption_resolution,[],[f3476,f221]) ).
fof(f3510,plain,
( ~ spl8_139
| ~ spl8_141 ),
inference(avatar_contradiction_clause,[],[f3509]) ).
fof(f3514,plain,
( ~ spl8_182
| ~ spl8_139 ),
inference(avatar_split_clause,[],[f3487,f1180,f1484]) ).
fof(f3527,plain,
( ~ spl8_204
| ~ spl8_18
| spl8_67
| ~ spl8_82
| ~ spl8_84
| ~ spl8_224 ),
inference(avatar_split_clause,[],[f3325,f1698,f910,f900,f840,f609,f1581]) ).
fof(f3538,plain,
( e20 = e22
| ~ spl8_137
| ~ spl8_139 ),
inference(forward_demodulation,[],[f1173,f1181]) ).
fof(f3540,plain,
( ~ spl8_169
| ~ spl8_138 ),
inference(avatar_split_clause,[],[f3071,f1176,f1428]) ).
fof(f3552,plain,
( ~ spl8_190
| ~ spl8_192 ),
inference(avatar_split_clause,[],[f3073,f1527,f1519]) ).
fof(f3577,plain,
( $false
| ~ spl8_137
| ~ spl8_139 ),
inference(forward_subsumption_resolution,[],[f3538,f223]) ).
fof(f3578,plain,
( ~ spl8_137
| ~ spl8_139 ),
inference(avatar_contradiction_clause,[],[f3577]) ).
fof(f3612,plain,
( ~ spl8_199
| ~ spl8_18
| spl8_71
| ~ spl8_84
| ~ spl8_249 ),
inference(avatar_split_clause,[],[f3363,f1808,f910,f856,f609,f1559]) ).
fof(f3616,plain,
( ~ spl8_173
| ~ spl8_12
| spl8_72
| ~ spl8_84
| ~ spl8_254 ),
inference(avatar_split_clause,[],[f3373,f1830,f910,f860,f580,f1445]) ).
fof(f3620,plain,
( ~ spl8_171
| ~ spl8_12
| spl8_77
| ~ spl8_82
| ~ spl8_240 ),
inference(avatar_split_clause,[],[f3411,f1767,f900,f880,f580,f1436]) ).
fof(f3624,plain,
( ~ spl8_214
| ~ spl8_204 ),
inference(avatar_split_clause,[],[f3478,f1581,f1629]) ).
fof(f3628,plain,
( ~ spl8_211
| ~ spl8_146 ),
inference(avatar_split_clause,[],[f3049,f1224,f1614]) ).
fof(f3631,plain,
( ~ spl8_174
| ~ spl8_210 ),
inference(avatar_split_clause,[],[f3026,f1609,f1449]) ).
fof(f3632,plain,
( ~ spl8_170
| ~ spl8_210 ),
inference(avatar_split_clause,[],[f3062,f1609,f1432]) ).
fof(f3683,plain,
( ~ spl8_172
| ~ spl8_138 ),
inference(avatar_split_clause,[],[f3040,f1176,f1441]) ).
fof(f3716,plain,
( ~ spl8_176
| ~ spl8_12
| ~ spl8_18
| spl8_78
| ~ spl8_84
| ~ spl8_252 ),
inference(avatar_split_clause,[],[f3421,f1821,f910,f884,f609,f580,f1458]) ).
fof(f3722,plain,
( ~ spl8_188
| ~ spl8_151 ),
inference(avatar_split_clause,[],[f3063,f1268,f1510]) ).
fof(f3723,plain,
( ~ spl8_181
| ~ spl8_139 ),
inference(avatar_split_clause,[],[f3485,f1180,f1480]) ).
fof(f3804,plain,
( e22 = e23
| ~ spl8_139
| ~ spl8_143 ),
inference(forward_demodulation,[],[f1205,f1181]) ).
fof(f3810,plain,
( ~ spl8_186
| ~ spl8_139 ),
inference(avatar_split_clause,[],[f3455,f1180,f1501]) ).
fof(f3829,plain,
( $false
| ~ spl8_139
| ~ spl8_143 ),
inference(forward_subsumption_resolution,[],[f3804,f219]) ).
fof(f3830,plain,
( ~ spl8_139
| ~ spl8_143 ),
inference(avatar_contradiction_clause,[],[f3829]) ).
fof(f3841,plain,
( e23 != h2(e10)
| spl8_70
| ~ spl8_84
| ~ spl8_151
| ~ spl8_154 ),
inference(forward_demodulation,[],[f3351,f1269]) ).
fof(f3845,plain,
( ~ spl8_201
| ~ spl8_18
| spl8_74
| ~ spl8_84
| ~ spl8_247 ),
inference(avatar_split_clause,[],[f3296,f1799,f910,f868,f609,f1568]) ).
fof(f3866,plain,
( ~ spl8_82
| spl8_70
| ~ spl8_84
| ~ spl8_151
| ~ spl8_154 ),
inference(avatar_split_clause,[],[f3841,f1304,f1268,f910,f852,f900]) ).
fof(f3914,plain,
( $false
| ~ spl8_33
| ~ spl8_135 ),
inference(forward_subsumption_resolution,[],[f222,f1949]) ).
fof(f3915,plain,
( ~ spl8_33
| ~ spl8_135 ),
inference(avatar_contradiction_clause,[],[f3914]) ).
cnf(s9,plain,
( spl8_11
| ~ spl8_12 ),
inference(sat_conversion,[],[f583]) ).
cnf(s14,plain,
( ~ spl8_16
| ~ spl8_18 ),
inference(sat_conversion,[],[f612]) ).
cnf(s51,plain,
( ~ spl8_11
| spl8_16
| ~ spl8_65
| ~ spl8_66
| ~ spl8_67
| ~ spl8_68
| ~ spl8_69
| ~ spl8_70
| ~ spl8_71
| ~ spl8_72
| ~ spl8_73
| ~ spl8_74
| ~ spl8_75
| ~ spl8_76
| ~ spl8_77
| ~ spl8_78
| ~ spl8_79
| ~ spl8_80
| ~ spl8_82
| ~ spl8_84 ),
inference(sat_conversion,[],[f913]) ).
cnf(s97,plain,
spl8_135,
inference(sat_conversion,[],[f1167]) ).
cnf(s99,plain,
spl8_18,
inference(sat_conversion,[],[f1169]) ).
cnf(s105,plain,
( ~ spl8_137
| spl8_138
| spl8_140
| spl8_142 ),
inference(sat_conversion,[],[f1199]) ).
cnf(s106,plain,
( spl8_137
| spl8_138
| spl8_140
| spl8_142 ),
inference(sat_conversion,[],[f1200]) ).
cnf(s130,plain,
( spl8_141
| spl8_144
| spl8_147
| ~ spl8_148 ),
inference(sat_conversion,[],[f1248]) ).
cnf(s146,plain,
( spl8_139
| spl8_145
| spl8_149
| ~ spl8_151 ),
inference(sat_conversion,[],[f1276]) ).
cnf(s169,plain,
( ~ spl8_153
| spl8_154
| spl8_156
| spl8_158 ),
inference(sat_conversion,[],[f1327]) ).
cnf(s170,plain,
( spl8_153
| spl8_154
| spl8_156
| spl8_158 ),
inference(sat_conversion,[],[f1328]) ).
cnf(s185,plain,
( ~ spl8_154
| spl8_160
| spl8_162
| spl8_163 ),
inference(sat_conversion,[],[f1363]) ).
cnf(s193,plain,
( ~ spl8_154
| spl8_160
| spl8_163
| ~ spl8_164 ),
inference(sat_conversion,[],[f1375]) ).
cnf(s210,plain,
( spl8_155
| spl8_161
| spl8_165
| ~ spl8_167 ),
inference(sat_conversion,[],[f1404]) ).
cnf(s216,plain,
( spl8_159
| ~ spl8_162
| ~ spl8_166
| spl8_168 ),
inference(sat_conversion,[],[f1414]) ).
cnf(s229,plain,
( spl8_137
| spl8_169
| spl8_170
| spl8_171 ),
inference(sat_conversion,[],[f1439]) ).
cnf(s230,plain,
( spl8_137
| spl8_172
| spl8_173
| spl8_174 ),
inference(sat_conversion,[],[f1452]) ).
cnf(s232,plain,
( spl8_141
| spl8_178
| spl8_179
| spl8_180 ),
inference(sat_conversion,[],[f1478]) ).
cnf(s235,plain,
( spl8_143
| spl8_187
| spl8_188
| spl8_189 ),
inference(sat_conversion,[],[f1517]) ).
cnf(s242,plain,
( spl8_145
| spl8_181
| spl8_203
| spl8_204 ),
inference(sat_conversion,[],[f1584]) ).
cnf(s243,plain,
( spl8_148
| spl8_190
| spl8_205
| spl8_206 ),
inference(sat_conversion,[],[f1593]) ).
cnf(s247,plain,
( spl8_147
| spl8_179
| spl8_199
| spl8_211 ),
inference(sat_conversion,[],[f1617]) ).
cnf(s249,plain,
( spl8_149
| spl8_185
| spl8_203
| spl8_213 ),
inference(sat_conversion,[],[f1627]) ).
cnf(s250,plain,
( spl8_149
| spl8_182
| spl8_201
| spl8_214 ),
inference(sat_conversion,[],[f1632]) ).
cnf(s263,plain,
( spl8_170
| spl8_176
| spl8_182
| spl8_188 ),
inference(sat_conversion,[],[f1653]) ).
cnf(s273,plain,
( spl8_174
| spl8_180
| spl8_186
| spl8_192 ),
inference(sat_conversion,[],[f1663]) ).
cnf(s277,plain,
( spl8_153
| spl8_217
| spl8_218
| spl8_219 ),
inference(sat_conversion,[],[f1679]) ).
cnf(s278,plain,
( spl8_153
| spl8_220
| spl8_221
| spl8_222 ),
inference(sat_conversion,[],[f1692]) ).
cnf(s279,plain,
( spl8_157
| spl8_223
| spl8_224
| spl8_225 ),
inference(sat_conversion,[],[f1705]) ).
cnf(s280,plain,
( spl8_157
| spl8_226
| spl8_227
| spl8_228 ),
inference(sat_conversion,[],[f1718]) ).
cnf(s283,plain,
( spl8_159
| spl8_235
| spl8_236
| spl8_237 ),
inference(sat_conversion,[],[f1757]) ).
cnf(s284,plain,
( spl8_159
| spl8_238
| spl8_239
| spl8_240 ),
inference(sat_conversion,[],[f1770]) ).
cnf(s287,plain,
( spl8_160
| spl8_226
| spl8_245
| spl8_246 ),
inference(sat_conversion,[],[f1797]) ).
cnf(s288,plain,
( spl8_160
| spl8_223
| spl8_247
| spl8_248 ),
inference(sat_conversion,[],[f1806]) ).
cnf(s291,plain,
( spl8_164
| spl8_238
| spl8_253
| spl8_254 ),
inference(sat_conversion,[],[f1833]) ).
cnf(s292,plain,
( spl8_164
| spl8_235
| spl8_255
| spl8_256 ),
inference(sat_conversion,[],[f1842]) ).
cnf(s293,plain,
( spl8_158
| spl8_221
| spl8_243
| spl8_257 ),
inference(sat_conversion,[],[f1847]) ).
cnf(s296,plain,
( spl8_163
| spl8_224
| spl8_245
| spl8_260 ),
inference(sat_conversion,[],[f1862]) ).
cnf(s298,plain,
( spl8_165
| spl8_230
| spl8_249
| spl8_262 ),
inference(sat_conversion,[],[f1872]) ).
cnf(s305,plain,
( spl8_166
| spl8_234
| spl8_252
| spl8_262 ),
inference(sat_conversion,[],[f1887]) ).
cnf(s306,plain,
( spl8_166
| spl8_231
| spl8_250
| spl8_261 ),
inference(sat_conversion,[],[f1888]) ).
cnf(s308,plain,
( spl8_168
| spl8_237
| spl8_254
| spl8_263 ),
inference(sat_conversion,[],[f1890]) ).
cnf(s325,plain,
spl8_167,
inference(sat_conversion,[],[f1910]) ).
cnf(s326,plain,
spl8_151,
inference(sat_conversion,[],[f1911]) ).
cnf(s335,plain,
( spl8_33
| ~ spl8_135
| ~ spl8_142
| ~ spl8_151 ),
inference(sat_conversion,[],[f1948]) ).
cnf(s346,plain,
( ~ spl8_158
| ~ spl8_167 ),
inference(sat_conversion,[],[f2003]) ).
cnf(s364,plain,
( ~ spl8_173
| ~ spl8_179 ),
inference(sat_conversion,[],[f2077]) ).
cnf(s380,plain,
( ~ spl8_199
| ~ spl8_203 ),
inference(sat_conversion,[],[f2151]) ).
cnf(s404,plain,
( ~ spl8_173
| ~ spl8_185 ),
inference(sat_conversion,[],[f2253]) ).
cnf(s407,plain,
( ~ spl8_149
| ~ spl8_151 ),
inference(sat_conversion,[],[f2265]) ).
cnf(s409,plain,
( spl8_33
| ~ spl8_135
| ~ spl8_171
| ~ spl8_189 ),
inference(sat_conversion,[],[f2275]) ).
cnf(s424,plain,
( ~ spl8_138
| ~ spl8_145 ),
inference(sat_conversion,[],[f2373]) ).
cnf(s425,plain,
( ~ spl8_140
| ~ spl8_146 ),
inference(sat_conversion,[],[f2375]) ).
cnf(s427,plain,
( ~ spl8_147
| ~ spl8_151 ),
inference(sat_conversion,[],[f2381]) ).
cnf(s438,plain,
( ~ spl8_217
| ~ spl8_235 ),
inference(sat_conversion,[],[f2466]) ).
cnf(s444,plain,
( ~ spl8_224
| ~ spl8_230 ),
inference(sat_conversion,[],[f2488]) ).
cnf(s446,plain,
( ~ spl8_221
| ~ spl8_227 ),
inference(sat_conversion,[],[f2497]) ).
cnf(s454,plain,
( ~ spl8_248
| ~ spl8_252 ),
inference(sat_conversion,[],[f2529]) ).
cnf(s458,plain,
( ~ spl8_246
| ~ spl8_254 ),
inference(sat_conversion,[],[f2548]) ).
cnf(s459,plain,
( ~ spl8_154
| ~ spl8_161 ),
inference(sat_conversion,[],[f2552]) ).
cnf(s463,plain,
( ~ spl8_222
| ~ spl8_234 ),
inference(sat_conversion,[],[f2565]) ).
cnf(s467,plain,
( ~ spl8_252
| ~ spl8_256 ),
inference(sat_conversion,[],[f2589]) ).
cnf(s469,plain,
( ~ spl8_258
| ~ spl8_260 ),
inference(sat_conversion,[],[f2601]) ).
cnf(s485,plain,
( ~ spl8_218
| ~ spl8_230 ),
inference(sat_conversion,[],[f2671]) ).
cnf(s488,plain,
( ~ spl8_226
| ~ spl8_238 ),
inference(sat_conversion,[],[f2681]) ).
cnf(s495,plain,
( ~ spl8_220
| ~ spl8_238 ),
inference(sat_conversion,[],[f2719]) ).
cnf(s496,plain,
( ~ spl8_234
| ~ spl8_240 ),
inference(sat_conversion,[],[f2723]) ).
cnf(s499,plain,
( ~ spl8_219
| ~ spl8_237 ),
inference(sat_conversion,[],[f2738]) ).
cnf(s503,plain,
( ~ spl8_228
| ~ spl8_234 ),
inference(sat_conversion,[],[f2766]) ).
cnf(s504,plain,
( ~ spl8_250
| ~ spl8_254 ),
inference(sat_conversion,[],[f2768]) ).
cnf(s514,plain,
( ~ spl8_219
| ~ spl8_225 ),
inference(sat_conversion,[],[f2826]) ).
cnf(s517,plain,
( ~ spl8_218
| ~ spl8_224 ),
inference(sat_conversion,[],[f2845]) ).
cnf(s520,plain,
( ~ spl8_257
| ~ spl8_261 ),
inference(sat_conversion,[],[f2876]) ).
cnf(s526,plain,
( ~ spl8_165
| ~ spl8_167 ),
inference(sat_conversion,[],[f2900]) ).
cnf(s528,plain,
( ~ spl8_223
| ~ spl8_235 ),
inference(sat_conversion,[],[f2909]) ).
cnf(s530,plain,
( ~ spl8_245
| ~ spl8_249 ),
inference(sat_conversion,[],[f2922]) ).
cnf(s535,plain,
( spl8_12
| ~ spl8_138 ),
inference(sat_conversion,[],[f2948]) ).
cnf(s540,plain,
( ~ spl8_167
| ~ spl8_262 ),
inference(sat_conversion,[],[f3089]) ).
cnf(s541,plain,
( ~ spl8_167
| spl8_258 ),
inference(sat_conversion,[],[f3091]) ).
cnf(s542,plain,
( ~ spl8_167
| ~ spl8_253 ),
inference(sat_conversion,[],[f3093]) ).
cnf(s543,plain,
( ~ spl8_167
| ~ spl8_255 ),
inference(sat_conversion,[],[f3094]) ).
cnf(s544,plain,
( ~ spl8_167
| ~ spl8_239 ),
inference(sat_conversion,[],[f3095]) ).
cnf(s545,plain,
( ~ spl8_167
| ~ spl8_236 ),
inference(sat_conversion,[],[f3096]) ).
cnf(s547,plain,
( ~ spl8_167
| ~ spl8_263 ),
inference(sat_conversion,[],[f3098]) ).
cnf(s548,plain,
( ~ spl8_155
| ~ spl8_159 ),
inference(sat_conversion,[],[f3103]) ).
cnf(s549,plain,
( ~ spl8_154
| ~ spl8_160 ),
inference(sat_conversion,[],[f3108]) ).
cnf(s550,plain,
( ~ spl8_156
| ~ spl8_258 ),
inference(sat_conversion,[],[f3109]) ).
cnf(s556,plain,
( ~ spl8_154
| ~ spl8_243 ),
inference(sat_conversion,[],[f3117]) ).
cnf(s560,plain,
( ~ spl8_238
| ~ spl8_254 ),
inference(sat_conversion,[],[f3121]) ).
cnf(s562,plain,
( ~ spl8_237
| ~ spl8_254 ),
inference(sat_conversion,[],[f3123]) ).
cnf(s567,plain,
( ~ spl8_155
| ~ spl8_157 ),
inference(sat_conversion,[],[f3129]) ).
cnf(s569,plain,
( ~ spl8_163
| ~ spl8_167 ),
inference(sat_conversion,[],[f3140]) ).
cnf(s570,plain,
( ~ spl8_155
| ~ spl8_231 ),
inference(sat_conversion,[],[f3144]) ).
cnf(s575,plain,
( ~ spl8_153
| ~ spl8_155 ),
inference(sat_conversion,[],[f3149]) ).
cnf(s576,plain,
( ~ spl8_162
| ~ spl8_168 ),
inference(sat_conversion,[],[f3156]) ).
cnf(s578,plain,
( spl8_82
| ~ spl8_138
| ~ spl8_187 ),
inference(sat_conversion,[],[f3260]) ).
cnf(s583,plain,
( spl8_84
| ~ spl8_138
| ~ spl8_139 ),
inference(sat_conversion,[],[f3295]) ).
cnf(s585,plain,
( ~ spl8_18
| spl8_65
| ~ spl8_82
| ~ spl8_146
| ~ spl8_155 ),
inference(sat_conversion,[],[f3307]) ).
cnf(s586,plain,
( ~ spl8_12
| spl8_66
| ~ spl8_82
| ~ spl8_84
| ~ spl8_210
| ~ spl8_235 ),
inference(sat_conversion,[],[f3317]) ).
cnf(s589,plain,
( spl8_69
| ~ spl8_82
| ~ spl8_84
| ~ spl8_213
| ~ spl8_226 ),
inference(sat_conversion,[],[f3347]) ).
cnf(s594,plain,
( ~ spl8_12
| ~ spl8_18
| spl8_75
| ~ spl8_138
| ~ spl8_167 ),
inference(sat_conversion,[],[f3394]) ).
cnf(s598,plain,
( ~ spl8_12
| ~ spl8_18
| spl8_79
| ~ spl8_82
| ~ spl8_187
| ~ spl8_258 ),
inference(sat_conversion,[],[f3433]) ).
cnf(s599,plain,
( ~ spl8_12
| spl8_80
| ~ spl8_84
| ~ spl8_139
| ~ spl8_162 ),
inference(sat_conversion,[],[f3442]) ).
cnf(s600,plain,
( ~ spl8_12
| spl8_68
| ~ spl8_82
| ~ spl8_192
| ~ spl8_219 ),
inference(sat_conversion,[],[f3446]) ).
cnf(s603,plain,
( ~ spl8_146
| ~ spl8_180 ),
inference(sat_conversion,[],[f3456]) ).
cnf(s609,plain,
( ~ spl8_18
| spl8_73
| ~ spl8_82
| ~ spl8_206
| ~ spl8_221 ),
inference(sat_conversion,[],[f3471]) ).
cnf(s610,plain,
( ~ spl8_12
| ~ spl8_18
| spl8_76
| ~ spl8_178
| ~ spl8_261 ),
inference(sat_conversion,[],[f3475]) ).
cnf(s611,plain,
( ~ spl8_151
| spl8_210 ),
inference(sat_conversion,[],[f3480]) ).
cnf(s613,plain,
( ~ spl8_151
| ~ spl8_205 ),
inference(sat_conversion,[],[f3483]) ).
cnf(s618,plain,
( spl8_146
| ~ spl8_151 ),
inference(sat_conversion,[],[f3495]) ).
cnf(s621,plain,
( ~ spl8_144
| ~ spl8_199 ),
inference(sat_conversion,[],[f3499]) ).
cnf(s623,plain,
( ~ spl8_139
| ~ spl8_141 ),
inference(sat_conversion,[],[f3510]) ).
cnf(s626,plain,
( ~ spl8_139
| ~ spl8_182 ),
inference(sat_conversion,[],[f3514]) ).
cnf(s635,plain,
( ~ spl8_18
| spl8_67
| ~ spl8_82
| ~ spl8_84
| ~ spl8_204
| ~ spl8_224 ),
inference(sat_conversion,[],[f3527]) ).
cnf(s639,plain,
( ~ spl8_138
| ~ spl8_169 ),
inference(sat_conversion,[],[f3540]) ).
cnf(s647,plain,
( ~ spl8_190
| ~ spl8_192 ),
inference(sat_conversion,[],[f3552]) ).
cnf(s658,plain,
( ~ spl8_137
| ~ spl8_139 ),
inference(sat_conversion,[],[f3578]) ).
cnf(s681,plain,
( ~ spl8_18
| spl8_71
| ~ spl8_84
| ~ spl8_199
| ~ spl8_249 ),
inference(sat_conversion,[],[f3612]) ).
cnf(s682,plain,
( ~ spl8_12
| spl8_72
| ~ spl8_84
| ~ spl8_173
| ~ spl8_254 ),
inference(sat_conversion,[],[f3616]) ).
cnf(s683,plain,
( ~ spl8_12
| spl8_77
| ~ spl8_82
| ~ spl8_171
| ~ spl8_240 ),
inference(sat_conversion,[],[f3620]) ).
cnf(s685,plain,
( ~ spl8_204
| ~ spl8_214 ),
inference(sat_conversion,[],[f3624]) ).
cnf(s689,plain,
( ~ spl8_146
| ~ spl8_211 ),
inference(sat_conversion,[],[f3628]) ).
cnf(s692,plain,
( ~ spl8_174
| ~ spl8_210 ),
inference(sat_conversion,[],[f3631]) ).
cnf(s693,plain,
( ~ spl8_170
| ~ spl8_210 ),
inference(sat_conversion,[],[f3632]) ).
cnf(s725,plain,
( ~ spl8_138
| ~ spl8_172 ),
inference(sat_conversion,[],[f3683]) ).
cnf(s740,plain,
( ~ spl8_12
| ~ spl8_18
| spl8_78
| ~ spl8_84
| ~ spl8_176
| ~ spl8_252 ),
inference(sat_conversion,[],[f3716]) ).
cnf(s747,plain,
( ~ spl8_151
| ~ spl8_188 ),
inference(sat_conversion,[],[f3722]) ).
cnf(s748,plain,
( ~ spl8_139
| ~ spl8_181 ),
inference(sat_conversion,[],[f3723]) ).
cnf(s801,plain,
( ~ spl8_139
| ~ spl8_186 ),
inference(sat_conversion,[],[f3810]) ).
cnf(s809,plain,
( ~ spl8_139
| ~ spl8_143 ),
inference(sat_conversion,[],[f3830]) ).
cnf(s827,plain,
( ~ spl8_18
| spl8_74
| ~ spl8_84
| ~ spl8_201
| ~ spl8_247 ),
inference(sat_conversion,[],[f3845]) ).
cnf(s837,plain,
( spl8_70
| ~ spl8_82
| ~ spl8_84
| ~ spl8_151
| ~ spl8_154 ),
inference(sat_conversion,[],[f3866]) ).
cnf(s852,plain,
( ~ spl8_33
| ~ spl8_135 ),
inference(sat_conversion,[],[f3915]) ).
cnf(s853,plain,
~ spl8_188,
inference(rat,[],[s747,s326]) ).
cnf(s856,plain,
spl8_146,
inference(rat,[],[s618,s326]) ).
cnf(s857,plain,
~ spl8_205,
inference(rat,[],[s613,s326]) ).
cnf(s858,plain,
spl8_210,
inference(rat,[],[s611,s326]) ).
cnf(s861,plain,
~ spl8_147,
inference(rat,[],[s427,s326]) ).
cnf(s862,plain,
~ spl8_149,
inference(rat,[],[s407,s326]) ).
cnf(s863,plain,
~ spl8_211,
inference(rat,[],[s689,s856]) ).
cnf(s867,plain,
~ spl8_180,
inference(rat,[],[s603,s856]) ).
cnf(s870,plain,
~ spl8_140,
inference(rat,[],[s425,s856]) ).
cnf(s872,plain,
~ spl8_170,
inference(rat,[],[s693,s858]) ).
cnf(s873,plain,
~ spl8_174,
inference(rat,[],[s692,s858]) ).
cnf(s875,plain,
~ spl8_163,
inference(rat,[],[s569,s325]) ).
cnf(s876,plain,
~ spl8_263,
inference(rat,[],[s547,s325]) ).
cnf(s878,plain,
~ spl8_236,
inference(rat,[],[s545,s325]) ).
cnf(s879,plain,
~ spl8_239,
inference(rat,[],[s544,s325]) ).
cnf(s880,plain,
~ spl8_255,
inference(rat,[],[s543,s325]) ).
cnf(s881,plain,
~ spl8_253,
inference(rat,[],[s542,s325]) ).
cnf(s882,plain,
spl8_258,
inference(rat,[],[s541,s325]) ).
cnf(s883,plain,
~ spl8_262,
inference(rat,[],[s540,s325]) ).
cnf(s884,plain,
~ spl8_165,
inference(rat,[],[s526,s325]) ).
cnf(s885,plain,
~ spl8_158,
inference(rat,[],[s346,s325]) ).
cnf(s886,plain,
~ spl8_156,
inference(rat,[],[s550,s882]) ).
cnf(s887,plain,
~ spl8_260,
inference(rat,[],[s469,s882]) ).
cnf(s894,plain,
( spl8_168
| spl8_237
| spl8_254 ),
inference(rat,[],[s308,s876]) ).
cnf(s896,plain,
( spl8_166
| spl8_234
| spl8_252 ),
inference(rat,[],[s305,s883]) ).
cnf(s899,plain,
( spl8_230
| spl8_249 ),
inference(rat,[],[s298,s883,s884]) ).
cnf(s901,plain,
( spl8_224
| spl8_245 ),
inference(rat,[],[s296,s887,s875]) ).
cnf(s903,plain,
( spl8_221
| spl8_243
| spl8_257 ),
inference(rat,[],[s293,s885]) ).
cnf(s904,plain,
( spl8_164
| spl8_235
| spl8_256 ),
inference(rat,[],[s292,s880]) ).
cnf(s905,plain,
( spl8_164
| spl8_238
| spl8_254 ),
inference(rat,[],[s291,s881]) ).
cnf(s906,plain,
( spl8_159
| spl8_238
| spl8_240 ),
inference(rat,[],[s284,s879]) ).
cnf(s907,plain,
( spl8_159
| spl8_235
| spl8_237 ),
inference(rat,[],[s283,s878]) ).
cnf(s909,plain,
( spl8_186
| spl8_192 ),
inference(rat,[],[s273,s867,s873]) ).
cnf(s915,plain,
( spl8_176
| spl8_182 ),
inference(rat,[],[s263,s853,s872]) ).
cnf(s918,plain,
( spl8_182
| spl8_201
| spl8_214 ),
inference(rat,[],[s250,s862]) ).
cnf(s919,plain,
( spl8_185
| spl8_203
| spl8_213 ),
inference(rat,[],[s249,s862]) ).
cnf(s921,plain,
( spl8_179
| spl8_199 ),
inference(rat,[],[s247,s863,s861]) ).
cnf(s922,plain,
( spl8_148
| spl8_190
| spl8_206 ),
inference(rat,[],[s243,s857]) ).
cnf(s928,plain,
( spl8_143
| spl8_187
| spl8_189 ),
inference(rat,[],[s235,s853]) ).
cnf(s929,plain,
( spl8_141
| spl8_178
| spl8_179 ),
inference(rat,[],[s232,s867]) ).
cnf(s931,plain,
( spl8_137
| spl8_172
| spl8_173 ),
inference(rat,[],[s230,s873]) ).
cnf(s932,plain,
( spl8_137
| spl8_169
| spl8_171 ),
inference(rat,[],[s229,s872]) ).
cnf(s933,plain,
( spl8_155
| spl8_161 ),
inference(rat,[],[s210,s325,s884]) ).
cnf(s938,plain,
( ~ spl8_154
| spl8_160
| ~ spl8_164 ),
inference(rat,[],[s193,s875]) ).
cnf(s942,plain,
( ~ spl8_154
| spl8_160
| spl8_162 ),
inference(rat,[],[s185,s875]) ).
cnf(s949,plain,
( spl8_153
| spl8_154 ),
inference(rat,[],[s170,s885,s886]) ).
cnf(s950,plain,
( ~ spl8_153
| spl8_154 ),
inference(rat,[],[s169,s885,s886]) ).
cnf(s957,plain,
( spl8_139
| spl8_145 ),
inference(rat,[],[s146,s326,s862]) ).
cnf(s963,plain,
( spl8_141
| spl8_144
| ~ spl8_148 ),
inference(rat,[],[s130,s861]) ).
cnf(s967,plain,
( spl8_137
| spl8_138
| spl8_142 ),
inference(rat,[],[s106,s870]) ).
cnf(s968,plain,
( ~ spl8_137
| spl8_138
| spl8_142 ),
inference(rat,[],[s105,s870]) ).
cnf(s974,plain,
~ spl8_33,
inference(rat,[],[s852,s97]) ).
cnf(s976,plain,
~ spl8_142,
inference(rat,[],[s335,s326,s97,s974]) ).
cnf(s990,plain,
~ spl8_16,
inference(rat,[],[s14,s99]) ).
cnf(s992,plain,
spl8_138,
inference(rat,[],[s968,s967,s976]) ).
cnf(s993,plain,
~ spl8_172,
inference(rat,[],[s725,s992]) ).
cnf(s994,plain,
~ spl8_169,
inference(rat,[],[s639,s992]) ).
cnf(s995,plain,
spl8_12,
inference(rat,[],[s535,s992]) ).
cnf(s996,plain,
~ spl8_145,
inference(rat,[],[s424,s992]) ).
cnf(s997,plain,
spl8_75,
inference(rat,[],[s594,s325,s992,s99,s995]) ).
cnf(s998,plain,
spl8_11,
inference(rat,[],[s9,s995]) ).
cnf(s999,plain,
spl8_139,
inference(rat,[],[s957,s996]) ).
cnf(s1000,plain,
~ spl8_143,
inference(rat,[],[s809,s999]) ).
cnf(s1001,plain,
~ spl8_186,
inference(rat,[],[s801,s999]) ).
cnf(s1002,plain,
~ spl8_181,
inference(rat,[],[s748,s999]) ).
cnf(s1004,plain,
~ spl8_137,
inference(rat,[],[s658,s999]) ).
cnf(s1005,plain,
~ spl8_182,
inference(rat,[],[s626,s999]) ).
cnf(s1006,plain,
~ spl8_141,
inference(rat,[],[s623,s999]) ).
cnf(s1009,plain,
spl8_84,
inference(rat,[],[s583,s992,s999]) ).
cnf(s1010,plain,
spl8_192,
inference(rat,[],[s909,s1001]) ).
cnf(s1011,plain,
spl8_173,
inference(rat,[],[s931,s993,s1004]) ).
cnf(s1012,plain,
spl8_171,
inference(rat,[],[s932,s994,s1004]) ).
cnf(s1013,plain,
spl8_176,
inference(rat,[],[s915,s1005]) ).
cnf(s1014,plain,
~ spl8_190,
inference(rat,[],[s647,s1010]) ).
cnf(s1015,plain,
~ spl8_185,
inference(rat,[],[s404,s1011]) ).
cnf(s1016,plain,
~ spl8_179,
inference(rat,[],[s364,s1011]) ).
cnf(s1019,plain,
~ spl8_189,
inference(rat,[],[s409,s974,s97,s1012]) ).
cnf(s1021,plain,
spl8_199,
inference(rat,[],[s921,s1016]) ).
cnf(s1022,plain,
spl8_178,
inference(rat,[],[s929,s1006,s1016]) ).
cnf(s1023,plain,
spl8_187,
inference(rat,[],[s928,s1000,s1019]) ).
cnf(s1024,plain,
~ spl8_144,
inference(rat,[],[s621,s1021]) ).
cnf(s1026,plain,
~ spl8_203,
inference(rat,[],[s380,s1021]) ).
cnf(s1029,plain,
spl8_82,
inference(rat,[],[s578,s992,s1023]) ).
cnf(s1030,plain,
~ spl8_148,
inference(rat,[],[s963,s1006,s1024]) ).
cnf(s1031,plain,
spl8_213,
inference(rat,[],[s919,s1015,s1026]) ).
cnf(s1032,plain,
spl8_204,
inference(rat,[],[s242,s1002,s996,s1026]) ).
cnf(s1033,plain,
spl8_79,
inference(rat,[],[s598,s882,s1023,s995,s99,s1029]) ).
cnf(s1034,plain,
spl8_206,
inference(rat,[],[s922,s1014,s1030]) ).
cnf(s1036,plain,
~ spl8_214,
inference(rat,[],[s685,s1032]) ).
cnf(s1040,plain,
spl8_201,
inference(rat,[],[s918,s1005,s1036]) ).
cnf(s1041,plain,
spl8_154,
inference(rat,[],[s950,s949]) ).
cnf(s1042,plain,
~ spl8_243,
inference(rat,[],[s556,s1041]) ).
cnf(s1043,plain,
~ spl8_160,
inference(rat,[],[s549,s1041]) ).
cnf(s1044,plain,
~ spl8_161,
inference(rat,[],[s459,s1041]) ).
cnf(s1045,plain,
spl8_70,
inference(rat,[],[s837,s1029,s326,s1009,s1041]) ).
cnf(s1046,plain,
~ spl8_164,
inference(rat,[],[s938,s1041,s1043]) ).
cnf(s1047,plain,
spl8_162,
inference(rat,[],[s942,s1041,s1043]) ).
cnf(s1048,plain,
spl8_155,
inference(rat,[],[s933,s1044]) ).
cnf(s1049,plain,
~ spl8_168,
inference(rat,[],[s576,s1047]) ).
cnf(s1050,plain,
spl8_80,
inference(rat,[],[s599,s1009,s999,s995,s1047]) ).
cnf(s1051,plain,
~ spl8_153,
inference(rat,[],[s575,s1048]) ).
cnf(s1053,plain,
~ spl8_231,
inference(rat,[],[s570,s1048]) ).
cnf(s1054,plain,
~ spl8_157,
inference(rat,[],[s567,s1048]) ).
cnf(s1055,plain,
~ spl8_159,
inference(rat,[],[s548,s1048]) ).
cnf(s1057,plain,
spl8_65,
inference(rat,[],[s585,s1029,s856,s99,s1048]) ).
cnf(s1058,plain,
~ spl8_166,
inference(rat,[],[s216,s1049,s1047,s1055]) ).
cnf(s1059,plain,
spl8_235,
inference(rat,[],[s446,s280,s278,s488,s495,s463,s503,s905,s896,s562,s467,s907,s904,s1054,s1051,s1046,s1058,s1055]) ).
cnf(s1060,plain,
~ spl8_223,
inference(rat,[],[s528,s1059]) ).
cnf(s1062,plain,
~ spl8_217,
inference(rat,[],[s438,s1059]) ).
cnf(s1063,plain,
spl8_66,
inference(rat,[],[s586,s1029,s858,s1009,s995,s1059]) ).
cnf(s1064,plain,
spl8_224,
inference(rat,[],[s485,s277,s899,s514,s530,s279,s901,s1051,s1062,s1054,s1060]) ).
cnf(s1065,plain,
~ spl8_218,
inference(rat,[],[s517,s1064]) ).
cnf(s1066,plain,
~ spl8_230,
inference(rat,[],[s444,s1064]) ).
cnf(s1067,plain,
spl8_67,
inference(rat,[],[s635,s1029,s1032,s1009,s99,s1064]) ).
cnf(s1068,plain,
spl8_219,
inference(rat,[],[s277,s1062,s1051,s1065]) ).
cnf(s1069,plain,
spl8_249,
inference(rat,[],[s899,s1066]) ).
cnf(s1071,plain,
~ spl8_237,
inference(rat,[],[s499,s1068]) ).
cnf(s1072,plain,
spl8_68,
inference(rat,[],[s600,s1029,s1010,s995,s1068]) ).
cnf(s1073,plain,
~ spl8_245,
inference(rat,[],[s530,s1069]) ).
cnf(s1074,plain,
spl8_71,
inference(rat,[],[s681,s1021,s1009,s99,s1069]) ).
cnf(s1075,plain,
spl8_254,
inference(rat,[],[s894,s1049,s1071]) ).
cnf(s1076,plain,
~ spl8_238,
inference(rat,[],[s560,s1075]) ).
cnf(s1077,plain,
~ spl8_250,
inference(rat,[],[s504,s1075]) ).
cnf(s1078,plain,
~ spl8_246,
inference(rat,[],[s458,s1075]) ).
cnf(s1080,plain,
spl8_72,
inference(rat,[],[s682,s1009,s1011,s995,s1075]) ).
cnf(s1081,plain,
spl8_240,
inference(rat,[],[s906,s1055,s1076]) ).
cnf(s1082,plain,
spl8_261,
inference(rat,[],[s306,s1053,s1058,s1077]) ).
cnf(s1083,plain,
spl8_226,
inference(rat,[],[s287,s1073,s1043,s1078]) ).
cnf(s1085,plain,
~ spl8_234,
inference(rat,[],[s496,s1081]) ).
cnf(s1087,plain,
spl8_77,
inference(rat,[],[s683,s1029,s1012,s995,s1081]) ).
cnf(s1088,plain,
~ spl8_257,
inference(rat,[],[s520,s1082]) ).
cnf(s1090,plain,
spl8_76,
inference(rat,[],[s610,s1022,s995,s99,s1082]) ).
cnf(s1093,plain,
spl8_69,
inference(rat,[],[s589,s1029,s1031,s1009,s1083]) ).
cnf(s1094,plain,
spl8_252,
inference(rat,[],[s896,s1058,s1085]) ).
cnf(s1095,plain,
spl8_221,
inference(rat,[],[s903,s1042,s1088]) ).
cnf(s1097,plain,
~ spl8_248,
inference(rat,[],[s454,s1094]) ).
cnf(s1098,plain,
spl8_78,
inference(rat,[],[s740,s1009,s1013,s995,s99,s1094]) ).
cnf(s1100,plain,
spl8_73,
inference(rat,[],[s609,s1029,s1034,s99,s1095]) ).
cnf(s1101,plain,
spl8_247,
inference(rat,[],[s288,s1060,s1043,s1097]) ).
cnf(s1102,plain,
~ spl8_74,
inference(rat,[],[s51,s1009,s1029,s1098,s1033,s1090,s1093,s1080,s997,s1072,s1074,s1045,s1067,s1063,s1057,s1050,s1087,s998,s990,s1100]) ).
cnf(s1104,plain,
$false,
inference(rat,[],[s827,s1040,s1009,s99,s1101,s1102]) ).
fof(f3916,plain,
$false,
inference(avatar_sat_refutation,[],[s1104]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG114+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n007.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 19:28:25 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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.20/0.35 % (2733622)Will run a generic schedule for satisfiability detection.
% 0.20/0.35 % (2733630)dis+10_1_sil=32000:sp=arity:random_seed=3539966105:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.35 % (2733628)% WARNING: option uhcvi not known.
% 0.20/0.35 % (2733627)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=372314979_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.35 % (2733629)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2762257981:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.35 % (2733628)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1461374133:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.35 % (2733631)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2877329941:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.35 % (2733633)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1914551724:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.35 % (2733632)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4285181412:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.35 % (2733630)Instruction limit reached!
% 0.20/0.35 % (2733630)------------------------------
% 0.20/0.35 % (2733630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (2733630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (2733630)CaDiCaL version: 2.1.3
% 0.20/0.35 % (2733630)Termination reason: Instruction limit
% 0.20/0.35 % (2733630)Termination phase: Saturation
% 0.20/0.35 % (2733630)Time elapsed: 0.028 s
% 0.20/0.35 % (2733630)Peak memory usage: 12 MB
% 0.20/0.35 % (2733630)Instructions burned: 104 (million)
% 0.20/0.35 % (2733641)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2109042258:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.20/0.35 % Detected minimum model sizes of [8]
% 0.20/0.35 % Detected maximum model sizes of [max]
% 0.20/0.35 % TRYING [8]
% 0.20/0.35 % Detected minimum model sizes of [8]
% 0.20/0.35 % Detected maximum model sizes of [max]
% 0.20/0.35 % TRYING [8]
% 0.20/0.35 % (2733631)Instruction limit reached!
% 0.20/0.35 % (2733631)------------------------------
% 0.20/0.35 % (2733631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (2733631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (2733631)CaDiCaL version: 2.1.3
% 0.20/0.35 % (2733631)Termination reason: Instruction limit
% 0.20/0.35 % (2733631)Termination phase: Saturation
% 0.20/0.35 % (2733631)Time elapsed: 0.054 s
% 0.20/0.35 % (2733631)Peak memory usage: 13 MB
% 0.20/0.35 % (2733631)Instructions burned: 117 (million)
% 0.20/0.35 % (2733632)Instruction limit reached!
% 0.20/0.35 % (2733632)------------------------------
% 0.20/0.35 % (2733632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (2733632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (2733632)CaDiCaL version: 2.1.3
% 0.20/0.35 % (2733632)Termination reason: Instruction limit
% 0.20/0.35 % (2733632)Termination phase: Saturation
% 0.20/0.35 % (2733632)Time elapsed: 0.063 s
% 0.20/0.35 % (2733632)Peak memory usage: 13 MB
% 0.20/0.35 % (2733632)Instructions burned: 131 (million)
% 0.20/0.35 % (2733643)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1841263313:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.35 % (2733628) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2733622-2733628"...
% 0.20/0.35 % (2733644)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3230670517:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.20/0.35 % (2733633)Instruction limit reached!
% 0.20/0.35 % (2733633)------------------------------
% 0.20/0.35 % (2733633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (2733633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (2733633)CaDiCaL version: 2.1.3
% 0.20/0.35 % (2733633)Termination reason: Instruction limit
% 0.20/0.35 % (2733633)Termination phase: Saturation
% 0.20/0.35 % (2733633)Time elapsed: 0.086 s
% 0.20/0.35 % (2733633)Peak memory usage: 14 MB
% 0.20/0.35 % (2733633)Instructions burned: 161 (million)
% 0.20/0.35 % (2733628)...printing done.
% 0.20/0.35 % (2733628)Refutation found. Thanks to Tanya!
% 0.20/0.35 % SZS status Theorem for theBenchmark
% 0.20/0.35 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/0.36 % (2733628)------------------------------
% 0.20/0.36 % (2733628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (2733628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (2733628)CaDiCaL version: 2.1.3
% 0.20/0.36 % (2733628)Termination reason: Refutation
% 0.20/0.36 % (2733628)Time elapsed: 0.091 s
% 0.20/0.36 % (2733628)Peak memory usage: 14 MB
% 0.20/0.36 % (2733628)Instructions burned: 182 (million)
% 0.20/0.36 % (2733622)Success in time 0.132 s
% 0.20/0.36 % Vampire exiting
%------------------------------------------------------------------------------