%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG080+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:09:31 AM UTC 2026
% Result : Theorem 4.25s 1.29s
% Output : Refutation 5.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 41
% Syntax : Number of formulae : 901 ( 93 unt; 36 def)
% Number of atoms : 3002 (1036 equ)
% Maximal formula atoms : 110 ( 3 avg)
% Number of connectives : 3855 (1754 ~;1723 |; 340 &)
% ( 36 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 70 ( 4 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 38 ( 36 usr; 37 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e10 != e14
& e11 != e12
& e11 != e13
& e11 != e14
& e12 != e13
& e12 != e14
& e13 != e14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e20 != e24
& e21 != e22
& e21 != e23
& e21 != e24
& e22 != e23
& e22 != e24
& e23 != e24 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f4,axiom,
( op1(e10,e10) = e10
& op1(e10,e11) = e11
& op1(e10,e12) = e12
& op1(e10,e13) = e13
& op1(e10,e14) = e14
& op1(e11,e10) = e11
& op1(e11,e11) = e10
& op1(e11,e12) = e14
& op1(e11,e13) = e12
& op1(e11,e14) = e13
& op1(e12,e10) = e12
& op1(e12,e11) = e14
& op1(e12,e12) = e13
& op1(e12,e13) = e10
& op1(e12,e14) = e11
& op1(e13,e10) = e13
& op1(e13,e11) = e12
& op1(e13,e12) = e11
& op1(e13,e13) = e14
& op1(e13,e14) = e10
& op1(e14,e10) = e14
& op1(e14,e11) = e13
& op1(e14,e12) = e10
& op1(e14,e13) = e11
& op1(e14,e14) = e12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op2(e20,e20) = e20
& op2(e20,e21) = e21
& op2(e20,e22) = e22
& op2(e20,e23) = e23
& op2(e20,e24) = e24
& op2(e21,e20) = e21
& op2(e21,e21) = e22
& op2(e21,e22) = e24
& op2(e21,e23) = e20
& op2(e21,e24) = e23
& op2(e22,e20) = e22
& op2(e22,e21) = e20
& op2(e22,e22) = e23
& op2(e22,e23) = e24
& op2(e22,e24) = e21
& op2(e23,e20) = e23
& op2(e23,e21) = e24
& op2(e23,e22) = e20
& op2(e23,e23) = e21
& op2(e23,e24) = e22
& op2(e24,e20) = e24
& op2(e24,e21) = e23
& op2(e24,e22) = e21
& op2(e24,e23) = e22
& op2(e24,e24) = e20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,conjecture,
( ( ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14 ) )
=> ~ ( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f7,negated_conjecture,
~ ( ( ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14 ) )
=> ~ ( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14 ) ),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f8,plain,
( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14
& ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14 ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f9,plain,
( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14
& ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14 ) ),
inference(flattening,[],[f8]) ).
fof(f10,plain,
( e10 = j(e24)
| e11 = j(e24)
| e12 = j(e24)
| e13 = j(e24)
| e14 = j(e24) ),
inference(cnf_transformation,[],[f9]) ).
fof(f11,plain,
( e10 = j(e23)
| e11 = j(e23)
| e12 = j(e23)
| e13 = j(e23)
| e14 = j(e23) ),
inference(cnf_transformation,[],[f9]) ).
fof(f12,plain,
( e10 = j(e22)
| e11 = j(e22)
| e12 = j(e22)
| e13 = j(e22)
| e14 = j(e22) ),
inference(cnf_transformation,[],[f9]) ).
fof(f13,plain,
( e10 = j(e21)
| e11 = j(e21)
| e12 = j(e21)
| e13 = j(e21)
| e14 = j(e21) ),
inference(cnf_transformation,[],[f9]) ).
fof(f14,plain,
( e10 = j(e20)
| e11 = j(e20)
| e12 = j(e20)
| e13 = j(e20)
| e14 = j(e20) ),
inference(cnf_transformation,[],[f9]) ).
fof(f18,plain,
( e20 = h(e11)
| e21 = h(e11)
| e22 = h(e11)
| e23 = h(e11)
| e24 = h(e11) ),
inference(cnf_transformation,[],[f9]) ).
fof(f23,plain,
e11 = j(h(e11)),
inference(cnf_transformation,[],[f9]) ).
fof(f25,plain,
e24 = h(j(e24)),
inference(cnf_transformation,[],[f9]) ).
fof(f26,plain,
e23 = h(j(e23)),
inference(cnf_transformation,[],[f9]) ).
fof(f27,plain,
e22 = h(j(e22)),
inference(cnf_transformation,[],[f9]) ).
fof(f28,plain,
e21 = h(j(e21)),
inference(cnf_transformation,[],[f9]) ).
fof(f29,plain,
e20 = h(j(e20)),
inference(cnf_transformation,[],[f9]) ).
fof(f30,plain,
j(op2(e24,e24)) = op1(j(e24),j(e24)),
inference(cnf_transformation,[],[f9]) ).
fof(f31,plain,
j(op2(e24,e23)) = op1(j(e24),j(e23)),
inference(cnf_transformation,[],[f9]) ).
fof(f32,plain,
j(op2(e24,e22)) = op1(j(e24),j(e22)),
inference(cnf_transformation,[],[f9]) ).
fof(f33,plain,
j(op2(e24,e21)) = op1(j(e24),j(e21)),
inference(cnf_transformation,[],[f9]) ).
fof(f34,plain,
j(op2(e24,e20)) = op1(j(e24),j(e20)),
inference(cnf_transformation,[],[f9]) ).
fof(f35,plain,
j(op2(e23,e24)) = op1(j(e23),j(e24)),
inference(cnf_transformation,[],[f9]) ).
fof(f36,plain,
j(op2(e23,e23)) = op1(j(e23),j(e23)),
inference(cnf_transformation,[],[f9]) ).
fof(f37,plain,
j(op2(e23,e22)) = op1(j(e23),j(e22)),
inference(cnf_transformation,[],[f9]) ).
fof(f38,plain,
j(op2(e23,e21)) = op1(j(e23),j(e21)),
inference(cnf_transformation,[],[f9]) ).
fof(f80,plain,
e20 = op2(e24,e24),
inference(cnf_transformation,[],[f5]) ).
fof(f81,plain,
e22 = op2(e24,e23),
inference(cnf_transformation,[],[f5]) ).
fof(f82,plain,
e21 = op2(e24,e22),
inference(cnf_transformation,[],[f5]) ).
fof(f83,plain,
e23 = op2(e24,e21),
inference(cnf_transformation,[],[f5]) ).
fof(f84,plain,
e24 = op2(e24,e20),
inference(cnf_transformation,[],[f5]) ).
fof(f85,plain,
e22 = op2(e23,e24),
inference(cnf_transformation,[],[f5]) ).
fof(f86,plain,
e21 = op2(e23,e23),
inference(cnf_transformation,[],[f5]) ).
fof(f87,plain,
e20 = op2(e23,e22),
inference(cnf_transformation,[],[f5]) ).
fof(f88,plain,
e24 = op2(e23,e21),
inference(cnf_transformation,[],[f5]) ).
fof(f105,plain,
e12 = op1(e14,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f107,plain,
e10 = op1(e14,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f108,plain,
e13 = op1(e14,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f110,plain,
e10 = op1(e13,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f112,plain,
e11 = op1(e13,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f113,plain,
e12 = op1(e13,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f114,plain,
e13 = op1(e13,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f115,plain,
e11 = op1(e12,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f116,plain,
e10 = op1(e12,e13),
inference(cnf_transformation,[],[f4]) ).
fof(f117,plain,
e13 = op1(e12,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f119,plain,
e12 = op1(e12,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f120,plain,
e13 = op1(e11,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f121,plain,
e12 = op1(e11,e13),
inference(cnf_transformation,[],[f4]) ).
fof(f123,plain,
e10 = op1(e11,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f124,plain,
e11 = op1(e11,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f128,plain,
e11 = op1(e10,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f129,plain,
e10 = op1(e10,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f155,plain,
e23 != e24,
inference(cnf_transformation,[],[f2]) ).
fof(f156,plain,
e22 != e24,
inference(cnf_transformation,[],[f2]) ).
fof(f157,plain,
e22 != e23,
inference(cnf_transformation,[],[f2]) ).
fof(f160,plain,
e21 != e22,
inference(cnf_transformation,[],[f2]) ).
fof(f161,plain,
e20 != e24,
inference(cnf_transformation,[],[f2]) ).
fof(f162,plain,
e20 != e23,
inference(cnf_transformation,[],[f2]) ).
fof(f163,plain,
e20 != e22,
inference(cnf_transformation,[],[f2]) ).
fof(f164,plain,
e20 != e21,
inference(cnf_transformation,[],[f2]) ).
fof(f165,plain,
e13 != e14,
inference(cnf_transformation,[],[f1]) ).
fof(f166,plain,
e12 != e14,
inference(cnf_transformation,[],[f1]) ).
fof(f167,plain,
e12 != e13,
inference(cnf_transformation,[],[f1]) ).
fof(f168,plain,
e11 != e14,
inference(cnf_transformation,[],[f1]) ).
fof(f169,plain,
e11 != e13,
inference(cnf_transformation,[],[f1]) ).
fof(f170,plain,
e11 != e12,
inference(cnf_transformation,[],[f1]) ).
fof(f171,plain,
e10 != e14,
inference(cnf_transformation,[],[f1]) ).
fof(f172,plain,
e10 != e13,
inference(cnf_transformation,[],[f1]) ).
fof(f173,plain,
e10 != e12,
inference(cnf_transformation,[],[f1]) ).
fof(f174,plain,
e10 != e11,
inference(cnf_transformation,[],[f1]) ).
fof(f176,definition,
( spl0_1
<=> e14 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f178,plain,
( e14 = j(e24)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f180,definition,
( spl0_2
<=> e13 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f182,plain,
( e13 = j(e24)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f184,definition,
( spl0_3
<=> e12 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f186,plain,
( e12 = j(e24)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f188,definition,
( spl0_4
<=> e11 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f190,plain,
( e11 = j(e24)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f192,definition,
( spl0_5
<=> e10 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f194,plain,
( e10 = j(e24)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f195,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5 ),
inference(avatar_split_clause,[],[f10,f192,f188,f184,f180,f176]) ).
fof(f197,definition,
( spl0_6
<=> e14 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f199,plain,
( e14 = j(e23)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f197]) ).
fof(f201,definition,
( spl0_7
<=> e13 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f203,plain,
( e13 = j(e23)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f205,definition,
( spl0_8
<=> e12 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f207,plain,
( e12 = j(e23)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f209,definition,
( spl0_9
<=> e11 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f211,plain,
( e11 = j(e23)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f209]) ).
fof(f213,definition,
( spl0_10
<=> e10 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f215,plain,
( e10 = j(e23)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f213]) ).
fof(f216,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10 ),
inference(avatar_split_clause,[],[f11,f213,f209,f205,f201,f197]) ).
fof(f218,definition,
( spl0_11
<=> e14 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f220,plain,
( e14 = j(e22)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f218]) ).
fof(f222,definition,
( spl0_12
<=> e13 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f224,plain,
( e13 = j(e22)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f222]) ).
fof(f226,definition,
( spl0_13
<=> e12 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f228,plain,
( e12 = j(e22)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f230,definition,
( spl0_14
<=> e11 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f232,plain,
( e11 = j(e22)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f234,definition,
( spl0_15
<=> e10 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f236,plain,
( e10 = j(e22)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f234]) ).
fof(f237,plain,
( spl0_11
| spl0_12
| spl0_13
| spl0_14
| spl0_15 ),
inference(avatar_split_clause,[],[f12,f234,f230,f226,f222,f218]) ).
fof(f239,definition,
( spl0_16
<=> e14 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f241,plain,
( e14 = j(e21)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f243,definition,
( spl0_17
<=> e13 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f245,plain,
( e13 = j(e21)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f247,definition,
( spl0_18
<=> e12 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f249,plain,
( e12 = j(e21)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f251,definition,
( spl0_19
<=> e11 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f253,plain,
( e11 = j(e21)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f255,definition,
( spl0_20
<=> e10 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f257,plain,
( e10 = j(e21)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f258,plain,
( spl0_16
| spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(avatar_split_clause,[],[f13,f255,f251,f247,f243,f239]) ).
fof(f260,definition,
( spl0_21
<=> e14 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f262,plain,
( e14 = j(e20)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f264,definition,
( spl0_22
<=> e13 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f266,plain,
( e13 = j(e20)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f268,definition,
( spl0_23
<=> e12 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f270,plain,
( e12 = j(e20)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f272,definition,
( spl0_24
<=> e11 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f274,plain,
( e11 = j(e20)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f272]) ).
fof(f276,definition,
( spl0_25
<=> e10 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f278,plain,
( e10 = j(e20)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f279,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_25 ),
inference(avatar_split_clause,[],[f14,f276,f272,f268,f264,f260]) ).
fof(f327,definition,
( spl0_37
<=> e23 = h(e12) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f329,plain,
( e23 = h(e12)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f331,definition,
( spl0_38
<=> e22 = h(e12) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f333,plain,
( e22 = h(e12)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f331]) ).
fof(f335,definition,
( spl0_39
<=> e21 = h(e12) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f337,plain,
( e21 = h(e12)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f339,definition,
( spl0_40
<=> e20 = h(e12) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f340,plain,
( e20 != h(e12)
| spl0_40 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f341,plain,
( e20 = h(e12)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f344,definition,
( spl0_41
<=> e24 = h(e11) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f346,plain,
( e24 = h(e11)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f344]) ).
fof(f348,definition,
( spl0_42
<=> e23 = h(e11) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f350,plain,
( e23 = h(e11)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f352,definition,
( spl0_43
<=> e22 = h(e11) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f354,plain,
( e22 = h(e11)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f356,definition,
( spl0_44
<=> e21 = h(e11) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f358,plain,
( e21 = h(e11)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f360,definition,
( spl0_45
<=> e20 = h(e11) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f361,plain,
( e20 != h(e11)
| spl0_45 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f362,plain,
( e20 = h(e11)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f363,plain,
( spl0_41
| spl0_42
| spl0_43
| spl0_44
| spl0_45 ),
inference(avatar_split_clause,[],[f18,f360,f356,f352,f348,f344]) ).
fof(f373,definition,
( spl0_48
<=> e22 = h(e10) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f374,plain,
( e22 != h(e10)
| spl0_48 ),
inference(avatar_component_clause,[],[f373]) ).
fof(f375,plain,
( e22 = h(e10)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f373]) ).
fof(f381,definition,
( spl0_50
<=> e20 = h(e10) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f383,plain,
( e20 = h(e10)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f381]) ).
fof(f385,plain,
j(e20) = op1(j(e24),j(e24)),
inference(forward_demodulation,[],[f30,f80]) ).
fof(f386,plain,
j(e22) = op1(j(e24),j(e23)),
inference(forward_demodulation,[],[f31,f81]) ).
fof(f387,plain,
j(e21) = op1(j(e24),j(e22)),
inference(forward_demodulation,[],[f32,f82]) ).
fof(f388,plain,
j(e23) = op1(j(e24),j(e21)),
inference(forward_demodulation,[],[f33,f83]) ).
fof(f389,plain,
j(e24) = op1(j(e24),j(e20)),
inference(forward_demodulation,[],[f34,f84]) ).
fof(f390,plain,
j(e22) = op1(j(e23),j(e24)),
inference(forward_demodulation,[],[f35,f85]) ).
fof(f391,plain,
j(e21) = op1(j(e23),j(e23)),
inference(forward_demodulation,[],[f36,f86]) ).
fof(f392,plain,
j(e20) = op1(j(e23),j(e22)),
inference(forward_demodulation,[],[f37,f87]) ).
fof(f393,plain,
j(e24) = op1(j(e23),j(e21)),
inference(forward_demodulation,[],[f38,f88]) ).
fof(f460,plain,
( e11 = j(e24)
| ~ spl0_41 ),
inference(superposition,[],[f23,f346]) ).
fof(f461,plain,
( spl0_4
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f460,f344,f188]) ).
fof(f463,plain,
( e11 = j(e23)
| ~ spl0_42 ),
inference(superposition,[],[f23,f350]) ).
fof(f464,plain,
( spl0_9
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f463,f348,f209]) ).
fof(f467,plain,
( e11 = j(e22)
| ~ spl0_43 ),
inference(superposition,[],[f23,f354]) ).
fof(f468,plain,
( spl0_14
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f467,f352,f230]) ).
fof(f479,plain,
( e11 = j(e21)
| ~ spl0_44 ),
inference(superposition,[],[f23,f358]) ).
fof(f480,plain,
( spl0_19
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f479,f356,f251]) ).
fof(f556,plain,
( e11 = j(e20)
| ~ spl0_45 ),
inference(superposition,[],[f23,f362]) ).
fof(f557,plain,
( spl0_24
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f556,f360,f272]) ).
fof(f626,plain,
( e23 = h(e12)
| ~ spl0_8 ),
inference(superposition,[],[f26,f207]) ).
fof(f629,plain,
( e20 = h(e10)
| ~ spl0_25 ),
inference(superposition,[],[f29,f278]) ).
fof(f633,plain,
( j(e22) = op1(j(e24),e12)
| ~ spl0_8 ),
inference(superposition,[],[f386,f207]) ).
fof(f654,plain,
( j(e22) = op1(e12,j(e24))
| ~ spl0_8 ),
inference(superposition,[],[f390,f207]) ).
fof(f660,plain,
( op1(e12,e12) = j(e21)
| ~ spl0_8 ),
inference(superposition,[],[f391,f207]) ).
fof(f663,plain,
( j(e20) = op1(j(e23),e14)
| ~ spl0_11 ),
inference(superposition,[],[f392,f220]) ).
fof(f664,plain,
( op1(e12,e14) = j(e20)
| ~ spl0_8
| ~ spl0_11 ),
inference(forward_demodulation,[],[f663,f207]) ).
fof(f668,plain,
( j(e24) = op1(e12,j(e21))
| ~ spl0_8 ),
inference(superposition,[],[f393,f207]) ).
fof(f671,plain,
( op1(e12,e13) = j(e24)
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_demodulation,[],[f668,f245]) ).
fof(f673,plain,
( e11 = op1(e12,e13)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_demodulation,[],[f671,f190]) ).
fof(f675,plain,
( e10 = e11
| ~ spl0_4
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_demodulation,[],[f673,f116]) ).
fof(f678,plain,
( $false
| ~ spl0_4
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f675,f174]) ).
fof(f679,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f678]) ).
fof(f722,plain,
( e11 = j(e20)
| ~ spl0_8
| ~ spl0_11 ),
inference(forward_demodulation,[],[f664,f115]) ).
fof(f748,plain,
( e24 = h(e10)
| ~ spl0_5 ),
inference(superposition,[],[f25,f194]) ).
fof(f750,plain,
( op1(e10,e10) = j(e20)
| ~ spl0_5 ),
inference(superposition,[],[f385,f194]) ).
fof(f761,plain,
( e11 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_24 ),
inference(forward_demodulation,[],[f750,f274]) ).
fof(f766,plain,
( e10 = e11
| ~ spl0_5
| ~ spl0_24 ),
inference(forward_demodulation,[],[f761,f129]) ).
fof(f768,plain,
( $false
| ~ spl0_5
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f766,f174]) ).
fof(f769,plain,
( ~ spl0_5
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f768]) ).
fof(f780,plain,
( e14 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_21 ),
inference(forward_demodulation,[],[f750,f262]) ).
fof(f789,plain,
( e10 = e14
| ~ spl0_5
| ~ spl0_21 ),
inference(forward_demodulation,[],[f780,f129]) ).
fof(f796,plain,
( $false
| ~ spl0_5
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f789,f171]) ).
fof(f797,plain,
( ~ spl0_5
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f796]) ).
fof(f813,plain,
( e12 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_23 ),
inference(forward_demodulation,[],[f750,f270]) ).
fof(f827,plain,
( e10 = e12
| ~ spl0_5
| ~ spl0_23 ),
inference(forward_demodulation,[],[f813,f129]) ).
fof(f832,plain,
( $false
| ~ spl0_5
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f827,f173]) ).
fof(f833,plain,
( ~ spl0_5
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f832]) ).
fof(f850,plain,
( e13 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_22 ),
inference(forward_demodulation,[],[f750,f266]) ).
fof(f854,plain,
( e14 = op1(e12,e12)
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f660,f241]) ).
fof(f858,plain,
( e10 = e13
| ~ spl0_5
| ~ spl0_22 ),
inference(forward_demodulation,[],[f850,f129]) ).
fof(f859,plain,
( e13 = e14
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f854,f117]) ).
fof(f863,plain,
( $false
| ~ spl0_5
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f858,f172]) ).
fof(f864,plain,
( ~ spl0_5
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f863]) ).
fof(f865,plain,
( $false
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f859,f165]) ).
fof(f866,plain,
( ~ spl0_8
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f865]) ).
fof(f869,plain,
( spl0_50
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f629,f276,f381]) ).
fof(f895,plain,
( op1(e12,e14) = j(e22)
| ~ spl0_1
| ~ spl0_8 ),
inference(forward_demodulation,[],[f654,f178]) ).
fof(f899,plain,
( e12 = op1(e12,e14)
| ~ spl0_1
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_demodulation,[],[f895,f228]) ).
fof(f904,plain,
( e11 = e12
| ~ spl0_1
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_demodulation,[],[f899,f115]) ).
fof(f909,plain,
( $false
| ~ spl0_1
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f904,f170]) ).
fof(f910,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f909]) ).
fof(f945,plain,
( op1(e14,e12) = j(e22)
| ~ spl0_1
| ~ spl0_8 ),
inference(forward_demodulation,[],[f633,f178]) ).
fof(f948,plain,
( e11 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_demodulation,[],[f945,f232]) ).
fof(f951,plain,
( e10 = e11
| ~ spl0_1
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_demodulation,[],[f948,f107]) ).
fof(f954,plain,
( $false
| ~ spl0_1
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f951,f174]) ).
fof(f955,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f954]) ).
fof(f972,plain,
( op1(e11,e11) = j(e20)
| ~ spl0_4 ),
inference(superposition,[],[f385,f190]) ).
fof(f974,plain,
( j(e21) = op1(e11,j(e22))
| ~ spl0_4 ),
inference(superposition,[],[f387,f190]) ).
fof(f975,plain,
( j(e23) = op1(e11,j(e21))
| ~ spl0_4 ),
inference(superposition,[],[f388,f190]) ).
fof(f981,plain,
( op1(e11,e11) = j(e21)
| ~ spl0_4
| ~ spl0_14 ),
inference(forward_demodulation,[],[f974,f232]) ).
fof(f983,plain,
( e12 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_23 ),
inference(forward_demodulation,[],[f972,f270]) ).
fof(f986,plain,
( e12 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_14
| ~ spl0_18 ),
inference(forward_demodulation,[],[f981,f249]) ).
fof(f988,plain,
( e10 = e12
| ~ spl0_4
| ~ spl0_23 ),
inference(forward_demodulation,[],[f983,f123]) ).
fof(f990,plain,
( e10 = e12
| ~ spl0_4
| ~ spl0_14
| ~ spl0_18 ),
inference(forward_demodulation,[],[f986,f123]) ).
fof(f991,plain,
( $false
| ~ spl0_4
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f988,f173]) ).
fof(f992,plain,
( ~ spl0_4
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f991]) ).
fof(f995,plain,
( $false
| ~ spl0_4
| ~ spl0_14
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f990,f173]) ).
fof(f996,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f995]) ).
fof(f1000,plain,
( e11 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_24 ),
inference(forward_demodulation,[],[f972,f274]) ).
fof(f1005,plain,
( op1(e11,e11) = j(e23)
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_demodulation,[],[f975,f253]) ).
fof(f1008,plain,
( e10 = e11
| ~ spl0_4
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1000,f123]) ).
fof(f1010,plain,
( e12 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1005,f207]) ).
fof(f1014,plain,
( $false
| ~ spl0_4
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f1008,f174]) ).
fof(f1015,plain,
( ~ spl0_4
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f1014]) ).
fof(f1016,plain,
( e10 = e12
| ~ spl0_4
| ~ spl0_8
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1010,f123]) ).
fof(f1019,plain,
( $false
| ~ spl0_4
| ~ spl0_8
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1016,f173]) ).
fof(f1020,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1019]) ).
fof(f1033,plain,
( op1(e12,e13) = j(e22)
| ~ spl0_2
| ~ spl0_8 ),
inference(forward_demodulation,[],[f654,f182]) ).
fof(f1040,plain,
( e11 = op1(e12,e13)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1033,f232]) ).
fof(f1042,plain,
( e10 = e11
| ~ spl0_2
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1040,f116]) ).
fof(f1045,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1042,f174]) ).
fof(f1046,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1045]) ).
fof(f1059,plain,
( e24 = h(e12)
| ~ spl0_3 ),
inference(superposition,[],[f25,f186]) ).
fof(f1081,plain,
( e23 = e24
| ~ spl0_3
| ~ spl0_37 ),
inference(forward_demodulation,[],[f1059,f329]) ).
fof(f1084,plain,
( $false
| ~ spl0_3
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f1081,f155]) ).
fof(f1085,plain,
( ~ spl0_3
| ~ spl0_37 ),
inference(avatar_contradiction_clause,[],[f1084]) ).
fof(f1106,plain,
( op1(e11,e11) = j(e20)
| ~ spl0_4 ),
inference(superposition,[],[f385,f190]) ).
fof(f1109,plain,
( j(e23) = op1(e11,j(e21))
| ~ spl0_4 ),
inference(superposition,[],[f388,f190]) ).
fof(f1114,plain,
( op1(e11,e10) = j(e23)
| ~ spl0_4
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1109,f257]) ).
fof(f1117,plain,
( e14 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1106,f262]) ).
fof(f1119,plain,
( e12 = op1(e11,e10)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1114,f207]) ).
fof(f1122,plain,
( e10 = e14
| ~ spl0_4
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1117,f123]) ).
fof(f1123,plain,
( e11 = e12
| ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1119,f124]) ).
fof(f1124,plain,
( $false
| ~ spl0_4
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1122,f171]) ).
fof(f1125,plain,
( ~ spl0_4
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1124]) ).
fof(f1126,plain,
( $false
| ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1123,f170]) ).
fof(f1127,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f1126]) ).
fof(f1152,plain,
( e20 = e24
| ~ spl0_5
| ~ spl0_50 ),
inference(forward_demodulation,[],[f748,f383]) ).
fof(f1155,plain,
( $false
| ~ spl0_5
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f1152,f161]) ).
fof(f1156,plain,
( ~ spl0_5
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f1155]) ).
fof(f1165,plain,
( op1(e14,e14) = j(e20)
| ~ spl0_1 ),
inference(superposition,[],[f385,f178]) ).
fof(f1166,plain,
( j(e22) = op1(e14,j(e23))
| ~ spl0_1 ),
inference(superposition,[],[f386,f178]) ).
fof(f1168,plain,
( j(e23) = op1(e14,j(e21))
| ~ spl0_1 ),
inference(superposition,[],[f388,f178]) ).
fof(f1170,plain,
( j(e22) = op1(j(e23),e14)
| ~ spl0_1 ),
inference(superposition,[],[f390,f178]) ).
fof(f1175,plain,
( op1(e14,e14) = j(e22)
| ~ spl0_1
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1166,f199]) ).
fof(f1176,plain,
( e10 = op1(e14,e14)
| ~ spl0_1
| ~ spl0_25 ),
inference(forward_demodulation,[],[f1165,f278]) ).
fof(f1182,plain,
( e11 = op1(e14,e14)
| ~ spl0_1
| ~ spl0_6
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1175,f232]) ).
fof(f1185,plain,
( e10 = e11
| ~ spl0_1
| ~ spl0_6
| ~ spl0_14
| ~ spl0_25 ),
inference(forward_demodulation,[],[f1182,f1176]) ).
fof(f1190,plain,
( $false
| ~ spl0_1
| ~ spl0_6
| ~ spl0_14
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f1185,f174]) ).
fof(f1191,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_14
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f1190]) ).
fof(f1206,plain,
( e23 = h(e10)
| ~ spl0_10 ),
inference(superposition,[],[f26,f215]) ).
fof(f1210,plain,
( op1(e10,e10) = j(e21)
| ~ spl0_10 ),
inference(superposition,[],[f391,f215]) ).
fof(f1215,plain,
( e13 = op1(e10,e10)
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1210,f245]) ).
fof(f1218,plain,
( e20 = e23
| ~ spl0_10
| ~ spl0_50 ),
inference(forward_demodulation,[],[f1206,f383]) ).
fof(f1221,plain,
( e10 = e13
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1215,f129]) ).
fof(f1224,plain,
( $false
| ~ spl0_10
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f1218,f162]) ).
fof(f1225,plain,
( ~ spl0_10
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f1224]) ).
fof(f1227,plain,
( $false
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1221,f172]) ).
fof(f1228,plain,
( ~ spl0_10
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1227]) ).
fof(f1242,plain,
( op1(e11,e11) = j(e21)
| ~ spl0_9 ),
inference(superposition,[],[f391,f211]) ).
fof(f1244,plain,
( j(e24) = op1(e11,j(e21))
| ~ spl0_9 ),
inference(superposition,[],[f393,f211]) ).
fof(f1245,plain,
( op1(e11,e13) = j(e24)
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1244,f245]) ).
fof(f1247,plain,
( e13 = op1(e11,e11)
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1242,f245]) ).
fof(f1252,plain,
( e14 = op1(e11,e13)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1245,f178]) ).
fof(f1254,plain,
( e10 = e13
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1247,f123]) ).
fof(f1257,plain,
( e12 = e14
| ~ spl0_1
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1252,f121]) ).
fof(f1258,plain,
( $false
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1254,f172]) ).
fof(f1259,plain,
( ~ spl0_9
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1258]) ).
fof(f1260,plain,
( $false
| ~ spl0_1
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1257,f166]) ).
fof(f1261,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1260]) ).
fof(f1265,plain,
( op1(e13,e14) = j(e22)
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1170,f203]) ).
fof(f1268,plain,
( e11 = op1(e13,e14)
| ~ spl0_1
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1265,f232]) ).
fof(f1271,plain,
( e10 = e11
| ~ spl0_1
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1268,f110]) ).
fof(f1274,plain,
( $false
| ~ spl0_1
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1271,f174]) ).
fof(f1275,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1274]) ).
fof(f1303,plain,
( op1(e11,e11) = j(e21)
| ~ spl0_9 ),
inference(superposition,[],[f391,f211]) ).
fof(f1305,plain,
( j(e24) = op1(e11,j(e21))
| ~ spl0_9 ),
inference(superposition,[],[f393,f211]) ).
fof(f1306,plain,
( op1(e11,e11) = j(e24)
| ~ spl0_9
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1305,f253]) ).
fof(f1308,plain,
( e11 = op1(e11,e11)
| ~ spl0_9
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1303,f253]) ).
fof(f1311,plain,
( e14 = op1(e11,e11)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1306,f178]) ).
fof(f1313,plain,
( e10 = e11
| ~ spl0_9
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1308,f123]) ).
fof(f1316,plain,
( e10 = e14
| ~ spl0_1
| ~ spl0_9
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1311,f123]) ).
fof(f1317,plain,
( $false
| ~ spl0_9
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1313,f174]) ).
fof(f1318,plain,
( ~ spl0_9
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1317]) ).
fof(f1319,plain,
( $false
| ~ spl0_1
| ~ spl0_9
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1316,f171]) ).
fof(f1320,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1319]) ).
fof(f1325,plain,
( op1(e11,e14) = j(e24)
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1305,f241]) ).
fof(f1326,plain,
( e14 = op1(e11,e11)
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1303,f241]) ).
fof(f1329,plain,
( e14 = op1(e11,e14)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1325,f178]) ).
fof(f1330,plain,
( e10 = e14
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1326,f123]) ).
fof(f1334,plain,
( e13 = e14
| ~ spl0_1
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1329,f120]) ).
fof(f1335,plain,
( $false
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1330,f171]) ).
fof(f1336,plain,
( ~ spl0_9
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1335]) ).
fof(f1339,plain,
( $false
| ~ spl0_1
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1334,f165]) ).
fof(f1340,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1339]) ).
fof(f1343,plain,
( op1(e14,e12) = j(e23)
| ~ spl0_1
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1168,f249]) ).
fof(f1346,plain,
( e12 = op1(e11,e11)
| ~ spl0_9
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1303,f249]) ).
fof(f1347,plain,
( e11 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1343,f211]) ).
fof(f1350,plain,
( e10 = e12
| ~ spl0_9
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1346,f123]) ).
fof(f1351,plain,
( e10 = e11
| ~ spl0_1
| ~ spl0_9
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1347,f107]) ).
fof(f1354,plain,
( $false
| ~ spl0_9
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1350,f173]) ).
fof(f1355,plain,
( ~ spl0_9
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1354]) ).
fof(f1356,plain,
( $false
| ~ spl0_1
| ~ spl0_9
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1351,f174]) ).
fof(f1357,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1356]) ).
fof(f1369,plain,
( j(e22) = op1(e13,j(e23))
| ~ spl0_2 ),
inference(superposition,[],[f386,f182]) ).
fof(f1370,plain,
( j(e21) = op1(e13,j(e22))
| ~ spl0_2 ),
inference(superposition,[],[f387,f182]) ).
fof(f1371,plain,
( j(e23) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(superposition,[],[f388,f182]) ).
fof(f1376,plain,
( op1(e13,e14) = j(e23)
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1371,f241]) ).
fof(f1377,plain,
( op1(e13,e11) = j(e21)
| ~ spl0_2
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1370,f232]) ).
fof(f1378,plain,
( op1(e13,e14) = j(e22)
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1369,f199]) ).
fof(f1383,plain,
( e14 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1376,f199]) ).
fof(f1384,plain,
( e14 = op1(e13,e11)
| ~ spl0_2
| ~ spl0_14
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1377,f241]) ).
fof(f1385,plain,
( e11 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1378,f232]) ).
fof(f1386,plain,
( e10 = e14
| ~ spl0_2
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1383,f110]) ).
fof(f1387,plain,
( e12 = e14
| ~ spl0_2
| ~ spl0_14
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1384,f113]) ).
fof(f1388,plain,
( e10 = e11
| ~ spl0_2
| ~ spl0_6
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1385,f110]) ).
fof(f1389,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1386,f171]) ).
fof(f1390,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1389]) ).
fof(f1391,plain,
( $false
| ~ spl0_2
| ~ spl0_14
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1387,f166]) ).
fof(f1392,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1391]) ).
fof(f1393,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1388,f174]) ).
fof(f1394,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1393]) ).
fof(f1395,plain,
( e20 = e24
| ~ spl0_3
| ~ spl0_40 ),
inference(forward_demodulation,[],[f1059,f341]) ).
fof(f1398,plain,
( $false
| ~ spl0_3
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f1395,f161]) ).
fof(f1399,plain,
( ~ spl0_3
| ~ spl0_40 ),
inference(avatar_contradiction_clause,[],[f1398]) ).
fof(f1408,plain,
( j(e22) = op1(e12,j(e23))
| ~ spl0_3 ),
inference(superposition,[],[f386,f186]) ).
fof(f1410,plain,
( j(e23) = op1(e12,j(e21))
| ~ spl0_3 ),
inference(superposition,[],[f388,f186]) ).
fof(f1412,plain,
( j(e22) = op1(j(e23),e12)
| ~ spl0_3 ),
inference(superposition,[],[f390,f186]) ).
fof(f1413,plain,
( op1(e14,e12) = j(e22)
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1412,f199]) ).
fof(f1415,plain,
( op1(e12,e14) = j(e23)
| ~ spl0_3
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1410,f241]) ).
fof(f1419,plain,
( e11 = op1(e14,e12)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1413,f232]) ).
fof(f1420,plain,
( e14 = op1(e12,e14)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1415,f199]) ).
fof(f1423,plain,
( e10 = e11
| ~ spl0_3
| ~ spl0_6
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1419,f107]) ).
fof(f1424,plain,
( e11 = e14
| ~ spl0_3
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1420,f115]) ).
fof(f1425,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1423,f174]) ).
fof(f1426,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1425]) ).
fof(f1427,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1424,f168]) ).
fof(f1428,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1427]) ).
fof(f1433,plain,
( op1(e12,e13) = j(e22)
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1408,f203]) ).
fof(f1434,plain,
( e13 = op1(e12,e14)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1415,f203]) ).
fof(f1436,plain,
( e11 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1433,f232]) ).
fof(f1437,plain,
( e11 = e13
| ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1434,f115]) ).
fof(f1438,plain,
( e10 = e11
| ~ spl0_3
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1436,f116]) ).
fof(f1439,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1437,f169]) ).
fof(f1440,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1439]) ).
fof(f1441,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1438,f174]) ).
fof(f1442,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1441]) ).
fof(f1452,plain,
( op1(e13,e13) = j(e20)
| ~ spl0_2 ),
inference(superposition,[],[f385,f182]) ).
fof(f1453,plain,
( j(e22) = op1(e13,j(e23))
| ~ spl0_2 ),
inference(superposition,[],[f386,f182]) ).
fof(f1454,plain,
( j(e21) = op1(e13,j(e22))
| ~ spl0_2 ),
inference(superposition,[],[f387,f182]) ).
fof(f1455,plain,
( j(e23) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(superposition,[],[f388,f182]) ).
fof(f1456,plain,
( e13 = op1(e13,j(e20))
| ~ spl0_2 ),
inference(superposition,[],[f389,f182]) ).
fof(f1461,plain,
( op1(e13,e11) = j(e21)
| ~ spl0_2
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1454,f232]) ).
fof(f1462,plain,
( op1(e13,e13) = j(e22)
| ~ spl0_2
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1453,f203]) ).
fof(f1463,plain,
( e10 = op1(e13,e13)
| ~ spl0_2
| ~ spl0_25 ),
inference(forward_demodulation,[],[f1452,f278]) ).
fof(f1466,plain,
( e13 = op1(e13,e11)
| ~ spl0_2
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1461,f245]) ).
fof(f1467,plain,
( e11 = op1(e13,e13)
| ~ spl0_2
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1462,f232]) ).
fof(f1470,plain,
( e12 = e13
| ~ spl0_2
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1466,f113]) ).
fof(f1471,plain,
( e10 = e11
| ~ spl0_2
| ~ spl0_7
| ~ spl0_14
| ~ spl0_25 ),
inference(forward_demodulation,[],[f1467,f1463]) ).
fof(f1476,plain,
( $false
| ~ spl0_2
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1470,f167]) ).
fof(f1477,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1476]) ).
fof(f1478,plain,
( $false
| ~ spl0_2
| ~ spl0_7
| ~ spl0_14
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f1471,f174]) ).
fof(f1479,plain,
( ~ spl0_2
| ~ spl0_7
| ~ spl0_14
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f1478]) ).
fof(f1487,plain,
( e13 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1456,f262]) ).
fof(f1491,plain,
( op1(e13,e12) = j(e23)
| ~ spl0_2
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1455,f249]) ).
fof(f1493,plain,
( e10 = e13
| ~ spl0_2
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1487,f110]) ).
fof(f1494,plain,
( e13 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1491,f203]) ).
fof(f1495,plain,
( $false
| ~ spl0_2
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1493,f172]) ).
fof(f1496,plain,
( ~ spl0_2
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1495]) ).
fof(f1497,plain,
( e11 = e13
| ~ spl0_2
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1494,f112]) ).
fof(f1498,plain,
( $false
| ~ spl0_2
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1497,f169]) ).
fof(f1499,plain,
( ~ spl0_2
| ~ spl0_7
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1498]) ).
fof(f1502,plain,
( e13 = op1(e13,e11)
| ~ spl0_2
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1456,f274]) ).
fof(f1505,plain,
( op1(e13,e11) = j(e23)
| ~ spl0_2
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1455,f253]) ).
fof(f1507,plain,
( e12 = e13
| ~ spl0_2
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1502,f113]) ).
fof(f1508,plain,
( e13 = op1(e13,e11)
| ~ spl0_2
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1505,f203]) ).
fof(f1509,plain,
( $false
| ~ spl0_2
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f1507,f167]) ).
fof(f1510,plain,
( ~ spl0_2
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f1509]) ).
fof(f1511,plain,
( e12 = e13
| ~ spl0_2
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1508,f113]) ).
fof(f1512,plain,
( $false
| ~ spl0_2
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1511,f167]) ).
fof(f1513,plain,
( ~ spl0_2
| ~ spl0_7
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1512]) ).
fof(f1530,plain,
( op1(e14,e14) = j(e20)
| ~ spl0_1 ),
inference(superposition,[],[f385,f178]) ).
fof(f1533,plain,
( j(e23) = op1(e14,j(e21))
| ~ spl0_1 ),
inference(superposition,[],[f388,f178]) ).
fof(f1541,plain,
( e14 = op1(e14,e14)
| ~ spl0_1
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1530,f262]) ).
fof(f1547,plain,
( e12 = e14
| ~ spl0_1
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1541,f105]) ).
fof(f1551,plain,
( $false
| ~ spl0_1
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1547,f166]) ).
fof(f1552,plain,
( ~ spl0_1
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1551]) ).
fof(f1558,plain,
( e13 = op1(e14,e14)
| ~ spl0_1
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1530,f266]) ).
fof(f1560,plain,
( op1(e14,e11) = j(e23)
| ~ spl0_1
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1533,f253]) ).
fof(f1563,plain,
( e12 = e13
| ~ spl0_1
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1558,f105]) ).
fof(f1564,plain,
( e14 = op1(e14,e11)
| ~ spl0_1
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1560,f199]) ).
fof(f1567,plain,
( $false
| ~ spl0_1
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1563,f167]) ).
fof(f1568,plain,
( ~ spl0_1
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f1567]) ).
fof(f1569,plain,
( e13 = e14
| ~ spl0_1
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1564,f108]) ).
fof(f1570,plain,
( $false
| ~ spl0_1
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1569,f165]) ).
fof(f1571,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1570]) ).
fof(f1574,plain,
( e22 = e23
| ~ spl0_10
| ~ spl0_48 ),
inference(forward_demodulation,[],[f1206,f375]) ).
fof(f1587,plain,
( $false
| ~ spl0_10
| ~ spl0_48 ),
inference(forward_subsumption_resolution,[],[f1574,f157]) ).
fof(f1588,plain,
( ~ spl0_10
| ~ spl0_48 ),
inference(avatar_contradiction_clause,[],[f1587]) ).
fof(f1601,plain,
( e13 = op1(e13,j(e20))
| ~ spl0_2 ),
inference(superposition,[],[f389,f182]) ).
fof(f1604,plain,
( e13 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1601,f270]) ).
fof(f1610,plain,
( e11 = e13
| ~ spl0_2
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1604,f112]) ).
fof(f1614,plain,
( $false
| ~ spl0_2
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1610,f169]) ).
fof(f1615,plain,
( ~ spl0_2
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f1614]) ).
fof(f1633,plain,
( op1(e10,e10) = j(e21)
| ~ spl0_10 ),
inference(superposition,[],[f391,f215]) ).
fof(f1634,plain,
( j(e20) = op1(e10,j(e22))
| ~ spl0_10 ),
inference(superposition,[],[f392,f215]) ).
fof(f1637,plain,
( op1(e10,e11) = j(e20)
| ~ spl0_10
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1634,f232]) ).
fof(f1638,plain,
( e12 = op1(e10,e10)
| ~ spl0_10
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1633,f249]) ).
fof(f1642,plain,
( e13 = op1(e10,e11)
| ~ spl0_10
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1637,f266]) ).
fof(f1643,plain,
( e10 = e12
| ~ spl0_10
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1638,f129]) ).
fof(f1647,plain,
( e11 = e13
| ~ spl0_10
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1642,f128]) ).
fof(f1648,plain,
( $false
| ~ spl0_10
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1643,f173]) ).
fof(f1649,plain,
( ~ spl0_10
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1648]) ).
fof(f1652,plain,
( $false
| ~ spl0_10
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1647,f169]) ).
fof(f1653,plain,
( ~ spl0_10
| ~ spl0_14
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f1652]) ).
fof(f1663,plain,
( e11 = op1(e10,e10)
| ~ spl0_10
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1633,f253]) ).
fof(f1673,plain,
( e10 = e11
| ~ spl0_10
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1663,f129]) ).
fof(f1677,plain,
( $false
| ~ spl0_10
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1673,f174]) ).
fof(f1678,plain,
( ~ spl0_10
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1677]) ).
fof(f1686,plain,
( e14 = op1(e10,e10)
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1633,f241]) ).
fof(f1694,plain,
( e10 = e14
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1686,f129]) ).
fof(f1697,plain,
( $false
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1694,f171]) ).
fof(f1698,plain,
( ~ spl0_10
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1697]) ).
fof(f1718,plain,
( op1(e11,e11) = j(e20)
| ~ spl0_4 ),
inference(superposition,[],[f385,f190]) ).
fof(f1719,plain,
( j(e22) = op1(e11,j(e23))
| ~ spl0_4 ),
inference(superposition,[],[f386,f190]) ).
fof(f1721,plain,
( j(e23) = op1(e11,j(e21))
| ~ spl0_4 ),
inference(superposition,[],[f388,f190]) ).
fof(f1726,plain,
( op1(e11,e13) = j(e23)
| ~ spl0_4
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1721,f245]) ).
fof(f1729,plain,
( e13 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1718,f266]) ).
fof(f1731,plain,
( e14 = op1(e11,e13)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1726,f199]) ).
fof(f1734,plain,
( e10 = e13
| ~ spl0_4
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1729,f123]) ).
fof(f1735,plain,
( e12 = e14
| ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1731,f121]) ).
fof(f1737,plain,
( $false
| ~ spl0_4
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1734,f172]) ).
fof(f1738,plain,
( ~ spl0_4
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f1737]) ).
fof(f1739,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1735,f166]) ).
fof(f1740,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1739]) ).
fof(f1750,plain,
( op1(e11,e14) = j(e23)
| ~ spl0_4
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1721,f241]) ).
fof(f1752,plain,
( e14 = op1(e11,e14)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1750,f199]) ).
fof(f1754,plain,
( e13 = e14
| ~ spl0_4
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1752,f120]) ).
fof(f1757,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1754,f165]) ).
fof(f1758,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1757]) ).
fof(f1761,plain,
( op1(e11,e10) = j(e23)
| ~ spl0_4
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1721,f257]) ).
fof(f1763,plain,
( e14 = op1(e11,e10)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1761,f199]) ).
fof(f1764,plain,
( e11 = e14
| ~ spl0_4
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1763,f124]) ).
fof(f1765,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1764,f168]) ).
fof(f1766,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f1765]) ).
fof(f1773,plain,
( op1(e11,e11) = j(e22)
| ~ spl0_4
| ~ spl0_9 ),
inference(forward_demodulation,[],[f1719,f211]) ).
fof(f1776,plain,
( e11 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_9
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1773,f232]) ).
fof(f1778,plain,
( e10 = e11
| ~ spl0_4
| ~ spl0_9
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1776,f123]) ).
fof(f1781,plain,
( $false
| ~ spl0_4
| ~ spl0_9
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1778,f174]) ).
fof(f1782,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1781]) ).
fof(f1790,plain,
( e13 = op1(e11,e10)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1761,f203]) ).
fof(f1793,plain,
( e11 = e13
| ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1790,f124]) ).
fof(f1794,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1793,f169]) ).
fof(f1795,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f1794]) ).
fof(f1823,plain,
( e14 = op1(e14,j(e20))
| ~ spl0_1 ),
inference(superposition,[],[f389,f178]) ).
fof(f1826,plain,
( e14 = op1(e14,e11)
| ~ spl0_1
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1823,f274]) ).
fof(f1832,plain,
( e13 = e14
| ~ spl0_1
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1826,f108]) ).
fof(f1836,plain,
( $false
| ~ spl0_1
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f1832,f165]) ).
fof(f1837,plain,
( ~ spl0_1
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f1836]) ).
fof(f1842,plain,
( e14 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1823,f270]) ).
fof(f1844,plain,
( e10 = e14
| ~ spl0_1
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1842,f107]) ).
fof(f1845,plain,
( $false
| ~ spl0_1
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1844,f171]) ).
fof(f1846,plain,
( ~ spl0_1
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f1845]) ).
fof(f1891,plain,
( e24 = h(e12)
| ~ spl0_3 ),
inference(superposition,[],[f25,f186]) ).
fof(f1948,plain,
( j(e20) = op1(e13,j(e22))
| ~ spl0_7 ),
inference(superposition,[],[f392,f203]) ).
fof(f1951,plain,
( op1(e13,e11) = j(e20)
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1948,f232]) ).
fof(f1958,plain,
( e13 = op1(e13,e11)
| ~ spl0_7
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1951,f266]) ).
fof(f1961,plain,
( e12 = e13
| ~ spl0_7
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1958,f113]) ).
fof(f1962,plain,
( $false
| ~ spl0_7
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1961,f167]) ).
fof(f1963,plain,
( ~ spl0_7
| ~ spl0_14
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f1962]) ).
fof(f1966,plain,
( e22 = e24
| ~ spl0_3
| ~ spl0_38 ),
inference(forward_demodulation,[],[f1891,f333]) ).
fof(f1985,plain,
( $false
| ~ spl0_3
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f1966,f156]) ).
fof(f1986,plain,
( ~ spl0_3
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f1985]) ).
fof(f2001,plain,
( op1(e12,e12) = j(e20)
| ~ spl0_3 ),
inference(superposition,[],[f385,f186]) ).
fof(f2002,plain,
( j(e22) = op1(e12,j(e23))
| ~ spl0_3 ),
inference(superposition,[],[f386,f186]) ).
fof(f2004,plain,
( j(e23) = op1(e12,j(e21))
| ~ spl0_3 ),
inference(superposition,[],[f388,f186]) ).
fof(f2009,plain,
( op1(e12,e10) = j(e23)
| ~ spl0_3
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2004,f257]) ).
fof(f2011,plain,
( op1(e12,e10) = j(e22)
| ~ spl0_3
| ~ spl0_10 ),
inference(forward_demodulation,[],[f2002,f215]) ).
fof(f2012,plain,
( e14 = op1(e12,e12)
| ~ spl0_3
| ~ spl0_21 ),
inference(forward_demodulation,[],[f2001,f262]) ).
fof(f2015,plain,
( e10 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_10
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2009,f215]) ).
fof(f2017,plain,
( e11 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_10
| ~ spl0_14 ),
inference(forward_demodulation,[],[f2011,f232]) ).
fof(f2018,plain,
( e13 = e14
| ~ spl0_3
| ~ spl0_21 ),
inference(forward_demodulation,[],[f2012,f117]) ).
fof(f2021,plain,
( e10 = e11
| ~ spl0_3
| ~ spl0_10
| ~ spl0_14
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2017,f2015]) ).
fof(f2022,plain,
( $false
| ~ spl0_3
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f2018,f165]) ).
fof(f2023,plain,
( ~ spl0_3
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f2022]) ).
fof(f2024,plain,
( $false
| ~ spl0_3
| ~ spl0_10
| ~ spl0_14
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2021,f174]) ).
fof(f2025,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_14
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2024]) ).
fof(f2041,plain,
( j(e22) = op1(e11,j(e23))
| ~ spl0_4 ),
inference(superposition,[],[f386,f190]) ).
fof(f2043,plain,
( j(e23) = op1(e11,j(e21))
| ~ spl0_4 ),
inference(superposition,[],[f388,f190]) ).
fof(f2059,plain,
( j(e22) = op1(j(e24),e11)
| ~ spl0_9 ),
inference(superposition,[],[f386,f211]) ).
fof(f2068,plain,
( op1(e11,e11) = j(e22)
| ~ spl0_4
| ~ spl0_9 ),
inference(forward_demodulation,[],[f2059,f190]) ).
fof(f2076,plain,
( e22 = h(e10)
| ~ spl0_15 ),
inference(superposition,[],[f27,f236]) ).
fof(f2077,plain,
( $false
| ~ spl0_15
| spl0_48 ),
inference(forward_subsumption_resolution,[],[f2076,f374]) ).
fof(f2078,plain,
( ~ spl0_15
| spl0_48 ),
inference(avatar_contradiction_clause,[],[f2077]) ).
fof(f2084,plain,
( e20 = e22
| ~ spl0_15
| ~ spl0_50 ),
inference(forward_demodulation,[],[f2076,f383]) ).
fof(f2087,plain,
( $false
| ~ spl0_15
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f2084,f163]) ).
fof(f2088,plain,
( ~ spl0_15
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f2087]) ).
fof(f2098,plain,
( e13 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_9
| ~ spl0_12 ),
inference(forward_demodulation,[],[f2068,f224]) ).
fof(f2104,plain,
( e10 = e13
| ~ spl0_4
| ~ spl0_9
| ~ spl0_12 ),
inference(forward_demodulation,[],[f2098,f123]) ).
fof(f2111,plain,
( $false
| ~ spl0_4
| ~ spl0_9
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f2104,f172]) ).
fof(f2112,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f2111]) ).
fof(f2120,plain,
( e12 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_9
| ~ spl0_13 ),
inference(forward_demodulation,[],[f2068,f228]) ).
fof(f2126,plain,
( e10 = e12
| ~ spl0_4
| ~ spl0_9
| ~ spl0_13 ),
inference(forward_demodulation,[],[f2120,f123]) ).
fof(f2133,plain,
( $false
| ~ spl0_4
| ~ spl0_9
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f2126,f173]) ).
fof(f2134,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f2133]) ).
fof(f2145,plain,
( e14 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2068,f220]) ).
fof(f2151,plain,
( e10 = e14
| ~ spl0_4
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2145,f123]) ).
fof(f2158,plain,
( $false
| ~ spl0_4
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f2151,f171]) ).
fof(f2159,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f2158]) ).
fof(f2164,plain,
( op1(e11,e11) = j(e23)
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2043,f253]) ).
fof(f2173,plain,
( e14 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2164,f199]) ).
fof(f2177,plain,
( e10 = e14
| ~ spl0_4
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2173,f123]) ).
fof(f2178,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2177,f171]) ).
fof(f2179,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2178]) ).
fof(f2192,plain,
( j(e24) = op1(e14,j(e21))
| ~ spl0_6 ),
inference(superposition,[],[f393,f199]) ).
fof(f2193,plain,
( op1(e14,e12) = j(e24)
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2192,f249]) ).
fof(f2200,plain,
( e11 = op1(e14,e12)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2193,f190]) ).
fof(f2204,plain,
( e10 = e11
| ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2200,f107]) ).
fof(f2205,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f2204,f174]) ).
fof(f2206,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2205]) ).
fof(f2213,plain,
( op1(e11,e13) = j(e22)
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f2041,f203]) ).
fof(f2220,plain,
( e13 = op1(e11,e13)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_12 ),
inference(forward_demodulation,[],[f2213,f224]) ).
fof(f2222,plain,
( e12 = e13
| ~ spl0_4
| ~ spl0_7
| ~ spl0_12 ),
inference(forward_demodulation,[],[f2220,f121]) ).
fof(f2225,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f2222,f167]) ).
fof(f2226,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f2225]) ).
fof(f2236,plain,
( j(e22) = op1(j(e24),e13)
| ~ spl0_7 ),
inference(superposition,[],[f386,f203]) ).
fof(f2240,plain,
( j(e24) = op1(e13,j(e21))
| ~ spl0_7 ),
inference(superposition,[],[f393,f203]) ).
fof(f2245,plain,
( op1(e11,e13) = j(e22)
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f2236,f190]) ).
fof(f2254,plain,
( e22 = h(e12)
| ~ spl0_13 ),
inference(superposition,[],[f27,f228]) ).
fof(f2262,plain,
( e21 = e22
| ~ spl0_13
| ~ spl0_39 ),
inference(forward_demodulation,[],[f2254,f337]) ).
fof(f2265,plain,
( $false
| ~ spl0_13
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f2262,f160]) ).
fof(f2266,plain,
( ~ spl0_13
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f2265]) ).
fof(f2270,plain,
( e21 = h(e12)
| ~ spl0_18 ),
inference(superposition,[],[f28,f249]) ).
fof(f2287,plain,
( e14 = op1(e11,e13)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2245,f220]) ).
fof(f2297,plain,
( e12 = e14
| ~ spl0_4
| ~ spl0_7
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2287,f121]) ).
fof(f2304,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f2297,f166]) ).
fof(f2305,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f2304]) ).
fof(f2306,plain,
( spl0_38
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f2254,f226,f331]) ).
fof(f2311,plain,
( op1(e11,e11) = j(e23)
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2043,f253]) ).
fof(f2322,plain,
( e13 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2311,f203]) ).
fof(f2326,plain,
( e10 = e13
| ~ spl0_4
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2322,f123]) ).
fof(f2327,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2326,f172]) ).
fof(f2328,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2327]) ).
fof(f2331,plain,
( op1(e11,e13) = j(e23)
| ~ spl0_4
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2043,f245]) ).
fof(f2335,plain,
( e13 = op1(e11,e13)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2331,f203]) ).
fof(f2337,plain,
( e12 = e13
| ~ spl0_4
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2335,f121]) ).
fof(f2338,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2337,f167]) ).
fof(f2339,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2338]) ).
fof(f2345,plain,
( op1(e13,e14) = j(e24)
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2240,f241]) ).
fof(f2349,plain,
( e11 = op1(e13,e14)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2345,f190]) ).
fof(f2350,plain,
( e10 = e11
| ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2349,f110]) ).
fof(f2351,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2350,f174]) ).
fof(f2352,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2351]) ).
fof(f2353,plain,
( spl0_37
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f626,f205,f327]) ).
fof(f2355,plain,
( spl0_39
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f2270,f247,f335]) ).
fof(f2361,plain,
( op1(e11,e12) = j(e23)
| ~ spl0_4
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2043,f249]) ).
fof(f2368,plain,
( op1(e11,e12) = j(e22)
| ~ spl0_4
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2041,f207]) ).
fof(f2369,plain,
( e12 = op1(e11,e12)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2361,f207]) ).
fof(f2372,plain,
( e13 = op1(e11,e12)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_12 ),
inference(forward_demodulation,[],[f2368,f224]) ).
fof(f2373,plain,
( e12 = e13
| ~ spl0_4
| ~ spl0_8
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2372,f2369]) ).
fof(f2374,plain,
( $false
| ~ spl0_4
| ~ spl0_8
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f2373,f167]) ).
fof(f2375,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_12
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2374]) ).
fof(f2408,plain,
( j(e22) = op1(e13,j(e23))
| ~ spl0_2 ),
inference(superposition,[],[f386,f182]) ).
fof(f2410,plain,
( j(e23) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(superposition,[],[f388,f182]) ).
fof(f2415,plain,
( op1(e13,e12) = j(e23)
| ~ spl0_2
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2410,f249]) ).
fof(f2417,plain,
( op1(e13,e12) = j(e22)
| ~ spl0_2
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2408,f207]) ).
fof(f2420,plain,
( e12 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2415,f207]) ).
fof(f2422,plain,
( e13 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_12 ),
inference(forward_demodulation,[],[f2417,f224]) ).
fof(f2424,plain,
( e11 = e12
| ~ spl0_2
| ~ spl0_8
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2420,f112]) ).
fof(f2426,plain,
( e11 = e13
| ~ spl0_2
| ~ spl0_8
| ~ spl0_12 ),
inference(forward_demodulation,[],[f2422,f112]) ).
fof(f2429,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f2424,f170]) ).
fof(f2430,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2429]) ).
fof(f2433,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f2426,f169]) ).
fof(f2434,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f2433]) ).
fof(f2444,plain,
( e12 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_demodulation,[],[f2417,f228]) ).
fof(f2448,plain,
( e11 = e12
| ~ spl0_2
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_demodulation,[],[f2444,f112]) ).
fof(f2451,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f2448,f170]) ).
fof(f2452,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f2451]) ).
fof(f2466,plain,
( j(e22) = op1(e14,j(e23))
| ~ spl0_1 ),
inference(superposition,[],[f386,f178]) ).
fof(f2475,plain,
( op1(e14,e12) = j(e22)
| ~ spl0_1
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2466,f207]) ).
fof(f2480,plain,
( e13 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_8
| ~ spl0_12 ),
inference(forward_demodulation,[],[f2475,f224]) ).
fof(f2482,plain,
( e10 = e13
| ~ spl0_1
| ~ spl0_8
| ~ spl0_12 ),
inference(forward_demodulation,[],[f2480,f107]) ).
fof(f2485,plain,
( $false
| ~ spl0_1
| ~ spl0_8
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f2482,f172]) ).
fof(f2486,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f2485]) ).
fof(f2504,plain,
( j(e21) = op1(e13,j(e22))
| ~ spl0_2 ),
inference(superposition,[],[f387,f182]) ).
fof(f2505,plain,
( j(e23) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(superposition,[],[f388,f182]) ).
fof(f2510,plain,
( op1(e13,e11) = j(e23)
| ~ spl0_2
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2505,f253]) ).
fof(f2524,plain,
( j(e20) = op1(e12,j(e22))
| ~ spl0_8 ),
inference(superposition,[],[f392,f207]) ).
fof(f2527,plain,
( op1(e12,e10) = j(e20)
| ~ spl0_8
| ~ spl0_15 ),
inference(forward_demodulation,[],[f2524,f236]) ).
fof(f2532,plain,
( e13 = op1(e12,e10)
| ~ spl0_8
| ~ spl0_15
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2527,f266]) ).
fof(f2535,plain,
( e12 = e13
| ~ spl0_8
| ~ spl0_15
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2532,f119]) ).
fof(f2536,plain,
( $false
| ~ spl0_8
| ~ spl0_15
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f2535,f167]) ).
fof(f2537,plain,
( ~ spl0_8
| ~ spl0_15
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f2536]) ).
fof(f2538,plain,
( spl0_24
| ~ spl0_8
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f722,f218,f205,f272]) ).
fof(f2545,plain,
( op1(e13,e14) = j(e21)
| ~ spl0_2
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2504,f220]) ).
fof(f2551,plain,
( e11 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_11
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2545,f253]) ).
fof(f2557,plain,
( e10 = e11
| ~ spl0_2
| ~ spl0_11
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2551,f110]) ).
fof(f2567,plain,
( $false
| ~ spl0_2
| ~ spl0_11
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2557,f174]) ).
fof(f2568,plain,
( ~ spl0_2
| ~ spl0_11
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2567]) ).
fof(f2586,plain,
( e14 = op1(e13,e11)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2510,f199]) ).
fof(f2590,plain,
( e12 = e14
| ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2586,f113]) ).
fof(f2593,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2590,f166]) ).
fof(f2594,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2593]) ).
fof(f2605,plain,
( op1(e13,e10) = j(e23)
| ~ spl0_2
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2505,f257]) ).
fof(f2611,plain,
( e14 = op1(e13,e10)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2605,f199]) ).
fof(f2615,plain,
( e13 = e14
| ~ spl0_2
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2611,f114]) ).
fof(f2620,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2615,f165]) ).
fof(f2621,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2620]) ).
fof(f2638,plain,
( j(e24) = op1(e11,j(e21))
| ~ spl0_9 ),
inference(superposition,[],[f393,f211]) ).
fof(f2639,plain,
( op1(e11,e10) = j(e24)
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2638,f257]) ).
fof(f2644,plain,
( e13 = op1(e11,e10)
| ~ spl0_2
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2639,f182]) ).
fof(f2648,plain,
( e11 = e13
| ~ spl0_2
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2644,f124]) ).
fof(f2649,plain,
( $false
| ~ spl0_2
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2648,f169]) ).
fof(f2650,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2649]) ).
fof(f2675,plain,
( j(e21) = op1(e12,j(e22))
| ~ spl0_3 ),
inference(superposition,[],[f387,f186]) ).
fof(f2676,plain,
( j(e23) = op1(e12,j(e21))
| ~ spl0_3 ),
inference(superposition,[],[f388,f186]) ).
fof(f2677,plain,
( e12 = op1(e12,j(e20))
| ~ spl0_3 ),
inference(superposition,[],[f389,f186]) ).
fof(f2680,plain,
( e12 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2677,f266]) ).
fof(f2681,plain,
( op1(e12,e13) = j(e23)
| ~ spl0_3
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2676,f245]) ).
fof(f2682,plain,
( op1(e12,e10) = j(e21)
| ~ spl0_3
| ~ spl0_15 ),
inference(forward_demodulation,[],[f2675,f236]) ).
fof(f2686,plain,
( e10 = e12
| ~ spl0_3
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2680,f116]) ).
fof(f2687,plain,
( e13 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2681,f203]) ).
fof(f2688,plain,
( e13 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_15
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2682,f245]) ).
fof(f2690,plain,
( $false
| ~ spl0_3
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f2686,f173]) ).
fof(f2691,plain,
( ~ spl0_3
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f2690]) ).
fof(f2692,plain,
( e10 = e13
| ~ spl0_3
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2687,f116]) ).
fof(f2693,plain,
( e12 = e13
| ~ spl0_3
| ~ spl0_15
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2688,f119]) ).
fof(f2694,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2692,f172]) ).
fof(f2695,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2694]) ).
fof(f2696,plain,
( $false
| ~ spl0_3
| ~ spl0_15
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2693,f167]) ).
fof(f2697,plain,
( ~ spl0_3
| ~ spl0_15
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2696]) ).
fof(f2709,plain,
( j(e22) = op1(j(e24),e13)
| ~ spl0_7 ),
inference(superposition,[],[f386,f203]) ).
fof(f2713,plain,
( j(e24) = op1(e13,j(e21))
| ~ spl0_7 ),
inference(superposition,[],[f393,f203]) ).
fof(f2714,plain,
( op1(e13,e12) = j(e24)
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2713,f249]) ).
fof(f2718,plain,
( op1(e12,e13) = j(e22)
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f2709,f186]) ).
fof(f2719,plain,
( e12 = op1(e13,e12)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2714,f186]) ).
fof(f2723,plain,
( e11 = e12
| ~ spl0_3
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2719,f112]) ).
fof(f2724,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f2723,f170]) ).
fof(f2725,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2724]) ).
fof(f2754,plain,
( e21 = h(e11)
| ~ spl0_19 ),
inference(superposition,[],[f28,f253]) ).
fof(f2759,plain,
( j(e24) = op1(j(e23),e11)
| ~ spl0_19 ),
inference(superposition,[],[f393,f253]) ).
fof(f2760,plain,
( op1(e13,e11) = j(e24)
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2759,f203]) ).
fof(f2766,plain,
( e20 = h(e12)
| ~ spl0_23 ),
inference(superposition,[],[f29,f270]) ).
fof(f2767,plain,
( $false
| ~ spl0_23
| spl0_40 ),
inference(forward_subsumption_resolution,[],[f2766,f340]) ).
fof(f2768,plain,
( ~ spl0_23
| spl0_40 ),
inference(avatar_contradiction_clause,[],[f2767]) ).
fof(f2777,plain,
( op1(e12,e13) = j(e21)
| ~ spl0_3
| ~ spl0_12 ),
inference(forward_demodulation,[],[f2675,f224]) ).
fof(f2783,plain,
( e11 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_12
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2777,f253]) ).
fof(f2789,plain,
( e10 = e11
| ~ spl0_3
| ~ spl0_12
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2783,f116]) ).
fof(f2798,plain,
( $false
| ~ spl0_3
| ~ spl0_12
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2789,f174]) ).
fof(f2799,plain,
( ~ spl0_3
| ~ spl0_12
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2798]) ).
fof(f2810,plain,
( e14 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2718,f220]) ).
fof(f2820,plain,
( e10 = e14
| ~ spl0_3
| ~ spl0_7
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2810,f116]) ).
fof(f2827,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f2820,f171]) ).
fof(f2828,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f2827]) ).
fof(f2845,plain,
( e14 = op1(e13,e11)
| ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2760,f178]) ).
fof(f2851,plain,
( e12 = e14
| ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2845,f113]) ).
fof(f2856,plain,
( $false
| ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2851,f166]) ).
fof(f2857,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2856]) ).
fof(f2911,plain,
( j(e23) = op1(e12,j(e21))
| ~ spl0_3 ),
inference(superposition,[],[f388,f186]) ).
fof(f2916,plain,
( op1(e12,e10) = j(e23)
| ~ spl0_3
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2911,f257]) ).
fof(f2921,plain,
( e13 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2916,f203]) ).
fof(f2924,plain,
( e12 = e13
| ~ spl0_3
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2921,f119]) ).
fof(f2925,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2924,f167]) ).
fof(f2926,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2925]) ).
fof(f2969,plain,
( j(e24) = op1(e11,j(e21))
| ~ spl0_9 ),
inference(superposition,[],[f393,f211]) ).
fof(f2970,plain,
( op1(e11,e10) = j(e24)
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2969,f257]) ).
fof(f2975,plain,
( e14 = op1(e11,e10)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2970,f178]) ).
fof(f2979,plain,
( e11 = e14
| ~ spl0_1
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2975,f124]) ).
fof(f2980,plain,
( $false
| ~ spl0_1
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2979,f168]) ).
fof(f2981,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2980]) ).
fof(f3004,plain,
( j(e22) = op1(e12,j(e23))
| ~ spl0_3 ),
inference(superposition,[],[f386,f186]) ).
fof(f3006,plain,
( j(e23) = op1(e12,j(e21))
| ~ spl0_3 ),
inference(superposition,[],[f388,f186]) ).
fof(f3011,plain,
( op1(e12,e10) = j(e23)
| ~ spl0_3
| ~ spl0_20 ),
inference(forward_demodulation,[],[f3006,f257]) ).
fof(f3013,plain,
( op1(e12,e14) = j(e22)
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f3004,f199]) ).
fof(f3016,plain,
( e14 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f3011,f199]) ).
fof(f3018,plain,
( e13 = op1(e12,e14)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_12 ),
inference(forward_demodulation,[],[f3013,f224]) ).
fof(f3020,plain,
( e12 = e14
| ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f3016,f119]) ).
fof(f3021,plain,
( e11 = e13
| ~ spl0_3
| ~ spl0_6
| ~ spl0_12 ),
inference(forward_demodulation,[],[f3018,f115]) ).
fof(f3024,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f3020,f166]) ).
fof(f3025,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f3024]) ).
fof(f3026,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f3021,f169]) ).
fof(f3027,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f3026]) ).
fof(f3037,plain,
( op1(e12,e10) = j(e22)
| ~ spl0_3
| ~ spl0_10 ),
inference(forward_demodulation,[],[f3004,f215]) ).
fof(f3040,plain,
( e13 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_10
| ~ spl0_12 ),
inference(forward_demodulation,[],[f3037,f224]) ).
fof(f3042,plain,
( e12 = e13
| ~ spl0_3
| ~ spl0_10
| ~ spl0_12 ),
inference(forward_demodulation,[],[f3040,f119]) ).
fof(f3045,plain,
( $false
| ~ spl0_3
| ~ spl0_10
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f3042,f167]) ).
fof(f3046,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f3045]) ).
fof(f3055,plain,
( e14 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_10
| ~ spl0_11 ),
inference(forward_demodulation,[],[f3037,f220]) ).
fof(f3058,plain,
( e12 = e14
| ~ spl0_3
| ~ spl0_10
| ~ spl0_11 ),
inference(forward_demodulation,[],[f3055,f119]) ).
fof(f3061,plain,
( $false
| ~ spl0_3
| ~ spl0_10
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f3058,f166]) ).
fof(f3062,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f3061]) ).
fof(f3118,plain,
( j(e24) = op1(e11,j(e21))
| ~ spl0_9 ),
inference(superposition,[],[f393,f211]) ).
fof(f3119,plain,
( op1(e11,e10) = j(e24)
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_demodulation,[],[f3118,f257]) ).
fof(f3124,plain,
( e12 = op1(e11,e10)
| ~ spl0_3
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_demodulation,[],[f3119,f186]) ).
fof(f3128,plain,
( e11 = e12
| ~ spl0_3
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_demodulation,[],[f3124,f124]) ).
fof(f3129,plain,
( $false
| ~ spl0_3
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f3128,f170]) ).
fof(f3130,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f3129]) ).
fof(f3134,plain,
( op1(e12,e12) = j(e23)
| ~ spl0_3
| ~ spl0_18 ),
inference(forward_demodulation,[],[f3006,f249]) ).
fof(f3141,plain,
( e14 = op1(e12,e12)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f3134,f199]) ).
fof(f3144,plain,
( e13 = e14
| ~ spl0_3
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f3141,f117]) ).
fof(f3145,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f3144,f165]) ).
fof(f3146,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f3145]) ).
fof(f3154,plain,
( e20 = e21
| ~ spl0_19
| ~ spl0_45 ),
inference(forward_demodulation,[],[f2754,f362]) ).
fof(f3157,plain,
( $false
| ~ spl0_19
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f3154,f164]) ).
fof(f3158,plain,
( ~ spl0_19
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f3157]) ).
fof(f3160,plain,
( j(e22) = op1(j(e24),e14)
| ~ spl0_6 ),
inference(superposition,[],[f386,f199]) ).
fof(f3169,plain,
( op1(e12,e14) = j(e22)
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f3160,f186]) ).
fof(f3197,plain,
( e20 = h(e11)
| ~ spl0_24 ),
inference(superposition,[],[f29,f274]) ).
fof(f3198,plain,
( $false
| ~ spl0_24
| spl0_45 ),
inference(forward_subsumption_resolution,[],[f3197,f361]) ).
fof(f3199,plain,
( ~ spl0_24
| spl0_45 ),
inference(avatar_contradiction_clause,[],[f3198]) ).
fof(f3212,plain,
( e14 = op1(e12,e14)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_11 ),
inference(forward_demodulation,[],[f3169,f220]) ).
fof(f3218,plain,
( e11 = e14
| ~ spl0_3
| ~ spl0_6
| ~ spl0_11 ),
inference(forward_demodulation,[],[f3212,f115]) ).
fof(f3225,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f3218,f168]) ).
fof(f3226,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f3225]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f195]) ).
cnf(s2,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f216]) ).
cnf(s3,plain,
( spl0_11
| spl0_12
| spl0_13
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f237]) ).
cnf(s4,plain,
( spl0_16
| spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f258]) ).
cnf(s5,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f279]) ).
cnf(s9,plain,
( spl0_41
| spl0_42
| spl0_43
| spl0_44
| spl0_45 ),
inference(sat_conversion,[],[f363]) ).
cnf(s17,plain,
( spl0_4
| ~ spl0_41 ),
inference(sat_conversion,[],[f461]) ).
cnf(s18,plain,
( spl0_9
| ~ spl0_42 ),
inference(sat_conversion,[],[f464]) ).
cnf(s19,plain,
( spl0_14
| ~ spl0_43 ),
inference(sat_conversion,[],[f468]) ).
cnf(s22,plain,
( spl0_19
| ~ spl0_44 ),
inference(sat_conversion,[],[f480]) ).
cnf(s41,plain,
( spl0_24
| ~ spl0_45 ),
inference(sat_conversion,[],[f557]) ).
cnf(s54,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_17 ),
inference(sat_conversion,[],[f679]) ).
cnf(s65,plain,
( ~ spl0_5
| ~ spl0_24 ),
inference(sat_conversion,[],[f769]) ).
cnf(s68,plain,
( ~ spl0_5
| ~ spl0_21 ),
inference(sat_conversion,[],[f797]) ).
cnf(s74,plain,
( ~ spl0_5
| ~ spl0_23 ),
inference(sat_conversion,[],[f833]) ).
cnf(s78,plain,
( ~ spl0_5
| ~ spl0_22 ),
inference(sat_conversion,[],[f864]) ).
cnf(s79,plain,
( ~ spl0_8
| ~ spl0_16 ),
inference(sat_conversion,[],[f866]) ).
cnf(s81,plain,
( ~ spl0_25
| spl0_50 ),
inference(sat_conversion,[],[f869]) ).
cnf(s86,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_13 ),
inference(sat_conversion,[],[f910]) ).
cnf(s91,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_14 ),
inference(sat_conversion,[],[f955]) ).
cnf(s95,plain,
( ~ spl0_4
| ~ spl0_23 ),
inference(sat_conversion,[],[f992]) ).
cnf(s97,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_18 ),
inference(sat_conversion,[],[f996]) ).
cnf(s99,plain,
( ~ spl0_4
| ~ spl0_24 ),
inference(sat_conversion,[],[f1015]) ).
cnf(s101,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_19 ),
inference(sat_conversion,[],[f1020]) ).
cnf(s105,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_14 ),
inference(sat_conversion,[],[f1046]) ).
cnf(s108,plain,
( ~ spl0_3
| ~ spl0_37 ),
inference(sat_conversion,[],[f1085]) ).
cnf(s112,plain,
( ~ spl0_4
| ~ spl0_21 ),
inference(sat_conversion,[],[f1125]) ).
cnf(s113,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(sat_conversion,[],[f1127]) ).
cnf(s120,plain,
( ~ spl0_5
| ~ spl0_50 ),
inference(sat_conversion,[],[f1156]) ).
cnf(s124,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_14
| ~ spl0_25 ),
inference(sat_conversion,[],[f1191]) ).
cnf(s127,plain,
( ~ spl0_10
| ~ spl0_50 ),
inference(sat_conversion,[],[f1225]) ).
cnf(s128,plain,
( ~ spl0_10
| ~ spl0_17 ),
inference(sat_conversion,[],[f1228]) ).
cnf(s131,plain,
( ~ spl0_9
| ~ spl0_17 ),
inference(sat_conversion,[],[f1259]) ).
cnf(s132,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_17 ),
inference(sat_conversion,[],[f1261]) ).
cnf(s134,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_14 ),
inference(sat_conversion,[],[f1275]) ).
cnf(s139,plain,
( ~ spl0_9
| ~ spl0_19 ),
inference(sat_conversion,[],[f1318]) ).
cnf(s140,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_19 ),
inference(sat_conversion,[],[f1320]) ).
cnf(s142,plain,
( ~ spl0_9
| ~ spl0_16 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s144,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_16 ),
inference(sat_conversion,[],[f1340]) ).
cnf(s146,plain,
( ~ spl0_9
| ~ spl0_18 ),
inference(sat_conversion,[],[f1355]) ).
cnf(s147,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_18 ),
inference(sat_conversion,[],[f1357]) ).
cnf(s149,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_16 ),
inference(sat_conversion,[],[f1390]) ).
cnf(s150,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_16 ),
inference(sat_conversion,[],[f1392]) ).
cnf(s151,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_14 ),
inference(sat_conversion,[],[f1394]) ).
cnf(s152,plain,
( ~ spl0_3
| ~ spl0_40 ),
inference(sat_conversion,[],[f1399]) ).
cnf(s155,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_14 ),
inference(sat_conversion,[],[f1426]) ).
cnf(s156,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_16 ),
inference(sat_conversion,[],[f1428]) ).
cnf(s157,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(sat_conversion,[],[f1440]) ).
cnf(s158,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_14 ),
inference(sat_conversion,[],[f1442]) ).
cnf(s163,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_17 ),
inference(sat_conversion,[],[f1477]) ).
cnf(s164,plain,
( ~ spl0_2
| ~ spl0_7
| ~ spl0_14
| ~ spl0_25 ),
inference(sat_conversion,[],[f1479]) ).
cnf(s165,plain,
( ~ spl0_2
| ~ spl0_21 ),
inference(sat_conversion,[],[f1496]) ).
cnf(s166,plain,
( ~ spl0_2
| ~ spl0_7
| ~ spl0_18 ),
inference(sat_conversion,[],[f1499]) ).
cnf(s167,plain,
( ~ spl0_2
| ~ spl0_24 ),
inference(sat_conversion,[],[f1510]) ).
cnf(s168,plain,
( ~ spl0_2
| ~ spl0_7
| ~ spl0_19 ),
inference(sat_conversion,[],[f1513]) ).
cnf(s172,plain,
( ~ spl0_1
| ~ spl0_21 ),
inference(sat_conversion,[],[f1552]) ).
cnf(s175,plain,
( ~ spl0_1
| ~ spl0_22 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s176,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_19 ),
inference(sat_conversion,[],[f1571]) ).
cnf(s179,plain,
( ~ spl0_10
| ~ spl0_48 ),
inference(sat_conversion,[],[f1588]) ).
cnf(s183,plain,
( ~ spl0_2
| ~ spl0_23 ),
inference(sat_conversion,[],[f1615]) ).
cnf(s185,plain,
( ~ spl0_10
| ~ spl0_18 ),
inference(sat_conversion,[],[f1649]) ).
cnf(s187,plain,
( ~ spl0_10
| ~ spl0_14
| ~ spl0_22 ),
inference(sat_conversion,[],[f1653]) ).
cnf(s192,plain,
( ~ spl0_10
| ~ spl0_19 ),
inference(sat_conversion,[],[f1678]) ).
cnf(s197,plain,
( ~ spl0_10
| ~ spl0_16 ),
inference(sat_conversion,[],[f1698]) ).
cnf(s202,plain,
( ~ spl0_4
| ~ spl0_22 ),
inference(sat_conversion,[],[f1738]) ).
cnf(s203,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(sat_conversion,[],[f1740]) ).
cnf(s207,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_16 ),
inference(sat_conversion,[],[f1758]) ).
cnf(s208,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_20 ),
inference(sat_conversion,[],[f1766]) ).
cnf(s213,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_14 ),
inference(sat_conversion,[],[f1782]) ).
cnf(s214,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(sat_conversion,[],[f1795]) ).
cnf(s220,plain,
( ~ spl0_1
| ~ spl0_24 ),
inference(sat_conversion,[],[f1837]) ).
cnf(s221,plain,
( ~ spl0_1
| ~ spl0_23 ),
inference(sat_conversion,[],[f1846]) ).
cnf(s238,plain,
( ~ spl0_7
| ~ spl0_14
| ~ spl0_22 ),
inference(sat_conversion,[],[f1963]) ).
cnf(s243,plain,
( ~ spl0_3
| ~ spl0_38 ),
inference(sat_conversion,[],[f1986]) ).
cnf(s252,plain,
( ~ spl0_3
| ~ spl0_21 ),
inference(sat_conversion,[],[f2023]) ).
cnf(s253,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_14
| ~ spl0_20 ),
inference(sat_conversion,[],[f2025]) ).
cnf(s261,plain,
( ~ spl0_15
| spl0_48 ),
inference(sat_conversion,[],[f2078]) ).
cnf(s263,plain,
( ~ spl0_15
| ~ spl0_50 ),
inference(sat_conversion,[],[f2088]) ).
cnf(s267,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_12 ),
inference(sat_conversion,[],[f2112]) ).
cnf(s271,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_13 ),
inference(sat_conversion,[],[f2134]) ).
cnf(s276,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_11 ),
inference(sat_conversion,[],[f2159]) ).
cnf(s277,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_19 ),
inference(sat_conversion,[],[f2179]) ).
cnf(s279,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(sat_conversion,[],[f2206]) ).
cnf(s283,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_12 ),
inference(sat_conversion,[],[f2226]) ).
cnf(s287,plain,
( ~ spl0_13
| ~ spl0_39 ),
inference(sat_conversion,[],[f2266]) ).
cnf(s294,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_11 ),
inference(sat_conversion,[],[f2305]) ).
cnf(s295,plain,
( ~ spl0_13
| spl0_38 ),
inference(sat_conversion,[],[f2306]) ).
cnf(s296,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_19 ),
inference(sat_conversion,[],[f2328]) ).
cnf(s298,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_17 ),
inference(sat_conversion,[],[f2339]) ).
cnf(s299,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(sat_conversion,[],[f2352]) ).
cnf(s300,plain,
( ~ spl0_8
| spl0_37 ),
inference(sat_conversion,[],[f2353]) ).
cnf(s301,plain,
( ~ spl0_18
| spl0_39 ),
inference(sat_conversion,[],[f2355]) ).
cnf(s302,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_12
| ~ spl0_18 ),
inference(sat_conversion,[],[f2375]) ).
cnf(s312,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_18 ),
inference(sat_conversion,[],[f2430]) ).
cnf(s314,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_12 ),
inference(sat_conversion,[],[f2434]) ).
cnf(s317,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_13 ),
inference(sat_conversion,[],[f2452]) ).
cnf(s322,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_12 ),
inference(sat_conversion,[],[f2486]) ).
cnf(s330,plain,
( ~ spl0_8
| ~ spl0_15
| ~ spl0_22 ),
inference(sat_conversion,[],[f2537]) ).
cnf(s331,plain,
( ~ spl0_8
| ~ spl0_11
| spl0_24 ),
inference(sat_conversion,[],[f2538]) ).
cnf(s338,plain,
( ~ spl0_2
| ~ spl0_11
| ~ spl0_19 ),
inference(sat_conversion,[],[f2568]) ).
cnf(s341,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(sat_conversion,[],[f2594]) ).
cnf(s349,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_20 ),
inference(sat_conversion,[],[f2621]) ).
cnf(s350,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_20 ),
inference(sat_conversion,[],[f2650]) ).
cnf(s359,plain,
( ~ spl0_3
| ~ spl0_22 ),
inference(sat_conversion,[],[f2691]) ).
cnf(s360,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_17 ),
inference(sat_conversion,[],[f2695]) ).
cnf(s361,plain,
( ~ spl0_3
| ~ spl0_15
| ~ spl0_17 ),
inference(sat_conversion,[],[f2697]) ).
cnf(s363,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_18 ),
inference(sat_conversion,[],[f2725]) ).
cnf(s365,plain,
( ~ spl0_23
| spl0_40 ),
inference(sat_conversion,[],[f2768]) ).
cnf(s371,plain,
( ~ spl0_3
| ~ spl0_12
| ~ spl0_19 ),
inference(sat_conversion,[],[f2799]) ).
cnf(s377,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_11 ),
inference(sat_conversion,[],[f2828]) ).
cnf(s383,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(sat_conversion,[],[f2857]) ).
cnf(s401,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_20 ),
inference(sat_conversion,[],[f2926]) ).
cnf(s407,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_20 ),
inference(sat_conversion,[],[f2981]) ).
cnf(s416,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(sat_conversion,[],[f3025]) ).
cnf(s417,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_12 ),
inference(sat_conversion,[],[f3027]) ).
cnf(s421,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_12 ),
inference(sat_conversion,[],[f3046]) ).
cnf(s424,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_11 ),
inference(sat_conversion,[],[f3062]) ).
cnf(s442,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_20 ),
inference(sat_conversion,[],[f3130]) ).
cnf(s445,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_18 ),
inference(sat_conversion,[],[f3146]) ).
cnf(s448,plain,
( ~ spl0_19
| ~ spl0_45 ),
inference(sat_conversion,[],[f3158]) ).
cnf(s449,plain,
( ~ spl0_24
| spl0_45 ),
inference(sat_conversion,[],[f3199]) ).
cnf(s455,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_11 ),
inference(sat_conversion,[],[f3226]) ).
cnf(s456,plain,
~ spl0_5,
inference(rat,[],[s5,s81,s65,s68,s74,s78,s120]) ).
cnf(s458,plain,
( ~ spl0_9
| ~ spl0_4 ),
inference(rat,[],[s3,s213,s267,s271,s276,s263,s81,s5,s112,s95,s99,s202]) ).
cnf(s459,plain,
( ~ spl0_8
| ~ spl0_4 ),
inference(rat,[],[s3,s287,s302,s97,s301,s4,s54,s113,s79,s101,s331,s263,s81,s5,s112,s95,s99,s202]) ).
cnf(s460,plain,
( ~ spl0_7
| ~ spl0_4 ),
inference(rat,[],[s3,s287,s97,s301,s4,s214,s283,s294,s296,s298,s299,s263,s81,s5,s112,s95,s99,s202]) ).
cnf(s461,plain,
( ~ spl0_6
| ~ spl0_4 ),
inference(rat,[],[s4,s203,s207,s208,s277,s279]) ).
cnf(s462,plain,
~ spl0_4,
inference(rat,[],[s461,s2,s460,s459,s458,s127,s81,s5,s95,s99,s112,s202]) ).
cnf(s463,plain,
~ spl0_41,
inference(rat,[],[s17,s462]) ).
cnf(s464,plain,
( ~ spl0_20
| spl0_6
| ~ spl0_3 ),
inference(rat,[],[s261,s3,s179,s253,s421,s424,s2,s401,s442,s295,s243,s300,s108]) ).
cnf(s465,plain,
( ~ spl0_19
| spl0_6
| ~ spl0_3 ),
inference(rat,[],[s263,s3,s81,s158,s377,s5,s2,s449,s371,s139,s192,s448,s359,s252,s295,s243,s365,s152,s300,s108]) ).
cnf(s466,plain,
( ~ spl0_18
| spl0_6
| ~ spl0_3 ),
inference(rat,[],[s2,s363,s146,s185,s300,s108]) ).
cnf(s467,plain,
( ~ spl0_17
| spl0_6
| ~ spl0_3 ),
inference(rat,[],[s2,s360,s128,s131,s300,s108]) ).
cnf(s468,plain,
( spl0_6
| ~ spl0_3 ),
inference(rat,[],[s2,s157,s142,s197,s4,s467,s466,s465,s464,s300,s108]) ).
cnf(s469,plain,
~ spl0_3,
inference(rat,[],[s449,s5,s448,s81,s4,s263,s361,s3,s155,s156,s416,s417,s445,s455,s468,s365,s295,s152,s243,s252,s359]) ).
cnf(s471,plain,
( ~ spl0_10
| ~ spl0_14
| ~ spl0_2 ),
inference(rat,[],[s81,s5,s127,s187,s183,s167,s165]) ).
cnf(s472,plain,
( spl0_19
| spl0_18
| spl0_17
| spl0_16
| spl0_6
| ~ spl0_2 ),
inference(rat,[],[s5,s164,s238,s2,s471,s105,s19,s9,s18,s350,s4,s22,s183,s165,s41,s167,s463]) ).
cnf(s473,plain,
( ~ spl0_19
| spl0_6
| ~ spl0_2 ),
inference(rat,[],[s81,s5,s263,s330,s3,s105,s314,s317,s2,s168,s338,s139,s192,s183,s167,s165]) ).
cnf(s474,plain,
( ~ spl0_18
| spl0_6
| ~ spl0_2 ),
inference(rat,[],[s2,s166,s312,s146,s185]) ).
cnf(s475,plain,
( ~ spl0_17
| spl0_44
| ~ spl0_2 ),
inference(rat,[],[s9,s19,s18,s163,s131,s41,s167,s463]) ).
cnf(s476,plain,
( spl0_6
| ~ spl0_2 ),
inference(rat,[],[s9,s19,s18,s150,s142,s472,s475,s474,s22,s473,s41,s167,s463]) ).
cnf(s477,plain,
~ spl0_2,
inference(rat,[],[s146,s18,s4,s9,s475,s19,s22,s149,s151,s341,s349,s476,s41,s167,s463]) ).
cnf(s479,plain,
spl0_1,
inference(rat,[],[s1,s469,s462,s456,s477]) ).
cnf(s480,plain,
~ spl0_23,
inference(rat,[],[s221,s479]) ).
cnf(s481,plain,
~ spl0_24,
inference(rat,[],[s220,s479]) ).
cnf(s483,plain,
~ spl0_22,
inference(rat,[],[s175,s479]) ).
cnf(s484,plain,
~ spl0_21,
inference(rat,[],[s172,s479]) ).
cnf(s487,plain,
~ spl0_45,
inference(rat,[],[s41,s481]) ).
cnf(s488,plain,
spl0_25,
inference(rat,[],[s5,s481,s480,s484,s483]) ).
cnf(s489,plain,
spl0_50,
inference(rat,[],[s81,s488]) ).
cnf(s490,plain,
~ spl0_15,
inference(rat,[],[s263,s489]) ).
cnf(s492,plain,
~ spl0_10,
inference(rat,[],[s127,s489]) ).
cnf(s495,plain,
~ spl0_8,
inference(rat,[],[s3,s86,s322,s91,s331,s490,s479,s481]) ).
cnf(s497,plain,
( spl0_9
| spl0_6 ),
inference(rat,[],[s9,s19,s22,s134,s383,s2,s18,s463,s487,s479,s492,s495]) ).
cnf(s498,plain,
~ spl0_9,
inference(rat,[],[s4,s132,s140,s144,s147,s407,s479]) ).
cnf(s499,plain,
~ spl0_42,
inference(rat,[],[s18,s498]) ).
cnf(s500,plain,
spl0_6,
inference(rat,[],[s497,s498]) ).
cnf(s502,plain,
~ spl0_19,
inference(rat,[],[s176,s479,s500]) ).
cnf(s504,plain,
~ spl0_14,
inference(rat,[],[s124,s488,s479,s500]) ).
cnf(s506,plain,
~ spl0_44,
inference(rat,[],[s22,s502]) ).
cnf(s507,plain,
~ spl0_43,
inference(rat,[],[s19,s504]) ).
cnf(s509,plain,
$false,
inference(rat,[],[s9,s487,s499,s463,s506,s507]) ).
fof(f3227,plain,
$false,
inference(avatar_sat_refutation,[],[s509]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG080+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n009.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 19:25:30 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 Running first-order theorem proving
% 0.09/0.20 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.25/1.29 % (3370681)Detected formulas, will run a generic FOF schedule.
% 4.25/1.29 % (3370686)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3052413042:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.25/1.29 % (3370691)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3261066535:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.25/1.29 % (3370688)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3795588953:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.25/1.29 % (3370690)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=504997886:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.25/1.29 % (3370687)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4066816405:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.25/1.29 % (3370689)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1784551156:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.25/1.29 % (3370692)dis-21_1_sil=8000:lcm=predicate:random_seed=882103440:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.25/1.29 % (3370692)Refutation not found, incomplete strategy
% 4.25/1.29 % (3370692)------------------------------
% 4.25/1.29 % (3370692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.25/1.29 % (3370692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.29 % (3370692)CaDiCaL version: 2.1.3
% 4.25/1.29 % (3370692)Termination reason: Refutation not found, incomplete strategy
% 4.25/1.29 % (3370692)Time elapsed: 0.005 s
% 4.25/1.29 % (3370692)Peak memory usage: 88 MB
% 4.25/1.29 % (3370692)Instructions burned: 8 (million)
% 4.25/1.29 % (3370690)Instruction limit reached!
% 4.25/1.29 % (3370690)------------------------------
% 4.25/1.29 % (3370690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.25/1.29 % (3370690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.29 % (3370690)CaDiCaL version: 2.1.3
% 4.25/1.29 % (3370690)Termination reason: Instruction limit
% 4.25/1.29 % (3370690)Termination phase: Saturation
% 4.25/1.29 % (3370690)Time elapsed: 0.050 s
% 4.25/1.29 % (3370690)Peak memory usage: 87 MB
% 4.25/1.29 % (3370690)Instructions burned: 121 (million)
% 4.25/1.29 % (3370689)Instruction limit reached!
% 4.25/1.29 % (3370689)------------------------------
% 4.25/1.29 % (3370689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.25/1.29 % (3370689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.29 % (3370689)CaDiCaL version: 2.1.3
% 4.25/1.29 % (3370689)Termination reason: Instruction limit
% 4.25/1.29 % (3370689)Termination phase: Saturation
% 4.25/1.29 % (3370689)Time elapsed: 0.059 s
% 4.25/1.29 % (3370689)Peak memory usage: 89 MB
% 4.25/1.29 % (3370689)Instructions burned: 110 (million)
% 4.25/1.29 % (3370691)Instruction limit reached!
% 4.25/1.29 % (3370691)------------------------------
% 4.25/1.29 % (3370691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.25/1.29 % (3370691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.29 % (3370691)CaDiCaL version: 2.1.3
% 4.25/1.29 % (3370691)Termination reason: Instruction limit
% 4.25/1.29 % (3370691)Termination phase: Saturation
% 4.25/1.29 % (3370691)Time elapsed: 0.077 s
% 4.25/1.29 % (3370691)Peak memory usage: 89 MB
% 4.25/1.29 % (3370691)Instructions burned: 140 (million)
% 4.25/1.29 [W928 19:25:31.344926580 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.344964533 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.344986188 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.344992720 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.345015393 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.345021576 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 % (3370700)lrs+10_1_sil=8000:sp=occurrence:random_seed=2365778762:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 4.25/1.29 % (3370701)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2790716427:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.25/1.29 % (3370702)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2207691256:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 4.25/1.29 % (3370700)First to succeed.
% 4.25/1.29 % (3370701)Also succeeded, but the first one will report.
% 4.25/1.29 % (3370700)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3370681"
% 4.25/1.29 % (3370692)------------------------------
% 4.25/1.29 % (3370692)------------------------------
% 4.25/1.29 % (3370702)Also succeeded, but the first one will report.
% 4.25/1.29 [W928 19:25:31.564135584 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.564135484 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.564165954 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.564166021 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.564202411 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.564203834 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.564215435 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.564217205 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.564240748 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.564250875 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.564256138 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 [W928 19:25:31.564280962 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.25/1.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.25/1.29 % (3370706)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1133862208:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 4.25/1.29 % (3370686)Also succeeded, but the first one will report.
% 4.25/1.29 % (3370700)Refutation found. Thanks to Tanya!
% 4.25/1.29 % SZS status Theorem for theBenchmark
% 4.25/1.29 % SZS output start Proof for theBenchmark
% See solution above
% 5.19/1.49 % (3370700)------------------------------
% 5.19/1.49 % (3370700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.19/1.49 % (3370700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.19/1.49 % (3370700)CaDiCaL version: 2.1.3
% 5.19/1.49 % (3370700)Termination reason: Refutation
% 5.19/1.49 % (3370700)Time elapsed: 0.051 s
% 5.19/1.49 % (3370700)Peak memory usage: 90 MB
% 5.19/1.49 % (3370700)Instructions burned: 92 (million)
% 5.19/1.49 % (3370700)------------------------------
% 5.19/1.49 % (3370700)------------------------------
% 5.19/1.49 % (3370681)Success in time 0.656 s
% 5.19/1.49 % Vampire exiting
%------------------------------------------------------------------------------