%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG124+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 : n009.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:23:12 AM UTC 2026
% Result : Theorem 0.20s 0.35s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 157
% Syntax : Number of formulae : 1168 ( 173 unt; 142 def)
% Number of atoms : 4236 (1907 equ)
% Maximal formula atoms : 132 ( 3 avg)
% Number of connectives : 5090 (2022 ~;2389 |; 537 &)
% ( 142 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 152 ( 150 usr; 151 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e10) = e11
| op1(e10,e10) = e12
| op1(e10,e10) = e13 )
& ( op1(e10,e11) = e10
| op1(e10,e11) = e11
| op1(e10,e11) = e12
| op1(e10,e11) = e13 )
& ( op1(e10,e12) = e10
| op1(e10,e12) = e11
| op1(e10,e12) = e12
| op1(e10,e12) = e13 )
& ( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e12
| op1(e10,e13) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 )
& ( op1(e11,e11) = e10
| op1(e11,e11) = e11
| op1(e11,e11) = e12
| op1(e11,e11) = e13 )
& ( op1(e11,e12) = e10
| op1(e11,e12) = e11
| op1(e11,e12) = e12
| op1(e11,e12) = e13 )
& ( op1(e11,e13) = e10
| op1(e11,e13) = e11
| op1(e11,e13) = e12
| op1(e11,e13) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e10) = e11
| op1(e12,e10) = e12
| op1(e12,e10) = e13 )
& ( op1(e12,e11) = e10
| op1(e12,e11) = e11
| op1(e12,e11) = e12
| op1(e12,e11) = e13 )
& ( op1(e12,e12) = e10
| op1(e12,e12) = e11
| op1(e12,e12) = e12
| op1(e12,e12) = e13 )
& ( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12
| op1(e12,e13) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e10) = e11
| op1(e13,e10) = e12
| op1(e13,e10) = e13 )
& ( op1(e13,e11) = e10
| op1(e13,e11) = e11
| op1(e13,e11) = e12
| op1(e13,e11) = e13 )
& ( op1(e13,e12) = e10
| op1(e13,e12) = e11
| op1(e13,e12) = e12
| op1(e13,e12) = e13 )
& ( op1(e13,e13) = e10
| op1(e13,e13) = e11
| op1(e13,e13) = e12
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e11) = e10
| op1(e10,e12) = e10
| op1(e10,e13) = e10 )
& ( op1(e10,e10) = e10
| op1(e11,e10) = e10
| op1(e12,e10) = e10
| op1(e13,e10) = e10 )
& ( op1(e10,e10) = e11
| op1(e10,e11) = e11
| op1(e10,e12) = e11
| op1(e10,e13) = e11 )
& ( op1(e10,e10) = e11
| op1(e11,e10) = e11
| op1(e12,e10) = e11
| op1(e13,e10) = e11 )
& ( op1(e10,e10) = e12
| op1(e10,e11) = e12
| op1(e10,e12) = e12
| op1(e10,e13) = e12 )
& ( op1(e10,e10) = e12
| op1(e11,e10) = e12
| op1(e12,e10) = e12
| op1(e13,e10) = e12 )
& ( op1(e10,e10) = e13
| op1(e10,e11) = e13
| op1(e10,e12) = e13
| op1(e10,e13) = e13 )
& ( op1(e10,e10) = e13
| op1(e11,e10) = e13
| op1(e12,e10) = e13
| op1(e13,e10) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e11) = e10
| op1(e11,e12) = e10
| op1(e11,e13) = e10 )
& ( op1(e10,e11) = e10
| op1(e11,e11) = e10
| op1(e12,e11) = e10
| op1(e13,e11) = e10 )
& ( op1(e11,e10) = e11
| op1(e11,e11) = e11
| op1(e11,e12) = e11
| op1(e11,e13) = e11 )
& ( op1(e10,e11) = e11
| op1(e11,e11) = e11
| op1(e12,e11) = e11
| op1(e13,e11) = e11 )
& ( op1(e11,e10) = e12
| op1(e11,e11) = e12
| op1(e11,e12) = e12
| op1(e11,e13) = e12 )
& ( op1(e10,e11) = e12
| op1(e11,e11) = e12
| op1(e12,e11) = e12
| op1(e13,e11) = e12 )
& ( op1(e11,e10) = e13
| op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e11,e13) = e13 )
& ( op1(e10,e11) = e13
| op1(e11,e11) = e13
| op1(e12,e11) = e13
| op1(e13,e11) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e11) = e10
| op1(e12,e12) = e10
| op1(e12,e13) = e10 )
& ( op1(e10,e12) = e10
| op1(e11,e12) = e10
| op1(e12,e12) = e10
| op1(e13,e12) = e10 )
& ( op1(e12,e10) = e11
| op1(e12,e11) = e11
| op1(e12,e12) = e11
| op1(e12,e13) = e11 )
& ( op1(e10,e12) = e11
| op1(e11,e12) = e11
| op1(e12,e12) = e11
| op1(e13,e12) = e11 )
& ( op1(e12,e10) = e12
| op1(e12,e11) = e12
| op1(e12,e12) = e12
| op1(e12,e13) = e12 )
& ( op1(e10,e12) = e12
| op1(e11,e12) = e12
| op1(e12,e12) = e12
| op1(e13,e12) = e12 )
& ( op1(e12,e10) = e13
| op1(e12,e11) = e13
| op1(e12,e12) = e13
| op1(e12,e13) = e13 )
& ( op1(e10,e12) = e13
| op1(e11,e12) = e13
| op1(e12,e12) = e13
| op1(e13,e12) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10 )
& ( op1(e10,e13) = e10
| op1(e11,e13) = e10
| op1(e12,e13) = e10
| op1(e13,e13) = e10 )
& ( op1(e13,e10) = e11
| op1(e13,e11) = e11
| op1(e13,e12) = e11
| op1(e13,e13) = e11 )
& ( op1(e10,e13) = e11
| op1(e11,e13) = e11
| op1(e12,e13) = e11
| op1(e13,e13) = e11 )
& ( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12
| op1(e13,e13) = e12 )
& ( op1(e10,e13) = e12
| op1(e11,e13) = e12
| op1(e12,e13) = e12
| op1(e13,e13) = e12 )
& ( op1(e13,e10) = e13
| op1(e13,e11) = e13
| op1(e13,e12) = e13
| op1(e13,e13) = e13 )
& ( op1(e10,e13) = e13
| op1(e11,e13) = e13
| op1(e12,e13) = e13
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e20) = e21
| op2(e20,e20) = e22
| op2(e20,e20) = e23 )
& ( op2(e20,e21) = e20
| op2(e20,e21) = e21
| op2(e20,e21) = e22
| op2(e20,e21) = e23 )
& ( op2(e20,e22) = e20
| op2(e20,e22) = e21
| op2(e20,e22) = e22
| op2(e20,e22) = e23 )
& ( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22
| op2(e20,e23) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e20) = e21
| op2(e21,e20) = e22
| op2(e21,e20) = e23 )
& ( op2(e21,e21) = e20
| op2(e21,e21) = e21
| op2(e21,e21) = e22
| op2(e21,e21) = e23 )
& ( op2(e21,e22) = e20
| op2(e21,e22) = e21
| op2(e21,e22) = e22
| op2(e21,e22) = e23 )
& ( op2(e21,e23) = e20
| op2(e21,e23) = e21
| op2(e21,e23) = e22
| op2(e21,e23) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e20) = e21
| op2(e22,e20) = e22
| op2(e22,e20) = e23 )
& ( op2(e22,e21) = e20
| op2(e22,e21) = e21
| op2(e22,e21) = e22
| op2(e22,e21) = e23 )
& ( op2(e22,e22) = e20
| op2(e22,e22) = e21
| op2(e22,e22) = e22
| op2(e22,e22) = e23 )
& ( op2(e22,e23) = e20
| op2(e22,e23) = e21
| op2(e22,e23) = e22
| op2(e22,e23) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e20) = e21
| op2(e23,e20) = e22
| op2(e23,e20) = e23 )
& ( op2(e23,e21) = e20
| op2(e23,e21) = e21
| op2(e23,e21) = e22
| op2(e23,e21) = e23 )
& ( op2(e23,e22) = e20
| op2(e23,e22) = e21
| op2(e23,e22) = e22
| op2(e23,e22) = e23 )
& ( op2(e23,e23) = e20
| op2(e23,e23) = e21
| op2(e23,e23) = e22
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e22) = e20
| op2(e20,e23) = e20 )
& ( op2(e20,e20) = e20
| op2(e21,e20) = e20
| op2(e22,e20) = e20
| op2(e23,e20) = e20 )
& ( op2(e20,e20) = e21
| op2(e20,e21) = e21
| op2(e20,e22) = e21
| op2(e20,e23) = e21 )
& ( op2(e20,e20) = e21
| op2(e21,e20) = e21
| op2(e22,e20) = e21
| op2(e23,e20) = e21 )
& ( op2(e20,e20) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 )
& ( op2(e20,e20) = e22
| op2(e21,e20) = e22
| op2(e22,e20) = e22
| op2(e23,e20) = e22 )
& ( op2(e20,e20) = e23
| op2(e20,e21) = e23
| op2(e20,e22) = e23
| op2(e20,e23) = e23 )
& ( op2(e20,e20) = e23
| op2(e21,e20) = e23
| op2(e22,e20) = e23
| op2(e23,e20) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e21) = e20
| op2(e21,e22) = e20
| op2(e21,e23) = e20 )
& ( op2(e20,e21) = e20
| op2(e21,e21) = e20
| op2(e22,e21) = e20
| op2(e23,e21) = e20 )
& ( op2(e21,e20) = e21
| op2(e21,e21) = e21
| op2(e21,e22) = e21
| op2(e21,e23) = e21 )
& ( op2(e20,e21) = e21
| op2(e21,e21) = e21
| op2(e22,e21) = e21
| op2(e23,e21) = e21 )
& ( op2(e21,e20) = e22
| op2(e21,e21) = e22
| op2(e21,e22) = e22
| op2(e21,e23) = e22 )
& ( op2(e20,e21) = e22
| op2(e21,e21) = e22
| op2(e22,e21) = e22
| op2(e23,e21) = e22 )
& ( op2(e21,e20) = e23
| op2(e21,e21) = e23
| op2(e21,e22) = e23
| op2(e21,e23) = e23 )
& ( op2(e20,e21) = e23
| op2(e21,e21) = e23
| op2(e22,e21) = e23
| op2(e23,e21) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e21) = e20
| op2(e22,e22) = e20
| op2(e22,e23) = e20 )
& ( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e22,e22) = e20
| op2(e23,e22) = e20 )
& ( op2(e22,e20) = e21
| op2(e22,e21) = e21
| op2(e22,e22) = e21
| op2(e22,e23) = e21 )
& ( op2(e20,e22) = e21
| op2(e21,e22) = e21
| op2(e22,e22) = e21
| op2(e23,e22) = e21 )
& ( op2(e22,e20) = e22
| op2(e22,e21) = e22
| op2(e22,e22) = e22
| op2(e22,e23) = e22 )
& ( op2(e20,e22) = e22
| op2(e21,e22) = e22
| op2(e22,e22) = e22
| op2(e23,e22) = e22 )
& ( op2(e22,e20) = e23
| op2(e22,e21) = e23
| op2(e22,e22) = e23
| op2(e22,e23) = e23 )
& ( op2(e20,e22) = e23
| op2(e21,e22) = e23
| op2(e22,e22) = e23
| op2(e23,e22) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e23) = e20 )
& ( op2(e20,e23) = e20
| op2(e21,e23) = e20
| op2(e22,e23) = e20
| op2(e23,e23) = e20 )
& ( op2(e23,e20) = e21
| op2(e23,e21) = e21
| op2(e23,e22) = e21
| op2(e23,e23) = e21 )
& ( op2(e20,e23) = e21
| op2(e21,e23) = e21
| op2(e22,e23) = e21
| op2(e23,e23) = e21 )
& ( op2(e23,e20) = e22
| op2(e23,e21) = e22
| op2(e23,e22) = e22
| op2(e23,e23) = e22 )
& ( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22
| op2(e23,e23) = e22 )
& ( op2(e23,e20) = e23
| op2(e23,e21) = e23
| op2(e23,e22) = e23
| op2(e23,e23) = e23 )
& ( op2(e20,e23) = e23
| op2(e21,e23) = e23
| op2(e22,e23) = e23
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op1(e10,e10) != op1(e11,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e12,e10) != op1(e13,e10)
& op1(e10,e11) != op1(e11,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e12,e11) != op1(e13,e11)
& op1(e10,e12) != op1(e11,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e12,e12) != op1(e13,e12)
& op1(e10,e13) != op1(e11,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e12,e13) != op1(e13,e13)
& op1(e10,e10) != op1(e10,e11)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e12) != op1(e10,e13)
& op1(e11,e10) != op1(e11,e11)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e12) != op1(e11,e13)
& op1(e12,e10) != op1(e12,e11)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e12) != op1(e12,e13)
& op1(e13,e10) != op1(e13,e11)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e12) != op1(e13,e13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( op2(e20,e20) != op2(e21,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e22,e20) != op2(e23,e20)
& op2(e20,e21) != op2(e21,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e22,e21) != op2(e23,e21)
& op2(e20,e22) != op2(e21,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e22,e22) != op2(e23,e22)
& op2(e20,e23) != op2(e21,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e22,e23) != op2(e23,e23)
& op2(e20,e20) != op2(e20,e21)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e22) != op2(e20,e23)
& op2(e21,e20) != op2(e21,e21)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e22) != op2(e21,e23)
& op2(e22,e20) != op2(e22,e21)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e22) != op2(e22,e23)
& op2(e23,e20) != op2(e23,e21)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e22) != op2(e23,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f10,axiom,
( op1(e10,e10) != e10
& op1(e11,e11) != e11
& op1(e12,e12) != e12
& op1(e13,e13) != e13
& ( ( ( op1(e10,e10) != e10
| op1(e10,e10) = e10 )
& ( op1(e10,e11) != e10
| op1(e10,e10) = e11 )
& ( op1(e10,e12) != e10
| op1(e10,e10) = e12 )
& ( op1(e10,e13) != e10
| op1(e10,e10) = e13 )
& ( op1(e11,e10) != e10
| op1(e11,e10) = e10 )
& ( op1(e11,e11) != e10
| op1(e11,e10) = e11 )
& ( op1(e11,e12) != e10
| op1(e11,e10) = e12 )
& ( op1(e11,e13) != e10
| op1(e11,e10) = e13 )
& ( op1(e12,e10) != e10
| op1(e12,e10) = e10 )
& ( op1(e12,e11) != e10
| op1(e12,e10) = e11 )
& ( op1(e12,e12) != e10
| op1(e12,e10) = e12 )
& ( op1(e12,e13) != e10
| op1(e12,e10) = e13 )
& ( op1(e13,e10) != e10
| op1(e13,e10) = e10 )
& ( op1(e13,e11) != e10
| op1(e13,e10) = e11 )
& ( op1(e13,e12) != e10
| op1(e13,e10) = e12 )
& ( op1(e13,e13) != e10
| op1(e13,e10) = e13 ) )
| ( ( op1(e10,e10) != e11
| op1(e10,e11) = e10 )
& ( op1(e10,e11) != e11
| op1(e10,e11) = e11 )
& ( op1(e10,e12) != e11
| op1(e10,e11) = e12 )
& ( op1(e10,e13) != e11
| op1(e10,e11) = e13 )
& ( op1(e11,e10) != e11
| op1(e11,e11) = e10 )
& ( op1(e11,e11) != e11
| op1(e11,e11) = e11 )
& ( op1(e11,e12) != e11
| op1(e11,e11) = e12 )
& ( op1(e11,e13) != e11
| op1(e11,e11) = e13 )
& ( op1(e12,e10) != e11
| op1(e12,e11) = e10 )
& ( op1(e12,e11) != e11
| op1(e12,e11) = e11 )
& ( op1(e12,e12) != e11
| op1(e12,e11) = e12 )
& ( op1(e12,e13) != e11
| op1(e12,e11) = e13 )
& ( op1(e13,e10) != e11
| op1(e13,e11) = e10 )
& ( op1(e13,e11) != e11
| op1(e13,e11) = e11 )
& ( op1(e13,e12) != e11
| op1(e13,e11) = e12 )
& ( op1(e13,e13) != e11
| op1(e13,e11) = e13 ) )
| ( ( op1(e10,e10) != e12
| op1(e10,e12) = e10 )
& ( op1(e10,e11) != e12
| op1(e10,e12) = e11 )
& ( op1(e10,e12) != e12
| op1(e10,e12) = e12 )
& ( op1(e10,e13) != e12
| op1(e10,e12) = e13 )
& ( op1(e11,e10) != e12
| op1(e11,e12) = e10 )
& ( op1(e11,e11) != e12
| op1(e11,e12) = e11 )
& ( op1(e11,e12) != e12
| op1(e11,e12) = e12 )
& ( op1(e11,e13) != e12
| op1(e11,e12) = e13 )
& ( op1(e12,e10) != e12
| op1(e12,e12) = e10 )
& ( op1(e12,e11) != e12
| op1(e12,e12) = e11 )
& ( op1(e12,e12) != e12
| op1(e12,e12) = e12 )
& ( op1(e12,e13) != e12
| op1(e12,e12) = e13 )
& ( op1(e13,e10) != e12
| op1(e13,e12) = e10 )
& ( op1(e13,e11) != e12
| op1(e13,e12) = e11 )
& ( op1(e13,e12) != e12
| op1(e13,e12) = e12 )
& ( op1(e13,e13) != e12
| op1(e13,e12) = e13 ) )
| ( ( op1(e10,e10) != e13
| op1(e10,e13) = e10 )
& ( op1(e10,e11) != e13
| op1(e10,e13) = e11 )
& ( op1(e10,e12) != e13
| op1(e10,e13) = e12 )
& ( op1(e10,e13) != e13
| op1(e10,e13) = e13 )
& ( op1(e11,e10) != e13
| op1(e11,e13) = e10 )
& ( op1(e11,e11) != e13
| op1(e11,e13) = e11 )
& ( op1(e11,e12) != e13
| op1(e11,e13) = e12 )
& ( op1(e11,e13) != e13
| op1(e11,e13) = e13 )
& ( op1(e12,e10) != e13
| op1(e12,e13) = e10 )
& ( op1(e12,e11) != e13
| op1(e12,e13) = e11 )
& ( op1(e12,e12) != e13
| op1(e12,e13) = e12 )
& ( op1(e12,e13) != e13
| op1(e12,e13) = e13 )
& ( op1(e13,e10) != e13
| op1(e13,e13) = e10 )
& ( op1(e13,e11) != e13
| op1(e13,e13) = e11 )
& ( op1(e13,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(e21,e21) != e21
& op2(e22,e22) != e22
& op2(e23,e23) != e23
& ( ( ( op2(e20,e20) != e20
| op2(e20,e20) = e20 )
& ( op2(e20,e21) != e20
| op2(e20,e20) = e21 )
& ( op2(e20,e22) != e20
| op2(e20,e20) = e22 )
& ( op2(e20,e23) != e20
| op2(e20,e20) = e23 )
& ( op2(e21,e20) != e20
| op2(e21,e20) = e20 )
& ( op2(e21,e21) != e20
| op2(e21,e20) = e21 )
& ( op2(e21,e22) != e20
| op2(e21,e20) = e22 )
& ( op2(e21,e23) != e20
| op2(e21,e20) = e23 )
& ( op2(e22,e20) != e20
| op2(e22,e20) = e20 )
& ( op2(e22,e21) != e20
| op2(e22,e20) = e21 )
& ( op2(e22,e22) != e20
| op2(e22,e20) = e22 )
& ( op2(e22,e23) != e20
| op2(e22,e20) = e23 )
& ( op2(e23,e20) != e20
| op2(e23,e20) = e20 )
& ( op2(e23,e21) != e20
| op2(e23,e20) = e21 )
& ( op2(e23,e22) != e20
| op2(e23,e20) = e22 )
& ( op2(e23,e23) != e20
| op2(e23,e20) = e23 ) )
| ( ( op2(e20,e20) != e21
| op2(e20,e21) = e20 )
& ( op2(e20,e21) != e21
| op2(e20,e21) = e21 )
& ( op2(e20,e22) != e21
| op2(e20,e21) = e22 )
& ( op2(e20,e23) != e21
| op2(e20,e21) = e23 )
& ( op2(e21,e20) != e21
| op2(e21,e21) = e20 )
& ( op2(e21,e21) != e21
| op2(e21,e21) = e21 )
& ( op2(e21,e22) != e21
| op2(e21,e21) = e22 )
& ( op2(e21,e23) != e21
| op2(e21,e21) = e23 )
& ( op2(e22,e20) != e21
| op2(e22,e21) = e20 )
& ( op2(e22,e21) != e21
| op2(e22,e21) = e21 )
& ( op2(e22,e22) != e21
| op2(e22,e21) = e22 )
& ( op2(e22,e23) != e21
| op2(e22,e21) = e23 )
& ( op2(e23,e20) != e21
| op2(e23,e21) = e20 )
& ( op2(e23,e21) != e21
| op2(e23,e21) = e21 )
& ( op2(e23,e22) != e21
| op2(e23,e21) = e22 )
& ( op2(e23,e23) != e21
| op2(e23,e21) = e23 ) )
| ( ( op2(e20,e20) != e22
| op2(e20,e22) = e20 )
& ( op2(e20,e21) != e22
| op2(e20,e22) = e21 )
& ( op2(e20,e22) != e22
| op2(e20,e22) = e22 )
& ( op2(e20,e23) != e22
| op2(e20,e22) = e23 )
& ( op2(e21,e20) != e22
| op2(e21,e22) = e20 )
& ( op2(e21,e21) != e22
| op2(e21,e22) = e21 )
& ( op2(e21,e22) != e22
| op2(e21,e22) = e22 )
& ( op2(e21,e23) != e22
| op2(e21,e22) = e23 )
& ( op2(e22,e20) != e22
| op2(e22,e22) = e20 )
& ( op2(e22,e21) != e22
| op2(e22,e22) = e21 )
& ( op2(e22,e22) != e22
| op2(e22,e22) = e22 )
& ( op2(e22,e23) != e22
| op2(e22,e22) = e23 )
& ( op2(e23,e20) != e22
| op2(e23,e22) = e20 )
& ( op2(e23,e21) != e22
| op2(e23,e22) = e21 )
& ( op2(e23,e22) != e22
| op2(e23,e22) = e22 )
& ( op2(e23,e23) != e22
| op2(e23,e22) = e23 ) )
| ( ( op2(e20,e20) != e23
| op2(e20,e23) = e20 )
& ( op2(e20,e21) != e23
| op2(e20,e23) = e21 )
& ( op2(e20,e22) != e23
| op2(e20,e23) = e22 )
& ( op2(e20,e23) != e23
| op2(e20,e23) = e23 )
& ( op2(e21,e20) != e23
| op2(e21,e23) = e20 )
& ( op2(e21,e21) != e23
| op2(e21,e23) = e21 )
& ( op2(e21,e22) != e23
| op2(e21,e23) = e22 )
& ( op2(e21,e23) != e23
| op2(e21,e23) = e23 )
& ( op2(e22,e20) != e23
| op2(e22,e23) = e20 )
& ( op2(e22,e21) != e23
| op2(e22,e23) = e21 )
& ( op2(e22,e22) != e23
| op2(e22,e23) = e22 )
& ( op2(e22,e23) != e23
| op2(e22,e23) = e23 )
& ( op2(e23,e20) != e23
| op2(e23,e23) = e20 )
& ( op2(e23,e21) != e23
| op2(e23,e23) = e21 )
& ( op2(e23,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,
( e11 = op1(op1(op1(e10,e10),e10),e10)
& e12 = op1(op1(e10,e10),e10)
& e13 = op1(e10,e10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e21 = op2(op2(op2(e20,e20),e20),e20)
& e22 = op2(op2(e20,e20),e20)
& e23 = op2(e20,e20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( h1(e10) = e20
& h1(e11) = op2(op2(op2(e20,e20),e20),e20)
& h1(e12) = op2(op2(e20,e20),e20)
& h1(e13) = op2(e20,e20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f16,axiom,
( h3(e10) = e22
& h3(e11) = op2(op2(op2(e22,e22),e22),e22)
& h3(e12) = op2(op2(e22,e22),e22)
& h3(e13) = op2(e22,e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f18,conjecture,
( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f19,negated_conjecture,
~ ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f20,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) ) )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) ) )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) ) )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) ) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f24,plain,
( e13 = op1(e10,e13)
| e12 = op1(e10,e13)
| e11 = op1(e10,e13)
| e10 = op1(e10,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f26,plain,
( e13 = op1(e11,e11)
| e12 = op1(e11,e11)
| e11 = op1(e11,e11)
| e10 = op1(e11,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f30,plain,
( e13 = op1(e12,e11)
| e12 = op1(e12,e11)
| e11 = op1(e12,e11)
| e10 = op1(e12,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f31,plain,
( e13 = op1(e12,e12)
| e12 = op1(e12,e12)
| e11 = op1(e12,e12)
| e10 = op1(e12,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f35,plain,
( e13 = op1(e13,e12)
| e12 = op1(e13,e12)
| e11 = op1(e13,e12)
| e10 = op1(e13,e12) ),
inference(cnf_transformation,[],[f1]) ).
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(f41,plain,
( e12 = op1(e10,e13)
| e12 = op1(e10,e12)
| e12 = op1(e10,e11)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f2]) ).
fof(f46,plain,
( e10 = op1(e13,e11)
| e10 = op1(e12,e11)
| e10 = op1(e11,e11)
| e10 = op1(e10,e11) ),
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(f49,plain,
( e12 = op1(e11,e13)
| e12 = op1(e11,e12)
| e12 = op1(e11,e11)
| e12 = 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(f57,plain,
( e12 = op1(e12,e13)
| e12 = op1(e12,e12)
| e12 = op1(e12,e11)
| e12 = op1(e12,e10) ),
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(f61,plain,
( e10 = op1(e13,e13)
| e10 = op1(e13,e12)
| e10 = op1(e13,e11)
| e10 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f62,plain,
( e10 = op1(e13,e13)
| e10 = op1(e12,e13)
| e10 = op1(e11,e13)
| e10 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f63,plain,
( e11 = op1(e13,e13)
| e11 = op1(e13,e12)
| e11 = op1(e13,e11)
| e11 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f64,plain,
( e11 = op1(e13,e13)
| e11 = op1(e12,e13)
| e11 = op1(e11,e13)
| e11 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f67,plain,
( e13 = op1(e13,e13)
| e13 = op1(e13,e12)
| e13 = op1(e13,e11)
| e13 = op1(e13,e10) ),
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(f74,plain,
( e23 = op2(e21,e21)
| e22 = op2(e21,e21)
| e21 = op2(e21,e21)
| e20 = op2(e21,e21) ),
inference(cnf_transformation,[],[f3]) ).
fof(f79,plain,
( e23 = op2(e22,e22)
| e22 = op2(e22,e22)
| e21 = op2(e22,e22)
| e20 = op2(e22,e22) ),
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(f87,plain,
( e21 = op2(e20,e23)
| e21 = op2(e20,e22)
| e21 = op2(e20,e21)
| op2(e20,e20) = e21 ),
inference(cnf_transformation,[],[f4]) ).
fof(f89,plain,
( e22 = op2(e20,e23)
| e22 = op2(e20,e22)
| e22 = op2(e20,e21)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f4]) ).
fof(f95,plain,
( e21 = op2(e21,e23)
| e21 = op2(e21,e22)
| e21 = op2(e21,e21)
| e21 = op2(e21,e20) ),
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(f101,plain,
( e20 = op2(e22,e23)
| e20 = op2(e22,e22)
| e20 = op2(e22,e21)
| e20 = op2(e22,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f104,plain,
( e21 = op2(e23,e22)
| e21 = op2(e22,e22)
| e21 = op2(e21,e22)
| e21 = op2(e20,e22) ),
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(f109,plain,
( e20 = op2(e23,e23)
| e20 = op2(e23,e22)
| e20 = op2(e23,e21)
| e20 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f110,plain,
( e20 = op2(e23,e23)
| e20 = op2(e22,e23)
| e20 = op2(e21,e23)
| e20 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f111,plain,
( e21 = op2(e23,e23)
| e21 = op2(e23,e22)
| e21 = op2(e23,e21)
| e21 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f114,plain,
( e22 = op2(e23,e23)
| e22 = op2(e22,e23)
| e22 = op2(e21,e23)
| e22 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f115,plain,
( e23 = op2(e23,e23)
| e23 = op2(e23,e22)
| e23 = op2(e23,e21)
| e23 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f119,plain,
op1(e13,e11) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f121,plain,
op1(e13,e10) != op1(e13,e12),
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(f128,plain,
op1(e12,e10) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f131,plain,
op1(e11,e11) != op1(e11,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f132,plain,
op1(e11,e10) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f134,plain,
op1(e11,e10) != op1(e11,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f136,plain,
op1(e10,e11) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f138,plain,
op1(e10,e10) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f139,plain,
op1(e10,e10) != op1(e10,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f140,plain,
op1(e10,e10) != op1(e10,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f144,plain,
op1(e10,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f147,plain,
op1(e12,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f148,plain,
op1(e11,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f150,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f152,plain,
op1(e10,e12) != op1(e11,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f154,plain,
op1(e11,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f155,plain,
op1(e11,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f157,plain,
op1(e10,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f159,plain,
op1(e12,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
op1(e10,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f173,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f175,plain,
op2(e22,e20) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f178,plain,
op2(e21,e21) != op2(e21,e23),
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(f190,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f192,plain,
op2(e20,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f193,plain,
op2(e20,e23) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f195,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f196,plain,
op2(e21,e22) != op2(e23,e22),
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(f200,plain,
op2(e20,e22) != op2(e21,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f202,plain,
op2(e21,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f206,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f207,plain,
op2(e22,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f209,plain,
op2(e21,e20) != op2(e22,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(f224,plain,
e20 != e21,
inference(cnf_transformation,[],[f8]) ).
fof(f248,plain,
( e12 = op1(e12,e10)
| e10 != op1(e12,e12)
| ~ sP2 ),
inference(cnf_transformation,[],[f10]) ).
fof(f250,plain,
( e11 = op1(e13,e10)
| e10 != op1(e13,e11)
| ~ sP2 ),
inference(cnf_transformation,[],[f10]) ).
fof(f252,plain,
( e13 = op1(e13,e10)
| e10 != op1(e13,e13)
| ~ sP2 ),
inference(cnf_transformation,[],[f10]) ).
fof(f257,plain,
( e12 = op1(e11,e11)
| e11 != op1(e11,e12)
| ~ sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f259,plain,
( e10 = op1(e12,e11)
| e11 != op1(e12,e10)
| ~ sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f264,plain,
( e13 = op1(e13,e11)
| e11 != op1(e13,e13)
| ~ sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f267,plain,
( e13 = op1(e10,e12)
| e12 != op1(e10,e13)
| ~ sP0 ),
inference(cnf_transformation,[],[f10]) ).
fof(f270,plain,
( e13 = op1(e11,e12)
| e12 != op1(e11,e13)
| ~ sP0 ),
inference(cnf_transformation,[],[f10]) ).
fof(f274,plain,
( e10 = op1(e13,e12)
| e12 != op1(e13,e10)
| ~ sP0 ),
inference(cnf_transformation,[],[f10]) ).
fof(f277,plain,
( e10 = op1(e10,e13)
| op1(e10,e10) != e13
| sP0
| sP1
| sP2 ),
inference(cnf_transformation,[],[f10]) ).
fof(f281,plain,
( e11 = op1(e11,e13)
| e13 != op1(e11,e11)
| sP0
| sP1
| sP2 ),
inference(cnf_transformation,[],[f10]) ).
fof(f284,plain,
( e11 = op1(e12,e13)
| e13 != op1(e12,e11)
| sP0
| sP1
| sP2 ),
inference(cnf_transformation,[],[f10]) ).
fof(f288,plain,
( e12 = op1(e13,e13)
| e13 != op1(e13,e12)
| sP0
| sP1
| sP2 ),
inference(cnf_transformation,[],[f10]) ).
fof(f289,plain,
e13 != op1(e13,e13),
inference(cnf_transformation,[],[f10]) ).
fof(f290,plain,
e12 != op1(e12,e12),
inference(cnf_transformation,[],[f10]) ).
fof(f291,plain,
e11 != op1(e11,e11),
inference(cnf_transformation,[],[f10]) ).
fof(f292,plain,
e10 != op1(e10,e10),
inference(cnf_transformation,[],[f10]) ).
fof(f293,plain,
( op2(e20,e20) = e21
| e20 != op2(e20,e21)
| ~ sP5 ),
inference(cnf_transformation,[],[f11]) ).
fof(f294,plain,
( op2(e20,e20) = e22
| e20 != op2(e20,e22)
| ~ sP5 ),
inference(cnf_transformation,[],[f11]) ).
fof(f300,plain,
( e22 = op2(e22,e20)
| e20 != op2(e22,e22)
| ~ sP5 ),
inference(cnf_transformation,[],[f11]) ).
fof(f310,plain,
( e23 = op2(e21,e21)
| e21 != op2(e21,e23)
| ~ sP4 ),
inference(cnf_transformation,[],[f11]) ).
fof(f311,plain,
( e20 = op2(e22,e21)
| e21 != op2(e22,e20)
| ~ sP4 ),
inference(cnf_transformation,[],[f11]) ).
fof(f321,plain,
( e21 = op2(e21,e22)
| e22 != op2(e21,e21)
| ~ sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f326,plain,
( e20 = op2(e23,e22)
| e22 != op2(e23,e20)
| ~ sP3 ),
inference(cnf_transformation,[],[f11]) ).
fof(f329,plain,
( e20 = op2(e20,e23)
| op2(e20,e20) != e23
| sP3
| sP4
| sP5 ),
inference(cnf_transformation,[],[f11]) ).
fof(f340,plain,
( e22 = op2(e23,e23)
| e23 != op2(e23,e22)
| sP3
| sP4
| sP5 ),
inference(cnf_transformation,[],[f11]) ).
fof(f341,plain,
e23 != op2(e23,e23),
inference(cnf_transformation,[],[f11]) ).
fof(f342,plain,
e22 != op2(e22,e22),
inference(cnf_transformation,[],[f11]) ).
fof(f343,plain,
e21 != op2(e21,e21),
inference(cnf_transformation,[],[f11]) ).
fof(f344,plain,
e20 != op2(e20,e20),
inference(cnf_transformation,[],[f11]) ).
fof(f345,plain,
op1(e10,e10) = e13,
inference(cnf_transformation,[],[f12]) ).
fof(f346,plain,
e12 = op1(op1(e10,e10),e10),
inference(cnf_transformation,[],[f12]) ).
fof(f347,plain,
e11 = op1(op1(op1(e10,e10),e10),e10),
inference(cnf_transformation,[],[f12]) ).
fof(f348,plain,
op2(e20,e20) = e23,
inference(cnf_transformation,[],[f13]) ).
fof(f349,plain,
e22 = op2(op2(e20,e20),e20),
inference(cnf_transformation,[],[f13]) ).
fof(f350,plain,
e21 = op2(op2(op2(e20,e20),e20),e20),
inference(cnf_transformation,[],[f13]) ).
fof(f351,plain,
op2(e20,e20) = h1(e13),
inference(cnf_transformation,[],[f14]) ).
fof(f352,plain,
op2(op2(e20,e20),e20) = h1(e12),
inference(cnf_transformation,[],[f14]) ).
fof(f353,plain,
op2(op2(op2(e20,e20),e20),e20) = h1(e11),
inference(cnf_transformation,[],[f14]) ).
fof(f354,plain,
e20 = h1(e10),
inference(cnf_transformation,[],[f14]) ).
fof(f359,plain,
op2(e22,e22) = h3(e13),
inference(cnf_transformation,[],[f16]) ).
fof(f362,plain,
e22 = h3(e10),
inference(cnf_transformation,[],[f16]) ).
fof(f370,plain,
( e20 != h1(e10)
| ~ sP13 ),
inference(cnf_transformation,[],[f20]) ).
fof(f373,plain,
( e21 != h1(e11)
| ~ sP12 ),
inference(cnf_transformation,[],[f20]) ).
fof(f412,plain,
( e23 != h1(e13)
| e22 != h1(e12)
| sP12
| sP13
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e10)) != op2(h1(e10),h1(e10)) ),
inference(cnf_transformation,[],[f20]) ).
fof(f463,plain,
( e12 = op1(e13,e13)
| e13 != op1(e13,e12)
| sP0
| ~ sP1
| ~ sP2 ),
inference(consistent_polarity_flipping,[],[f288]) ).
fof(f467,plain,
( e11 = op1(e12,e13)
| e13 != op1(e12,e11)
| sP0
| ~ sP1
| ~ sP2 ),
inference(consistent_polarity_flipping,[],[f284]) ).
fof(f470,plain,
( e11 = op1(e11,e13)
| e13 != op1(e11,e11)
| sP0
| ~ sP1
| ~ sP2 ),
inference(consistent_polarity_flipping,[],[f281]) ).
fof(f474,plain,
( e10 = op1(e10,e13)
| op1(e10,e10) != e13
| sP0
| ~ sP1
| ~ sP2 ),
inference(consistent_polarity_flipping,[],[f277]) ).
fof(f475,plain,
( e13 = op1(e13,e11)
| e11 != op1(e13,e13)
| sP1 ),
inference(consistent_polarity_flipping,[],[f264]) ).
fof(f480,plain,
( e10 = op1(e12,e11)
| e11 != op1(e12,e10)
| sP1 ),
inference(consistent_polarity_flipping,[],[f259]) ).
fof(f482,plain,
( e12 = op1(e11,e11)
| e11 != op1(e11,e12)
| sP1 ),
inference(consistent_polarity_flipping,[],[f257]) ).
fof(f487,plain,
( e13 = op1(e13,e10)
| e10 != op1(e13,e13)
| sP2 ),
inference(consistent_polarity_flipping,[],[f252]) ).
fof(f489,plain,
( e11 = op1(e13,e10)
| e10 != op1(e13,e11)
| sP2 ),
inference(consistent_polarity_flipping,[],[f250]) ).
fof(f491,plain,
( e12 = op1(e12,e10)
| e10 != op1(e12,e12)
| sP2 ),
inference(consistent_polarity_flipping,[],[f248]) ).
fof(f499,plain,
( e22 = op2(e23,e23)
| e23 != op2(e23,e22)
| ~ sP3
| ~ sP4
| sP5 ),
inference(consistent_polarity_flipping,[],[f340]) ).
fof(f510,plain,
( e20 = op2(e20,e23)
| op2(e20,e20) != e23
| ~ sP3
| ~ sP4
| sP5 ),
inference(consistent_polarity_flipping,[],[f329]) ).
fof(f513,plain,
( e20 = op2(e23,e22)
| e22 != op2(e23,e20)
| sP3 ),
inference(consistent_polarity_flipping,[],[f326]) ).
fof(f518,plain,
( e21 = op2(e21,e22)
| e22 != op2(e21,e21)
| sP3 ),
inference(consistent_polarity_flipping,[],[f321]) ).
fof(f528,plain,
( e20 = op2(e22,e21)
| e21 != op2(e22,e20)
| sP4 ),
inference(consistent_polarity_flipping,[],[f311]) ).
fof(f529,plain,
( e23 = op2(e21,e21)
| e21 != op2(e21,e23)
| sP4 ),
inference(consistent_polarity_flipping,[],[f310]) ).
fof(f569,plain,
( e23 != h1(e13)
| e22 != h1(e12)
| sP12
| ~ sP13
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e10)) != op2(h1(e10),h1(e10)) ),
inference(consistent_polarity_flipping,[],[f412]) ).
fof(f591,plain,
( e20 != h1(e10)
| sP13 ),
inference(consistent_polarity_flipping,[],[f370]) ).
fof(f596,definition,
( spl14_1
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl14_1])],[avatar_definition]) ).
fof(f615,definition,
( spl14_5
<=> e20 = h1(e10) ),
introduced(definition,[new_symbols(definition,[spl14_5])],[avatar_definition]) ).
fof(f616,plain,
( e20 = h1(e10)
| ~ spl14_5 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f618,plain,
( spl14_1
| ~ spl14_5 ),
inference(avatar_split_clause,[],[f591,f615,f596]) ).
fof(f620,definition,
( spl14_6
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl14_6])],[avatar_definition]) ).
fof(f634,definition,
( spl14_9
<=> e21 = h1(e11) ),
introduced(definition,[new_symbols(definition,[spl14_9])],[avatar_definition]) ).
fof(f635,plain,
( e21 = h1(e11)
| ~ spl14_9 ),
inference(avatar_component_clause,[],[f634]) ).
fof(f637,plain,
( ~ spl14_6
| ~ spl14_9 ),
inference(avatar_split_clause,[],[f373,f634,f620]) ).
fof(f711,definition,
( spl14_25
<=> e20 = h3(e10) ),
introduced(definition,[new_symbols(definition,[spl14_25])],[avatar_definition]) ).
fof(f712,plain,
( e20 = h3(e10)
| ~ spl14_25 ),
inference(avatar_component_clause,[],[f711]) ).
fof(f713,plain,
( e20 != h3(e10)
| spl14_25 ),
inference(avatar_component_clause,[],[f711]) ).
fof(f788,definition,
( spl14_41
<=> h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl14_41])],[avatar_definition]) ).
fof(f790,plain,
( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| spl14_41 ),
inference(avatar_component_clause,[],[f788]) ).
fof(f792,definition,
( spl14_42
<=> h1(op1(e10,e11)) = op2(h1(e10),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl14_42])],[avatar_definition]) ).
fof(f794,plain,
( h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| spl14_42 ),
inference(avatar_component_clause,[],[f792]) ).
fof(f796,definition,
( spl14_43
<=> h1(op1(e10,e12)) = op2(h1(e10),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl14_43])],[avatar_definition]) ).
fof(f798,plain,
( h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| spl14_43 ),
inference(avatar_component_clause,[],[f796]) ).
fof(f800,definition,
( spl14_44
<=> h1(op1(e10,e13)) = op2(h1(e10),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl14_44])],[avatar_definition]) ).
fof(f802,plain,
( h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| spl14_44 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f804,definition,
( spl14_45
<=> h1(op1(e11,e10)) = op2(h1(e11),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl14_45])],[avatar_definition]) ).
fof(f806,plain,
( h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| spl14_45 ),
inference(avatar_component_clause,[],[f804]) ).
fof(f808,definition,
( spl14_46
<=> h1(op1(e11,e11)) = op2(h1(e11),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl14_46])],[avatar_definition]) ).
fof(f810,plain,
( h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| spl14_46 ),
inference(avatar_component_clause,[],[f808]) ).
fof(f812,definition,
( spl14_47
<=> h1(op1(e11,e12)) = op2(h1(e11),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl14_47])],[avatar_definition]) ).
fof(f814,plain,
( h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| spl14_47 ),
inference(avatar_component_clause,[],[f812]) ).
fof(f816,definition,
( spl14_48
<=> h1(op1(e11,e13)) = op2(h1(e11),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl14_48])],[avatar_definition]) ).
fof(f818,plain,
( h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| spl14_48 ),
inference(avatar_component_clause,[],[f816]) ).
fof(f820,definition,
( spl14_49
<=> h1(op1(e12,e10)) = op2(h1(e12),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl14_49])],[avatar_definition]) ).
fof(f822,plain,
( h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| spl14_49 ),
inference(avatar_component_clause,[],[f820]) ).
fof(f824,definition,
( spl14_50
<=> h1(op1(e12,e11)) = op2(h1(e12),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl14_50])],[avatar_definition]) ).
fof(f826,plain,
( h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| spl14_50 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f828,definition,
( spl14_51
<=> h1(op1(e12,e12)) = op2(h1(e12),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl14_51])],[avatar_definition]) ).
fof(f830,plain,
( h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| spl14_51 ),
inference(avatar_component_clause,[],[f828]) ).
fof(f832,definition,
( spl14_52
<=> h1(op1(e12,e13)) = op2(h1(e12),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl14_52])],[avatar_definition]) ).
fof(f834,plain,
( h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| spl14_52 ),
inference(avatar_component_clause,[],[f832]) ).
fof(f836,definition,
( spl14_53
<=> h1(op1(e13,e10)) = op2(h1(e13),h1(e10)) ),
introduced(definition,[new_symbols(definition,[spl14_53])],[avatar_definition]) ).
fof(f838,plain,
( h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| spl14_53 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f840,definition,
( spl14_54
<=> h1(op1(e13,e11)) = op2(h1(e13),h1(e11)) ),
introduced(definition,[new_symbols(definition,[spl14_54])],[avatar_definition]) ).
fof(f842,plain,
( h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| spl14_54 ),
inference(avatar_component_clause,[],[f840]) ).
fof(f844,definition,
( spl14_55
<=> h1(op1(e13,e12)) = op2(h1(e13),h1(e12)) ),
introduced(definition,[new_symbols(definition,[spl14_55])],[avatar_definition]) ).
fof(f846,plain,
( h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| spl14_55 ),
inference(avatar_component_clause,[],[f844]) ).
fof(f848,definition,
( spl14_56
<=> h1(op1(e13,e13)) = op2(h1(e13),h1(e13)) ),
introduced(definition,[new_symbols(definition,[spl14_56])],[avatar_definition]) ).
fof(f850,plain,
( h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| spl14_56 ),
inference(avatar_component_clause,[],[f848]) ).
fof(f861,definition,
( spl14_59
<=> e22 = h1(e12) ),
introduced(definition,[new_symbols(definition,[spl14_59])],[avatar_definition]) ).
fof(f862,plain,
( e22 = h1(e12)
| ~ spl14_59 ),
inference(avatar_component_clause,[],[f861]) ).
fof(f892,definition,
( spl14_64
<=> e23 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl14_64])],[avatar_definition]) ).
fof(f893,plain,
( e23 = h1(e13)
| ~ spl14_64 ),
inference(avatar_component_clause,[],[f892]) ).
fof(f896,plain,
( ~ spl14_41
| ~ spl14_42
| ~ spl14_43
| ~ spl14_44
| ~ spl14_45
| ~ spl14_46
| ~ spl14_47
| ~ spl14_48
| ~ spl14_49
| ~ spl14_50
| ~ spl14_51
| ~ spl14_52
| ~ spl14_53
| ~ spl14_54
| ~ spl14_55
| ~ spl14_56
| ~ spl14_1
| spl14_6
| ~ spl14_59
| ~ spl14_64 ),
inference(avatar_split_clause,[],[f569,f892,f861,f620,f596,f848,f844,f840,f836,f832,f828,f824,f820,f816,f812,f808,f804,f800,f796,f792,f788]) ).
fof(f1095,definition,
( spl14_109
<=> e22 = h3(e10) ),
introduced(definition,[new_symbols(definition,[spl14_109])],[avatar_definition]) ).
fof(f1096,plain,
( e22 = h3(e10)
| ~ spl14_109 ),
inference(avatar_component_clause,[],[f1095]) ).
fof(f1116,definition,
( spl14_112
<=> e23 = h3(e13) ),
introduced(definition,[new_symbols(definition,[spl14_112])],[avatar_definition]) ).
fof(f1117,plain,
( e23 = h3(e13)
| ~ spl14_112 ),
inference(avatar_component_clause,[],[f1116]) ).
fof(f1236,plain,
spl14_109,
inference(avatar_split_clause,[],[f362,f1095]) ).
fof(f1238,plain,
spl14_5,
inference(avatar_split_clause,[],[f354,f615]) ).
fof(f1240,definition,
( spl14_137
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl14_137])],[avatar_definition]) ).
fof(f1244,definition,
( spl14_138
<=> e20 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl14_138])],[avatar_definition]) ).
fof(f1245,plain,
( e20 = op2(e20,e21)
| ~ spl14_138 ),
inference(avatar_component_clause,[],[f1244]) ).
fof(f1248,definition,
( spl14_139
<=> op2(e20,e20) = e21 ),
introduced(definition,[new_symbols(definition,[spl14_139])],[avatar_definition]) ).
fof(f1250,plain,
( op2(e20,e20) = e21
| ~ spl14_139 ),
inference(avatar_component_clause,[],[f1248]) ).
fof(f1251,plain,
( ~ spl14_137
| ~ spl14_138
| spl14_139 ),
inference(avatar_split_clause,[],[f293,f1248,f1244,f1240]) ).
fof(f1253,definition,
( spl14_140
<=> e20 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl14_140])],[avatar_definition]) ).
fof(f1254,plain,
( e20 = op2(e20,e22)
| ~ spl14_140 ),
inference(avatar_component_clause,[],[f1253]) ).
fof(f1257,definition,
( spl14_141
<=> op2(e20,e20) = e22 ),
introduced(definition,[new_symbols(definition,[spl14_141])],[avatar_definition]) ).
fof(f1259,plain,
( op2(e20,e20) = e22
| ~ spl14_141 ),
inference(avatar_component_clause,[],[f1257]) ).
fof(f1260,plain,
( ~ spl14_137
| ~ spl14_140
| spl14_141 ),
inference(avatar_split_clause,[],[f294,f1257,f1253,f1240]) ).
fof(f1262,definition,
( spl14_142
<=> e20 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl14_142])],[avatar_definition]) ).
fof(f1263,plain,
( e20 = op2(e20,e23)
| ~ spl14_142 ),
inference(avatar_component_clause,[],[f1262]) ).
fof(f1266,definition,
( spl14_143
<=> op2(e20,e20) = e23 ),
introduced(definition,[new_symbols(definition,[spl14_143])],[avatar_definition]) ).
fof(f1268,plain,
( op2(e20,e20) = e23
| ~ spl14_143 ),
inference(avatar_component_clause,[],[f1266]) ).
fof(f1271,definition,
( spl14_144
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl14_144])],[avatar_definition]) ).
fof(f1272,plain,
( e20 = op2(e21,e21)
| ~ spl14_144 ),
inference(avatar_component_clause,[],[f1271]) ).
fof(f1275,definition,
( spl14_145
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl14_145])],[avatar_definition]) ).
fof(f1277,plain,
( e21 = op2(e21,e20)
| ~ spl14_145 ),
inference(avatar_component_clause,[],[f1275]) ).
fof(f1289,definition,
( spl14_148
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl14_148])],[avatar_definition]) ).
fof(f1290,plain,
( e20 = op2(e21,e23)
| ~ spl14_148 ),
inference(avatar_component_clause,[],[f1289]) ).
fof(f1293,definition,
( spl14_149
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl14_149])],[avatar_definition]) ).
fof(f1295,plain,
( e23 = op2(e21,e20)
| ~ spl14_149 ),
inference(avatar_component_clause,[],[f1293]) ).
fof(f1298,definition,
( spl14_150
<=> e20 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl14_150])],[avatar_definition]) ).
fof(f1299,plain,
( e20 = op2(e22,e21)
| ~ spl14_150 ),
inference(avatar_component_clause,[],[f1298]) ).
fof(f1302,definition,
( spl14_151
<=> e21 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl14_151])],[avatar_definition]) ).
fof(f1304,plain,
( e21 = op2(e22,e20)
| ~ spl14_151 ),
inference(avatar_component_clause,[],[f1302]) ).
fof(f1307,definition,
( spl14_152
<=> e20 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl14_152])],[avatar_definition]) ).
fof(f1308,plain,
( e20 = op2(e22,e22)
| ~ spl14_152 ),
inference(avatar_component_clause,[],[f1307]) ).
fof(f1311,definition,
( spl14_153
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl14_153])],[avatar_definition]) ).
fof(f1313,plain,
( e22 = op2(e22,e20)
| ~ spl14_153 ),
inference(avatar_component_clause,[],[f1311]) ).
fof(f1314,plain,
( ~ spl14_137
| ~ spl14_152
| spl14_153 ),
inference(avatar_split_clause,[],[f300,f1311,f1307,f1240]) ).
fof(f1316,definition,
( spl14_154
<=> e20 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl14_154])],[avatar_definition]) ).
fof(f1317,plain,
( e20 = op2(e22,e23)
| ~ spl14_154 ),
inference(avatar_component_clause,[],[f1316]) ).
fof(f1325,definition,
( spl14_156
<=> e20 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl14_156])],[avatar_definition]) ).
fof(f1326,plain,
( e20 = op2(e23,e21)
| ~ spl14_156 ),
inference(avatar_component_clause,[],[f1325]) ).
fof(f1329,definition,
( spl14_157
<=> e21 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl14_157])],[avatar_definition]) ).
fof(f1330,plain,
( e21 != op2(e23,e20)
| spl14_157 ),
inference(avatar_component_clause,[],[f1329]) ).
fof(f1331,plain,
( e21 = op2(e23,e20)
| ~ spl14_157 ),
inference(avatar_component_clause,[],[f1329]) ).
fof(f1334,definition,
( spl14_158
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl14_158])],[avatar_definition]) ).
fof(f1335,plain,
( e20 = op2(e23,e22)
| ~ spl14_158 ),
inference(avatar_component_clause,[],[f1334]) ).
fof(f1338,definition,
( spl14_159
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl14_159])],[avatar_definition]) ).
fof(f1340,plain,
( e22 = op2(e23,e20)
| ~ spl14_159 ),
inference(avatar_component_clause,[],[f1338]) ).
fof(f1343,definition,
( spl14_160
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl14_160])],[avatar_definition]) ).
fof(f1344,plain,
( e20 = op2(e23,e23)
| ~ spl14_160 ),
inference(avatar_component_clause,[],[f1343]) ).
fof(f1347,definition,
( spl14_161
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl14_161])],[avatar_definition]) ).
fof(f1349,plain,
( e23 = op2(e23,e20)
| ~ spl14_161 ),
inference(avatar_component_clause,[],[f1347]) ).
fof(f1352,definition,
( spl14_162
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl14_162])],[avatar_definition]) ).
fof(f1357,definition,
( spl14_163
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl14_163])],[avatar_definition]) ).
fof(f1358,plain,
( e21 = op2(e20,e22)
| ~ spl14_163 ),
inference(avatar_component_clause,[],[f1357]) ).
fof(f1361,definition,
( spl14_164
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl14_164])],[avatar_definition]) ).
fof(f1366,definition,
( spl14_165
<=> e21 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl14_165])],[avatar_definition]) ).
fof(f1367,plain,
( e21 = op2(e20,e23)
| ~ spl14_165 ),
inference(avatar_component_clause,[],[f1366]) ).
fof(f1376,definition,
( spl14_167
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl14_167])],[avatar_definition]) ).
fof(f1377,plain,
( e21 = op2(e21,e22)
| ~ spl14_167 ),
inference(avatar_component_clause,[],[f1376]) ).
fof(f1380,definition,
( spl14_168
<=> e22 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl14_168])],[avatar_definition]) ).
fof(f1382,plain,
( e22 = op2(e21,e21)
| ~ spl14_168 ),
inference(avatar_component_clause,[],[f1380]) ).
fof(f1385,definition,
( spl14_169
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl14_169])],[avatar_definition]) ).
fof(f1389,definition,
( spl14_170
<=> e23 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl14_170])],[avatar_definition]) ).
fof(f1392,plain,
( spl14_162
| ~ spl14_169
| spl14_170 ),
inference(avatar_split_clause,[],[f529,f1389,f1385,f1352]) ).
fof(f1393,plain,
( spl14_162
| ~ spl14_151
| spl14_150 ),
inference(avatar_split_clause,[],[f528,f1298,f1302,f1352]) ).
fof(f1395,definition,
( spl14_171
<=> e21 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl14_171])],[avatar_definition]) ).
fof(f1396,plain,
( e21 = op2(e22,e22)
| ~ spl14_171 ),
inference(avatar_component_clause,[],[f1395]) ).
fof(f1399,definition,
( spl14_172
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl14_172])],[avatar_definition]) ).
fof(f1401,plain,
( e22 = op2(e22,e21)
| ~ spl14_172 ),
inference(avatar_component_clause,[],[f1399]) ).
fof(f1414,definition,
( spl14_175
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl14_175])],[avatar_definition]) ).
fof(f1415,plain,
( e21 = op2(e23,e22)
| ~ spl14_175 ),
inference(avatar_component_clause,[],[f1414]) ).
fof(f1423,definition,
( spl14_177
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl14_177])],[avatar_definition]) ).
fof(f1424,plain,
( e21 = op2(e23,e23)
| ~ spl14_177 ),
inference(avatar_component_clause,[],[f1423]) ).
fof(f1427,definition,
( spl14_178
<=> e23 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl14_178])],[avatar_definition]) ).
fof(f1429,plain,
( e23 = op2(e23,e21)
| ~ spl14_178 ),
inference(avatar_component_clause,[],[f1427]) ).
fof(f1432,definition,
( spl14_179
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl14_179])],[avatar_definition]) ).
fof(f1438,definition,
( spl14_180
<=> e22 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl14_180])],[avatar_definition]) ).
fof(f1439,plain,
( e22 = op2(e20,e23)
| ~ spl14_180 ),
inference(avatar_component_clause,[],[f1438]) ).
fof(f1442,definition,
( spl14_181
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl14_181])],[avatar_definition]) ).
fof(f1447,plain,
( spl14_179
| ~ spl14_168
| spl14_167 ),
inference(avatar_split_clause,[],[f518,f1376,f1380,f1432]) ).
fof(f1449,definition,
( spl14_182
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl14_182])],[avatar_definition]) ).
fof(f1450,plain,
( e22 = op2(e21,e23)
| ~ spl14_182 ),
inference(avatar_component_clause,[],[f1449]) ).
fof(f1453,definition,
( spl14_183
<=> e23 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl14_183])],[avatar_definition]) ).
fof(f1455,plain,
( e23 = op2(e21,e22)
| ~ spl14_183 ),
inference(avatar_component_clause,[],[f1453]) ).
fof(f1460,definition,
( spl14_184
<=> e22 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl14_184])],[avatar_definition]) ).
fof(f1461,plain,
( e22 = op2(e22,e23)
| ~ spl14_184 ),
inference(avatar_component_clause,[],[f1460]) ).
fof(f1464,definition,
( spl14_185
<=> e23 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl14_185])],[avatar_definition]) ).
fof(f1466,plain,
( e23 = op2(e22,e22)
| ~ spl14_185 ),
inference(avatar_component_clause,[],[f1464]) ).
fof(f1468,plain,
( spl14_179
| ~ spl14_159
| spl14_158 ),
inference(avatar_split_clause,[],[f513,f1334,f1338,f1432]) ).
fof(f1471,definition,
( spl14_186
<=> e22 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl14_186])],[avatar_definition]) ).
fof(f1472,plain,
( e22 = op2(e23,e23)
| ~ spl14_186 ),
inference(avatar_component_clause,[],[f1471]) ).
fof(f1475,definition,
( spl14_187
<=> e23 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl14_187])],[avatar_definition]) ).
fof(f1477,plain,
( e23 = op2(e23,e22)
| ~ spl14_187 ),
inference(avatar_component_clause,[],[f1475]) ).
fof(f1479,plain,
( spl14_137
| ~ spl14_162
| ~ spl14_179
| ~ spl14_143
| spl14_142 ),
inference(avatar_split_clause,[],[f510,f1262,f1266,f1432,f1352,f1240]) ).
fof(f1490,plain,
( spl14_137
| ~ spl14_162
| ~ spl14_179
| ~ spl14_187
| spl14_186 ),
inference(avatar_split_clause,[],[f499,f1471,f1475,f1432,f1352,f1240]) ).
fof(f1492,definition,
( spl14_188
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl14_188])],[avatar_definition]) ).
fof(f1496,definition,
( spl14_189
<=> e10 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl14_189])],[avatar_definition]) ).
fof(f1505,definition,
( spl14_191
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl14_191])],[avatar_definition]) ).
fof(f1509,definition,
( spl14_192
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[spl14_192])],[avatar_definition]) ).
fof(f1511,plain,
( op1(e10,e10) = e12
| ~ spl14_192 ),
inference(avatar_component_clause,[],[f1509]) ).
fof(f1514,definition,
( spl14_193
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl14_193])],[avatar_definition]) ).
fof(f1515,plain,
( e10 = op1(e10,e13)
| ~ spl14_193 ),
inference(avatar_component_clause,[],[f1514]) ).
fof(f1518,definition,
( spl14_194
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl14_194])],[avatar_definition]) ).
fof(f1520,plain,
( op1(e10,e10) = e13
| ~ spl14_194 ),
inference(avatar_component_clause,[],[f1518]) ).
fof(f1523,definition,
( spl14_195
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl14_195])],[avatar_definition]) ).
fof(f1527,definition,
( spl14_196
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl14_196])],[avatar_definition]) ).
fof(f1529,plain,
( e11 = op1(e11,e10)
| ~ spl14_196 ),
inference(avatar_component_clause,[],[f1527]) ).
fof(f1536,definition,
( spl14_198
<=> e12 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl14_198])],[avatar_definition]) ).
fof(f1538,plain,
( e12 = op1(e11,e10)
| ~ spl14_198 ),
inference(avatar_component_clause,[],[f1536]) ).
fof(f1541,definition,
( spl14_199
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl14_199])],[avatar_definition]) ).
fof(f1550,definition,
( spl14_201
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl14_201])],[avatar_definition]) ).
fof(f1551,plain,
( e10 = op1(e12,e11)
| ~ spl14_201 ),
inference(avatar_component_clause,[],[f1550]) ).
fof(f1554,definition,
( spl14_202
<=> e11 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl14_202])],[avatar_definition]) ).
fof(f1556,plain,
( e11 = op1(e12,e10)
| ~ spl14_202 ),
inference(avatar_component_clause,[],[f1554]) ).
fof(f1559,definition,
( spl14_203
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl14_203])],[avatar_definition]) ).
fof(f1560,plain,
( e10 = op1(e12,e12)
| ~ spl14_203 ),
inference(avatar_component_clause,[],[f1559]) ).
fof(f1563,definition,
( spl14_204
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl14_204])],[avatar_definition]) ).
fof(f1565,plain,
( e12 = op1(e12,e10)
| ~ spl14_204 ),
inference(avatar_component_clause,[],[f1563]) ).
fof(f1566,plain,
( spl14_188
| ~ spl14_203
| spl14_204 ),
inference(avatar_split_clause,[],[f491,f1563,f1559,f1492]) ).
fof(f1568,definition,
( spl14_205
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl14_205])],[avatar_definition]) ).
fof(f1569,plain,
( e10 = op1(e12,e13)
| ~ spl14_205 ),
inference(avatar_component_clause,[],[f1568]) ).
fof(f1577,definition,
( spl14_207
<=> e10 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl14_207])],[avatar_definition]) ).
fof(f1578,plain,
( e10 = op1(e13,e11)
| ~ spl14_207 ),
inference(avatar_component_clause,[],[f1577]) ).
fof(f1581,definition,
( spl14_208
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl14_208])],[avatar_definition]) ).
fof(f1583,plain,
( e11 = op1(e13,e10)
| ~ spl14_208 ),
inference(avatar_component_clause,[],[f1581]) ).
fof(f1584,plain,
( spl14_188
| ~ spl14_207
| spl14_208 ),
inference(avatar_split_clause,[],[f489,f1581,f1577,f1492]) ).
fof(f1586,definition,
( spl14_209
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl14_209])],[avatar_definition]) ).
fof(f1587,plain,
( e10 = op1(e13,e12)
| ~ spl14_209 ),
inference(avatar_component_clause,[],[f1586]) ).
fof(f1590,definition,
( spl14_210
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl14_210])],[avatar_definition]) ).
fof(f1592,plain,
( e12 = op1(e13,e10)
| ~ spl14_210 ),
inference(avatar_component_clause,[],[f1590]) ).
fof(f1595,definition,
( spl14_211
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl14_211])],[avatar_definition]) ).
fof(f1596,plain,
( e10 = op1(e13,e13)
| ~ spl14_211 ),
inference(avatar_component_clause,[],[f1595]) ).
fof(f1599,definition,
( spl14_212
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl14_212])],[avatar_definition]) ).
fof(f1602,plain,
( spl14_188
| ~ spl14_211
| spl14_212 ),
inference(avatar_split_clause,[],[f487,f1599,f1595,f1492]) ).
fof(f1604,definition,
( spl14_213
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl14_213])],[avatar_definition]) ).
fof(f1613,definition,
( spl14_215
<=> e12 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl14_215])],[avatar_definition]) ).
fof(f1615,plain,
( e12 = op1(e10,e11)
| ~ spl14_215 ),
inference(avatar_component_clause,[],[f1613]) ).
fof(f1618,definition,
( spl14_216
<=> e11 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl14_216])],[avatar_definition]) ).
fof(f1622,definition,
( spl14_217
<=> e13 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl14_217])],[avatar_definition]) ).
fof(f1628,definition,
( spl14_218
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl14_218])],[avatar_definition]) ).
fof(f1629,plain,
( e11 = op1(e11,e12)
| ~ spl14_218 ),
inference(avatar_component_clause,[],[f1628]) ).
fof(f1632,definition,
( spl14_219
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl14_219])],[avatar_definition]) ).
fof(f1634,plain,
( e12 = op1(e11,e11)
| ~ spl14_219 ),
inference(avatar_component_clause,[],[f1632]) ).
fof(f1635,plain,
( spl14_213
| ~ spl14_218
| spl14_219 ),
inference(avatar_split_clause,[],[f482,f1632,f1628,f1604]) ).
fof(f1637,definition,
( spl14_220
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl14_220])],[avatar_definition]) ).
fof(f1638,plain,
( e11 = op1(e11,e13)
| ~ spl14_220 ),
inference(avatar_component_clause,[],[f1637]) ).
fof(f1641,definition,
( spl14_221
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl14_221])],[avatar_definition]) ).
fof(f1643,plain,
( e13 = op1(e11,e11)
| ~ spl14_221 ),
inference(avatar_component_clause,[],[f1641]) ).
fof(f1645,plain,
( spl14_213
| ~ spl14_202
| spl14_201 ),
inference(avatar_split_clause,[],[f480,f1550,f1554,f1604]) ).
fof(f1647,definition,
( spl14_222
<=> e11 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl14_222])],[avatar_definition]) ).
fof(f1651,definition,
( spl14_223
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl14_223])],[avatar_definition]) ).
fof(f1656,definition,
( spl14_224
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl14_224])],[avatar_definition]) ).
fof(f1657,plain,
( e11 = op1(e12,e13)
| ~ spl14_224 ),
inference(avatar_component_clause,[],[f1656]) ).
fof(f1660,definition,
( spl14_225
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl14_225])],[avatar_definition]) ).
fof(f1666,definition,
( spl14_226
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl14_226])],[avatar_definition]) ).
fof(f1667,plain,
( e11 = op1(e13,e12)
| ~ spl14_226 ),
inference(avatar_component_clause,[],[f1666]) ).
fof(f1675,definition,
( spl14_228
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl14_228])],[avatar_definition]) ).
fof(f1676,plain,
( e11 = op1(e13,e13)
| ~ spl14_228 ),
inference(avatar_component_clause,[],[f1675]) ).
fof(f1679,definition,
( spl14_229
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl14_229])],[avatar_definition]) ).
fof(f1681,plain,
( e13 = op1(e13,e11)
| ~ spl14_229 ),
inference(avatar_component_clause,[],[f1679]) ).
fof(f1682,plain,
( spl14_213
| ~ spl14_228
| spl14_229 ),
inference(avatar_split_clause,[],[f475,f1679,f1675,f1604]) ).
fof(f1684,definition,
( spl14_230
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl14_230])],[avatar_definition]) ).
fof(f1690,definition,
( spl14_231
<=> e12 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl14_231])],[avatar_definition]) ).
fof(f1691,plain,
( e12 = op1(e10,e13)
| ~ spl14_231 ),
inference(avatar_component_clause,[],[f1690]) ).
fof(f1694,definition,
( spl14_232
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl14_232])],[avatar_definition]) ).
fof(f1697,plain,
( ~ spl14_230
| ~ spl14_231
| spl14_232 ),
inference(avatar_split_clause,[],[f267,f1694,f1690,f1684]) ).
fof(f1701,definition,
( spl14_233
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl14_233])],[avatar_definition]) ).
fof(f1702,plain,
( e12 = op1(e11,e13)
| ~ spl14_233 ),
inference(avatar_component_clause,[],[f1701]) ).
fof(f1705,definition,
( spl14_234
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl14_234])],[avatar_definition]) ).
fof(f1708,plain,
( ~ spl14_230
| ~ spl14_233
| spl14_234 ),
inference(avatar_split_clause,[],[f270,f1705,f1701,f1684]) ).
fof(f1712,definition,
( spl14_235
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl14_235])],[avatar_definition]) ).
fof(f1713,plain,
( e12 = op1(e12,e13)
| ~ spl14_235 ),
inference(avatar_component_clause,[],[f1712]) ).
fof(f1716,definition,
( spl14_236
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl14_236])],[avatar_definition]) ).
fof(f1718,plain,
( e13 = op1(e12,e12)
| ~ spl14_236 ),
inference(avatar_component_clause,[],[f1716]) ).
fof(f1720,plain,
( ~ spl14_230
| ~ spl14_210
| spl14_209 ),
inference(avatar_split_clause,[],[f274,f1586,f1590,f1684]) ).
fof(f1723,definition,
( spl14_237
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl14_237])],[avatar_definition]) ).
fof(f1724,plain,
( e12 = op1(e13,e13)
| ~ spl14_237 ),
inference(avatar_component_clause,[],[f1723]) ).
fof(f1727,definition,
( spl14_238
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl14_238])],[avatar_definition]) ).
fof(f1729,plain,
( e13 = op1(e13,e12)
| ~ spl14_238 ),
inference(avatar_component_clause,[],[f1727]) ).
fof(f1731,plain,
( ~ spl14_188
| ~ spl14_213
| spl14_230
| ~ spl14_194
| spl14_193 ),
inference(avatar_split_clause,[],[f474,f1514,f1518,f1684,f1604,f1492]) ).
fof(f1735,plain,
( ~ spl14_188
| ~ spl14_213
| spl14_230
| ~ spl14_221
| spl14_220 ),
inference(avatar_split_clause,[],[f470,f1637,f1641,f1684,f1604,f1492]) ).
fof(f1738,plain,
( ~ spl14_188
| ~ spl14_213
| spl14_230
| ~ spl14_225
| spl14_224 ),
inference(avatar_split_clause,[],[f467,f1656,f1660,f1684,f1604,f1492]) ).
fof(f1742,plain,
( ~ spl14_188
| ~ spl14_213
| spl14_230
| ~ spl14_238
| spl14_237 ),
inference(avatar_split_clause,[],[f463,f1723,f1727,f1684,f1604,f1492]) ).
fof(f1744,definition,
( spl14_239
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl14_239])],[avatar_definition]) ).
fof(f1747,plain,
( spl14_239
| spl14_138
| spl14_140
| spl14_142 ),
inference(avatar_split_clause,[],[f85,f1262,f1253,f1244,f1744]) ).
fof(f1749,definition,
( spl14_240
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl14_240])],[avatar_definition]) ).
fof(f1751,plain,
( e20 = op2(e21,e20)
| ~ spl14_240 ),
inference(avatar_component_clause,[],[f1749]) ).
fof(f1753,definition,
( spl14_241
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl14_241])],[avatar_definition]) ).
fof(f1755,plain,
( e20 = op2(e22,e20)
| ~ spl14_241 ),
inference(avatar_component_clause,[],[f1753]) ).
fof(f1757,definition,
( spl14_242
<=> e20 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl14_242])],[avatar_definition]) ).
fof(f1759,plain,
( e20 = op2(e23,e20)
| ~ spl14_242 ),
inference(avatar_component_clause,[],[f1757]) ).
fof(f1760,plain,
( spl14_239
| spl14_240
| spl14_241
| spl14_242 ),
inference(avatar_split_clause,[],[f86,f1757,f1753,f1749,f1744]) ).
fof(f1762,definition,
( spl14_243
<=> e21 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl14_243])],[avatar_definition]) ).
fof(f1764,plain,
( e21 = op2(e20,e21)
| ~ spl14_243 ),
inference(avatar_component_clause,[],[f1762]) ).
fof(f1765,plain,
( spl14_139
| spl14_243
| spl14_163
| spl14_165 ),
inference(avatar_split_clause,[],[f87,f1366,f1357,f1762,f1248]) ).
fof(f1768,definition,
( spl14_244
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl14_244])],[avatar_definition]) ).
fof(f1770,plain,
( e22 = op2(e20,e22)
| ~ spl14_244 ),
inference(avatar_component_clause,[],[f1768]) ).
fof(f1771,plain,
( spl14_141
| spl14_164
| spl14_244
| spl14_180 ),
inference(avatar_split_clause,[],[f89,f1438,f1768,f1361,f1257]) ).
fof(f1782,definition,
( spl14_246
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl14_246])],[avatar_definition]) ).
fof(f1785,plain,
( spl14_145
| spl14_246
| spl14_167
| spl14_169 ),
inference(avatar_split_clause,[],[f95,f1385,f1376,f1782,f1275]) ).
fof(f1791,definition,
( spl14_248
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl14_248])],[avatar_definition]) ).
fof(f1793,plain,
( e21 = op2(e23,e21)
| ~ spl14_248 ),
inference(avatar_component_clause,[],[f1791]) ).
fof(f1802,definition,
( spl14_250
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl14_250])],[avatar_definition]) ).
fof(f1804,plain,
( e23 = op2(e21,e23)
| ~ spl14_250 ),
inference(avatar_component_clause,[],[f1802]) ).
fof(f1805,plain,
( spl14_149
| spl14_170
| spl14_183
| spl14_250 ),
inference(avatar_split_clause,[],[f99,f1802,f1453,f1389,f1293]) ).
fof(f1807,plain,
( spl14_241
| spl14_150
| spl14_152
| spl14_154 ),
inference(avatar_split_clause,[],[f101,f1316,f1307,f1298,f1753]) ).
fof(f1810,plain,
( spl14_163
| spl14_167
| spl14_171
| spl14_175 ),
inference(avatar_split_clause,[],[f104,f1414,f1395,f1376,f1357]) ).
fof(f1812,definition,
( spl14_251
<=> e22 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl14_251])],[avatar_definition]) ).
fof(f1815,plain,
( spl14_153
| spl14_172
| spl14_251
| spl14_184 ),
inference(avatar_split_clause,[],[f105,f1460,f1812,f1399,f1311]) ).
fof(f1817,definition,
( spl14_252
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl14_252])],[avatar_definition]) ).
fof(f1827,plain,
( spl14_242
| spl14_156
| spl14_158
| spl14_160 ),
inference(avatar_split_clause,[],[f109,f1343,f1334,f1325,f1757]) ).
fof(f1828,plain,
( spl14_142
| spl14_148
| spl14_154
| spl14_160 ),
inference(avatar_split_clause,[],[f110,f1343,f1316,f1289,f1262]) ).
fof(f1829,plain,
( spl14_157
| spl14_248
| spl14_175
| spl14_177 ),
inference(avatar_split_clause,[],[f111,f1423,f1414,f1791,f1329]) ).
fof(f1832,plain,
( spl14_180
| spl14_182
| spl14_184
| spl14_186 ),
inference(avatar_split_clause,[],[f114,f1471,f1460,f1449,f1438]) ).
fof(f1834,definition,
( spl14_254
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl14_254])],[avatar_definition]) ).
fof(f1837,plain,
( spl14_161
| spl14_178
| spl14_187
| spl14_254 ),
inference(avatar_split_clause,[],[f115,f1834,f1475,f1427,f1347]) ).
fof(f1841,plain,
( spl14_140
| spl14_163
| spl14_244
| spl14_181 ),
inference(avatar_split_clause,[],[f71,f1442,f1768,f1357,f1253]) ).
fof(f1844,plain,
( spl14_144
| spl14_246
| spl14_168
| spl14_170 ),
inference(avatar_split_clause,[],[f74,f1389,f1380,f1782,f1271]) ).
fof(f1849,plain,
( spl14_152
| spl14_171
| spl14_251
| spl14_185 ),
inference(avatar_split_clause,[],[f79,f1464,f1812,f1395,f1307]) ).
fof(f1856,definition,
( spl14_255
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl14_255])],[avatar_definition]) ).
fof(f1859,plain,
( spl14_255
| spl14_189
| spl14_191
| spl14_193 ),
inference(avatar_split_clause,[],[f37,f1514,f1505,f1496,f1856]) ).
fof(f1861,definition,
( spl14_256
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl14_256])],[avatar_definition]) ).
fof(f1863,plain,
( e10 = op1(e11,e10)
| ~ spl14_256 ),
inference(avatar_component_clause,[],[f1861]) ).
fof(f1865,definition,
( spl14_257
<=> e10 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl14_257])],[avatar_definition]) ).
fof(f1867,plain,
( e10 = op1(e12,e10)
| ~ spl14_257 ),
inference(avatar_component_clause,[],[f1865]) ).
fof(f1869,definition,
( spl14_258
<=> e10 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl14_258])],[avatar_definition]) ).
fof(f1871,plain,
( e10 = op1(e13,e10)
| ~ spl14_258 ),
inference(avatar_component_clause,[],[f1869]) ).
fof(f1872,plain,
( spl14_255
| spl14_256
| spl14_257
| spl14_258 ),
inference(avatar_split_clause,[],[f38,f1869,f1865,f1861,f1856]) ).
fof(f1874,definition,
( spl14_259
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl14_259])],[avatar_definition]) ).
fof(f1876,plain,
( e11 = op1(e10,e11)
| ~ spl14_259 ),
inference(avatar_component_clause,[],[f1874]) ).
fof(f1880,definition,
( spl14_260
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl14_260])],[avatar_definition]) ).
fof(f1882,plain,
( e12 = op1(e10,e12)
| ~ spl14_260 ),
inference(avatar_component_clause,[],[f1880]) ).
fof(f1883,plain,
( spl14_192
| spl14_215
| spl14_260
| spl14_231 ),
inference(avatar_split_clause,[],[f41,f1690,f1880,f1613,f1509]) ).
fof(f1886,definition,
( spl14_261
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl14_261])],[avatar_definition]) ).
fof(f1892,plain,
( spl14_189
| spl14_195
| spl14_201
| spl14_207 ),
inference(avatar_split_clause,[],[f46,f1577,f1550,f1523,f1496]) ).
fof(f1894,definition,
( spl14_262
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl14_262])],[avatar_definition]) ).
fof(f1897,plain,
( spl14_196
| spl14_262
| spl14_218
| spl14_220 ),
inference(avatar_split_clause,[],[f47,f1637,f1628,f1894,f1527]) ).
fof(f1899,definition,
( spl14_263
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl14_263])],[avatar_definition]) ).
fof(f1903,definition,
( spl14_264
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl14_264])],[avatar_definition]) ).
fof(f1905,plain,
( e11 = op1(e13,e11)
| ~ spl14_264 ),
inference(avatar_component_clause,[],[f1903]) ).
fof(f1906,plain,
( spl14_259
| spl14_262
| spl14_263
| spl14_264 ),
inference(avatar_split_clause,[],[f48,f1903,f1899,f1894,f1874]) ).
fof(f1908,definition,
( spl14_265
<=> e12 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl14_265])],[avatar_definition]) ).
fof(f1910,plain,
( e12 = op1(e11,e12)
| ~ spl14_265 ),
inference(avatar_component_clause,[],[f1908]) ).
fof(f1911,plain,
( spl14_198
| spl14_219
| spl14_265
| spl14_233 ),
inference(avatar_split_clause,[],[f49,f1701,f1908,f1632,f1536]) ).
fof(f1914,definition,
( spl14_266
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl14_266])],[avatar_definition]) ).
fof(f1916,plain,
( e13 = op1(e11,e13)
| ~ spl14_266 ),
inference(avatar_component_clause,[],[f1914]) ).
fof(f1918,plain,
( spl14_217
| spl14_221
| spl14_225
| spl14_229 ),
inference(avatar_split_clause,[],[f52,f1679,f1660,f1641,f1622]) ).
fof(f1919,plain,
( spl14_257
| spl14_201
| spl14_203
| spl14_205 ),
inference(avatar_split_clause,[],[f53,f1568,f1559,f1550,f1865]) ).
fof(f1924,definition,
( spl14_267
<=> e12 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl14_267])],[avatar_definition]) ).
fof(f1927,plain,
( spl14_204
| spl14_223
| spl14_267
| spl14_235 ),
inference(avatar_split_clause,[],[f57,f1712,f1924,f1651,f1563]) ).
fof(f1929,definition,
( spl14_268
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl14_268])],[avatar_definition]) ).
fof(f1932,plain,
( spl14_260
| spl14_265
| spl14_267
| spl14_268 ),
inference(avatar_split_clause,[],[f58,f1929,f1924,f1908,f1880]) ).
fof(f1934,definition,
( spl14_269
<=> e13 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl14_269])],[avatar_definition]) ).
fof(f1936,plain,
( e13 = op1(e12,e13)
| ~ spl14_269 ),
inference(avatar_component_clause,[],[f1934]) ).
fof(f1939,plain,
( spl14_258
| spl14_207
| spl14_209
| spl14_211 ),
inference(avatar_split_clause,[],[f61,f1595,f1586,f1577,f1869]) ).
fof(f1940,plain,
( spl14_193
| spl14_199
| spl14_205
| spl14_211 ),
inference(avatar_split_clause,[],[f62,f1595,f1568,f1541,f1514]) ).
fof(f1941,plain,
( spl14_208
| spl14_264
| spl14_226
| spl14_228 ),
inference(avatar_split_clause,[],[f63,f1675,f1666,f1903,f1581]) ).
fof(f1942,plain,
( spl14_216
| spl14_220
| spl14_224
| spl14_228 ),
inference(avatar_split_clause,[],[f64,f1675,f1656,f1637,f1618]) ).
fof(f1946,definition,
( spl14_270
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl14_270])],[avatar_definition]) ).
fof(f1949,plain,
( spl14_212
| spl14_229
| spl14_238
| spl14_270 ),
inference(avatar_split_clause,[],[f67,f1946,f1727,f1679,f1599]) ).
fof(f1950,plain,
( spl14_261
| spl14_266
| spl14_269
| spl14_270 ),
inference(avatar_split_clause,[],[f68,f1946,f1934,f1914,f1886]) ).
fof(f1954,plain,
( spl14_193
| spl14_216
| spl14_231
| spl14_261 ),
inference(avatar_split_clause,[],[f24,f1886,f1690,f1618,f1514]) ).
fof(f1956,plain,
( spl14_195
| spl14_262
| spl14_219
| spl14_221 ),
inference(avatar_split_clause,[],[f26,f1641,f1632,f1894,f1523]) ).
fof(f1960,plain,
( spl14_201
| spl14_263
| spl14_223
| spl14_225 ),
inference(avatar_split_clause,[],[f30,f1660,f1651,f1899,f1550]) ).
fof(f1961,plain,
( spl14_203
| spl14_222
| spl14_267
| spl14_236 ),
inference(avatar_split_clause,[],[f31,f1716,f1924,f1647,f1559]) ).
fof(f1965,plain,
( spl14_209
| spl14_226
| spl14_268
| spl14_238 ),
inference(avatar_split_clause,[],[f35,f1727,f1929,f1666,f1586]) ).
fof(f1967,plain,
( e20 != e22
| spl14_25
| ~ spl14_109 ),
inference(superposition,[],[f713,f1096]) ).
fof(f1968,plain,
( h1(op1(e10,e11)) != op2(e20,h1(e11))
| ~ spl14_5
| spl14_42 ),
inference(forward_demodulation,[],[f794,f616]) ).
fof(f1971,plain,
~ spl14_270,
inference(avatar_split_clause,[],[f289,f1946]) ).
fof(f1972,plain,
~ spl14_267,
inference(avatar_split_clause,[],[f290,f1924]) ).
fof(f1973,plain,
~ spl14_262,
inference(avatar_split_clause,[],[f291,f1894]) ).
fof(f1974,plain,
~ spl14_255,
inference(avatar_split_clause,[],[f292,f1856]) ).
fof(f1975,plain,
~ spl14_254,
inference(avatar_split_clause,[],[f341,f1834]) ).
fof(f1976,plain,
~ spl14_251,
inference(avatar_split_clause,[],[f342,f1812]) ).
fof(f1977,plain,
~ spl14_246,
inference(avatar_split_clause,[],[f343,f1782]) ).
fof(f1978,plain,
~ spl14_239,
inference(avatar_split_clause,[],[f344,f1744]) ).
fof(f1979,plain,
spl14_194,
inference(avatar_split_clause,[],[f345,f1518]) ).
fof(f1980,plain,
spl14_143,
inference(avatar_split_clause,[],[f348,f1266]) ).
fof(f1982,plain,
( e21 = e23
| ~ spl14_139
| ~ spl14_143 ),
inference(superposition,[],[f1268,f1250]) ).
fof(f1987,plain,
( $false
| ~ spl14_139
| ~ spl14_143 ),
inference(forward_subsumption_resolution,[],[f1982,f220]) ).
fof(f1988,plain,
( ~ spl14_139
| ~ spl14_143 ),
inference(avatar_contradiction_clause,[],[f1987]) ).
fof(f2014,plain,
( e21 = e22
| ~ spl14_157
| ~ spl14_159 ),
inference(superposition,[],[f1340,f1331]) ).
fof(f2018,plain,
( $false
| ~ spl14_157
| ~ spl14_159 ),
inference(forward_subsumption_resolution,[],[f2014,f221]) ).
fof(f2019,plain,
( ~ spl14_157
| ~ spl14_159 ),
inference(avatar_contradiction_clause,[],[f2018]) ).
fof(f2020,plain,
( e20 = e21
| ~ spl14_158
| ~ spl14_175 ),
inference(forward_demodulation,[],[f1415,f1335]) ).
fof(f2021,plain,
( $false
| ~ spl14_158
| ~ spl14_175 ),
inference(forward_subsumption_resolution,[],[f2020,f224]) ).
fof(f2022,plain,
( ~ spl14_158
| ~ spl14_175 ),
inference(avatar_contradiction_clause,[],[f2021]) ).
fof(f2023,plain,
( e22 = e23
| ~ spl14_141
| ~ spl14_143 ),
inference(superposition,[],[f1259,f1268]) ).
fof(f2027,plain,
( $false
| ~ spl14_141
| ~ spl14_143 ),
inference(forward_subsumption_resolution,[],[f2023,f219]) ).
fof(f2028,plain,
( ~ spl14_141
| ~ spl14_143 ),
inference(avatar_contradiction_clause,[],[f2027]) ).
fof(f2036,plain,
( e22 = e23
| ~ spl14_159
| ~ spl14_161 ),
inference(forward_demodulation,[],[f1349,f1340]) ).
fof(f2037,plain,
( $false
| ~ spl14_159
| ~ spl14_161 ),
inference(forward_subsumption_resolution,[],[f2036,f219]) ).
fof(f2038,plain,
( ~ spl14_159
| ~ spl14_161 ),
inference(avatar_contradiction_clause,[],[f2037]) ).
fof(f2067,plain,
( e20 = e22
| ~ spl14_150
| ~ spl14_172 ),
inference(superposition,[],[f1401,f1299]) ).
fof(f2071,plain,
( $false
| spl14_25
| ~ spl14_109
| ~ spl14_150
| ~ spl14_172 ),
inference(forward_subsumption_resolution,[],[f2067,f1967]) ).
fof(f2072,plain,
( spl14_25
| ~ spl14_109
| ~ spl14_150
| ~ spl14_172 ),
inference(avatar_contradiction_clause,[],[f2071]) ).
fof(f2073,plain,
( e20 = e22
| ~ spl14_25
| ~ spl14_109 ),
inference(forward_demodulation,[],[f712,f1096]) ).
fof(f2080,plain,
( e22 = op2(e22,e22)
| ~ spl14_25
| ~ spl14_109
| ~ spl14_140 ),
inference(superposition,[],[f1254,f2073]) ).
fof(f2082,plain,
( e23 = op2(e22,e22)
| ~ spl14_25
| ~ spl14_109
| ~ spl14_143 ),
inference(superposition,[],[f1268,f2073]) ).
fof(f2089,plain,
( e21 != op2(e23,e22)
| ~ spl14_25
| ~ spl14_109
| spl14_157 ),
inference(superposition,[],[f1330,f2073]) ).
fof(f2090,plain,
( e22 = op2(e23,e22)
| ~ spl14_25
| ~ spl14_109
| ~ spl14_159 ),
inference(superposition,[],[f1340,f2073]) ).
fof(f2098,plain,
( spl14_252
| ~ spl14_25
| ~ spl14_109
| ~ spl14_159 ),
inference(avatar_split_clause,[],[f2090,f1338,f1095,f711,f1817]) ).
fof(f2106,plain,
( spl14_185
| ~ spl14_25
| ~ spl14_109
| ~ spl14_143 ),
inference(avatar_split_clause,[],[f2082,f1266,f1095,f711,f1464]) ).
fof(f2108,plain,
( spl14_251
| ~ spl14_25
| ~ spl14_109
| ~ spl14_140 ),
inference(avatar_split_clause,[],[f2080,f1253,f1095,f711,f1812]) ).
fof(f2111,plain,
( e20 != e22
| spl14_25
| ~ spl14_109 ),
inference(forward_demodulation,[],[f713,f1096]) ).
fof(f2116,plain,
( e20 = e21
| ~ spl14_160
| ~ spl14_177 ),
inference(forward_demodulation,[],[f1424,f1344]) ).
fof(f2117,plain,
( $false
| ~ spl14_160
| ~ spl14_177 ),
inference(forward_subsumption_resolution,[],[f2116,f224]) ).
fof(f2118,plain,
( ~ spl14_160
| ~ spl14_177 ),
inference(avatar_contradiction_clause,[],[f2117]) ).
fof(f2120,plain,
( e20 = e23
| ~ spl14_156
| ~ spl14_178 ),
inference(superposition,[],[f1429,f1326]) ).
fof(f2125,plain,
( $false
| ~ spl14_156
| ~ spl14_178 ),
inference(forward_subsumption_resolution,[],[f2120,f222]) ).
fof(f2126,plain,
( ~ spl14_156
| ~ spl14_178 ),
inference(avatar_contradiction_clause,[],[f2125]) ).
fof(f2128,plain,
( e21 = e22
| ~ spl14_165
| ~ spl14_180 ),
inference(superposition,[],[f1439,f1367]) ).
fof(f2132,plain,
( $false
| ~ spl14_165
| ~ spl14_180 ),
inference(forward_subsumption_resolution,[],[f2128,f221]) ).
fof(f2133,plain,
( ~ spl14_165
| ~ spl14_180 ),
inference(avatar_contradiction_clause,[],[f2132]) ).
fof(f2197,plain,
( e10 = e13
| ~ spl14_205
| ~ spl14_269 ),
inference(forward_demodulation,[],[f1936,f1569]) ).
fof(f2198,plain,
( $false
| ~ spl14_205
| ~ spl14_269 ),
inference(forward_subsumption_resolution,[],[f2197,f216]) ).
fof(f2199,plain,
( ~ spl14_205
| ~ spl14_269 ),
inference(avatar_contradiction_clause,[],[f2198]) ).
fof(f2200,plain,
( e11 = e12
| ~ spl14_208
| ~ spl14_210 ),
inference(forward_demodulation,[],[f1592,f1583]) ).
fof(f2201,plain,
( $false
| ~ spl14_208
| ~ spl14_210 ),
inference(forward_subsumption_resolution,[],[f2200,f215]) ).
fof(f2202,plain,
( ~ spl14_208
| ~ spl14_210 ),
inference(avatar_contradiction_clause,[],[f2201]) ).
fof(f2216,plain,
( e10 = e13
| ~ spl14_209
| ~ spl14_238 ),
inference(forward_demodulation,[],[f1729,f1587]) ).
fof(f2217,plain,
( $false
| ~ spl14_209
| ~ spl14_238 ),
inference(forward_subsumption_resolution,[],[f2216,f216]) ).
fof(f2218,plain,
( ~ spl14_209
| ~ spl14_238 ),
inference(avatar_contradiction_clause,[],[f2217]) ).
fof(f2244,plain,
( e10 = e12
| ~ spl14_193
| ~ spl14_231 ),
inference(forward_demodulation,[],[f1691,f1515]) ).
fof(f2245,plain,
( $false
| ~ spl14_193
| ~ spl14_231 ),
inference(forward_subsumption_resolution,[],[f2244,f217]) ).
fof(f2246,plain,
( ~ spl14_193
| ~ spl14_231 ),
inference(avatar_contradiction_clause,[],[f2245]) ).
fof(f2252,plain,
( e10 = e12
| ~ spl14_211
| ~ spl14_237 ),
inference(forward_demodulation,[],[f1724,f1596]) ).
fof(f2253,plain,
( $false
| ~ spl14_211
| ~ spl14_237 ),
inference(forward_subsumption_resolution,[],[f2252,f217]) ).
fof(f2254,plain,
( ~ spl14_211
| ~ spl14_237 ),
inference(avatar_contradiction_clause,[],[f2253]) ).
fof(f2275,plain,
( e20 = e21
| ~ spl14_138
| ~ spl14_243 ),
inference(forward_demodulation,[],[f1764,f1245]) ).
fof(f2276,plain,
( $false
| ~ spl14_138
| ~ spl14_243 ),
inference(forward_subsumption_resolution,[],[f2275,f224]) ).
fof(f2277,plain,
( ~ spl14_138
| ~ spl14_243 ),
inference(avatar_contradiction_clause,[],[f2276]) ).
fof(f2278,plain,
( e20 = e22
| ~ spl14_142
| ~ spl14_180 ),
inference(forward_demodulation,[],[f1263,f1439]) ).
fof(f2280,plain,
( $false
| spl14_25
| ~ spl14_109
| ~ spl14_142
| ~ spl14_180 ),
inference(forward_subsumption_resolution,[],[f2278,f2111]) ).
fof(f2281,plain,
( spl14_25
| ~ spl14_109
| ~ spl14_142
| ~ spl14_180 ),
inference(avatar_contradiction_clause,[],[f2280]) ).
fof(f2296,plain,
( e21 = e22
| ~ spl14_177
| ~ spl14_186 ),
inference(superposition,[],[f1472,f1424]) ).
fof(f2297,plain,
( e21 = e22
| ~ spl14_177
| ~ spl14_186 ),
inference(superposition,[],[f1424,f1472]) ).
fof(f2299,plain,
( $false
| ~ spl14_177
| ~ spl14_186 ),
inference(forward_subsumption_resolution,[],[f2297,f221]) ).
fof(f2300,plain,
( ~ spl14_177
| ~ spl14_186 ),
inference(avatar_contradiction_clause,[],[f2299]) ).
fof(f2301,plain,
( $false
| ~ spl14_177
| ~ spl14_186 ),
inference(forward_subsumption_resolution,[],[f2296,f221]) ).
fof(f2302,plain,
( ~ spl14_177
| ~ spl14_186 ),
inference(avatar_contradiction_clause,[],[f2301]) ).
fof(f2313,plain,
( e20 = e22
| ~ spl14_154
| ~ spl14_184 ),
inference(superposition,[],[f1461,f1317]) ).
fof(f2317,plain,
( $false
| spl14_25
| ~ spl14_109
| ~ spl14_154
| ~ spl14_184 ),
inference(forward_subsumption_resolution,[],[f2313,f2111]) ).
fof(f2318,plain,
( spl14_25
| ~ spl14_109
| ~ spl14_154
| ~ spl14_184 ),
inference(avatar_contradiction_clause,[],[f2317]) ).
fof(f2379,plain,
( e21 = e23
| ~ spl14_178
| ~ spl14_248 ),
inference(forward_demodulation,[],[f1793,f1429]) ).
fof(f2380,plain,
( $false
| ~ spl14_178
| ~ spl14_248 ),
inference(forward_subsumption_resolution,[],[f2379,f220]) ).
fof(f2381,plain,
( ~ spl14_178
| ~ spl14_248 ),
inference(avatar_contradiction_clause,[],[f2380]) ).
fof(f2385,plain,
( e20 = e23
| ~ spl14_148
| ~ spl14_250 ),
inference(superposition,[],[f1804,f1290]) ).
fof(f2390,plain,
( $false
| ~ spl14_148
| ~ spl14_250 ),
inference(forward_subsumption_resolution,[],[f2385,f222]) ).
fof(f2391,plain,
( ~ spl14_148
| ~ spl14_250 ),
inference(avatar_contradiction_clause,[],[f2390]) ).
fof(f2404,plain,
( e20 = e21
| ~ spl14_142
| ~ spl14_165 ),
inference(superposition,[],[f1263,f1367]) ).
fof(f2410,plain,
( $false
| ~ spl14_142
| ~ spl14_165 ),
inference(forward_subsumption_resolution,[],[f2404,f224]) ).
fof(f2411,plain,
( ~ spl14_142
| ~ spl14_165 ),
inference(avatar_contradiction_clause,[],[f2410]) ).
fof(f2412,plain,
( e21 = e23
| ~ spl14_175
| ~ spl14_187 ),
inference(forward_demodulation,[],[f1415,f1477]) ).
fof(f2413,plain,
( $false
| ~ spl14_175
| ~ spl14_187 ),
inference(forward_subsumption_resolution,[],[f2412,f220]) ).
fof(f2414,plain,
( ~ spl14_175
| ~ spl14_187 ),
inference(avatar_contradiction_clause,[],[f2413]) ).
fof(f2421,plain,
( e20 = e21
| ~ spl14_156
| ~ spl14_248 ),
inference(superposition,[],[f1326,f1793]) ).
fof(f2426,plain,
( $false
| ~ spl14_156
| ~ spl14_248 ),
inference(forward_subsumption_resolution,[],[f2421,f224]) ).
fof(f2427,plain,
( ~ spl14_156
| ~ spl14_248 ),
inference(avatar_contradiction_clause,[],[f2426]) ).
fof(f2443,plain,
( e20 = e23
| ~ spl14_149
| ~ spl14_240 ),
inference(forward_demodulation,[],[f1751,f1295]) ).
fof(f2444,plain,
( $false
| ~ spl14_149
| ~ spl14_240 ),
inference(forward_subsumption_resolution,[],[f2443,f222]) ).
fof(f2445,plain,
( ~ spl14_149
| ~ spl14_240 ),
inference(avatar_contradiction_clause,[],[f2444]) ).
fof(f2478,plain,
( e10 = e11
| ~ spl14_196
| ~ spl14_256 ),
inference(superposition,[],[f1863,f1529]) ).
fof(f2482,plain,
( $false
| ~ spl14_196
| ~ spl14_256 ),
inference(forward_subsumption_resolution,[],[f2478,f218]) ).
fof(f2483,plain,
( ~ spl14_196
| ~ spl14_256 ),
inference(avatar_contradiction_clause,[],[f2482]) ).
fof(f2508,plain,
( e10 = e11
| ~ spl14_207
| ~ spl14_264 ),
inference(forward_demodulation,[],[f1905,f1578]) ).
fof(f2509,plain,
( $false
| ~ spl14_207
| ~ spl14_264 ),
inference(forward_subsumption_resolution,[],[f2508,f218]) ).
fof(f2510,plain,
( ~ spl14_207
| ~ spl14_264 ),
inference(avatar_contradiction_clause,[],[f2509]) ).
fof(f2511,plain,
( e11 = e12
| ~ spl14_224
| ~ spl14_235 ),
inference(forward_demodulation,[],[f1713,f1657]) ).
fof(f2512,plain,
( $false
| ~ spl14_224
| ~ spl14_235 ),
inference(forward_subsumption_resolution,[],[f2511,f215]) ).
fof(f2513,plain,
( ~ spl14_224
| ~ spl14_235 ),
inference(avatar_contradiction_clause,[],[f2512]) ).
fof(f2549,plain,
( e11 = e12
| ~ spl14_220
| ~ spl14_233 ),
inference(forward_demodulation,[],[f1702,f1638]) ).
fof(f2550,plain,
( $false
| ~ spl14_220
| ~ spl14_233 ),
inference(forward_subsumption_resolution,[],[f2549,f215]) ).
fof(f2551,plain,
( ~ spl14_220
| ~ spl14_233 ),
inference(avatar_contradiction_clause,[],[f2550]) ).
fof(f2553,plain,
( e12 = e13
| ~ spl14_219
| ~ spl14_221 ),
inference(superposition,[],[f1634,f1643]) ).
fof(f2558,plain,
( $false
| ~ spl14_219
| ~ spl14_221 ),
inference(forward_subsumption_resolution,[],[f2553,f213]) ).
fof(f2559,plain,
( ~ spl14_219
| ~ spl14_221 ),
inference(avatar_contradiction_clause,[],[f2558]) ).
fof(f2573,plain,
( e10 = e11
| ~ spl14_202
| ~ spl14_257 ),
inference(superposition,[],[f1867,f1556]) ).
fof(f2579,plain,
( $false
| ~ spl14_202
| ~ spl14_257 ),
inference(forward_subsumption_resolution,[],[f2573,f218]) ).
fof(f2580,plain,
( ~ spl14_202
| ~ spl14_257 ),
inference(avatar_contradiction_clause,[],[f2579]) ).
fof(f2581,plain,
( e10 = e12
| ~ spl14_198
| ~ spl14_256 ),
inference(superposition,[],[f1863,f1538]) ).
fof(f2586,plain,
( $false
| ~ spl14_198
| ~ spl14_256 ),
inference(forward_subsumption_resolution,[],[f2581,f217]) ).
fof(f2587,plain,
( ~ spl14_198
| ~ spl14_256 ),
inference(avatar_contradiction_clause,[],[f2586]) ).
fof(f2591,plain,
( e11 = e12
| ~ spl14_215
| ~ spl14_259 ),
inference(superposition,[],[f1876,f1615]) ).
fof(f2594,plain,
( h1(e11) != op2(e20,h1(e11))
| ~ spl14_5
| spl14_42
| ~ spl14_259 ),
inference(superposition,[],[f1968,f1876]) ).
fof(f2597,plain,
( $false
| ~ spl14_215
| ~ spl14_259 ),
inference(forward_subsumption_resolution,[],[f2591,f215]) ).
fof(f2598,plain,
( ~ spl14_215
| ~ spl14_259 ),
inference(avatar_contradiction_clause,[],[f2597]) ).
fof(f2617,plain,
( e12 = e13
| ~ spl14_235
| ~ spl14_269 ),
inference(forward_demodulation,[],[f1936,f1713]) ).
fof(f2618,plain,
( $false
| ~ spl14_235
| ~ spl14_269 ),
inference(forward_subsumption_resolution,[],[f2617,f213]) ).
fof(f2619,plain,
( ~ spl14_235
| ~ spl14_269 ),
inference(avatar_contradiction_clause,[],[f2618]) ).
fof(f2621,plain,
( e11 = e13
| ~ spl14_220
| ~ spl14_266 ),
inference(forward_demodulation,[],[f1916,f1638]) ).
fof(f2625,plain,
( $false
| ~ spl14_220
| ~ spl14_266 ),
inference(forward_subsumption_resolution,[],[f2621,f214]) ).
fof(f2626,plain,
( ~ spl14_220
| ~ spl14_266 ),
inference(avatar_contradiction_clause,[],[f2625]) ).
fof(f2641,plain,
( e12 = e13
| ~ spl14_192
| ~ spl14_194 ),
inference(superposition,[],[f1511,f1520]) ).
fof(f2651,plain,
( $false
| ~ spl14_192
| ~ spl14_194 ),
inference(forward_subsumption_resolution,[],[f2641,f213]) ).
fof(f2652,plain,
( ~ spl14_192
| ~ spl14_194 ),
inference(avatar_contradiction_clause,[],[f2651]) ).
fof(f2665,plain,
( e11 = e13
| ~ spl14_226
| ~ spl14_238 ),
inference(forward_demodulation,[],[f1729,f1667]) ).
fof(f2666,plain,
( $false
| ~ spl14_226
| ~ spl14_238 ),
inference(forward_subsumption_resolution,[],[f2665,f214]) ).
fof(f2667,plain,
( ~ spl14_226
| ~ spl14_238 ),
inference(avatar_contradiction_clause,[],[f2666]) ).
fof(f2676,plain,
( e10 = e12
| ~ spl14_205
| ~ spl14_235 ),
inference(superposition,[],[f1569,f1713]) ).
fof(f2681,plain,
( $false
| ~ spl14_205
| ~ spl14_235 ),
inference(forward_subsumption_resolution,[],[f2676,f217]) ).
fof(f2682,plain,
( ~ spl14_205
| ~ spl14_235 ),
inference(avatar_contradiction_clause,[],[f2681]) ).
fof(f2756,plain,
( e23 = h1(e13)
| ~ spl14_143 ),
inference(forward_demodulation,[],[f351,f1268]) ).
fof(f2757,plain,
( spl14_64
| ~ spl14_143 ),
inference(avatar_split_clause,[],[f2756,f1266,f892]) ).
fof(f2760,plain,
( e20 = h3(e13)
| ~ spl14_152 ),
inference(forward_demodulation,[],[f359,f1308]) ).
fof(f2789,plain,
( e13 != op1(e13,e11)
| ~ spl14_238 ),
inference(forward_demodulation,[],[f119,f1729]) ).
fof(f2798,plain,
( e10 != op1(e12,e11)
| ~ spl14_203 ),
inference(forward_demodulation,[],[f125,f1560]) ).
fof(f2812,plain,
( e10 != op1(e10,e11)
| ~ spl14_193 ),
inference(forward_demodulation,[],[f136,f1515]) ).
fof(f2825,plain,
( e13 != op1(e12,e12)
| ~ spl14_238 ),
inference(forward_demodulation,[],[f147,f1729]) ).
fof(f2827,plain,
( e13 != op1(e11,e12)
| ~ spl14_238 ),
inference(forward_demodulation,[],[f148,f1729]) ).
fof(f2888,plain,
( e23 != op2(e22,e22)
| ~ spl14_187 ),
inference(forward_demodulation,[],[f195,f1477]) ).
fof(f2889,plain,
( ~ spl14_185
| ~ spl14_187 ),
inference(avatar_split_clause,[],[f2888,f1475,f1464]) ).
fof(f2897,plain,
( e21 != op2(e20,e22)
| ~ spl14_167 ),
inference(forward_demodulation,[],[f200,f1377]) ).
fof(f2905,plain,
( e22 != op2(e20,e21)
| ~ spl14_168 ),
inference(forward_demodulation,[],[f206,f1382]) ).
fof(f2914,plain,
( e12 = op1(e13,e10)
| ~ spl14_194 ),
inference(forward_demodulation,[],[f346,f1520]) ).
fof(f2917,plain,
( e13 != op1(e10,e12)
| ~ spl14_194 ),
inference(forward_demodulation,[],[f139,f1520]) ).
fof(f2918,plain,
( e13 != op1(e10,e11)
| ~ spl14_194 ),
inference(forward_demodulation,[],[f140,f1520]) ).
fof(f2924,plain,
( e10 != op1(e13,e13)
| ~ spl14_193 ),
inference(forward_demodulation,[],[f144,f1515]) ).
fof(f2928,plain,
( ~ spl14_234
| ~ spl14_238 ),
inference(avatar_split_clause,[],[f2827,f1727,f1705]) ).
fof(f2929,plain,
( spl14_210
| ~ spl14_194 ),
inference(avatar_split_clause,[],[f2914,f1518,f1590]) ).
fof(f2931,plain,
( e12 != op1(e13,e10)
| ~ spl14_204 ),
inference(forward_demodulation,[],[f159,f1565]) ).
fof(f2932,plain,
( e13 != op1(e13,e10)
| ~ spl14_194 ),
inference(forward_demodulation,[],[f162,f1520]) ).
fof(f2934,plain,
( ~ spl14_217
| ~ spl14_194 ),
inference(avatar_split_clause,[],[f2918,f1518,f1622]) ).
fof(f2937,plain,
( ~ spl14_211
| ~ spl14_193 ),
inference(avatar_split_clause,[],[f2924,f1514,f1595]) ).
fof(f2938,plain,
( ~ spl14_210
| ~ spl14_204 ),
inference(avatar_split_clause,[],[f2931,f1563,f1590]) ).
fof(f2939,plain,
( ~ spl14_212
| ~ spl14_194 ),
inference(avatar_split_clause,[],[f2932,f1518,f1599]) ).
fof(f2940,plain,
( ~ spl14_229
| ~ spl14_238 ),
inference(avatar_split_clause,[],[f2789,f1727,f1679]) ).
fof(f2944,plain,
( ~ spl14_236
| ~ spl14_238 ),
inference(avatar_split_clause,[],[f2825,f1727,f1716]) ).
fof(f2987,plain,
( e10 = e12
| ~ spl14_210
| ~ spl14_258 ),
inference(superposition,[],[f1871,f1592]) ).
fof(f2992,plain,
( $false
| ~ spl14_210
| ~ spl14_258 ),
inference(forward_subsumption_resolution,[],[f2987,f217]) ).
fof(f2993,plain,
( ~ spl14_210
| ~ spl14_258 ),
inference(avatar_contradiction_clause,[],[f2992]) ).
fof(f3013,plain,
( e11 = e13
| ~ spl14_229
| ~ spl14_264 ),
inference(superposition,[],[f1905,f1681]) ).
fof(f3019,plain,
( $false
| ~ spl14_229
| ~ spl14_264 ),
inference(forward_subsumption_resolution,[],[f3013,f214]) ).
fof(f3020,plain,
( ~ spl14_229
| ~ spl14_264 ),
inference(avatar_contradiction_clause,[],[f3019]) ).
fof(f3041,plain,
( e13 != op1(e12,e11)
| ~ spl14_236 ),
inference(forward_demodulation,[],[f125,f1718]) ).
fof(f3046,plain,
( e12 != op1(e11,e11)
| ~ spl14_265 ),
inference(forward_demodulation,[],[f131,f1910]) ).
fof(f3052,plain,
( e10 != op1(e12,e12)
| ~ spl14_209 ),
inference(forward_demodulation,[],[f147,f1587]) ).
fof(f3055,plain,
( e10 != op1(e10,e12)
| ~ spl14_209 ),
inference(forward_demodulation,[],[f150,f1587]) ).
fof(f3057,plain,
( e12 != op1(e10,e12)
| ~ spl14_265 ),
inference(forward_demodulation,[],[f152,f1910]) ).
fof(f3061,plain,
( e13 != op1(e11,e11)
| ~ spl14_229 ),
inference(forward_demodulation,[],[f154,f1681]) ).
fof(f3071,plain,
( e22 = op2(e23,e20)
| ~ spl14_143 ),
inference(forward_demodulation,[],[f349,f1268]) ).
fof(f3078,plain,
( ~ spl14_175
| ~ spl14_25
| ~ spl14_109
| spl14_157 ),
inference(avatar_split_clause,[],[f2089,f1329,f1095,f711,f1414]) ).
fof(f3082,plain,
( e20 != op2(e23,e22)
| ~ spl14_152 ),
inference(forward_demodulation,[],[f195,f1308]) ).
fof(f3083,plain,
( e21 != op2(e23,e22)
| ~ spl14_167 ),
inference(forward_demodulation,[],[f196,f1377]) ).
fof(f3084,plain,
( e22 != op2(e23,e22)
| ~ spl14_244 ),
inference(forward_demodulation,[],[f198,f1770]) ).
fof(f3089,plain,
( e20 != op2(e23,e23)
| ~ spl14_142 ),
inference(forward_demodulation,[],[f192,f1263]) ).
fof(f3090,plain,
( spl14_159
| ~ spl14_143 ),
inference(avatar_split_clause,[],[f3071,f1266,f1338]) ).
fof(f3091,plain,
( e22 != op2(e23,e20)
| ~ spl14_153 ),
inference(forward_demodulation,[],[f207,f1313]) ).
fof(f3097,plain,
( ~ spl14_158
| ~ spl14_152 ),
inference(avatar_split_clause,[],[f3082,f1307,f1334]) ).
fof(f3098,plain,
( ~ spl14_175
| ~ spl14_167 ),
inference(avatar_split_clause,[],[f3083,f1376,f1414]) ).
fof(f3099,plain,
( ~ spl14_252
| ~ spl14_244 ),
inference(avatar_split_clause,[],[f3084,f1768,f1817]) ).
fof(f3104,plain,
( ~ spl14_160
| ~ spl14_142 ),
inference(avatar_split_clause,[],[f3089,f1262,f1343]) ).
fof(f3105,plain,
( ~ spl14_159
| ~ spl14_153 ),
inference(avatar_split_clause,[],[f3091,f1311,f1338]) ).
fof(f3112,plain,
( e20 != op2(e22,e23)
| ~ spl14_142 ),
inference(forward_demodulation,[],[f193,f1263]) ).
fof(f3226,plain,
( e21 != op2(e22,e20)
| ~ spl14_171 ),
inference(forward_demodulation,[],[f175,f1396]) ).
fof(f3229,plain,
( e22 != op2(e21,e21)
| ~ spl14_182 ),
inference(forward_demodulation,[],[f178,f1450]) ).
fof(f3233,plain,
( e20 != op2(e21,e20)
| ~ spl14_144 ),
inference(forward_demodulation,[],[f182,f1272]) ).
fof(f3245,plain,
( e23 != op2(e21,e21)
| ~ spl14_178 ),
inference(forward_demodulation,[],[f202,f1429]) ).
fof(f3250,plain,
( op2(e23,e20) = h1(e12)
| ~ spl14_143 ),
inference(forward_demodulation,[],[f352,f1268]) ).
fof(f3251,plain,
( e22 = h1(e12)
| ~ spl14_143
| ~ spl14_159 ),
inference(forward_demodulation,[],[f3250,f1340]) ).
fof(f3252,plain,
( spl14_59
| ~ spl14_143
| ~ spl14_159 ),
inference(avatar_split_clause,[],[f3251,f1338,f1266,f861]) ).
fof(f3266,plain,
( e11 = op1(op1(e13,e10),e10)
| ~ spl14_194 ),
inference(forward_demodulation,[],[f347,f1520]) ).
fof(f3267,plain,
( e11 = op1(e12,e10)
| ~ spl14_194
| ~ spl14_210 ),
inference(forward_demodulation,[],[f3266,f1592]) ).
fof(f3273,plain,
( ~ spl14_225
| ~ spl14_236 ),
inference(avatar_split_clause,[],[f3041,f1716,f1660]) ).
fof(f3276,plain,
( ~ spl14_260
| ~ spl14_265 ),
inference(avatar_split_clause,[],[f3057,f1908,f1880]) ).
fof(f3277,plain,
( spl14_202
| ~ spl14_194
| ~ spl14_210 ),
inference(avatar_split_clause,[],[f3267,f1590,f1518,f1554]) ).
fof(f3278,plain,
( ~ spl14_219
| ~ spl14_265 ),
inference(avatar_split_clause,[],[f3046,f1908,f1632]) ).
fof(f3279,plain,
( ~ spl14_221
| ~ spl14_229 ),
inference(avatar_split_clause,[],[f3061,f1679,f1641]) ).
fof(f3313,plain,
( e10 != op1(e10,e11)
| ~ spl14_201 ),
inference(forward_demodulation,[],[f157,f1551]) ).
fof(f3316,plain,
( e21 = op2(op2(e23,e20),e20)
| ~ spl14_143 ),
inference(forward_demodulation,[],[f350,f1268]) ).
fof(f3317,plain,
( e21 = op2(e22,e20)
| ~ spl14_143
| ~ spl14_159 ),
inference(forward_demodulation,[],[f3316,f1340]) ).
fof(f3322,plain,
( e20 = e21
| ~ spl14_143
| ~ spl14_159
| ~ spl14_241 ),
inference(forward_demodulation,[],[f3317,f1755]) ).
fof(f3325,plain,
( $false
| ~ spl14_143
| ~ spl14_159
| ~ spl14_241 ),
inference(forward_subsumption_resolution,[],[f3322,f224]) ).
fof(f3326,plain,
( ~ spl14_143
| ~ spl14_159
| ~ spl14_241 ),
inference(avatar_contradiction_clause,[],[f3325]) ).
fof(f3328,plain,
( e20 = e22
| ~ spl14_159
| ~ spl14_242 ),
inference(forward_demodulation,[],[f1759,f1340]) ).
fof(f3330,plain,
( e21 != op2(e22,e20)
| ~ spl14_145 ),
inference(forward_demodulation,[],[f209,f1277]) ).
fof(f3331,plain,
( ~ spl14_151
| ~ spl14_171 ),
inference(avatar_split_clause,[],[f3226,f1395,f1302]) ).
fof(f3332,plain,
( spl14_151
| ~ spl14_143
| ~ spl14_159 ),
inference(avatar_split_clause,[],[f3317,f1338,f1266,f1302]) ).
fof(f3336,plain,
( $false
| spl14_25
| ~ spl14_109
| ~ spl14_159
| ~ spl14_242 ),
inference(forward_subsumption_resolution,[],[f3328,f2111]) ).
fof(f3337,plain,
( spl14_25
| ~ spl14_109
| ~ spl14_159
| ~ spl14_242 ),
inference(avatar_contradiction_clause,[],[f3336]) ).
fof(f3338,plain,
( ~ spl14_151
| ~ spl14_145 ),
inference(avatar_split_clause,[],[f3330,f1275,f1302]) ).
fof(f3340,plain,
( e21 = e22
| ~ spl14_163
| ~ spl14_244 ),
inference(forward_demodulation,[],[f1358,f1770]) ).
fof(f3344,plain,
( ~ spl14_240
| ~ spl14_144 ),
inference(avatar_split_clause,[],[f3233,f1271,f1749]) ).
fof(f3352,plain,
( e23 != op2(e22,e22)
| ~ spl14_183 ),
inference(forward_demodulation,[],[f197,f1455]) ).
fof(f3356,plain,
( $false
| ~ spl14_163
| ~ spl14_244 ),
inference(forward_subsumption_resolution,[],[f3340,f221]) ).
fof(f3357,plain,
( ~ spl14_163
| ~ spl14_244 ),
inference(avatar_contradiction_clause,[],[f3356]) ).
fof(f3363,plain,
( ~ spl14_185
| ~ spl14_183 ),
inference(avatar_split_clause,[],[f3352,f1453,f1464]) ).
fof(f3364,plain,
( ~ spl14_154
| ~ spl14_142 ),
inference(avatar_split_clause,[],[f3112,f1262,f1316]) ).
fof(f3367,plain,
( e23 != op2(e20,e22)
| ~ spl14_143 ),
inference(forward_demodulation,[],[f187,f1268]) ).
fof(f3368,plain,
( e20 != op2(e20,e22)
| ~ spl14_158 ),
inference(forward_demodulation,[],[f198,f1335]) ).
fof(f3371,plain,
( ~ spl14_170
| ~ spl14_178 ),
inference(avatar_split_clause,[],[f3245,f1427,f1389]) ).
fof(f3375,plain,
( ~ spl14_181
| ~ spl14_143 ),
inference(avatar_split_clause,[],[f3367,f1266,f1442]) ).
fof(f3376,plain,
( ~ spl14_140
| ~ spl14_158 ),
inference(avatar_split_clause,[],[f3368,f1334,f1253]) ).
fof(f3382,plain,
( ~ spl14_163
| ~ spl14_167 ),
inference(avatar_split_clause,[],[f2897,f1376,f1357]) ).
fof(f3385,plain,
( ~ spl14_164
| ~ spl14_168 ),
inference(avatar_split_clause,[],[f2905,f1380,f1361]) ).
fof(f3393,plain,
( e21 != op2(e21,e23)
| ~ spl14_177 ),
inference(forward_demodulation,[],[f190,f1424]) ).
fof(f3400,plain,
( ~ spl14_169
| ~ spl14_177 ),
inference(avatar_split_clause,[],[f3393,f1423,f1385]) ).
fof(f3502,plain,
( e23 = h3(e13)
| ~ spl14_185 ),
inference(forward_demodulation,[],[f359,f1466]) ).
fof(f3509,plain,
( spl14_112
| ~ spl14_185 ),
inference(avatar_split_clause,[],[f3502,f1464,f1116]) ).
fof(f3540,plain,
( h1(e11) = op2(op2(e23,e20),e20)
| ~ spl14_143 ),
inference(forward_demodulation,[],[f353,f1268]) ).
fof(f3541,plain,
( op2(e22,e20) = h1(e11)
| ~ spl14_143
| ~ spl14_159 ),
inference(forward_demodulation,[],[f3540,f1340]) ).
fof(f3542,plain,
( e21 = h1(e11)
| ~ spl14_143
| ~ spl14_151
| ~ spl14_159 ),
inference(forward_demodulation,[],[f3541,f1304]) ).
fof(f3543,plain,
( spl14_9
| ~ spl14_143
| ~ spl14_151
| ~ spl14_159 ),
inference(avatar_split_clause,[],[f3542,f1338,f1302,f1266,f634]) ).
fof(f3544,plain,
( e21 != op2(e20,e21)
| ~ spl14_5
| ~ spl14_9
| spl14_42
| ~ spl14_259 ),
inference(superposition,[],[f2594,f635]) ).
fof(f3545,plain,
( $false
| ~ spl14_5
| ~ spl14_9
| spl14_42
| ~ spl14_243
| ~ spl14_259 ),
inference(forward_subsumption_resolution,[],[f3544,f1764]) ).
fof(f3546,plain,
( ~ spl14_5
| ~ spl14_9
| spl14_42
| ~ spl14_243
| ~ spl14_259 ),
inference(avatar_contradiction_clause,[],[f3545]) ).
fof(f3547,plain,
( op2(e20,e20) != h1(op1(e10,e10))
| ~ spl14_5
| spl14_41 ),
inference(forward_demodulation,[],[f790,f616]) ).
fof(f3549,plain,
( op2(e20,e20) != h1(e13)
| ~ spl14_5
| spl14_41
| ~ spl14_194 ),
inference(forward_demodulation,[],[f3547,f1520]) ).
fof(f3551,plain,
( op2(e20,e20) != e23
| ~ spl14_5
| spl14_41
| ~ spl14_64
| ~ spl14_194 ),
inference(forward_demodulation,[],[f3549,f893]) ).
fof(f3553,plain,
( $false
| ~ spl14_5
| spl14_41
| ~ spl14_64
| ~ spl14_143
| ~ spl14_194 ),
inference(forward_subsumption_resolution,[],[f3551,f1268]) ).
fof(f3554,plain,
( ~ spl14_5
| spl14_41
| ~ spl14_64
| ~ spl14_143
| ~ spl14_194 ),
inference(avatar_contradiction_clause,[],[f3553]) ).
fof(f3557,plain,
( h1(op1(e10,e12)) != op2(h1(e10),e22)
| spl14_43
| ~ spl14_59 ),
inference(forward_demodulation,[],[f798,f862]) ).
fof(f3559,plain,
( op2(e20,e22) != h1(op1(e10,e12))
| ~ spl14_5
| spl14_43
| ~ spl14_59 ),
inference(forward_demodulation,[],[f3557,f616]) ).
fof(f3561,plain,
( op2(e20,e22) != h1(e12)
| ~ spl14_5
| spl14_43
| ~ spl14_59
| ~ spl14_260 ),
inference(forward_demodulation,[],[f3559,f1882]) ).
fof(f3562,plain,
( e22 != op2(e20,e22)
| ~ spl14_5
| spl14_43
| ~ spl14_59
| ~ spl14_260 ),
inference(forward_demodulation,[],[f3561,f862]) ).
fof(f3563,plain,
( $false
| ~ spl14_5
| spl14_43
| ~ spl14_59
| ~ spl14_244
| ~ spl14_260 ),
inference(forward_subsumption_resolution,[],[f3562,f1770]) ).
fof(f3564,plain,
( ~ spl14_5
| spl14_43
| ~ spl14_59
| ~ spl14_244
| ~ spl14_260 ),
inference(avatar_contradiction_clause,[],[f3563]) ).
fof(f3566,plain,
( h1(op1(e10,e13)) != op2(h1(e10),e23)
| spl14_44
| ~ spl14_64 ),
inference(forward_demodulation,[],[f802,f893]) ).
fof(f3568,plain,
( op2(e20,e23) != h1(op1(e10,e13))
| ~ spl14_5
| spl14_44
| ~ spl14_64 ),
inference(forward_demodulation,[],[f3566,f616]) ).
fof(f3570,plain,
( op2(e20,e23) != h1(e10)
| ~ spl14_5
| spl14_44
| ~ spl14_64
| ~ spl14_193 ),
inference(forward_demodulation,[],[f3568,f1515]) ).
fof(f3572,plain,
( e20 != op2(e20,e23)
| ~ spl14_5
| spl14_44
| ~ spl14_64
| ~ spl14_193 ),
inference(forward_demodulation,[],[f3570,f616]) ).
fof(f3576,plain,
( h1(op1(e11,e10)) != op2(h1(e11),e20)
| ~ spl14_5
| spl14_45 ),
inference(forward_demodulation,[],[f806,f616]) ).
fof(f3578,plain,
( op2(e21,e20) != h1(op1(e11,e10))
| ~ spl14_5
| ~ spl14_9
| spl14_45 ),
inference(forward_demodulation,[],[f3576,f635]) ).
fof(f3580,plain,
( op2(e21,e20) != h1(e10)
| ~ spl14_5
| ~ spl14_9
| spl14_45
| ~ spl14_256 ),
inference(forward_demodulation,[],[f3578,f1863]) ).
fof(f3582,plain,
( e20 != op2(e21,e20)
| ~ spl14_5
| ~ spl14_9
| spl14_45
| ~ spl14_256 ),
inference(forward_demodulation,[],[f3580,f616]) ).
fof(f3583,plain,
( $false
| ~ spl14_5
| ~ spl14_9
| spl14_45
| ~ spl14_240
| ~ spl14_256 ),
inference(forward_subsumption_resolution,[],[f3582,f1751]) ).
fof(f3584,plain,
( ~ spl14_5
| ~ spl14_9
| spl14_45
| ~ spl14_240
| ~ spl14_256 ),
inference(avatar_contradiction_clause,[],[f3583]) ).
fof(f3586,plain,
( op2(e21,e21) != h1(op1(e11,e11))
| ~ spl14_9
| spl14_46 ),
inference(forward_demodulation,[],[f810,f635]) ).
fof(f3588,plain,
( op2(e21,e21) != h1(e12)
| ~ spl14_9
| spl14_46
| ~ spl14_219 ),
inference(forward_demodulation,[],[f3586,f1634]) ).
fof(f3590,plain,
( e22 != op2(e21,e21)
| ~ spl14_9
| spl14_46
| ~ spl14_59
| ~ spl14_219 ),
inference(forward_demodulation,[],[f3588,f862]) ).
fof(f3592,plain,
( $false
| ~ spl14_9
| spl14_46
| ~ spl14_59
| ~ spl14_168
| ~ spl14_219 ),
inference(forward_subsumption_resolution,[],[f3590,f1382]) ).
fof(f3593,plain,
( ~ spl14_9
| spl14_46
| ~ spl14_59
| ~ spl14_168
| ~ spl14_219 ),
inference(avatar_contradiction_clause,[],[f3592]) ).
fof(f3595,plain,
( h1(op1(e11,e12)) != op2(h1(e11),e22)
| spl14_47
| ~ spl14_59 ),
inference(forward_demodulation,[],[f814,f862]) ).
fof(f3597,plain,
( op2(e21,e22) != h1(op1(e11,e12))
| ~ spl14_9
| spl14_47
| ~ spl14_59 ),
inference(forward_demodulation,[],[f3595,f635]) ).
fof(f3599,plain,
( op2(e21,e22) != h1(e11)
| ~ spl14_9
| spl14_47
| ~ spl14_59
| ~ spl14_218 ),
inference(forward_demodulation,[],[f3597,f1629]) ).
fof(f3600,plain,
( e21 != op2(e21,e22)
| ~ spl14_9
| spl14_47
| ~ spl14_59
| ~ spl14_218 ),
inference(forward_demodulation,[],[f3599,f635]) ).
fof(f3601,plain,
( $false
| ~ spl14_9
| spl14_47
| ~ spl14_59
| ~ spl14_167
| ~ spl14_218 ),
inference(forward_subsumption_resolution,[],[f3600,f1377]) ).
fof(f3602,plain,
( ~ spl14_9
| spl14_47
| ~ spl14_59
| ~ spl14_167
| ~ spl14_218 ),
inference(avatar_contradiction_clause,[],[f3601]) ).
fof(f3604,plain,
( h1(op1(e11,e13)) != op2(h1(e11),e23)
| spl14_48
| ~ spl14_64 ),
inference(forward_demodulation,[],[f818,f893]) ).
fof(f3606,plain,
( op2(e21,e23) != h1(op1(e11,e13))
| ~ spl14_9
| spl14_48
| ~ spl14_64 ),
inference(forward_demodulation,[],[f3604,f635]) ).
fof(f3608,plain,
( op2(e21,e23) != h1(e13)
| ~ spl14_9
| spl14_48
| ~ spl14_64
| ~ spl14_266 ),
inference(forward_demodulation,[],[f3606,f1916]) ).
fof(f3610,plain,
( e23 != op2(e21,e23)
| ~ spl14_9
| spl14_48
| ~ spl14_64
| ~ spl14_266 ),
inference(forward_demodulation,[],[f3608,f893]) ).
fof(f3611,plain,
( $false
| ~ spl14_9
| spl14_48
| ~ spl14_64
| ~ spl14_250
| ~ spl14_266 ),
inference(forward_subsumption_resolution,[],[f3610,f1804]) ).
fof(f3612,plain,
( ~ spl14_9
| spl14_48
| ~ spl14_64
| ~ spl14_250
| ~ spl14_266 ),
inference(avatar_contradiction_clause,[],[f3611]) ).
fof(f3614,plain,
( h1(op1(e12,e10)) != op2(h1(e12),e20)
| ~ spl14_5
| spl14_49 ),
inference(forward_demodulation,[],[f822,f616]) ).
fof(f3616,plain,
( op2(e22,e20) != h1(op1(e12,e10))
| ~ spl14_5
| spl14_49
| ~ spl14_59 ),
inference(forward_demodulation,[],[f3614,f862]) ).
fof(f3618,plain,
( op2(e22,e20) != h1(e11)
| ~ spl14_5
| spl14_49
| ~ spl14_59
| ~ spl14_202 ),
inference(forward_demodulation,[],[f3616,f1556]) ).
fof(f3620,plain,
( e21 != op2(e22,e20)
| ~ spl14_5
| ~ spl14_9
| spl14_49
| ~ spl14_59
| ~ spl14_202 ),
inference(forward_demodulation,[],[f3618,f635]) ).
fof(f3621,plain,
( $false
| ~ spl14_5
| ~ spl14_9
| spl14_49
| ~ spl14_59
| ~ spl14_151
| ~ spl14_202 ),
inference(forward_subsumption_resolution,[],[f3620,f1304]) ).
fof(f3622,plain,
( ~ spl14_5
| ~ spl14_9
| spl14_49
| ~ spl14_59
| ~ spl14_151
| ~ spl14_202 ),
inference(avatar_contradiction_clause,[],[f3621]) ).
fof(f3624,plain,
( h1(op1(e12,e11)) != op2(h1(e12),e21)
| ~ spl14_9
| spl14_50 ),
inference(forward_demodulation,[],[f826,f635]) ).
fof(f3626,plain,
( op2(e22,e21) != h1(op1(e12,e11))
| ~ spl14_9
| spl14_50
| ~ spl14_59 ),
inference(forward_demodulation,[],[f3624,f862]) ).
fof(f3628,plain,
( op2(e22,e21) != h1(e10)
| ~ spl14_9
| spl14_50
| ~ spl14_59
| ~ spl14_201 ),
inference(forward_demodulation,[],[f3626,f1551]) ).
fof(f3630,plain,
( e20 != op2(e22,e21)
| ~ spl14_5
| ~ spl14_9
| spl14_50
| ~ spl14_59
| ~ spl14_201 ),
inference(forward_demodulation,[],[f3628,f616]) ).
fof(f3631,plain,
( $false
| ~ spl14_5
| ~ spl14_9
| spl14_50
| ~ spl14_59
| ~ spl14_150
| ~ spl14_201 ),
inference(forward_subsumption_resolution,[],[f3630,f1299]) ).
fof(f3632,plain,
( ~ spl14_5
| ~ spl14_9
| spl14_50
| ~ spl14_59
| ~ spl14_150
| ~ spl14_201 ),
inference(avatar_contradiction_clause,[],[f3631]) ).
fof(f3634,plain,
( op2(e22,e22) != h1(op1(e12,e12))
| spl14_51
| ~ spl14_59 ),
inference(forward_demodulation,[],[f830,f862]) ).
fof(f3636,plain,
( op2(e22,e22) != h1(e13)
| spl14_51
| ~ spl14_59
| ~ spl14_236 ),
inference(forward_demodulation,[],[f3634,f1718]) ).
fof(f3638,plain,
( e23 != op2(e22,e22)
| spl14_51
| ~ spl14_59
| ~ spl14_64
| ~ spl14_236 ),
inference(forward_demodulation,[],[f3636,f893]) ).
fof(f3640,plain,
( $false
| spl14_51
| ~ spl14_59
| ~ spl14_64
| ~ spl14_185
| ~ spl14_236 ),
inference(forward_subsumption_resolution,[],[f3638,f1466]) ).
fof(f3641,plain,
( spl14_51
| ~ spl14_59
| ~ spl14_64
| ~ spl14_185
| ~ spl14_236 ),
inference(avatar_contradiction_clause,[],[f3640]) ).
fof(f3643,plain,
( h1(op1(e12,e13)) != op2(h1(e12),e23)
| spl14_52
| ~ spl14_64 ),
inference(forward_demodulation,[],[f834,f893]) ).
fof(f3645,plain,
( op2(e22,e23) != h1(op1(e12,e13))
| spl14_52
| ~ spl14_59
| ~ spl14_64 ),
inference(forward_demodulation,[],[f3643,f862]) ).
fof(f3647,plain,
( op2(e22,e23) != h1(e12)
| spl14_52
| ~ spl14_59
| ~ spl14_64
| ~ spl14_235 ),
inference(forward_demodulation,[],[f3645,f1713]) ).
fof(f3648,plain,
( e22 != op2(e22,e23)
| spl14_52
| ~ spl14_59
| ~ spl14_64
| ~ spl14_235 ),
inference(forward_demodulation,[],[f3647,f862]) ).
fof(f3649,plain,
( $false
| spl14_52
| ~ spl14_59
| ~ spl14_64
| ~ spl14_184
| ~ spl14_235 ),
inference(forward_subsumption_resolution,[],[f3648,f1461]) ).
fof(f3650,plain,
( spl14_52
| ~ spl14_59
| ~ spl14_64
| ~ spl14_184
| ~ spl14_235 ),
inference(avatar_contradiction_clause,[],[f3649]) ).
fof(f3652,plain,
( h1(op1(e13,e10)) != op2(h1(e13),e20)
| ~ spl14_5
| spl14_53 ),
inference(forward_demodulation,[],[f838,f616]) ).
fof(f3654,plain,
( op2(e23,e20) != h1(op1(e13,e10))
| ~ spl14_5
| spl14_53
| ~ spl14_64 ),
inference(forward_demodulation,[],[f3652,f893]) ).
fof(f3656,plain,
( op2(e23,e20) != h1(e12)
| ~ spl14_5
| spl14_53
| ~ spl14_64
| ~ spl14_210 ),
inference(forward_demodulation,[],[f3654,f1592]) ).
fof(f3658,plain,
( e22 != op2(e23,e20)
| ~ spl14_5
| spl14_53
| ~ spl14_59
| ~ spl14_64
| ~ spl14_210 ),
inference(forward_demodulation,[],[f3656,f862]) ).
fof(f3659,plain,
( $false
| ~ spl14_5
| spl14_53
| ~ spl14_59
| ~ spl14_64
| ~ spl14_159
| ~ spl14_210 ),
inference(forward_subsumption_resolution,[],[f3658,f1340]) ).
fof(f3660,plain,
( ~ spl14_5
| spl14_53
| ~ spl14_59
| ~ spl14_64
| ~ spl14_159
| ~ spl14_210 ),
inference(avatar_contradiction_clause,[],[f3659]) ).
fof(f3662,plain,
( h1(op1(e13,e11)) != op2(h1(e13),e21)
| ~ spl14_9
| spl14_54 ),
inference(forward_demodulation,[],[f842,f635]) ).
fof(f3664,plain,
( op2(e23,e21) != h1(op1(e13,e11))
| ~ spl14_9
| spl14_54
| ~ spl14_64 ),
inference(forward_demodulation,[],[f3662,f893]) ).
fof(f3666,plain,
( op2(e23,e21) != h1(e13)
| ~ spl14_9
| spl14_54
| ~ spl14_64
| ~ spl14_229 ),
inference(forward_demodulation,[],[f3664,f1681]) ).
fof(f3668,plain,
( e23 != op2(e23,e21)
| ~ spl14_9
| spl14_54
| ~ spl14_64
| ~ spl14_229 ),
inference(forward_demodulation,[],[f3666,f893]) ).
fof(f3669,plain,
( $false
| ~ spl14_9
| spl14_54
| ~ spl14_64
| ~ spl14_178
| ~ spl14_229 ),
inference(forward_subsumption_resolution,[],[f3668,f1429]) ).
fof(f3670,plain,
( ~ spl14_9
| spl14_54
| ~ spl14_64
| ~ spl14_178
| ~ spl14_229 ),
inference(avatar_contradiction_clause,[],[f3669]) ).
fof(f3672,plain,
( h1(op1(e13,e12)) != op2(h1(e13),e22)
| spl14_55
| ~ spl14_59 ),
inference(forward_demodulation,[],[f846,f862]) ).
fof(f3674,plain,
( op2(e23,e22) != h1(op1(e13,e12))
| spl14_55
| ~ spl14_59
| ~ spl14_64 ),
inference(forward_demodulation,[],[f3672,f893]) ).
fof(f3676,plain,
( op2(e23,e22) != h1(e10)
| spl14_55
| ~ spl14_59
| ~ spl14_64
| ~ spl14_209 ),
inference(forward_demodulation,[],[f3674,f1587]) ).
fof(f3678,plain,
( e20 != op2(e23,e22)
| ~ spl14_5
| spl14_55
| ~ spl14_59
| ~ spl14_64
| ~ spl14_209 ),
inference(forward_demodulation,[],[f3676,f616]) ).
fof(f3679,plain,
( $false
| ~ spl14_5
| spl14_55
| ~ spl14_59
| ~ spl14_64
| ~ spl14_158
| ~ spl14_209 ),
inference(forward_subsumption_resolution,[],[f3678,f1335]) ).
fof(f3680,plain,
( ~ spl14_5
| spl14_55
| ~ spl14_59
| ~ spl14_64
| ~ spl14_158
| ~ spl14_209 ),
inference(avatar_contradiction_clause,[],[f3679]) ).
fof(f3682,plain,
( op2(e23,e23) != h1(op1(e13,e13))
| spl14_56
| ~ spl14_64 ),
inference(forward_demodulation,[],[f850,f893]) ).
fof(f3684,plain,
( op2(e23,e23) != h1(e11)
| spl14_56
| ~ spl14_64
| ~ spl14_228 ),
inference(forward_demodulation,[],[f3682,f1676]) ).
fof(f3686,plain,
( e21 != op2(e23,e23)
| ~ spl14_9
| spl14_56
| ~ spl14_64
| ~ spl14_228 ),
inference(forward_demodulation,[],[f3684,f635]) ).
fof(f3688,plain,
( $false
| ~ spl14_9
| spl14_56
| ~ spl14_64
| ~ spl14_177
| ~ spl14_228 ),
inference(forward_subsumption_resolution,[],[f3686,f1424]) ).
fof(f3689,plain,
( ~ spl14_9
| spl14_56
| ~ spl14_64
| ~ spl14_177
| ~ spl14_228 ),
inference(avatar_contradiction_clause,[],[f3688]) ).
fof(f3694,plain,
( ~ spl14_142
| ~ spl14_5
| spl14_44
| ~ spl14_64
| ~ spl14_193 ),
inference(avatar_split_clause,[],[f3572,f1514,f892,f800,f615,f1262]) ).
fof(f3697,plain,
( e20 = e23
| ~ spl14_112
| ~ spl14_152 ),
inference(forward_demodulation,[],[f2760,f1117]) ).
fof(f3703,plain,
( $false
| ~ spl14_168
| ~ spl14_182 ),
inference(forward_subsumption_resolution,[],[f3229,f1382]) ).
fof(f3704,plain,
( ~ spl14_168
| ~ spl14_182 ),
inference(avatar_contradiction_clause,[],[f3703]) ).
fof(f3717,plain,
( e20 != op2(e22,e22)
| ~ spl14_150 ),
inference(forward_demodulation,[],[f173,f1299]) ).
fof(f3754,plain,
( $false
| ~ spl14_112
| ~ spl14_152 ),
inference(forward_subsumption_resolution,[],[f3697,f222]) ).
fof(f3755,plain,
( ~ spl14_112
| ~ spl14_152 ),
inference(avatar_contradiction_clause,[],[f3754]) ).
fof(f3761,plain,
( ~ spl14_152
| ~ spl14_150 ),
inference(avatar_split_clause,[],[f3717,f1298,f1307]) ).
fof(f3790,plain,
( ~ spl14_201
| ~ spl14_203 ),
inference(avatar_split_clause,[],[f2798,f1559,f1550]) ).
fof(f3797,plain,
( e10 != op1(e11,e13)
| ~ spl14_256 ),
inference(forward_demodulation,[],[f132,f1863]) ).
fof(f3801,plain,
( e11 != op1(e12,e12)
| ~ spl14_202 ),
inference(forward_demodulation,[],[f127,f1556]) ).
fof(f3806,plain,
( ~ spl14_203
| ~ spl14_209 ),
inference(avatar_split_clause,[],[f3052,f1586,f1559]) ).
fof(f3807,plain,
( e11 != op1(e12,e11)
| ~ spl14_202 ),
inference(forward_demodulation,[],[f128,f1556]) ).
fof(f3808,plain,
( e12 != op1(e12,e11)
| ~ spl14_219 ),
inference(forward_demodulation,[],[f155,f1634]) ).
fof(f3810,plain,
( ~ spl14_189
| ~ spl14_193 ),
inference(avatar_split_clause,[],[f2812,f1514,f1496]) ).
fof(f3821,plain,
( ~ spl14_199
| ~ spl14_256 ),
inference(avatar_split_clause,[],[f3797,f1861,f1541]) ).
fof(f3824,plain,
( ~ spl14_263
| ~ spl14_202 ),
inference(avatar_split_clause,[],[f3807,f1554,f1899]) ).
fof(f3825,plain,
( ~ spl14_223
| ~ spl14_219 ),
inference(avatar_split_clause,[],[f3808,f1632,f1651]) ).
fof(f3841,plain,
( e11 = e12
| ~ spl14_218
| ~ spl14_265 ),
inference(forward_demodulation,[],[f1910,f1629]) ).
fof(f3847,plain,
( ~ spl14_232
| ~ spl14_194 ),
inference(avatar_split_clause,[],[f2917,f1518,f1694]) ).
fof(f3848,plain,
( ~ spl14_222
| ~ spl14_202 ),
inference(avatar_split_clause,[],[f3801,f1554,f1647]) ).
fof(f3850,plain,
( e10 != op1(e11,e11)
| ~ spl14_256 ),
inference(forward_demodulation,[],[f134,f1863]) ).
fof(f3853,plain,
( e11 != op1(e10,e13)
| ~ spl14_259 ),
inference(forward_demodulation,[],[f136,f1876]) ).
fof(f3854,plain,
( e13 != op1(e10,e13)
| ~ spl14_194 ),
inference(forward_demodulation,[],[f138,f1520]) ).
fof(f3856,plain,
( ~ spl14_191
| ~ spl14_209 ),
inference(avatar_split_clause,[],[f3055,f1586,f1505]) ).
fof(f3857,plain,
( $false
| ~ spl14_218
| ~ spl14_265 ),
inference(forward_subsumption_resolution,[],[f3841,f215]) ).
fof(f3858,plain,
( ~ spl14_218
| ~ spl14_265 ),
inference(avatar_contradiction_clause,[],[f3857]) ).
fof(f3859,plain,
( ~ spl14_195
| ~ spl14_256 ),
inference(avatar_split_clause,[],[f3850,f1861,f1523]) ).
fof(f3860,plain,
( ~ spl14_261
| ~ spl14_194 ),
inference(avatar_split_clause,[],[f3854,f1518,f1886]) ).
fof(f3869,plain,
( ~ spl14_189
| ~ spl14_201 ),
inference(avatar_split_clause,[],[f3313,f1550,f1496]) ).
fof(f3874,plain,
( ~ spl14_216
| ~ spl14_259 ),
inference(avatar_split_clause,[],[f3853,f1874,f1618]) ).
fof(f3881,plain,
( e12 != op1(e13,e12)
| ~ spl14_210 ),
inference(forward_demodulation,[],[f121,f1592]) ).
fof(f3882,plain,
( e11 != op1(e13,e12)
| ~ spl14_218 ),
inference(forward_demodulation,[],[f148,f1629]) ).
fof(f3883,plain,
( ~ spl14_268
| ~ spl14_210 ),
inference(avatar_split_clause,[],[f3881,f1590,f1929]) ).
fof(f3885,plain,
( ~ spl14_226
| ~ spl14_218 ),
inference(avatar_split_clause,[],[f3882,f1628,f1666]) ).
cnf(s4,plain,
( spl14_1
| ~ spl14_5 ),
inference(sat_conversion,[],[f618]) ).
cnf(s7,plain,
( ~ spl14_6
| ~ spl14_9 ),
inference(sat_conversion,[],[f637]) ).
cnf(s46,plain,
( ~ spl14_1
| spl14_6
| ~ spl14_41
| ~ spl14_42
| ~ spl14_43
| ~ spl14_44
| ~ spl14_45
| ~ spl14_46
| ~ spl14_47
| ~ spl14_48
| ~ spl14_49
| ~ spl14_50
| ~ spl14_51
| ~ spl14_52
| ~ spl14_53
| ~ spl14_54
| ~ spl14_55
| ~ spl14_56
| ~ spl14_59
| ~ spl14_64 ),
inference(sat_conversion,[],[f896]) ).
cnf(s98,plain,
spl14_109,
inference(sat_conversion,[],[f1236]) ).
cnf(s100,plain,
spl14_5,
inference(sat_conversion,[],[f1238]) ).
cnf(s101,plain,
( ~ spl14_137
| ~ spl14_138
| spl14_139 ),
inference(sat_conversion,[],[f1251]) ).
cnf(s102,plain,
( ~ spl14_137
| ~ spl14_140
| spl14_141 ),
inference(sat_conversion,[],[f1260]) ).
cnf(s108,plain,
( ~ spl14_137
| ~ spl14_152
| spl14_153 ),
inference(sat_conversion,[],[f1314]) ).
cnf(s118,plain,
( spl14_162
| ~ spl14_169
| spl14_170 ),
inference(sat_conversion,[],[f1392]) ).
cnf(s119,plain,
( spl14_150
| ~ spl14_151
| spl14_162 ),
inference(sat_conversion,[],[f1393]) ).
cnf(s129,plain,
( spl14_167
| ~ spl14_168
| spl14_179 ),
inference(sat_conversion,[],[f1447]) ).
cnf(s134,plain,
( spl14_158
| ~ spl14_159
| spl14_179 ),
inference(sat_conversion,[],[f1468]) ).
cnf(s137,plain,
( spl14_137
| spl14_142
| ~ spl14_143
| ~ spl14_162
| ~ spl14_179 ),
inference(sat_conversion,[],[f1479]) ).
cnf(s148,plain,
( spl14_137
| ~ spl14_162
| ~ spl14_179
| spl14_186
| ~ spl14_187 ),
inference(sat_conversion,[],[f1490]) ).
cnf(s156,plain,
( spl14_188
| ~ spl14_203
| spl14_204 ),
inference(sat_conversion,[],[f1566]) ).
cnf(s158,plain,
( spl14_188
| ~ spl14_207
| spl14_208 ),
inference(sat_conversion,[],[f1584]) ).
cnf(s160,plain,
( spl14_188
| ~ spl14_211
| spl14_212 ),
inference(sat_conversion,[],[f1602]) ).
cnf(s165,plain,
( spl14_213
| ~ spl14_218
| spl14_219 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s167,plain,
( spl14_201
| ~ spl14_202
| spl14_213 ),
inference(sat_conversion,[],[f1645]) ).
cnf(s172,plain,
( spl14_213
| ~ spl14_228
| spl14_229 ),
inference(sat_conversion,[],[f1682]) ).
cnf(s175,plain,
( ~ spl14_230
| ~ spl14_231
| spl14_232 ),
inference(sat_conversion,[],[f1697]) ).
cnf(s178,plain,
( ~ spl14_230
| ~ spl14_233
| spl14_234 ),
inference(sat_conversion,[],[f1708]) ).
cnf(s182,plain,
( spl14_209
| ~ spl14_210
| ~ spl14_230 ),
inference(sat_conversion,[],[f1720]) ).
cnf(s185,plain,
( ~ spl14_188
| spl14_193
| ~ spl14_194
| ~ spl14_213
| spl14_230 ),
inference(sat_conversion,[],[f1731]) ).
cnf(s189,plain,
( ~ spl14_188
| ~ spl14_213
| spl14_220
| ~ spl14_221
| spl14_230 ),
inference(sat_conversion,[],[f1735]) ).
cnf(s192,plain,
( ~ spl14_188
| ~ spl14_213
| spl14_224
| ~ spl14_225
| spl14_230 ),
inference(sat_conversion,[],[f1738]) ).
cnf(s196,plain,
( ~ spl14_188
| ~ spl14_213
| spl14_230
| spl14_237
| ~ spl14_238 ),
inference(sat_conversion,[],[f1742]) ).
cnf(s197,plain,
( spl14_138
| spl14_140
| spl14_142
| spl14_239 ),
inference(sat_conversion,[],[f1747]) ).
cnf(s198,plain,
( spl14_239
| spl14_240
| spl14_241
| spl14_242 ),
inference(sat_conversion,[],[f1760]) ).
cnf(s199,plain,
( spl14_139
| spl14_163
| spl14_165
| spl14_243 ),
inference(sat_conversion,[],[f1765]) ).
cnf(s201,plain,
( spl14_141
| spl14_164
| spl14_180
| spl14_244 ),
inference(sat_conversion,[],[f1771]) ).
cnf(s207,plain,
( spl14_145
| spl14_167
| spl14_169
| spl14_246 ),
inference(sat_conversion,[],[f1785]) ).
cnf(s211,plain,
( spl14_149
| spl14_170
| spl14_183
| spl14_250 ),
inference(sat_conversion,[],[f1805]) ).
cnf(s213,plain,
( spl14_150
| spl14_152
| spl14_154
| spl14_241 ),
inference(sat_conversion,[],[f1807]) ).
cnf(s216,plain,
( spl14_163
| spl14_167
| spl14_171
| spl14_175 ),
inference(sat_conversion,[],[f1810]) ).
cnf(s217,plain,
( spl14_153
| spl14_172
| spl14_184
| spl14_251 ),
inference(sat_conversion,[],[f1815]) ).
cnf(s221,plain,
( spl14_156
| spl14_158
| spl14_160
| spl14_242 ),
inference(sat_conversion,[],[f1827]) ).
cnf(s222,plain,
( spl14_142
| spl14_148
| spl14_154
| spl14_160 ),
inference(sat_conversion,[],[f1828]) ).
cnf(s223,plain,
( spl14_157
| spl14_175
| spl14_177
| spl14_248 ),
inference(sat_conversion,[],[f1829]) ).
cnf(s226,plain,
( spl14_180
| spl14_182
| spl14_184
| spl14_186 ),
inference(sat_conversion,[],[f1832]) ).
cnf(s227,plain,
( spl14_161
| spl14_178
| spl14_187
| spl14_254 ),
inference(sat_conversion,[],[f1837]) ).
cnf(s231,plain,
( spl14_140
| spl14_163
| spl14_181
| spl14_244 ),
inference(sat_conversion,[],[f1841]) ).
cnf(s234,plain,
( spl14_144
| spl14_168
| spl14_170
| spl14_246 ),
inference(sat_conversion,[],[f1844]) ).
cnf(s239,plain,
( spl14_152
| spl14_171
| spl14_185
| spl14_251 ),
inference(sat_conversion,[],[f1849]) ).
cnf(s245,plain,
( spl14_189
| spl14_191
| spl14_193
| spl14_255 ),
inference(sat_conversion,[],[f1859]) ).
cnf(s246,plain,
( spl14_255
| spl14_256
| spl14_257
| spl14_258 ),
inference(sat_conversion,[],[f1872]) ).
cnf(s249,plain,
( spl14_192
| spl14_215
| spl14_231
| spl14_260 ),
inference(sat_conversion,[],[f1883]) ).
cnf(s254,plain,
( spl14_189
| spl14_195
| spl14_201
| spl14_207 ),
inference(sat_conversion,[],[f1892]) ).
cnf(s255,plain,
( spl14_196
| spl14_218
| spl14_220
| spl14_262 ),
inference(sat_conversion,[],[f1897]) ).
cnf(s256,plain,
( spl14_259
| spl14_262
| spl14_263
| spl14_264 ),
inference(sat_conversion,[],[f1906]) ).
cnf(s257,plain,
( spl14_198
| spl14_219
| spl14_233
| spl14_265 ),
inference(sat_conversion,[],[f1911]) ).
cnf(s260,plain,
( spl14_217
| spl14_221
| spl14_225
| spl14_229 ),
inference(sat_conversion,[],[f1918]) ).
cnf(s261,plain,
( spl14_201
| spl14_203
| spl14_205
| spl14_257 ),
inference(sat_conversion,[],[f1919]) ).
cnf(s265,plain,
( spl14_204
| spl14_223
| spl14_235
| spl14_267 ),
inference(sat_conversion,[],[f1927]) ).
cnf(s266,plain,
( spl14_260
| spl14_265
| spl14_267
| spl14_268 ),
inference(sat_conversion,[],[f1932]) ).
cnf(s269,plain,
( spl14_207
| spl14_209
| spl14_211
| spl14_258 ),
inference(sat_conversion,[],[f1939]) ).
cnf(s270,plain,
( spl14_193
| spl14_199
| spl14_205
| spl14_211 ),
inference(sat_conversion,[],[f1940]) ).
cnf(s271,plain,
( spl14_208
| spl14_226
| spl14_228
| spl14_264 ),
inference(sat_conversion,[],[f1941]) ).
cnf(s272,plain,
( spl14_216
| spl14_220
| spl14_224
| spl14_228 ),
inference(sat_conversion,[],[f1942]) ).
cnf(s275,plain,
( spl14_212
| spl14_229
| spl14_238
| spl14_270 ),
inference(sat_conversion,[],[f1949]) ).
cnf(s276,plain,
( spl14_261
| spl14_266
| spl14_269
| spl14_270 ),
inference(sat_conversion,[],[f1950]) ).
cnf(s280,plain,
( spl14_193
| spl14_216
| spl14_231
| spl14_261 ),
inference(sat_conversion,[],[f1954]) ).
cnf(s282,plain,
( spl14_195
| spl14_219
| spl14_221
| spl14_262 ),
inference(sat_conversion,[],[f1956]) ).
cnf(s286,plain,
( spl14_201
| spl14_223
| spl14_225
| spl14_263 ),
inference(sat_conversion,[],[f1960]) ).
cnf(s287,plain,
( spl14_203
| spl14_222
| spl14_236
| spl14_267 ),
inference(sat_conversion,[],[f1961]) ).
cnf(s291,plain,
( spl14_209
| spl14_226
| spl14_238
| spl14_268 ),
inference(sat_conversion,[],[f1965]) ).
cnf(s293,plain,
~ spl14_270,
inference(sat_conversion,[],[f1971]) ).
cnf(s294,plain,
~ spl14_267,
inference(sat_conversion,[],[f1972]) ).
cnf(s295,plain,
~ spl14_262,
inference(sat_conversion,[],[f1973]) ).
cnf(s296,plain,
~ spl14_255,
inference(sat_conversion,[],[f1974]) ).
cnf(s297,plain,
~ spl14_254,
inference(sat_conversion,[],[f1975]) ).
cnf(s298,plain,
~ spl14_251,
inference(sat_conversion,[],[f1976]) ).
cnf(s299,plain,
~ spl14_246,
inference(sat_conversion,[],[f1977]) ).
cnf(s300,plain,
~ spl14_239,
inference(sat_conversion,[],[f1978]) ).
cnf(s301,plain,
spl14_194,
inference(sat_conversion,[],[f1979]) ).
cnf(s302,plain,
spl14_143,
inference(sat_conversion,[],[f1980]) ).
cnf(s304,plain,
( ~ spl14_139
| ~ spl14_143 ),
inference(sat_conversion,[],[f1988]) ).
cnf(s312,plain,
( ~ spl14_157
| ~ spl14_159 ),
inference(sat_conversion,[],[f2019]) ).
cnf(s313,plain,
( ~ spl14_158
| ~ spl14_175 ),
inference(sat_conversion,[],[f2022]) ).
cnf(s315,plain,
( ~ spl14_141
| ~ spl14_143 ),
inference(sat_conversion,[],[f2028]) ).
cnf(s317,plain,
( ~ spl14_159
| ~ spl14_161 ),
inference(sat_conversion,[],[f2038]) ).
cnf(s325,plain,
( spl14_25
| ~ spl14_109
| ~ spl14_150
| ~ spl14_172 ),
inference(sat_conversion,[],[f2072]) ).
cnf(s327,plain,
( ~ spl14_25
| ~ spl14_109
| ~ spl14_159
| spl14_252 ),
inference(sat_conversion,[],[f2098]) ).
cnf(s333,plain,
( ~ spl14_25
| ~ spl14_109
| ~ spl14_143
| spl14_185 ),
inference(sat_conversion,[],[f2106]) ).
cnf(s335,plain,
( ~ spl14_25
| ~ spl14_109
| ~ spl14_140
| spl14_251 ),
inference(sat_conversion,[],[f2108]) ).
cnf(s337,plain,
( ~ spl14_160
| ~ spl14_177 ),
inference(sat_conversion,[],[f2118]) ).
cnf(s339,plain,
( ~ spl14_156
| ~ spl14_178 ),
inference(sat_conversion,[],[f2126]) ).
cnf(s341,plain,
( ~ spl14_165
| ~ spl14_180 ),
inference(sat_conversion,[],[f2133]) ).
cnf(s358,plain,
( ~ spl14_205
| ~ spl14_269 ),
inference(sat_conversion,[],[f2199]) ).
cnf(s359,plain,
( ~ spl14_208
| ~ spl14_210 ),
inference(sat_conversion,[],[f2202]) ).
cnf(s363,plain,
( ~ spl14_209
| ~ spl14_238 ),
inference(sat_conversion,[],[f2218]) ).
cnf(s369,plain,
( ~ spl14_193
| ~ spl14_231 ),
inference(sat_conversion,[],[f2246]) ).
cnf(s371,plain,
( ~ spl14_211
| ~ spl14_237 ),
inference(sat_conversion,[],[f2254]) ).
cnf(s375,plain,
( ~ spl14_138
| ~ spl14_243 ),
inference(sat_conversion,[],[f2277]) ).
cnf(s376,plain,
( spl14_25
| ~ spl14_109
| ~ spl14_142
| ~ spl14_180 ),
inference(sat_conversion,[],[f2281]) ).
cnf(s379,plain,
( ~ spl14_177
| ~ spl14_186 ),
inference(sat_conversion,[],[f2300]) ).
cnf(s380,plain,
( ~ spl14_177
| ~ spl14_186 ),
inference(sat_conversion,[],[f2302]) ).
cnf(s385,plain,
( spl14_25
| ~ spl14_109
| ~ spl14_154
| ~ spl14_184 ),
inference(sat_conversion,[],[f2318]) ).
cnf(s397,plain,
( ~ spl14_178
| ~ spl14_248 ),
inference(sat_conversion,[],[f2381]) ).
cnf(s399,plain,
( ~ spl14_148
| ~ spl14_250 ),
inference(sat_conversion,[],[f2391]) ).
cnf(s404,plain,
( ~ spl14_142
| ~ spl14_165 ),
inference(sat_conversion,[],[f2411]) ).
cnf(s405,plain,
( ~ spl14_175
| ~ spl14_187 ),
inference(sat_conversion,[],[f2414]) ).
cnf(s407,plain,
( ~ spl14_156
| ~ spl14_248 ),
inference(sat_conversion,[],[f2427]) ).
cnf(s409,plain,
( ~ spl14_149
| ~ spl14_240 ),
inference(sat_conversion,[],[f2445]) ).
cnf(s415,plain,
( ~ spl14_196
| ~ spl14_256 ),
inference(sat_conversion,[],[f2483]) ).
cnf(s421,plain,
( ~ spl14_207
| ~ spl14_264 ),
inference(sat_conversion,[],[f2510]) ).
cnf(s422,plain,
( ~ spl14_224
| ~ spl14_235 ),
inference(sat_conversion,[],[f2513]) ).
cnf(s429,plain,
( ~ spl14_220
| ~ spl14_233 ),
inference(sat_conversion,[],[f2551]) ).
cnf(s431,plain,
( ~ spl14_219
| ~ spl14_221 ),
inference(sat_conversion,[],[f2559]) ).
cnf(s435,plain,
( ~ spl14_202
| ~ spl14_257 ),
inference(sat_conversion,[],[f2580]) ).
cnf(s437,plain,
( ~ spl14_198
| ~ spl14_256 ),
inference(sat_conversion,[],[f2587]) ).
cnf(s439,plain,
( ~ spl14_215
| ~ spl14_259 ),
inference(sat_conversion,[],[f2598]) ).
cnf(s442,plain,
( ~ spl14_235
| ~ spl14_269 ),
inference(sat_conversion,[],[f2619]) ).
cnf(s444,plain,
( ~ spl14_220
| ~ spl14_266 ),
inference(sat_conversion,[],[f2626]) ).
cnf(s449,plain,
( ~ spl14_192
| ~ spl14_194 ),
inference(sat_conversion,[],[f2652]) ).
cnf(s451,plain,
( ~ spl14_226
| ~ spl14_238 ),
inference(sat_conversion,[],[f2667]) ).
cnf(s454,plain,
( ~ spl14_205
| ~ spl14_235 ),
inference(sat_conversion,[],[f2682]) ).
cnf(s459,plain,
( spl14_64
| ~ spl14_143 ),
inference(sat_conversion,[],[f2757]) ).
cnf(s471,plain,
( ~ spl14_185
| ~ spl14_187 ),
inference(sat_conversion,[],[f2889]) ).
cnf(s477,plain,
( ~ spl14_234
| ~ spl14_238 ),
inference(sat_conversion,[],[f2928]) ).
cnf(s478,plain,
( ~ spl14_194
| spl14_210 ),
inference(sat_conversion,[],[f2929]) ).
cnf(s480,plain,
( ~ spl14_194
| ~ spl14_217 ),
inference(sat_conversion,[],[f2934]) ).
cnf(s483,plain,
( ~ spl14_193
| ~ spl14_211 ),
inference(sat_conversion,[],[f2937]) ).
cnf(s484,plain,
( ~ spl14_204
| ~ spl14_210 ),
inference(sat_conversion,[],[f2938]) ).
cnf(s485,plain,
( ~ spl14_194
| ~ spl14_212 ),
inference(sat_conversion,[],[f2939]) ).
cnf(s486,plain,
( ~ spl14_229
| ~ spl14_238 ),
inference(sat_conversion,[],[f2940]) ).
cnf(s487,plain,
( ~ spl14_236
| ~ spl14_238 ),
inference(sat_conversion,[],[f2944]) ).
cnf(s493,plain,
( ~ spl14_210
| ~ spl14_258 ),
inference(sat_conversion,[],[f2993]) ).
cnf(s498,plain,
( ~ spl14_229
| ~ spl14_264 ),
inference(sat_conversion,[],[f3020]) ).
cnf(s503,plain,
( ~ spl14_25
| ~ spl14_109
| spl14_157
| ~ spl14_175 ),
inference(sat_conversion,[],[f3078]) ).
cnf(s505,plain,
( ~ spl14_143
| spl14_159 ),
inference(sat_conversion,[],[f3090]) ).
cnf(s507,plain,
( ~ spl14_152
| ~ spl14_158 ),
inference(sat_conversion,[],[f3097]) ).
cnf(s508,plain,
( ~ spl14_167
| ~ spl14_175 ),
inference(sat_conversion,[],[f3098]) ).
cnf(s509,plain,
( ~ spl14_244
| ~ spl14_252 ),
inference(sat_conversion,[],[f3099]) ).
cnf(s514,plain,
( ~ spl14_142
| ~ spl14_160 ),
inference(sat_conversion,[],[f3104]) ).
cnf(s515,plain,
( ~ spl14_153
| ~ spl14_159 ),
inference(sat_conversion,[],[f3105]) ).
cnf(s542,plain,
( spl14_59
| ~ spl14_143
| ~ spl14_159 ),
inference(sat_conversion,[],[f3252]) ).
cnf(s551,plain,
( ~ spl14_225
| ~ spl14_236 ),
inference(sat_conversion,[],[f3273]) ).
cnf(s554,plain,
( ~ spl14_260
| ~ spl14_265 ),
inference(sat_conversion,[],[f3276]) ).
cnf(s555,plain,
( ~ spl14_194
| spl14_202
| ~ spl14_210 ),
inference(sat_conversion,[],[f3277]) ).
cnf(s556,plain,
( ~ spl14_219
| ~ spl14_265 ),
inference(sat_conversion,[],[f3278]) ).
cnf(s557,plain,
( ~ spl14_221
| ~ spl14_229 ),
inference(sat_conversion,[],[f3279]) ).
cnf(s560,plain,
( ~ spl14_143
| ~ spl14_159
| ~ spl14_241 ),
inference(sat_conversion,[],[f3326]) ).
cnf(s561,plain,
( ~ spl14_151
| ~ spl14_171 ),
inference(sat_conversion,[],[f3331]) ).
cnf(s562,plain,
( ~ spl14_143
| spl14_151
| ~ spl14_159 ),
inference(sat_conversion,[],[f3332]) ).
cnf(s564,plain,
( spl14_25
| ~ spl14_109
| ~ spl14_159
| ~ spl14_242 ),
inference(sat_conversion,[],[f3337]) ).
cnf(s565,plain,
( ~ spl14_145
| ~ spl14_151 ),
inference(sat_conversion,[],[f3338]) ).
cnf(s566,plain,
( ~ spl14_144
| ~ spl14_240 ),
inference(sat_conversion,[],[f3344]) ).
cnf(s571,plain,
( ~ spl14_163
| ~ spl14_244 ),
inference(sat_conversion,[],[f3357]) ).
cnf(s578,plain,
( ~ spl14_183
| ~ spl14_185 ),
inference(sat_conversion,[],[f3363]) ).
cnf(s579,plain,
( ~ spl14_142
| ~ spl14_154 ),
inference(sat_conversion,[],[f3364]) ).
cnf(s582,plain,
( ~ spl14_170
| ~ spl14_178 ),
inference(sat_conversion,[],[f3371]) ).
cnf(s584,plain,
( ~ spl14_143
| ~ spl14_181 ),
inference(sat_conversion,[],[f3375]) ).
cnf(s585,plain,
( ~ spl14_140
| ~ spl14_158 ),
inference(sat_conversion,[],[f3376]) ).
cnf(s590,plain,
( ~ spl14_163
| ~ spl14_167 ),
inference(sat_conversion,[],[f3382]) ).
cnf(s594,plain,
( ~ spl14_164
| ~ spl14_168 ),
inference(sat_conversion,[],[f3385]) ).
cnf(s603,plain,
( ~ spl14_169
| ~ spl14_177 ),
inference(sat_conversion,[],[f3400]) ).
cnf(s634,plain,
( spl14_112
| ~ spl14_185 ),
inference(sat_conversion,[],[f3509]) ).
cnf(s639,plain,
( spl14_9
| ~ spl14_143
| ~ spl14_151
| ~ spl14_159 ),
inference(sat_conversion,[],[f3543]) ).
cnf(s640,plain,
( ~ spl14_5
| ~ spl14_9
| spl14_42
| ~ spl14_243
| ~ spl14_259 ),
inference(sat_conversion,[],[f3546]) ).
cnf(s641,plain,
( ~ spl14_5
| spl14_41
| ~ spl14_64
| ~ spl14_143
| ~ spl14_194 ),
inference(sat_conversion,[],[f3554]) ).
cnf(s642,plain,
( ~ spl14_5
| spl14_43
| ~ spl14_59
| ~ spl14_244
| ~ spl14_260 ),
inference(sat_conversion,[],[f3564]) ).
cnf(s644,plain,
( ~ spl14_5
| ~ spl14_9
| spl14_45
| ~ spl14_240
| ~ spl14_256 ),
inference(sat_conversion,[],[f3584]) ).
cnf(s645,plain,
( ~ spl14_9
| spl14_46
| ~ spl14_59
| ~ spl14_168
| ~ spl14_219 ),
inference(sat_conversion,[],[f3593]) ).
cnf(s646,plain,
( ~ spl14_9
| spl14_47
| ~ spl14_59
| ~ spl14_167
| ~ spl14_218 ),
inference(sat_conversion,[],[f3602]) ).
cnf(s647,plain,
( ~ spl14_9
| spl14_48
| ~ spl14_64
| ~ spl14_250
| ~ spl14_266 ),
inference(sat_conversion,[],[f3612]) ).
cnf(s648,plain,
( ~ spl14_5
| ~ spl14_9
| spl14_49
| ~ spl14_59
| ~ spl14_151
| ~ spl14_202 ),
inference(sat_conversion,[],[f3622]) ).
cnf(s649,plain,
( ~ spl14_5
| ~ spl14_9
| spl14_50
| ~ spl14_59
| ~ spl14_150
| ~ spl14_201 ),
inference(sat_conversion,[],[f3632]) ).
cnf(s650,plain,
( spl14_51
| ~ spl14_59
| ~ spl14_64
| ~ spl14_185
| ~ spl14_236 ),
inference(sat_conversion,[],[f3641]) ).
cnf(s651,plain,
( spl14_52
| ~ spl14_59
| ~ spl14_64
| ~ spl14_184
| ~ spl14_235 ),
inference(sat_conversion,[],[f3650]) ).
cnf(s652,plain,
( ~ spl14_5
| spl14_53
| ~ spl14_59
| ~ spl14_64
| ~ spl14_159
| ~ spl14_210 ),
inference(sat_conversion,[],[f3660]) ).
cnf(s653,plain,
( ~ spl14_9
| spl14_54
| ~ spl14_64
| ~ spl14_178
| ~ spl14_229 ),
inference(sat_conversion,[],[f3670]) ).
cnf(s654,plain,
( ~ spl14_5
| spl14_55
| ~ spl14_59
| ~ spl14_64
| ~ spl14_158
| ~ spl14_209 ),
inference(sat_conversion,[],[f3680]) ).
cnf(s655,plain,
( ~ spl14_9
| spl14_56
| ~ spl14_64
| ~ spl14_177
| ~ spl14_228 ),
inference(sat_conversion,[],[f3689]) ).
cnf(s658,plain,
( ~ spl14_5
| spl14_44
| ~ spl14_64
| ~ spl14_142
| ~ spl14_193 ),
inference(sat_conversion,[],[f3694]) ).
cnf(s665,plain,
( ~ spl14_168
| ~ spl14_182 ),
inference(sat_conversion,[],[f3704]) ).
cnf(s678,plain,
( ~ spl14_112
| ~ spl14_152 ),
inference(sat_conversion,[],[f3755]) ).
cnf(s686,plain,
( ~ spl14_150
| ~ spl14_152 ),
inference(sat_conversion,[],[f3761]) ).
cnf(s705,plain,
( ~ spl14_201
| ~ spl14_203 ),
inference(sat_conversion,[],[f3790]) ).
cnf(s707,plain,
( ~ spl14_203
| ~ spl14_209 ),
inference(sat_conversion,[],[f3806]) ).
cnf(s708,plain,
( ~ spl14_189
| ~ spl14_193 ),
inference(sat_conversion,[],[f3810]) ).
cnf(s712,plain,
( ~ spl14_199
| ~ spl14_256 ),
inference(sat_conversion,[],[f3821]) ).
cnf(s714,plain,
( ~ spl14_202
| ~ spl14_263 ),
inference(sat_conversion,[],[f3824]) ).
cnf(s715,plain,
( ~ spl14_219
| ~ spl14_223 ),
inference(sat_conversion,[],[f3825]) ).
cnf(s731,plain,
( ~ spl14_194
| ~ spl14_232 ),
inference(sat_conversion,[],[f3847]) ).
cnf(s732,plain,
( ~ spl14_202
| ~ spl14_222 ),
inference(sat_conversion,[],[f3848]) ).
cnf(s734,plain,
( ~ spl14_191
| ~ spl14_209 ),
inference(sat_conversion,[],[f3856]) ).
cnf(s736,plain,
( ~ spl14_218
| ~ spl14_265 ),
inference(sat_conversion,[],[f3858]) ).
cnf(s737,plain,
( ~ spl14_195
| ~ spl14_256 ),
inference(sat_conversion,[],[f3859]) ).
cnf(s738,plain,
( ~ spl14_194
| ~ spl14_261 ),
inference(sat_conversion,[],[f3860]) ).
cnf(s740,plain,
( ~ spl14_189
| ~ spl14_201 ),
inference(sat_conversion,[],[f3869]) ).
cnf(s744,plain,
( ~ spl14_216
| ~ spl14_259 ),
inference(sat_conversion,[],[f3874]) ).
cnf(s747,plain,
( ~ spl14_210
| ~ spl14_268 ),
inference(sat_conversion,[],[f3883]) ).
cnf(s749,plain,
( ~ spl14_218
| ~ spl14_226 ),
inference(sat_conversion,[],[f3885]) ).
cnf(s751,plain,
~ spl14_181,
inference(rat,[],[s584,s302]) ).
cnf(s752,plain,
spl14_159,
inference(rat,[],[s505,s302]) ).
cnf(s753,plain,
spl14_64,
inference(rat,[],[s459,s302]) ).
cnf(s754,plain,
~ spl14_141,
inference(rat,[],[s315,s302]) ).
cnf(s755,plain,
~ spl14_139,
inference(rat,[],[s304,s302]) ).
cnf(s756,plain,
~ spl14_241,
inference(rat,[],[s560,s302,s752]) ).
cnf(s757,plain,
~ spl14_153,
inference(rat,[],[s515,s752]) ).
cnf(s758,plain,
~ spl14_161,
inference(rat,[],[s317,s752]) ).
cnf(s759,plain,
~ spl14_157,
inference(rat,[],[s312,s752]) ).
cnf(s760,plain,
spl14_151,
inference(rat,[],[s562,s302,s752]) ).
cnf(s761,plain,
spl14_59,
inference(rat,[],[s542,s302,s752]) ).
cnf(s762,plain,
~ spl14_145,
inference(rat,[],[s565,s760]) ).
cnf(s763,plain,
~ spl14_171,
inference(rat,[],[s561,s760]) ).
cnf(s764,plain,
spl14_9,
inference(rat,[],[s639,s752,s302,s760]) ).
cnf(s766,plain,
~ spl14_261,
inference(rat,[],[s738,s301]) ).
cnf(s767,plain,
~ spl14_232,
inference(rat,[],[s731,s301]) ).
cnf(s769,plain,
~ spl14_212,
inference(rat,[],[s485,s301]) ).
cnf(s770,plain,
~ spl14_217,
inference(rat,[],[s480,s301]) ).
cnf(s771,plain,
spl14_210,
inference(rat,[],[s478,s301]) ).
cnf(s772,plain,
~ spl14_192,
inference(rat,[],[s449,s301]) ).
cnf(s774,plain,
~ spl14_268,
inference(rat,[],[s747,s771]) ).
cnf(s775,plain,
~ spl14_258,
inference(rat,[],[s493,s771]) ).
cnf(s776,plain,
~ spl14_204,
inference(rat,[],[s484,s771]) ).
cnf(s777,plain,
~ spl14_208,
inference(rat,[],[s359,s771]) ).
cnf(s778,plain,
spl14_202,
inference(rat,[],[s555,s301,s771]) ).
cnf(s779,plain,
~ spl14_222,
inference(rat,[],[s732,s778]) ).
cnf(s780,plain,
~ spl14_263,
inference(rat,[],[s714,s778]) ).
cnf(s781,plain,
~ spl14_257,
inference(rat,[],[s435,s778]) ).
cnf(s783,plain,
( spl14_209
| spl14_226
| spl14_238 ),
inference(rat,[],[s291,s774]) ).
cnf(s784,plain,
( spl14_203
| spl14_236 ),
inference(rat,[],[s287,s294,s779]) ).
cnf(s785,plain,
( spl14_201
| spl14_223
| spl14_225 ),
inference(rat,[],[s286,s780]) ).
cnf(s786,plain,
( spl14_195
| spl14_219
| spl14_221 ),
inference(rat,[],[s282,s295]) ).
cnf(s787,plain,
( spl14_193
| spl14_216
| spl14_231 ),
inference(rat,[],[s280,s766]) ).
cnf(s790,plain,
( spl14_266
| spl14_269 ),
inference(rat,[],[s276,s293,s766]) ).
cnf(s791,plain,
( spl14_229
| spl14_238 ),
inference(rat,[],[s275,s293,s769]) ).
cnf(s792,plain,
( spl14_226
| spl14_228
| spl14_264 ),
inference(rat,[],[s271,s777]) ).
cnf(s793,plain,
( spl14_207
| spl14_209
| spl14_211 ),
inference(rat,[],[s269,s775]) ).
cnf(s796,plain,
( spl14_260
| spl14_265 ),
inference(rat,[],[s266,s774,s294]) ).
cnf(s797,plain,
( spl14_223
| spl14_235 ),
inference(rat,[],[s265,s294,s776]) ).
cnf(s799,plain,
( spl14_201
| spl14_203
| spl14_205 ),
inference(rat,[],[s261,s781]) ).
cnf(s800,plain,
( spl14_221
| spl14_225
| spl14_229 ),
inference(rat,[],[s260,s770]) ).
cnf(s801,plain,
( spl14_259
| spl14_264 ),
inference(rat,[],[s256,s780,s295]) ).
cnf(s802,plain,
( spl14_196
| spl14_218
| spl14_220 ),
inference(rat,[],[s255,s295]) ).
cnf(s803,plain,
( spl14_215
| spl14_231
| spl14_260 ),
inference(rat,[],[s249,s772]) ).
cnf(s805,plain,
spl14_256,
inference(rat,[],[s246,s775,s781,s296]) ).
cnf(s806,plain,
~ spl14_195,
inference(rat,[],[s737,s805]) ).
cnf(s807,plain,
~ spl14_199,
inference(rat,[],[s712,s805]) ).
cnf(s808,plain,
~ spl14_198,
inference(rat,[],[s437,s805]) ).
cnf(s809,plain,
~ spl14_196,
inference(rat,[],[s415,s805]) ).
cnf(s810,plain,
( spl14_189
| spl14_191
| spl14_193 ),
inference(rat,[],[s245,s296]) ).
cnf(s812,plain,
( spl14_152
| spl14_185 ),
inference(rat,[],[s239,s298,s763]) ).
cnf(s813,plain,
( spl14_144
| spl14_168
| spl14_170 ),
inference(rat,[],[s234,s299]) ).
cnf(s815,plain,
( spl14_140
| spl14_163
| spl14_244 ),
inference(rat,[],[s231,s751]) ).
cnf(s818,plain,
( spl14_178
| spl14_187 ),
inference(rat,[],[s227,s297,s758]) ).
cnf(s819,plain,
( spl14_175
| spl14_177
| spl14_248 ),
inference(rat,[],[s223,s759]) ).
cnf(s822,plain,
( spl14_172
| spl14_184 ),
inference(rat,[],[s217,s298,s757]) ).
cnf(s823,plain,
( spl14_163
| spl14_167
| spl14_175 ),
inference(rat,[],[s216,s763]) ).
cnf(s824,plain,
( spl14_150
| spl14_152
| spl14_154 ),
inference(rat,[],[s213,s756]) ).
cnf(s827,plain,
( spl14_167
| spl14_169 ),
inference(rat,[],[s207,s299,s762]) ).
cnf(s828,plain,
( spl14_164
| spl14_180
| spl14_244 ),
inference(rat,[],[s201,s754]) ).
cnf(s829,plain,
( spl14_163
| spl14_165
| spl14_243 ),
inference(rat,[],[s199,s755]) ).
cnf(s830,plain,
( spl14_240
| spl14_242 ),
inference(rat,[],[s198,s756,s300]) ).
cnf(s831,plain,
( spl14_138
| spl14_140
| spl14_142 ),
inference(rat,[],[s197,s300]) ).
cnf(s833,plain,
( ~ spl14_188
| spl14_193
| ~ spl14_213
| spl14_230 ),
inference(rat,[],[s185,s301]) ).
cnf(s834,plain,
( spl14_209
| ~ spl14_230 ),
inference(rat,[],[s182,s771]) ).
cnf(s836,plain,
( ~ spl14_230
| ~ spl14_231 ),
inference(rat,[],[s175,s767]) ).
cnf(s837,plain,
( spl14_201
| spl14_213 ),
inference(rat,[],[s167,s778]) ).
cnf(s839,plain,
( spl14_188
| ~ spl14_211 ),
inference(rat,[],[s160,s769]) ).
cnf(s840,plain,
( spl14_188
| ~ spl14_207 ),
inference(rat,[],[s158,s777]) ).
cnf(s842,plain,
( spl14_188
| ~ spl14_203 ),
inference(rat,[],[s156,s776]) ).
cnf(s846,plain,
( spl14_137
| spl14_142
| ~ spl14_162
| ~ spl14_179 ),
inference(rat,[],[s137,s302]) ).
cnf(s847,plain,
( spl14_158
| spl14_179 ),
inference(rat,[],[s134,s752]) ).
cnf(s850,plain,
( spl14_150
| spl14_162 ),
inference(rat,[],[s119,s760]) ).
cnf(s854,plain,
( ~ spl14_137
| ~ spl14_152 ),
inference(rat,[],[s108,s757]) ).
cnf(s856,plain,
( ~ spl14_137
| ~ spl14_140 ),
inference(rat,[],[s102,s754]) ).
cnf(s857,plain,
( ~ spl14_137
| ~ spl14_138 ),
inference(rat,[],[s101,s755]) ).
cnf(s858,plain,
spl14_53,
inference(rat,[],[s652,s771,s752,s753,s761,s100]) ).
cnf(s859,plain,
spl14_49,
inference(rat,[],[s648,s778,s760,s761,s764,s100]) ).
cnf(s860,plain,
spl14_41,
inference(rat,[],[s641,s301,s302,s753,s100]) ).
cnf(s871,plain,
( ~ spl14_1
| spl14_6
| ~ spl14_42
| ~ spl14_43
| ~ spl14_44
| ~ spl14_45
| ~ spl14_46
| ~ spl14_47
| ~ spl14_48
| ~ spl14_50
| ~ spl14_51
| ~ spl14_52
| ~ spl14_54
| ~ spl14_55
| ~ spl14_56 ),
inference(rat,[],[s46,s753,s761,s858,s859,s860]) ).
cnf(s886,plain,
~ spl14_6,
inference(rat,[],[s7,s764]) ).
cnf(s887,plain,
spl14_1,
inference(rat,[],[s4,s100]) ).
cnf(s890,plain,
~ spl14_152,
inference(rat,[],[s379,s819,s148,s405,s818,s339,s407,s221,s514,s564,s846,s333,s847,s634,s850,s854,s507,s678,s686,s752,s98,s302]) ).
cnf(s892,plain,
spl14_185,
inference(rat,[],[s812,s890]) ).
cnf(s895,plain,
~ spl14_183,
inference(rat,[],[s578,s892]) ).
cnf(s897,plain,
~ spl14_187,
inference(rat,[],[s471,s892]) ).
cnf(s900,plain,
spl14_178,
inference(rat,[],[s818,s897]) ).
cnf(s902,plain,
~ spl14_170,
inference(rat,[],[s582,s900]) ).
cnf(s903,plain,
~ spl14_248,
inference(rat,[],[s397,s900]) ).
cnf(s904,plain,
~ spl14_156,
inference(rat,[],[s339,s900]) ).
cnf(s905,plain,
~ spl14_25,
inference(rat,[],[s590,s827,s815,s603,s509,s819,s327,s335,s503,s903,s752,s98,s298,s759]) ).
cnf(s906,plain,
~ spl14_242,
inference(rat,[],[s564,s98,s752,s905]) ).
cnf(s907,plain,
spl14_240,
inference(rat,[],[s830,s906]) ).
cnf(s908,plain,
~ spl14_149,
inference(rat,[],[s409,s907]) ).
cnf(s909,plain,
spl14_45,
inference(rat,[],[s644,s805,s100,s764,s907]) ).
cnf(s910,plain,
spl14_250,
inference(rat,[],[s211,s895,s902,s908]) ).
cnf(s912,plain,
~ spl14_148,
inference(rat,[],[s399,s910]) ).
cnf(s913,plain,
~ spl14_264,
inference(rat,[],[s196,s837,s371,s842,s705,s793,s834,s784,s363,s487,s791,s421,s498]) ).
cnf(s914,plain,
spl14_259,
inference(rat,[],[s801,s913]) ).
cnf(s915,plain,
~ spl14_216,
inference(rat,[],[s744,s914]) ).
cnf(s916,plain,
~ spl14_215,
inference(rat,[],[s439,s914]) ).
cnf(s917,plain,
spl14_260,
inference(rat,[],[s196,s172,s839,s371,s792,s270,s451,s358,s791,s790,s557,s444,s786,s802,s836,s369,s556,s736,s803,s796,s913,s807,s806,s809,s916]) ).
cnf(s918,plain,
~ spl14_265,
inference(rat,[],[s554,s917]) ).
cnf(s920,plain,
( spl14_219
| spl14_193 ),
inference(rat,[],[s842,s833,s784,s165,s487,s802,s791,s429,s557,s257,s786,s836,s787,s809,s808,s918,s806,s915]) ).
cnf(s921,plain,
spl14_193,
inference(rat,[],[s734,s783,s810,s486,s740,s172,s749,s837,s272,s802,s833,s444,s839,s790,s270,s422,s442,s454,s797,s715,s920,s836,s787,s915,s809,s807]) ).
cnf(s922,plain,
~ spl14_189,
inference(rat,[],[s708,s921]) ).
cnf(s923,plain,
~ spl14_211,
inference(rat,[],[s483,s921]) ).
cnf(s925,plain,
spl14_219,
inference(rat,[],[s842,s189,s178,s784,s165,s477,s487,s802,s791,s429,s557,s257,s786,s809,s808,s918,s806]) ).
cnf(s926,plain,
~ spl14_223,
inference(rat,[],[s715,s925]) ).
cnf(s928,plain,
~ spl14_221,
inference(rat,[],[s431,s925]) ).
cnf(s929,plain,
spl14_235,
inference(rat,[],[s797,s926]) ).
cnf(s930,plain,
~ spl14_205,
inference(rat,[],[s454,s929]) ).
cnf(s931,plain,
~ spl14_269,
inference(rat,[],[s442,s929]) ).
cnf(s932,plain,
~ spl14_224,
inference(rat,[],[s422,s929]) ).
cnf(s933,plain,
spl14_266,
inference(rat,[],[s790,s931]) ).
cnf(s935,plain,
~ spl14_220,
inference(rat,[],[s444,s933]) ).
cnf(s936,plain,
spl14_48,
inference(rat,[],[s647,s910,s764,s753,s933]) ).
cnf(s937,plain,
spl14_218,
inference(rat,[],[s802,s809,s935]) ).
cnf(s938,plain,
spl14_228,
inference(rat,[],[s272,s915,s932,s935]) ).
cnf(s939,plain,
~ spl14_226,
inference(rat,[],[s749,s937]) ).
cnf(s941,plain,
( spl14_188
| ~ spl14_47
| ~ spl14_44
| ~ spl14_42
| ~ spl14_43
| ~ spl14_158
| ~ spl14_150
| ~ spl14_46 ),
inference(rat,[],[s653,s871,s791,s650,s654,s363,s649,s784,s793,s254,s842,s840,s651,s822,s325,s655,s819,s313,s753,s764,s900,s886,s887,s909,s936,s761,s892,s100,s923,s806,s922,s903,s938,s905,s98,s929]) ).
cnf(s942,plain,
( spl14_203
| ~ spl14_47
| ~ spl14_44
| ~ spl14_42
| ~ spl14_43
| ~ spl14_158
| ~ spl14_150
| ~ spl14_46 ),
inference(rat,[],[s871,s654,s653,s783,s800,s649,s650,s487,s551,s799,s784,s651,s822,s325,s655,s819,s313,s886,s887,s909,s936,s761,s753,s100,s764,s900,s939,s928,s892,s930,s903,s938,s905,s98,s929]) ).
cnf(s943,plain,
( ~ spl14_47
| ~ spl14_44
| ~ spl14_46
| ~ spl14_42
| ~ spl14_43
| ~ spl14_158
| ~ spl14_150 ),
inference(rat,[],[s192,s785,s837,s834,s705,s707,s942,s941,s926,s932]) ).
cnf(s944,plain,
( ~ spl14_142
| ~ spl14_168 ),
inference(rat,[],[s943,s646,s658,s640,s823,s829,s642,s571,s313,s828,s221,s824,s376,s404,s514,s579,s594,s645,s937,s761,s764,s921,s753,s100,s914,s917,s904,s906,s890,s98,s905,s925]) ).
cnf(s945,plain,
( spl14_167
| spl14_137
| ~ spl14_168 ),
inference(rat,[],[s846,s118,s129,s827,s944,s902]) ).
cnf(s946,plain,
( ~ spl14_167
| ~ spl14_168 ),
inference(rat,[],[s829,s341,s375,s226,s831,s385,s585,s222,s221,s337,s380,s819,s508,s590,s665,s944,s98,s905,s912,s904,s906,s903]) ).
cnf(s947,plain,
~ spl14_168,
inference(rat,[],[s831,s857,s856,s945,s946,s944]) ).
cnf(s948,plain,
~ spl14_144,
inference(rat,[],[s566,s907]) ).
cnf(s950,plain,
$false,
inference(rat,[],[s813,s902,s948,s947]) ).
fof(f3886,plain,
$false,
inference(avatar_sat_refutation,[],[s950]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG124+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.07/0.17 % Computer : n009.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.17 % CPULimit : 300
% 0.07/0.17 % WCLimit : 300
% 0.07/0.17 % DateTime : Mon Sep 28 19:31:15 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/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 % (3372369)Will run a generic schedule for satisfiability detection.
% 0.20/0.35 % (3372374)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1506377229_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.35 % (3372375)% WARNING: option uhcvi not known.
% 0.20/0.35 % (3372377)dis+10_1_sil=32000:sp=arity:random_seed=4038180047:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.35 % (3372375)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2833006295:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.35 % (3372376)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=114111675:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.35 % (3372378)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3254106026:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.35 % (3372380)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3889106811:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.35 % (3372379)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2207506111:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.35 % TRYING [1]
% 0.20/0.35 % TRYING [2]
% 0.20/0.35 % TRYING [3]
% 0.20/0.35 % TRYING [4]
% 0.20/0.35 % TRYING [5]
% 0.20/0.35 % TRYING [6]
% 0.20/0.35 % (3372377)Instruction limit reached!
% 0.20/0.35 % (3372377)------------------------------
% 0.20/0.35 % (3372377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (3372377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (3372377)CaDiCaL version: 2.1.3
% 0.20/0.35 % (3372377)Termination reason: Instruction limit
% 0.20/0.35 % (3372377)Termination phase: Saturation
% 0.20/0.35 % (3372377)Time elapsed: 0.051 s
% 0.20/0.35 % (3372377)Peak memory usage: 12 MB
% 0.20/0.35 % (3372377)Instructions burned: 103 (million)
% 0.20/0.35 % (3372378)Instruction limit reached!
% 0.20/0.35 % (3372378)------------------------------
% 0.20/0.35 % (3372378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (3372378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (3372378)CaDiCaL version: 2.1.3
% 0.20/0.35 % (3372378)Termination reason: Instruction limit
% 0.20/0.35 % (3372378)Termination phase: Saturation
% 0.20/0.35 % (3372378)Time elapsed: 0.056 s
% 0.20/0.35 % (3372378)Peak memory usage: 13 MB
% 0.20/0.35 % (3372378)Instructions burned: 116 (million)
% 0.20/0.35 % (3372379)Instruction limit reached!
% 0.20/0.35 % (3372379)------------------------------
% 0.20/0.35 % (3372379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (3372379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (3372379)CaDiCaL version: 2.1.3
% 0.20/0.35 % (3372379)Termination reason: Instruction limit
% 0.20/0.35 % (3372379)Termination phase: Saturation
% 0.20/0.35 % (3372379)Time elapsed: 0.061 s
% 0.20/0.35 % (3372379)Peak memory usage: 13 MB
% 0.20/0.35 % (3372379)Instructions burned: 131 (million)
% 0.20/0.35 % (3372388)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3791363389:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.20/0.35 % TRYING [7]
% 0.20/0.35 % (3372389)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1459882269:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.35 % (3372375) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3372369-3372375"...
% 0.20/0.35 % (3372390)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=1517780149:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.20/0.35 % (3372380)Instruction limit reached!
% 0.20/0.35 % (3372380)------------------------------
% 0.20/0.35 % (3372380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (3372380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (3372380)CaDiCaL version: 2.1.3
% 0.20/0.35 % (3372380)Termination reason: Instruction limit
% 0.20/0.35 % (3372380)Termination phase: Saturation
% 0.20/0.35 % (3372380)Time elapsed: 0.086 s
% 0.20/0.35 % (3372380)Peak memory usage: 14 MB
% 0.20/0.35 % (3372380)Instructions burned: 160 (million)
% 0.20/0.35 % (3372375)...printing done.
% 0.20/0.35 % (3372375)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 % (3372375)------------------------------
% 0.20/0.36 % (3372375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (3372375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (3372375)CaDiCaL version: 2.1.3
% 0.20/0.36 % (3372375)Termination reason: Refutation
% 0.20/0.36 % (3372375)Time elapsed: 0.091 s
% 0.20/0.36 % (3372375)Peak memory usage: 14 MB
% 0.20/0.36 % (3372375)Instructions burned: 182 (million)
% 0.20/0.36 % (3372369)Success in time 0.133 s
% 0.20/0.36 % Vampire exiting
%------------------------------------------------------------------------------