%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG115+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:22:48 AM UTC 2026
% Result : Theorem 0.82s 0.48s
% Output : Refutation 1.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 199
% Syntax : Number of formulae : 1291 ( 212 unt; 183 def)
% Number of atoms : 4875 (2147 equ)
% Maximal formula atoms : 288 ( 3 avg)
% Number of connectives : 5489 (1905 ~;2571 |; 830 &)
% ( 183 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 68 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 249 ( 247 usr; 248 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e10) = e11
| op1(e10,e10) = e12
| op1(e10,e10) = e13 )
& ( op1(e10,e11) = e10
| op1(e10,e11) = e11
| op1(e10,e11) = e12
| op1(e10,e11) = e13 )
& ( op1(e10,e12) = e10
| op1(e10,e12) = e11
| op1(e10,e12) = e12
| op1(e10,e12) = e13 )
& ( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e12
| op1(e10,e13) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 )
& ( op1(e11,e11) = e10
| op1(e11,e11) = e11
| op1(e11,e11) = e12
| op1(e11,e11) = e13 )
& ( op1(e11,e12) = e10
| op1(e11,e12) = e11
| op1(e11,e12) = e12
| op1(e11,e12) = e13 )
& ( op1(e11,e13) = e10
| op1(e11,e13) = e11
| op1(e11,e13) = e12
| op1(e11,e13) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e10) = e11
| op1(e12,e10) = e12
| op1(e12,e10) = e13 )
& ( op1(e12,e11) = e10
| op1(e12,e11) = e11
| op1(e12,e11) = e12
| op1(e12,e11) = e13 )
& ( op1(e12,e12) = e10
| op1(e12,e12) = e11
| op1(e12,e12) = e12
| op1(e12,e12) = e13 )
& ( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12
| op1(e12,e13) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e10) = e11
| op1(e13,e10) = e12
| op1(e13,e10) = e13 )
& ( op1(e13,e11) = e10
| op1(e13,e11) = e11
| op1(e13,e11) = e12
| op1(e13,e11) = e13 )
& ( op1(e13,e12) = e10
| op1(e13,e12) = e11
| op1(e13,e12) = e12
| op1(e13,e12) = e13 )
& ( op1(e13,e13) = e10
| op1(e13,e13) = e11
| op1(e13,e13) = e12
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e11) = e10
| op1(e10,e12) = e10
| op1(e10,e13) = e10 )
& ( op1(e10,e10) = e10
| op1(e11,e10) = e10
| op1(e12,e10) = e10
| op1(e13,e10) = e10 )
& ( op1(e10,e10) = e11
| op1(e10,e11) = e11
| op1(e10,e12) = e11
| op1(e10,e13) = e11 )
& ( op1(e10,e10) = e11
| op1(e11,e10) = e11
| op1(e12,e10) = e11
| op1(e13,e10) = e11 )
& ( op1(e10,e10) = e12
| op1(e10,e11) = e12
| op1(e10,e12) = e12
| op1(e10,e13) = e12 )
& ( op1(e10,e10) = e12
| op1(e11,e10) = e12
| op1(e12,e10) = e12
| op1(e13,e10) = e12 )
& ( op1(e10,e10) = e13
| op1(e10,e11) = e13
| op1(e10,e12) = e13
| op1(e10,e13) = e13 )
& ( op1(e10,e10) = e13
| op1(e11,e10) = e13
| op1(e12,e10) = e13
| op1(e13,e10) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e11) = e10
| op1(e11,e12) = e10
| op1(e11,e13) = e10 )
& ( op1(e10,e11) = e10
| op1(e11,e11) = e10
| op1(e12,e11) = e10
| op1(e13,e11) = e10 )
& ( op1(e11,e10) = e11
| op1(e11,e11) = e11
| op1(e11,e12) = e11
| op1(e11,e13) = e11 )
& ( op1(e10,e11) = e11
| op1(e11,e11) = e11
| op1(e12,e11) = e11
| op1(e13,e11) = e11 )
& ( op1(e11,e10) = e12
| op1(e11,e11) = e12
| op1(e11,e12) = e12
| op1(e11,e13) = e12 )
& ( op1(e10,e11) = e12
| op1(e11,e11) = e12
| op1(e12,e11) = e12
| op1(e13,e11) = e12 )
& ( op1(e11,e10) = e13
| op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e11,e13) = e13 )
& ( op1(e10,e11) = e13
| op1(e11,e11) = e13
| op1(e12,e11) = e13
| op1(e13,e11) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e11) = e10
| op1(e12,e12) = e10
| op1(e12,e13) = e10 )
& ( op1(e10,e12) = e10
| op1(e11,e12) = e10
| op1(e12,e12) = e10
| op1(e13,e12) = e10 )
& ( op1(e12,e10) = e11
| op1(e12,e11) = e11
| op1(e12,e12) = e11
| op1(e12,e13) = e11 )
& ( op1(e10,e12) = e11
| op1(e11,e12) = e11
| op1(e12,e12) = e11
| op1(e13,e12) = e11 )
& ( op1(e12,e10) = e12
| op1(e12,e11) = e12
| op1(e12,e12) = e12
| op1(e12,e13) = e12 )
& ( op1(e10,e12) = e12
| op1(e11,e12) = e12
| op1(e12,e12) = e12
| op1(e13,e12) = e12 )
& ( op1(e12,e10) = e13
| op1(e12,e11) = e13
| op1(e12,e12) = e13
| op1(e12,e13) = e13 )
& ( op1(e10,e12) = e13
| op1(e11,e12) = e13
| op1(e12,e12) = e13
| op1(e13,e12) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10 )
& ( op1(e10,e13) = e10
| op1(e11,e13) = e10
| op1(e12,e13) = e10
| op1(e13,e13) = e10 )
& ( op1(e13,e10) = e11
| op1(e13,e11) = e11
| op1(e13,e12) = e11
| op1(e13,e13) = e11 )
& ( op1(e10,e13) = e11
| op1(e11,e13) = e11
| op1(e12,e13) = e11
| op1(e13,e13) = e11 )
& ( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12
| op1(e13,e13) = e12 )
& ( op1(e10,e13) = e12
| op1(e11,e13) = e12
| op1(e12,e13) = e12
| op1(e13,e13) = e12 )
& ( op1(e13,e10) = e13
| op1(e13,e11) = e13
| op1(e13,e12) = e13
| op1(e13,e13) = e13 )
& ( op1(e10,e13) = e13
| op1(e11,e13) = e13
| op1(e12,e13) = e13
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e20) = e21
| op2(e20,e20) = e22
| op2(e20,e20) = e23 )
& ( op2(e20,e21) = e20
| op2(e20,e21) = e21
| op2(e20,e21) = e22
| op2(e20,e21) = e23 )
& ( op2(e20,e22) = e20
| op2(e20,e22) = e21
| op2(e20,e22) = e22
| op2(e20,e22) = e23 )
& ( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22
| op2(e20,e23) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e20) = e21
| op2(e21,e20) = e22
| op2(e21,e20) = e23 )
& ( op2(e21,e21) = e20
| op2(e21,e21) = e21
| op2(e21,e21) = e22
| op2(e21,e21) = e23 )
& ( op2(e21,e22) = e20
| op2(e21,e22) = e21
| op2(e21,e22) = e22
| op2(e21,e22) = e23 )
& ( op2(e21,e23) = e20
| op2(e21,e23) = e21
| op2(e21,e23) = e22
| op2(e21,e23) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e20) = e21
| op2(e22,e20) = e22
| op2(e22,e20) = e23 )
& ( op2(e22,e21) = e20
| op2(e22,e21) = e21
| op2(e22,e21) = e22
| op2(e22,e21) = e23 )
& ( op2(e22,e22) = e20
| op2(e22,e22) = e21
| op2(e22,e22) = e22
| op2(e22,e22) = e23 )
& ( op2(e22,e23) = e20
| op2(e22,e23) = e21
| op2(e22,e23) = e22
| op2(e22,e23) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e20) = e21
| op2(e23,e20) = e22
| op2(e23,e20) = e23 )
& ( op2(e23,e21) = e20
| op2(e23,e21) = e21
| op2(e23,e21) = e22
| op2(e23,e21) = e23 )
& ( op2(e23,e22) = e20
| op2(e23,e22) = e21
| op2(e23,e22) = e22
| op2(e23,e22) = e23 )
& ( op2(e23,e23) = e20
| op2(e23,e23) = e21
| op2(e23,e23) = e22
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e22) = e20
| op2(e20,e23) = e20 )
& ( op2(e20,e20) = e20
| op2(e21,e20) = e20
| op2(e22,e20) = e20
| op2(e23,e20) = e20 )
& ( op2(e20,e20) = e21
| op2(e20,e21) = e21
| op2(e20,e22) = e21
| op2(e20,e23) = e21 )
& ( op2(e20,e20) = e21
| op2(e21,e20) = e21
| op2(e22,e20) = e21
| op2(e23,e20) = e21 )
& ( op2(e20,e20) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 )
& ( op2(e20,e20) = e22
| op2(e21,e20) = e22
| op2(e22,e20) = e22
| op2(e23,e20) = e22 )
& ( op2(e20,e20) = e23
| op2(e20,e21) = e23
| op2(e20,e22) = e23
| op2(e20,e23) = e23 )
& ( op2(e20,e20) = e23
| op2(e21,e20) = e23
| op2(e22,e20) = e23
| op2(e23,e20) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e21) = e20
| op2(e21,e22) = e20
| op2(e21,e23) = e20 )
& ( op2(e20,e21) = e20
| op2(e21,e21) = e20
| op2(e22,e21) = e20
| op2(e23,e21) = e20 )
& ( op2(e21,e20) = e21
| op2(e21,e21) = e21
| op2(e21,e22) = e21
| op2(e21,e23) = e21 )
& ( op2(e20,e21) = e21
| op2(e21,e21) = e21
| op2(e22,e21) = e21
| op2(e23,e21) = e21 )
& ( op2(e21,e20) = e22
| op2(e21,e21) = e22
| op2(e21,e22) = e22
| op2(e21,e23) = e22 )
& ( op2(e20,e21) = e22
| op2(e21,e21) = e22
| op2(e22,e21) = e22
| op2(e23,e21) = e22 )
& ( op2(e21,e20) = e23
| op2(e21,e21) = e23
| op2(e21,e22) = e23
| op2(e21,e23) = e23 )
& ( op2(e20,e21) = e23
| op2(e21,e21) = e23
| op2(e22,e21) = e23
| op2(e23,e21) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e21) = e20
| op2(e22,e22) = e20
| op2(e22,e23) = e20 )
& ( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e22,e22) = e20
| op2(e23,e22) = e20 )
& ( op2(e22,e20) = e21
| op2(e22,e21) = e21
| op2(e22,e22) = e21
| op2(e22,e23) = e21 )
& ( op2(e20,e22) = e21
| op2(e21,e22) = e21
| op2(e22,e22) = e21
| op2(e23,e22) = e21 )
& ( op2(e22,e20) = e22
| op2(e22,e21) = e22
| op2(e22,e22) = e22
| op2(e22,e23) = e22 )
& ( op2(e20,e22) = e22
| op2(e21,e22) = e22
| op2(e22,e22) = e22
| op2(e23,e22) = e22 )
& ( op2(e22,e20) = e23
| op2(e22,e21) = e23
| op2(e22,e22) = e23
| op2(e22,e23) = e23 )
& ( op2(e20,e22) = e23
| op2(e21,e22) = e23
| op2(e22,e22) = e23
| op2(e23,e22) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e23) = e20 )
& ( op2(e20,e23) = e20
| op2(e21,e23) = e20
| op2(e22,e23) = e20
| op2(e23,e23) = e20 )
& ( op2(e23,e20) = e21
| op2(e23,e21) = e21
| op2(e23,e22) = e21
| op2(e23,e23) = e21 )
& ( op2(e20,e23) = e21
| op2(e21,e23) = e21
| op2(e22,e23) = e21
| op2(e23,e23) = e21 )
& ( op2(e23,e20) = e22
| op2(e23,e21) = e22
| op2(e23,e22) = e22
| op2(e23,e23) = e22 )
& ( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22
| op2(e23,e23) = e22 )
& ( op2(e23,e20) = e23
| op2(e23,e21) = e23
| op2(e23,e22) = e23
| op2(e23,e23) = e23 )
& ( op2(e20,e23) = e23
| op2(e21,e23) = e23
| op2(e22,e23) = e23
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op1(e10,e10) != op1(e11,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e12,e10) != op1(e13,e10)
& op1(e10,e11) != op1(e11,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e12,e11) != op1(e13,e11)
& op1(e10,e12) != op1(e11,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e12,e12) != op1(e13,e12)
& op1(e10,e13) != op1(e11,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e12,e13) != op1(e13,e13)
& op1(e10,e10) != op1(e10,e11)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e12) != op1(e10,e13)
& op1(e11,e10) != op1(e11,e11)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e12) != op1(e11,e13)
& op1(e12,e10) != op1(e12,e11)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e12) != op1(e12,e13)
& op1(e13,e10) != op1(e13,e11)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e12) != op1(e13,e13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( op2(e20,e20) != op2(e21,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e22,e20) != op2(e23,e20)
& op2(e20,e21) != op2(e21,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e22,e21) != op2(e23,e21)
& op2(e20,e22) != op2(e21,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e22,e22) != op2(e23,e22)
& op2(e20,e23) != op2(e21,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e22,e23) != op2(e23,e23)
& op2(e20,e20) != op2(e20,e21)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e22) != op2(e20,e23)
& op2(e21,e20) != op2(e21,e21)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e22) != op2(e21,e23)
& op2(e22,e20) != op2(e22,e21)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e22) != op2(e22,e23)
& op2(e23,e20) != op2(e23,e21)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e22) != op2(e23,e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
fof(f10,axiom,
( ( op1(e10,e10) = e10
| op1(e11,e11) = e10
| op1(e12,e12) = e10
| op1(e13,e13) = e10 )
& ( op1(e10,e10) = e11
| op1(e11,e11) = e11
| op1(e12,e12) = e11
| op1(e13,e13) = e11 )
& ( op1(e10,e10) = e12
| op1(e11,e11) = e12
| op1(e12,e12) = e12
| op1(e13,e13) = e12 )
& ( op1(e10,e10) = e13
| op1(e11,e11) = e13
| op1(e12,e12) = e13
| op1(e13,e13) = e13 )
& ( ( op1(e10,op1(e10,e10)) != e10
& op1(e10,op1(e10,e11)) != e11
& op1(e10,op1(e10,e12)) != e12
& op1(e10,op1(e10,e13)) != e13 )
| ( op1(e11,op1(e11,e10)) != e10
& op1(e11,op1(e11,e11)) != e11
& op1(e11,op1(e11,e12)) != e12
& op1(e11,op1(e11,e13)) != e13 )
| ( op1(e12,op1(e12,e10)) != e10
& op1(e12,op1(e12,e11)) != e11
& op1(e12,op1(e12,e12)) != e12
& op1(e12,op1(e12,e13)) != e13 )
| ( op1(e13,op1(e13,e10)) != e10
& op1(e13,op1(e13,e11)) != e11
& op1(e13,op1(e13,e12)) != e12
& op1(e13,op1(e13,e13)) != e13 ) )
& ( ( op1(e10,e10) = e10
& op1(e10,e10) = e10
& op1(e10,e10) = e10
& op1(e10,e10) = e10 )
| ( op1(e10,e10) = e10
& op1(e10,e10) = e10
& op1(e11,e10) = e10
& op1(e10,e11) = e10 )
| ( op1(e10,e10) = e10
& op1(e10,e10) = e10
& op1(e12,e10) = e10
& op1(e10,e12) = e10 )
| ( op1(e10,e10) = e10
& op1(e10,e10) = e10
& op1(e13,e10) = e10
& op1(e10,e13) = e10 )
| ( op1(e10,e11) = e10
& op1(e11,e10) = e10
& op1(e10,e11) = e11
& op1(e11,e10) = e11 )
| ( op1(e10,e11) = e10
& op1(e11,e10) = e10
& op1(e11,e11) = e11
& op1(e11,e11) = e11 )
| ( op1(e10,e11) = e10
& op1(e11,e10) = e10
& op1(e12,e11) = e11
& op1(e11,e12) = e11 )
| ( op1(e10,e11) = e10
& op1(e11,e10) = e10
& op1(e13,e11) = e11
& op1(e11,e13) = e11 )
| ( op1(e10,e12) = e10
& op1(e12,e10) = e10
& op1(e10,e12) = e12
& op1(e12,e10) = e12 )
| ( op1(e10,e12) = e10
& op1(e12,e10) = e10
& op1(e11,e12) = e12
& op1(e12,e11) = e12 )
| ( op1(e10,e12) = e10
& op1(e12,e10) = e10
& op1(e12,e12) = e12
& op1(e12,e12) = e12 )
| ( op1(e10,e12) = e10
& op1(e12,e10) = e10
& op1(e13,e12) = e12
& op1(e12,e13) = e12 )
| ( op1(e10,e13) = e10
& op1(e13,e10) = e10
& op1(e10,e13) = e13
& op1(e13,e10) = e13 )
| ( op1(e10,e13) = e10
& op1(e13,e10) = e10
& op1(e11,e13) = e13
& op1(e13,e11) = e13 )
| ( op1(e10,e13) = e10
& op1(e13,e10) = e10
& op1(e12,e13) = e13
& op1(e13,e12) = e13 )
| ( op1(e10,e13) = e10
& op1(e13,e10) = e10
& op1(e13,e13) = e13
& op1(e13,e13) = e13 )
| ( op1(e11,e10) = e11
& op1(e10,e11) = e11
& op1(e10,e10) = e10
& op1(e10,e10) = e10 )
| ( op1(e11,e10) = e11
& op1(e10,e11) = e11
& op1(e11,e10) = e10
& op1(e10,e11) = e10 )
| ( op1(e11,e10) = e11
& op1(e10,e11) = e11
& op1(e12,e10) = e10
& op1(e10,e12) = e10 )
| ( op1(e11,e10) = e11
& op1(e10,e11) = e11
& op1(e13,e10) = e10
& op1(e10,e13) = e10 )
| ( op1(e11,e11) = e11
& op1(e11,e11) = e11
& op1(e10,e11) = e11
& op1(e11,e10) = e11 )
| ( op1(e11,e11) = e11
& op1(e11,e11) = e11
& op1(e11,e11) = e11
& op1(e11,e11) = e11 )
| ( op1(e11,e11) = e11
& op1(e11,e11) = e11
& op1(e12,e11) = e11
& op1(e11,e12) = e11 )
| ( op1(e11,e11) = e11
& op1(e11,e11) = e11
& op1(e13,e11) = e11
& op1(e11,e13) = e11 )
| ( op1(e11,e12) = e11
& op1(e12,e11) = e11
& op1(e10,e12) = e12
& op1(e12,e10) = e12 )
| ( op1(e11,e12) = e11
& op1(e12,e11) = e11
& op1(e11,e12) = e12
& op1(e12,e11) = e12 )
| ( op1(e11,e12) = e11
& op1(e12,e11) = e11
& op1(e12,e12) = e12
& op1(e12,e12) = e12 )
| ( op1(e11,e12) = e11
& op1(e12,e11) = e11
& op1(e13,e12) = e12
& op1(e12,e13) = e12 )
| ( op1(e11,e13) = e11
& op1(e13,e11) = e11
& op1(e10,e13) = e13
& op1(e13,e10) = e13 )
| ( op1(e11,e13) = e11
& op1(e13,e11) = e11
& op1(e11,e13) = e13
& op1(e13,e11) = e13 )
| ( op1(e11,e13) = e11
& op1(e13,e11) = e11
& op1(e12,e13) = e13
& op1(e13,e12) = e13 )
| ( op1(e11,e13) = e11
& op1(e13,e11) = e11
& op1(e13,e13) = e13
& op1(e13,e13) = e13 )
| ( op1(e12,e10) = e12
& op1(e10,e12) = e12
& op1(e10,e10) = e10
& op1(e10,e10) = e10 )
| ( op1(e12,e10) = e12
& op1(e10,e12) = e12
& op1(e11,e10) = e10
& op1(e10,e11) = e10 )
| ( op1(e12,e10) = e12
& op1(e10,e12) = e12
& op1(e12,e10) = e10
& op1(e10,e12) = e10 )
| ( op1(e12,e10) = e12
& op1(e10,e12) = e12
& op1(e13,e10) = e10
& op1(e10,e13) = e10 )
| ( op1(e12,e11) = e12
& op1(e11,e12) = e12
& op1(e10,e11) = e11
& op1(e11,e10) = e11 )
| ( op1(e12,e11) = e12
& op1(e11,e12) = e12
& op1(e11,e11) = e11
& op1(e11,e11) = e11 )
| ( op1(e12,e11) = e12
& op1(e11,e12) = e12
& op1(e12,e11) = e11
& op1(e11,e12) = e11 )
| ( op1(e12,e11) = e12
& op1(e11,e12) = e12
& op1(e13,e11) = e11
& op1(e11,e13) = e11 )
| ( op1(e12,e12) = e12
& op1(e12,e12) = e12
& op1(e10,e12) = e12
& op1(e12,e10) = e12 )
| ( op1(e12,e12) = e12
& op1(e12,e12) = e12
& op1(e11,e12) = e12
& op1(e12,e11) = e12 )
| ( op1(e12,e12) = e12
& op1(e12,e12) = e12
& op1(e12,e12) = e12
& op1(e12,e12) = e12 )
| ( op1(e12,e12) = e12
& op1(e12,e12) = e12
& op1(e13,e12) = e12
& op1(e12,e13) = e12 )
| ( op1(e12,e13) = e12
& op1(e13,e12) = e12
& op1(e10,e13) = e13
& op1(e13,e10) = e13 )
| ( op1(e12,e13) = e12
& op1(e13,e12) = e12
& op1(e11,e13) = e13
& op1(e13,e11) = e13 )
| ( op1(e12,e13) = e12
& op1(e13,e12) = e12
& op1(e12,e13) = e13
& op1(e13,e12) = e13 )
| ( op1(e12,e13) = e12
& op1(e13,e12) = e12
& op1(e13,e13) = e13
& op1(e13,e13) = e13 )
| ( op1(e13,e10) = e13
& op1(e10,e13) = e13
& op1(e10,e10) = e10
& op1(e10,e10) = e10 )
| ( op1(e13,e10) = e13
& op1(e10,e13) = e13
& op1(e11,e10) = e10
& op1(e10,e11) = e10 )
| ( op1(e13,e10) = e13
& op1(e10,e13) = e13
& op1(e12,e10) = e10
& op1(e10,e12) = e10 )
| ( op1(e13,e10) = e13
& op1(e10,e13) = e13
& op1(e13,e10) = e10
& op1(e10,e13) = e10 )
| ( op1(e13,e11) = e13
& op1(e11,e13) = e13
& op1(e10,e11) = e11
& op1(e11,e10) = e11 )
| ( op1(e13,e11) = e13
& op1(e11,e13) = e13
& op1(e11,e11) = e11
& op1(e11,e11) = e11 )
| ( op1(e13,e11) = e13
& op1(e11,e13) = e13
& op1(e12,e11) = e11
& op1(e11,e12) = e11 )
| ( op1(e13,e11) = e13
& op1(e11,e13) = e13
& op1(e13,e11) = e11
& op1(e11,e13) = e11 )
| ( op1(e13,e12) = e13
& op1(e12,e13) = e13
& op1(e10,e12) = e12
& op1(e12,e10) = e12 )
| ( op1(e13,e12) = e13
& op1(e12,e13) = e13
& op1(e11,e12) = e12
& op1(e12,e11) = e12 )
| ( op1(e13,e12) = e13
& op1(e12,e13) = e13
& op1(e12,e12) = e12
& op1(e12,e12) = e12 )
| ( op1(e13,e12) = e13
& op1(e12,e13) = e13
& op1(e13,e12) = e12
& op1(e12,e13) = e12 )
| ( op1(e13,e13) = e13
& op1(e13,e13) = e13
& op1(e10,e13) = e13
& op1(e13,e10) = e13 )
| ( op1(e13,e13) = e13
& op1(e13,e13) = e13
& op1(e11,e13) = e13
& op1(e13,e11) = e13 )
| ( op1(e13,e13) = e13
& op1(e13,e13) = e13
& op1(e12,e13) = e13
& op1(e13,e12) = e13 )
| ( op1(e13,e13) = e13
& op1(e13,e13) = e13
& op1(e13,e13) = e13
& op1(e13,e13) = e13 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( ( op2(e20,e20) = e20
| op2(e21,e21) = e20
| op2(e22,e22) = e20
| op2(e23,e23) = e20 )
& ( op2(e20,e20) = e21
| op2(e21,e21) = e21
| op2(e22,e22) = e21
| op2(e23,e23) = e21 )
& ( op2(e20,e20) = e22
| op2(e21,e21) = e22
| op2(e22,e22) = e22
| op2(e23,e23) = e22 )
& ( op2(e20,e20) = e23
| op2(e21,e21) = e23
| op2(e22,e22) = e23
| op2(e23,e23) = e23 )
& ( ( op2(e20,op2(e20,e20)) != e20
& op2(e20,op2(e20,e21)) != e21
& op2(e20,op2(e20,e22)) != e22
& op2(e20,op2(e20,e23)) != e23 )
| ( op2(e21,op2(e21,e20)) != e20
& op2(e21,op2(e21,e21)) != e21
& op2(e21,op2(e21,e22)) != e22
& op2(e21,op2(e21,e23)) != e23 )
| ( op2(e22,op2(e22,e20)) != e20
& op2(e22,op2(e22,e21)) != e21
& op2(e22,op2(e22,e22)) != e22
& op2(e22,op2(e22,e23)) != e23 )
| ( op2(e23,op2(e23,e20)) != e20
& op2(e23,op2(e23,e21)) != e21
& op2(e23,op2(e23,e22)) != e22
& op2(e23,op2(e23,e23)) != e23 ) )
& ( ( op2(e20,e20) = e20
& op2(e20,e20) = e20
& op2(e20,e20) = e20
& op2(e20,e20) = e20 )
| ( op2(e20,e20) = e20
& op2(e20,e20) = e20
& op2(e21,e20) = e20
& op2(e20,e21) = e20 )
| ( op2(e20,e20) = e20
& op2(e20,e20) = e20
& op2(e22,e20) = e20
& op2(e20,e22) = e20 )
| ( op2(e20,e20) = e20
& op2(e20,e20) = e20
& op2(e23,e20) = e20
& op2(e20,e23) = e20 )
| ( op2(e20,e21) = e20
& op2(e21,e20) = e20
& op2(e20,e21) = e21
& op2(e21,e20) = e21 )
| ( op2(e20,e21) = e20
& op2(e21,e20) = e20
& op2(e21,e21) = e21
& op2(e21,e21) = e21 )
| ( op2(e20,e21) = e20
& op2(e21,e20) = e20
& op2(e22,e21) = e21
& op2(e21,e22) = e21 )
| ( op2(e20,e21) = e20
& op2(e21,e20) = e20
& op2(e23,e21) = e21
& op2(e21,e23) = e21 )
| ( op2(e20,e22) = e20
& op2(e22,e20) = e20
& op2(e20,e22) = e22
& op2(e22,e20) = e22 )
| ( op2(e20,e22) = e20
& op2(e22,e20) = e20
& op2(e21,e22) = e22
& op2(e22,e21) = e22 )
| ( op2(e20,e22) = e20
& op2(e22,e20) = e20
& op2(e22,e22) = e22
& op2(e22,e22) = e22 )
| ( op2(e20,e22) = e20
& op2(e22,e20) = e20
& op2(e23,e22) = e22
& op2(e22,e23) = e22 )
| ( op2(e20,e23) = e20
& op2(e23,e20) = e20
& op2(e20,e23) = e23
& op2(e23,e20) = e23 )
| ( op2(e20,e23) = e20
& op2(e23,e20) = e20
& op2(e21,e23) = e23
& op2(e23,e21) = e23 )
| ( op2(e20,e23) = e20
& op2(e23,e20) = e20
& op2(e22,e23) = e23
& op2(e23,e22) = e23 )
| ( op2(e20,e23) = e20
& op2(e23,e20) = e20
& op2(e23,e23) = e23
& op2(e23,e23) = e23 )
| ( op2(e21,e20) = e21
& op2(e20,e21) = e21
& op2(e20,e20) = e20
& op2(e20,e20) = e20 )
| ( op2(e21,e20) = e21
& op2(e20,e21) = e21
& op2(e21,e20) = e20
& op2(e20,e21) = e20 )
| ( op2(e21,e20) = e21
& op2(e20,e21) = e21
& op2(e22,e20) = e20
& op2(e20,e22) = e20 )
| ( op2(e21,e20) = e21
& op2(e20,e21) = e21
& op2(e23,e20) = e20
& op2(e20,e23) = e20 )
| ( op2(e21,e21) = e21
& op2(e21,e21) = e21
& op2(e20,e21) = e21
& op2(e21,e20) = e21 )
| ( op2(e21,e21) = e21
& op2(e21,e21) = e21
& op2(e21,e21) = e21
& op2(e21,e21) = e21 )
| ( op2(e21,e21) = e21
& op2(e21,e21) = e21
& op2(e22,e21) = e21
& op2(e21,e22) = e21 )
| ( op2(e21,e21) = e21
& op2(e21,e21) = e21
& op2(e23,e21) = e21
& op2(e21,e23) = e21 )
| ( op2(e21,e22) = e21
& op2(e22,e21) = e21
& op2(e20,e22) = e22
& op2(e22,e20) = e22 )
| ( op2(e21,e22) = e21
& op2(e22,e21) = e21
& op2(e21,e22) = e22
& op2(e22,e21) = e22 )
| ( op2(e21,e22) = e21
& op2(e22,e21) = e21
& op2(e22,e22) = e22
& op2(e22,e22) = e22 )
| ( op2(e21,e22) = e21
& op2(e22,e21) = e21
& op2(e23,e22) = e22
& op2(e22,e23) = e22 )
| ( op2(e21,e23) = e21
& op2(e23,e21) = e21
& op2(e20,e23) = e23
& op2(e23,e20) = e23 )
| ( op2(e21,e23) = e21
& op2(e23,e21) = e21
& op2(e21,e23) = e23
& op2(e23,e21) = e23 )
| ( op2(e21,e23) = e21
& op2(e23,e21) = e21
& op2(e22,e23) = e23
& op2(e23,e22) = e23 )
| ( op2(e21,e23) = e21
& op2(e23,e21) = e21
& op2(e23,e23) = e23
& op2(e23,e23) = e23 )
| ( op2(e22,e20) = e22
& op2(e20,e22) = e22
& op2(e20,e20) = e20
& op2(e20,e20) = e20 )
| ( op2(e22,e20) = e22
& op2(e20,e22) = e22
& op2(e21,e20) = e20
& op2(e20,e21) = e20 )
| ( op2(e22,e20) = e22
& op2(e20,e22) = e22
& op2(e22,e20) = e20
& op2(e20,e22) = e20 )
| ( op2(e22,e20) = e22
& op2(e20,e22) = e22
& op2(e23,e20) = e20
& op2(e20,e23) = e20 )
| ( op2(e22,e21) = e22
& op2(e21,e22) = e22
& op2(e20,e21) = e21
& op2(e21,e20) = e21 )
| ( op2(e22,e21) = e22
& op2(e21,e22) = e22
& op2(e21,e21) = e21
& op2(e21,e21) = e21 )
| ( op2(e22,e21) = e22
& op2(e21,e22) = e22
& op2(e22,e21) = e21
& op2(e21,e22) = e21 )
| ( op2(e22,e21) = e22
& op2(e21,e22) = e22
& op2(e23,e21) = e21
& op2(e21,e23) = e21 )
| ( op2(e22,e22) = e22
& op2(e22,e22) = e22
& op2(e20,e22) = e22
& op2(e22,e20) = e22 )
| ( op2(e22,e22) = e22
& op2(e22,e22) = e22
& op2(e21,e22) = e22
& op2(e22,e21) = e22 )
| ( op2(e22,e22) = e22
& op2(e22,e22) = e22
& op2(e22,e22) = e22
& op2(e22,e22) = e22 )
| ( op2(e22,e22) = e22
& op2(e22,e22) = e22
& op2(e23,e22) = e22
& op2(e22,e23) = e22 )
| ( op2(e22,e23) = e22
& op2(e23,e22) = e22
& op2(e20,e23) = e23
& op2(e23,e20) = e23 )
| ( op2(e22,e23) = e22
& op2(e23,e22) = e22
& op2(e21,e23) = e23
& op2(e23,e21) = e23 )
| ( op2(e22,e23) = e22
& op2(e23,e22) = e22
& op2(e22,e23) = e23
& op2(e23,e22) = e23 )
| ( op2(e22,e23) = e22
& op2(e23,e22) = e22
& op2(e23,e23) = e23
& op2(e23,e23) = e23 )
| ( op2(e23,e20) = e23
& op2(e20,e23) = e23
& op2(e20,e20) = e20
& op2(e20,e20) = e20 )
| ( op2(e23,e20) = e23
& op2(e20,e23) = e23
& op2(e21,e20) = e20
& op2(e20,e21) = e20 )
| ( op2(e23,e20) = e23
& op2(e20,e23) = e23
& op2(e22,e20) = e20
& op2(e20,e22) = e20 )
| ( op2(e23,e20) = e23
& op2(e20,e23) = e23
& op2(e23,e20) = e20
& op2(e20,e23) = e20 )
| ( op2(e23,e21) = e23
& op2(e21,e23) = e23
& op2(e20,e21) = e21
& op2(e21,e20) = e21 )
| ( op2(e23,e21) = e23
& op2(e21,e23) = e23
& op2(e21,e21) = e21
& op2(e21,e21) = e21 )
| ( op2(e23,e21) = e23
& op2(e21,e23) = e23
& op2(e22,e21) = e21
& op2(e21,e22) = e21 )
| ( op2(e23,e21) = e23
& op2(e21,e23) = e23
& op2(e23,e21) = e21
& op2(e21,e23) = e21 )
| ( op2(e23,e22) = e23
& op2(e22,e23) = e23
& op2(e20,e22) = e22
& op2(e22,e20) = e22 )
| ( op2(e23,e22) = e23
& op2(e22,e23) = e23
& op2(e21,e22) = e22
& op2(e22,e21) = e22 )
| ( op2(e23,e22) = e23
& op2(e22,e23) = e23
& op2(e22,e22) = e22
& op2(e22,e22) = e22 )
| ( op2(e23,e22) = e23
& op2(e22,e23) = e23
& op2(e23,e22) = e22
& op2(e22,e23) = e22 )
| ( op2(e23,e23) = e23
& op2(e23,e23) = e23
& op2(e20,e23) = e23
& op2(e23,e20) = e23 )
| ( op2(e23,e23) = e23
& op2(e23,e23) = e23
& op2(e21,e23) = e23
& op2(e23,e21) = e23 )
| ( op2(e23,e23) = e23
& op2(e23,e23) = e23
& op2(e22,e23) = e23
& op2(e23,e22) = e23 )
| ( op2(e23,e23) = e23
& op2(e23,e23) = e23
& op2(e23,e23) = e23
& op2(e23,e23) = e23 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e10 = op1(op1(e13,e13),op1(op1(e13,e13),e13))
& e11 = op1(e13,e13)
& e12 = op1(op1(e13,e13),e13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e20 = op2(op2(e23,e23),op2(op2(e23,e23),e23))
& e21 = op2(e23,e23)
& e22 = op2(op2(e23,e23),e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( h1(e13) = e20
& h1(e10) = op2(op2(e20,e20),op2(op2(e20,e20),e20))
& h1(e11) = op2(e20,e20)
& h1(e12) = op2(op2(e20,e20),e20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
( h2(e13) = e21
& h2(e10) = op2(op2(e21,e21),op2(op2(e21,e21),e21))
& h2(e11) = op2(e21,e21)
& h2(e12) = op2(op2(e21,e21),e21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
fof(f17,axiom,
( h4(e13) = e23
& h4(e10) = op2(op2(e23,e23),op2(op2(e23,e23),e23))
& h4(e11) = op2(e23,e23)
& h4(e12) = op2(op2(e23,e23),e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
fof(f18,conjecture,
( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f19,negated_conjecture,
~ ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f20,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) ) )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) ) )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) ) )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) ) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f23,plain,
( e13 = op1(e10,e12)
| e12 = op1(e10,e12)
| e11 = op1(e10,e12)
| e10 = op1(e10,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f33,plain,
( e13 = op1(e13,e10)
| e12 = op1(e13,e10)
| e11 = op1(e13,e10)
| e10 = op1(e13,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f41,plain,
( e12 = op1(e10,e13)
| e12 = op1(e10,e12)
| e12 = op1(e10,e11)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f2]) ).
fof(f44,plain,
( e13 = op1(e13,e10)
| e13 = op1(e12,e10)
| e13 = op1(e11,e10)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f2]) ).
fof(f47,plain,
( e11 = op1(e11,e13)
| e11 = op1(e11,e12)
| e11 = op1(e11,e11)
| e11 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f48,plain,
( e11 = op1(e13,e11)
| e11 = op1(e12,e11)
| e11 = op1(e11,e11)
| e11 = op1(e10,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f51,plain,
( e13 = op1(e11,e13)
| e13 = op1(e11,e12)
| e13 = op1(e11,e11)
| e13 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f60,plain,
( e13 = op1(e13,e12)
| e13 = op1(e12,e12)
| e13 = op1(e11,e12)
| e13 = 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(f68,plain,
( e13 = op1(e13,e13)
| e13 = op1(e12,e13)
| e13 = op1(e11,e13)
| e13 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f77,plain,
( e23 = op2(e22,e20)
| e22 = op2(e22,e20)
| e21 = op2(e22,e20)
| e20 = op2(e22,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f89,plain,
( e22 = op2(e20,e23)
| e22 = op2(e20,e22)
| e22 = op2(e20,e21)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f4]) ).
fof(f90,plain,
( e22 = op2(e23,e20)
| e22 = op2(e22,e20)
| e22 = op2(e21,e20)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f4]) ).
fof(f91,plain,
( e23 = op2(e20,e23)
| e23 = op2(e20,e22)
| e23 = op2(e20,e21)
| op2(e20,e20) = e23 ),
inference(cnf_transformation,[],[f4]) ).
fof(f95,plain,
( e21 = op2(e21,e23)
| e21 = op2(e21,e22)
| e21 = op2(e21,e21)
| e21 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f96,plain,
( e21 = op2(e23,e21)
| e21 = op2(e22,e21)
| e21 = op2(e21,e21)
| e21 = op2(e20,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f99,plain,
( e23 = op2(e21,e23)
| e23 = op2(e21,e22)
| e23 = op2(e21,e21)
| e23 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f104,plain,
( e21 = op2(e23,e22)
| e21 = op2(e22,e22)
| e21 = op2(e21,e22)
| e21 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f108,plain,
( e23 = op2(e23,e22)
| e23 = op2(e22,e22)
| e23 = op2(e21,e22)
| e23 = op2(e20,e22) ),
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(f120,plain,
op1(e13,e10) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f121,plain,
op1(e13,e10) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f123,plain,
op1(e12,e12) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f126,plain,
op1(e12,e10) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f134,plain,
op1(e11,e10) != op1(e11,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f135,plain,
op1(e10,e12) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f138,plain,
op1(e10,e10) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f143,plain,
op1(e11,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f148,plain,
op1(e11,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f151,plain,
op1(e10,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f152,plain,
op1(e10,e12) != op1(e11,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
op1(e10,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f165,plain,
op2(e23,e22) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f166,plain,
op2(e23,e21) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f171,plain,
op2(e22,e22) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f175,plain,
op2(e22,e20) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f176,plain,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f178,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f190,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f194,plain,
op2(e20,e23) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f199,plain,
op2(e20,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f206,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f210,plain,
op2(e20,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f211,plain,
op2(e20,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(f223,plain,
e20 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f252,plain,
( e10 = op1(e10,e10)
| ~ sP61 ),
inference(cnf_transformation,[],[f10]) ).
fof(f256,plain,
( e10 = op1(e10,e10)
| ~ sP60 ),
inference(cnf_transformation,[],[f10]) ).
fof(f257,plain,
( e10 = op1(e10,e12)
| ~ sP59 ),
inference(cnf_transformation,[],[f10]) ).
fof(f264,plain,
( e10 = op1(e10,e10)
| ~ sP58 ),
inference(cnf_transformation,[],[f10]) ).
fof(f267,plain,
( e10 = op1(e11,e10)
| ~ sP57 ),
inference(cnf_transformation,[],[f10]) ).
fof(f270,plain,
( e11 = op1(e11,e11)
| ~ sP56 ),
inference(cnf_transformation,[],[f10]) ).
fof(f273,plain,
( e11 = op1(e11,e12)
| ~ sP55 ),
inference(cnf_transformation,[],[f10]) ).
fof(f277,plain,
( e11 = op1(e11,e13)
| ~ sP54 ),
inference(cnf_transformation,[],[f10]) ).
fof(f284,plain,
( e10 = op1(e10,e12)
| ~ sP53 ),
inference(cnf_transformation,[],[f10]) ).
fof(f288,plain,
( e10 = op1(e10,e12)
| ~ sP52 ),
inference(cnf_transformation,[],[f10]) ).
fof(f292,plain,
( e10 = op1(e10,e12)
| ~ sP51 ),
inference(cnf_transformation,[],[f10]) ).
fof(f296,plain,
( e10 = op1(e10,e12)
| ~ sP50 ),
inference(cnf_transformation,[],[f10]) ).
fof(f298,plain,
( e13 = op1(e10,e13)
| ~ sP49 ),
inference(cnf_transformation,[],[f10]) ).
fof(f302,plain,
( e13 = op1(e11,e13)
| ~ sP48 ),
inference(cnf_transformation,[],[f10]) ).
fof(f305,plain,
( e13 = op1(e13,e12)
| ~ sP47 ),
inference(cnf_transformation,[],[f10]) ).
fof(f310,plain,
( e13 = op1(e13,e13)
| ~ sP46 ),
inference(cnf_transformation,[],[f10]) ).
fof(f314,plain,
( e10 = op1(e10,e10)
| ~ sP45 ),
inference(cnf_transformation,[],[f10]) ).
fof(f318,plain,
( e10 = op1(e11,e10)
| ~ sP44 ),
inference(cnf_transformation,[],[f10]) ).
fof(f321,plain,
( e10 = op1(e10,e12)
| ~ sP43 ),
inference(cnf_transformation,[],[f10]) ).
fof(f326,plain,
( e10 = op1(e13,e10)
| ~ sP42 ),
inference(cnf_transformation,[],[f10]) ).
fof(f332,plain,
( e11 = op1(e11,e11)
| ~ sP41 ),
inference(cnf_transformation,[],[f10]) ).
fof(f336,plain,
( e11 = op1(e11,e11)
| ~ sP40 ),
inference(cnf_transformation,[],[f10]) ).
fof(f337,plain,
( e11 = op1(e11,e12)
| ~ sP39 ),
inference(cnf_transformation,[],[f10]) ).
fof(f341,plain,
( e11 = op1(e11,e13)
| ~ sP38 ),
inference(cnf_transformation,[],[f10]) ).
fof(f348,plain,
( e11 = op1(e11,e12)
| ~ sP37 ),
inference(cnf_transformation,[],[f10]) ).
fof(f352,plain,
( e11 = op1(e11,e12)
| ~ sP36 ),
inference(cnf_transformation,[],[f10]) ).
fof(f356,plain,
( e11 = op1(e11,e12)
| ~ sP35 ),
inference(cnf_transformation,[],[f10]) ).
fof(f360,plain,
( e11 = op1(e11,e12)
| ~ sP34 ),
inference(cnf_transformation,[],[f10]) ).
fof(f364,plain,
( e11 = op1(e11,e13)
| ~ sP33 ),
inference(cnf_transformation,[],[f10]) ).
fof(f368,plain,
( e11 = op1(e11,e13)
| ~ sP32 ),
inference(cnf_transformation,[],[f10]) ).
fof(f372,plain,
( e11 = op1(e11,e13)
| ~ sP31 ),
inference(cnf_transformation,[],[f10]) ).
fof(f376,plain,
( e11 = op1(e11,e13)
| ~ sP30 ),
inference(cnf_transformation,[],[f10]) ).
fof(f378,plain,
( e10 = op1(e10,e10)
| ~ sP29 ),
inference(cnf_transformation,[],[f10]) ).
fof(f382,plain,
( e10 = op1(e11,e10)
| ~ sP28 ),
inference(cnf_transformation,[],[f10]) ).
fof(f385,plain,
( e10 = op1(e10,e12)
| ~ sP27 ),
inference(cnf_transformation,[],[f10]) ).
fof(f390,plain,
( e10 = op1(e13,e10)
| ~ sP26 ),
inference(cnf_transformation,[],[f10]) ).
fof(f395,plain,
( e12 = op1(e11,e12)
| ~ sP25 ),
inference(cnf_transformation,[],[f10]) ).
fof(f399,plain,
( e12 = op1(e11,e12)
| ~ sP24 ),
inference(cnf_transformation,[],[f10]) ).
fof(f403,plain,
( e12 = op1(e11,e12)
| ~ sP23 ),
inference(cnf_transformation,[],[f10]) ).
fof(f407,plain,
( e12 = op1(e11,e12)
| ~ sP22 ),
inference(cnf_transformation,[],[f10]) ).
fof(f412,plain,
( e12 = op1(e12,e12)
| ~ sP21 ),
inference(cnf_transformation,[],[f10]) ).
fof(f414,plain,
( e12 = op1(e11,e12)
| ~ sP20 ),
inference(cnf_transformation,[],[f10]) ).
fof(f420,plain,
( e12 = op1(e12,e12)
| ~ sP19 ),
inference(cnf_transformation,[],[f10]) ).
fof(f421,plain,
( e12 = op1(e12,e13)
| ~ sP18 ),
inference(cnf_transformation,[],[f10]) ).
fof(f428,plain,
( e12 = op1(e12,e13)
| ~ sP17 ),
inference(cnf_transformation,[],[f10]) ).
fof(f432,plain,
( e12 = op1(e12,e13)
| ~ sP16 ),
inference(cnf_transformation,[],[f10]) ).
fof(f436,plain,
( e12 = op1(e12,e13)
| ~ sP15 ),
inference(cnf_transformation,[],[f10]) ).
fof(f440,plain,
( e12 = op1(e12,e13)
| ~ sP14 ),
inference(cnf_transformation,[],[f10]) ).
fof(f442,plain,
( e10 = op1(e10,e10)
| ~ sP13 ),
inference(cnf_transformation,[],[f10]) ).
fof(f447,plain,
( e13 = op1(e10,e13)
| ~ sP12 ),
inference(cnf_transformation,[],[f10]) ).
fof(f449,plain,
( e10 = op1(e10,e12)
| ~ sP11 ),
inference(cnf_transformation,[],[f10]) ).
fof(f455,plain,
( e13 = op1(e10,e13)
| ~ sP10 ),
inference(cnf_transformation,[],[f10]) ).
fof(f459,plain,
( e13 = op1(e11,e13)
| ~ sP9 ),
inference(cnf_transformation,[],[f10]) ).
fof(f463,plain,
( e13 = op1(e11,e13)
| ~ sP8 ),
inference(cnf_transformation,[],[f10]) ).
fof(f467,plain,
( e13 = op1(e11,e13)
| ~ sP7 ),
inference(cnf_transformation,[],[f10]) ).
fof(f471,plain,
( e13 = op1(e11,e13)
| ~ sP6 ),
inference(cnf_transformation,[],[f10]) ).
fof(f476,plain,
( e13 = op1(e13,e12)
| ~ sP5 ),
inference(cnf_transformation,[],[f10]) ).
fof(f478,plain,
( e12 = op1(e11,e12)
| ~ sP4 ),
inference(cnf_transformation,[],[f10]) ).
fof(f482,plain,
( e12 = op1(e12,e12)
| ~ sP3 ),
inference(cnf_transformation,[],[f10]) ).
fof(f485,plain,
( e12 = op1(e12,e13)
| ~ sP2 ),
inference(cnf_transformation,[],[f10]) ).
fof(f492,plain,
( e13 = op1(e13,e13)
| ~ sP1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f496,plain,
( e13 = op1(e13,e13)
| ~ sP0 ),
inference(cnf_transformation,[],[f10]) ).
fof(f528,plain,
( e13 = op1(e13,e13)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| sP24
| sP25
| sP26
| sP27
| sP28
| sP29
| sP30
| sP31
| sP32
| sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| sP41
| sP42
| sP43
| sP44
| sP45
| sP46
| sP47
| sP48
| sP49
| sP50
| sP51
| sP52
| sP53
| sP54
| sP55
| sP56
| sP57
| sP58
| sP59
| sP60
| sP61 ),
inference(cnf_transformation,[],[f10]) ).
fof(f529,plain,
( e10 = op1(e13,e13)
| e10 = op1(e12,e12)
| e10 = op1(e11,e11)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f10]) ).
fof(f531,plain,
( e12 = op1(e13,e13)
| e12 = op1(e12,e12)
| e12 = op1(e11,e11)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f10]) ).
fof(f532,plain,
( e13 = op1(e13,e13)
| e13 = op1(e12,e12)
| e13 = op1(e11,e11)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f10]) ).
fof(f821,plain,
( e20 = op2(e23,e23)
| e20 = op2(e22,e22)
| e20 = op2(e21,e21)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f11]) ).
fof(f823,plain,
( e22 = op2(e23,e23)
| e22 = op2(e22,e22)
| e22 = op2(e21,e21)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f11]) ).
fof(f824,plain,
( e23 = op2(e23,e23)
| e23 = op2(e22,e22)
| e23 = op2(e21,e21)
| op2(e20,e20) = e23 ),
inference(cnf_transformation,[],[f11]) ).
fof(f825,plain,
e12 = op1(op1(e13,e13),e13),
inference(cnf_transformation,[],[f12]) ).
fof(f826,plain,
e11 = op1(e13,e13),
inference(cnf_transformation,[],[f12]) ).
fof(f827,plain,
e10 = op1(op1(e13,e13),op1(op1(e13,e13),e13)),
inference(cnf_transformation,[],[f12]) ).
fof(f828,plain,
e22 = op2(op2(e23,e23),e23),
inference(cnf_transformation,[],[f13]) ).
fof(f829,plain,
e21 = op2(e23,e23),
inference(cnf_transformation,[],[f13]) ).
fof(f830,plain,
e20 = op2(op2(e23,e23),op2(op2(e23,e23),e23)),
inference(cnf_transformation,[],[f13]) ).
fof(f834,plain,
e20 = h1(e13),
inference(cnf_transformation,[],[f14]) ).
fof(f835,plain,
op2(op2(e21,e21),e21) = h2(e12),
inference(cnf_transformation,[],[f15]) ).
fof(f836,plain,
op2(e21,e21) = h2(e11),
inference(cnf_transformation,[],[f15]) ).
fof(f837,plain,
h2(e10) = op2(op2(e21,e21),op2(op2(e21,e21),e21)),
inference(cnf_transformation,[],[f15]) ).
fof(f838,plain,
e21 = h2(e13),
inference(cnf_transformation,[],[f15]) ).
fof(f846,plain,
e23 = h4(e13),
inference(cnf_transformation,[],[f17]) ).
fof(f856,plain,
( e20 != h2(e12)
| ~ sP133 ),
inference(cnf_transformation,[],[f20]) ).
fof(f859,plain,
( e21 != h2(e13)
| ~ sP132 ),
inference(cnf_transformation,[],[f20]) ).
fof(f902,plain,
( e23 != h2(e11)
| e22 != h2(e10)
| sP132
| sP133
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(cnf_transformation,[],[f20]) ).
fof(f943,plain,
( e13 = op1(e13,e13)
| ~ sP0
| ~ sP1
| sP2
| ~ sP3
| ~ sP4
| ~ sP5
| ~ sP6
| sP7
| sP8
| ~ sP9
| sP10
| ~ sP11
| ~ sP12
| ~ sP13
| sP14
| ~ sP15
| sP16
| sP17
| ~ sP18
| sP19
| ~ sP20
| sP21
| sP22
| sP23
| sP24
| ~ sP25
| sP26
| ~ sP27
| ~ sP28
| sP29
| ~ sP30
| ~ sP31
| ~ sP32
| sP33
| ~ sP34
| sP35
| ~ sP36
| sP37
| ~ sP38
| sP39
| ~ sP40
| sP41
| ~ sP42
| sP43
| ~ sP44
| sP45
| ~ sP46
| ~ sP47
| ~ sP48
| sP49
| sP50
| ~ sP51
| sP52
| sP53
| ~ sP54
| sP55
| sP56
| sP57
| sP58
| sP59
| ~ sP60
| sP61 ),
inference(consistent_polarity_flipping,[],[f528]) ).
fof(f975,plain,
( e13 = op1(e13,e13)
| sP0 ),
inference(consistent_polarity_flipping,[],[f496]) ).
fof(f979,plain,
( e13 = op1(e13,e13)
| sP1 ),
inference(consistent_polarity_flipping,[],[f492]) ).
fof(f985,plain,
( e12 = op1(e12,e12)
| sP3 ),
inference(consistent_polarity_flipping,[],[f482]) ).
fof(f989,plain,
( e12 = op1(e11,e12)
| sP4 ),
inference(consistent_polarity_flipping,[],[f478]) ).
fof(f991,plain,
( e13 = op1(e13,e12)
| sP5 ),
inference(consistent_polarity_flipping,[],[f476]) ).
fof(f996,plain,
( e13 = op1(e11,e13)
| sP6 ),
inference(consistent_polarity_flipping,[],[f471]) ).
fof(f1000,plain,
( e13 = op1(e11,e13)
| sP9 ),
inference(consistent_polarity_flipping,[],[f459]) ).
fof(f1006,plain,
( e10 = op1(e10,e12)
| sP11 ),
inference(consistent_polarity_flipping,[],[f449]) ).
fof(f1008,plain,
( e13 = op1(e10,e13)
| sP12 ),
inference(consistent_polarity_flipping,[],[f447]) ).
fof(f1013,plain,
( e10 = op1(e10,e10)
| sP13 ),
inference(consistent_polarity_flipping,[],[f442]) ).
fof(f1015,plain,
( e12 = op1(e12,e13)
| sP15 ),
inference(consistent_polarity_flipping,[],[f436]) ).
fof(f1022,plain,
( e12 = op1(e12,e13)
| sP18 ),
inference(consistent_polarity_flipping,[],[f421]) ).
fof(f1025,plain,
( e12 = op1(e11,e12)
| sP20 ),
inference(consistent_polarity_flipping,[],[f414]) ).
fof(f1028,plain,
( e12 = op1(e11,e12)
| sP25 ),
inference(consistent_polarity_flipping,[],[f395]) ).
fof(f1034,plain,
( e10 = op1(e10,e12)
| sP27 ),
inference(consistent_polarity_flipping,[],[f385]) ).
fof(f1037,plain,
( e10 = op1(e11,e10)
| sP28 ),
inference(consistent_polarity_flipping,[],[f382]) ).
fof(f1039,plain,
( e11 = op1(e11,e13)
| sP30 ),
inference(consistent_polarity_flipping,[],[f376]) ).
fof(f1043,plain,
( e11 = op1(e11,e13)
| sP31 ),
inference(consistent_polarity_flipping,[],[f372]) ).
fof(f1047,plain,
( e11 = op1(e11,e13)
| sP32 ),
inference(consistent_polarity_flipping,[],[f368]) ).
fof(f1051,plain,
( e11 = op1(e11,e12)
| sP34 ),
inference(consistent_polarity_flipping,[],[f360]) ).
fof(f1055,plain,
( e11 = op1(e11,e12)
| sP36 ),
inference(consistent_polarity_flipping,[],[f352]) ).
fof(f1062,plain,
( e11 = op1(e11,e13)
| sP38 ),
inference(consistent_polarity_flipping,[],[f341]) ).
fof(f1063,plain,
( e11 = op1(e11,e11)
| sP40 ),
inference(consistent_polarity_flipping,[],[f336]) ).
fof(f1069,plain,
( e10 = op1(e13,e10)
| sP42 ),
inference(consistent_polarity_flipping,[],[f326]) ).
fof(f1073,plain,
( e10 = op1(e11,e10)
| sP44 ),
inference(consistent_polarity_flipping,[],[f318]) ).
fof(f1077,plain,
( e13 = op1(e13,e13)
| sP46 ),
inference(consistent_polarity_flipping,[],[f310]) ).
fof(f1082,plain,
( e13 = op1(e13,e12)
| sP47 ),
inference(consistent_polarity_flipping,[],[f305]) ).
fof(f1085,plain,
( e13 = op1(e11,e13)
| sP48 ),
inference(consistent_polarity_flipping,[],[f302]) ).
fof(f1087,plain,
( e10 = op1(e10,e12)
| sP51 ),
inference(consistent_polarity_flipping,[],[f292]) ).
fof(f1094,plain,
( e11 = op1(e11,e13)
| sP54 ),
inference(consistent_polarity_flipping,[],[f277]) ).
fof(f1095,plain,
( e10 = op1(e10,e10)
| sP60 ),
inference(consistent_polarity_flipping,[],[f256]) ).
fof(f1299,plain,
( e23 != h2(e11)
| e22 != h2(e10)
| ~ sP132
| sP133
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(consistent_polarity_flipping,[],[f902]) ).
fof(f1334,plain,
( e21 != h2(e13)
| sP132 ),
inference(consistent_polarity_flipping,[],[f859]) ).
fof(f1348,definition,
( spl136_2
<=> e20 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl136_2])],[avatar_definition]) ).
fof(f1349,plain,
( e20 = h1(e13)
| ~ spl136_2 ),
inference(avatar_component_clause,[],[f1348]) ).
fof(f1372,definition,
( spl136_7
<=> e21 = h1(e13) ),
introduced(definition,[new_symbols(definition,[spl136_7])],[avatar_definition]) ).
fof(f1373,plain,
( e21 = h1(e13)
| ~ spl136_7 ),
inference(avatar_component_clause,[],[f1372]) ).
fof(f1374,plain,
( e21 != h1(e13)
| spl136_7 ),
inference(avatar_component_clause,[],[f1372]) ).
fof(f1392,definition,
( spl136_11
<=> sP133 ),
introduced(definition,[new_symbols(definition,[spl136_11])],[avatar_definition]) ).
fof(f1401,definition,
( spl136_13
<=> e20 = h2(e12) ),
introduced(definition,[new_symbols(definition,[spl136_13])],[avatar_definition]) ).
fof(f1402,plain,
( e20 = h2(e12)
| ~ spl136_13 ),
inference(avatar_component_clause,[],[f1401]) ).
fof(f1404,plain,
( ~ spl136_11
| ~ spl136_13 ),
inference(avatar_split_clause,[],[f856,f1401,f1392]) ).
fof(f1416,definition,
( spl136_16
<=> sP132 ),
introduced(definition,[new_symbols(definition,[spl136_16])],[avatar_definition]) ).
fof(f1420,definition,
( spl136_17
<=> e21 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl136_17])],[avatar_definition]) ).
fof(f1421,plain,
( e21 = h2(e13)
| ~ spl136_17 ),
inference(avatar_component_clause,[],[f1420]) ).
fof(f1423,plain,
( spl136_16
| ~ spl136_17 ),
inference(avatar_split_clause,[],[f1334,f1420,f1416]) ).
fof(f1492,definition,
( spl136_32
<=> e20 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl136_32])],[avatar_definition]) ).
fof(f1493,plain,
( e20 = h4(e13)
| ~ spl136_32 ),
inference(avatar_component_clause,[],[f1492]) ).
fof(f1494,plain,
( e20 != h4(e13)
| spl136_32 ),
inference(avatar_component_clause,[],[f1492]) ).
fof(f1516,definition,
( spl136_37
<=> e21 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl136_37])],[avatar_definition]) ).
fof(f1517,plain,
( e21 = h4(e13)
| ~ spl136_37 ),
inference(avatar_component_clause,[],[f1516]) ).
fof(f1518,plain,
( e21 != h4(e13)
| spl136_37 ),
inference(avatar_component_clause,[],[f1516]) ).
fof(f1648,definition,
( spl136_65
<=> h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl136_65])],[avatar_definition]) ).
fof(f1650,plain,
( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| spl136_65 ),
inference(avatar_component_clause,[],[f1648]) ).
fof(f1652,definition,
( spl136_66
<=> h2(op1(e10,e11)) = op2(h2(e10),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl136_66])],[avatar_definition]) ).
fof(f1654,plain,
( h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| spl136_66 ),
inference(avatar_component_clause,[],[f1652]) ).
fof(f1656,definition,
( spl136_67
<=> h2(op1(e10,e12)) = op2(h2(e10),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl136_67])],[avatar_definition]) ).
fof(f1658,plain,
( h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| spl136_67 ),
inference(avatar_component_clause,[],[f1656]) ).
fof(f1660,definition,
( spl136_68
<=> h2(op1(e10,e13)) = op2(h2(e10),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl136_68])],[avatar_definition]) ).
fof(f1662,plain,
( h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| spl136_68 ),
inference(avatar_component_clause,[],[f1660]) ).
fof(f1664,definition,
( spl136_69
<=> h2(op1(e11,e10)) = op2(h2(e11),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl136_69])],[avatar_definition]) ).
fof(f1666,plain,
( h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| spl136_69 ),
inference(avatar_component_clause,[],[f1664]) ).
fof(f1668,definition,
( spl136_70
<=> h2(op1(e11,e11)) = op2(h2(e11),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl136_70])],[avatar_definition]) ).
fof(f1670,plain,
( h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| spl136_70 ),
inference(avatar_component_clause,[],[f1668]) ).
fof(f1672,definition,
( spl136_71
<=> h2(op1(e11,e12)) = op2(h2(e11),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl136_71])],[avatar_definition]) ).
fof(f1674,plain,
( h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| spl136_71 ),
inference(avatar_component_clause,[],[f1672]) ).
fof(f1676,definition,
( spl136_72
<=> h2(op1(e11,e13)) = op2(h2(e11),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl136_72])],[avatar_definition]) ).
fof(f1678,plain,
( h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| spl136_72 ),
inference(avatar_component_clause,[],[f1676]) ).
fof(f1680,definition,
( spl136_73
<=> h2(op1(e12,e10)) = op2(h2(e12),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl136_73])],[avatar_definition]) ).
fof(f1682,plain,
( h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| spl136_73 ),
inference(avatar_component_clause,[],[f1680]) ).
fof(f1684,definition,
( spl136_74
<=> h2(op1(e12,e11)) = op2(h2(e12),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl136_74])],[avatar_definition]) ).
fof(f1686,plain,
( h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| spl136_74 ),
inference(avatar_component_clause,[],[f1684]) ).
fof(f1688,definition,
( spl136_75
<=> h2(op1(e12,e12)) = op2(h2(e12),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl136_75])],[avatar_definition]) ).
fof(f1690,plain,
( h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| spl136_75 ),
inference(avatar_component_clause,[],[f1688]) ).
fof(f1692,definition,
( spl136_76
<=> h2(op1(e12,e13)) = op2(h2(e12),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl136_76])],[avatar_definition]) ).
fof(f1694,plain,
( h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| spl136_76 ),
inference(avatar_component_clause,[],[f1692]) ).
fof(f1696,definition,
( spl136_77
<=> h2(op1(e13,e10)) = op2(h2(e13),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl136_77])],[avatar_definition]) ).
fof(f1698,plain,
( h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| spl136_77 ),
inference(avatar_component_clause,[],[f1696]) ).
fof(f1700,definition,
( spl136_78
<=> h2(op1(e13,e11)) = op2(h2(e13),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl136_78])],[avatar_definition]) ).
fof(f1702,plain,
( h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| spl136_78 ),
inference(avatar_component_clause,[],[f1700]) ).
fof(f1704,definition,
( spl136_79
<=> h2(op1(e13,e12)) = op2(h2(e13),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl136_79])],[avatar_definition]) ).
fof(f1706,plain,
( h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| spl136_79 ),
inference(avatar_component_clause,[],[f1704]) ).
fof(f1708,definition,
( spl136_80
<=> h2(op1(e13,e13)) = op2(h2(e13),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl136_80])],[avatar_definition]) ).
fof(f1710,plain,
( h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| spl136_80 ),
inference(avatar_component_clause,[],[f1708]) ).
fof(f1731,definition,
( spl136_85
<=> e22 = h2(e10) ),
introduced(definition,[new_symbols(definition,[spl136_85])],[avatar_definition]) ).
fof(f1732,plain,
( e22 = h2(e10)
| ~ spl136_85 ),
inference(avatar_component_clause,[],[f1731]) ).
fof(f1736,definition,
( spl136_86
<=> e23 = h2(e11) ),
introduced(definition,[new_symbols(definition,[spl136_86])],[avatar_definition]) ).
fof(f1737,plain,
( e23 = h2(e11)
| ~ spl136_86 ),
inference(avatar_component_clause,[],[f1736]) ).
fof(f1742,plain,
( ~ spl136_65
| ~ spl136_66
| ~ spl136_67
| ~ spl136_68
| ~ spl136_69
| ~ spl136_70
| ~ spl136_71
| ~ spl136_72
| ~ spl136_73
| ~ spl136_74
| ~ spl136_75
| ~ spl136_76
| ~ spl136_77
| ~ spl136_78
| ~ spl136_79
| ~ spl136_80
| spl136_11
| ~ spl136_16
| ~ spl136_85
| ~ spl136_86 ),
inference(avatar_split_clause,[],[f1299,f1736,f1731,f1416,f1392,f1708,f1704,f1700,f1696,f1692,f1688,f1684,f1680,f1676,f1672,f1668,f1664,f1660,f1656,f1652,f1648]) ).
fof(f1976,definition,
( spl136_136
<=> e23 = h4(e13) ),
introduced(definition,[new_symbols(definition,[spl136_136])],[avatar_definition]) ).
fof(f1977,plain,
( e23 = h4(e13)
| ~ spl136_136 ),
inference(avatar_component_clause,[],[f1976]) ).
fof(f1983,plain,
spl136_136,
inference(avatar_split_clause,[],[f846,f1976]) ).
fof(f1985,plain,
spl136_17,
inference(avatar_split_clause,[],[f838,f1420]) ).
fof(f1986,plain,
spl136_2,
inference(avatar_split_clause,[],[f834,f1348]) ).
fof(f2040,definition,
( spl136_148
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl136_148])],[avatar_definition]) ).
fof(f2042,plain,
( e20 = op2(e20,e20)
| ~ spl136_148 ),
inference(avatar_component_clause,[],[f2040]) ).
fof(f2073,definition,
( spl136_154
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl136_154])],[avatar_definition]) ).
fof(f2084,definition,
( spl136_156
<=> e20 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl136_156])],[avatar_definition]) ).
fof(f2086,plain,
( e20 = op2(e20,e23)
| ~ spl136_156 ),
inference(avatar_component_clause,[],[f2084]) ).
fof(f2089,definition,
( spl136_157
<=> e20 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl136_157])],[avatar_definition]) ).
fof(f2091,plain,
( e20 = op2(e23,e20)
| ~ spl136_157 ),
inference(avatar_component_clause,[],[f2089]) ).
fof(f2100,definition,
( spl136_159
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl136_159])],[avatar_definition]) ).
fof(f2102,plain,
( e21 = op2(e21,e20)
| ~ spl136_159 ),
inference(avatar_component_clause,[],[f2100]) ).
fof(f2105,definition,
( spl136_160
<=> e21 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl136_160])],[avatar_definition]) ).
fof(f2107,plain,
( e21 = op2(e20,e21)
| ~ spl136_160 ),
inference(avatar_component_clause,[],[f2105]) ).
fof(f2116,definition,
( spl136_162
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl136_162])],[avatar_definition]) ).
fof(f2118,plain,
( e21 = op2(e21,e21)
| ~ spl136_162 ),
inference(avatar_component_clause,[],[f2116]) ).
fof(f2128,definition,
( spl136_164
<=> e21 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl136_164])],[avatar_definition]) ).
fof(f2130,plain,
( e21 = op2(e21,e22)
| ~ spl136_164 ),
inference(avatar_component_clause,[],[f2128]) ).
fof(f2133,definition,
( spl136_165
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl136_165])],[avatar_definition]) ).
fof(f2135,plain,
( e21 = op2(e22,e21)
| ~ spl136_165 ),
inference(avatar_component_clause,[],[f2133]) ).
fof(f2144,definition,
( spl136_167
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl136_167])],[avatar_definition]) ).
fof(f2149,definition,
( spl136_168
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl136_168])],[avatar_definition]) ).
fof(f2160,definition,
( spl136_170
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl136_170])],[avatar_definition]) ).
fof(f2165,definition,
( spl136_171
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl136_171])],[avatar_definition]) ).
fof(f2192,definition,
( spl136_176
<=> e22 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl136_176])],[avatar_definition]) ).
fof(f2194,plain,
( e22 = op2(e22,e22)
| ~ spl136_176 ),
inference(avatar_component_clause,[],[f2192]) ).
fof(f2225,definition,
( spl136_182
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl136_182])],[avatar_definition]) ).
fof(f2227,plain,
( e23 = op2(e20,e23)
| ~ spl136_182 ),
inference(avatar_component_clause,[],[f2225]) ).
fof(f2241,definition,
( spl136_185
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl136_185])],[avatar_definition]) ).
fof(f2243,plain,
( e23 = op2(e21,e23)
| ~ spl136_185 ),
inference(avatar_component_clause,[],[f2241]) ).
fof(f2252,definition,
( spl136_187
<=> e23 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl136_187])],[avatar_definition]) ).
fof(f2254,plain,
( e23 = op2(e23,e22)
| ~ spl136_187 ),
inference(avatar_component_clause,[],[f2252]) ).
fof(f2268,definition,
( spl136_190
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl136_190])],[avatar_definition]) ).
fof(f2270,plain,
( e23 = op2(e23,e23)
| ~ spl136_190 ),
inference(avatar_component_clause,[],[f2268]) ).
fof(f2708,definition,
( spl136_245
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl136_245])],[avatar_definition]) ).
fof(f2710,plain,
( e20 = op2(e21,e21)
| ~ spl136_245 ),
inference(avatar_component_clause,[],[f2708]) ).
fof(f2712,definition,
( spl136_246
<=> e20 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl136_246])],[avatar_definition]) ).
fof(f2714,plain,
( e20 = op2(e22,e22)
| ~ spl136_246 ),
inference(avatar_component_clause,[],[f2712]) ).
fof(f2716,definition,
( spl136_247
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl136_247])],[avatar_definition]) ).
fof(f2718,plain,
( e20 = op2(e23,e23)
| ~ spl136_247 ),
inference(avatar_component_clause,[],[f2716]) ).
fof(f2719,plain,
( spl136_148
| spl136_245
| spl136_246
| spl136_247 ),
inference(avatar_split_clause,[],[f821,f2716,f2712,f2708,f2040]) ).
fof(f2725,definition,
( spl136_249
<=> e21 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl136_249])],[avatar_definition]) ).
fof(f2727,plain,
( e21 = op2(e22,e22)
| ~ spl136_249 ),
inference(avatar_component_clause,[],[f2725]) ).
fof(f2729,definition,
( spl136_250
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl136_250])],[avatar_definition]) ).
fof(f2731,plain,
( e21 = op2(e23,e23)
| ~ spl136_250 ),
inference(avatar_component_clause,[],[f2729]) ).
fof(f2734,definition,
( spl136_251
<=> op2(e20,e20) = e22 ),
introduced(definition,[new_symbols(definition,[spl136_251])],[avatar_definition]) ).
fof(f2736,plain,
( op2(e20,e20) = e22
| ~ spl136_251 ),
inference(avatar_component_clause,[],[f2734]) ).
fof(f2738,definition,
( spl136_252
<=> e22 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl136_252])],[avatar_definition]) ).
fof(f2742,definition,
( spl136_253
<=> e22 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl136_253])],[avatar_definition]) ).
fof(f2744,plain,
( e22 = op2(e23,e23)
| ~ spl136_253 ),
inference(avatar_component_clause,[],[f2742]) ).
fof(f2745,plain,
( spl136_251
| spl136_252
| spl136_176
| spl136_253 ),
inference(avatar_split_clause,[],[f823,f2742,f2192,f2738,f2734]) ).
fof(f2747,definition,
( spl136_254
<=> op2(e20,e20) = e23 ),
introduced(definition,[new_symbols(definition,[spl136_254])],[avatar_definition]) ).
fof(f2749,plain,
( op2(e20,e20) = e23
| ~ spl136_254 ),
inference(avatar_component_clause,[],[f2747]) ).
fof(f2751,definition,
( spl136_255
<=> e23 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl136_255])],[avatar_definition]) ).
fof(f2753,plain,
( e23 = op2(e21,e21)
| ~ spl136_255 ),
inference(avatar_component_clause,[],[f2751]) ).
fof(f2755,definition,
( spl136_256
<=> e23 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl136_256])],[avatar_definition]) ).
fof(f2757,plain,
( e23 = op2(e22,e22)
| ~ spl136_256 ),
inference(avatar_component_clause,[],[f2755]) ).
fof(f2758,plain,
( spl136_254
| spl136_255
| spl136_256
| spl136_190 ),
inference(avatar_split_clause,[],[f824,f2268,f2755,f2751,f2747]) ).
fof(f2808,definition,
( spl136_267
<=> sP61 ),
introduced(definition,[new_symbols(definition,[spl136_267])],[avatar_definition]) ).
fof(f2812,definition,
( spl136_268
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl136_268])],[avatar_definition]) ).
fof(f2814,plain,
( e10 = op1(e10,e10)
| ~ spl136_268 ),
inference(avatar_component_clause,[],[f2812]) ).
fof(f2818,plain,
( ~ spl136_267
| spl136_268 ),
inference(avatar_split_clause,[],[f252,f2812,f2808]) ).
fof(f2820,definition,
( spl136_269
<=> sP60 ),
introduced(definition,[new_symbols(definition,[spl136_269])],[avatar_definition]) ).
fof(f2829,definition,
( spl136_271
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl136_271])],[avatar_definition]) ).
fof(f2831,plain,
( e10 = op1(e11,e10)
| ~ spl136_271 ),
inference(avatar_component_clause,[],[f2829]) ).
fof(f2834,plain,
( spl136_269
| spl136_268 ),
inference(avatar_split_clause,[],[f1095,f2812,f2820]) ).
fof(f2836,definition,
( spl136_272
<=> sP59 ),
introduced(definition,[new_symbols(definition,[spl136_272])],[avatar_definition]) ).
fof(f2840,definition,
( spl136_273
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl136_273])],[avatar_definition]) ).
fof(f2843,plain,
( ~ spl136_272
| spl136_273 ),
inference(avatar_split_clause,[],[f257,f2840,f2836]) ).
fof(f2852,definition,
( spl136_275
<=> sP58 ),
introduced(definition,[new_symbols(definition,[spl136_275])],[avatar_definition]) ).
fof(f2856,definition,
( spl136_276
<=> e10 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl136_276])],[avatar_definition]) ).
fof(f2858,plain,
( e10 = op1(e10,e13)
| ~ spl136_276 ),
inference(avatar_component_clause,[],[f2856]) ).
fof(f2861,definition,
( spl136_277
<=> e10 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl136_277])],[avatar_definition]) ).
fof(f2863,plain,
( e10 = op1(e13,e10)
| ~ spl136_277 ),
inference(avatar_component_clause,[],[f2861]) ).
fof(f2866,plain,
( ~ spl136_275
| spl136_268 ),
inference(avatar_split_clause,[],[f264,f2812,f2852]) ).
fof(f2868,definition,
( spl136_278
<=> sP57 ),
introduced(definition,[new_symbols(definition,[spl136_278])],[avatar_definition]) ).
fof(f2872,definition,
( spl136_279
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl136_279])],[avatar_definition]) ).
fof(f2874,plain,
( e11 = op1(e11,e10)
| ~ spl136_279 ),
inference(avatar_component_clause,[],[f2872]) ).
fof(f2877,definition,
( spl136_280
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl136_280])],[avatar_definition]) ).
fof(f2879,plain,
( e11 = op1(e10,e11)
| ~ spl136_280 ),
inference(avatar_component_clause,[],[f2877]) ).
fof(f2881,plain,
( ~ spl136_278
| spl136_271 ),
inference(avatar_split_clause,[],[f267,f2829,f2868]) ).
fof(f2884,definition,
( spl136_281
<=> sP56 ),
introduced(definition,[new_symbols(definition,[spl136_281])],[avatar_definition]) ).
fof(f2888,definition,
( spl136_282
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl136_282])],[avatar_definition]) ).
fof(f2890,plain,
( e11 = op1(e11,e11)
| ~ spl136_282 ),
inference(avatar_component_clause,[],[f2888]) ).
fof(f2892,plain,
( ~ spl136_281
| spl136_282 ),
inference(avatar_split_clause,[],[f270,f2888,f2884]) ).
fof(f2896,definition,
( spl136_283
<=> sP55 ),
introduced(definition,[new_symbols(definition,[spl136_283])],[avatar_definition]) ).
fof(f2900,definition,
( spl136_284
<=> e11 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl136_284])],[avatar_definition]) ).
fof(f2902,plain,
( e11 = op1(e11,e12)
| ~ spl136_284 ),
inference(avatar_component_clause,[],[f2900]) ).
fof(f2903,plain,
( ~ spl136_283
| spl136_284 ),
inference(avatar_split_clause,[],[f273,f2900,f2896]) ).
fof(f2905,definition,
( spl136_285
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl136_285])],[avatar_definition]) ).
fof(f2907,plain,
( e11 = op1(e12,e11)
| ~ spl136_285 ),
inference(avatar_component_clause,[],[f2905]) ).
fof(f2912,definition,
( spl136_286
<=> sP54 ),
introduced(definition,[new_symbols(definition,[spl136_286])],[avatar_definition]) ).
fof(f2916,definition,
( spl136_287
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl136_287])],[avatar_definition]) ).
fof(f2918,plain,
( e11 = op1(e11,e13)
| ~ spl136_287 ),
inference(avatar_component_clause,[],[f2916]) ).
fof(f2919,plain,
( spl136_286
| spl136_287 ),
inference(avatar_split_clause,[],[f1094,f2916,f2912]) ).
fof(f2921,definition,
( spl136_288
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl136_288])],[avatar_definition]) ).
fof(f2923,plain,
( e11 = op1(e13,e11)
| ~ spl136_288 ),
inference(avatar_component_clause,[],[f2921]) ).
fof(f2928,definition,
( spl136_289
<=> sP53 ),
introduced(definition,[new_symbols(definition,[spl136_289])],[avatar_definition]) ).
fof(f2937,definition,
( spl136_291
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl136_291])],[avatar_definition]) ).
fof(f2942,plain,
( ~ spl136_289
| spl136_273 ),
inference(avatar_split_clause,[],[f284,f2840,f2928]) ).
fof(f2944,definition,
( spl136_292
<=> sP52 ),
introduced(definition,[new_symbols(definition,[spl136_292])],[avatar_definition]) ).
fof(f2953,definition,
( spl136_294
<=> e12 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl136_294])],[avatar_definition]) ).
fof(f2955,plain,
( e12 = op1(e11,e12)
| ~ spl136_294 ),
inference(avatar_component_clause,[],[f2953]) ).
fof(f2958,plain,
( ~ spl136_292
| spl136_273 ),
inference(avatar_split_clause,[],[f288,f2840,f2944]) ).
fof(f2960,definition,
( spl136_295
<=> sP51 ),
introduced(definition,[new_symbols(definition,[spl136_295])],[avatar_definition]) ).
fof(f2964,definition,
( spl136_296
<=> e12 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl136_296])],[avatar_definition]) ).
fof(f2966,plain,
( e12 = op1(e12,e12)
| ~ spl136_296 ),
inference(avatar_component_clause,[],[f2964]) ).
fof(f2970,plain,
( spl136_295
| spl136_273 ),
inference(avatar_split_clause,[],[f1087,f2840,f2960]) ).
fof(f2972,definition,
( spl136_297
<=> sP50 ),
introduced(definition,[new_symbols(definition,[spl136_297])],[avatar_definition]) ).
fof(f2976,definition,
( spl136_298
<=> e12 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl136_298])],[avatar_definition]) ).
fof(f2986,plain,
( ~ spl136_297
| spl136_273 ),
inference(avatar_split_clause,[],[f296,f2840,f2972]) ).
fof(f2988,definition,
( spl136_300
<=> sP49 ),
introduced(definition,[new_symbols(definition,[spl136_300])],[avatar_definition]) ).
fof(f2992,definition,
( spl136_301
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl136_301])],[avatar_definition]) ).
fof(f2994,plain,
( e13 = op1(e13,e10)
| ~ spl136_301 ),
inference(avatar_component_clause,[],[f2992]) ).
fof(f2997,definition,
( spl136_302
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl136_302])],[avatar_definition]) ).
fof(f2999,plain,
( e13 = op1(e10,e13)
| ~ spl136_302 ),
inference(avatar_component_clause,[],[f2997]) ).
fof(f3000,plain,
( ~ spl136_300
| spl136_302 ),
inference(avatar_split_clause,[],[f298,f2997,f2988]) ).
fof(f3004,definition,
( spl136_303
<=> sP48 ),
introduced(definition,[new_symbols(definition,[spl136_303])],[avatar_definition]) ).
fof(f3013,definition,
( spl136_305
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl136_305])],[avatar_definition]) ).
fof(f3015,plain,
( e13 = op1(e11,e13)
| ~ spl136_305 ),
inference(avatar_component_clause,[],[f3013]) ).
fof(f3016,plain,
( spl136_303
| spl136_305 ),
inference(avatar_split_clause,[],[f1085,f3013,f3004]) ).
fof(f3020,definition,
( spl136_306
<=> sP47 ),
introduced(definition,[new_symbols(definition,[spl136_306])],[avatar_definition]) ).
fof(f3024,definition,
( spl136_307
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl136_307])],[avatar_definition]) ).
fof(f3026,plain,
( e13 = op1(e13,e12)
| ~ spl136_307 ),
inference(avatar_component_clause,[],[f3024]) ).
fof(f3027,plain,
( spl136_306
| spl136_307 ),
inference(avatar_split_clause,[],[f1082,f3024,f3020]) ).
fof(f3029,definition,
( spl136_308
<=> e13 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl136_308])],[avatar_definition]) ).
fof(f3031,plain,
( e13 = op1(e12,e13)
| ~ spl136_308 ),
inference(avatar_component_clause,[],[f3029]) ).
fof(f3036,definition,
( spl136_309
<=> sP46 ),
introduced(definition,[new_symbols(definition,[spl136_309])],[avatar_definition]) ).
fof(f3040,definition,
( spl136_310
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl136_310])],[avatar_definition]) ).
fof(f3042,plain,
( e13 = op1(e13,e13)
| ~ spl136_310 ),
inference(avatar_component_clause,[],[f3040]) ).
fof(f3044,plain,
( spl136_309
| spl136_310 ),
inference(avatar_split_clause,[],[f1077,f3040,f3036]) ).
fof(f3048,definition,
( spl136_311
<=> sP45 ),
introduced(definition,[new_symbols(definition,[spl136_311])],[avatar_definition]) ).
fof(f3052,plain,
( ~ spl136_311
| spl136_268 ),
inference(avatar_split_clause,[],[f314,f2812,f3048]) ).
fof(f3056,definition,
( spl136_312
<=> sP44 ),
introduced(definition,[new_symbols(definition,[spl136_312])],[avatar_definition]) ).
fof(f3060,plain,
( spl136_312
| spl136_271 ),
inference(avatar_split_clause,[],[f1073,f2829,f3056]) ).
fof(f3064,definition,
( spl136_313
<=> sP43 ),
introduced(definition,[new_symbols(definition,[spl136_313])],[avatar_definition]) ).
fof(f3067,plain,
( ~ spl136_313
| spl136_273 ),
inference(avatar_split_clause,[],[f321,f2840,f3064]) ).
fof(f3072,definition,
( spl136_314
<=> sP42 ),
introduced(definition,[new_symbols(definition,[spl136_314])],[avatar_definition]) ).
fof(f3076,plain,
( spl136_314
| spl136_277 ),
inference(avatar_split_clause,[],[f1069,f2861,f3072]) ).
fof(f3080,definition,
( spl136_315
<=> sP41 ),
introduced(definition,[new_symbols(definition,[spl136_315])],[avatar_definition]) ).
fof(f3086,plain,
( ~ spl136_315
| spl136_282 ),
inference(avatar_split_clause,[],[f332,f2888,f3080]) ).
fof(f3088,definition,
( spl136_316
<=> sP40 ),
introduced(definition,[new_symbols(definition,[spl136_316])],[avatar_definition]) ).
fof(f3094,plain,
( spl136_316
| spl136_282 ),
inference(avatar_split_clause,[],[f1063,f2888,f3088]) ).
fof(f3096,definition,
( spl136_317
<=> sP39 ),
introduced(definition,[new_symbols(definition,[spl136_317])],[avatar_definition]) ).
fof(f3099,plain,
( ~ spl136_317
| spl136_284 ),
inference(avatar_split_clause,[],[f337,f2900,f3096]) ).
fof(f3104,definition,
( spl136_318
<=> sP38 ),
introduced(definition,[new_symbols(definition,[spl136_318])],[avatar_definition]) ).
fof(f3107,plain,
( spl136_318
| spl136_287 ),
inference(avatar_split_clause,[],[f1062,f2916,f3104]) ).
fof(f3112,definition,
( spl136_319
<=> sP37 ),
introduced(definition,[new_symbols(definition,[spl136_319])],[avatar_definition]) ).
fof(f3118,plain,
( ~ spl136_319
| spl136_284 ),
inference(avatar_split_clause,[],[f348,f2900,f3112]) ).
fof(f3120,definition,
( spl136_320
<=> sP36 ),
introduced(definition,[new_symbols(definition,[spl136_320])],[avatar_definition]) ).
fof(f3126,plain,
( spl136_320
| spl136_284 ),
inference(avatar_split_clause,[],[f1055,f2900,f3120]) ).
fof(f3128,definition,
( spl136_321
<=> sP35 ),
introduced(definition,[new_symbols(definition,[spl136_321])],[avatar_definition]) ).
fof(f3134,plain,
( ~ spl136_321
| spl136_284 ),
inference(avatar_split_clause,[],[f356,f2900,f3128]) ).
fof(f3136,definition,
( spl136_322
<=> sP34 ),
introduced(definition,[new_symbols(definition,[spl136_322])],[avatar_definition]) ).
fof(f3142,plain,
( spl136_322
| spl136_284 ),
inference(avatar_split_clause,[],[f1051,f2900,f3136]) ).
fof(f3144,definition,
( spl136_323
<=> sP33 ),
introduced(definition,[new_symbols(definition,[spl136_323])],[avatar_definition]) ).
fof(f3150,plain,
( ~ spl136_323
| spl136_287 ),
inference(avatar_split_clause,[],[f364,f2916,f3144]) ).
fof(f3152,definition,
( spl136_324
<=> sP32 ),
introduced(definition,[new_symbols(definition,[spl136_324])],[avatar_definition]) ).
fof(f3158,plain,
( spl136_324
| spl136_287 ),
inference(avatar_split_clause,[],[f1047,f2916,f3152]) ).
fof(f3160,definition,
( spl136_325
<=> sP31 ),
introduced(definition,[new_symbols(definition,[spl136_325])],[avatar_definition]) ).
fof(f3166,plain,
( spl136_325
| spl136_287 ),
inference(avatar_split_clause,[],[f1043,f2916,f3160]) ).
fof(f3168,definition,
( spl136_326
<=> sP30 ),
introduced(definition,[new_symbols(definition,[spl136_326])],[avatar_definition]) ).
fof(f3174,plain,
( spl136_326
| spl136_287 ),
inference(avatar_split_clause,[],[f1039,f2916,f3168]) ).
fof(f3176,definition,
( spl136_327
<=> sP29 ),
introduced(definition,[new_symbols(definition,[spl136_327])],[avatar_definition]) ).
fof(f3180,plain,
( ~ spl136_327
| spl136_268 ),
inference(avatar_split_clause,[],[f378,f2812,f3176]) ).
fof(f3184,definition,
( spl136_328
<=> sP28 ),
introduced(definition,[new_symbols(definition,[spl136_328])],[avatar_definition]) ).
fof(f3188,plain,
( spl136_328
| spl136_271 ),
inference(avatar_split_clause,[],[f1037,f2829,f3184]) ).
fof(f3192,definition,
( spl136_329
<=> sP27 ),
introduced(definition,[new_symbols(definition,[spl136_329])],[avatar_definition]) ).
fof(f3195,plain,
( spl136_329
| spl136_273 ),
inference(avatar_split_clause,[],[f1034,f2840,f3192]) ).
fof(f3200,definition,
( spl136_330
<=> sP26 ),
introduced(definition,[new_symbols(definition,[spl136_330])],[avatar_definition]) ).
fof(f3204,plain,
( ~ spl136_330
| spl136_277 ),
inference(avatar_split_clause,[],[f390,f2861,f3200]) ).
fof(f3208,definition,
( spl136_331
<=> sP25 ),
introduced(definition,[new_symbols(definition,[spl136_331])],[avatar_definition]) ).
fof(f3213,plain,
( spl136_331
| spl136_294 ),
inference(avatar_split_clause,[],[f1028,f2953,f3208]) ).
fof(f3216,definition,
( spl136_332
<=> sP24 ),
introduced(definition,[new_symbols(definition,[spl136_332])],[avatar_definition]) ).
fof(f3221,plain,
( ~ spl136_332
| spl136_294 ),
inference(avatar_split_clause,[],[f399,f2953,f3216]) ).
fof(f3224,definition,
( spl136_333
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl136_333])],[avatar_definition]) ).
fof(f3229,plain,
( ~ spl136_333
| spl136_294 ),
inference(avatar_split_clause,[],[f403,f2953,f3224]) ).
fof(f3232,definition,
( spl136_334
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl136_334])],[avatar_definition]) ).
fof(f3237,plain,
( ~ spl136_334
| spl136_294 ),
inference(avatar_split_clause,[],[f407,f2953,f3232]) ).
fof(f3240,definition,
( spl136_335
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl136_335])],[avatar_definition]) ).
fof(f3246,plain,
( ~ spl136_335
| spl136_296 ),
inference(avatar_split_clause,[],[f412,f2964,f3240]) ).
fof(f3248,definition,
( spl136_336
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl136_336])],[avatar_definition]) ).
fof(f3252,plain,
( spl136_336
| spl136_294 ),
inference(avatar_split_clause,[],[f1025,f2953,f3248]) ).
fof(f3256,definition,
( spl136_337
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl136_337])],[avatar_definition]) ).
fof(f3262,plain,
( ~ spl136_337
| spl136_296 ),
inference(avatar_split_clause,[],[f420,f2964,f3256]) ).
fof(f3264,definition,
( spl136_338
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl136_338])],[avatar_definition]) ).
fof(f3267,plain,
( spl136_338
| spl136_298 ),
inference(avatar_split_clause,[],[f1022,f2976,f3264]) ).
fof(f3272,definition,
( spl136_339
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl136_339])],[avatar_definition]) ).
fof(f3278,plain,
( ~ spl136_339
| spl136_298 ),
inference(avatar_split_clause,[],[f428,f2976,f3272]) ).
fof(f3280,definition,
( spl136_340
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl136_340])],[avatar_definition]) ).
fof(f3286,plain,
( ~ spl136_340
| spl136_298 ),
inference(avatar_split_clause,[],[f432,f2976,f3280]) ).
fof(f3288,definition,
( spl136_341
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl136_341])],[avatar_definition]) ).
fof(f3294,plain,
( spl136_341
| spl136_298 ),
inference(avatar_split_clause,[],[f1015,f2976,f3288]) ).
fof(f3296,definition,
( spl136_342
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl136_342])],[avatar_definition]) ).
fof(f3302,plain,
( ~ spl136_342
| spl136_298 ),
inference(avatar_split_clause,[],[f440,f2976,f3296]) ).
fof(f3304,definition,
( spl136_343
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl136_343])],[avatar_definition]) ).
fof(f3308,plain,
( spl136_343
| spl136_268 ),
inference(avatar_split_clause,[],[f1013,f2812,f3304]) ).
fof(f3312,definition,
( spl136_344
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl136_344])],[avatar_definition]) ).
fof(f3317,plain,
( spl136_344
| spl136_302 ),
inference(avatar_split_clause,[],[f1008,f2997,f3312]) ).
fof(f3320,definition,
( spl136_345
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl136_345])],[avatar_definition]) ).
fof(f3323,plain,
( spl136_345
| spl136_273 ),
inference(avatar_split_clause,[],[f1006,f2840,f3320]) ).
fof(f3328,definition,
( spl136_346
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl136_346])],[avatar_definition]) ).
fof(f3333,plain,
( ~ spl136_346
| spl136_302 ),
inference(avatar_split_clause,[],[f455,f2997,f3328]) ).
fof(f3336,definition,
( spl136_347
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl136_347])],[avatar_definition]) ).
fof(f3341,plain,
( spl136_347
| spl136_305 ),
inference(avatar_split_clause,[],[f1000,f3013,f3336]) ).
fof(f3344,definition,
( spl136_348
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl136_348])],[avatar_definition]) ).
fof(f3349,plain,
( ~ spl136_348
| spl136_305 ),
inference(avatar_split_clause,[],[f463,f3013,f3344]) ).
fof(f3352,definition,
( spl136_349
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl136_349])],[avatar_definition]) ).
fof(f3357,plain,
( ~ spl136_349
| spl136_305 ),
inference(avatar_split_clause,[],[f467,f3013,f3352]) ).
fof(f3360,definition,
( spl136_350
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl136_350])],[avatar_definition]) ).
fof(f3365,plain,
( spl136_350
| spl136_305 ),
inference(avatar_split_clause,[],[f996,f3013,f3360]) ).
fof(f3368,definition,
( spl136_351
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl136_351])],[avatar_definition]) ).
fof(f3374,plain,
( spl136_351
| spl136_307 ),
inference(avatar_split_clause,[],[f991,f3024,f3368]) ).
fof(f3376,definition,
( spl136_352
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl136_352])],[avatar_definition]) ).
fof(f3380,plain,
( spl136_352
| spl136_294 ),
inference(avatar_split_clause,[],[f989,f2953,f3376]) ).
fof(f3384,definition,
( spl136_353
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl136_353])],[avatar_definition]) ).
fof(f3388,plain,
( spl136_353
| spl136_296 ),
inference(avatar_split_clause,[],[f985,f2964,f3384]) ).
fof(f3392,definition,
( spl136_354
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl136_354])],[avatar_definition]) ).
fof(f3395,plain,
( ~ spl136_354
| spl136_298 ),
inference(avatar_split_clause,[],[f485,f2976,f3392]) ).
fof(f3400,definition,
( spl136_355
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl136_355])],[avatar_definition]) ).
fof(f3406,plain,
( spl136_355
| spl136_310 ),
inference(avatar_split_clause,[],[f979,f3040,f3400]) ).
fof(f3408,definition,
( spl136_356
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl136_356])],[avatar_definition]) ).
fof(f3414,plain,
( spl136_356
| spl136_310 ),
inference(avatar_split_clause,[],[f975,f3040,f3408]) ).
fof(f3478,plain,
( spl136_267
| ~ spl136_269
| spl136_272
| spl136_275
| spl136_278
| spl136_281
| spl136_283
| ~ spl136_286
| spl136_289
| spl136_292
| ~ spl136_295
| spl136_297
| spl136_300
| ~ spl136_303
| ~ spl136_306
| ~ spl136_309
| spl136_311
| ~ spl136_312
| spl136_313
| ~ spl136_314
| spl136_315
| ~ spl136_316
| spl136_317
| ~ spl136_318
| spl136_319
| ~ spl136_320
| spl136_321
| ~ spl136_322
| spl136_323
| ~ spl136_324
| ~ spl136_325
| ~ spl136_326
| spl136_327
| ~ spl136_328
| ~ spl136_329
| spl136_330
| ~ spl136_331
| spl136_332
| spl136_333
| spl136_334
| spl136_335
| ~ spl136_336
| spl136_337
| ~ spl136_338
| spl136_339
| spl136_340
| ~ spl136_341
| spl136_342
| ~ spl136_343
| ~ spl136_344
| ~ spl136_345
| spl136_346
| ~ spl136_347
| spl136_348
| spl136_349
| ~ spl136_350
| ~ spl136_351
| ~ spl136_352
| ~ spl136_353
| spl136_354
| ~ spl136_355
| ~ spl136_356
| spl136_310 ),
inference(avatar_split_clause,[],[f943,f3040,f3408,f3400,f3392,f3384,f3376,f3368,f3360,f3352,f3344,f3336,f3328,f3320,f3312,f3304,f3296,f3288,f3280,f3272,f3264,f3256,f3248,f3240,f3232,f3224,f3216,f3208,f3200,f3192,f3184,f3176,f3168,f3160,f3152,f3144,f3136,f3128,f3120,f3112,f3104,f3096,f3088,f3080,f3072,f3064,f3056,f3048,f3036,f3020,f3004,f2988,f2972,f2960,f2944,f2928,f2912,f2896,f2884,f2868,f2852,f2836,f2820,f2808]) ).
fof(f3480,definition,
( spl136_365
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl136_365])],[avatar_definition]) ).
fof(f3482,plain,
( e10 = op1(e11,e11)
| ~ spl136_365 ),
inference(avatar_component_clause,[],[f3480]) ).
fof(f3484,definition,
( spl136_366
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl136_366])],[avatar_definition]) ).
fof(f3486,plain,
( e10 = op1(e12,e12)
| ~ spl136_366 ),
inference(avatar_component_clause,[],[f3484]) ).
fof(f3488,definition,
( spl136_367
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl136_367])],[avatar_definition]) ).
fof(f3490,plain,
( e10 = op1(e13,e13)
| ~ spl136_367 ),
inference(avatar_component_clause,[],[f3488]) ).
fof(f3491,plain,
( spl136_268
| spl136_365
| spl136_366
| spl136_367 ),
inference(avatar_split_clause,[],[f529,f3488,f3484,f3480,f2812]) ).
fof(f3501,definition,
( spl136_370
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl136_370])],[avatar_definition]) ).
fof(f3503,plain,
( e11 = op1(e13,e13)
| ~ spl136_370 ),
inference(avatar_component_clause,[],[f3501]) ).
fof(f3506,definition,
( spl136_371
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[spl136_371])],[avatar_definition]) ).
fof(f3508,plain,
( op1(e10,e10) = e12
| ~ spl136_371 ),
inference(avatar_component_clause,[],[f3506]) ).
fof(f3510,definition,
( spl136_372
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl136_372])],[avatar_definition]) ).
fof(f3512,plain,
( e12 = op1(e11,e11)
| ~ spl136_372 ),
inference(avatar_component_clause,[],[f3510]) ).
fof(f3514,definition,
( spl136_373
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl136_373])],[avatar_definition]) ).
fof(f3516,plain,
( e12 = op1(e13,e13)
| ~ spl136_373 ),
inference(avatar_component_clause,[],[f3514]) ).
fof(f3517,plain,
( spl136_371
| spl136_372
| spl136_296
| spl136_373 ),
inference(avatar_split_clause,[],[f531,f3514,f2964,f3510,f3506]) ).
fof(f3519,definition,
( spl136_374
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[spl136_374])],[avatar_definition]) ).
fof(f3521,plain,
( op1(e10,e10) = e13
| ~ spl136_374 ),
inference(avatar_component_clause,[],[f3519]) ).
fof(f3523,definition,
( spl136_375
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl136_375])],[avatar_definition]) ).
fof(f3525,plain,
( e13 = op1(e11,e11)
| ~ spl136_375 ),
inference(avatar_component_clause,[],[f3523]) ).
fof(f3527,definition,
( spl136_376
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl136_376])],[avatar_definition]) ).
fof(f3529,plain,
( e13 = op1(e12,e12)
| ~ spl136_376 ),
inference(avatar_component_clause,[],[f3527]) ).
fof(f3530,plain,
( spl136_374
| spl136_375
| spl136_376
| spl136_310 ),
inference(avatar_split_clause,[],[f532,f3040,f3527,f3523,f3519]) ).
fof(f3534,definition,
( spl136_377
<=> e21 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl136_377])],[avatar_definition]) ).
fof(f3536,plain,
( e21 = op2(e20,e22)
| ~ spl136_377 ),
inference(avatar_component_clause,[],[f3534]) ).
fof(f3543,definition,
( spl136_379
<=> e21 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl136_379])],[avatar_definition]) ).
fof(f3545,plain,
( e21 = op2(e22,e20)
| ~ spl136_379 ),
inference(avatar_component_clause,[],[f3543]) ).
fof(f3552,definition,
( spl136_381
<=> e22 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl136_381])],[avatar_definition]) ).
fof(f3554,plain,
( e22 = op2(e20,e21)
| ~ spl136_381 ),
inference(avatar_component_clause,[],[f3552]) ).
fof(f3556,definition,
( spl136_382
<=> e22 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl136_382])],[avatar_definition]) ).
fof(f3558,plain,
( e22 = op2(e20,e23)
| ~ spl136_382 ),
inference(avatar_component_clause,[],[f3556]) ).
fof(f3559,plain,
( spl136_251
| spl136_381
| spl136_171
| spl136_382 ),
inference(avatar_split_clause,[],[f89,f3556,f2165,f3552,f2734]) ).
fof(f3561,definition,
( spl136_383
<=> e22 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl136_383])],[avatar_definition]) ).
fof(f3563,plain,
( e22 = op2(e21,e20)
| ~ spl136_383 ),
inference(avatar_component_clause,[],[f3561]) ).
fof(f3565,definition,
( spl136_384
<=> e22 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl136_384])],[avatar_definition]) ).
fof(f3567,plain,
( e22 = op2(e23,e20)
| ~ spl136_384 ),
inference(avatar_component_clause,[],[f3565]) ).
fof(f3568,plain,
( spl136_251
| spl136_383
| spl136_170
| spl136_384 ),
inference(avatar_split_clause,[],[f90,f3565,f2160,f3561,f2734]) ).
fof(f3570,definition,
( spl136_385
<=> e23 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl136_385])],[avatar_definition]) ).
fof(f3572,plain,
( e23 = op2(e20,e21)
| ~ spl136_385 ),
inference(avatar_component_clause,[],[f3570]) ).
fof(f3574,definition,
( spl136_386
<=> e23 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl136_386])],[avatar_definition]) ).
fof(f3576,plain,
( e23 = op2(e20,e22)
| ~ spl136_386 ),
inference(avatar_component_clause,[],[f3574]) ).
fof(f3577,plain,
( spl136_254
| spl136_385
| spl136_386
| spl136_182 ),
inference(avatar_split_clause,[],[f91,f2225,f3574,f3570,f2747]) ).
fof(f3579,definition,
( spl136_387
<=> e23 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl136_387])],[avatar_definition]) ).
fof(f3581,plain,
( e23 = op2(e21,e20)
| ~ spl136_387 ),
inference(avatar_component_clause,[],[f3579]) ).
fof(f3583,definition,
( spl136_388
<=> e23 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl136_388])],[avatar_definition]) ).
fof(f3588,definition,
( spl136_389
<=> e20 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl136_389])],[avatar_definition]) ).
fof(f3590,plain,
( e20 = op2(e21,e22)
| ~ spl136_389 ),
inference(avatar_component_clause,[],[f3588]) ).
fof(f3592,definition,
( spl136_390
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl136_390])],[avatar_definition]) ).
fof(f3594,plain,
( e20 = op2(e21,e23)
| ~ spl136_390 ),
inference(avatar_component_clause,[],[f3592]) ).
fof(f3601,definition,
( spl136_392
<=> e20 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl136_392])],[avatar_definition]) ).
fof(f3603,plain,
( e20 = op2(e23,e21)
| ~ spl136_392 ),
inference(avatar_component_clause,[],[f3601]) ).
fof(f3605,plain,
( spl136_159
| spl136_162
| spl136_164
| spl136_167 ),
inference(avatar_split_clause,[],[f95,f2144,f2128,f2116,f2100]) ).
fof(f3606,plain,
( spl136_160
| spl136_162
| spl136_165
| spl136_168 ),
inference(avatar_split_clause,[],[f96,f2149,f2133,f2116,f2105]) ).
fof(f3608,definition,
( spl136_393
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl136_393])],[avatar_definition]) ).
fof(f3610,plain,
( e22 = op2(e21,e23)
| ~ spl136_393 ),
inference(avatar_component_clause,[],[f3608]) ).
fof(f3618,definition,
( spl136_395
<=> e23 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl136_395])],[avatar_definition]) ).
fof(f3620,plain,
( e23 = op2(e21,e22)
| ~ spl136_395 ),
inference(avatar_component_clause,[],[f3618]) ).
fof(f3621,plain,
( spl136_387
| spl136_255
| spl136_395
| spl136_185 ),
inference(avatar_split_clause,[],[f99,f2241,f3618,f2751,f3579]) ).
fof(f3628,definition,
( spl136_397
<=> e20 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl136_397])],[avatar_definition]) ).
fof(f3630,plain,
( e20 = op2(e22,e23)
| ~ spl136_397 ),
inference(avatar_component_clause,[],[f3628]) ).
fof(f3633,definition,
( spl136_398
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl136_398])],[avatar_definition]) ).
fof(f3635,plain,
( e20 = op2(e23,e22)
| ~ spl136_398 ),
inference(avatar_component_clause,[],[f3633]) ).
fof(f3643,definition,
( spl136_400
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl136_400])],[avatar_definition]) ).
fof(f3646,plain,
( spl136_377
| spl136_164
| spl136_249
| spl136_400 ),
inference(avatar_split_clause,[],[f104,f3643,f2725,f2128,f3534]) ).
fof(f3650,plain,
( spl136_386
| spl136_395
| spl136_256
| spl136_187 ),
inference(avatar_split_clause,[],[f108,f2252,f2755,f3618,f3574]) ).
fof(f3651,plain,
( spl136_157
| spl136_392
| spl136_398
| spl136_247 ),
inference(avatar_split_clause,[],[f109,f2716,f3633,f3601,f2089]) ).
fof(f3652,plain,
( spl136_156
| spl136_390
| spl136_397
| spl136_247 ),
inference(avatar_split_clause,[],[f110,f2716,f3628,f3592,f2084]) ).
fof(f3667,plain,
( spl136_154
| spl136_379
| spl136_170
| spl136_388 ),
inference(avatar_split_clause,[],[f77,f3583,f2160,f3543,f2073]) ).
fof(f3678,definition,
( spl136_401
<=> e11 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl136_401])],[avatar_definition]) ).
fof(f3680,plain,
( e11 = op1(e10,e12)
| ~ spl136_401 ),
inference(avatar_component_clause,[],[f3678]) ).
fof(f3691,definition,
( spl136_404
<=> e11 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl136_404])],[avatar_definition]) ).
fof(f3696,definition,
( spl136_405
<=> e12 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl136_405])],[avatar_definition]) ).
fof(f3698,plain,
( e12 = op1(e10,e11)
| ~ spl136_405 ),
inference(avatar_component_clause,[],[f3696]) ).
fof(f3700,definition,
( spl136_406
<=> e12 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl136_406])],[avatar_definition]) ).
fof(f3702,plain,
( e12 = op1(e10,e13)
| ~ spl136_406 ),
inference(avatar_component_clause,[],[f3700]) ).
fof(f3703,plain,
( spl136_371
| spl136_405
| spl136_291
| spl136_406 ),
inference(avatar_split_clause,[],[f41,f3700,f2937,f3696,f3506]) ).
fof(f3709,definition,
( spl136_408
<=> e12 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl136_408])],[avatar_definition]) ).
fof(f3711,plain,
( e12 = op1(e13,e10)
| ~ spl136_408 ),
inference(avatar_component_clause,[],[f3709]) ).
fof(f3718,definition,
( spl136_410
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl136_410])],[avatar_definition]) ).
fof(f3723,definition,
( spl136_411
<=> e13 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl136_411])],[avatar_definition]) ).
fof(f3725,plain,
( e13 = op1(e11,e10)
| ~ spl136_411 ),
inference(avatar_component_clause,[],[f3723]) ).
fof(f3727,definition,
( spl136_412
<=> e13 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl136_412])],[avatar_definition]) ).
fof(f3729,plain,
( e13 = op1(e12,e10)
| ~ spl136_412 ),
inference(avatar_component_clause,[],[f3727]) ).
fof(f3730,plain,
( spl136_374
| spl136_411
| spl136_412
| spl136_301 ),
inference(avatar_split_clause,[],[f44,f2992,f3727,f3723,f3519]) ).
fof(f3732,definition,
( spl136_413
<=> e10 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl136_413])],[avatar_definition]) ).
fof(f3734,plain,
( e10 = op1(e11,e12)
| ~ spl136_413 ),
inference(avatar_component_clause,[],[f3732]) ).
fof(f3736,definition,
( spl136_414
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl136_414])],[avatar_definition]) ).
fof(f3738,plain,
( e10 = op1(e11,e13)
| ~ spl136_414 ),
inference(avatar_component_clause,[],[f3736]) ).
fof(f3745,definition,
( spl136_416
<=> e10 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl136_416])],[avatar_definition]) ).
fof(f3747,plain,
( e10 = op1(e13,e11)
| ~ spl136_416 ),
inference(avatar_component_clause,[],[f3745]) ).
fof(f3749,plain,
( spl136_279
| spl136_282
| spl136_284
| spl136_287 ),
inference(avatar_split_clause,[],[f47,f2916,f2900,f2888,f2872]) ).
fof(f3750,plain,
( spl136_280
| spl136_282
| spl136_285
| spl136_288 ),
inference(avatar_split_clause,[],[f48,f2921,f2905,f2888,f2877]) ).
fof(f3752,definition,
( spl136_417
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl136_417])],[avatar_definition]) ).
fof(f3754,plain,
( e12 = op1(e11,e13)
| ~ spl136_417 ),
inference(avatar_component_clause,[],[f3752]) ).
fof(f3762,definition,
( spl136_419
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl136_419])],[avatar_definition]) ).
fof(f3764,plain,
( e13 = op1(e11,e12)
| ~ spl136_419 ),
inference(avatar_component_clause,[],[f3762]) ).
fof(f3765,plain,
( spl136_411
| spl136_375
| spl136_419
| spl136_305 ),
inference(avatar_split_clause,[],[f51,f3013,f3762,f3523,f3723]) ).
fof(f3772,definition,
( spl136_421
<=> e10 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl136_421])],[avatar_definition]) ).
fof(f3774,plain,
( e10 = op1(e12,e13)
| ~ spl136_421 ),
inference(avatar_component_clause,[],[f3772]) ).
fof(f3777,definition,
( spl136_422
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl136_422])],[avatar_definition]) ).
fof(f3779,plain,
( e10 = op1(e13,e12)
| ~ spl136_422 ),
inference(avatar_component_clause,[],[f3777]) ).
fof(f3794,plain,
( spl136_410
| spl136_419
| spl136_376
| spl136_307 ),
inference(avatar_split_clause,[],[f60,f3024,f3527,f3762,f3718]) ).
fof(f3795,plain,
( spl136_277
| spl136_416
| spl136_422
| spl136_367 ),
inference(avatar_split_clause,[],[f61,f3488,f3777,f3745,f2861]) ).
fof(f3796,plain,
( spl136_276
| spl136_414
| spl136_421
| spl136_367 ),
inference(avatar_split_clause,[],[f62,f3488,f3772,f3736,f2856]) ).
fof(f3802,plain,
( spl136_302
| spl136_305
| spl136_308
| spl136_310 ),
inference(avatar_split_clause,[],[f68,f3040,f3029,f3013,f2997]) ).
fof(f3805,plain,
( spl136_273
| spl136_401
| spl136_291
| spl136_410 ),
inference(avatar_split_clause,[],[f23,f3718,f2937,f3678,f2840]) ).
fof(f3815,plain,
( spl136_277
| spl136_404
| spl136_408
| spl136_301 ),
inference(avatar_split_clause,[],[f33,f2992,f3709,f3691,f2861]) ).
fof(f3819,plain,
( e20 != e21
| ~ spl136_2
| spl136_7 ),
inference(forward_demodulation,[],[f1374,f1349]) ).
fof(f3822,plain,
spl136_370,
inference(avatar_split_clause,[],[f826,f3501]) ).
fof(f3823,plain,
spl136_250,
inference(avatar_split_clause,[],[f829,f2729]) ).
fof(f3866,plain,
( e20 = e23
| ~ spl136_32
| ~ spl136_136 ),
inference(forward_demodulation,[],[f1493,f1977]) ).
fof(f3888,plain,
( e20 != e23
| spl136_32
| ~ spl136_136 ),
inference(forward_demodulation,[],[f1494,f1977]) ).
fof(f3890,plain,
( e20 = e23
| ~ spl136_156
| ~ spl136_182 ),
inference(superposition,[],[f2227,f2086]) ).
fof(f3894,plain,
( $false
| spl136_32
| ~ spl136_136
| ~ spl136_156
| ~ spl136_182 ),
inference(forward_subsumption_resolution,[],[f3890,f3888]) ).
fof(f3895,plain,
( spl136_32
| ~ spl136_136
| ~ spl136_156
| ~ spl136_182 ),
inference(avatar_contradiction_clause,[],[f3894]) ).
fof(f3903,plain,
( e21 = e23
| ~ spl136_37
| ~ spl136_136 ),
inference(forward_demodulation,[],[f1517,f1977]) ).
fof(f3926,plain,
( $false
| ~ spl136_37
| ~ spl136_136 ),
inference(forward_subsumption_resolution,[],[f220,f3903]) ).
fof(f3927,plain,
( ~ spl136_37
| ~ spl136_136 ),
inference(avatar_contradiction_clause,[],[f3926]) ).
fof(f3928,plain,
( e21 != e23
| spl136_37
| ~ spl136_136 ),
inference(forward_demodulation,[],[f1518,f1977]) ).
fof(f3951,plain,
( e20 = e21
| ~ spl136_162
| ~ spl136_245 ),
inference(superposition,[],[f2710,f2118]) ).
fof(f3955,plain,
( $false
| ~ spl136_2
| spl136_7
| ~ spl136_162
| ~ spl136_245 ),
inference(forward_subsumption_resolution,[],[f3951,f3819]) ).
fof(f3956,plain,
( ~ spl136_2
| spl136_7
| ~ spl136_162
| ~ spl136_245 ),
inference(avatar_contradiction_clause,[],[f3955]) ).
fof(f3958,plain,
( e20 = e22
| ~ spl136_176
| ~ spl136_246 ),
inference(forward_demodulation,[],[f2714,f2194]) ).
fof(f3959,plain,
( $false
| ~ spl136_176
| ~ spl136_246 ),
inference(forward_subsumption_resolution,[],[f3958,f223]) ).
fof(f3960,plain,
( ~ spl136_176
| ~ spl136_246 ),
inference(avatar_contradiction_clause,[],[f3959]) ).
fof(f3984,plain,
( $false
| ~ spl136_32
| ~ spl136_136 ),
inference(forward_subsumption_resolution,[],[f222,f3866]) ).
fof(f3985,plain,
( ~ spl136_32
| ~ spl136_136 ),
inference(avatar_contradiction_clause,[],[f3984]) ).
fof(f3999,plain,
( e20 = e21
| ~ spl136_246
| ~ spl136_249 ),
inference(forward_demodulation,[],[f2727,f2714]) ).
fof(f4000,plain,
( $false
| ~ spl136_2
| spl136_7
| ~ spl136_246
| ~ spl136_249 ),
inference(forward_subsumption_resolution,[],[f3999,f3819]) ).
fof(f4001,plain,
( ~ spl136_2
| spl136_7
| ~ spl136_246
| ~ spl136_249 ),
inference(avatar_contradiction_clause,[],[f4000]) ).
fof(f4002,plain,
( e20 = e21
| ~ spl136_2
| ~ spl136_7 ),
inference(forward_demodulation,[],[f1373,f1349]) ).
fof(f4039,plain,
( e21 = e23
| ~ spl136_190
| ~ spl136_250 ),
inference(forward_demodulation,[],[f2731,f2270]) ).
fof(f4040,plain,
( $false
| spl136_37
| ~ spl136_136
| ~ spl136_190
| ~ spl136_250 ),
inference(forward_subsumption_resolution,[],[f4039,f3928]) ).
fof(f4041,plain,
( spl136_37
| ~ spl136_136
| ~ spl136_190
| ~ spl136_250 ),
inference(avatar_contradiction_clause,[],[f4040]) ).
fof(f4053,plain,
( e21 = e22
| ~ spl136_250
| ~ spl136_253 ),
inference(superposition,[],[f2744,f2731]) ).
fof(f4059,plain,
( $false
| ~ spl136_250
| ~ spl136_253 ),
inference(forward_subsumption_resolution,[],[f4053,f221]) ).
fof(f4060,plain,
( ~ spl136_250
| ~ spl136_253 ),
inference(avatar_contradiction_clause,[],[f4059]) ).
fof(f4065,plain,
( e22 = e23
| ~ spl136_251
| ~ spl136_254 ),
inference(superposition,[],[f2749,f2736]) ).
fof(f4070,plain,
( $false
| ~ spl136_251
| ~ spl136_254 ),
inference(forward_subsumption_resolution,[],[f4065,f219]) ).
fof(f4071,plain,
( ~ spl136_251
| ~ spl136_254 ),
inference(avatar_contradiction_clause,[],[f4070]) ).
fof(f4072,plain,
( e20 = e23
| ~ spl136_148
| ~ spl136_254 ),
inference(forward_demodulation,[],[f2042,f2749]) ).
fof(f4075,plain,
( $false
| spl136_32
| ~ spl136_136
| ~ spl136_148
| ~ spl136_254 ),
inference(forward_subsumption_resolution,[],[f4072,f3888]) ).
fof(f4076,plain,
( spl136_32
| ~ spl136_136
| ~ spl136_148
| ~ spl136_254 ),
inference(avatar_contradiction_clause,[],[f4075]) ).
fof(f4103,plain,
( e20 = e23
| ~ spl136_245
| ~ spl136_255 ),
inference(forward_demodulation,[],[f2710,f2753]) ).
fof(f4106,plain,
( $false
| spl136_32
| ~ spl136_136
| ~ spl136_245
| ~ spl136_255 ),
inference(forward_subsumption_resolution,[],[f4103,f3888]) ).
fof(f4107,plain,
( spl136_32
| ~ spl136_136
| ~ spl136_245
| ~ spl136_255 ),
inference(avatar_contradiction_clause,[],[f4106]) ).
fof(f4119,plain,
( e20 = e23
| ~ spl136_246
| ~ spl136_256 ),
inference(superposition,[],[f2757,f2714]) ).
fof(f4124,plain,
( $false
| spl136_32
| ~ spl136_136
| ~ spl136_246
| ~ spl136_256 ),
inference(forward_subsumption_resolution,[],[f4119,f3888]) ).
fof(f4125,plain,
( spl136_32
| ~ spl136_136
| ~ spl136_246
| ~ spl136_256 ),
inference(avatar_contradiction_clause,[],[f4124]) ).
fof(f4141,plain,
( e10 = e11
| ~ spl136_271
| ~ spl136_279 ),
inference(forward_demodulation,[],[f2874,f2831]) ).
fof(f4142,plain,
( $false
| ~ spl136_271
| ~ spl136_279 ),
inference(forward_subsumption_resolution,[],[f4141,f218]) ).
fof(f4143,plain,
( ~ spl136_271
| ~ spl136_279 ),
inference(avatar_contradiction_clause,[],[f4142]) ).
fof(f4177,plain,
( e10 = e13
| ~ spl136_277
| ~ spl136_301 ),
inference(superposition,[],[f2994,f2863]) ).
fof(f4181,plain,
( $false
| ~ spl136_277
| ~ spl136_301 ),
inference(forward_subsumption_resolution,[],[f4177,f216]) ).
fof(f4182,plain,
( ~ spl136_277
| ~ spl136_301 ),
inference(avatar_contradiction_clause,[],[f4181]) ).
fof(f4184,plain,
( e10 = e13
| ~ spl136_276
| ~ spl136_302 ),
inference(superposition,[],[f2999,f2858]) ).
fof(f4188,plain,
( $false
| ~ spl136_276
| ~ spl136_302 ),
inference(forward_subsumption_resolution,[],[f4184,f216]) ).
fof(f4189,plain,
( ~ spl136_276
| ~ spl136_302 ),
inference(avatar_contradiction_clause,[],[f4188]) ).
fof(f4219,plain,
( e11 = e13
| ~ spl136_310
| ~ spl136_370 ),
inference(forward_demodulation,[],[f3503,f3042]) ).
fof(f4220,plain,
( $false
| ~ spl136_310
| ~ spl136_370 ),
inference(forward_subsumption_resolution,[],[f4219,f214]) ).
fof(f4221,plain,
( ~ spl136_310
| ~ spl136_370 ),
inference(avatar_contradiction_clause,[],[f4220]) ).
fof(f4223,plain,
( e10 = e13
| ~ spl136_268
| ~ spl136_374 ),
inference(superposition,[],[f3521,f2814]) ).
fof(f4227,plain,
( $false
| ~ spl136_268
| ~ spl136_374 ),
inference(forward_subsumption_resolution,[],[f4223,f216]) ).
fof(f4228,plain,
( ~ spl136_268
| ~ spl136_374 ),
inference(avatar_contradiction_clause,[],[f4227]) ).
fof(f4230,plain,
( e10 = e11
| ~ spl136_282
| ~ spl136_365 ),
inference(superposition,[],[f3482,f2890]) ).
fof(f4234,plain,
( $false
| ~ spl136_282
| ~ spl136_365 ),
inference(forward_subsumption_resolution,[],[f4230,f218]) ).
fof(f4235,plain,
( ~ spl136_282
| ~ spl136_365 ),
inference(avatar_contradiction_clause,[],[f4234]) ).
fof(f4248,plain,
( e21 = e22
| ~ spl136_176
| ~ spl136_249 ),
inference(forward_demodulation,[],[f2727,f2194]) ).
fof(f4250,plain,
( $false
| ~ spl136_176
| ~ spl136_249 ),
inference(forward_subsumption_resolution,[],[f4248,f221]) ).
fof(f4251,plain,
( ~ spl136_176
| ~ spl136_249 ),
inference(avatar_contradiction_clause,[],[f4250]) ).
fof(f4296,plain,
( e21 = e22
| ~ spl136_159
| ~ spl136_383 ),
inference(superposition,[],[f3563,f2102]) ).
fof(f4301,plain,
( $false
| ~ spl136_159
| ~ spl136_383 ),
inference(forward_subsumption_resolution,[],[f4296,f221]) ).
fof(f4302,plain,
( ~ spl136_159
| ~ spl136_383 ),
inference(avatar_contradiction_clause,[],[f4301]) ).
fof(f4303,plain,
( e20 = e23
| ~ spl136_187
| ~ spl136_398 ),
inference(forward_demodulation,[],[f3635,f2254]) ).
fof(f4304,plain,
( $false
| spl136_32
| ~ spl136_136
| ~ spl136_187
| ~ spl136_398 ),
inference(forward_subsumption_resolution,[],[f4303,f3888]) ).
fof(f4305,plain,
( spl136_32
| ~ spl136_136
| ~ spl136_187
| ~ spl136_398 ),
inference(avatar_contradiction_clause,[],[f4304]) ).
fof(f4311,plain,
( e22 = e23
| ~ spl136_381
| ~ spl136_385 ),
inference(superposition,[],[f3572,f3554]) ).
fof(f4315,plain,
( $false
| ~ spl136_381
| ~ spl136_385 ),
inference(forward_subsumption_resolution,[],[f4311,f219]) ).
fof(f4316,plain,
( ~ spl136_381
| ~ spl136_385 ),
inference(avatar_contradiction_clause,[],[f4315]) ).
fof(f4347,plain,
( e20 = e22
| ~ spl136_390
| ~ spl136_393 ),
inference(superposition,[],[f3610,f3594]) ).
fof(f4353,plain,
( $false
| ~ spl136_390
| ~ spl136_393 ),
inference(forward_subsumption_resolution,[],[f4347,f223]) ).
fof(f4354,plain,
( ~ spl136_390
| ~ spl136_393 ),
inference(avatar_contradiction_clause,[],[f4353]) ).
fof(f4364,plain,
( e20 = e23
| ~ spl136_389
| ~ spl136_395 ),
inference(superposition,[],[f3620,f3590]) ).
fof(f4370,plain,
( $false
| spl136_32
| ~ spl136_136
| ~ spl136_389
| ~ spl136_395 ),
inference(forward_subsumption_resolution,[],[f4364,f3888]) ).
fof(f4371,plain,
( spl136_32
| ~ spl136_136
| ~ spl136_389
| ~ spl136_395 ),
inference(avatar_contradiction_clause,[],[f4370]) ).
fof(f4372,plain,
( e21 = e23
| ~ spl136_159
| ~ spl136_387 ),
inference(superposition,[],[f3581,f2102]) ).
fof(f4378,plain,
( $false
| spl136_37
| ~ spl136_136
| ~ spl136_159
| ~ spl136_387 ),
inference(forward_subsumption_resolution,[],[f4372,f3928]) ).
fof(f4379,plain,
( spl136_37
| ~ spl136_136
| ~ spl136_159
| ~ spl136_387 ),
inference(avatar_contradiction_clause,[],[f4378]) ).
fof(f4414,plain,
( e20 = e21
| ~ spl136_247
| ~ spl136_250 ),
inference(superposition,[],[f2718,f2731]) ).
fof(f4420,plain,
( $false
| ~ spl136_2
| spl136_7
| ~ spl136_247
| ~ spl136_250 ),
inference(forward_subsumption_resolution,[],[f4414,f3819]) ).
fof(f4421,plain,
( ~ spl136_2
| spl136_7
| ~ spl136_247
| ~ spl136_250 ),
inference(avatar_contradiction_clause,[],[f4420]) ).
fof(f4431,plain,
( e22 = e23
| ~ spl136_176
| ~ spl136_256 ),
inference(superposition,[],[f2757,f2194]) ).
fof(f4435,plain,
( $false
| ~ spl136_176
| ~ spl136_256 ),
inference(forward_subsumption_resolution,[],[f4431,f219]) ).
fof(f4436,plain,
( ~ spl136_176
| ~ spl136_256 ),
inference(avatar_contradiction_clause,[],[f4435]) ).
fof(f4447,plain,
( e21 = e22
| ~ spl136_160
| ~ spl136_381 ),
inference(superposition,[],[f3554,f2107]) ).
fof(f4453,plain,
( $false
| ~ spl136_160
| ~ spl136_381 ),
inference(forward_subsumption_resolution,[],[f4447,f221]) ).
fof(f4454,plain,
( ~ spl136_160
| ~ spl136_381 ),
inference(avatar_contradiction_clause,[],[f4453]) ).
fof(f4552,plain,
( e21 = e23
| ~ spl136_377
| ~ spl136_386 ),
inference(superposition,[],[f3576,f3536]) ).
fof(f4558,plain,
( $false
| spl136_37
| ~ spl136_136
| ~ spl136_377
| ~ spl136_386 ),
inference(forward_subsumption_resolution,[],[f4552,f3928]) ).
fof(f4559,plain,
( spl136_37
| ~ spl136_136
| ~ spl136_377
| ~ spl136_386 ),
inference(avatar_contradiction_clause,[],[f4558]) ).
fof(f4633,plain,
( e20 = e21
| ~ spl136_164
| ~ spl136_389 ),
inference(superposition,[],[f3590,f2130]) ).
fof(f4639,plain,
( $false
| ~ spl136_2
| spl136_7
| ~ spl136_164
| ~ spl136_389 ),
inference(forward_subsumption_resolution,[],[f4633,f3819]) ).
fof(f4640,plain,
( ~ spl136_2
| spl136_7
| ~ spl136_164
| ~ spl136_389 ),
inference(avatar_contradiction_clause,[],[f4639]) ).
fof(f4732,plain,
( e11 = e12
| ~ spl136_280
| ~ spl136_405 ),
inference(superposition,[],[f3698,f2879]) ).
fof(f4737,plain,
( $false
| ~ spl136_280
| ~ spl136_405 ),
inference(forward_subsumption_resolution,[],[f4732,f215]) ).
fof(f4738,plain,
( ~ spl136_280
| ~ spl136_405 ),
inference(avatar_contradiction_clause,[],[f4737]) ).
fof(f4765,plain,
( e12 = e13
| ~ spl136_372
| ~ spl136_375 ),
inference(superposition,[],[f3525,f3512]) ).
fof(f4771,plain,
( $false
| ~ spl136_372
| ~ spl136_375 ),
inference(forward_subsumption_resolution,[],[f4765,f213]) ).
fof(f4772,plain,
( ~ spl136_372
| ~ spl136_375 ),
inference(avatar_contradiction_clause,[],[f4771]) ).
fof(f4773,plain,
( e10 = e11
| ~ spl136_367
| ~ spl136_370 ),
inference(superposition,[],[f3490,f3503]) ).
fof(f4778,plain,
( $false
| ~ spl136_367
| ~ spl136_370 ),
inference(forward_subsumption_resolution,[],[f4773,f218]) ).
fof(f4779,plain,
( ~ spl136_367
| ~ spl136_370 ),
inference(avatar_contradiction_clause,[],[f4778]) ).
fof(f4780,plain,
( e10 = e12
| ~ spl136_296
| ~ spl136_366 ),
inference(forward_demodulation,[],[f3486,f2966]) ).
fof(f4781,plain,
( $false
| ~ spl136_296
| ~ spl136_366 ),
inference(forward_subsumption_resolution,[],[f4780,f217]) ).
fof(f4782,plain,
( ~ spl136_296
| ~ spl136_366 ),
inference(avatar_contradiction_clause,[],[f4781]) ).
fof(f4787,plain,
( e12 = e13
| ~ spl136_296
| ~ spl136_376 ),
inference(superposition,[],[f3529,f2966]) ).
fof(f4791,plain,
( $false
| ~ spl136_296
| ~ spl136_376 ),
inference(forward_subsumption_resolution,[],[f4787,f213]) ).
fof(f4792,plain,
( ~ spl136_296
| ~ spl136_376 ),
inference(avatar_contradiction_clause,[],[f4791]) ).
fof(f4817,plain,
( e12 = e13
| ~ spl136_302
| ~ spl136_406 ),
inference(forward_demodulation,[],[f3702,f2999]) ).
fof(f4818,plain,
( $false
| ~ spl136_302
| ~ spl136_406 ),
inference(forward_subsumption_resolution,[],[f4817,f213]) ).
fof(f4819,plain,
( ~ spl136_302
| ~ spl136_406 ),
inference(avatar_contradiction_clause,[],[f4818]) ).
fof(f4838,plain,
( e12 = e13
| ~ spl136_371
| ~ spl136_374 ),
inference(forward_demodulation,[],[f3508,f3521]) ).
fof(f4842,plain,
( $false
| ~ spl136_371
| ~ spl136_374 ),
inference(forward_subsumption_resolution,[],[f4838,f213]) ).
fof(f4843,plain,
( ~ spl136_371
| ~ spl136_374 ),
inference(avatar_contradiction_clause,[],[f4842]) ).
fof(f4851,plain,
( e11 = e12
| ~ spl136_370
| ~ spl136_373 ),
inference(superposition,[],[f3516,f3503]) ).
fof(f4857,plain,
( $false
| ~ spl136_370
| ~ spl136_373 ),
inference(forward_subsumption_resolution,[],[f4851,f215]) ).
fof(f4858,plain,
( ~ spl136_370
| ~ spl136_373 ),
inference(avatar_contradiction_clause,[],[f4857]) ).
fof(f4862,plain,
( e10 = e12
| ~ spl136_294
| ~ spl136_413 ),
inference(forward_demodulation,[],[f3734,f2955]) ).
fof(f4864,plain,
( $false
| ~ spl136_294
| ~ spl136_413 ),
inference(forward_subsumption_resolution,[],[f4862,f217]) ).
fof(f4865,plain,
( ~ spl136_294
| ~ spl136_413 ),
inference(avatar_contradiction_clause,[],[f4864]) ).
fof(f4907,plain,
( e11 = e13
| ~ spl136_279
| ~ spl136_411 ),
inference(superposition,[],[f3725,f2874]) ).
fof(f4909,plain,
( e11 = e13
| ~ spl136_279
| ~ spl136_411 ),
inference(superposition,[],[f2874,f3725]) ).
fof(f4911,plain,
( $false
| ~ spl136_279
| ~ spl136_411 ),
inference(forward_subsumption_resolution,[],[f4909,f214]) ).
fof(f4912,plain,
( ~ spl136_279
| ~ spl136_411 ),
inference(avatar_contradiction_clause,[],[f4911]) ).
fof(f4913,plain,
( $false
| ~ spl136_279
| ~ spl136_411 ),
inference(forward_subsumption_resolution,[],[f4907,f214]) ).
fof(f4914,plain,
( ~ spl136_279
| ~ spl136_411 ),
inference(avatar_contradiction_clause,[],[f4913]) ).
fof(f4939,plain,
( e10 = e12
| ~ spl136_414
| ~ spl136_417 ),
inference(superposition,[],[f3754,f3738]) ).
fof(f4945,plain,
( $false
| ~ spl136_414
| ~ spl136_417 ),
inference(forward_subsumption_resolution,[],[f4939,f217]) ).
fof(f4946,plain,
( ~ spl136_414
| ~ spl136_417 ),
inference(avatar_contradiction_clause,[],[f4945]) ).
fof(f4948,plain,
( e10 = e13
| ~ spl136_308
| ~ spl136_421 ),
inference(forward_demodulation,[],[f3774,f3031]) ).
fof(f4949,plain,
( $false
| ~ spl136_308
| ~ spl136_421 ),
inference(forward_subsumption_resolution,[],[f4948,f216]) ).
fof(f4950,plain,
( ~ spl136_308
| ~ spl136_421 ),
inference(avatar_contradiction_clause,[],[f4949]) ).
fof(f5074,plain,
( e10 = e13
| ~ spl136_365
| ~ spl136_375 ),
inference(superposition,[],[f3525,f3482]) ).
fof(f5080,plain,
( $false
| ~ spl136_365
| ~ spl136_375 ),
inference(forward_subsumption_resolution,[],[f5074,f216]) ).
fof(f5081,plain,
( ~ spl136_365
| ~ spl136_375 ),
inference(avatar_contradiction_clause,[],[f5080]) ).
fof(f5106,plain,
( e10 = e13
| ~ spl136_366
| ~ spl136_376 ),
inference(superposition,[],[f3529,f3486]) ).
fof(f5112,plain,
( $false
| ~ spl136_366
| ~ spl136_376 ),
inference(forward_subsumption_resolution,[],[f5106,f216]) ).
fof(f5113,plain,
( ~ spl136_366
| ~ spl136_376 ),
inference(avatar_contradiction_clause,[],[f5112]) ).
fof(f5124,plain,
( e11 = e13
| ~ spl136_282
| ~ spl136_375 ),
inference(forward_demodulation,[],[f2890,f3525]) ).
fof(f5125,plain,
( $false
| ~ spl136_282
| ~ spl136_375 ),
inference(forward_subsumption_resolution,[],[f5124,f214]) ).
fof(f5126,plain,
( ~ spl136_282
| ~ spl136_375 ),
inference(avatar_contradiction_clause,[],[f5125]) ).
fof(f5150,plain,
( e10 = e11
| ~ spl136_288
| ~ spl136_416 ),
inference(superposition,[],[f3747,f2923]) ).
fof(f5155,plain,
( $false
| ~ spl136_288
| ~ spl136_416 ),
inference(forward_subsumption_resolution,[],[f5150,f218]) ).
fof(f5156,plain,
( ~ spl136_288
| ~ spl136_416 ),
inference(avatar_contradiction_clause,[],[f5155]) ).
fof(f5186,plain,
( e11 = e12
| ~ spl136_287
| ~ spl136_417 ),
inference(superposition,[],[f3754,f2918]) ).
fof(f5192,plain,
( $false
| ~ spl136_287
| ~ spl136_417 ),
inference(forward_subsumption_resolution,[],[f5186,f215]) ).
fof(f5193,plain,
( ~ spl136_287
| ~ spl136_417 ),
inference(avatar_contradiction_clause,[],[f5192]) ).
fof(f5215,plain,
( e10 = e13
| ~ spl136_413
| ~ spl136_419 ),
inference(forward_demodulation,[],[f3734,f3764]) ).
fof(f5217,plain,
( $false
| ~ spl136_413
| ~ spl136_419 ),
inference(forward_subsumption_resolution,[],[f5215,f216]) ).
fof(f5218,plain,
( ~ spl136_413
| ~ spl136_419 ),
inference(avatar_contradiction_clause,[],[f5217]) ).
fof(f5272,plain,
( e11 = e12
| ~ spl136_282
| ~ spl136_372 ),
inference(superposition,[],[f3512,f2890]) ).
fof(f5278,plain,
( $false
| ~ spl136_282
| ~ spl136_372 ),
inference(forward_subsumption_resolution,[],[f5272,f215]) ).
fof(f5279,plain,
( ~ spl136_282
| ~ spl136_372 ),
inference(avatar_contradiction_clause,[],[f5278]) ).
fof(f5338,plain,
( e11 != op1(e13,e10)
| ~ spl136_370 ),
inference(forward_demodulation,[],[f120,f3503]) ).
fof(f5340,plain,
( e13 != op1(e13,e10)
| ~ spl136_307 ),
inference(forward_demodulation,[],[f121,f3026]) ).
fof(f5342,plain,
( e10 != op1(e12,e12)
| ~ spl136_421 ),
inference(forward_demodulation,[],[f123,f3774]) ).
fof(f5374,plain,
( e12 != op1(e10,e12)
| ~ spl136_296 ),
inference(forward_demodulation,[],[f151,f2966]) ).
fof(f5386,plain,
( e10 != op1(e10,e10)
| ~ spl136_277 ),
inference(forward_demodulation,[],[f162,f2863]) ).
fof(f5389,plain,
( e21 != op2(e23,e22)
| ~ spl136_250 ),
inference(forward_demodulation,[],[f165,f2731]) ).
fof(f5391,plain,
( e21 != op2(e23,e21)
| ~ spl136_250 ),
inference(forward_demodulation,[],[f166,f2731]) ).
fof(f5396,plain,
( e20 != op2(e22,e22)
| ~ spl136_397 ),
inference(forward_demodulation,[],[f171,f3630]) ).
fof(f5402,plain,
( e22 != op2(e22,e20)
| ~ spl136_176 ),
inference(forward_demodulation,[],[f175,f2194]) ).
fof(f5418,plain,
( e21 != op2(e21,e23)
| ~ spl136_250 ),
inference(forward_demodulation,[],[f190,f2731]) ).
fof(f5428,plain,
( e22 != op2(e20,e22)
| ~ spl136_176 ),
inference(forward_demodulation,[],[f199,f2194]) ).
fof(f5439,plain,
( e20 != op2(e20,e20)
| ~ spl136_157 ),
inference(forward_demodulation,[],[f210,f2091]) ).
fof(f5442,plain,
( e12 = op1(e11,e13)
| ~ spl136_370 ),
inference(forward_demodulation,[],[f825,f3503]) ).
fof(f5443,plain,
( e12 = e13
| ~ spl136_305
| ~ spl136_370 ),
inference(forward_demodulation,[],[f5442,f3015]) ).
fof(f5444,plain,
( $false
| ~ spl136_305
| ~ spl136_370 ),
inference(forward_subsumption_resolution,[],[f5443,f213]) ).
fof(f5445,plain,
( ~ spl136_305
| ~ spl136_370 ),
inference(avatar_contradiction_clause,[],[f5444]) ).
fof(f5453,plain,
( spl136_417
| ~ spl136_370 ),
inference(avatar_split_clause,[],[f5442,f3501,f3752]) ).
fof(f5454,plain,
( ~ spl136_366
| ~ spl136_421 ),
inference(avatar_split_clause,[],[f5342,f3772,f3484]) ).
fof(f5457,plain,
( ~ spl136_404
| ~ spl136_370 ),
inference(avatar_split_clause,[],[f5338,f3501,f3691]) ).
fof(f5524,plain,
( e13 != op1(e12,e10)
| ~ spl136_308 ),
inference(forward_demodulation,[],[f126,f3031]) ).
fof(f5542,plain,
( e10 != op1(e11,e12)
| ~ spl136_422 ),
inference(forward_demodulation,[],[f148,f3779]) ).
fof(f5556,plain,
( e22 = op2(e21,e23)
| ~ spl136_250 ),
inference(forward_demodulation,[],[f828,f2731]) ).
fof(f5557,plain,
( e22 = e23
| ~ spl136_185
| ~ spl136_250 ),
inference(forward_demodulation,[],[f5556,f2243]) ).
fof(f5558,plain,
( $false
| ~ spl136_185
| ~ spl136_250 ),
inference(forward_subsumption_resolution,[],[f5557,f219]) ).
fof(f5559,plain,
( ~ spl136_185
| ~ spl136_250 ),
inference(avatar_contradiction_clause,[],[f5558]) ).
fof(f5570,plain,
( e22 != op2(e21,e23)
| ~ spl136_382 ),
inference(forward_demodulation,[],[f194,f3558]) ).
fof(f5571,plain,
( spl136_393
| ~ spl136_250 ),
inference(avatar_split_clause,[],[f5556,f2729,f3608]) ).
fof(f5577,plain,
( ~ spl136_167
| ~ spl136_250 ),
inference(avatar_split_clause,[],[f5418,f2729,f2144]) ).
fof(f5588,plain,
( ~ spl136_393
| ~ spl136_382 ),
inference(avatar_split_clause,[],[f5570,f3556,f3608]) ).
fof(f5594,plain,
( ~ spl136_246
| ~ spl136_397 ),
inference(avatar_split_clause,[],[f5396,f3628,f2712]) ).
fof(f5596,plain,
( e21 != op2(e22,e21)
| ~ spl136_379 ),
inference(forward_demodulation,[],[f176,f3545]) ).
fof(f5605,plain,
( ~ spl136_400
| ~ spl136_250 ),
inference(avatar_split_clause,[],[f5389,f2729,f3643]) ).
fof(f5609,plain,
( ~ spl136_148
| ~ spl136_157 ),
inference(avatar_split_clause,[],[f5439,f2089,f2040]) ).
fof(f5631,plain,
( e20 = e22
| ~ spl136_148
| ~ spl136_251 ),
inference(superposition,[],[f2736,f2042]) ).
fof(f5636,plain,
( $false
| ~ spl136_148
| ~ spl136_251 ),
inference(forward_subsumption_resolution,[],[f5631,f223]) ).
fof(f5637,plain,
( ~ spl136_148
| ~ spl136_251 ),
inference(avatar_contradiction_clause,[],[f5636]) ).
fof(f5639,plain,
( ~ spl136_171
| ~ spl136_176 ),
inference(avatar_split_clause,[],[f5428,f2192,f2165]) ).
fof(f5642,plain,
( e20 != op2(e22,e20)
| ~ spl136_148 ),
inference(forward_demodulation,[],[f211,f2042]) ).
fof(f5696,plain,
( e23 = h2(e11)
| ~ spl136_255 ),
inference(forward_demodulation,[],[f836,f2753]) ).
fof(f5697,plain,
( spl136_86
| ~ spl136_255 ),
inference(avatar_split_clause,[],[f5696,f2751,f1736]) ).
fof(f5699,plain,
( h2(op1(e12,e11)) != op2(h2(e12),e23)
| spl136_74
| ~ spl136_86 ),
inference(superposition,[],[f1686,f1737]) ).
fof(f5700,plain,
( h2(e11) != op2(h2(e12),e23)
| spl136_74
| ~ spl136_86
| ~ spl136_285 ),
inference(forward_demodulation,[],[f5699,f2907]) ).
fof(f5701,plain,
( e23 != op2(h2(e12),e23)
| spl136_74
| ~ spl136_86
| ~ spl136_285 ),
inference(forward_demodulation,[],[f5700,f1737]) ).
fof(f5713,plain,
( e22 != op2(e21,e21)
| ~ spl136_393 ),
inference(forward_demodulation,[],[f178,f3610]) ).
fof(f5737,plain,
( e23 != op2(e20,e21)
| ~ spl136_255 ),
inference(forward_demodulation,[],[f206,f2753]) ).
fof(f5795,plain,
( ~ spl136_268
| ~ spl136_277 ),
inference(avatar_split_clause,[],[f5386,f2861,f2812]) ).
fof(f5811,plain,
( e12 != op1(e12,e13)
| ~ spl136_417 ),
inference(forward_demodulation,[],[f143,f3754]) ).
fof(f5818,plain,
( ~ spl136_298
| ~ spl136_417 ),
inference(avatar_split_clause,[],[f5811,f3752,f2976]) ).
fof(f5824,plain,
( ~ spl136_301
| ~ spl136_307 ),
inference(avatar_split_clause,[],[f5340,f3024,f2992]) ).
fof(f5826,plain,
( ~ spl136_291
| ~ spl136_296 ),
inference(avatar_split_clause,[],[f5374,f2964,f2937]) ).
fof(f5882,plain,
( e13 != op1(e10,e12)
| ~ spl136_302 ),
inference(forward_demodulation,[],[f135,f2999]) ).
fof(f5894,plain,
( e10 != op1(e10,e12)
| ~ spl136_413 ),
inference(forward_demodulation,[],[f152,f3734]) ).
fof(f5929,plain,
( op2(e23,e21) = h2(e12)
| ~ spl136_255 ),
inference(forward_demodulation,[],[f835,f2753]) ).
fof(f5930,plain,
( e20 = h2(e12)
| ~ spl136_255
| ~ spl136_392 ),
inference(forward_demodulation,[],[f5929,f3603]) ).
fof(f5931,plain,
( spl136_13
| ~ spl136_255
| ~ spl136_392 ),
inference(avatar_split_clause,[],[f5930,f3601,f2751,f1401]) ).
fof(f5932,plain,
( e23 != op2(e20,e23)
| ~ spl136_13
| spl136_74
| ~ spl136_86
| ~ spl136_285 ),
inference(superposition,[],[f5701,f1402]) ).
fof(f5941,plain,
( h2(e10) != op2(h2(e10),h2(e10))
| spl136_65
| ~ spl136_268 ),
inference(forward_demodulation,[],[f1650,f2814]) ).
fof(f5954,plain,
( e10 = op1(e11,op1(e11,e13))
| ~ spl136_370 ),
inference(forward_demodulation,[],[f827,f3503]) ).
fof(f5955,plain,
( e10 = op1(e11,e12)
| ~ spl136_370
| ~ spl136_417 ),
inference(forward_demodulation,[],[f5954,f3754]) ).
fof(f5956,plain,
( e20 = op2(e21,op2(e21,e23))
| ~ spl136_250 ),
inference(forward_demodulation,[],[f830,f2731]) ).
fof(f5957,plain,
( e20 = op2(e21,e22)
| ~ spl136_250
| ~ spl136_393 ),
inference(forward_demodulation,[],[f5956,f3610]) ).
fof(f6122,plain,
( op2(e23,op2(e23,e21)) = h2(e10)
| ~ spl136_255 ),
inference(forward_demodulation,[],[f837,f2753]) ).
fof(f6123,plain,
( op2(e23,e20) = h2(e10)
| ~ spl136_255
| ~ spl136_392 ),
inference(forward_demodulation,[],[f6122,f3603]) ).
fof(f6124,plain,
( e22 = h2(e10)
| ~ spl136_255
| ~ spl136_384
| ~ spl136_392 ),
inference(forward_demodulation,[],[f6123,f3567]) ).
fof(f6125,plain,
( spl136_85
| ~ spl136_255
| ~ spl136_384
| ~ spl136_392 ),
inference(avatar_split_clause,[],[f6124,f3601,f3565,f2751,f1731]) ).
fof(f6126,plain,
( e22 != op2(e22,e22)
| spl136_65
| ~ spl136_85
| ~ spl136_268 ),
inference(superposition,[],[f5941,f1732]) ).
fof(f6127,plain,
( $false
| spl136_65
| ~ spl136_85
| ~ spl136_176
| ~ spl136_268 ),
inference(forward_subsumption_resolution,[],[f6126,f2194]) ).
fof(f6128,plain,
( spl136_65
| ~ spl136_85
| ~ spl136_176
| ~ spl136_268 ),
inference(avatar_contradiction_clause,[],[f6127]) ).
fof(f6130,plain,
( h2(op1(e10,e11)) != op2(h2(e10),e23)
| spl136_66
| ~ spl136_86 ),
inference(forward_demodulation,[],[f1654,f1737]) ).
fof(f6132,plain,
( op2(e22,e23) != h2(op1(e10,e11))
| spl136_66
| ~ spl136_85
| ~ spl136_86 ),
inference(forward_demodulation,[],[f6130,f1732]) ).
fof(f6134,plain,
( op2(e22,e23) != h2(e12)
| spl136_66
| ~ spl136_85
| ~ spl136_86
| ~ spl136_405 ),
inference(forward_demodulation,[],[f6132,f3698]) ).
fof(f6135,plain,
( e20 != op2(e22,e23)
| ~ spl136_13
| spl136_66
| ~ spl136_85
| ~ spl136_86
| ~ spl136_405 ),
inference(forward_demodulation,[],[f6134,f1402]) ).
fof(f6139,plain,
( h2(op1(e10,e12)) != op2(h2(e10),e20)
| ~ spl136_13
| spl136_67 ),
inference(forward_demodulation,[],[f1658,f1402]) ).
fof(f6141,plain,
( op2(e22,e20) != h2(op1(e10,e12))
| ~ spl136_13
| spl136_67
| ~ spl136_85 ),
inference(forward_demodulation,[],[f6139,f1732]) ).
fof(f6143,plain,
( op2(e22,e20) != h2(e11)
| ~ spl136_13
| spl136_67
| ~ spl136_85
| ~ spl136_401 ),
inference(forward_demodulation,[],[f6141,f3680]) ).
fof(f6145,plain,
( e23 != op2(e22,e20)
| ~ spl136_13
| spl136_67
| ~ spl136_85
| ~ spl136_86
| ~ spl136_401 ),
inference(forward_demodulation,[],[f6143,f1737]) ).
fof(f6149,plain,
( h2(op1(e10,e13)) != op2(h2(e10),e21)
| ~ spl136_17
| spl136_68 ),
inference(forward_demodulation,[],[f1662,f1421]) ).
fof(f6151,plain,
( op2(e22,e21) != h2(op1(e10,e13))
| ~ spl136_17
| spl136_68
| ~ spl136_85 ),
inference(forward_demodulation,[],[f6149,f1732]) ).
fof(f6153,plain,
( op2(e22,e21) != h2(e13)
| ~ spl136_17
| spl136_68
| ~ spl136_85
| ~ spl136_302 ),
inference(forward_demodulation,[],[f6151,f2999]) ).
fof(f6155,plain,
( e21 != op2(e22,e21)
| ~ spl136_17
| spl136_68
| ~ spl136_85
| ~ spl136_302 ),
inference(forward_demodulation,[],[f6153,f1421]) ).
fof(f6156,plain,
( $false
| ~ spl136_17
| spl136_68
| ~ spl136_85
| ~ spl136_165
| ~ spl136_302 ),
inference(forward_subsumption_resolution,[],[f6155,f2135]) ).
fof(f6157,plain,
( ~ spl136_17
| spl136_68
| ~ spl136_85
| ~ spl136_165
| ~ spl136_302 ),
inference(avatar_contradiction_clause,[],[f6156]) ).
fof(f6159,plain,
( h2(op1(e11,e10)) != op2(h2(e11),e22)
| spl136_69
| ~ spl136_85 ),
inference(forward_demodulation,[],[f1666,f1732]) ).
fof(f6161,plain,
( op2(e23,e22) != h2(op1(e11,e10))
| spl136_69
| ~ spl136_85
| ~ spl136_86 ),
inference(forward_demodulation,[],[f6159,f1737]) ).
fof(f6163,plain,
( op2(e23,e22) != h2(e11)
| spl136_69
| ~ spl136_85
| ~ spl136_86
| ~ spl136_279 ),
inference(forward_demodulation,[],[f6161,f2874]) ).
fof(f6165,plain,
( e23 != op2(e23,e22)
| spl136_69
| ~ spl136_85
| ~ spl136_86
| ~ spl136_279 ),
inference(forward_demodulation,[],[f6163,f1737]) ).
fof(f6166,plain,
( $false
| spl136_69
| ~ spl136_85
| ~ spl136_86
| ~ spl136_187
| ~ spl136_279 ),
inference(forward_subsumption_resolution,[],[f6165,f2254]) ).
fof(f6167,plain,
( spl136_69
| ~ spl136_85
| ~ spl136_86
| ~ spl136_187
| ~ spl136_279 ),
inference(avatar_contradiction_clause,[],[f6166]) ).
fof(f6169,plain,
( op2(e23,e23) != h2(op1(e11,e11))
| spl136_70
| ~ spl136_86 ),
inference(forward_demodulation,[],[f1670,f1737]) ).
fof(f6171,plain,
( op2(e23,e23) != h2(e13)
| spl136_70
| ~ spl136_86
| ~ spl136_375 ),
inference(forward_demodulation,[],[f6169,f3525]) ).
fof(f6173,plain,
( e21 != op2(e23,e23)
| ~ spl136_17
| spl136_70
| ~ spl136_86
| ~ spl136_375 ),
inference(forward_demodulation,[],[f6171,f1421]) ).
fof(f6175,plain,
( $false
| ~ spl136_17
| spl136_70
| ~ spl136_86
| ~ spl136_250
| ~ spl136_375 ),
inference(forward_subsumption_resolution,[],[f6173,f2731]) ).
fof(f6176,plain,
( ~ spl136_17
| spl136_70
| ~ spl136_86
| ~ spl136_250
| ~ spl136_375 ),
inference(avatar_contradiction_clause,[],[f6175]) ).
fof(f6178,plain,
( h2(op1(e11,e12)) != op2(h2(e11),e20)
| ~ spl136_13
| spl136_71 ),
inference(forward_demodulation,[],[f1674,f1402]) ).
fof(f6180,plain,
( op2(e23,e20) != h2(op1(e11,e12))
| ~ spl136_13
| spl136_71
| ~ spl136_86 ),
inference(forward_demodulation,[],[f6178,f1737]) ).
fof(f6182,plain,
( op2(e23,e20) != h2(e10)
| ~ spl136_13
| spl136_71
| ~ spl136_86
| ~ spl136_413 ),
inference(forward_demodulation,[],[f6180,f3734]) ).
fof(f6183,plain,
( e22 != op2(e23,e20)
| ~ spl136_13
| spl136_71
| ~ spl136_85
| ~ spl136_86
| ~ spl136_413 ),
inference(forward_demodulation,[],[f6182,f1732]) ).
fof(f6184,plain,
( $false
| ~ spl136_13
| spl136_71
| ~ spl136_85
| ~ spl136_86
| ~ spl136_384
| ~ spl136_413 ),
inference(forward_subsumption_resolution,[],[f6183,f3567]) ).
fof(f6185,plain,
( ~ spl136_13
| spl136_71
| ~ spl136_85
| ~ spl136_86
| ~ spl136_384
| ~ spl136_413 ),
inference(avatar_contradiction_clause,[],[f6184]) ).
fof(f6187,plain,
( h2(op1(e11,e13)) != op2(h2(e11),e21)
| ~ spl136_17
| spl136_72 ),
inference(forward_demodulation,[],[f1678,f1421]) ).
fof(f6189,plain,
( op2(e23,e21) != h2(op1(e11,e13))
| ~ spl136_17
| spl136_72
| ~ spl136_86 ),
inference(forward_demodulation,[],[f6187,f1737]) ).
fof(f6191,plain,
( op2(e23,e21) != h2(e12)
| ~ spl136_17
| spl136_72
| ~ spl136_86
| ~ spl136_417 ),
inference(forward_demodulation,[],[f6189,f3754]) ).
fof(f6193,plain,
( e20 != op2(e23,e21)
| ~ spl136_13
| ~ spl136_17
| spl136_72
| ~ spl136_86
| ~ spl136_417 ),
inference(forward_demodulation,[],[f6191,f1402]) ).
fof(f6194,plain,
( $false
| ~ spl136_13
| ~ spl136_17
| spl136_72
| ~ spl136_86
| ~ spl136_392
| ~ spl136_417 ),
inference(forward_subsumption_resolution,[],[f6193,f3603]) ).
fof(f6195,plain,
( ~ spl136_13
| ~ spl136_17
| spl136_72
| ~ spl136_86
| ~ spl136_392
| ~ spl136_417 ),
inference(avatar_contradiction_clause,[],[f6194]) ).
fof(f6197,plain,
( h2(op1(e12,e10)) != op2(h2(e12),e22)
| spl136_73
| ~ spl136_85 ),
inference(forward_demodulation,[],[f1682,f1732]) ).
fof(f6199,plain,
( op2(e20,e22) != h2(op1(e12,e10))
| ~ spl136_13
| spl136_73
| ~ spl136_85 ),
inference(forward_demodulation,[],[f6197,f1402]) ).
fof(f6201,plain,
( op2(e20,e22) != h2(e13)
| ~ spl136_13
| spl136_73
| ~ spl136_85
| ~ spl136_412 ),
inference(forward_demodulation,[],[f6199,f3729]) ).
fof(f6203,plain,
( e21 != op2(e20,e22)
| ~ spl136_13
| ~ spl136_17
| spl136_73
| ~ spl136_85
| ~ spl136_412 ),
inference(forward_demodulation,[],[f6201,f1421]) ).
fof(f6204,plain,
( $false
| ~ spl136_13
| ~ spl136_17
| spl136_73
| ~ spl136_85
| ~ spl136_377
| ~ spl136_412 ),
inference(forward_subsumption_resolution,[],[f6203,f3536]) ).
fof(f6205,plain,
( ~ spl136_13
| ~ spl136_17
| spl136_73
| ~ spl136_85
| ~ spl136_377
| ~ spl136_412 ),
inference(avatar_contradiction_clause,[],[f6204]) ).
fof(f6207,plain,
( op2(e20,e20) != h2(op1(e12,e12))
| ~ spl136_13
| spl136_75 ),
inference(forward_demodulation,[],[f1690,f1402]) ).
fof(f6209,plain,
( op2(e20,e20) != h2(e12)
| ~ spl136_13
| spl136_75
| ~ spl136_296 ),
inference(forward_demodulation,[],[f6207,f2966]) ).
fof(f6211,plain,
( e20 != op2(e20,e20)
| ~ spl136_13
| spl136_75
| ~ spl136_296 ),
inference(forward_demodulation,[],[f6209,f1402]) ).
fof(f6216,plain,
( h2(op1(e12,e13)) != op2(h2(e12),e21)
| ~ spl136_17
| spl136_76 ),
inference(forward_demodulation,[],[f1694,f1421]) ).
fof(f6218,plain,
( op2(e20,e21) != h2(op1(e12,e13))
| ~ spl136_13
| ~ spl136_17
| spl136_76 ),
inference(forward_demodulation,[],[f6216,f1402]) ).
fof(f6220,plain,
( op2(e20,e21) != h2(e10)
| ~ spl136_13
| ~ spl136_17
| spl136_76
| ~ spl136_421 ),
inference(forward_demodulation,[],[f6218,f3774]) ).
fof(f6221,plain,
( e22 != op2(e20,e21)
| ~ spl136_13
| ~ spl136_17
| spl136_76
| ~ spl136_85
| ~ spl136_421 ),
inference(forward_demodulation,[],[f6220,f1732]) ).
fof(f6222,plain,
( $false
| ~ spl136_13
| ~ spl136_17
| spl136_76
| ~ spl136_85
| ~ spl136_381
| ~ spl136_421 ),
inference(forward_subsumption_resolution,[],[f6221,f3554]) ).
fof(f6223,plain,
( ~ spl136_13
| ~ spl136_17
| spl136_76
| ~ spl136_85
| ~ spl136_381
| ~ spl136_421 ),
inference(avatar_contradiction_clause,[],[f6222]) ).
fof(f6225,plain,
( h2(op1(e13,e10)) != op2(h2(e13),e22)
| spl136_77
| ~ spl136_85 ),
inference(forward_demodulation,[],[f1698,f1732]) ).
fof(f6227,plain,
( op2(e21,e22) != h2(op1(e13,e10))
| ~ spl136_17
| spl136_77
| ~ spl136_85 ),
inference(forward_demodulation,[],[f6225,f1421]) ).
fof(f6229,plain,
( op2(e21,e22) != h2(e12)
| ~ spl136_17
| spl136_77
| ~ spl136_85
| ~ spl136_408 ),
inference(forward_demodulation,[],[f6227,f3711]) ).
fof(f6231,plain,
( e20 != op2(e21,e22)
| ~ spl136_13
| ~ spl136_17
| spl136_77
| ~ spl136_85
| ~ spl136_408 ),
inference(forward_demodulation,[],[f6229,f1402]) ).
fof(f6232,plain,
( $false
| ~ spl136_13
| ~ spl136_17
| spl136_77
| ~ spl136_85
| ~ spl136_389
| ~ spl136_408 ),
inference(forward_subsumption_resolution,[],[f6231,f3590]) ).
fof(f6233,plain,
( ~ spl136_13
| ~ spl136_17
| spl136_77
| ~ spl136_85
| ~ spl136_389
| ~ spl136_408 ),
inference(avatar_contradiction_clause,[],[f6232]) ).
fof(f6235,plain,
( h2(op1(e13,e11)) != op2(h2(e13),e23)
| spl136_78
| ~ spl136_86 ),
inference(forward_demodulation,[],[f1702,f1737]) ).
fof(f6237,plain,
( op2(e21,e23) != h2(op1(e13,e11))
| ~ spl136_17
| spl136_78
| ~ spl136_86 ),
inference(forward_demodulation,[],[f6235,f1421]) ).
fof(f6239,plain,
( op2(e21,e23) != h2(e10)
| ~ spl136_17
| spl136_78
| ~ spl136_86
| ~ spl136_416 ),
inference(forward_demodulation,[],[f6237,f3747]) ).
fof(f6245,plain,
( h2(op1(e13,e12)) != op2(h2(e13),e20)
| ~ spl136_13
| spl136_79 ),
inference(forward_demodulation,[],[f1706,f1402]) ).
fof(f6247,plain,
( op2(e21,e20) != h2(op1(e13,e12))
| ~ spl136_13
| ~ spl136_17
| spl136_79 ),
inference(forward_demodulation,[],[f6245,f1421]) ).
fof(f6249,plain,
( op2(e21,e20) != h2(e13)
| ~ spl136_13
| ~ spl136_17
| spl136_79
| ~ spl136_307 ),
inference(forward_demodulation,[],[f6247,f3026]) ).
fof(f6251,plain,
( e21 != op2(e21,e20)
| ~ spl136_13
| ~ spl136_17
| spl136_79
| ~ spl136_307 ),
inference(forward_demodulation,[],[f6249,f1421]) ).
fof(f6252,plain,
( $false
| ~ spl136_13
| ~ spl136_17
| spl136_79
| ~ spl136_159
| ~ spl136_307 ),
inference(forward_subsumption_resolution,[],[f6251,f2102]) ).
fof(f6253,plain,
( ~ spl136_13
| ~ spl136_17
| spl136_79
| ~ spl136_159
| ~ spl136_307 ),
inference(avatar_contradiction_clause,[],[f6252]) ).
fof(f6255,plain,
( op2(e21,e21) != h2(op1(e13,e13))
| ~ spl136_17
| spl136_80 ),
inference(forward_demodulation,[],[f1710,f1421]) ).
fof(f6257,plain,
( op2(e21,e21) != h2(e11)
| ~ spl136_17
| spl136_80
| ~ spl136_370 ),
inference(forward_demodulation,[],[f6255,f3503]) ).
fof(f6259,plain,
( e23 != op2(e21,e21)
| ~ spl136_17
| spl136_80
| ~ spl136_86
| ~ spl136_370 ),
inference(forward_demodulation,[],[f6257,f1737]) ).
fof(f6261,plain,
( $false
| ~ spl136_17
| spl136_80
| ~ spl136_86
| ~ spl136_255
| ~ spl136_370 ),
inference(forward_subsumption_resolution,[],[f6259,f2753]) ).
fof(f6262,plain,
( ~ spl136_17
| spl136_80
| ~ spl136_86
| ~ spl136_255
| ~ spl136_370 ),
inference(avatar_contradiction_clause,[],[f6261]) ).
fof(f6267,plain,
( ~ spl136_397
| ~ spl136_13
| spl136_66
| ~ spl136_85
| ~ spl136_86
| ~ spl136_405 ),
inference(avatar_split_clause,[],[f6135,f3696,f1736,f1731,f1652,f1401,f3628]) ).
fof(f6269,plain,
( e21 = e23
| ~ spl136_162
| ~ spl136_255 ),
inference(forward_demodulation,[],[f2118,f2753]) ).
fof(f6271,plain,
( ~ spl136_165
| ~ spl136_379 ),
inference(avatar_split_clause,[],[f5596,f3543,f2133]) ).
fof(f6276,plain,
( spl136_389
| ~ spl136_250
| ~ spl136_393 ),
inference(avatar_split_clause,[],[f5957,f3608,f2729,f3588]) ).
fof(f6279,plain,
( ~ spl136_385
| ~ spl136_255 ),
inference(avatar_split_clause,[],[f5737,f2751,f3570]) ).
fof(f6318,plain,
( $false
| spl136_37
| ~ spl136_136
| ~ spl136_162
| ~ spl136_255 ),
inference(forward_subsumption_resolution,[],[f6269,f3928]) ).
fof(f6319,plain,
( spl136_37
| ~ spl136_136
| ~ spl136_162
| ~ spl136_255 ),
inference(avatar_contradiction_clause,[],[f6318]) ).
fof(f6408,plain,
( e22 != h2(e10)
| ~ spl136_17
| spl136_78
| ~ spl136_86
| ~ spl136_393
| ~ spl136_416 ),
inference(forward_demodulation,[],[f6239,f3610]) ).
fof(f6414,plain,
( ~ spl136_170
| ~ spl136_176 ),
inference(avatar_split_clause,[],[f5402,f2192,f2160]) ).
fof(f6430,plain,
( ~ spl136_252
| ~ spl136_393 ),
inference(avatar_split_clause,[],[f5713,f3608,f2738]) ).
fof(f6432,plain,
( ~ spl136_168
| ~ spl136_250 ),
inference(avatar_split_clause,[],[f5391,f2729,f2149]) ).
fof(f6436,plain,
( ~ spl136_85
| ~ spl136_17
| spl136_78
| ~ spl136_86
| ~ spl136_393
| ~ spl136_416 ),
inference(avatar_split_clause,[],[f6408,f3745,f3608,f1736,f1700,f1420,f1731]) ).
fof(f6441,plain,
( ~ spl136_182
| ~ spl136_13
| spl136_74
| ~ spl136_86
| ~ spl136_285 ),
inference(avatar_split_clause,[],[f5932,f2905,f1736,f1684,f1401,f2225]) ).
fof(f6447,plain,
( ~ spl136_388
| ~ spl136_13
| spl136_67
| ~ spl136_85
| ~ spl136_86
| ~ spl136_401 ),
inference(avatar_split_clause,[],[f6145,f3678,f1736,f1731,f1656,f1401,f3583]) ).
fof(f6454,plain,
( ~ spl136_148
| ~ spl136_13
| spl136_75
| ~ spl136_296 ),
inference(avatar_split_clause,[],[f6211,f2964,f1688,f1401,f2040]) ).
fof(f6517,plain,
( e22 = op2(e20,e23)
| ~ spl136_2
| ~ spl136_7
| ~ spl136_393 ),
inference(superposition,[],[f3610,f4002]) ).
fof(f6521,plain,
( spl136_382
| ~ spl136_2
| ~ spl136_7
| ~ spl136_393 ),
inference(avatar_split_clause,[],[f6517,f3608,f1372,f1348,f3556]) ).
fof(f6564,plain,
( ~ spl136_154
| ~ spl136_148 ),
inference(avatar_split_clause,[],[f5642,f2040,f2073]) ).
fof(f6565,plain,
( e10 = e11
| ~ spl136_284
| ~ spl136_413 ),
inference(forward_demodulation,[],[f2902,f3734]) ).
fof(f6574,plain,
( ~ spl136_410
| ~ spl136_302 ),
inference(avatar_split_clause,[],[f5882,f2997,f3718]) ).
fof(f6600,plain,
( $false
| ~ spl136_284
| ~ spl136_413 ),
inference(forward_subsumption_resolution,[],[f6565,f218]) ).
fof(f6601,plain,
( ~ spl136_284
| ~ spl136_413 ),
inference(avatar_contradiction_clause,[],[f6600]) ).
fof(f6617,plain,
( ~ spl136_412
| ~ spl136_308 ),
inference(avatar_split_clause,[],[f5524,f3029,f3727]) ).
fof(f6624,plain,
( ~ spl136_413
| ~ spl136_422 ),
inference(avatar_split_clause,[],[f5542,f3777,f3732]) ).
fof(f6628,plain,
( spl136_413
| ~ spl136_370
| ~ spl136_417 ),
inference(avatar_split_clause,[],[f5955,f3752,f3501,f3732]) ).
fof(f6634,plain,
( e10 != op1(e10,e13)
| ~ spl136_268 ),
inference(forward_demodulation,[],[f138,f2814]) ).
fof(f6637,plain,
( e13 != op1(e11,e10)
| ~ spl136_375 ),
inference(forward_demodulation,[],[f134,f3525]) ).
fof(f6640,plain,
( ~ spl136_276
| ~ spl136_268 ),
inference(avatar_split_clause,[],[f6634,f2812,f2856]) ).
fof(f6658,plain,
( ~ spl136_411
| ~ spl136_375 ),
inference(avatar_split_clause,[],[f6637,f3523,f3723]) ).
fof(f6665,plain,
( ~ spl136_273
| ~ spl136_413 ),
inference(avatar_split_clause,[],[f5894,f3732,f2840]) ).
fof(f6881,plain,
( e10 = e12
| ~ spl136_268
| ~ spl136_371 ),
inference(superposition,[],[f3508,f2814]) ).
fof(f6886,plain,
( $false
| ~ spl136_268
| ~ spl136_371 ),
inference(forward_subsumption_resolution,[],[f6881,f217]) ).
fof(f6887,plain,
( ~ spl136_268
| ~ spl136_371 ),
inference(avatar_contradiction_clause,[],[f6886]) ).
cnf(s10,plain,
( ~ spl136_11
| ~ spl136_13 ),
inference(sat_conversion,[],[f1404]) ).
cnf(s13,plain,
( spl136_16
| ~ spl136_17 ),
inference(sat_conversion,[],[f1423]) ).
cnf(s56,plain,
( spl136_11
| ~ spl136_16
| ~ spl136_65
| ~ spl136_66
| ~ spl136_67
| ~ spl136_68
| ~ spl136_69
| ~ spl136_70
| ~ spl136_71
| ~ spl136_72
| ~ spl136_73
| ~ spl136_74
| ~ spl136_75
| ~ spl136_76
| ~ spl136_77
| ~ spl136_78
| ~ spl136_79
| ~ spl136_80
| ~ spl136_85
| ~ spl136_86 ),
inference(sat_conversion,[],[f1742]) ).
cnf(s97,plain,
spl136_136,
inference(sat_conversion,[],[f1983]) ).
cnf(s99,plain,
spl136_17,
inference(sat_conversion,[],[f1985]) ).
cnf(s100,plain,
spl136_2,
inference(sat_conversion,[],[f1986]) ).
cnf(s389,plain,
( spl136_148
| spl136_245
| spl136_246
| spl136_247 ),
inference(sat_conversion,[],[f2719]) ).
cnf(s391,plain,
( spl136_176
| spl136_251
| spl136_252
| spl136_253 ),
inference(sat_conversion,[],[f2745]) ).
cnf(s392,plain,
( spl136_190
| spl136_254
| spl136_255
| spl136_256 ),
inference(sat_conversion,[],[f2758]) ).
cnf(s404,plain,
( ~ spl136_267
| spl136_268 ),
inference(sat_conversion,[],[f2818]) ).
cnf(s408,plain,
( spl136_268
| spl136_269 ),
inference(sat_conversion,[],[f2834]) ).
cnf(s409,plain,
( ~ spl136_272
| spl136_273 ),
inference(sat_conversion,[],[f2843]) ).
cnf(s416,plain,
( spl136_268
| ~ spl136_275 ),
inference(sat_conversion,[],[f2866]) ).
cnf(s419,plain,
( spl136_271
| ~ spl136_278 ),
inference(sat_conversion,[],[f2881]) ).
cnf(s422,plain,
( ~ spl136_281
| spl136_282 ),
inference(sat_conversion,[],[f2892]) ).
cnf(s425,plain,
( ~ spl136_283
| spl136_284 ),
inference(sat_conversion,[],[f2903]) ).
cnf(s429,plain,
( spl136_286
| spl136_287 ),
inference(sat_conversion,[],[f2919]) ).
cnf(s436,plain,
( spl136_273
| ~ spl136_289 ),
inference(sat_conversion,[],[f2942]) ).
cnf(s440,plain,
( spl136_273
| ~ spl136_292 ),
inference(sat_conversion,[],[f2958]) ).
cnf(s444,plain,
( spl136_273
| spl136_295 ),
inference(sat_conversion,[],[f2970]) ).
cnf(s448,plain,
( spl136_273
| ~ spl136_297 ),
inference(sat_conversion,[],[f2986]) ).
cnf(s450,plain,
( ~ spl136_300
| spl136_302 ),
inference(sat_conversion,[],[f3000]) ).
cnf(s454,plain,
( spl136_303
| spl136_305 ),
inference(sat_conversion,[],[f3016]) ).
cnf(s457,plain,
( spl136_306
| spl136_307 ),
inference(sat_conversion,[],[f3027]) ).
cnf(s462,plain,
( spl136_309
| spl136_310 ),
inference(sat_conversion,[],[f3044]) ).
cnf(s466,plain,
( spl136_268
| ~ spl136_311 ),
inference(sat_conversion,[],[f3052]) ).
cnf(s470,plain,
( spl136_271
| spl136_312 ),
inference(sat_conversion,[],[f3060]) ).
cnf(s473,plain,
( spl136_273
| ~ spl136_313 ),
inference(sat_conversion,[],[f3067]) ).
cnf(s478,plain,
( spl136_277
| spl136_314 ),
inference(sat_conversion,[],[f3076]) ).
cnf(s484,plain,
( spl136_282
| ~ spl136_315 ),
inference(sat_conversion,[],[f3086]) ).
cnf(s488,plain,
( spl136_282
| spl136_316 ),
inference(sat_conversion,[],[f3094]) ).
cnf(s489,plain,
( spl136_284
| ~ spl136_317 ),
inference(sat_conversion,[],[f3099]) ).
cnf(s493,plain,
( spl136_287
| spl136_318 ),
inference(sat_conversion,[],[f3107]) ).
cnf(s500,plain,
( spl136_284
| ~ spl136_319 ),
inference(sat_conversion,[],[f3118]) ).
cnf(s504,plain,
( spl136_284
| spl136_320 ),
inference(sat_conversion,[],[f3126]) ).
cnf(s508,plain,
( spl136_284
| ~ spl136_321 ),
inference(sat_conversion,[],[f3134]) ).
cnf(s512,plain,
( spl136_284
| spl136_322 ),
inference(sat_conversion,[],[f3142]) ).
cnf(s516,plain,
( spl136_287
| ~ spl136_323 ),
inference(sat_conversion,[],[f3150]) ).
cnf(s520,plain,
( spl136_287
| spl136_324 ),
inference(sat_conversion,[],[f3158]) ).
cnf(s524,plain,
( spl136_287
| spl136_325 ),
inference(sat_conversion,[],[f3166]) ).
cnf(s528,plain,
( spl136_287
| spl136_326 ),
inference(sat_conversion,[],[f3174]) ).
cnf(s530,plain,
( spl136_268
| ~ spl136_327 ),
inference(sat_conversion,[],[f3180]) ).
cnf(s534,plain,
( spl136_271
| spl136_328 ),
inference(sat_conversion,[],[f3188]) ).
cnf(s537,plain,
( spl136_273
| spl136_329 ),
inference(sat_conversion,[],[f3195]) ).
cnf(s542,plain,
( spl136_277
| ~ spl136_330 ),
inference(sat_conversion,[],[f3204]) ).
cnf(s547,plain,
( spl136_294
| spl136_331 ),
inference(sat_conversion,[],[f3213]) ).
cnf(s551,plain,
( spl136_294
| ~ spl136_332 ),
inference(sat_conversion,[],[f3221]) ).
cnf(s555,plain,
( spl136_294
| ~ spl136_333 ),
inference(sat_conversion,[],[f3229]) ).
cnf(s559,plain,
( spl136_294
| ~ spl136_334 ),
inference(sat_conversion,[],[f3237]) ).
cnf(s564,plain,
( spl136_296
| ~ spl136_335 ),
inference(sat_conversion,[],[f3246]) ).
cnf(s566,plain,
( spl136_294
| spl136_336 ),
inference(sat_conversion,[],[f3252]) ).
cnf(s572,plain,
( spl136_296
| ~ spl136_337 ),
inference(sat_conversion,[],[f3262]) ).
cnf(s573,plain,
( spl136_298
| spl136_338 ),
inference(sat_conversion,[],[f3267]) ).
cnf(s580,plain,
( spl136_298
| ~ spl136_339 ),
inference(sat_conversion,[],[f3278]) ).
cnf(s584,plain,
( spl136_298
| ~ spl136_340 ),
inference(sat_conversion,[],[f3286]) ).
cnf(s588,plain,
( spl136_298
| spl136_341 ),
inference(sat_conversion,[],[f3294]) ).
cnf(s592,plain,
( spl136_298
| ~ spl136_342 ),
inference(sat_conversion,[],[f3302]) ).
cnf(s594,plain,
( spl136_268
| spl136_343 ),
inference(sat_conversion,[],[f3308]) ).
cnf(s599,plain,
( spl136_302
| spl136_344 ),
inference(sat_conversion,[],[f3317]) ).
cnf(s601,plain,
( spl136_273
| spl136_345 ),
inference(sat_conversion,[],[f3323]) ).
cnf(s607,plain,
( spl136_302
| ~ spl136_346 ),
inference(sat_conversion,[],[f3333]) ).
cnf(s611,plain,
( spl136_305
| spl136_347 ),
inference(sat_conversion,[],[f3341]) ).
cnf(s615,plain,
( spl136_305
| ~ spl136_348 ),
inference(sat_conversion,[],[f3349]) ).
cnf(s619,plain,
( spl136_305
| ~ spl136_349 ),
inference(sat_conversion,[],[f3357]) ).
cnf(s623,plain,
( spl136_305
| spl136_350 ),
inference(sat_conversion,[],[f3365]) ).
cnf(s628,plain,
( spl136_307
| spl136_351 ),
inference(sat_conversion,[],[f3374]) ).
cnf(s630,plain,
( spl136_294
| spl136_352 ),
inference(sat_conversion,[],[f3380]) ).
cnf(s634,plain,
( spl136_296
| spl136_353 ),
inference(sat_conversion,[],[f3388]) ).
cnf(s637,plain,
( spl136_298
| ~ spl136_354 ),
inference(sat_conversion,[],[f3395]) ).
cnf(s644,plain,
( spl136_310
| spl136_355 ),
inference(sat_conversion,[],[f3406]) ).
cnf(s648,plain,
( spl136_310
| spl136_356 ),
inference(sat_conversion,[],[f3414]) ).
cnf(s680,plain,
( spl136_267
| ~ spl136_269
| spl136_272
| spl136_275
| spl136_278
| spl136_281
| spl136_283
| ~ spl136_286
| spl136_289
| spl136_292
| ~ spl136_295
| spl136_297
| spl136_300
| ~ spl136_303
| ~ spl136_306
| ~ spl136_309
| spl136_310
| spl136_311
| ~ spl136_312
| spl136_313
| ~ spl136_314
| spl136_315
| ~ spl136_316
| spl136_317
| ~ spl136_318
| spl136_319
| ~ spl136_320
| spl136_321
| ~ spl136_322
| spl136_323
| ~ spl136_324
| ~ spl136_325
| ~ spl136_326
| spl136_327
| ~ spl136_328
| ~ spl136_329
| spl136_330
| ~ spl136_331
| spl136_332
| spl136_333
| spl136_334
| spl136_335
| ~ spl136_336
| spl136_337
| ~ spl136_338
| spl136_339
| spl136_340
| ~ spl136_341
| spl136_342
| ~ spl136_343
| ~ spl136_344
| ~ spl136_345
| spl136_346
| ~ spl136_347
| spl136_348
| spl136_349
| ~ spl136_350
| ~ spl136_351
| ~ spl136_352
| ~ spl136_353
| spl136_354
| ~ spl136_355
| ~ spl136_356 ),
inference(sat_conversion,[],[f3478]) ).
cnf(s681,plain,
( spl136_268
| spl136_365
| spl136_366
| spl136_367 ),
inference(sat_conversion,[],[f3491]) ).
cnf(s683,plain,
( spl136_296
| spl136_371
| spl136_372
| spl136_373 ),
inference(sat_conversion,[],[f3517]) ).
cnf(s684,plain,
( spl136_310
| spl136_374
| spl136_375
| spl136_376 ),
inference(sat_conversion,[],[f3530]) ).
cnf(s689,plain,
( spl136_171
| spl136_251
| spl136_381
| spl136_382 ),
inference(sat_conversion,[],[f3559]) ).
cnf(s690,plain,
( spl136_170
| spl136_251
| spl136_383
| spl136_384 ),
inference(sat_conversion,[],[f3568]) ).
cnf(s691,plain,
( spl136_182
| spl136_254
| spl136_385
| spl136_386 ),
inference(sat_conversion,[],[f3577]) ).
cnf(s695,plain,
( spl136_159
| spl136_162
| spl136_164
| spl136_167 ),
inference(sat_conversion,[],[f3605]) ).
cnf(s696,plain,
( spl136_160
| spl136_162
| spl136_165
| spl136_168 ),
inference(sat_conversion,[],[f3606]) ).
cnf(s699,plain,
( spl136_185
| spl136_255
| spl136_387
| spl136_395 ),
inference(sat_conversion,[],[f3621]) ).
cnf(s704,plain,
( spl136_164
| spl136_249
| spl136_377
| spl136_400 ),
inference(sat_conversion,[],[f3646]) ).
cnf(s708,plain,
( spl136_187
| spl136_256
| spl136_386
| spl136_395 ),
inference(sat_conversion,[],[f3650]) ).
cnf(s709,plain,
( spl136_157
| spl136_247
| spl136_392
| spl136_398 ),
inference(sat_conversion,[],[f3651]) ).
cnf(s710,plain,
( spl136_156
| spl136_247
| spl136_390
| spl136_397 ),
inference(sat_conversion,[],[f3652]) ).
cnf(s725,plain,
( spl136_154
| spl136_170
| spl136_379
| spl136_388 ),
inference(sat_conversion,[],[f3667]) ).
cnf(s737,plain,
( spl136_291
| spl136_371
| spl136_405
| spl136_406 ),
inference(sat_conversion,[],[f3703]) ).
cnf(s740,plain,
( spl136_301
| spl136_374
| spl136_411
| spl136_412 ),
inference(sat_conversion,[],[f3730]) ).
cnf(s743,plain,
( spl136_279
| spl136_282
| spl136_284
| spl136_287 ),
inference(sat_conversion,[],[f3749]) ).
cnf(s744,plain,
( spl136_280
| spl136_282
| spl136_285
| spl136_288 ),
inference(sat_conversion,[],[f3750]) ).
cnf(s747,plain,
( spl136_305
| spl136_375
| spl136_411
| spl136_419 ),
inference(sat_conversion,[],[f3765]) ).
cnf(s756,plain,
( spl136_307
| spl136_376
| spl136_410
| spl136_419 ),
inference(sat_conversion,[],[f3794]) ).
cnf(s757,plain,
( spl136_277
| spl136_367
| spl136_416
| spl136_422 ),
inference(sat_conversion,[],[f3795]) ).
cnf(s758,plain,
( spl136_276
| spl136_367
| spl136_414
| spl136_421 ),
inference(sat_conversion,[],[f3796]) ).
cnf(s764,plain,
( spl136_302
| spl136_305
| spl136_308
| spl136_310 ),
inference(sat_conversion,[],[f3802]) ).
cnf(s767,plain,
( spl136_273
| spl136_291
| spl136_401
| spl136_410 ),
inference(sat_conversion,[],[f3805]) ).
cnf(s777,plain,
( spl136_277
| spl136_301
| spl136_404
| spl136_408 ),
inference(sat_conversion,[],[f3815]) ).
cnf(s781,plain,
spl136_370,
inference(sat_conversion,[],[f3822]) ).
cnf(s782,plain,
spl136_250,
inference(sat_conversion,[],[f3823]) ).
cnf(s802,plain,
( spl136_32
| ~ spl136_136
| ~ spl136_156
| ~ spl136_182 ),
inference(sat_conversion,[],[f3895]) ).
cnf(s809,plain,
( ~ spl136_37
| ~ spl136_136 ),
inference(sat_conversion,[],[f3927]) ).
cnf(s817,plain,
( ~ spl136_2
| spl136_7
| ~ spl136_162
| ~ spl136_245 ),
inference(sat_conversion,[],[f3956]) ).
cnf(s818,plain,
( ~ spl136_176
| ~ spl136_246 ),
inference(sat_conversion,[],[f3960]) ).
cnf(s823,plain,
( ~ spl136_32
| ~ spl136_136 ),
inference(sat_conversion,[],[f3985]) ).
cnf(s825,plain,
( ~ spl136_2
| spl136_7
| ~ spl136_246
| ~ spl136_249 ),
inference(sat_conversion,[],[f4001]) ).
cnf(s833,plain,
( spl136_37
| ~ spl136_136
| ~ spl136_190
| ~ spl136_250 ),
inference(sat_conversion,[],[f4041]) ).
cnf(s837,plain,
( ~ spl136_250
| ~ spl136_253 ),
inference(sat_conversion,[],[f4060]) ).
cnf(s839,plain,
( ~ spl136_251
| ~ spl136_254 ),
inference(sat_conversion,[],[f4071]) ).
cnf(s840,plain,
( spl136_32
| ~ spl136_136
| ~ spl136_148
| ~ spl136_254 ),
inference(sat_conversion,[],[f4076]) ).
cnf(s845,plain,
( spl136_32
| ~ spl136_136
| ~ spl136_245
| ~ spl136_255 ),
inference(sat_conversion,[],[f4107]) ).
cnf(s847,plain,
( spl136_32
| ~ spl136_136
| ~ spl136_246
| ~ spl136_256 ),
inference(sat_conversion,[],[f4125]) ).
cnf(s849,plain,
( ~ spl136_271
| ~ spl136_279 ),
inference(sat_conversion,[],[f4143]) ).
cnf(s860,plain,
( ~ spl136_277
| ~ spl136_301 ),
inference(sat_conversion,[],[f4182]) ).
cnf(s862,plain,
( ~ spl136_276
| ~ spl136_302 ),
inference(sat_conversion,[],[f4189]) ).
cnf(s871,plain,
( ~ spl136_310
| ~ spl136_370 ),
inference(sat_conversion,[],[f4221]) ).
cnf(s873,plain,
( ~ spl136_268
| ~ spl136_374 ),
inference(sat_conversion,[],[f4228]) ).
cnf(s875,plain,
( ~ spl136_282
| ~ spl136_365 ),
inference(sat_conversion,[],[f4235]) ).
cnf(s879,plain,
( ~ spl136_176
| ~ spl136_249 ),
inference(sat_conversion,[],[f4251]) ).
cnf(s890,plain,
( ~ spl136_159
| ~ spl136_383 ),
inference(sat_conversion,[],[f4302]) ).
cnf(s891,plain,
( spl136_32
| ~ spl136_136
| ~ spl136_187
| ~ spl136_398 ),
inference(sat_conversion,[],[f4305]) ).
cnf(s893,plain,
( ~ spl136_381
| ~ spl136_385 ),
inference(sat_conversion,[],[f4316]) ).
cnf(s900,plain,
( ~ spl136_390
| ~ spl136_393 ),
inference(sat_conversion,[],[f4354]) ).
cnf(s904,plain,
( spl136_32
| ~ spl136_136
| ~ spl136_389
| ~ spl136_395 ),
inference(sat_conversion,[],[f4371]) ).
cnf(s906,plain,
( spl136_37
| ~ spl136_136
| ~ spl136_159
| ~ spl136_387 ),
inference(sat_conversion,[],[f4379]) ).
cnf(s914,plain,
( ~ spl136_2
| spl136_7
| ~ spl136_247
| ~ spl136_250 ),
inference(sat_conversion,[],[f4421]) ).
cnf(s917,plain,
( ~ spl136_176
| ~ spl136_256 ),
inference(sat_conversion,[],[f4436]) ).
cnf(s919,plain,
( ~ spl136_160
| ~ spl136_381 ),
inference(sat_conversion,[],[f4454]) ).
cnf(s934,plain,
( spl136_37
| ~ spl136_136
| ~ spl136_377
| ~ spl136_386 ),
inference(sat_conversion,[],[f4559]) ).
cnf(s941,plain,
( ~ spl136_2
| spl136_7
| ~ spl136_164
| ~ spl136_389 ),
inference(sat_conversion,[],[f4640]) ).
cnf(s952,plain,
( ~ spl136_280
| ~ spl136_405 ),
inference(sat_conversion,[],[f4738]) ).
cnf(s960,plain,
( ~ spl136_372
| ~ spl136_375 ),
inference(sat_conversion,[],[f4772]) ).
cnf(s962,plain,
( ~ spl136_367
| ~ spl136_370 ),
inference(sat_conversion,[],[f4779]) ).
cnf(s963,plain,
( ~ spl136_296
| ~ spl136_366 ),
inference(sat_conversion,[],[f4782]) ).
cnf(s965,plain,
( ~ spl136_296
| ~ spl136_376 ),
inference(sat_conversion,[],[f4792]) ).
cnf(s970,plain,
( ~ spl136_302
| ~ spl136_406 ),
inference(sat_conversion,[],[f4819]) ).
cnf(s976,plain,
( ~ spl136_371
| ~ spl136_374 ),
inference(sat_conversion,[],[f4843]) ).
cnf(s978,plain,
( ~ spl136_370
| ~ spl136_373 ),
inference(sat_conversion,[],[f4858]) ).
cnf(s980,plain,
( ~ spl136_294
| ~ spl136_413 ),
inference(sat_conversion,[],[f4865]) ).
cnf(s985,plain,
( ~ spl136_279
| ~ spl136_411 ),
inference(sat_conversion,[],[f4912]) ).
cnf(s986,plain,
( ~ spl136_279
| ~ spl136_411 ),
inference(sat_conversion,[],[f4914]) ).
cnf(s993,plain,
( ~ spl136_414
| ~ spl136_417 ),
inference(sat_conversion,[],[f4946]) ).
cnf(s994,plain,
( ~ spl136_308
| ~ spl136_421 ),
inference(sat_conversion,[],[f4950]) ).
cnf(s1015,plain,
( ~ spl136_365
| ~ spl136_375 ),
inference(sat_conversion,[],[f5081]) ).
cnf(s1019,plain,
( ~ spl136_366
| ~ spl136_376 ),
inference(sat_conversion,[],[f5113]) ).
cnf(s1021,plain,
( ~ spl136_282
| ~ spl136_375 ),
inference(sat_conversion,[],[f5126]) ).
cnf(s1025,plain,
( ~ spl136_288
| ~ spl136_416 ),
inference(sat_conversion,[],[f5156]) ).
cnf(s1031,plain,
( ~ spl136_287
| ~ spl136_417 ),
inference(sat_conversion,[],[f5193]) ).
cnf(s1036,plain,
( ~ spl136_413
| ~ spl136_419 ),
inference(sat_conversion,[],[f5218]) ).
cnf(s1043,plain,
( ~ spl136_282
| ~ spl136_372 ),
inference(sat_conversion,[],[f5279]) ).
cnf(s1049,plain,
( ~ spl136_305
| ~ spl136_370 ),
inference(sat_conversion,[],[f5445]) ).
cnf(s1053,plain,
( ~ spl136_370
| spl136_417 ),
inference(sat_conversion,[],[f5453]) ).
cnf(s1054,plain,
( ~ spl136_366
| ~ spl136_421 ),
inference(sat_conversion,[],[f5454]) ).
cnf(s1055,plain,
( ~ spl136_370
| ~ spl136_404 ),
inference(sat_conversion,[],[f5457]) ).
cnf(s1065,plain,
( ~ spl136_185
| ~ spl136_250 ),
inference(sat_conversion,[],[f5559]) ).
cnf(s1069,plain,
( ~ spl136_250
| spl136_393 ),
inference(sat_conversion,[],[f5571]) ).
cnf(s1070,plain,
( ~ spl136_167
| ~ spl136_250 ),
inference(sat_conversion,[],[f5577]) ).
cnf(s1077,plain,
( ~ spl136_382
| ~ spl136_393 ),
inference(sat_conversion,[],[f5588]) ).
cnf(s1083,plain,
( ~ spl136_246
| ~ spl136_397 ),
inference(sat_conversion,[],[f5594]) ).
cnf(s1086,plain,
( ~ spl136_250
| ~ spl136_400 ),
inference(sat_conversion,[],[f5605]) ).
cnf(s1088,plain,
( ~ spl136_148
| ~ spl136_157 ),
inference(sat_conversion,[],[f5609]) ).
cnf(s1094,plain,
( ~ spl136_148
| ~ spl136_251 ),
inference(sat_conversion,[],[f5637]) ).
cnf(s1098,plain,
( ~ spl136_171
| ~ spl136_176 ),
inference(sat_conversion,[],[f5639]) ).
cnf(s1104,plain,
( spl136_86
| ~ spl136_255 ),
inference(sat_conversion,[],[f5697]) ).
cnf(s1118,plain,
( ~ spl136_268
| ~ spl136_277 ),
inference(sat_conversion,[],[f5795]) ).
cnf(s1133,plain,
( ~ spl136_298
| ~ spl136_417 ),
inference(sat_conversion,[],[f5818]) ).
cnf(s1141,plain,
( ~ spl136_301
| ~ spl136_307 ),
inference(sat_conversion,[],[f5824]) ).
cnf(s1147,plain,
( ~ spl136_291
| ~ spl136_296 ),
inference(sat_conversion,[],[f5826]) ).
cnf(s1158,plain,
( spl136_13
| ~ spl136_255
| ~ spl136_392 ),
inference(sat_conversion,[],[f5931]) ).
cnf(s1181,plain,
( spl136_85
| ~ spl136_255
| ~ spl136_384
| ~ spl136_392 ),
inference(sat_conversion,[],[f6125]) ).
cnf(s1182,plain,
( spl136_65
| ~ spl136_85
| ~ spl136_176
| ~ spl136_268 ),
inference(sat_conversion,[],[f6128]) ).
cnf(s1185,plain,
( ~ spl136_17
| spl136_68
| ~ spl136_85
| ~ spl136_165
| ~ spl136_302 ),
inference(sat_conversion,[],[f6157]) ).
cnf(s1186,plain,
( spl136_69
| ~ spl136_85
| ~ spl136_86
| ~ spl136_187
| ~ spl136_279 ),
inference(sat_conversion,[],[f6167]) ).
cnf(s1187,plain,
( ~ spl136_17
| spl136_70
| ~ spl136_86
| ~ spl136_250
| ~ spl136_375 ),
inference(sat_conversion,[],[f6176]) ).
cnf(s1188,plain,
( ~ spl136_13
| spl136_71
| ~ spl136_85
| ~ spl136_86
| ~ spl136_384
| ~ spl136_413 ),
inference(sat_conversion,[],[f6185]) ).
cnf(s1189,plain,
( ~ spl136_13
| ~ spl136_17
| spl136_72
| ~ spl136_86
| ~ spl136_392
| ~ spl136_417 ),
inference(sat_conversion,[],[f6195]) ).
cnf(s1190,plain,
( ~ spl136_13
| ~ spl136_17
| spl136_73
| ~ spl136_85
| ~ spl136_377
| ~ spl136_412 ),
inference(sat_conversion,[],[f6205]) ).
cnf(s1192,plain,
( ~ spl136_13
| ~ spl136_17
| spl136_76
| ~ spl136_85
| ~ spl136_381
| ~ spl136_421 ),
inference(sat_conversion,[],[f6223]) ).
cnf(s1193,plain,
( ~ spl136_13
| ~ spl136_17
| spl136_77
| ~ spl136_85
| ~ spl136_389
| ~ spl136_408 ),
inference(sat_conversion,[],[f6233]) ).
cnf(s1195,plain,
( ~ spl136_13
| ~ spl136_17
| spl136_79
| ~ spl136_159
| ~ spl136_307 ),
inference(sat_conversion,[],[f6253]) ).
cnf(s1196,plain,
( ~ spl136_17
| spl136_80
| ~ spl136_86
| ~ spl136_255
| ~ spl136_370 ),
inference(sat_conversion,[],[f6262]) ).
cnf(s1197,plain,
( ~ spl136_13
| spl136_66
| ~ spl136_85
| ~ spl136_86
| ~ spl136_397
| ~ spl136_405 ),
inference(sat_conversion,[],[f6267]) ).
cnf(s1200,plain,
( ~ spl136_165
| ~ spl136_379 ),
inference(sat_conversion,[],[f6271]) ).
cnf(s1202,plain,
( ~ spl136_250
| spl136_389
| ~ spl136_393 ),
inference(sat_conversion,[],[f6276]) ).
cnf(s1205,plain,
( ~ spl136_255
| ~ spl136_385 ),
inference(sat_conversion,[],[f6279]) ).
cnf(s1232,plain,
( spl136_37
| ~ spl136_136
| ~ spl136_162
| ~ spl136_255 ),
inference(sat_conversion,[],[f6319]) ).
cnf(s1274,plain,
( ~ spl136_170
| ~ spl136_176 ),
inference(sat_conversion,[],[f6414]) ).
cnf(s1310,plain,
( ~ spl136_252
| ~ spl136_393 ),
inference(sat_conversion,[],[f6430]) ).
cnf(s1312,plain,
( ~ spl136_168
| ~ spl136_250 ),
inference(sat_conversion,[],[f6432]) ).
cnf(s1314,plain,
( ~ spl136_17
| spl136_78
| ~ spl136_85
| ~ spl136_86
| ~ spl136_393
| ~ spl136_416 ),
inference(sat_conversion,[],[f6436]) ).
cnf(s1319,plain,
( ~ spl136_13
| spl136_74
| ~ spl136_86
| ~ spl136_182
| ~ spl136_285 ),
inference(sat_conversion,[],[f6441]) ).
cnf(s1324,plain,
( ~ spl136_13
| spl136_67
| ~ spl136_85
| ~ spl136_86
| ~ spl136_388
| ~ spl136_401 ),
inference(sat_conversion,[],[f6447]) ).
cnf(s1328,plain,
( ~ spl136_13
| spl136_75
| ~ spl136_148
| ~ spl136_296 ),
inference(sat_conversion,[],[f6454]) ).
cnf(s1366,plain,
( ~ spl136_2
| ~ spl136_7
| spl136_382
| ~ spl136_393 ),
inference(sat_conversion,[],[f6521]) ).
cnf(s1392,plain,
( ~ spl136_148
| ~ spl136_154 ),
inference(sat_conversion,[],[f6564]) ).
cnf(s1410,plain,
( ~ spl136_302
| ~ spl136_410 ),
inference(sat_conversion,[],[f6574]) ).
cnf(s1418,plain,
( ~ spl136_284
| ~ spl136_413 ),
inference(sat_conversion,[],[f6601]) ).
cnf(s1437,plain,
( ~ spl136_308
| ~ spl136_412 ),
inference(sat_conversion,[],[f6617]) ).
cnf(s1443,plain,
( ~ spl136_413
| ~ spl136_422 ),
inference(sat_conversion,[],[f6624]) ).
cnf(s1445,plain,
( ~ spl136_370
| spl136_413
| ~ spl136_417 ),
inference(sat_conversion,[],[f6628]) ).
cnf(s1448,plain,
( ~ spl136_268
| ~ spl136_276 ),
inference(sat_conversion,[],[f6640]) ).
cnf(s1481,plain,
( ~ spl136_375
| ~ spl136_411 ),
inference(sat_conversion,[],[f6658]) ).
cnf(s1487,plain,
( ~ spl136_273
| ~ spl136_413 ),
inference(sat_conversion,[],[f6665]) ).
cnf(s1527,plain,
( ~ spl136_268
| ~ spl136_371 ),
inference(sat_conversion,[],[f6887]) ).
cnf(s1528,plain,
~ spl136_168,
inference(rat,[],[s1312,s782]) ).
cnf(s1529,plain,
~ spl136_400,
inference(rat,[],[s1086,s782]) ).
cnf(s1531,plain,
~ spl136_167,
inference(rat,[],[s1070,s782]) ).
cnf(s1532,plain,
spl136_393,
inference(rat,[],[s1069,s782]) ).
cnf(s1534,plain,
~ spl136_185,
inference(rat,[],[s1065,s782]) ).
cnf(s1536,plain,
~ spl136_253,
inference(rat,[],[s837,s782]) ).
cnf(s1538,plain,
~ spl136_252,
inference(rat,[],[s1310,s1532]) ).
cnf(s1539,plain,
~ spl136_382,
inference(rat,[],[s1077,s1532]) ).
cnf(s1540,plain,
~ spl136_390,
inference(rat,[],[s900,s1532]) ).
cnf(s1541,plain,
spl136_389,
inference(rat,[],[s1202,s782,s1532]) ).
cnf(s1547,plain,
~ spl136_404,
inference(rat,[],[s1055,s781]) ).
cnf(s1548,plain,
spl136_417,
inference(rat,[],[s1053,s781]) ).
cnf(s1550,plain,
~ spl136_305,
inference(rat,[],[s1049,s781]) ).
cnf(s1551,plain,
~ spl136_373,
inference(rat,[],[s978,s781]) ).
cnf(s1552,plain,
~ spl136_367,
inference(rat,[],[s962,s781]) ).
cnf(s1553,plain,
~ spl136_310,
inference(rat,[],[s871,s781]) ).
cnf(s1554,plain,
~ spl136_298,
inference(rat,[],[s1133,s1548]) ).
cnf(s1555,plain,
~ spl136_287,
inference(rat,[],[s1031,s1548]) ).
cnf(s1556,plain,
~ spl136_414,
inference(rat,[],[s993,s1548]) ).
cnf(s1557,plain,
spl136_413,
inference(rat,[],[s1445,s781,s1548]) ).
cnf(s1558,plain,
~ spl136_273,
inference(rat,[],[s1487,s1557]) ).
cnf(s1559,plain,
~ spl136_422,
inference(rat,[],[s1443,s1557]) ).
cnf(s1560,plain,
~ spl136_284,
inference(rat,[],[s1418,s1557]) ).
cnf(s1561,plain,
~ spl136_419,
inference(rat,[],[s1036,s1557]) ).
cnf(s1562,plain,
~ spl136_294,
inference(rat,[],[s980,s1557]) ).
cnf(s1564,plain,
( spl136_277
| spl136_301
| spl136_408 ),
inference(rat,[],[s777,s1547]) ).
cnf(s1566,plain,
( spl136_291
| spl136_401
| spl136_410 ),
inference(rat,[],[s767,s1558]) ).
cnf(s1567,plain,
( spl136_302
| spl136_308 ),
inference(rat,[],[s764,s1553,s1550]) ).
cnf(s1570,plain,
( spl136_276
| spl136_421 ),
inference(rat,[],[s758,s1556,s1552]) ).
cnf(s1571,plain,
( spl136_277
| spl136_416 ),
inference(rat,[],[s757,s1559,s1552]) ).
cnf(s1572,plain,
( spl136_307
| spl136_376
| spl136_410 ),
inference(rat,[],[s756,s1561]) ).
cnf(s1577,plain,
( spl136_375
| spl136_411 ),
inference(rat,[],[s747,s1561,s1550]) ).
cnf(s1578,plain,
( spl136_279
| spl136_282 ),
inference(rat,[],[s743,s1555,s1560]) ).
cnf(s1590,plain,
( spl136_156
| spl136_247
| spl136_397 ),
inference(rat,[],[s710,s1540]) ).
cnf(s1593,plain,
( spl136_164
| spl136_249
| spl136_377 ),
inference(rat,[],[s704,s1529]) ).
cnf(s1595,plain,
( spl136_255
| spl136_387
| spl136_395 ),
inference(rat,[],[s699,s1534]) ).
cnf(s1597,plain,
( spl136_160
| spl136_162
| spl136_165 ),
inference(rat,[],[s696,s1528]) ).
cnf(s1598,plain,
( spl136_159
| spl136_162
| spl136_164 ),
inference(rat,[],[s695,s1531]) ).
cnf(s1599,plain,
( spl136_171
| spl136_251
| spl136_381 ),
inference(rat,[],[s689,s1539]) ).
cnf(s1603,plain,
( spl136_374
| spl136_375
| spl136_376 ),
inference(rat,[],[s684,s1553]) ).
cnf(s1604,plain,
( spl136_296
| spl136_371
| spl136_372 ),
inference(rat,[],[s683,s1551]) ).
cnf(s1605,plain,
( spl136_268
| spl136_365
| spl136_366 ),
inference(rat,[],[s681,s1552]) ).
cnf(s1606,plain,
( spl136_267
| ~ spl136_269
| spl136_272
| spl136_275
| spl136_278
| spl136_281
| spl136_283
| ~ spl136_286
| spl136_289
| spl136_292
| ~ spl136_295
| spl136_297
| spl136_300
| ~ spl136_303
| ~ spl136_306
| ~ spl136_309
| spl136_311
| ~ spl136_312
| spl136_313
| ~ spl136_314
| spl136_315
| ~ spl136_316
| spl136_317
| ~ spl136_318
| spl136_319
| ~ spl136_320
| spl136_321
| ~ spl136_322
| spl136_323
| ~ spl136_324
| ~ spl136_325
| ~ spl136_326
| spl136_327
| ~ spl136_328
| ~ spl136_329
| spl136_330
| ~ spl136_331
| spl136_332
| spl136_333
| spl136_334
| spl136_335
| ~ spl136_336
| spl136_337
| ~ spl136_338
| spl136_339
| spl136_340
| ~ spl136_341
| spl136_342
| ~ spl136_343
| ~ spl136_344
| ~ spl136_345
| spl136_346
| ~ spl136_347
| spl136_348
| spl136_349
| ~ spl136_350
| ~ spl136_351
| ~ spl136_352
| ~ spl136_353
| spl136_354
| ~ spl136_355
| ~ spl136_356 ),
inference(rat,[],[s680,s1553]) ).
cnf(s1622,plain,
spl136_356,
inference(rat,[],[s648,s1553]) ).
cnf(s1623,plain,
spl136_355,
inference(rat,[],[s644,s1553]) ).
cnf(s1624,plain,
~ spl136_354,
inference(rat,[],[s637,s1554]) ).
cnf(s1625,plain,
spl136_352,
inference(rat,[],[s630,s1562]) ).
cnf(s1626,plain,
spl136_350,
inference(rat,[],[s623,s1550]) ).
cnf(s1627,plain,
~ spl136_349,
inference(rat,[],[s619,s1550]) ).
cnf(s1628,plain,
~ spl136_348,
inference(rat,[],[s615,s1550]) ).
cnf(s1629,plain,
spl136_347,
inference(rat,[],[s611,s1550]) ).
cnf(s1630,plain,
spl136_345,
inference(rat,[],[s601,s1558]) ).
cnf(s1631,plain,
~ spl136_342,
inference(rat,[],[s592,s1554]) ).
cnf(s1632,plain,
spl136_341,
inference(rat,[],[s588,s1554]) ).
cnf(s1633,plain,
~ spl136_340,
inference(rat,[],[s584,s1554]) ).
cnf(s1634,plain,
~ spl136_339,
inference(rat,[],[s580,s1554]) ).
cnf(s1635,plain,
spl136_338,
inference(rat,[],[s573,s1554]) ).
cnf(s1636,plain,
spl136_336,
inference(rat,[],[s566,s1562]) ).
cnf(s1637,plain,
~ spl136_334,
inference(rat,[],[s559,s1562]) ).
cnf(s1638,plain,
~ spl136_333,
inference(rat,[],[s555,s1562]) ).
cnf(s1639,plain,
~ spl136_332,
inference(rat,[],[s551,s1562]) ).
cnf(s1640,plain,
spl136_331,
inference(rat,[],[s547,s1562]) ).
cnf(s1641,plain,
spl136_329,
inference(rat,[],[s537,s1558]) ).
cnf(s1642,plain,
spl136_326,
inference(rat,[],[s528,s1555]) ).
cnf(s1643,plain,
spl136_325,
inference(rat,[],[s524,s1555]) ).
cnf(s1644,plain,
spl136_324,
inference(rat,[],[s520,s1555]) ).
cnf(s1645,plain,
~ spl136_323,
inference(rat,[],[s516,s1555]) ).
cnf(s1646,plain,
spl136_322,
inference(rat,[],[s512,s1560]) ).
cnf(s1647,plain,
~ spl136_321,
inference(rat,[],[s508,s1560]) ).
cnf(s1648,plain,
spl136_320,
inference(rat,[],[s504,s1560]) ).
cnf(s1649,plain,
~ spl136_319,
inference(rat,[],[s500,s1560]) ).
cnf(s1650,plain,
spl136_318,
inference(rat,[],[s493,s1555]) ).
cnf(s1651,plain,
~ spl136_317,
inference(rat,[],[s489,s1560]) ).
cnf(s1652,plain,
~ spl136_313,
inference(rat,[],[s473,s1558]) ).
cnf(s1653,plain,
spl136_309,
inference(rat,[],[s462,s1553]) ).
cnf(s1654,plain,
spl136_303,
inference(rat,[],[s454,s1550]) ).
cnf(s1655,plain,
~ spl136_297,
inference(rat,[],[s448,s1558]) ).
cnf(s1656,plain,
spl136_295,
inference(rat,[],[s444,s1558]) ).
cnf(s1657,plain,
~ spl136_292,
inference(rat,[],[s440,s1558]) ).
cnf(s1658,plain,
~ spl136_289,
inference(rat,[],[s436,s1558]) ).
cnf(s1659,plain,
spl136_286,
inference(rat,[],[s429,s1555]) ).
cnf(s1660,plain,
~ spl136_283,
inference(rat,[],[s425,s1560]) ).
cnf(s1661,plain,
~ spl136_272,
inference(rat,[],[s409,s1558]) ).
cnf(s1662,plain,
( spl136_176
| spl136_251 ),
inference(rat,[],[s391,s1536,s1538]) ).
cnf(s1704,plain,
~ spl136_7,
inference(rat,[],[s1366,s1532,s1539,s100]) ).
cnf(s1705,plain,
~ spl136_164,
inference(rat,[],[s941,s1541,s100,s1704]) ).
cnf(s1706,plain,
~ spl136_247,
inference(rat,[],[s914,s782,s100,s1704]) ).
cnf(s1710,plain,
~ spl136_32,
inference(rat,[],[s823,s97]) ).
cnf(s1711,plain,
~ spl136_37,
inference(rat,[],[s809,s97]) ).
cnf(s1712,plain,
~ spl136_395,
inference(rat,[],[s904,s97,s1541,s1710]) ).
cnf(s1713,plain,
~ spl136_190,
inference(rat,[],[s833,s782,s97,s1711]) ).
cnf(s1728,plain,
spl136_16,
inference(rat,[],[s13,s99]) ).
cnf(s1730,plain,
~ spl136_246,
inference(rat,[],[s1205,s392,s691,s934,s839,s802,s1593,s1662,s1590,s847,s825,s818,s1083,s1713,s97,s1711,s1710,s1705,s1706,s100,s1704]) ).
cnf(s1731,plain,
~ spl136_245,
inference(rat,[],[s906,s1595,s1598,s845,s817,s97,s1711,s1712,s1705,s1710,s100,s1704]) ).
cnf(s1733,plain,
spl136_148,
inference(rat,[],[s389,s1706,s1730,s1731]) ).
cnf(s1734,plain,
~ spl136_154,
inference(rat,[],[s1392,s1733]) ).
cnf(s1738,plain,
~ spl136_251,
inference(rat,[],[s1094,s1733]) ).
cnf(s1739,plain,
~ spl136_157,
inference(rat,[],[s1088,s1733]) ).
cnf(s1741,plain,
~ spl136_254,
inference(rat,[],[s840,s1710,s97,s1733]) ).
cnf(s1745,plain,
spl136_176,
inference(rat,[],[s1662,s1738]) ).
cnf(s1753,plain,
~ spl136_170,
inference(rat,[],[s1274,s1745]) ).
cnf(s1755,plain,
~ spl136_171,
inference(rat,[],[s1098,s1745]) ).
cnf(s1758,plain,
~ spl136_256,
inference(rat,[],[s917,s1745]) ).
cnf(s1759,plain,
~ spl136_249,
inference(rat,[],[s879,s1745]) ).
cnf(s1763,plain,
spl136_381,
inference(rat,[],[s1599,s1738,s1755]) ).
cnf(s1764,plain,
spl136_255,
inference(rat,[],[s392,s1741,s1713,s1758]) ).
cnf(s1765,plain,
spl136_377,
inference(rat,[],[s1593,s1705,s1759]) ).
cnf(s1766,plain,
~ spl136_160,
inference(rat,[],[s919,s1763]) ).
cnf(s1767,plain,
~ spl136_385,
inference(rat,[],[s893,s1763]) ).
cnf(s1772,plain,
spl136_86,
inference(rat,[],[s1104,s1764]) ).
cnf(s1773,plain,
~ spl136_162,
inference(rat,[],[s1232,s1711,s97,s1764]) ).
cnf(s1774,plain,
~ spl136_386,
inference(rat,[],[s934,s1711,s97,s1765]) ).
cnf(s1777,plain,
spl136_165,
inference(rat,[],[s1597,s1773,s1766]) ).
cnf(s1778,plain,
spl136_182,
inference(rat,[],[s691,s1774,s1741,s1767]) ).
cnf(s1779,plain,
spl136_80,
inference(rat,[],[s1196,s781,s1764,s99,s1772]) ).
cnf(s1780,plain,
spl136_159,
inference(rat,[],[s1598,s1705,s1773]) ).
cnf(s1782,plain,
spl136_187,
inference(rat,[],[s708,s1712,s1758,s1774]) ).
cnf(s1783,plain,
~ spl136_379,
inference(rat,[],[s1200,s1777]) ).
cnf(s1784,plain,
~ spl136_156,
inference(rat,[],[s802,s1710,s97,s1778]) ).
cnf(s1785,plain,
~ spl136_383,
inference(rat,[],[s890,s1780]) ).
cnf(s1788,plain,
~ spl136_398,
inference(rat,[],[s891,s1710,s97,s1782]) ).
cnf(s1789,plain,
spl136_388,
inference(rat,[],[s725,s1753,s1734,s1783]) ).
cnf(s1790,plain,
spl136_397,
inference(rat,[],[s1590,s1706,s1784]) ).
cnf(s1791,plain,
spl136_384,
inference(rat,[],[s690,s1753,s1738,s1785]) ).
cnf(s1793,plain,
spl136_392,
inference(rat,[],[s709,s1739,s1706,s1788]) ).
cnf(s1797,plain,
spl136_85,
inference(rat,[],[s1181,s1793,s1764,s1791]) ).
cnf(s1799,plain,
spl136_13,
inference(rat,[],[s1158,s1764,s1793]) ).
cnf(s1801,plain,
spl136_72,
inference(rat,[],[s1189,s1548,s1793,s1772,s99,s1799]) ).
cnf(s1802,plain,
spl136_71,
inference(rat,[],[s1188,s1557,s1791,s1772,s1797,s1799]) ).
cnf(s1803,plain,
~ spl136_11,
inference(rat,[],[s10,s1799]) ).
cnf(s1804,plain,
( ~ spl136_282
| spl136_296
| spl136_268 ),
inference(rat,[],[s1603,s1019,s976,s1605,s1604,s875,s1021,s1043]) ).
cnf(s1805,plain,
( spl136_302
| spl136_296
| spl136_268 ),
inference(rat,[],[s1606,s478,s542,s457,s628,s860,s1141,s740,s1437,s450,s599,s607,s1567,s594,s530,s466,s416,s408,s404,s634,s572,s564,s488,s484,s422,s534,s470,s419,s849,s976,s1604,s960,s1577,s986,s1578,s1804,s1661,s1660,s1659,s1658,s1657,s1656,s1655,s1654,s1653,s1652,s1651,s1650,s1649,s1648,s1647,s1646,s1645,s1644,s1643,s1642,s1641,s1640,s1639,s1638,s1637,s1636,s1635,s1634,s1633,s1632,s1631,s1630,s1629,s1628,s1627,s1626,s1625,s1624,s1623,s1622]) ).
cnf(s1806,plain,
( spl136_296
| spl136_268 ),
inference(rat,[],[s1570,s862,s1054,s1805,s1605,s1015,s1577,s986,s1578,s1804]) ).
cnf(s1807,plain,
~ spl136_365,
inference(rat,[],[s985,s1578,s1577,s875,s1015]) ).
cnf(s1808,plain,
spl136_268,
inference(rat,[],[s963,s1605,s1806,s1807]) ).
cnf(s1809,plain,
~ spl136_371,
inference(rat,[],[s1527,s1808]) ).
cnf(s1811,plain,
~ spl136_276,
inference(rat,[],[s1448,s1808]) ).
cnf(s1814,plain,
~ spl136_277,
inference(rat,[],[s1118,s1808]) ).
cnf(s1815,plain,
~ spl136_374,
inference(rat,[],[s873,s1808]) ).
cnf(s1817,plain,
spl136_65,
inference(rat,[],[s1182,s1797,s1745,s1808]) ).
cnf(s1824,plain,
spl136_421,
inference(rat,[],[s1570,s1811]) ).
cnf(s1832,plain,
spl136_416,
inference(rat,[],[s1571,s1814]) ).
cnf(s1836,plain,
~ spl136_308,
inference(rat,[],[s994,s1824]) ).
cnf(s1838,plain,
spl136_76,
inference(rat,[],[s1192,s1799,s1763,s1797,s99,s1824]) ).
cnf(s1839,plain,
~ spl136_288,
inference(rat,[],[s1025,s1832]) ).
cnf(s1842,plain,
spl136_78,
inference(rat,[],[s1314,s1797,s1532,s1772,s99,s1832]) ).
cnf(s1843,plain,
spl136_302,
inference(rat,[],[s1567,s1836]) ).
cnf(s1847,plain,
~ spl136_410,
inference(rat,[],[s1410,s1843]) ).
cnf(s1848,plain,
~ spl136_406,
inference(rat,[],[s970,s1843]) ).
cnf(s1851,plain,
spl136_68,
inference(rat,[],[s1185,s1797,s1777,s99,s1843]) ).
cnf(s1852,plain,
~ spl136_372,
inference(rat,[],[s985,s1577,s1578,s960,s1043]) ).
cnf(s1853,plain,
spl136_296,
inference(rat,[],[s1604,s1809,s1852]) ).
cnf(s1854,plain,
~ spl136_291,
inference(rat,[],[s1147,s1853]) ).
cnf(s1857,plain,
~ spl136_376,
inference(rat,[],[s965,s1853]) ).
cnf(s1860,plain,
spl136_75,
inference(rat,[],[s1328,s1799,s1733,s1853]) ).
cnf(s1863,plain,
spl136_405,
inference(rat,[],[s737,s1809,s1848,s1854]) ).
cnf(s1864,plain,
spl136_401,
inference(rat,[],[s1566,s1847,s1854]) ).
cnf(s1865,plain,
spl136_375,
inference(rat,[],[s1603,s1815,s1857]) ).
cnf(s1866,plain,
spl136_307,
inference(rat,[],[s1572,s1847,s1857]) ).
cnf(s1869,plain,
~ spl136_280,
inference(rat,[],[s952,s1863]) ).
cnf(s1871,plain,
spl136_66,
inference(rat,[],[s1197,s1799,s1790,s1772,s1797,s1863]) ).
cnf(s1875,plain,
spl136_67,
inference(rat,[],[s1324,s1799,s1789,s1772,s1797,s1864]) ).
cnf(s1876,plain,
~ spl136_411,
inference(rat,[],[s1481,s1865]) ).
cnf(s1877,plain,
~ spl136_282,
inference(rat,[],[s1021,s1865]) ).
cnf(s1879,plain,
spl136_70,
inference(rat,[],[s1187,s1772,s782,s99,s1865]) ).
cnf(s1880,plain,
~ spl136_301,
inference(rat,[],[s1141,s1866]) ).
cnf(s1882,plain,
spl136_79,
inference(rat,[],[s1195,s1799,s1780,s99,s1866]) ).
cnf(s1886,plain,
spl136_285,
inference(rat,[],[s744,s1877,s1839,s1869]) ).
cnf(s1887,plain,
spl136_279,
inference(rat,[],[s1578,s1877]) ).
cnf(s1890,plain,
spl136_408,
inference(rat,[],[s1564,s1814,s1880]) ).
cnf(s1891,plain,
spl136_412,
inference(rat,[],[s740,s1815,s1876,s1880]) ).
cnf(s1896,plain,
spl136_74,
inference(rat,[],[s1319,s1799,s1778,s1772,s1886]) ).
cnf(s1899,plain,
spl136_69,
inference(rat,[],[s1186,s1797,s1782,s1772,s1887]) ).
cnf(s1901,plain,
spl136_77,
inference(rat,[],[s1193,s1799,s1541,s1797,s99,s1890]) ).
cnf(s1904,plain,
spl136_73,
inference(rat,[],[s1190,s1799,s1765,s1797,s99,s1891]) ).
cnf(s1905,plain,
$false,
inference(rat,[],[s56,s1772,s1797,s1779,s1842,s1838,s1860,s1896,s1904,s1879,s1882,s1801,s1802,s1851,s1875,s1871,s1817,s1803,s1728,s1899,s1901]) ).
fof(f6888,plain,
$false,
inference(avatar_sat_refutation,[],[s1905]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG115+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 % Computer : n026.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Mon Sep 28 19:33:14 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.25 Running first-order model finding
% 0.09/0.25 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.48 % (4173631)Will run a generic schedule for satisfiability detection.
% 0.82/0.48 % (4173640)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1980538182:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.82/0.48 % (4173637)% WARNING: option uhcvi not known.
% 0.82/0.48 % (4173636)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1123290543_2999 on theBenchmark for (2999ds/0Mi)
% 0.82/0.48 % (4173637)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4042481579:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.82/0.48 % (4173638)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2608925200:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.82/0.48 % (4173639)dis+10_1_sil=32000:sp=arity:random_seed=1026068680:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.82/0.48 % (4173641)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1174520743:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.82/0.48 % (4173642)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1876390396:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.82/0.48 % (4173640)Instruction limit reached!
% 0.82/0.48 % (4173640)------------------------------
% 0.82/0.48 % (4173640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.48 % (4173640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.48 % (4173640)CaDiCaL version: 2.1.3
% 0.82/0.48 % (4173640)Termination reason: Instruction limit
% 0.82/0.48 % (4173640)Termination phase: Saturation
% 0.82/0.48 % (4173640)Time elapsed: 0.027 s
% 0.82/0.48 % (4173640)Peak memory usage: 12 MB
% 0.82/0.48 % (4173640)Instructions burned: 117 (million)
% 0.82/0.48 % (4173650)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=543134842:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.82/0.48 % Detected minimum model sizes of [8]
% 0.82/0.48 % Detected maximum model sizes of [max]
% 0.82/0.48 % TRYING [8]
% 0.82/0.48 % (4173639)Instruction limit reached!
% 0.82/0.48 % (4173639)------------------------------
% 0.82/0.48 % (4173639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.48 % (4173639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.48 % (4173639)CaDiCaL version: 2.1.3
% 0.82/0.48 % (4173639)Termination reason: Instruction limit
% 0.82/0.48 % (4173639)Termination phase: Saturation
% 0.82/0.48 % (4173639)Time elapsed: 0.051 s
% 0.82/0.48 % (4173639)Peak memory usage: 13 MB
% 0.82/0.48 % (4173639)Instructions burned: 103 (million)
% 0.82/0.48 % Detected minimum model sizes of [8]
% 0.82/0.48 % Detected maximum model sizes of [max]
% 0.82/0.48 % TRYING [8]
% 0.82/0.48 % (4173641)Instruction limit reached!
% 0.82/0.48 % (4173641)------------------------------
% 0.82/0.48 % (4173641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.48 % (4173641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.48 % (4173641)CaDiCaL version: 2.1.3
% 0.82/0.48 % (4173641)Termination reason: Instruction limit
% 0.82/0.48 % (4173641)Termination phase: Saturation
% 0.82/0.48 % (4173641)Time elapsed: 0.066 s
% 0.82/0.48 % (4173641)Peak memory usage: 14 MB
% 0.82/0.48 % (4173641)Instructions burned: 132 (million)
% 0.82/0.48 % (4173652)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1141669237:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.82/0.48 % (4173653)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=4256359485:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.82/0.48 % (4173642)Instruction limit reached!
% 0.82/0.48 % (4173642)------------------------------
% 0.82/0.48 % (4173642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.48 % (4173642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.48 % (4173642)CaDiCaL version: 2.1.3
% 0.82/0.48 % (4173642)Termination reason: Instruction limit
% 0.82/0.48 % (4173642)Termination phase: Saturation
% 0.82/0.48 % (4173642)Time elapsed: 0.095 s
% 0.82/0.48 % (4173642)Peak memory usage: 14 MB
% 0.82/0.48 % (4173642)Instructions burned: 159 (million)
% 0.82/0.48 % (4173656)ott-21_1_sil=16000:fs=off:random_seed=3924148845:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.82/0.48 % TRYING [9]
% 0.82/0.48 % (4173652)Instruction limit reached!
% 0.82/0.48 % (4173652)------------------------------
% 0.82/0.48 % (4173652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.48 % (4173652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.48 % (4173652)CaDiCaL version: 2.1.3
% 0.82/0.48 % (4173652)Termination reason: Instruction limit
% 0.82/0.48 % (4173652)Termination phase: Saturation
% 0.82/0.48 % (4173652)Time elapsed: 0.064 s
% 0.82/0.48 % (4173652)Peak memory usage: 13 MB
% 0.82/0.48 % (4173652)Instructions burned: 131 (million)
% 0.82/0.48 % (4173637) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4173631-4173637"...
% 0.82/0.48 % (4173658)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3309588735:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 0.82/0.48 % (4173637)...printing done.
% 0.82/0.48 % (4173637)Refutation found. Thanks to Tanya!
% 0.82/0.48 % SZS status Theorem for theBenchmark
% 0.82/0.48 % SZS output start Proof for theBenchmark
% See solution above
% 1.57/0.49 % (4173637)------------------------------
% 1.57/0.49 % (4173637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.49 % (4173637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.49 % (4173637)CaDiCaL version: 2.1.3
% 1.57/0.49 % (4173637)Termination reason: Refutation
% 1.57/0.49 % (4173637)Time elapsed: 0.161 s
% 1.57/0.49 % (4173637)Peak memory usage: 16 MB
% 1.57/0.49 % (4173637)Instructions burned: 317 (million)
% 1.57/0.49 % (4173631)Success in time 0.215 s
% 1.57/0.49 % Vampire exiting
%------------------------------------------------------------------------------