%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG079+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.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 2.96s 1.08s
% Output : Refutation 3.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 48
% Syntax : Number of formulae : 705 ( 79 unt; 43 def)
% Number of atoms : 2305 ( 921 equ)
% Maximal formula atoms : 110 ( 3 avg)
% Number of connectives : 2755 (1155 ~;1215 |; 340 &)
% ( 43 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 70 ( 4 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 45 ( 43 usr; 44 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/sandbox2/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/sandbox2/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/sandbox2/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) = e23
& op2(e21,e23) = e24
& op2(e21,e24) = e20
& op2(e22,e20) = e22
& op2(e22,e21) = e24
& op2(e22,e22) = e21
& op2(e22,e23) = e20
& op2(e22,e24) = e23
& op2(e23,e20) = e23
& op2(e23,e21) = e20
& op2(e23,e22) = e24
& op2(e23,e23) = e21
& op2(e23,e24) = e22
& op2(e24,e20) = e24
& op2(e24,e21) = e23
& op2(e24,e22) = e20
& op2(e24,e23) = e22
& op2(e24,e24) = e21 ),
file('/export/starexec/sandbox2/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/sandbox2/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(f15,plain,
( e20 = h(e14)
| e21 = h(e14)
| e22 = h(e14)
| e23 = h(e14)
| e24 = h(e14) ),
inference(cnf_transformation,[],[f9]) ).
fof(f17,plain,
( e20 = h(e12)
| e21 = h(e12)
| e22 = h(e12)
| e23 = h(e12)
| e24 = h(e12) ),
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(f20,plain,
e14 = j(h(e14)),
inference(cnf_transformation,[],[f9]) ).
fof(f22,plain,
e12 = j(h(e12)),
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(f80,plain,
e21 = op2(e24,e24),
inference(cnf_transformation,[],[f5]) ).
fof(f81,plain,
e22 = op2(e24,e23),
inference(cnf_transformation,[],[f5]) ).
fof(f82,plain,
e20 = 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(f105,plain,
e12 = op1(e14,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f106,plain,
e11 = op1(e14,e13),
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(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(f123,plain,
e10 = op1(e11,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f124,plain,
e11 = op1(e11,e10),
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(f157,plain,
e22 != e23,
inference(cnf_transformation,[],[f2]) ).
fof(f158,plain,
e21 != e24,
inference(cnf_transformation,[],[f2]) ).
fof(f159,plain,
e21 != e23,
inference(cnf_transformation,[],[f2]) ).
fof(f160,plain,
e21 != e22,
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(f177,plain,
( e14 != j(e24)
| spl0_1 ),
inference(avatar_component_clause,[],[f176]) ).
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(f198,plain,
( e14 != j(e23)
| spl0_6 ),
inference(avatar_component_clause,[],[f197]) ).
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(f219,plain,
( e14 != j(e22)
| spl0_11 ),
inference(avatar_component_clause,[],[f218]) ).
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(f231,plain,
( e11 != j(e22)
| spl0_14 ),
inference(avatar_component_clause,[],[f230]) ).
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(f240,plain,
( e14 != j(e21)
| spl0_16 ),
inference(avatar_component_clause,[],[f239]) ).
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(f261,plain,
( e14 != j(e20)
| spl0_21 ),
inference(avatar_component_clause,[],[f260]) ).
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(f281,definition,
( spl0_26
<=> e24 = h(e14) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f283,plain,
( e24 = h(e14)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f285,definition,
( spl0_27
<=> e23 = h(e14) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f287,plain,
( e23 = h(e14)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f289,definition,
( spl0_28
<=> e22 = h(e14) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f291,plain,
( e22 = h(e14)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f293,definition,
( spl0_29
<=> e21 = h(e14) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f295,plain,
( e21 = h(e14)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f297,definition,
( spl0_30
<=> e20 = h(e14) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f299,plain,
( e20 = h(e14)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f300,plain,
( spl0_26
| spl0_27
| spl0_28
| spl0_29
| spl0_30 ),
inference(avatar_split_clause,[],[f15,f297,f293,f289,f285,f281]) ).
fof(f323,definition,
( spl0_36
<=> e24 = h(e12) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f325,plain,
( e24 = h(e12)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f323]) ).
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(f341,plain,
( e20 = h(e12)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f342,plain,
( spl0_36
| spl0_37
| spl0_38
| spl0_39
| spl0_40 ),
inference(avatar_split_clause,[],[f17,f339,f335,f331,f327,f323]) ).
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(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(f369,definition,
( spl0_47
<=> e23 = h(e10) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f371,plain,
( e23 = h(e10)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f377,definition,
( spl0_49
<=> e21 = h(e10) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f379,plain,
( e21 = h(e10)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f377]) ).
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(e21) = 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(e20) = 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(f442,plain,
( e12 = j(e24)
| ~ spl0_36 ),
inference(superposition,[],[f22,f325]) ).
fof(f443,plain,
( spl0_3
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f442,f323,f184]) ).
fof(f445,plain,
( e12 = j(e23)
| ~ spl0_37 ),
inference(superposition,[],[f22,f329]) ).
fof(f446,plain,
( spl0_8
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f445,f327,f205]) ).
fof(f459,plain,
( e14 = j(e22)
| ~ spl0_28 ),
inference(superposition,[],[f20,f291]) ).
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(f469,plain,
( e11 = e14
| ~ spl0_11
| ~ spl0_14 ),
inference(superposition,[],[f232,f220]) ).
fof(f473,plain,
( $false
| ~ spl0_11
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f469,f168]) ).
fof(f474,plain,
( ~ spl0_11
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f473]) ).
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(f481,plain,
( e11 = e14
| ~ spl0_16
| ~ spl0_19 ),
inference(superposition,[],[f253,f241]) ).
fof(f485,plain,
( $false
| ~ spl0_16
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f481,f168]) ).
fof(f486,plain,
( ~ spl0_16
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f485]) ).
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(f590,plain,
( $false
| spl0_11
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f459,f219]) ).
fof(f591,plain,
( spl0_11
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f590]) ).
fof(f626,plain,
( e23 = h(e12)
| ~ spl0_8 ),
inference(superposition,[],[f26,f207]) ).
fof(f627,plain,
( e22 = h(e14)
| ~ spl0_11 ),
inference(superposition,[],[f27,f220]) ).
fof(f629,plain,
( e20 = h(e10)
| ~ spl0_25 ),
inference(superposition,[],[f29,f278]) ).
fof(f630,plain,
( op1(e11,e11) = j(e21)
| ~ spl0_4 ),
inference(superposition,[],[f385,f190]) ).
fof(f631,plain,
( e13 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_17 ),
inference(forward_demodulation,[],[f630,f245]) ).
fof(f632,plain,
( e10 = e13
| ~ spl0_4
| ~ spl0_17 ),
inference(forward_demodulation,[],[f631,f123]) ).
fof(f633,plain,
( $false
| ~ spl0_4
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f632,f172]) ).
fof(f634,plain,
( ~ spl0_4
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f633]) ).
fof(f649,plain,
( e24 = h(e12)
| ~ spl0_3 ),
inference(superposition,[],[f25,f186]) ).
fof(f656,plain,
( op1(e10,e10) = j(e21)
| ~ spl0_5 ),
inference(superposition,[],[f385,f194]) ).
fof(f658,plain,
( e13 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_17 ),
inference(forward_demodulation,[],[f656,f245]) ).
fof(f659,plain,
( e10 = e13
| ~ spl0_5
| ~ spl0_17 ),
inference(forward_demodulation,[],[f658,f129]) ).
fof(f660,plain,
( $false
| ~ spl0_5
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f659,f172]) ).
fof(f661,plain,
( ~ spl0_5
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f660]) ).
fof(f673,plain,
( e23 = e24
| ~ spl0_3
| ~ spl0_37 ),
inference(forward_demodulation,[],[f649,f329]) ).
fof(f677,plain,
( $false
| ~ spl0_3
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f673,f155]) ).
fof(f678,plain,
( ~ spl0_3
| ~ spl0_37 ),
inference(avatar_contradiction_clause,[],[f677]) ).
fof(f706,plain,
( e23 = h(e10)
| ~ spl0_10 ),
inference(superposition,[],[f26,f215]) ).
fof(f714,plain,
( e23 = h(e11)
| ~ spl0_9 ),
inference(superposition,[],[f26,f211]) ).
fof(f715,plain,
( e20 = e23
| ~ spl0_9
| ~ spl0_45 ),
inference(forward_demodulation,[],[f714,f362]) ).
fof(f716,plain,
( $false
| ~ spl0_9
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f715,f162]) ).
fof(f717,plain,
( ~ spl0_9
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f716]) ).
fof(f722,plain,
( e23 = h(e14)
| ~ spl0_6 ),
inference(superposition,[],[f26,f199]) ).
fof(f732,plain,
( e22 = h(e10)
| ~ spl0_15 ),
inference(superposition,[],[f27,f236]) ).
fof(f733,plain,
( e20 = h(e11)
| ~ spl0_24 ),
inference(superposition,[],[f29,f274]) ).
fof(f737,plain,
( e14 = j(e23)
| ~ spl0_27 ),
inference(superposition,[],[f20,f287]) ).
fof(f755,plain,
( j(e20) = op1(j(e24),e10)
| ~ spl0_15 ),
inference(superposition,[],[f387,f236]) ).
fof(f760,plain,
( j(e23) = op1(e12,j(e21))
| ~ spl0_3 ),
inference(superposition,[],[f388,f186]) ).
fof(f763,plain,
( op1(e12,e13) = j(e23)
| ~ spl0_3
| ~ spl0_17 ),
inference(forward_demodulation,[],[f760,f245]) ).
fof(f765,plain,
( e14 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_demodulation,[],[f763,f199]) ).
fof(f767,plain,
( e10 = e14
| ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_demodulation,[],[f765,f116]) ).
fof(f770,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f767,f171]) ).
fof(f771,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f770]) ).
fof(f792,plain,
( $false
| spl0_6
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f737,f198]) ).
fof(f793,plain,
( spl0_6
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f792]) ).
fof(f808,plain,
( op1(e11,e10) = j(e20)
| ~ spl0_4
| ~ spl0_15 ),
inference(forward_demodulation,[],[f755,f190]) ).
fof(f844,plain,
( e14 = op1(e11,e10)
| ~ spl0_4
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_demodulation,[],[f808,f262]) ).
fof(f845,plain,
( e11 = e14
| ~ spl0_4
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_demodulation,[],[f844,f124]) ).
fof(f846,plain,
( $false
| ~ spl0_4
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f845,f168]) ).
fof(f847,plain,
( ~ spl0_4
| ~ spl0_15
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f846]) ).
fof(f848,plain,
( spl0_47
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f706,f213,f369]) ).
fof(f857,plain,
( op1(e11,e11) = j(e21)
| ~ spl0_4 ),
inference(superposition,[],[f385,f190]) ).
fof(f858,plain,
( j(e22) = op1(e11,j(e23))
| ~ spl0_4 ),
inference(superposition,[],[f386,f190]) ).
fof(f860,plain,
( j(e23) = op1(e11,j(e21))
| ~ spl0_4 ),
inference(superposition,[],[f388,f190]) ).
fof(f864,plain,
( e12 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_18 ),
inference(forward_demodulation,[],[f857,f249]) ).
fof(f868,plain,
( e10 = e12
| ~ spl0_4
| ~ spl0_18 ),
inference(forward_demodulation,[],[f864,f123]) ).
fof(f869,plain,
( $false
| ~ spl0_4
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f868,f173]) ).
fof(f870,plain,
( ~ spl0_4
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f869]) ).
fof(f874,plain,
( e11 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_demodulation,[],[f857,f253]) ).
fof(f876,plain,
( e10 = e11
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_demodulation,[],[f874,f123]) ).
fof(f878,plain,
( $false
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f876,f174]) ).
fof(f879,plain,
( ~ spl0_4
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f878]) ).
fof(f885,plain,
( e14 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_16 ),
inference(forward_demodulation,[],[f857,f241]) ).
fof(f887,plain,
( e10 = e14
| ~ spl0_4
| ~ spl0_16 ),
inference(forward_demodulation,[],[f885,f123]) ).
fof(f889,plain,
( $false
| ~ spl0_4
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f887,f171]) ).
fof(f890,plain,
( ~ spl0_4
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f889]) ).
fof(f894,plain,
( op1(e11,e10) = j(e23)
| ~ spl0_4
| ~ spl0_20 ),
inference(forward_demodulation,[],[f860,f257]) ).
fof(f896,plain,
( e14 = op1(e11,e10)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f894,f199]) ).
fof(f897,plain,
( e11 = e14
| ~ spl0_4
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f896,f124]) ).
fof(f898,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f897,f168]) ).
fof(f899,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f898]) ).
fof(f953,plain,
( e12 = op1(e11,e10)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_demodulation,[],[f894,f207]) ).
fof(f960,plain,
( e11 = e12
| ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_demodulation,[],[f953,f124]) ).
fof(f961,plain,
( $false
| ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f960,f170]) ).
fof(f962,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f961]) ).
fof(f968,plain,
( op1(e11,e11) = j(e22)
| ~ spl0_4
| ~ spl0_9 ),
inference(forward_demodulation,[],[f858,f211]) ).
fof(f970,plain,
( e12 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_9
| ~ spl0_13 ),
inference(forward_demodulation,[],[f968,f228]) ).
fof(f971,plain,
( e10 = e12
| ~ spl0_4
| ~ spl0_9
| ~ spl0_13 ),
inference(forward_demodulation,[],[f970,f123]) ).
fof(f972,plain,
( $false
| ~ spl0_4
| ~ spl0_9
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f971,f173]) ).
fof(f973,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f972]) ).
fof(f980,plain,
( e13 = op1(e11,e10)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f894,f203]) ).
fof(f986,plain,
( e11 = e13
| ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f980,f124]) ).
fof(f987,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f986,f169]) ).
fof(f988,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f987]) ).
fof(f1000,plain,
( op1(e11,e11) = j(e22)
| ~ spl0_4
| ~ spl0_9 ),
inference(forward_demodulation,[],[f858,f211]) ).
fof(f1003,plain,
( e13 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_9
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1000,f224]) ).
fof(f1005,plain,
( e10 = e13
| ~ spl0_4
| ~ spl0_9
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1003,f123]) ).
fof(f1008,plain,
( $false
| ~ spl0_4
| ~ spl0_9
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f1005,f172]) ).
fof(f1009,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f1008]) ).
fof(f1017,plain,
( e14 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_demodulation,[],[f1000,f220]) ).
fof(f1023,plain,
( e10 = e14
| ~ spl0_4
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_demodulation,[],[f1017,f123]) ).
fof(f1025,plain,
( $false
| ~ spl0_4
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f1023,f171]) ).
fof(f1026,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f1025]) ).
fof(f1034,plain,
( e11 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_9
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1000,f232]) ).
fof(f1036,plain,
( e10 = e11
| ~ spl0_4
| ~ spl0_9
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1034,f123]) ).
fof(f1038,plain,
( $false
| ~ spl0_4
| ~ spl0_9
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1036,f174]) ).
fof(f1039,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1038]) ).
fof(f1042,plain,
( e21 = e23
| ~ spl0_10
| ~ spl0_49 ),
inference(forward_demodulation,[],[f706,f379]) ).
fof(f1051,plain,
( $false
| ~ spl0_10
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f1042,f159]) ).
fof(f1052,plain,
( ~ spl0_10
| ~ spl0_49 ),
inference(avatar_contradiction_clause,[],[f1051]) ).
fof(f1059,plain,
( spl0_50
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f629,f276,f381]) ).
fof(f1080,plain,
( j(e23) = op1(j(e24),e10)
| ~ spl0_20 ),
inference(superposition,[],[f388,f257]) ).
fof(f1081,plain,
( e21 = h(e10)
| ~ spl0_20 ),
inference(superposition,[],[f28,f257]) ).
fof(f1092,plain,
( e20 = e21
| ~ spl0_20
| ~ spl0_50 ),
inference(forward_demodulation,[],[f1081,f383]) ).
fof(f1102,plain,
( $false
| ~ spl0_20
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f1092,f164]) ).
fof(f1103,plain,
( ~ spl0_20
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f1102]) ).
fof(f1126,plain,
( e24 = h(e12)
| ~ spl0_3 ),
inference(superposition,[],[f25,f186]) ).
fof(f1200,plain,
( op1(e10,e10) = j(e23)
| ~ spl0_5
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1080,f194]) ).
fof(f1201,plain,
( e11 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1200,f211]) ).
fof(f1202,plain,
( e10 = e11
| ~ spl0_5
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1201,f129]) ).
fof(f1203,plain,
( $false
| ~ spl0_5
| ~ spl0_9
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1202,f174]) ).
fof(f1204,plain,
( ~ spl0_5
| ~ spl0_9
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f1203]) ).
fof(f1207,plain,
( e21 = e24
| ~ spl0_3
| ~ spl0_39 ),
inference(forward_demodulation,[],[f1126,f337]) ).
fof(f1219,plain,
( $false
| ~ spl0_3
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f1207,f158]) ).
fof(f1220,plain,
( ~ spl0_3
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f1219]) ).
fof(f1257,plain,
( e24 = h(e10)
| ~ spl0_5 ),
inference(superposition,[],[f25,f194]) ).
fof(f1261,plain,
( op1(e10,e10) = j(e21)
| ~ spl0_5 ),
inference(superposition,[],[f385,f194]) ).
fof(f1268,plain,
( e14 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1261,f241]) ).
fof(f1272,plain,
( e10 = e14
| ~ spl0_5
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1268,f129]) ).
fof(f1274,plain,
( $false
| ~ spl0_5
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1272,f171]) ).
fof(f1275,plain,
( ~ spl0_5
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1274]) ).
fof(f1280,plain,
( spl0_49
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f1081,f255,f377]) ).
fof(f1288,plain,
( e24 = h(e14)
| ~ spl0_1 ),
inference(superposition,[],[f25,f178]) ).
fof(f1291,plain,
( op1(e14,e14) = j(e21)
| ~ spl0_1 ),
inference(superposition,[],[f385,f178]) ).
fof(f1298,plain,
( e14 = op1(e14,e14)
| ~ spl0_1
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1291,f241]) ).
fof(f1302,plain,
( e12 = e14
| ~ spl0_1
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1298,f105]) ).
fof(f1304,plain,
( $false
| ~ spl0_1
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1302,f166]) ).
fof(f1305,plain,
( ~ spl0_1
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1304]) ).
fof(f1362,plain,
( j(e23) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(superposition,[],[f388,f182]) ).
fof(f1379,plain,
( op1(e13,e14) = j(e23)
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1362,f241]) ).
fof(f1381,plain,
( e13 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1379,f203]) ).
fof(f1382,plain,
( e10 = e13
| ~ spl0_2
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1381,f110]) ).
fof(f1383,plain,
( $false
| ~ spl0_2
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1382,f172]) ).
fof(f1384,plain,
( ~ spl0_2
| ~ spl0_7
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1383]) ).
fof(f1420,plain,
( e23 = e24
| ~ spl0_5
| ~ spl0_47 ),
inference(forward_demodulation,[],[f1257,f371]) ).
fof(f1428,plain,
( $false
| ~ spl0_5
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f1420,f155]) ).
fof(f1429,plain,
( ~ spl0_5
| ~ spl0_47 ),
inference(avatar_contradiction_clause,[],[f1428]) ).
fof(f1437,plain,
( e21 = e23
| ~ spl0_8
| ~ spl0_39 ),
inference(forward_demodulation,[],[f626,f337]) ).
fof(f1443,plain,
( $false
| ~ spl0_8
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f1437,f159]) ).
fof(f1444,plain,
( ~ spl0_8
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f1443]) ).
fof(f1447,plain,
( spl0_37
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f626,f205,f327]) ).
fof(f1452,plain,
( op1(e10,e10) = j(e21)
| ~ spl0_5 ),
inference(superposition,[],[f385,f194]) ).
fof(f1455,plain,
( j(e23) = op1(e10,j(e21))
| ~ spl0_5 ),
inference(superposition,[],[f388,f194]) ).
fof(f1459,plain,
( e11 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1452,f253]) ).
fof(f1463,plain,
( e10 = e11
| ~ spl0_5
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1459,f129]) ).
fof(f1466,plain,
( $false
| ~ spl0_5
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1463,f174]) ).
fof(f1467,plain,
( ~ spl0_5
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1466]) ).
fof(f1472,plain,
( spl0_27
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f722,f197,f285]) ).
fof(f1478,plain,
( e12 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1452,f249]) ).
fof(f1484,plain,
( e10 = e12
| ~ spl0_5
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1478,f129]) ).
fof(f1487,plain,
( $false
| ~ spl0_5
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1484,f173]) ).
fof(f1488,plain,
( ~ spl0_5
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1487]) ).
fof(f1492,plain,
( op1(e10,e10) = j(e23)
| ~ spl0_5
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1455,f257]) ).
fof(f1494,plain,
( e14 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1492,f199]) ).
fof(f1495,plain,
( e10 = e14
| ~ spl0_5
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1494,f129]) ).
fof(f1496,plain,
( $false
| ~ spl0_5
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1495,f171]) ).
fof(f1497,plain,
( ~ spl0_5
| ~ spl0_6
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f1496]) ).
fof(f1499,plain,
( e23 = e24
| ~ spl0_1
| ~ spl0_27 ),
inference(forward_demodulation,[],[f1288,f287]) ).
fof(f1501,plain,
( spl0_45
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f733,f272,f360]) ).
fof(f1510,plain,
( $false
| ~ spl0_1
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f1499,f155]) ).
fof(f1511,plain,
( ~ spl0_1
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f1510]) ).
fof(f1523,plain,
( j(e22) = op1(e14,j(e23))
| ~ spl0_1 ),
inference(superposition,[],[f386,f178]) ).
fof(f1528,plain,
( op1(e14,e12) = j(e22)
| ~ spl0_1
| ~ spl0_8 ),
inference(forward_demodulation,[],[f1523,f207]) ).
fof(f1532,plain,
( e13 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_8
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1528,f224]) ).
fof(f1533,plain,
( e10 = e13
| ~ spl0_1
| ~ spl0_8
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1532,f107]) ).
fof(f1534,plain,
( $false
| ~ spl0_1
| ~ spl0_8
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f1533,f172]) ).
fof(f1535,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f1534]) ).
fof(f1551,plain,
( e23 = h(e10)
| ~ spl0_10 ),
inference(superposition,[],[f26,f215]) ).
fof(f1558,plain,
( e22 = h(e11)
| ~ spl0_14 ),
inference(superposition,[],[f27,f232]) ).
fof(f1572,plain,
( e21 = h(e12)
| ~ spl0_18 ),
inference(superposition,[],[f28,f249]) ).
fof(f1578,plain,
( e14 = j(e24)
| ~ spl0_26 ),
inference(superposition,[],[f20,f283]) ).
fof(f1588,plain,
( e12 = j(e21)
| ~ spl0_39 ),
inference(superposition,[],[f22,f337]) ).
fof(f1594,plain,
( e14 = op1(e14,j(e20))
| ~ spl0_1 ),
inference(superposition,[],[f389,f178]) ).
fof(f1597,plain,
( e14 = op1(e14,e11)
| ~ spl0_1
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1594,f274]) ).
fof(f1599,plain,
( e13 = e14
| ~ spl0_1
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1597,f108]) ).
fof(f1602,plain,
( $false
| ~ spl0_1
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f1599,f165]) ).
fof(f1603,plain,
( ~ spl0_1
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f1602]) ).
fof(f1606,plain,
( spl0_39
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f1572,f247,f335]) ).
fof(f1614,plain,
( $false
| spl0_1
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f1578,f177]) ).
fof(f1615,plain,
( spl0_1
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f1614]) ).
fof(f1659,plain,
( e21 = h(e11)
| ~ spl0_19 ),
inference(superposition,[],[f28,f253]) ).
fof(f1670,plain,
( e12 = j(e22)
| ~ spl0_38 ),
inference(superposition,[],[f22,f333]) ).
fof(f1671,plain,
( spl0_13
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f1670,f331,f226]) ).
fof(f1676,plain,
( e12 = j(e20)
| ~ spl0_40 ),
inference(superposition,[],[f22,f341]) ).
fof(f1698,plain,
( e11 = e12
| ~ spl0_19
| ~ spl0_39 ),
inference(forward_demodulation,[],[f1588,f253]) ).
fof(f1702,plain,
( $false
| ~ spl0_19
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f1698,f170]) ).
fof(f1703,plain,
( ~ spl0_19
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f1702]) ).
fof(f1723,plain,
( op1(e12,e12) = j(e21)
| ~ spl0_3 ),
inference(superposition,[],[f385,f186]) ).
fof(f1724,plain,
( j(e22) = op1(e12,j(e23))
| ~ spl0_3 ),
inference(superposition,[],[f386,f186]) ).
fof(f1726,plain,
( j(e23) = op1(e12,j(e21))
| ~ spl0_3 ),
inference(superposition,[],[f388,f186]) ).
fof(f1731,plain,
( op1(e12,e14) = j(e22)
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1724,f199]) ).
fof(f1735,plain,
( e13 = op1(e12,e14)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1731,f224]) ).
fof(f1736,plain,
( e11 = e13
| ~ spl0_3
| ~ spl0_6
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1735,f115]) ).
fof(f1737,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f1736,f169]) ).
fof(f1738,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f1737]) ).
fof(f1739,plain,
( e21 = e23
| ~ spl0_9
| ~ spl0_44 ),
inference(forward_demodulation,[],[f714,f358]) ).
fof(f1746,plain,
( $false
| ~ spl0_9
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f1739,f159]) ).
fof(f1747,plain,
( ~ spl0_9
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f1746]) ).
fof(f1758,plain,
( e14 = op1(e12,e12)
| ~ spl0_3
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1723,f241]) ).
fof(f1760,plain,
( e13 = e14
| ~ spl0_3
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1758,f117]) ).
fof(f1761,plain,
( $false
| ~ spl0_3
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1760,f165]) ).
fof(f1762,plain,
( ~ spl0_3
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1761]) ).
fof(f1766,plain,
( op1(e12,e13) = j(e23)
| ~ spl0_3
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1726,f245]) ).
fof(f1768,plain,
( e11 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1766,f211]) ).
fof(f1769,plain,
( e10 = e11
| ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1768,f116]) ).
fof(f1770,plain,
( $false
| ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1769,f174]) ).
fof(f1771,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1770]) ).
fof(f1786,plain,
( j(e22) = op1(e14,j(e23))
| ~ spl0_1 ),
inference(superposition,[],[f386,f178]) ).
fof(f1788,plain,
( j(e23) = op1(e14,j(e21))
| ~ spl0_1 ),
inference(superposition,[],[f388,f178]) ).
fof(f1789,plain,
( e14 = op1(e14,j(e20))
| ~ spl0_1 ),
inference(superposition,[],[f389,f178]) ).
fof(f1791,plain,
( op1(e14,e12) = j(e23)
| ~ spl0_1
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1788,f249]) ).
fof(f1795,plain,
( e11 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1791,f211]) ).
fof(f1798,plain,
( e10 = e11
| ~ spl0_1
| ~ spl0_9
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1795,f107]) ).
fof(f1799,plain,
( $false
| ~ spl0_1
| ~ spl0_9
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1798,f174]) ).
fof(f1800,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1799]) ).
fof(f1804,plain,
( e20 = e23
| ~ spl0_10
| ~ spl0_50 ),
inference(forward_demodulation,[],[f1551,f383]) ).
fof(f1820,plain,
( $false
| ~ spl0_10
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f1804,f162]) ).
fof(f1821,plain,
( ~ spl0_10
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f1820]) ).
fof(f1830,plain,
( op1(e14,e13) = j(e22)
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1786,f203]) ).
fof(f1831,plain,
( e13 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1791,f203]) ).
fof(f1833,plain,
( e10 = e13
| ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1831,f107]) ).
fof(f1834,plain,
( $false
| ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1833,f172]) ).
fof(f1835,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1834]) ).
fof(f1852,plain,
( e11 = j(e22)
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1830,f106]) ).
fof(f1854,plain,
( $false
| ~ spl0_1
| ~ spl0_7
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f1852,f231]) ).
fof(f1855,plain,
( ~ spl0_1
| ~ spl0_7
| spl0_14 ),
inference(avatar_contradiction_clause,[],[f1854]) ).
fof(f1857,plain,
( e21 = e22
| ~ spl0_14
| ~ spl0_44 ),
inference(forward_demodulation,[],[f1558,f358]) ).
fof(f1865,plain,
( op1(e14,e12) = j(e22)
| ~ spl0_1
| ~ spl0_8 ),
inference(forward_demodulation,[],[f1786,f207]) ).
fof(f1869,plain,
( $false
| ~ spl0_14
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f1857,f160]) ).
fof(f1870,plain,
( ~ spl0_14
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f1869]) ).
fof(f1880,plain,
( spl0_28
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f627,f218,f289]) ).
fof(f1884,plain,
( e14 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_8
| ~ spl0_11 ),
inference(forward_demodulation,[],[f1865,f220]) ).
fof(f1885,plain,
( e10 = e14
| ~ spl0_1
| ~ spl0_8
| ~ spl0_11 ),
inference(forward_demodulation,[],[f1884,f107]) ).
fof(f1886,plain,
( $false
| ~ spl0_1
| ~ spl0_8
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f1885,f171]) ).
fof(f1887,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f1886]) ).
fof(f1891,plain,
( e12 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_demodulation,[],[f1865,f228]) ).
fof(f1892,plain,
( e10 = e12
| ~ spl0_1
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_demodulation,[],[f1891,f107]) ).
fof(f1893,plain,
( $false
| ~ spl0_1
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f1892,f173]) ).
fof(f1894,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f1893]) ).
fof(f1895,plain,
( e20 = e22
| ~ spl0_15
| ~ spl0_50 ),
inference(forward_demodulation,[],[f732,f383]) ).
fof(f1901,plain,
( $false
| ~ spl0_15
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f1895,f163]) ).
fof(f1902,plain,
( ~ spl0_15
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f1901]) ).
fof(f1908,plain,
( e14 = op1(e14,e14)
| ~ spl0_1
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1789,f262]) ).
fof(f1910,plain,
( e12 = e14
| ~ spl0_1
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1908,f105]) ).
fof(f1912,plain,
( $false
| ~ spl0_1
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1910,f166]) ).
fof(f1913,plain,
( ~ spl0_1
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1912]) ).
fof(f1916,plain,
( e14 = op1(e14,e13)
| ~ spl0_1
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1789,f266]) ).
fof(f1918,plain,
( e11 = e14
| ~ spl0_1
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1916,f106]) ).
fof(f1919,plain,
( $false
| ~ spl0_1
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1918,f168]) ).
fof(f1920,plain,
( ~ spl0_1
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f1919]) ).
fof(f1922,plain,
( e14 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1789,f270]) ).
fof(f1924,plain,
( e10 = e14
| ~ spl0_1
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1922,f107]) ).
fof(f1925,plain,
( $false
| ~ spl0_1
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1924,f171]) ).
fof(f1926,plain,
( ~ spl0_1
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f1925]) ).
fof(f1944,plain,
( j(e22) = op1(e12,j(e23))
| ~ spl0_3 ),
inference(superposition,[],[f386,f186]) ).
fof(f1951,plain,
( op1(e12,e13) = j(e22)
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1944,f203]) ).
fof(f1955,plain,
( e14 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_11 ),
inference(forward_demodulation,[],[f1951,f220]) ).
fof(f1956,plain,
( e10 = e14
| ~ spl0_3
| ~ spl0_7
| ~ spl0_11 ),
inference(forward_demodulation,[],[f1955,f116]) ).
fof(f1957,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f1956,f171]) ).
fof(f1958,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f1957]) ).
fof(f1990,plain,
( j(e22) = op1(e13,j(e23))
| ~ spl0_2 ),
inference(superposition,[],[f386,f182]) ).
fof(f1991,plain,
( j(e20) = op1(e13,j(e22))
| ~ spl0_2 ),
inference(superposition,[],[f387,f182]) ).
fof(f1992,plain,
( j(e23) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(superposition,[],[f388,f182]) ).
fof(f1993,plain,
( e13 = op1(e13,j(e20))
| ~ spl0_2 ),
inference(superposition,[],[f389,f182]) ).
fof(f1995,plain,
( op1(e13,e11) = j(e23)
| ~ spl0_2
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1992,f253]) ).
fof(f1999,plain,
( e14 = op1(e13,e11)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1995,f199]) ).
fof(f2002,plain,
( e12 = e14
| ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1999,f113]) ).
fof(f2004,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2002,f166]) ).
fof(f2005,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2004]) ).
fof(f2015,plain,
( op1(e13,e14) = j(e23)
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1992,f241]) ).
fof(f2022,plain,
( e12 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2015,f207]) ).
fof(f2025,plain,
( e10 = e12
| ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2022,f110]) ).
fof(f2026,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2025,f173]) ).
fof(f2027,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2026]) ).
fof(f2031,plain,
( spl0_23
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1676,f339,f268]) ).
fof(f2036,plain,
( e13 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1993,f262]) ).
fof(f2040,plain,
( op1(e13,e14) = j(e22)
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1990,f199]) ).
fof(f2042,plain,
( e10 = e13
| ~ spl0_2
| ~ spl0_21 ),
inference(forward_demodulation,[],[f2036,f110]) ).
fof(f2044,plain,
( e11 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_14 ),
inference(forward_demodulation,[],[f2040,f232]) ).
fof(f2046,plain,
( $false
| ~ spl0_2
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f2042,f172]) ).
fof(f2047,plain,
( ~ spl0_2
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f2046]) ).
fof(f2050,plain,
( e10 = e11
| ~ spl0_2
| ~ spl0_6
| ~ spl0_14 ),
inference(forward_demodulation,[],[f2044,f110]) ).
fof(f2053,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f2050,f174]) ).
fof(f2054,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f2053]) ).
fof(f2059,plain,
( e13 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1993,f270]) ).
fof(f2065,plain,
( e11 = e13
| ~ spl0_2
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2059,f112]) ).
fof(f2067,plain,
( $false
| ~ spl0_2
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f2065,f169]) ).
fof(f2068,plain,
( ~ spl0_2
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f2067]) ).
fof(f2075,plain,
( e13 = op1(e13,e11)
| ~ spl0_2
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1993,f274]) ).
fof(f2079,plain,
( e12 = e13
| ~ spl0_2
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2075,f113]) ).
fof(f2081,plain,
( $false
| ~ spl0_2
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f2079,f167]) ).
fof(f2082,plain,
( ~ spl0_2
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f2081]) ).
fof(f2098,plain,
( op1(e13,e11) = j(e20)
| ~ spl0_2
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1991,f232]) ).
fof(f2103,plain,
( e13 = op1(e13,e11)
| ~ spl0_2
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2098,f266]) ).
fof(f2105,plain,
( e12 = e13
| ~ spl0_2
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2103,f113]) ).
fof(f2106,plain,
( $false
| ~ spl0_2
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f2105,f167]) ).
fof(f2107,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f2106]) ).
fof(f2146,plain,
( e14 = j(e20)
| ~ spl0_30 ),
inference(superposition,[],[f20,f299]) ).
fof(f2147,plain,
( $false
| spl0_21
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f2146,f261]) ).
fof(f2148,plain,
( spl0_21
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f2147]) ).
fof(f2153,plain,
( e14 = j(e21)
| ~ spl0_29 ),
inference(superposition,[],[f20,f295]) ).
fof(f2154,plain,
( $false
| spl0_16
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f2153,f240]) ).
fof(f2155,plain,
( spl0_16
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f2154]) ).
fof(f2181,plain,
( j(e23) = op1(e10,j(e21))
| ~ spl0_5 ),
inference(superposition,[],[f388,f194]) ).
fof(f2184,plain,
( op1(e10,e10) = j(e23)
| ~ spl0_5
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2181,f257]) ).
fof(f2188,plain,
( e12 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2184,f207]) ).
fof(f2191,plain,
( e10 = e12
| ~ spl0_5
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2188,f129]) ).
fof(f2193,plain,
( $false
| ~ spl0_5
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2191,f173]) ).
fof(f2194,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2193]) ).
fof(f2198,plain,
( e12 = e14
| ~ spl0_11
| ~ spl0_13 ),
inference(forward_demodulation,[],[f220,f228]) ).
fof(f2212,plain,
( e13 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2184,f203]) ).
fof(f2213,plain,
( $false
| ~ spl0_11
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f2198,f166]) ).
fof(f2214,plain,
( ~ spl0_11
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f2213]) ).
fof(f2218,plain,
( e10 = e13
| ~ spl0_5
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2212,f129]) ).
fof(f2219,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2218,f172]) ).
fof(f2220,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2219]) ).
fof(f2222,plain,
( e22 = e23
| ~ spl0_6
| ~ spl0_28 ),
inference(forward_demodulation,[],[f722,f291]) ).
fof(f2235,plain,
( $false
| ~ spl0_6
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f2222,f157]) ).
fof(f2236,plain,
( ~ spl0_6
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f2235]) ).
fof(f2242,plain,
( op1(e12,e12) = j(e21)
| ~ spl0_3 ),
inference(superposition,[],[f385,f186]) ).
fof(f2243,plain,
( j(e22) = op1(e12,j(e23))
| ~ spl0_3 ),
inference(superposition,[],[f386,f186]) ).
fof(f2245,plain,
( j(e23) = op1(e12,j(e21))
| ~ spl0_3 ),
inference(superposition,[],[f388,f186]) ).
fof(f2246,plain,
( e12 = op1(e12,j(e20))
| ~ spl0_3 ),
inference(superposition,[],[f389,f186]) ).
fof(f2248,plain,
( op1(e12,e10) = j(e23)
| ~ spl0_3
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2245,f257]) ).
fof(f2250,plain,
( op1(e12,e14) = j(e22)
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f2243,f199]) ).
fof(f2252,plain,
( e14 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2248,f199]) ).
fof(f2254,plain,
( e12 = op1(e12,e14)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_13 ),
inference(forward_demodulation,[],[f2250,f228]) ).
fof(f2255,plain,
( e12 = e14
| ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2252,f119]) ).
fof(f2257,plain,
( e11 = e12
| ~ spl0_3
| ~ spl0_6
| ~ spl0_13 ),
inference(forward_demodulation,[],[f2254,f115]) ).
fof(f2258,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2255,f166]) ).
fof(f2259,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2258]) ).
fof(f2262,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f2257,f170]) ).
fof(f2263,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f2262]) ).
fof(f2264,plain,
( e20 = e21
| ~ spl0_19
| ~ spl0_45 ),
inference(forward_demodulation,[],[f1659,f362]) ).
fof(f2272,plain,
( e11 = op1(e12,e12)
| ~ spl0_3
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2242,f253]) ).
fof(f2275,plain,
( $false
| ~ spl0_19
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f2264,f164]) ).
fof(f2276,plain,
( ~ spl0_19
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f2275]) ).
fof(f2282,plain,
( spl0_44
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f1659,f251,f356]) ).
fof(f2285,plain,
( e12 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2246,f266]) ).
fof(f2287,plain,
( e10 = e12
| ~ spl0_3
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2285,f116]) ).
fof(f2289,plain,
( $false
| ~ spl0_3
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f2287,f173]) ).
fof(f2290,plain,
( ~ spl0_3
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f2289]) ).
fof(f2296,plain,
( e12 = op1(e12,e14)
| ~ spl0_3
| ~ spl0_21 ),
inference(forward_demodulation,[],[f2246,f262]) ).
fof(f2298,plain,
( e11 = e12
| ~ spl0_3
| ~ spl0_21 ),
inference(forward_demodulation,[],[f2296,f115]) ).
fof(f2300,plain,
( $false
| ~ spl0_3
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f2298,f170]) ).
fof(f2301,plain,
( ~ spl0_3
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f2300]) ).
fof(f2307,plain,
( e12 = op1(e12,e12)
| ~ spl0_3
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2246,f270]) ).
fof(f2309,plain,
( e11 = e12
| ~ spl0_3
| ~ spl0_19
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2307,f2272]) ).
fof(f2310,plain,
( $false
| ~ spl0_3
| ~ spl0_19
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f2309,f170]) ).
fof(f2311,plain,
( ~ spl0_3
| ~ spl0_19
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f2310]) ).
fof(f2329,plain,
( j(e22) = op1(e13,j(e23))
| ~ spl0_2 ),
inference(superposition,[],[f386,f182]) ).
fof(f2331,plain,
( j(e23) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(superposition,[],[f388,f182]) ).
fof(f2336,plain,
( op1(e13,e12) = j(e22)
| ~ spl0_2
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2329,f207]) ).
fof(f2340,plain,
( e14 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2336,f220]) ).
fof(f2341,plain,
( e11 = e14
| ~ spl0_2
| ~ spl0_8
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2340,f112]) ).
fof(f2342,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f2341,f168]) ).
fof(f2343,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f2342]) ).
fof(f2355,plain,
( op1(e13,e14) = j(e23)
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2331,f241]) ).
fof(f2360,plain,
( op1(e13,e11) = j(e22)
| ~ spl0_2
| ~ spl0_9 ),
inference(forward_demodulation,[],[f2329,f211]) ).
fof(f2361,plain,
( e11 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2355,f211]) ).
fof(f2364,plain,
( e10 = e11
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2361,f110]) ).
fof(f2366,plain,
( $false
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2364,f174]) ).
fof(f2367,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2366]) ).
fof(f2379,plain,
( e14 = op1(e13,e11)
| ~ spl0_2
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2360,f220]) ).
fof(f2382,plain,
( e12 = e14
| ~ spl0_2
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2379,f113]) ).
fof(f2384,plain,
( $false
| ~ spl0_2
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f2382,f166]) ).
fof(f2385,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f2384]) ).
fof(f2388,plain,
( e11 = e14
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f199,f211]) ).
fof(f2400,plain,
( $false
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f2388,f168]) ).
fof(f2401,plain,
( ~ spl0_6
| ~ spl0_9 ),
inference(avatar_contradiction_clause,[],[f2400]) ).
fof(f2428,plain,
( j(e22) = op1(e12,j(e23))
| ~ spl0_3 ),
inference(superposition,[],[f386,f186]) ).
fof(f2429,plain,
( j(e20) = op1(e12,j(e22))
| ~ spl0_3 ),
inference(superposition,[],[f387,f186]) ).
fof(f2434,plain,
( op1(e12,e14) = j(e20)
| ~ spl0_3
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2429,f220]) ).
fof(f2435,plain,
( op1(e12,e10) = j(e22)
| ~ spl0_3
| ~ spl0_10 ),
inference(forward_demodulation,[],[f2428,f215]) ).
fof(f2439,plain,
( e14 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_10
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2435,f220]) ).
fof(f2440,plain,
( e12 = e14
| ~ spl0_3
| ~ spl0_10
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2439,f119]) ).
fof(f2441,plain,
( $false
| ~ spl0_3
| ~ spl0_10
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f2440,f166]) ).
fof(f2442,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f2441]) ).
fof(f2452,plain,
( e12 = op1(e12,e14)
| ~ spl0_3
| ~ spl0_11
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2434,f270]) ).
fof(f2459,plain,
( e11 = e12
| ~ spl0_3
| ~ spl0_11
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2452,f115]) ).
fof(f2462,plain,
( $false
| ~ spl0_3
| ~ spl0_11
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f2459,f170]) ).
fof(f2463,plain,
( ~ spl0_3
| ~ spl0_11
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f2462]) ).
fof(f2489,plain,
( op1(e14,e14) = j(e21)
| ~ spl0_1 ),
inference(superposition,[],[f385,f178]) ).
fof(f2498,plain,
( e13 = op1(e14,e14)
| ~ spl0_1
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2489,f245]) ).
fof(f2502,plain,
( e12 = e13
| ~ spl0_1
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2498,f105]) ).
fof(f2503,plain,
( $false
| ~ spl0_1
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2502,f167]) ).
fof(f2504,plain,
( ~ spl0_1
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2503]) ).
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(s6,plain,
( spl0_26
| spl0_27
| spl0_28
| spl0_29
| spl0_30 ),
inference(sat_conversion,[],[f300]) ).
cnf(s8,plain,
( spl0_36
| spl0_37
| spl0_38
| spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f342]) ).
cnf(s9,plain,
( spl0_41
| spl0_42
| spl0_43
| spl0_44
| spl0_45 ),
inference(sat_conversion,[],[f363]) ).
cnf(s12,plain,
( spl0_3
| ~ spl0_36 ),
inference(sat_conversion,[],[f443]) ).
cnf(s13,plain,
( spl0_8
| ~ spl0_37 ),
inference(sat_conversion,[],[f446]) ).
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(s21,plain,
( ~ spl0_11
| ~ spl0_14 ),
inference(sat_conversion,[],[f474]) ).
cnf(s22,plain,
( spl0_19
| ~ spl0_44 ),
inference(sat_conversion,[],[f480]) ).
cnf(s24,plain,
( ~ spl0_16
| ~ spl0_19 ),
inference(sat_conversion,[],[f486]) ).
cnf(s41,plain,
( spl0_24
| ~ spl0_45 ),
inference(sat_conversion,[],[f557]) ).
cnf(s48,plain,
( spl0_11
| ~ spl0_28 ),
inference(sat_conversion,[],[f591]) ).
cnf(s53,plain,
( ~ spl0_4
| ~ spl0_17 ),
inference(sat_conversion,[],[f634]) ).
cnf(s57,plain,
( ~ spl0_5
| ~ spl0_17 ),
inference(sat_conversion,[],[f661]) ).
cnf(s59,plain,
( ~ spl0_3
| ~ spl0_37 ),
inference(sat_conversion,[],[f678]) ).
cnf(s67,plain,
( ~ spl0_9
| ~ spl0_45 ),
inference(sat_conversion,[],[f717]) ).
cnf(s72,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(sat_conversion,[],[f771]) ).
cnf(s77,plain,
( spl0_6
| ~ spl0_27 ),
inference(sat_conversion,[],[f793]) ).
cnf(s90,plain,
( ~ spl0_4
| ~ spl0_15
| ~ spl0_21 ),
inference(sat_conversion,[],[f847]) ).
cnf(s91,plain,
( ~ spl0_10
| spl0_47 ),
inference(sat_conversion,[],[f848]) ).
cnf(s92,plain,
( ~ spl0_4
| ~ spl0_18 ),
inference(sat_conversion,[],[f870]) ).
cnf(s93,plain,
( ~ spl0_4
| ~ spl0_19 ),
inference(sat_conversion,[],[f879]) ).
cnf(s95,plain,
( ~ spl0_4
| ~ spl0_16 ),
inference(sat_conversion,[],[f890]) ).
cnf(s97,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_20 ),
inference(sat_conversion,[],[f899]) ).
cnf(s107,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(sat_conversion,[],[f962]) ).
cnf(s109,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_13 ),
inference(sat_conversion,[],[f973]) ).
cnf(s112,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(sat_conversion,[],[f988]) ).
cnf(s115,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_12 ),
inference(sat_conversion,[],[f1009]) ).
cnf(s118,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_11 ),
inference(sat_conversion,[],[f1026]) ).
cnf(s120,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_14 ),
inference(sat_conversion,[],[f1039]) ).
cnf(s122,plain,
( ~ spl0_10
| ~ spl0_49 ),
inference(sat_conversion,[],[f1052]) ).
cnf(s125,plain,
( ~ spl0_25
| spl0_50 ),
inference(sat_conversion,[],[f1059]) ).
cnf(s132,plain,
( ~ spl0_20
| ~ spl0_50 ),
inference(sat_conversion,[],[f1103]) ).
cnf(s147,plain,
( ~ spl0_5
| ~ spl0_9
| ~ spl0_20 ),
inference(sat_conversion,[],[f1204]) ).
cnf(s150,plain,
( ~ spl0_3
| ~ spl0_39 ),
inference(sat_conversion,[],[f1220]) ).
cnf(s158,plain,
( ~ spl0_5
| ~ spl0_16 ),
inference(sat_conversion,[],[f1275]) ).
cnf(s160,plain,
( ~ spl0_20
| spl0_49 ),
inference(sat_conversion,[],[f1280]) ).
cnf(s164,plain,
( ~ spl0_1
| ~ spl0_16 ),
inference(sat_conversion,[],[f1305]) ).
cnf(s182,plain,
( ~ spl0_2
| ~ spl0_7
| ~ spl0_16 ),
inference(sat_conversion,[],[f1384]) ).
cnf(s187,plain,
( ~ spl0_5
| ~ spl0_47 ),
inference(sat_conversion,[],[f1429]) ).
cnf(s192,plain,
( ~ spl0_8
| ~ spl0_39 ),
inference(sat_conversion,[],[f1444]) ).
cnf(s194,plain,
( ~ spl0_8
| spl0_37 ),
inference(sat_conversion,[],[f1447]) ).
cnf(s195,plain,
( ~ spl0_5
| ~ spl0_19 ),
inference(sat_conversion,[],[f1467]) ).
cnf(s198,plain,
( ~ spl0_6
| spl0_27 ),
inference(sat_conversion,[],[f1472]) ).
cnf(s199,plain,
( ~ spl0_5
| ~ spl0_18 ),
inference(sat_conversion,[],[f1488]) ).
cnf(s202,plain,
( ~ spl0_5
| ~ spl0_6
| ~ spl0_20 ),
inference(sat_conversion,[],[f1497]) ).
cnf(s203,plain,
( ~ spl0_24
| spl0_45 ),
inference(sat_conversion,[],[f1501]) ).
cnf(s205,plain,
( ~ spl0_1
| ~ spl0_27 ),
inference(sat_conversion,[],[f1511]) ).
cnf(s210,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_12 ),
inference(sat_conversion,[],[f1535]) ).
cnf(s217,plain,
( ~ spl0_1
| ~ spl0_24 ),
inference(sat_conversion,[],[f1603]) ).
cnf(s222,plain,
( ~ spl0_18
| spl0_39 ),
inference(sat_conversion,[],[f1606]) ).
cnf(s224,plain,
( spl0_1
| ~ spl0_26 ),
inference(sat_conversion,[],[f1615]) ).
cnf(s228,plain,
( spl0_13
| ~ spl0_38 ),
inference(sat_conversion,[],[f1671]) ).
cnf(s235,plain,
( ~ spl0_19
| ~ spl0_39 ),
inference(sat_conversion,[],[f1703]) ).
cnf(s241,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_12 ),
inference(sat_conversion,[],[f1738]) ).
cnf(s242,plain,
( ~ spl0_9
| ~ spl0_44 ),
inference(sat_conversion,[],[f1747]) ).
cnf(s246,plain,
( ~ spl0_3
| ~ spl0_16 ),
inference(sat_conversion,[],[f1762]) ).
cnf(s248,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(sat_conversion,[],[f1771]) ).
cnf(s254,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_18 ),
inference(sat_conversion,[],[f1800]) ).
cnf(s260,plain,
( ~ spl0_10
| ~ spl0_50 ),
inference(sat_conversion,[],[f1821]) ).
cnf(s263,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(sat_conversion,[],[f1835]) ).
cnf(s268,plain,
( ~ spl0_1
| ~ spl0_7
| spl0_14 ),
inference(sat_conversion,[],[f1855]) ).
cnf(s271,plain,
( ~ spl0_14
| ~ spl0_44 ),
inference(sat_conversion,[],[f1870]) ).
cnf(s275,plain,
( ~ spl0_11
| spl0_28 ),
inference(sat_conversion,[],[f1880]) ).
cnf(s276,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_11 ),
inference(sat_conversion,[],[f1887]) ).
cnf(s278,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_13 ),
inference(sat_conversion,[],[f1894]) ).
cnf(s279,plain,
( ~ spl0_15
| ~ spl0_50 ),
inference(sat_conversion,[],[f1902]) ).
cnf(s282,plain,
( ~ spl0_1
| ~ spl0_21 ),
inference(sat_conversion,[],[f1913]) ).
cnf(s283,plain,
( ~ spl0_1
| ~ spl0_22 ),
inference(sat_conversion,[],[f1920]) ).
cnf(s284,plain,
( ~ spl0_1
| ~ spl0_23 ),
inference(sat_conversion,[],[f1926]) ).
cnf(s294,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_11 ),
inference(sat_conversion,[],[f1958]) ).
cnf(s303,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(sat_conversion,[],[f2005]) ).
cnf(s308,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(sat_conversion,[],[f2027]) ).
cnf(s311,plain,
( spl0_23
| ~ spl0_40 ),
inference(sat_conversion,[],[f2031]) ).
cnf(s312,plain,
( ~ spl0_2
| ~ spl0_21 ),
inference(sat_conversion,[],[f2047]) ).
cnf(s315,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_14 ),
inference(sat_conversion,[],[f2054]) ).
cnf(s320,plain,
( ~ spl0_2
| ~ spl0_23 ),
inference(sat_conversion,[],[f2068]) ).
cnf(s324,plain,
( ~ spl0_2
| ~ spl0_24 ),
inference(sat_conversion,[],[f2082]) ).
cnf(s329,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_22 ),
inference(sat_conversion,[],[f2107]) ).
cnf(s333,plain,
( spl0_21
| ~ spl0_30 ),
inference(sat_conversion,[],[f2148]) ).
cnf(s334,plain,
( spl0_16
| ~ spl0_29 ),
inference(sat_conversion,[],[f2155]) ).
cnf(s343,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_20 ),
inference(sat_conversion,[],[f2194]) ).
cnf(s347,plain,
( ~ spl0_11
| ~ spl0_13 ),
inference(sat_conversion,[],[f2214]) ).
cnf(s349,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_20 ),
inference(sat_conversion,[],[f2220]) ).
cnf(s356,plain,
( ~ spl0_6
| ~ spl0_28 ),
inference(sat_conversion,[],[f2236]) ).
cnf(s360,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(sat_conversion,[],[f2259]) ).
cnf(s362,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_13 ),
inference(sat_conversion,[],[f2263]) ).
cnf(s364,plain,
( ~ spl0_19
| ~ spl0_45 ),
inference(sat_conversion,[],[f2276]) ).
cnf(s366,plain,
( ~ spl0_19
| spl0_44 ),
inference(sat_conversion,[],[f2282]) ).
cnf(s367,plain,
( ~ spl0_3
| ~ spl0_22 ),
inference(sat_conversion,[],[f2290]) ).
cnf(s369,plain,
( ~ spl0_3
| ~ spl0_21 ),
inference(sat_conversion,[],[f2301]) ).
cnf(s371,plain,
( ~ spl0_3
| ~ spl0_19
| ~ spl0_23 ),
inference(sat_conversion,[],[f2311]) ).
cnf(s382,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_11 ),
inference(sat_conversion,[],[f2343]) ).
cnf(s389,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(sat_conversion,[],[f2367]) ).
cnf(s393,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_11 ),
inference(sat_conversion,[],[f2385]) ).
cnf(s397,plain,
( ~ spl0_6
| ~ spl0_9 ),
inference(sat_conversion,[],[f2401]) ).
cnf(s416,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_11 ),
inference(sat_conversion,[],[f2442]) ).
cnf(s419,plain,
( ~ spl0_3
| ~ spl0_11
| ~ spl0_23 ),
inference(sat_conversion,[],[f2463]) ).
cnf(s434,plain,
( ~ spl0_1
| ~ spl0_17 ),
inference(sat_conversion,[],[f2504]) ).
cnf(s435,plain,
~ spl0_5,
inference(rat,[],[s2,s147,s202,s343,s349,s4,s91,s57,s158,s187,s195,s199]) ).
cnf(s437,plain,
( ~ spl0_4
| spl0_26 ),
inference(rat,[],[s333,s90,s6,s3,s48,s109,s115,s118,s120,s77,s2,s122,s97,s107,s112,s160,s4,s334,s53,s92,s93,s95]) ).
cnf(s438,plain,
( spl0_6
| ~ spl0_3
| spl0_26 ),
inference(rat,[],[s125,s132,s5,s4,s203,s366,s67,s242,s248,s2,s416,s294,s419,s48,s6,s77,s367,s333,s369,s334,s246,s222,s150,s194,s59]) ).
cnf(s439,plain,
( ~ spl0_3
| spl0_26 ),
inference(rat,[],[s125,s279,s5,s3,s203,s271,s364,s366,s371,s275,s4,s72,s241,s356,s360,s362,s438,s222,s150,s246,s367,s369]) ).
cnf(s440,plain,
( ~ spl0_11
| spl0_1 ),
inference(rat,[],[s235,s22,s8,s9,s13,s18,s19,s228,s382,s393,s21,s347,s17,s12,s41,s324,s311,s320,s1,s439,s437,s224,s435]) ).
cnf(s441,plain,
( spl0_6
| spl0_1 ),
inference(rat,[],[s5,s329,s125,s19,s260,s9,s2,s18,s22,s182,s308,s389,s24,s334,s6,s77,s17,s320,s41,s324,s333,s312,s1,s439,s437,s224,s48,s440,s435]) ).
cnf(s442,plain,
spl0_1,
inference(rat,[],[s9,s22,s19,s18,s303,s315,s397,s441,s41,s324,s1,s439,s17,s437,s224,s435]) ).
cnf(s443,plain,
~ spl0_17,
inference(rat,[],[s434,s442]) ).
cnf(s444,plain,
~ spl0_23,
inference(rat,[],[s284,s442]) ).
cnf(s445,plain,
~ spl0_22,
inference(rat,[],[s283,s442]) ).
cnf(s446,plain,
~ spl0_21,
inference(rat,[],[s282,s442]) ).
cnf(s447,plain,
~ spl0_24,
inference(rat,[],[s217,s442]) ).
cnf(s448,plain,
~ spl0_27,
inference(rat,[],[s205,s442]) ).
cnf(s449,plain,
~ spl0_16,
inference(rat,[],[s164,s442]) ).
cnf(s454,plain,
spl0_25,
inference(rat,[],[s5,s446,s444,s447,s445]) ).
cnf(s456,plain,
~ spl0_6,
inference(rat,[],[s198,s448]) ).
cnf(s460,plain,
spl0_50,
inference(rat,[],[s125,s454]) ).
cnf(s464,plain,
~ spl0_15,
inference(rat,[],[s279,s460]) ).
cnf(s466,plain,
~ spl0_10,
inference(rat,[],[s260,s460]) ).
cnf(s467,plain,
~ spl0_20,
inference(rat,[],[s132,s460]) ).
cnf(s469,plain,
~ spl0_44,
inference(rat,[],[s3,s210,s276,s278,s2,s268,s242,s271,s464,s442,s456,s466]) ).
cnf(s470,plain,
~ spl0_19,
inference(rat,[],[s366,s469]) ).
cnf(s471,plain,
spl0_18,
inference(rat,[],[s4,s467,s449,s443,s470]) ).
cnf(s472,plain,
spl0_39,
inference(rat,[],[s222,s471]) ).
cnf(s473,plain,
~ spl0_7,
inference(rat,[],[s263,s442,s471]) ).
cnf(s474,plain,
~ spl0_9,
inference(rat,[],[s254,s442,s471]) ).
cnf(s476,plain,
~ spl0_8,
inference(rat,[],[s192,s472]) ).
cnf(s480,plain,
$false,
inference(rat,[],[s2,s474,s466,s456,s476,s473]) ).
fof(f2505,plain,
$false,
inference(avatar_sat_refutation,[],[s480]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG079+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.19 % Computer : n019.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Mon Sep 28 19:25:19 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 Running first-order theorem proving
% 0.10/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.96/1.08 % (141433)Detected formulas, will run a generic FOF schedule.
% 2.96/1.08 % (141442)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2008765748:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.96/1.08 % (141442)Instruction limit reached!
% 2.96/1.08 % (141442)------------------------------
% 2.96/1.08 % (141442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.96/1.08 % (141442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.96/1.08 % (141442)CaDiCaL version: 2.1.3
% 2.96/1.08 % (141442)Termination reason: Instruction limit
% 2.96/1.08 % (141442)Termination phase: Saturation
% 2.96/1.08 % (141442)Time elapsed: 0.027 s
% 2.96/1.08 % (141442)Peak memory usage: 87 MB
% 2.96/1.08 % (141442)Instructions burned: 122 (million)
% 2.96/1.08 % (141438)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=631476098:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.96/1.08 % (141440)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=88279206:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.96/1.08 % (141443)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4130099821:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.96/1.08 % (141441)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=127998155:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.96/1.08 % (141439)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=2940895010:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.96/1.08 % (141444)dis-21_1_sil=8000:lcm=predicate:random_seed=1765547767: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)
% 2.96/1.08 % (141444)Refutation not found, incomplete strategy
% 2.96/1.08 % (141444)------------------------------
% 2.96/1.08 % (141444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.96/1.08 % (141444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.96/1.08 % (141444)CaDiCaL version: 2.1.3
% 2.96/1.08 % (141444)Termination reason: Refutation not found, incomplete strategy
% 2.96/1.08 % (141444)Time elapsed: 0.005 s
% 2.96/1.08 % (141444)Peak memory usage: 88 MB
% 2.96/1.08 % (141444)Instructions burned: 8 (million)
% 2.96/1.08 % (141441)Instruction limit reached!
% 2.96/1.08 % (141441)------------------------------
% 2.96/1.08 % (141441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.96/1.08 % (141441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.96/1.08 % (141441)CaDiCaL version: 2.1.3
% 2.96/1.08 % (141441)Termination reason: Instruction limit
% 2.96/1.08 % (141441)Termination phase: Saturation
% 2.96/1.08 % (141441)Time elapsed: 0.059 s
% 2.96/1.08 % (141441)Peak memory usage: 89 MB
% 2.96/1.08 % (141441)Instructions burned: 111 (million)
% 2.96/1.08 % (141446)lrs+10_1_sil=8000:sp=occurrence:random_seed=1669867949:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 2.96/1.08 % (141443)Instruction limit reached!
% 2.96/1.08 % (141443)------------------------------
% 2.96/1.08 % (141443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.96/1.08 % (141443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.96/1.08 % (141443)CaDiCaL version: 2.1.3
% 2.96/1.08 % (141443)Termination reason: Instruction limit
% 2.96/1.08 % (141443)Termination phase: Saturation
% 2.96/1.08 % (141443)Time elapsed: 0.075 s
% 2.96/1.08 % (141443)Peak memory usage: 89 MB
% 2.96/1.08 % (141443)Instructions burned: 139 (million)
% 2.96/1.08 % (141446)First to succeed.
% 2.96/1.08 % (141446)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-141433"
% 2.96/1.08 % (141453)lrs+10_1_sil=32000:urr=on:br=off:random_seed=236210782:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 2.96/1.08 % (141455)lrs+1011_1_sil=32000:sp=occurrence:random_seed=532637070:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 2.96/1.08 % (141453)Also succeeded, but the first one will report.
% 2.96/1.08 % (141455)Also succeeded, but the first one will report.
% 2.96/1.08 % (141446)Refutation found. Thanks to Tanya!
% 2.96/1.08 % SZS status Theorem for theBenchmark
% 2.96/1.08 % SZS output start Proof for theBenchmark
% See solution above
% 3.47/1.27 % (141446)------------------------------
% 3.47/1.27 % (141446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.47/1.27 % (141446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/1.27 % (141446)CaDiCaL version: 2.1.3
% 3.47/1.27 % (141446)Termination reason: Refutation
% 3.47/1.27 % (141446)Time elapsed: 0.024 s
% 3.47/1.27 % (141446)Peak memory usage: 90 MB
% 3.47/1.27 % (141446)Instructions burned: 80 (million)
% 3.47/1.27 % (141446)------------------------------
% 3.47/1.27 % (141446)------------------------------
% 3.47/1.27 % (141433)Success in time 0.405 s
% 3.47/1.27 % Vampire exiting
%------------------------------------------------------------------------------