%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG185+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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:28:50 AM UTC 2026
% Result : Theorem 1.00s 0.41s
% Output : Refutation 1.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 30
% Syntax : Number of formulae : 674 ( 65 unt; 25 def)
% Number of atoms : 2222 ( 930 equ)
% Maximal formula atoms : 110 ( 3 avg)
% Number of connectives : 2626 (1078 ~;1181 |; 340 &)
% ( 25 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 70 ( 4 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 27 ( 25 usr; 26 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e10 != e14
& e11 != e12
& e11 != e13
& e11 != e14
& e12 != e13
& e12 != e14
& e13 != e14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e20 != e24
& e21 != e22
& e21 != e23
& e21 != e24
& e22 != e23
& e22 != e24
& e23 != e24 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f4,axiom,
( op1(e10,e10) = e10
& op1(e10,e11) = e13
& op1(e10,e12) = e14
& op1(e10,e13) = e11
& op1(e10,e14) = e12
& op1(e11,e10) = e14
& op1(e11,e11) = e11
& op1(e11,e12) = e13
& op1(e11,e13) = e12
& op1(e11,e14) = e10
& op1(e12,e10) = e11
& op1(e12,e11) = e10
& op1(e12,e12) = e12
& op1(e12,e13) = e14
& op1(e12,e14) = e13
& op1(e13,e10) = e12
& op1(e13,e11) = e14
& op1(e13,e12) = e10
& op1(e13,e13) = e13
& op1(e13,e14) = e11
& op1(e14,e10) = e13
& op1(e14,e11) = e12
& op1(e14,e12) = e11
& op1(e14,e13) = e10
& op1(e14,e14) = e14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op2(e20,e20) = e20
& op2(e20,e21) = e23
& op2(e20,e22) = e24
& op2(e20,e23) = e22
& op2(e20,e24) = e21
& op2(e21,e20) = e22
& op2(e21,e21) = e21
& op2(e21,e22) = e23
& op2(e21,e23) = e24
& op2(e21,e24) = e20
& op2(e22,e20) = e21
& op2(e22,e21) = e24
& op2(e22,e22) = e22
& op2(e22,e23) = e20
& op2(e22,e24) = e23
& op2(e23,e20) = e24
& op2(e23,e21) = e20
& op2(e23,e22) = e21
& op2(e23,e23) = e23
& op2(e23,e24) = e22
& op2(e24,e20) = e23
& op2(e24,e21) = e22
& op2(e24,e22) = e20
& op2(e24,e23) = e21
& op2(e24,e24) = e24 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,conjecture,
( ( ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14 ) )
=> ~ ( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f7,negated_conjecture,
~ ( ( ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14 ) )
=> ~ ( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14 ) ),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f8,plain,
( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14
& ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14 ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f9,plain,
( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14
& ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14 ) ),
inference(flattening,[],[f8]) ).
fof(f14,plain,
e11 != e13,
inference(cnf_transformation,[],[f1]) ).
fof(f19,plain,
e10 != e11,
inference(cnf_transformation,[],[f1]) ).
fof(f20,plain,
e23 != e24,
inference(cnf_transformation,[],[f2]) ).
fof(f21,plain,
e22 != e24,
inference(cnf_transformation,[],[f2]) ).
fof(f22,plain,
e22 != e23,
inference(cnf_transformation,[],[f2]) ).
fof(f23,plain,
e21 != e24,
inference(cnf_transformation,[],[f2]) ).
fof(f24,plain,
e21 != e23,
inference(cnf_transformation,[],[f2]) ).
fof(f25,plain,
e21 != e22,
inference(cnf_transformation,[],[f2]) ).
fof(f26,plain,
e20 != e24,
inference(cnf_transformation,[],[f2]) ).
fof(f27,plain,
e20 != e23,
inference(cnf_transformation,[],[f2]) ).
fof(f28,plain,
e20 != e22,
inference(cnf_transformation,[],[f2]) ).
fof(f29,plain,
e20 != e21,
inference(cnf_transformation,[],[f2]) ).
fof(f55,plain,
e14 = op1(e14,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f56,plain,
e10 = op1(e14,e13),
inference(cnf_transformation,[],[f4]) ).
fof(f57,plain,
e11 = op1(e14,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f58,plain,
e12 = op1(e14,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f59,plain,
e13 = op1(e14,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f60,plain,
e11 = op1(e13,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f62,plain,
e10 = op1(e13,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f63,plain,
e14 = op1(e13,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f64,plain,
e12 = op1(e13,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f65,plain,
e13 = op1(e12,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f66,plain,
e14 = op1(e12,e13),
inference(cnf_transformation,[],[f4]) ).
fof(f67,plain,
e12 = op1(e12,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f68,plain,
e10 = op1(e12,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f69,plain,
e11 = op1(e12,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f70,plain,
e10 = op1(e11,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f71,plain,
e12 = op1(e11,e13),
inference(cnf_transformation,[],[f4]) ).
fof(f72,plain,
e13 = op1(e11,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f73,plain,
e11 = op1(e11,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f74,plain,
e14 = op1(e11,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f75,plain,
e12 = op1(e10,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f76,plain,
e11 = op1(e10,e13),
inference(cnf_transformation,[],[f4]) ).
fof(f77,plain,
e14 = op1(e10,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f78,plain,
e13 = op1(e10,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f81,plain,
e21 = op2(e24,e23),
inference(cnf_transformation,[],[f5]) ).
fof(f83,plain,
e22 = op2(e24,e21),
inference(cnf_transformation,[],[f5]) ).
fof(f105,plain,
( e10 = j(e24)
| e11 = j(e24)
| e12 = j(e24)
| e13 = j(e24)
| e14 = j(e24) ),
inference(cnf_transformation,[],[f9]) ).
fof(f106,plain,
( e10 = j(e23)
| e11 = j(e23)
| e12 = j(e23)
| e13 = j(e23)
| e14 = j(e23) ),
inference(cnf_transformation,[],[f9]) ).
fof(f108,plain,
( e10 = j(e21)
| e11 = j(e21)
| e12 = j(e21)
| e13 = j(e21)
| e14 = j(e21) ),
inference(cnf_transformation,[],[f9]) ).
fof(f109,plain,
( e10 = j(e20)
| e11 = j(e20)
| e12 = j(e20)
| e13 = j(e20)
| e14 = j(e20) ),
inference(cnf_transformation,[],[f9]) ).
fof(f120,plain,
e24 = h(j(e24)),
inference(cnf_transformation,[],[f9]) ).
fof(f121,plain,
e23 = h(j(e23)),
inference(cnf_transformation,[],[f9]) ).
fof(f122,plain,
e22 = h(j(e22)),
inference(cnf_transformation,[],[f9]) ).
fof(f123,plain,
e21 = h(j(e21)),
inference(cnf_transformation,[],[f9]) ).
fof(f124,plain,
e20 = h(j(e20)),
inference(cnf_transformation,[],[f9]) ).
fof(f126,plain,
j(op2(e24,e23)) = op1(j(e24),j(e23)),
inference(cnf_transformation,[],[f9]) ).
fof(f128,plain,
j(op2(e24,e21)) = op1(j(e24),j(e21)),
inference(cnf_transformation,[],[f9]) ).
fof(f154,plain,
h(op1(e14,e10)) = op2(h(e14),h(e10)),
inference(cnf_transformation,[],[f9]) ).
fof(f155,plain,
h(op1(e13,e14)) = op2(h(e13),h(e14)),
inference(cnf_transformation,[],[f9]) ).
fof(f159,plain,
h(op1(e13,e10)) = op2(h(e13),h(e10)),
inference(cnf_transformation,[],[f9]) ).
fof(f160,plain,
h(op1(e12,e14)) = op2(h(e12),h(e14)),
inference(cnf_transformation,[],[f9]) ).
fof(f161,plain,
h(op1(e12,e13)) = op2(h(e12),h(e13)),
inference(cnf_transformation,[],[f9]) ).
fof(f163,plain,
h(op1(e12,e11)) = op2(h(e12),h(e11)),
inference(cnf_transformation,[],[f9]) ).
fof(f167,plain,
h(op1(e11,e12)) = op2(h(e11),h(e12)),
inference(cnf_transformation,[],[f9]) ).
fof(f170,plain,
h(op1(e10,e14)) = op2(h(e10),h(e14)),
inference(cnf_transformation,[],[f9]) ).
fof(f176,definition,
( spl0_1
<=> e14 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f178,plain,
( e14 = j(e24)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f180,definition,
( spl0_2
<=> e13 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f182,plain,
( e13 = j(e24)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f184,definition,
( spl0_3
<=> e12 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f186,plain,
( e12 = j(e24)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f188,definition,
( spl0_4
<=> e11 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f190,plain,
( e11 = j(e24)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f192,definition,
( spl0_5
<=> e10 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f194,plain,
( e10 = j(e24)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f195,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5 ),
inference(avatar_split_clause,[],[f105,f192,f188,f184,f180,f176]) ).
fof(f196,plain,
( e24 = h(e14)
| ~ spl0_1 ),
inference(superposition,[],[f120,f178]) ).
fof(f217,definition,
( spl0_6
<=> e14 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f219,plain,
( e14 = j(e23)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f217]) ).
fof(f221,definition,
( spl0_7
<=> e13 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f223,plain,
( e13 = j(e23)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f225,definition,
( spl0_8
<=> e12 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f227,plain,
( e12 = j(e23)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f229,definition,
( spl0_9
<=> e11 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f231,plain,
( e11 = j(e23)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f233,definition,
( spl0_10
<=> e10 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f235,plain,
( e10 = j(e23)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f236,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10 ),
inference(avatar_split_clause,[],[f106,f233,f229,f225,f221,f217]) ).
fof(f237,plain,
( e23 = h(e14)
| ~ spl0_6 ),
inference(superposition,[],[f121,f219]) ).
fof(f250,plain,
( e23 = e24
| ~ spl0_1
| ~ spl0_6 ),
inference(superposition,[],[f237,f196]) ).
fof(f264,plain,
( $false
| ~ spl0_1
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f250,f20]) ).
fof(f265,plain,
( ~ spl0_1
| ~ spl0_6 ),
inference(avatar_contradiction_clause,[],[f264]) ).
fof(f266,plain,
( e24 = h(e10)
| ~ spl0_5 ),
inference(superposition,[],[f120,f194]) ).
fof(f296,definition,
( spl0_11
<=> e14 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f297,plain,
( e14 != j(e22)
| spl0_11 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f298,plain,
( e14 = j(e22)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f300,definition,
( spl0_12
<=> e13 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f301,plain,
( e13 != j(e22)
| spl0_12 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f302,plain,
( e13 = j(e22)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f304,definition,
( spl0_13
<=> e12 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f305,plain,
( e12 != j(e22)
| spl0_13 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f306,plain,
( e12 = j(e22)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f308,definition,
( spl0_14
<=> e11 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f309,plain,
( e11 != j(e22)
| spl0_14 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f310,plain,
( e11 = j(e22)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f312,definition,
( spl0_15
<=> e10 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f313,plain,
( e10 != j(e22)
| spl0_15 ),
inference(avatar_component_clause,[],[f312]) ).
fof(f314,plain,
( e10 = j(e22)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f312]) ).
fof(f316,plain,
( e22 = h(e14)
| ~ spl0_11 ),
inference(superposition,[],[f122,f298]) ).
fof(f334,plain,
( e22 = e23
| ~ spl0_6
| ~ spl0_11 ),
inference(superposition,[],[f316,f237]) ).
fof(f350,plain,
( $false
| ~ spl0_6
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f334,f22]) ).
fof(f351,plain,
( ~ spl0_6
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f350]) ).
fof(f354,plain,
( e23 = h(e10)
| ~ spl0_10 ),
inference(superposition,[],[f121,f235]) ).
fof(f369,plain,
( e23 = e24
| ~ spl0_5
| ~ spl0_10 ),
inference(superposition,[],[f354,f266]) ).
fof(f385,plain,
( $false
| ~ spl0_5
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f369,f20]) ).
fof(f386,plain,
( ~ spl0_5
| ~ spl0_10 ),
inference(avatar_contradiction_clause,[],[f385]) ).
fof(f387,plain,
( e23 = h(e12)
| ~ spl0_8 ),
inference(superposition,[],[f121,f227]) ).
fof(f426,definition,
( spl0_16
<=> e14 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f427,plain,
( e14 != j(e21)
| spl0_16 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f428,plain,
( e14 = j(e21)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f430,definition,
( spl0_17
<=> e13 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f431,plain,
( e13 != j(e21)
| spl0_17 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f432,plain,
( e13 = j(e21)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f434,definition,
( spl0_18
<=> e12 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f435,plain,
( e12 != j(e21)
| spl0_18 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f436,plain,
( e12 = j(e21)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f438,definition,
( spl0_19
<=> e11 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f439,plain,
( e11 != j(e21)
| spl0_19 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f440,plain,
( e11 = j(e21)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f442,definition,
( spl0_20
<=> e10 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f443,plain,
( e10 != j(e21)
| spl0_20 ),
inference(avatar_component_clause,[],[f442]) ).
fof(f444,plain,
( e10 = j(e21)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f442]) ).
fof(f445,plain,
( spl0_16
| spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(avatar_split_clause,[],[f108,f442,f438,f434,f430,f426]) ).
fof(f446,plain,
( e21 = h(e14)
| ~ spl0_16 ),
inference(superposition,[],[f123,f428]) ).
fof(f468,plain,
( e21 = e22
| ~ spl0_11
| ~ spl0_16 ),
inference(superposition,[],[f446,f316]) ).
fof(f486,plain,
( $false
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f468,f25]) ).
fof(f487,plain,
( ~ spl0_11
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f486]) ).
fof(f531,plain,
( e22 = h(e12)
| ~ spl0_13 ),
inference(superposition,[],[f122,f306]) ).
fof(f551,plain,
( e22 = e23
| ~ spl0_8
| ~ spl0_13 ),
inference(superposition,[],[f531,f387]) ).
fof(f571,plain,
( $false
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f551,f22]) ).
fof(f572,plain,
( ~ spl0_8
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f571]) ).
fof(f573,plain,
( e22 = h(e11)
| ~ spl0_14 ),
inference(superposition,[],[f122,f310]) ).
fof(f615,definition,
( spl0_21
<=> e14 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f617,plain,
( e14 = j(e20)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f619,definition,
( spl0_22
<=> e13 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f621,plain,
( e13 = j(e20)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f623,definition,
( spl0_23
<=> e12 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f625,plain,
( e12 = j(e20)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f623]) ).
fof(f627,definition,
( spl0_24
<=> e11 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f629,plain,
( e11 = j(e20)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f631,definition,
( spl0_25
<=> e10 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f633,plain,
( e10 = j(e20)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f631]) ).
fof(f634,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_25 ),
inference(avatar_split_clause,[],[f109,f631,f627,f623,f619,f615]) ).
fof(f635,plain,
( e20 = h(e14)
| ~ spl0_21 ),
inference(superposition,[],[f124,f617]) ).
fof(f657,plain,
( e20 = e21
| ~ spl0_16
| ~ spl0_21 ),
inference(superposition,[],[f635,f446]) ).
fof(f677,plain,
( $false
| ~ spl0_16
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f657,f29]) ).
fof(f678,plain,
( ~ spl0_16
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f677]) ).
fof(f685,plain,
( e21 = h(e10)
| ~ spl0_20 ),
inference(superposition,[],[f123,f444]) ).
fof(f736,plain,
( e24 = h(e12)
| ~ spl0_3 ),
inference(superposition,[],[f120,f186]) ).
fof(f756,plain,
( e23 = e24
| ~ spl0_3
| ~ spl0_8 ),
inference(forward_demodulation,[],[f736,f387]) ).
fof(f757,plain,
( $false
| ~ spl0_3
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f756,f20]) ).
fof(f758,plain,
( ~ spl0_3
| ~ spl0_8 ),
inference(avatar_contradiction_clause,[],[f757]) ).
fof(f971,plain,
( e23 = h(e11)
| ~ spl0_9 ),
inference(superposition,[],[f121,f231]) ).
fof(f994,plain,
( e22 = e23
| ~ spl0_9
| ~ spl0_14 ),
inference(forward_demodulation,[],[f971,f573]) ).
fof(f1003,plain,
( $false
| ~ spl0_9
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f994,f22]) ).
fof(f1004,plain,
( ~ spl0_9
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1003]) ).
fof(f1005,plain,
( e23 = h(e10)
| ~ spl0_10 ),
inference(superposition,[],[f121,f235]) ).
fof(f1028,plain,
( e21 = e23
| ~ spl0_10
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1005,f685]) ).
fof(f1037,plain,
( $false
| ~ spl0_10
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1028,f24]) ).
fof(f1038,plain,
( ~ spl0_10
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f1037]) ).
fof(f1049,plain,
( e21 = h(e13)
| ~ spl0_17 ),
inference(superposition,[],[f123,f432]) ).
fof(f1300,plain,
( e24 = h(e13)
| ~ spl0_2 ),
inference(superposition,[],[f120,f182]) ).
fof(f1319,plain,
( e21 = e24
| ~ spl0_2
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1300,f1049]) ).
fof(f1325,plain,
( $false
| ~ spl0_2
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1319,f23]) ).
fof(f1326,plain,
( ~ spl0_2
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1325]) ).
fof(f1380,plain,
( e23 = h(e12)
| ~ spl0_8 ),
inference(superposition,[],[f121,f227]) ).
fof(f1381,plain,
( j(op2(e24,e23)) = op1(j(e24),e12)
| ~ spl0_8 ),
inference(superposition,[],[f126,f227]) ).
fof(f1535,plain,
( j(e21) = op1(j(e24),e12)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f1381,f81]) ).
fof(f1711,plain,
( e20 = h(e11)
| ~ spl0_24 ),
inference(superposition,[],[f124,f629]) ).
fof(f1752,plain,
( e20 = e22
| ~ spl0_14
| ~ spl0_24 ),
inference(superposition,[],[f573,f1711]) ).
fof(f1753,plain,
( $false
| ~ spl0_14
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f1752,f28]) ).
fof(f1754,plain,
( ~ spl0_14
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f1753]) ).
fof(f1852,plain,
( e24 = h(e13)
| ~ spl0_2 ),
inference(superposition,[],[f120,f182]) ).
fof(f1854,plain,
( j(op2(e24,e23)) = op1(e13,j(e23))
| ~ spl0_2 ),
inference(superposition,[],[f126,f182]) ).
fof(f1869,plain,
( op1(e13,e12) = j(op2(e24,e23))
| ~ spl0_2
| ~ spl0_8 ),
inference(forward_demodulation,[],[f1854,f227]) ).
fof(f1874,plain,
( op1(e13,e12) = j(e21)
| ~ spl0_2
| ~ spl0_8 ),
inference(forward_demodulation,[],[f1869,f81]) ).
fof(f1875,plain,
( e10 = j(e21)
| ~ spl0_2
| ~ spl0_8 ),
inference(forward_demodulation,[],[f1874,f62]) ).
fof(f1876,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1875,f443]) ).
fof(f1877,plain,
( ~ spl0_2
| ~ spl0_8
| spl0_20 ),
inference(avatar_contradiction_clause,[],[f1876]) ).
fof(f1904,plain,
( e21 = h(e10)
| ~ spl0_20 ),
inference(superposition,[],[f123,f444]) ).
fof(f1935,plain,
( e20 = h(e10)
| ~ spl0_25 ),
inference(superposition,[],[f124,f633]) ).
fof(f1997,plain,
( h(op1(e13,e10)) = op2(h(e13),e21)
| ~ spl0_20 ),
inference(superposition,[],[f159,f1904]) ).
fof(f2012,plain,
( op2(e24,e21) = h(op1(e13,e10))
| ~ spl0_2
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1997,f1852]) ).
fof(f2021,plain,
( op2(e24,e21) = h(e12)
| ~ spl0_2
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2012,f64]) ).
fof(f2026,plain,
( e23 = op2(e24,e21)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2021,f1380]) ).
fof(f2027,plain,
( e20 = e21
| ~ spl0_20
| ~ spl0_25 ),
inference(superposition,[],[f1935,f1904]) ).
fof(f2050,plain,
( $false
| ~ spl0_20
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f2027,f29]) ).
fof(f2051,plain,
( ~ spl0_20
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f2050]) ).
fof(f2065,plain,
( e20 = h(e14)
| ~ spl0_21 ),
inference(superposition,[],[f124,f617]) ).
fof(f2245,plain,
( e22 = e23
| ~ spl0_2
| ~ spl0_8
| ~ spl0_20 ),
inference(superposition,[],[f83,f2026]) ).
fof(f2249,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2245,f22]) ).
fof(f2250,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2249]) ).
fof(f2269,plain,
( e24 = h(e14)
| ~ spl0_1 ),
inference(superposition,[],[f120,f178]) ).
fof(f2292,plain,
( e20 = e24
| ~ spl0_1
| ~ spl0_21 ),
inference(forward_demodulation,[],[f2269,f2065]) ).
fof(f2301,plain,
( $false
| ~ spl0_1
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f2292,f26]) ).
fof(f2302,plain,
( ~ spl0_1
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f2301]) ).
fof(f2385,plain,
( j(op2(e24,e21)) = op1(e11,j(e21))
| ~ spl0_4 ),
inference(superposition,[],[f128,f190]) ).
fof(f2398,plain,
( op1(e11,e10) = j(op2(e24,e21))
| ~ spl0_4
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2385,f444]) ).
fof(f2405,plain,
( op1(e11,e10) = j(e22)
| ~ spl0_4
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2398,f83]) ).
fof(f2407,plain,
( e14 = j(e22)
| ~ spl0_4
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2405,f74]) ).
fof(f2409,plain,
( $false
| ~ spl0_4
| spl0_11
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2407,f297]) ).
fof(f2410,plain,
( ~ spl0_4
| spl0_11
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2409]) ).
fof(f2582,plain,
( op1(e11,e12) = j(e21)
| ~ spl0_4
| ~ spl0_8 ),
inference(forward_demodulation,[],[f1535,f190]) ).
fof(f2586,plain,
( j(e22) = op1(e11,j(e21))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f2385,f83]) ).
fof(f2596,plain,
( e13 = j(e21)
| ~ spl0_4
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2582,f72]) ).
fof(f2606,plain,
( $false
| ~ spl0_4
| ~ spl0_8
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f2596,f431]) ).
fof(f2607,plain,
( ~ spl0_4
| ~ spl0_8
| spl0_17 ),
inference(avatar_contradiction_clause,[],[f2606]) ).
fof(f2647,plain,
( op1(e11,e13) = j(e22)
| ~ spl0_4
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2586,f432]) ).
fof(f2649,plain,
( e12 = j(e22)
| ~ spl0_4
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2647,f71]) ).
fof(f2652,plain,
( $false
| ~ spl0_4
| spl0_13
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2649,f305]) ).
fof(f2653,plain,
( ~ spl0_4
| spl0_13
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2652]) ).
fof(f2660,plain,
( j(op2(e24,e21)) = op1(e10,j(e21))
| ~ spl0_5 ),
inference(superposition,[],[f128,f194]) ).
fof(f2672,plain,
( op1(e10,e13) = j(op2(e24,e21))
| ~ spl0_5
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2660,f432]) ).
fof(f2677,plain,
( op1(e10,e13) = j(e22)
| ~ spl0_5
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2672,f83]) ).
fof(f2679,plain,
( e11 = j(e22)
| ~ spl0_5
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2677,f76]) ).
fof(f2681,plain,
( $false
| ~ spl0_5
| spl0_14
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2679,f309]) ).
fof(f2682,plain,
( ~ spl0_5
| spl0_14
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2681]) ).
fof(f2685,plain,
( j(op2(e24,e23)) = op1(e14,j(e23))
| ~ spl0_1 ),
inference(superposition,[],[f126,f178]) ).
fof(f2698,plain,
( op1(e14,e12) = j(op2(e24,e23))
| ~ spl0_1
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2685,f227]) ).
fof(f2701,plain,
( op1(e14,e12) = j(e21)
| ~ spl0_1
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2698,f81]) ).
fof(f2702,plain,
( e11 = j(e21)
| ~ spl0_1
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2701,f57]) ).
fof(f2703,plain,
( $false
| ~ spl0_1
| ~ spl0_8
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f2702,f439]) ).
fof(f2704,plain,
( ~ spl0_1
| ~ spl0_8
| spl0_19 ),
inference(avatar_contradiction_clause,[],[f2703]) ).
fof(f2758,plain,
( e21 = h(e11)
| ~ spl0_19 ),
inference(superposition,[],[f123,f440]) ).
fof(f2759,plain,
( j(op2(e24,e21)) = op1(j(e24),e11)
| ~ spl0_19 ),
inference(superposition,[],[f128,f440]) ).
fof(f2778,plain,
( op1(e14,e11) = j(op2(e24,e21))
| ~ spl0_1
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2759,f178]) ).
fof(f2784,plain,
( op1(e14,e11) = j(e22)
| ~ spl0_1
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2778,f83]) ).
fof(f2789,plain,
( e12 = j(e22)
| ~ spl0_1
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2784,f58]) ).
fof(f2790,plain,
( $false
| ~ spl0_1
| spl0_13
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2789,f305]) ).
fof(f2791,plain,
( ~ spl0_1
| spl0_13
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2790]) ).
fof(f2793,plain,
( e24 = h(e10)
| ~ spl0_5 ),
inference(superposition,[],[f120,f194]) ).
fof(f2795,plain,
( j(op2(e24,e23)) = op1(e10,j(e23))
| ~ spl0_5 ),
inference(superposition,[],[f126,f194]) ).
fof(f2797,plain,
( j(op2(e24,e21)) = op1(e10,j(e21))
| ~ spl0_5 ),
inference(superposition,[],[f128,f194]) ).
fof(f2808,plain,
( op1(e10,e11) = j(op2(e24,e21))
| ~ spl0_5
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2797,f440]) ).
fof(f2809,plain,
( op1(e10,e12) = j(op2(e24,e23))
| ~ spl0_5
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2795,f227]) ).
fof(f2813,plain,
( op1(e10,e11) = j(e22)
| ~ spl0_5
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2808,f83]) ).
fof(f2814,plain,
( op1(e10,e12) = j(e21)
| ~ spl0_5
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2809,f81]) ).
fof(f2815,plain,
( e13 = j(e22)
| ~ spl0_5
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2813,f78]) ).
fof(f2845,plain,
( e20 = h(e11)
| ~ spl0_24 ),
inference(superposition,[],[f124,f629]) ).
fof(f2962,plain,
( e20 = e21
| ~ spl0_19
| ~ spl0_24 ),
inference(superposition,[],[f2845,f2758]) ).
fof(f2985,plain,
( $false
| ~ spl0_19
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f2962,f29]) ).
fof(f2986,plain,
( ~ spl0_19
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f2985]) ).
fof(f3101,plain,
( $false
| ~ spl0_5
| spl0_12
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2815,f301]) ).
fof(f3102,plain,
( ~ spl0_5
| spl0_12
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f3101]) ).
fof(f3232,plain,
( j(e22) = op1(e10,j(e21))
| ~ spl0_5 ),
inference(forward_demodulation,[],[f2797,f83]) ).
fof(f3233,plain,
( e14 = j(e21)
| ~ spl0_5
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2814,f77]) ).
fof(f3332,plain,
( $false
| ~ spl0_5
| ~ spl0_8
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f3233,f427]) ).
fof(f3333,plain,
( ~ spl0_5
| ~ spl0_8
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f3332]) ).
fof(f3336,plain,
( op1(e10,e12) = j(e22)
| ~ spl0_5
| ~ spl0_18 ),
inference(forward_demodulation,[],[f3232,f436]) ).
fof(f3342,plain,
( e14 = j(e22)
| ~ spl0_5
| ~ spl0_18 ),
inference(forward_demodulation,[],[f3336,f77]) ).
fof(f3345,plain,
( $false
| ~ spl0_5
| spl0_11
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f3342,f297]) ).
fof(f3346,plain,
( ~ spl0_5
| spl0_11
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f3345]) ).
fof(f3370,plain,
( e21 = h(e14)
| ~ spl0_16 ),
inference(superposition,[],[f123,f428]) ).
fof(f3466,plain,
( h(op1(e10,e14)) = op2(h(e10),e21)
| ~ spl0_16 ),
inference(superposition,[],[f170,f3370]) ).
fof(f3467,plain,
( op2(e24,e21) = h(op1(e10,e14))
| ~ spl0_5
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3466,f2793]) ).
fof(f3476,plain,
( op2(e24,e21) = h(e12)
| ~ spl0_5
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3467,f75]) ).
fof(f3485,plain,
( e23 = op2(e24,e21)
| ~ spl0_5
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3476,f1380]) ).
fof(f3489,plain,
( e22 = e23
| ~ spl0_5
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3485,f83]) ).
fof(f3490,plain,
( $false
| ~ spl0_5
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f3489,f22]) ).
fof(f3491,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f3490]) ).
fof(f3492,plain,
( j(e21) = op1(e10,j(e23))
| ~ spl0_5 ),
inference(forward_demodulation,[],[f2795,f81]) ).
fof(f3508,plain,
( e23 = h(e14)
| ~ spl0_6 ),
inference(superposition,[],[f121,f219]) ).
fof(f3530,plain,
( e21 = e23
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3508,f3370]) ).
fof(f3539,plain,
( $false
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f3530,f24]) ).
fof(f3540,plain,
( ~ spl0_6
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f3539]) ).
fof(f3581,plain,
( op1(e10,e13) = j(e21)
| ~ spl0_5
| ~ spl0_7 ),
inference(forward_demodulation,[],[f3492,f223]) ).
fof(f3585,plain,
( e11 = j(e21)
| ~ spl0_5
| ~ spl0_7 ),
inference(forward_demodulation,[],[f3581,f76]) ).
fof(f3588,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f3585,f439]) ).
fof(f3589,plain,
( ~ spl0_5
| ~ spl0_7
| spl0_19 ),
inference(avatar_contradiction_clause,[],[f3588]) ).
fof(f3592,plain,
( j(op2(e24,e23)) = op1(j(e24),e14)
| ~ spl0_6 ),
inference(superposition,[],[f126,f219]) ).
fof(f3609,plain,
( op1(e10,e14) = j(op2(e24,e23))
| ~ spl0_5
| ~ spl0_6 ),
inference(forward_demodulation,[],[f3592,f194]) ).
fof(f3613,plain,
( op1(e10,e14) = j(e21)
| ~ spl0_5
| ~ spl0_6 ),
inference(forward_demodulation,[],[f3609,f81]) ).
fof(f3614,plain,
( e12 = j(e21)
| ~ spl0_5
| ~ spl0_6 ),
inference(forward_demodulation,[],[f3613,f75]) ).
fof(f3615,plain,
( $false
| ~ spl0_5
| ~ spl0_6
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f3614,f435]) ).
fof(f3616,plain,
( ~ spl0_5
| ~ spl0_6
| spl0_18 ),
inference(avatar_contradiction_clause,[],[f3615]) ).
fof(f3621,plain,
( j(op2(e24,e23)) = op1(j(e24),e11)
| ~ spl0_9 ),
inference(superposition,[],[f126,f231]) ).
fof(f3636,plain,
( op1(e10,e11) = j(op2(e24,e23))
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f3621,f194]) ).
fof(f3638,plain,
( op1(e10,e11) = j(e21)
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f3636,f81]) ).
fof(f3639,plain,
( e13 = j(e21)
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f3638,f78]) ).
fof(f3640,plain,
( $false
| ~ spl0_5
| ~ spl0_9
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f3639,f431]) ).
fof(f3641,plain,
( ~ spl0_5
| ~ spl0_9
| spl0_17 ),
inference(avatar_contradiction_clause,[],[f3640]) ).
fof(f3642,plain,
( e23 = h(e13)
| ~ spl0_7 ),
inference(superposition,[],[f121,f223]) ).
fof(f3662,plain,
( e22 = h(e13)
| ~ spl0_12 ),
inference(superposition,[],[f122,f302]) ).
fof(f3685,plain,
( e21 = h(e11)
| ~ spl0_19 ),
inference(superposition,[],[f123,f440]) ).
fof(f3713,plain,
( e20 = h(e12)
| ~ spl0_23 ),
inference(superposition,[],[f124,f625]) ).
fof(f3769,plain,
( e22 = e23
| ~ spl0_7
| ~ spl0_12 ),
inference(superposition,[],[f3662,f3642]) ).
fof(f3792,plain,
( $false
| ~ spl0_7
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f3769,f22]) ).
fof(f3793,plain,
( ~ spl0_7
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f3792]) ).
fof(f3804,plain,
( e24 = h(e12)
| ~ spl0_3 ),
inference(superposition,[],[f120,f186]) ).
fof(f3840,plain,
( e23 = h(e14)
| ~ spl0_6 ),
inference(superposition,[],[f121,f219]) ).
fof(f3943,plain,
( e20 = e24
| ~ spl0_3
| ~ spl0_23 ),
inference(forward_demodulation,[],[f3804,f3713]) ).
fof(f3944,plain,
( $false
| ~ spl0_3
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f3943,f26]) ).
fof(f3945,plain,
( ~ spl0_3
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f3944]) ).
fof(f3946,plain,
( e20 = h(e14)
| ~ spl0_21 ),
inference(superposition,[],[f124,f617]) ).
fof(f3983,plain,
( h(op1(e12,e11)) = op2(e24,h(e11))
| ~ spl0_3 ),
inference(superposition,[],[f163,f3804]) ).
fof(f3990,plain,
( op2(e24,e21) = h(op1(e12,e11))
| ~ spl0_3
| ~ spl0_19 ),
inference(forward_demodulation,[],[f3983,f3685]) ).
fof(f3998,plain,
( op2(e24,e21) = h(e10)
| ~ spl0_3
| ~ spl0_19 ),
inference(forward_demodulation,[],[f3990,f68]) ).
fof(f4001,plain,
( e22 = h(e10)
| ~ spl0_3
| ~ spl0_19 ),
inference(forward_demodulation,[],[f3998,f83]) ).
fof(f4009,plain,
( h(op1(e12,e14)) = op2(h(e12),e23)
| ~ spl0_6 ),
inference(superposition,[],[f160,f3840]) ).
fof(f4014,plain,
( op2(e24,e23) = h(op1(e12,e14))
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f4009,f3804]) ).
fof(f4023,plain,
( op2(e24,e23) = h(e13)
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f4014,f65]) ).
fof(f4028,plain,
( e21 = h(e13)
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f4023,f81]) ).
fof(f4063,plain,
( e20 = e23
| ~ spl0_6
| ~ spl0_21 ),
inference(superposition,[],[f3946,f3840]) ).
fof(f4086,plain,
( $false
| ~ spl0_6
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f4063,f27]) ).
fof(f4087,plain,
( ~ spl0_6
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f4086]) ).
fof(f4101,plain,
( e20 = h(e13)
| ~ spl0_22 ),
inference(superposition,[],[f124,f621]) ).
fof(f4168,plain,
( e20 = e21
| ~ spl0_3
| ~ spl0_6
| ~ spl0_22 ),
inference(forward_demodulation,[],[f4028,f4101]) ).
fof(f4169,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f4168,f29]) ).
fof(f4170,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f4169]) ).
fof(f4171,plain,
( e20 = h(e10)
| ~ spl0_25 ),
inference(superposition,[],[f124,f633]) ).
fof(f4240,plain,
( e20 = e22
| ~ spl0_3
| ~ spl0_19
| ~ spl0_25 ),
inference(forward_demodulation,[],[f4001,f4171]) ).
fof(f4242,plain,
( $false
| ~ spl0_3
| ~ spl0_19
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f4240,f28]) ).
fof(f4243,plain,
( ~ spl0_3
| ~ spl0_19
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f4242]) ).
fof(f4253,plain,
( j(op2(e24,e21)) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(superposition,[],[f128,f182]) ).
fof(f4265,plain,
( op1(e13,e11) = j(op2(e24,e21))
| ~ spl0_2
| ~ spl0_19 ),
inference(forward_demodulation,[],[f4253,f440]) ).
fof(f4270,plain,
( op1(e13,e11) = j(e22)
| ~ spl0_2
| ~ spl0_19 ),
inference(forward_demodulation,[],[f4265,f83]) ).
fof(f4272,plain,
( e14 = j(e22)
| ~ spl0_2
| ~ spl0_19 ),
inference(forward_demodulation,[],[f4270,f63]) ).
fof(f4274,plain,
( $false
| ~ spl0_2
| spl0_11
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f4272,f297]) ).
fof(f4275,plain,
( ~ spl0_2
| spl0_11
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f4274]) ).
fof(f4276,plain,
( e24 = h(e11)
| ~ spl0_4 ),
inference(superposition,[],[f120,f190]) ).
fof(f4295,plain,
( e21 = e24
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_demodulation,[],[f4276,f3685]) ).
fof(f4300,plain,
( $false
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f4295,f23]) ).
fof(f4301,plain,
( ~ spl0_4
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f4300]) ).
fof(f4309,plain,
( e24 = h(e13)
| ~ spl0_2 ),
inference(superposition,[],[f120,f182]) ).
fof(f4358,plain,
( e23 = h(e13)
| ~ spl0_7 ),
inference(superposition,[],[f121,f223]) ).
fof(f4441,plain,
( e20 = h(e13)
| ~ spl0_22 ),
inference(superposition,[],[f124,f621]) ).
fof(f4496,plain,
( e23 = e24
| ~ spl0_2
| ~ spl0_7 ),
inference(superposition,[],[f4358,f4309]) ).
fof(f4519,plain,
( $false
| ~ spl0_2
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f4496,f20]) ).
fof(f4520,plain,
( ~ spl0_2
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[],[f4519]) ).
fof(f4531,plain,
( j(op2(e24,e23)) = op1(e14,j(e23))
| ~ spl0_1 ),
inference(superposition,[],[f126,f178]) ).
fof(f4548,plain,
( op1(e14,e13) = j(op2(e24,e23))
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f4531,f223]) ).
fof(f4555,plain,
( op1(e14,e13) = j(e21)
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f4548,f81]) ).
fof(f4557,plain,
( e11 = op1(e14,e13)
| ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f4555,f440]) ).
fof(f4558,plain,
( e10 = e11
| ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f4557,f56]) ).
fof(f4559,plain,
( $false
| ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f4558,f19]) ).
fof(f4560,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f4559]) ).
fof(f4561,plain,
( e24 = h(e13)
| ~ spl0_2 ),
inference(superposition,[],[f120,f182]) ).
fof(f4587,plain,
( e23 = h(e10)
| ~ spl0_10 ),
inference(superposition,[],[f121,f235]) ).
fof(f4615,plain,
( e22 = h(e14)
| ~ spl0_11 ),
inference(superposition,[],[f122,f298]) ).
fof(f4670,plain,
( e20 = e24
| ~ spl0_2
| ~ spl0_22 ),
inference(forward_demodulation,[],[f4561,f4441]) ).
fof(f4671,plain,
( $false
| ~ spl0_2
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f4670,f26]) ).
fof(f4672,plain,
( ~ spl0_2
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f4671]) ).
fof(f4673,plain,
( e20 = h(e12)
| ~ spl0_23 ),
inference(superposition,[],[f124,f625]) ).
fof(f4730,plain,
( h(op1(e13,e10)) = op2(h(e13),e23)
| ~ spl0_10 ),
inference(superposition,[],[f159,f4587]) ).
fof(f4745,plain,
( op2(e24,e23) = h(op1(e13,e10))
| ~ spl0_2
| ~ spl0_10 ),
inference(forward_demodulation,[],[f4730,f4561]) ).
fof(f4752,plain,
( op2(e24,e23) = h(e12)
| ~ spl0_2
| ~ spl0_10 ),
inference(forward_demodulation,[],[f4745,f64]) ).
fof(f4756,plain,
( e21 = h(e12)
| ~ spl0_2
| ~ spl0_10 ),
inference(forward_demodulation,[],[f4752,f81]) ).
fof(f4825,plain,
( e20 = e21
| ~ spl0_2
| ~ spl0_10
| ~ spl0_23 ),
inference(forward_demodulation,[],[f4756,f4673]) ).
fof(f4826,plain,
( $false
| ~ spl0_2
| ~ spl0_10
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f4825,f29]) ).
fof(f4827,plain,
( ~ spl0_2
| ~ spl0_10
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f4826]) ).
fof(f4828,plain,
( e20 = h(e14)
| ~ spl0_21 ),
inference(superposition,[],[f124,f617]) ).
fof(f4869,plain,
( e20 = e22
| ~ spl0_11
| ~ spl0_21 ),
inference(superposition,[],[f4615,f4828]) ).
fof(f4870,plain,
( $false
| ~ spl0_11
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f4869,f28]) ).
fof(f4871,plain,
( ~ spl0_11
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f4870]) ).
fof(f4896,plain,
( e20 = h(e10)
| ~ spl0_25 ),
inference(superposition,[],[f124,f633]) ).
fof(f4927,plain,
( e20 = e23
| ~ spl0_10
| ~ spl0_25 ),
inference(superposition,[],[f4896,f4587]) ).
fof(f4950,plain,
( $false
| ~ spl0_10
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f4927,f27]) ).
fof(f4951,plain,
( ~ spl0_10
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f4950]) ).
fof(f4970,plain,
( e24 = h(e14)
| ~ spl0_1 ),
inference(superposition,[],[f120,f178]) ).
fof(f4995,plain,
( e22 = h(e12)
| ~ spl0_13 ),
inference(superposition,[],[f122,f306]) ).
fof(f5022,plain,
( e20 = h(e12)
| ~ spl0_23 ),
inference(superposition,[],[f124,f625]) ).
fof(f5058,plain,
( h(op1(e14,e10)) = op2(e24,h(e10))
| ~ spl0_1 ),
inference(superposition,[],[f154,f4970]) ).
fof(f5067,plain,
( op2(e24,e23) = h(op1(e14,e10))
| ~ spl0_1
| ~ spl0_10 ),
inference(forward_demodulation,[],[f5058,f4587]) ).
fof(f5075,plain,
( op2(e24,e23) = h(e13)
| ~ spl0_1
| ~ spl0_10 ),
inference(forward_demodulation,[],[f5067,f59]) ).
fof(f5081,plain,
( e21 = h(e13)
| ~ spl0_1
| ~ spl0_10 ),
inference(forward_demodulation,[],[f5075,f81]) ).
fof(f5115,plain,
( e20 = e22
| ~ spl0_13
| ~ spl0_23 ),
inference(superposition,[],[f5022,f4995]) ).
fof(f5138,plain,
( $false
| ~ spl0_13
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f5115,f28]) ).
fof(f5139,plain,
( ~ spl0_13
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f5138]) ).
fof(f5153,plain,
( e20 = h(e13)
| ~ spl0_22 ),
inference(superposition,[],[f124,f621]) ).
fof(f5220,plain,
( e20 = e21
| ~ spl0_1
| ~ spl0_10
| ~ spl0_22 ),
inference(forward_demodulation,[],[f5081,f5153]) ).
fof(f5221,plain,
( $false
| ~ spl0_1
| ~ spl0_10
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f5220,f29]) ).
fof(f5222,plain,
( ~ spl0_1
| ~ spl0_10
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f5221]) ).
fof(f5226,plain,
( e24 = h(e12)
| ~ spl0_3 ),
inference(superposition,[],[f120,f186]) ).
fof(f5247,plain,
( e22 = e24
| ~ spl0_3
| ~ spl0_13 ),
inference(forward_demodulation,[],[f5226,f4995]) ).
fof(f5254,plain,
( $false
| ~ spl0_3
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f5247,f21]) ).
fof(f5255,plain,
( ~ spl0_3
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f5254]) ).
fof(f5325,plain,
( h(op1(e12,e11)) = op2(e24,h(e11))
| ~ spl0_3 ),
inference(superposition,[],[f163,f5226]) ).
fof(f5332,plain,
( op2(e24,e21) = h(op1(e12,e11))
| ~ spl0_3
| ~ spl0_19 ),
inference(forward_demodulation,[],[f5325,f3685]) ).
fof(f5341,plain,
( op2(e24,e21) = h(e10)
| ~ spl0_3
| ~ spl0_19 ),
inference(forward_demodulation,[],[f5332,f68]) ).
fof(f5346,plain,
( e23 = op2(e24,e21)
| ~ spl0_3
| ~ spl0_10
| ~ spl0_19 ),
inference(forward_demodulation,[],[f5341,f4587]) ).
fof(f5347,plain,
( e22 = e23
| ~ spl0_3
| ~ spl0_10
| ~ spl0_19 ),
inference(forward_demodulation,[],[f5346,f83]) ).
fof(f5348,plain,
( $false
| ~ spl0_3
| ~ spl0_10
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f5347,f22]) ).
fof(f5349,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f5348]) ).
fof(f5356,plain,
( e23 = h(e13)
| ~ spl0_7 ),
inference(superposition,[],[f121,f223]) ).
fof(f5357,plain,
( j(op2(e24,e23)) = op1(j(e24),e13)
| ~ spl0_7 ),
inference(superposition,[],[f126,f223]) ).
fof(f5376,plain,
( op1(e12,e13) = j(op2(e24,e23))
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f5357,f186]) ).
fof(f5382,plain,
( op1(e12,e13) = j(e21)
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f5376,f81]) ).
fof(f5518,plain,
( e14 = j(e21)
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f5382,f66]) ).
fof(f5550,plain,
( e21 = h(e14)
| ~ spl0_16 ),
inference(superposition,[],[f123,f428]) ).
fof(f5644,plain,
( h(op1(e12,e14)) = op2(h(e12),e21)
| ~ spl0_16 ),
inference(superposition,[],[f160,f5550]) ).
fof(f5649,plain,
( op2(e24,e21) = h(op1(e12,e14))
| ~ spl0_3
| ~ spl0_16 ),
inference(forward_demodulation,[],[f5644,f5226]) ).
fof(f5658,plain,
( op2(e24,e21) = h(e13)
| ~ spl0_3
| ~ spl0_16 ),
inference(forward_demodulation,[],[f5649,f65]) ).
fof(f5665,plain,
( e23 = op2(e24,e21)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f5658,f5356]) ).
fof(f5669,plain,
( e22 = e23
| ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f5665,f83]) ).
fof(f5670,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f5669,f22]) ).
fof(f5671,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f5670]) ).
fof(f5673,plain,
( j(op2(e24,e21)) = op1(j(e24),e12)
| ~ spl0_18 ),
inference(superposition,[],[f128,f436]) ).
fof(f5694,plain,
( op1(e12,e12) = j(op2(e24,e21))
| ~ spl0_3
| ~ spl0_18 ),
inference(forward_demodulation,[],[f5673,f186]) ).
fof(f5702,plain,
( op1(e12,e12) = j(e22)
| ~ spl0_3
| ~ spl0_18 ),
inference(forward_demodulation,[],[f5694,f83]) ).
fof(f5704,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f5518,f427]) ).
fof(f5705,plain,
( ~ spl0_3
| ~ spl0_7
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f5704]) ).
fof(f5706,plain,
( e12 = j(e22)
| ~ spl0_3
| ~ spl0_18 ),
inference(forward_demodulation,[],[f5702,f67]) ).
fof(f5708,plain,
( $false
| ~ spl0_3
| spl0_13
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5706,f305]) ).
fof(f5709,plain,
( ~ spl0_3
| spl0_13
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f5708]) ).
fof(f5711,plain,
( j(op2(e24,e23)) = op1(j(e24),e11)
| ~ spl0_9 ),
inference(superposition,[],[f126,f231]) ).
fof(f5728,plain,
( op1(e12,e11) = j(op2(e24,e23))
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_demodulation,[],[f5711,f186]) ).
fof(f5732,plain,
( op1(e12,e11) = j(e21)
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_demodulation,[],[f5728,f81]) ).
fof(f5733,plain,
( e10 = j(e21)
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_demodulation,[],[f5732,f68]) ).
fof(f5734,plain,
( $false
| ~ spl0_3
| ~ spl0_9
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f5733,f443]) ).
fof(f5735,plain,
( ~ spl0_3
| ~ spl0_9
| spl0_20 ),
inference(avatar_contradiction_clause,[],[f5734]) ).
fof(f5788,plain,
( j(op2(e24,e21)) = op1(j(e24),e10)
| ~ spl0_20 ),
inference(superposition,[],[f128,f444]) ).
fof(f5809,plain,
( op1(e12,e10) = j(op2(e24,e21))
| ~ spl0_3
| ~ spl0_20 ),
inference(forward_demodulation,[],[f5788,f186]) ).
fof(f5817,plain,
( op1(e12,e10) = j(e22)
| ~ spl0_3
| ~ spl0_20 ),
inference(forward_demodulation,[],[f5809,f83]) ).
fof(f5823,plain,
( e11 = j(e22)
| ~ spl0_3
| ~ spl0_20 ),
inference(forward_demodulation,[],[f5817,f69]) ).
fof(f5824,plain,
( $false
| ~ spl0_3
| spl0_14
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f5823,f309]) ).
fof(f5825,plain,
( ~ spl0_3
| spl0_14
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f5824]) ).
fof(f5826,plain,
( e23 = h(e14)
| ~ spl0_6 ),
inference(superposition,[],[f121,f219]) ).
fof(f5846,plain,
( e22 = h(e10)
| ~ spl0_15 ),
inference(superposition,[],[f122,f314]) ).
fof(f5869,plain,
( e21 = h(e13)
| ~ spl0_17 ),
inference(superposition,[],[f123,f432]) ).
fof(f5988,plain,
( h(op1(e12,e13)) = op2(h(e12),e21)
| ~ spl0_17 ),
inference(superposition,[],[f161,f5869]) ).
fof(f5993,plain,
( op2(e24,e21) = h(op1(e12,e13))
| ~ spl0_3
| ~ spl0_17 ),
inference(forward_demodulation,[],[f5988,f5226]) ).
fof(f6002,plain,
( op2(e24,e21) = h(e14)
| ~ spl0_3
| ~ spl0_17 ),
inference(forward_demodulation,[],[f5993,f66]) ).
fof(f6009,plain,
( e23 = op2(e24,e21)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_demodulation,[],[f6002,f5826]) ).
fof(f6013,plain,
( e22 = e23
| ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_demodulation,[],[f6009,f83]) ).
fof(f6014,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f6013,f22]) ).
fof(f6015,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f6014]) ).
fof(f6024,plain,
( e23 = h(e10)
| ~ spl0_10 ),
inference(superposition,[],[f121,f235]) ).
fof(f6025,plain,
( j(op2(e24,e23)) = op1(j(e24),e10)
| ~ spl0_10 ),
inference(superposition,[],[f126,f235]) ).
fof(f6046,plain,
( op1(e12,e10) = j(op2(e24,e23))
| ~ spl0_3
| ~ spl0_10 ),
inference(forward_demodulation,[],[f6025,f186]) ).
fof(f6047,plain,
( e22 = e23
| ~ spl0_10
| ~ spl0_15 ),
inference(forward_demodulation,[],[f6024,f5846]) ).
fof(f6055,plain,
( op1(e12,e10) = j(e21)
| ~ spl0_3
| ~ spl0_10 ),
inference(forward_demodulation,[],[f6046,f81]) ).
fof(f6056,plain,
( $false
| ~ spl0_10
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f6047,f22]) ).
fof(f6057,plain,
( ~ spl0_10
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f6056]) ).
fof(f6062,plain,
( e11 = j(e21)
| ~ spl0_3
| ~ spl0_10 ),
inference(forward_demodulation,[],[f6055,f69]) ).
fof(f6063,plain,
( $false
| ~ spl0_3
| ~ spl0_10
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f6062,f439]) ).
fof(f6064,plain,
( ~ spl0_3
| ~ spl0_10
| spl0_19 ),
inference(avatar_contradiction_clause,[],[f6063]) ).
fof(f6086,plain,
( e23 = h(e11)
| ~ spl0_9 ),
inference(superposition,[],[f121,f231]) ).
fof(f6087,plain,
( j(op2(e24,e23)) = op1(j(e24),e11)
| ~ spl0_9 ),
inference(superposition,[],[f126,f231]) ).
fof(f6103,plain,
( op1(e11,e11) = j(op2(e24,e23))
| ~ spl0_4
| ~ spl0_9 ),
inference(forward_demodulation,[],[f6087,f190]) ).
fof(f6107,plain,
( op1(e11,e11) = j(e21)
| ~ spl0_4
| ~ spl0_9 ),
inference(forward_demodulation,[],[f6103,f81]) ).
fof(f6108,plain,
( e11 = j(e21)
| ~ spl0_4
| ~ spl0_9 ),
inference(forward_demodulation,[],[f6107,f73]) ).
fof(f6109,plain,
( $false
| ~ spl0_4
| ~ spl0_9
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f6108,f439]) ).
fof(f6110,plain,
( ~ spl0_4
| ~ spl0_9
| spl0_19 ),
inference(avatar_contradiction_clause,[],[f6109]) ).
fof(f6114,plain,
( j(op2(e24,e23)) = op1(e14,j(e23))
| ~ spl0_1 ),
inference(superposition,[],[f126,f178]) ).
fof(f6130,plain,
( op1(e14,e11) = j(op2(e24,e23))
| ~ spl0_1
| ~ spl0_9 ),
inference(forward_demodulation,[],[f6114,f231]) ).
fof(f6135,plain,
( op1(e14,e11) = j(e21)
| ~ spl0_1
| ~ spl0_9 ),
inference(forward_demodulation,[],[f6130,f81]) ).
fof(f6136,plain,
( e12 = j(e21)
| ~ spl0_1
| ~ spl0_9 ),
inference(forward_demodulation,[],[f6135,f58]) ).
fof(f6137,plain,
( $false
| ~ spl0_1
| ~ spl0_9
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f6136,f435]) ).
fof(f6138,plain,
( ~ spl0_1
| ~ spl0_9
| spl0_18 ),
inference(avatar_contradiction_clause,[],[f6137]) ).
fof(f6166,plain,
( e21 = h(e12)
| ~ spl0_18 ),
inference(superposition,[],[f123,f436]) ).
fof(f6167,plain,
( j(op2(e24,e21)) = op1(j(e24),e12)
| ~ spl0_18 ),
inference(superposition,[],[f128,f436]) ).
fof(f6188,plain,
( op1(e14,e12) = j(op2(e24,e21))
| ~ spl0_1
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6167,f178]) ).
fof(f6196,plain,
( op1(e14,e12) = j(e22)
| ~ spl0_1
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6188,f83]) ).
fof(f6197,plain,
( e13 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6196,f302]) ).
fof(f6198,plain,
( e11 = e13
| ~ spl0_1
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6197,f57]) ).
fof(f6199,plain,
( $false
| ~ spl0_1
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f6198,f14]) ).
fof(f6200,plain,
( ~ spl0_1
| ~ spl0_12
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f6199]) ).
fof(f6202,plain,
( e11 = j(e22)
| ~ spl0_1
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6196,f57]) ).
fof(f6203,plain,
( $false
| ~ spl0_1
| spl0_14
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f6202,f309]) ).
fof(f6204,plain,
( ~ spl0_1
| spl0_14
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f6203]) ).
fof(f6206,plain,
( e24 = h(e13)
| ~ spl0_2 ),
inference(superposition,[],[f120,f182]) ).
fof(f6208,plain,
( j(op2(e24,e23)) = op1(e13,j(e23))
| ~ spl0_2 ),
inference(superposition,[],[f126,f182]) ).
fof(f6225,plain,
( op1(e13,e11) = j(op2(e24,e23))
| ~ spl0_2
| ~ spl0_9 ),
inference(forward_demodulation,[],[f6208,f231]) ).
fof(f6232,plain,
( op1(e13,e11) = j(e21)
| ~ spl0_2
| ~ spl0_9 ),
inference(forward_demodulation,[],[f6225,f81]) ).
fof(f6289,plain,
( e20 = h(e12)
| ~ spl0_23 ),
inference(superposition,[],[f124,f625]) ).
fof(f6426,plain,
( e20 = e21
| ~ spl0_18
| ~ spl0_23 ),
inference(superposition,[],[f6289,f6166]) ).
fof(f6449,plain,
( $false
| ~ spl0_18
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f6426,f29]) ).
fof(f6450,plain,
( ~ spl0_18
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f6449]) ).
fof(f6465,plain,
( e14 = j(e21)
| ~ spl0_2
| ~ spl0_9 ),
inference(forward_demodulation,[],[f6232,f63]) ).
fof(f6483,plain,
( e21 = h(e14)
| ~ spl0_16 ),
inference(superposition,[],[f123,f428]) ).
fof(f6521,plain,
( h(op1(e13,e14)) = op2(h(e13),e21)
| ~ spl0_16 ),
inference(superposition,[],[f155,f6483]) ).
fof(f6528,plain,
( op2(e24,e21) = h(op1(e13,e14))
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_demodulation,[],[f6521,f6206]) ).
fof(f6537,plain,
( op2(e24,e21) = h(e11)
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_demodulation,[],[f6528,f60]) ).
fof(f6546,plain,
( e23 = op2(e24,e21)
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f6537,f6086]) ).
fof(f6551,plain,
( e22 = e23
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f6546,f83]) ).
fof(f6552,plain,
( $false
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f6551,f22]) ).
fof(f6553,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f6552]) ).
fof(f6586,plain,
( $false
| ~ spl0_2
| ~ spl0_9
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f6465,f427]) ).
fof(f6587,plain,
( ~ spl0_2
| ~ spl0_9
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f6586]) ).
fof(f6606,plain,
( e24 = h(e11)
| ~ spl0_4 ),
inference(superposition,[],[f120,f190]) ).
fof(f6608,plain,
( j(op2(e24,e23)) = op1(e11,j(e23))
| ~ spl0_4 ),
inference(superposition,[],[f126,f190]) ).
fof(f6624,plain,
( j(e21) = op1(e11,j(e23))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f6608,f81]) ).
fof(f6632,plain,
( e23 = h(e13)
| ~ spl0_7 ),
inference(superposition,[],[f121,f223]) ).
fof(f6819,plain,
( op1(e11,e13) = j(e21)
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f6624,f223]) ).
fof(f6825,plain,
( e12 = j(e21)
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f6819,f71]) ).
fof(f6831,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f6825,f435]) ).
fof(f6832,plain,
( ~ spl0_4
| ~ spl0_7
| spl0_18 ),
inference(avatar_contradiction_clause,[],[f6831]) ).
fof(f6864,plain,
( e21 = h(e12)
| ~ spl0_18 ),
inference(superposition,[],[f123,f436]) ).
fof(f6959,plain,
( h(op1(e11,e12)) = op2(h(e11),e21)
| ~ spl0_18 ),
inference(superposition,[],[f167,f6864]) ).
fof(f6962,plain,
( op2(e24,e21) = h(op1(e11,e12))
| ~ spl0_4
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6959,f6606]) ).
fof(f6971,plain,
( op2(e24,e21) = h(e13)
| ~ spl0_4
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6962,f72]) ).
fof(f6979,plain,
( e23 = op2(e24,e21)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6971,f6632]) ).
fof(f6983,plain,
( e22 = e23
| ~ spl0_4
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6979,f83]) ).
fof(f6984,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f6983,f22]) ).
fof(f6985,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f6984]) ).
fof(f6995,plain,
( j(op2(e24,e23)) = op1(e14,j(e23))
| ~ spl0_1 ),
inference(superposition,[],[f126,f178]) ).
fof(f6997,plain,
( j(op2(e24,e21)) = op1(e14,j(e21))
| ~ spl0_1 ),
inference(superposition,[],[f128,f178]) ).
fof(f7009,plain,
( j(e22) = op1(e14,j(e21))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f6997,f83]) ).
fof(f7011,plain,
( op1(e14,e13) = j(op2(e24,e23))
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f6995,f223]) ).
fof(f7017,plain,
( op1(e14,e13) = j(e21)
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f7011,f81]) ).
fof(f7018,plain,
( e10 = j(e21)
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f7017,f56]) ).
fof(f7109,plain,
( op1(e14,e10) = j(e22)
| ~ spl0_1
| ~ spl0_20 ),
inference(forward_demodulation,[],[f7009,f444]) ).
fof(f7114,plain,
( e13 = j(e22)
| ~ spl0_1
| ~ spl0_20 ),
inference(forward_demodulation,[],[f7109,f59]) ).
fof(f7118,plain,
( $false
| ~ spl0_1
| spl0_12
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f7114,f301]) ).
fof(f7119,plain,
( ~ spl0_1
| spl0_12
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f7118]) ).
fof(f7179,plain,
( $false
| ~ spl0_1
| ~ spl0_7
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f7018,f443]) ).
fof(f7180,plain,
( ~ spl0_1
| ~ spl0_7
| spl0_20 ),
inference(avatar_contradiction_clause,[],[f7179]) ).
fof(f7208,plain,
( j(op2(e24,e23)) = op1(j(e24),e14)
| ~ spl0_6 ),
inference(superposition,[],[f126,f219]) ).
fof(f7227,plain,
( op1(e11,e14) = j(op2(e24,e23))
| ~ spl0_4
| ~ spl0_6 ),
inference(forward_demodulation,[],[f7208,f190]) ).
fof(f7233,plain,
( op1(e11,e14) = j(e21)
| ~ spl0_4
| ~ spl0_6 ),
inference(forward_demodulation,[],[f7227,f81]) ).
fof(f7234,plain,
( e10 = j(e21)
| ~ spl0_4
| ~ spl0_6 ),
inference(forward_demodulation,[],[f7233,f70]) ).
fof(f7235,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f7234,f443]) ).
fof(f7236,plain,
( ~ spl0_4
| ~ spl0_6
| spl0_20 ),
inference(avatar_contradiction_clause,[],[f7235]) ).
fof(f7240,plain,
( j(op2(e24,e23)) = op1(e13,j(e23))
| ~ spl0_2 ),
inference(superposition,[],[f126,f182]) ).
fof(f7242,plain,
( j(op2(e24,e21)) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(superposition,[],[f128,f182]) ).
fof(f7256,plain,
( j(e22) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f7242,f83]) ).
fof(f7258,plain,
( op1(e13,e14) = j(op2(e24,e23))
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_demodulation,[],[f7240,f219]) ).
fof(f7266,plain,
( op1(e13,e14) = j(e21)
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_demodulation,[],[f7258,f81]) ).
fof(f7267,plain,
( e11 = j(e21)
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_demodulation,[],[f7266,f60]) ).
fof(f7268,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f7267,f439]) ).
fof(f7269,plain,
( ~ spl0_2
| ~ spl0_6
| spl0_19 ),
inference(avatar_contradiction_clause,[],[f7268]) ).
fof(f7334,plain,
( op1(e13,e12) = j(e22)
| ~ spl0_2
| ~ spl0_18 ),
inference(forward_demodulation,[],[f7256,f436]) ).
fof(f7336,plain,
( e10 = j(e22)
| ~ spl0_2
| ~ spl0_18 ),
inference(forward_demodulation,[],[f7334,f62]) ).
fof(f7339,plain,
( $false
| ~ spl0_2
| spl0_15
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f7336,f313]) ).
fof(f7340,plain,
( ~ spl0_2
| spl0_15
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f7339]) ).
fof(f7369,plain,
( j(op2(e24,e21)) = op1(j(e24),e14)
| ~ spl0_16 ),
inference(superposition,[],[f128,f428]) ).
fof(f7390,plain,
( op1(e13,e14) = j(op2(e24,e21))
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_demodulation,[],[f7369,f182]) ).
fof(f7398,plain,
( op1(e13,e14) = j(e22)
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_demodulation,[],[f7390,f83]) ).
fof(f7403,plain,
( e11 = j(e22)
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_demodulation,[],[f7398,f60]) ).
fof(f7404,plain,
( $false
| ~ spl0_2
| spl0_14
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f7403,f309]) ).
fof(f7405,plain,
( ~ spl0_2
| spl0_14
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f7404]) ).
fof(f7413,plain,
( j(op2(e24,e21)) = op1(e14,j(e21))
| ~ spl0_1 ),
inference(superposition,[],[f128,f178]) ).
fof(f7425,plain,
( op1(e14,e14) = j(op2(e24,e21))
| ~ spl0_1
| ~ spl0_16 ),
inference(forward_demodulation,[],[f7413,f428]) ).
fof(f7430,plain,
( op1(e14,e14) = j(e22)
| ~ spl0_1
| ~ spl0_16 ),
inference(forward_demodulation,[],[f7425,f83]) ).
fof(f7432,plain,
( e14 = j(e22)
| ~ spl0_1
| ~ spl0_16 ),
inference(forward_demodulation,[],[f7430,f55]) ).
fof(f7434,plain,
( $false
| ~ spl0_1
| spl0_11
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f7432,f297]) ).
fof(f7435,plain,
( ~ spl0_1
| spl0_11
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f7434]) ).
fof(f7467,plain,
( j(op2(e24,e21)) = op1(j(e24),e13)
| ~ spl0_17 ),
inference(superposition,[],[f128,f432]) ).
fof(f7486,plain,
( op1(e14,e13) = j(op2(e24,e21))
| ~ spl0_1
| ~ spl0_17 ),
inference(forward_demodulation,[],[f7467,f178]) ).
fof(f7492,plain,
( op1(e14,e13) = j(e22)
| ~ spl0_1
| ~ spl0_17 ),
inference(forward_demodulation,[],[f7486,f83]) ).
fof(f7497,plain,
( e10 = j(e22)
| ~ spl0_1
| ~ spl0_17 ),
inference(forward_demodulation,[],[f7492,f56]) ).
fof(f7498,plain,
( $false
| ~ spl0_1
| spl0_15
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f7497,f313]) ).
fof(f7499,plain,
( ~ spl0_1
| spl0_15
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f7498]) ).
fof(f7504,plain,
( j(op2(e24,e23)) = op1(e11,j(e23))
| ~ spl0_4 ),
inference(superposition,[],[f126,f190]) ).
fof(f7519,plain,
( op1(e11,e10) = j(op2(e24,e23))
| ~ spl0_4
| ~ spl0_10 ),
inference(forward_demodulation,[],[f7504,f235]) ).
fof(f7524,plain,
( op1(e11,e10) = j(e21)
| ~ spl0_4
| ~ spl0_10 ),
inference(forward_demodulation,[],[f7519,f81]) ).
fof(f7833,plain,
( e14 = j(e21)
| ~ spl0_4
| ~ spl0_10 ),
inference(forward_demodulation,[],[f7524,f74]) ).
fof(f7861,plain,
( j(op2(e24,e21)) = op1(j(e24),e14)
| ~ spl0_16 ),
inference(superposition,[],[f128,f428]) ).
fof(f7880,plain,
( op1(e11,e14) = j(op2(e24,e21))
| ~ spl0_4
| ~ spl0_16 ),
inference(forward_demodulation,[],[f7861,f190]) ).
fof(f7886,plain,
( op1(e11,e14) = j(e22)
| ~ spl0_4
| ~ spl0_16 ),
inference(forward_demodulation,[],[f7880,f83]) ).
fof(f7891,plain,
( e10 = j(e22)
| ~ spl0_4
| ~ spl0_16 ),
inference(forward_demodulation,[],[f7886,f70]) ).
fof(f7892,plain,
( $false
| ~ spl0_4
| spl0_15
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f7891,f313]) ).
fof(f7893,plain,
( ~ spl0_4
| spl0_15
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f7892]) ).
fof(f7976,plain,
( $false
| ~ spl0_4
| ~ spl0_10
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f7833,f427]) ).
fof(f7977,plain,
( ~ spl0_4
| ~ spl0_10
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f7976]) ).
cnf(s272,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f195]) ).
cnf(s301,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f236]) ).
cnf(s326,plain,
( ~ spl0_1
| ~ spl0_6 ),
inference(sat_conversion,[],[f265]) ).
cnf(s412,plain,
( ~ spl0_6
| ~ spl0_11 ),
inference(sat_conversion,[],[f351]) ).
cnf(s444,plain,
( ~ spl0_5
| ~ spl0_10 ),
inference(sat_conversion,[],[f386]) ).
cnf(s506,plain,
( spl0_16
| spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f445]) ).
cnf(s532,plain,
( ~ spl0_11
| ~ spl0_16 ),
inference(sat_conversion,[],[f487]) ).
cnf(s598,plain,
( ~ spl0_8
| ~ spl0_13 ),
inference(sat_conversion,[],[f572]) ).
cnf(s634,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f634]) ).
cnf(s656,plain,
( ~ spl0_16
| ~ spl0_21 ),
inference(sat_conversion,[],[f678]) ).
cnf(s730,plain,
( ~ spl0_3
| ~ spl0_8 ),
inference(sat_conversion,[],[f758]) ).
cnf(s937,plain,
( ~ spl0_9
| ~ spl0_14 ),
inference(sat_conversion,[],[f1004]) ).
cnf(s951,plain,
( ~ spl0_10
| ~ spl0_20 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s1128,plain,
( ~ spl0_2
| ~ spl0_17 ),
inference(sat_conversion,[],[f1326]) ).
cnf(s1308,plain,
( ~ spl0_14
| ~ spl0_24 ),
inference(sat_conversion,[],[f1754]) ).
cnf(s1378,plain,
( ~ spl0_2
| ~ spl0_8
| spl0_20 ),
inference(sat_conversion,[],[f1877]) ).
cnf(s1438,plain,
( ~ spl0_20
| ~ spl0_25 ),
inference(sat_conversion,[],[f2051]) ).
cnf(s1509,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_20 ),
inference(sat_conversion,[],[f2250]) ).
cnf(s1548,plain,
( ~ spl0_1
| ~ spl0_21 ),
inference(sat_conversion,[],[f2302]) ).
cnf(s1636,plain,
( ~ spl0_4
| spl0_11
| ~ spl0_20 ),
inference(sat_conversion,[],[f2410]) ).
cnf(s1719,plain,
( ~ spl0_4
| ~ spl0_8
| spl0_17 ),
inference(sat_conversion,[],[f2607]) ).
cnf(s1769,plain,
( ~ spl0_4
| spl0_13
| ~ spl0_17 ),
inference(sat_conversion,[],[f2653]) ).
cnf(s1793,plain,
( ~ spl0_5
| spl0_14
| ~ spl0_17 ),
inference(sat_conversion,[],[f2682]) ).
cnf(s1812,plain,
( ~ spl0_1
| ~ spl0_8
| spl0_19 ),
inference(sat_conversion,[],[f2704]) ).
cnf(s1854,plain,
( ~ spl0_1
| spl0_13
| ~ spl0_19 ),
inference(sat_conversion,[],[f2791]) ).
cnf(s1925,plain,
( ~ spl0_19
| ~ spl0_24 ),
inference(sat_conversion,[],[f2986]) ).
cnf(s1979,plain,
( ~ spl0_5
| spl0_12
| ~ spl0_19 ),
inference(sat_conversion,[],[f3102]) ).
cnf(s2086,plain,
( ~ spl0_5
| ~ spl0_8
| spl0_16 ),
inference(sat_conversion,[],[f3333]) ).
cnf(s2098,plain,
( ~ spl0_5
| spl0_11
| ~ spl0_18 ),
inference(sat_conversion,[],[f3346]) ).
cnf(s2158,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_16 ),
inference(sat_conversion,[],[f3491]) ).
cnf(s2184,plain,
( ~ spl0_6
| ~ spl0_16 ),
inference(sat_conversion,[],[f3540]) ).
cnf(s2219,plain,
( ~ spl0_5
| ~ spl0_7
| spl0_19 ),
inference(sat_conversion,[],[f3589]) ).
cnf(s2241,plain,
( ~ spl0_5
| ~ spl0_6
| spl0_18 ),
inference(sat_conversion,[],[f3616]) ).
cnf(s2271,plain,
( ~ spl0_5
| ~ spl0_9
| spl0_17 ),
inference(sat_conversion,[],[f3641]) ).
cnf(s2336,plain,
( ~ spl0_7
| ~ spl0_12 ),
inference(sat_conversion,[],[f3793]) ).
cnf(s2435,plain,
( ~ spl0_3
| ~ spl0_23 ),
inference(sat_conversion,[],[f3945]) ).
cnf(s2489,plain,
( ~ spl0_6
| ~ spl0_21 ),
inference(sat_conversion,[],[f4087]) ).
cnf(s2523,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_22 ),
inference(sat_conversion,[],[f4170]) ).
cnf(s2557,plain,
( ~ spl0_3
| ~ spl0_19
| ~ spl0_25 ),
inference(sat_conversion,[],[f4243]) ).
cnf(s2580,plain,
( ~ spl0_2
| spl0_11
| ~ spl0_19 ),
inference(sat_conversion,[],[f4275]) ).
cnf(s2590,plain,
( ~ spl0_4
| ~ spl0_19 ),
inference(sat_conversion,[],[f4301]) ).
cnf(s2685,plain,
( ~ spl0_2
| ~ spl0_7 ),
inference(sat_conversion,[],[f4520]) ).
cnf(s2718,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(sat_conversion,[],[f4560]) ).
cnf(s2773,plain,
( ~ spl0_2
| ~ spl0_22 ),
inference(sat_conversion,[],[f4672]) ).
cnf(s2835,plain,
( ~ spl0_2
| ~ spl0_10
| ~ spl0_23 ),
inference(sat_conversion,[],[f4827]) ).
cnf(s2852,plain,
( ~ spl0_11
| ~ spl0_21 ),
inference(sat_conversion,[],[f4871]) ).
cnf(s2879,plain,
( ~ spl0_10
| ~ spl0_25 ),
inference(sat_conversion,[],[f4951]) ).
cnf(s2959,plain,
( ~ spl0_13
| ~ spl0_23 ),
inference(sat_conversion,[],[f5139]) ).
cnf(s2993,plain,
( ~ spl0_1
| ~ spl0_10
| ~ spl0_22 ),
inference(sat_conversion,[],[f5222]) ).
cnf(s3008,plain,
( ~ spl0_3
| ~ spl0_13 ),
inference(sat_conversion,[],[f5255]) ).
cnf(s3051,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_19 ),
inference(sat_conversion,[],[f5349]) ).
cnf(s3200,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(sat_conversion,[],[f5671]) ).
cnf(s3219,plain,
( ~ spl0_3
| ~ spl0_7
| spl0_16 ),
inference(sat_conversion,[],[f5705]) ).
cnf(s3233,plain,
( ~ spl0_3
| spl0_13
| ~ spl0_18 ),
inference(sat_conversion,[],[f5709]) ).
cnf(s3251,plain,
( ~ spl0_3
| ~ spl0_9
| spl0_20 ),
inference(sat_conversion,[],[f5735]) ).
cnf(s3298,plain,
( ~ spl0_3
| spl0_14
| ~ spl0_20 ),
inference(sat_conversion,[],[f5825]) ).
cnf(s3379,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(sat_conversion,[],[f6015]) ).
cnf(s3399,plain,
( ~ spl0_10
| ~ spl0_15 ),
inference(sat_conversion,[],[f6057]) ).
cnf(s3421,plain,
( ~ spl0_3
| ~ spl0_10
| spl0_19 ),
inference(sat_conversion,[],[f6064]) ).
cnf(s3451,plain,
( ~ spl0_4
| ~ spl0_9
| spl0_19 ),
inference(sat_conversion,[],[f6110]) ).
cnf(s3467,plain,
( ~ spl0_1
| ~ spl0_9
| spl0_18 ),
inference(sat_conversion,[],[f6138]) ).
cnf(s3493,plain,
( ~ spl0_1
| ~ spl0_12
| ~ spl0_18 ),
inference(sat_conversion,[],[f6200]) ).
cnf(s3498,plain,
( ~ spl0_1
| spl0_14
| ~ spl0_18 ),
inference(sat_conversion,[],[f6204]) ).
cnf(s3603,plain,
( ~ spl0_18
| ~ spl0_23 ),
inference(sat_conversion,[],[f6450]) ).
cnf(s3652,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(sat_conversion,[],[f6553]) ).
cnf(s3668,plain,
( ~ spl0_2
| ~ spl0_9
| spl0_16 ),
inference(sat_conversion,[],[f6587]) ).
cnf(s3805,plain,
( ~ spl0_4
| ~ spl0_7
| spl0_18 ),
inference(sat_conversion,[],[f6832]) ).
cnf(s3883,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_18 ),
inference(sat_conversion,[],[f6985]) ).
cnf(s3961,plain,
( ~ spl0_1
| spl0_12
| ~ spl0_20 ),
inference(sat_conversion,[],[f7119]) ).
cnf(s3992,plain,
( ~ spl0_1
| ~ spl0_7
| spl0_20 ),
inference(sat_conversion,[],[f7180]) ).
cnf(s4031,plain,
( ~ spl0_4
| ~ spl0_6
| spl0_20 ),
inference(sat_conversion,[],[f7236]) ).
cnf(s4050,plain,
( ~ spl0_2
| ~ spl0_6
| spl0_19 ),
inference(sat_conversion,[],[f7269]) ).
cnf(s4087,plain,
( ~ spl0_2
| spl0_15
| ~ spl0_18 ),
inference(sat_conversion,[],[f7340]) ).
cnf(s4119,plain,
( ~ spl0_2
| spl0_14
| ~ spl0_16 ),
inference(sat_conversion,[],[f7405]) ).
cnf(s4147,plain,
( ~ spl0_1
| spl0_11
| ~ spl0_16 ),
inference(sat_conversion,[],[f7435]) ).
cnf(s4182,plain,
( ~ spl0_1
| spl0_15
| ~ spl0_17 ),
inference(sat_conversion,[],[f7499]) ).
cnf(s4363,plain,
( ~ spl0_4
| spl0_15
| ~ spl0_16 ),
inference(sat_conversion,[],[f7893]) ).
cnf(s4402,plain,
( ~ spl0_4
| ~ spl0_10
| spl0_16 ),
inference(sat_conversion,[],[f7977]) ).
cnf(s4403,plain,
( ~ spl0_9
| ~ spl0_5 ),
inference(rat,[],[s1793,s937,s2271]) ).
cnf(s4404,plain,
( ~ spl0_8
| ~ spl0_5 ),
inference(rat,[],[s2086,s2158]) ).
cnf(s4405,plain,
( ~ spl0_7
| ~ spl0_5 ),
inference(rat,[],[s1979,s2219,s2336]) ).
cnf(s4406,plain,
( ~ spl0_6
| ~ spl0_5 ),
inference(rat,[],[s2098,s412,s2241]) ).
cnf(s4407,plain,
~ spl0_5,
inference(rat,[],[s4406,s301,s4405,s4404,s4403,s444]) ).
cnf(s4408,plain,
( ~ spl0_10
| ~ spl0_4 ),
inference(rat,[],[s4363,s3399,s4402]) ).
cnf(s4409,plain,
( ~ spl0_7
| ~ spl0_4 ),
inference(rat,[],[s3805,s3883]) ).
cnf(s4410,plain,
( ~ spl0_8
| ~ spl0_4 ),
inference(rat,[],[s1769,s598,s1719]) ).
cnf(s4411,plain,
( ~ spl0_6
| ~ spl0_4 ),
inference(rat,[],[s1636,s412,s4031]) ).
cnf(s4412,plain,
( spl0_19
| ~ spl0_4 ),
inference(rat,[],[s4411,s301,s4410,s4409,s4408,s3451]) ).
cnf(s4413,plain,
~ spl0_4,
inference(rat,[],[s4412,s2590]) ).
cnf(s4414,plain,
( ~ spl0_10
| ~ spl0_3 ),
inference(rat,[],[s3051,s3421]) ).
cnf(s4415,plain,
( ~ spl0_9
| ~ spl0_3 ),
inference(rat,[],[s3298,s937,s3251]) ).
cnf(s4416,plain,
( ~ spl0_7
| ~ spl0_3 ),
inference(rat,[],[s3200,s3219]) ).
cnf(s4417,plain,
( ~ spl0_20
| ~ spl0_3 ),
inference(rat,[],[s1308,s634,s3298,s1438,s2435,s2523,s2489,s301,s4416,s4414,s730,s4415]) ).
cnf(s4418,plain,
~ spl0_3,
inference(rat,[],[s634,s1925,s2557,s506,s4417,s2184,s2489,s2523,s3379,s301,s4416,s4415,s4414,s3233,s730,s2435,s3008]) ).
cnf(s4419,plain,
( ~ spl0_6
| ~ spl0_2 ),
inference(rat,[],[s2580,s412,s4050]) ).
cnf(s4420,plain,
( ~ spl0_8
| ~ spl0_2 ),
inference(rat,[],[s1378,s1509]) ).
cnf(s4421,plain,
( ~ spl0_9
| ~ spl0_2 ),
inference(rat,[],[s3652,s3668]) ).
cnf(s4422,plain,
( ~ spl0_16
| ~ spl0_2 ),
inference(rat,[],[s1308,s634,s4119,s656,s2773,s2879,s2835,s301,s4421,s4419,s4420,s2685]) ).
cnf(s4423,plain,
~ spl0_2,
inference(rat,[],[s2852,s634,s2580,s1925,s506,s4422,s4087,s951,s2835,s2879,s3399,s301,s4421,s4420,s4419,s1128,s2685,s2773]) ).
cnf(s4424,plain,
spl0_1,
inference(rat,[],[s272,s4413,s4418,s4407,s4423]) ).
cnf(s4425,plain,
~ spl0_21,
inference(rat,[],[s1548,s4424]) ).
cnf(s4426,plain,
~ spl0_6,
inference(rat,[],[s326,s4424]) ).
cnf(s4427,plain,
( ~ spl0_20
| spl0_8 ),
inference(rat,[],[s301,s3467,s2336,s3493,s3961,s951,s4426,s4424]) ).
cnf(s4428,plain,
~ spl0_9,
inference(rat,[],[s3498,s937,s3467,s4424]) ).
cnf(s4429,plain,
( spl0_19
| spl0_16 ),
inference(rat,[],[s1308,s634,s3498,s3603,s506,s4182,s2879,s2993,s3399,s301,s3992,s4427,s1812,s4425,s4424,s4428,s4426]) ).
cnf(s4430,plain,
~ spl0_19,
inference(rat,[],[s634,s2879,s2993,s301,s598,s2959,s1854,s2718,s1925,s4425,s4424,s4426,s4428]) ).
cnf(s4432,plain,
spl0_16,
inference(rat,[],[s4429,s4430]) ).
cnf(s4435,plain,
~ spl0_11,
inference(rat,[],[s532,s4432]) ).
cnf(s4437,plain,
$false,
inference(rat,[],[s4147,s4424,s4432,s4435]) ).
fof(f7978,plain,
$false,
inference(avatar_sat_refutation,[],[s4437]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG185+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n005.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 19:40:02 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.22 Running first-order model finding
% 0.07/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.00/0.41 % (1077726)Will run a generic schedule for satisfiability detection.
% 1.00/0.41 % (1077736)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3633655273:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.00/0.41 % (1077732)% WARNING: option uhcvi not known.
% 1.00/0.41 % (1077731)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3553951624_2999 on theBenchmark for (2999ds/0Mi)
% 1.00/0.41 % (1077735)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=806394247:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.00/0.41 % (1077732)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3229778200:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.00/0.41 % (1077733)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1229399094:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.00/0.41 % (1077734)dis+10_1_sil=32000:sp=arity:random_seed=482521684:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.00/0.41 % (1077737)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3156081212:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.00/0.41 % Detected minimum model sizes of [10]
% 1.00/0.41 % Detected maximum model sizes of [max]
% 1.00/0.41 % TRYING [10]
% 1.00/0.41 % (1077736)Instruction limit reached!
% 1.00/0.41 % (1077736)------------------------------
% 1.00/0.41 % (1077736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.41 % (1077736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.41 % (1077736)CaDiCaL version: 2.1.3
% 1.00/0.41 % (1077736)Termination reason: Instruction limit
% 1.00/0.41 % (1077736)Termination phase: Saturation
% 1.00/0.41 % (1077736)Time elapsed: 0.035 s
% 1.00/0.41 % (1077736)Peak memory usage: 13 MB
% 1.00/0.41 % (1077736)Instructions burned: 135 (million)
% 1.00/0.41 % (1077745)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1972444278:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.00/0.41 % Detected minimum model sizes of [10]
% 1.00/0.41 % Detected maximum model sizes of [max]
% 1.00/0.41 % TRYING [10]
% 1.00/0.41 % (1077734)Instruction limit reached!
% 1.00/0.41 % (1077734)------------------------------
% 1.00/0.41 % (1077734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.41 % (1077734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.41 % (1077734)CaDiCaL version: 2.1.3
% 1.00/0.41 % (1077734)Termination reason: Instruction limit
% 1.00/0.41 % (1077734)Termination phase: Saturation
% 1.00/0.41 % (1077734)Time elapsed: 0.051 s
% 1.00/0.41 % (1077734)Peak memory usage: 12 MB
% 1.00/0.41 % (1077734)Instructions burned: 103 (million)
% 1.00/0.41 % (1077735)Instruction limit reached!
% 1.00/0.41 % (1077735)------------------------------
% 1.00/0.41 % (1077735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.41 % (1077735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.41 % (1077735)CaDiCaL version: 2.1.3
% 1.00/0.41 % (1077735)Termination reason: Instruction limit
% 1.00/0.41 % (1077735)Termination phase: Saturation
% 1.00/0.41 % (1077735)Time elapsed: 0.059 s
% 1.00/0.41 % (1077735)Peak memory usage: 12 MB
% 1.00/0.41 % (1077735)Instructions burned: 116 (million)
% 1.00/0.41 % (1077747)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1589675690:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.00/0.41 % (1077748)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2707770805:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.00/0.41 % (1077737)Instruction limit reached!
% 1.00/0.41 % (1077737)------------------------------
% 1.00/0.41 % (1077737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.41 % (1077737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.41 % (1077737)CaDiCaL version: 2.1.3
% 1.00/0.41 % (1077737)Termination reason: Instruction limit
% 1.00/0.41 % (1077737)Termination phase: Saturation
% 1.00/0.41 % (1077737)Time elapsed: 0.085 s
% 1.00/0.41 % (1077737)Peak memory usage: 12 MB
% 1.00/0.41 % (1077737)Instructions burned: 160 (million)
% 1.00/0.41 % (1077751)ott-21_1_sil=16000:fs=off:random_seed=3432287793:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.00/0.41 % TRYING [11]
% 1.00/0.41 % (1077733) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1077726-1077733"...
% 1.00/0.41 % (1077747)Instruction limit reached!
% 1.00/0.41 % (1077747)------------------------------
% 1.00/0.41 % (1077747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.41 % (1077747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.41 % (1077747)CaDiCaL version: 2.1.3
% 1.00/0.41 % (1077747)Termination reason: Instruction limit
% 1.00/0.41 % (1077747)Termination phase: Saturation
% 1.00/0.41 % (1077747)Time elapsed: 0.070 s
% 1.00/0.41 % (1077747)Peak memory usage: 13 MB
% 1.00/0.41 % (1077747)Instructions burned: 132 (million)
% 1.00/0.41 % (1077733)...printing done.
% 1.00/0.41 % (1077733)Refutation found. Thanks to Tanya!
% 1.00/0.41 % SZS status Theorem for theBenchmark
% 1.00/0.41 % SZS output start Proof for theBenchmark
% See solution above
% 1.00/0.42 % (1077733)------------------------------
% 1.00/0.42 % (1077733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.42 % (1077733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.42 % (1077733)CaDiCaL version: 2.1.3
% 1.00/0.42 % (1077733)Termination reason: Refutation
% 1.00/0.42 % (1077733)Time elapsed: 0.146 s
% 1.00/0.42 % (1077733)Peak memory usage: 14 MB
% 1.00/0.42 % (1077733)Instructions burned: 290 (million)
% 1.00/0.42 % (1077726)Success in time 0.183 s
% 1.00/0.42 % Vampire exiting
%------------------------------------------------------------------------------