%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX071+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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 01:45:49 PM UTC 2026
% Result : Theorem 19.48s 6.93s
% Output : Refutation 44.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 54
% Syntax : Number of formulae : 572 ( 20 unt; 34 def)
% Number of atoms : 3223 ( 401 equ)
% Maximal formula atoms : 141 ( 5 avg)
% Number of connectives : 4510 (1859 ~;2106 |; 374 &)
% ( 41 <=>; 130 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 69 ( 67 usr; 35 prp; 0-6 aty)
% Number of functors : 62 ( 62 usr; 26 con; 0-3 aty)
% Number of variables : 1349 ( 0 sgn1131 !; 218 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f16,axiom,
'1' != '0',
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id16) ).
fof(f26,axiom,
! [X0,X1] : p(X0) != neg(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id26) ).
fof(f68,axiom,
! [X0,X1] :
( member_terminates(X0,X1)
=> ( member_succeeds(X0,X1)
| member_fails(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id68) ).
fof(f74,axiom,
! [X0,X1,X2] :
( eval_succeeds(X0,X1,X2)
<=> ( ? [X3,X4] :
( X0 = or(X3,X4)
& X2 = '0'
& eval_succeeds(X3,X1,'0')
& eval_succeeds(X4,X1,'0') )
| ? [X5,X6] :
( X0 = or(X5,X6)
& X2 = '1'
& eval_succeeds(X6,X1,'1') )
| ? [X7,X8] :
( X0 = or(X7,X8)
& X2 = '1'
& eval_succeeds(X7,X1,'1') )
| ? [X9,X10] :
( X0 = and(X9,X10)
& X2 = '0'
& eval_succeeds(X10,X1,'0') )
| ? [X11,X12] :
( X0 = and(X11,X12)
& X2 = '0'
& eval_succeeds(X11,X1,'0') )
| ? [X13,X14] :
( X0 = and(X13,X14)
& X2 = '1'
& eval_succeeds(X13,X1,'1')
& eval_succeeds(X14,X1,'1') )
| ? [X15] :
( X0 = neg(X15)
& X2 = '0'
& eval_succeeds(X15,X1,'1') )
| ? [X16] :
( X0 = neg(X16)
& X2 = '1'
& eval_succeeds(X16,X1,'0') )
| ? [X17] :
( X0 = p(X17)
& X2 = '0'
& member_succeeds(neg(p(X17)),X1) )
| ? [X18] :
( X0 = p(X18)
& X2 = '1'
& member_succeeds(p(X18),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id74) ).
fof(f77,axiom,
! [X0,X1,X2] :
( false_succeeds(X0,X1,X2)
<=> ( ? [X3,X4,X5] :
( X0 = or(X3,X4)
& false_succeeds(X3,X1,X5)
& false_succeeds(X4,X5,X2) )
| ? [X6,X7] :
( X0 = and(X6,X7)
& false_succeeds(X7,X1,X2) )
| ? [X8,X9] :
( X0 = and(X8,X9)
& false_succeeds(X8,X1,X2) )
| ? [X10] :
( X0 = neg(X10)
& true_succeeds(X10,X1,X2) )
| ? [X11] :
( X0 = p(X11)
& X2 = cons(neg(p(X11)),X1)
& member_fails(p(X11),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id77) ).
fof(f80,axiom,
! [X0,X1,X2] :
( true_succeeds(X0,X1,X2)
<=> ( ? [X3,X4] :
( X0 = or(X3,X4)
& true_succeeds(X4,X1,X2) )
| ? [X5,X6] :
( X0 = or(X5,X6)
& true_succeeds(X5,X1,X2) )
| ? [X7,X8,X9] :
( X0 = and(X7,X8)
& true_succeeds(X7,X1,X9)
& true_succeeds(X8,X9,X2) )
| ? [X10] :
( X0 = neg(X10)
& false_succeeds(X10,X1,X2) )
| ? [X11] :
( X0 = p(X11)
& X2 = cons(p(X11),X1)
& member_fails(neg(p(X11)),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id80) ).
fof(f98,axiom,
! [X0] :
( literal_succeeds(X0)
<=> ( ? [X1] : X0 = neg(p(X1))
| ? [X2] : X0 = p(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id98) ).
fof(f99,axiom,
! [X0] :
( literal_fails(X0)
<=> ( ! [X1] : X0 != neg(p(X1))
& ! [X2] : X0 != p(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id99) ).
fof(f110,axiom,
! [X0,X1] :
( sub(X0,X1)
<=> ! [X2] :
( member_succeeds(X2,X0)
=> member_succeeds(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','sub/2') ).
fof(f111,axiom,
! [X0,X1] :
( list_succeeds(X1)
=> member_terminates(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(member:termination)') ).
fof(f116,axiom,
! [X0,X1,X2] :
( ( sub(X1,X2)
& member_succeeds(X0,X2) )
=> sub(cons(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(sub:member)') ).
fof(f118,axiom,
! [X0] :
( literal_list_succeeds(X0)
=> list_succeeds(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(literal_list:list)') ).
fof(f119,axiom,
! [X0] :
( interpretation_succeeds(X0)
=> ( literal_list_succeeds(X0)
& ~ ? [X1] :
( member_succeeds(p(X1),X0)
& member_succeeds(neg(p(X1)),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(interpretation:elimination)') ).
fof(f120,axiom,
! [X0] :
( ( literal_list_succeeds(X0)
& ~ ? [X1] :
( member_succeeds(p(X1),X0)
& member_succeeds(neg(p(X1)),X0) ) )
=> interpretation_succeeds(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(interpretation:introduction)') ).
fof(f127,axiom,
! [X0,X1,X2] :
( ( true_succeeds(X0,X1,X2)
& interpretation_succeeds(X1) )
=> interpretation_succeeds(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(true:interpretation)') ).
fof(f130,axiom,
! [X0,X1,X2] :
( ( false_succeeds(X0,X1,X2)
& literal_list_succeeds(X1) )
=> literal_list_succeeds(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(false:literal_list)') ).
fof(f141,axiom,
! [X0,X1,X2,X3] :
( ( eval_succeeds(X0,X1,X3)
& sub(X1,X2) )
=> eval_succeeds(X0,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(eval:sub)') ).
fof(f144,axiom,
! [X0,X1,X2] :
( eval_succeeds(X0,X1,X2)
=> ( interpretation_succeeds(X1)
=> ! [X3] :
( eval_succeeds(X0,X1,X3)
=> X2 = X3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(eval:function)') ).
fof(f149,axiom,
( ! [X0,X1,X2] :
( ( ? [X3,X4] :
( X0 = or(X3,X4)
& X2 = '0'
& eval_succeeds(X3,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( ( literal_list_succeeds(X5)
& sub(X5,X1) )
=> ( ( '0' = '1'
=> ? [X6] :
( sub(X6,X1)
& true_succeeds(X3,X5,X6) ) )
& ( '0' = '0'
=> ? [X6] :
( sub(X6,X1)
& false_succeeds(X3,X5,X6) ) ) ) ) )
& eval_succeeds(X4,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( ( literal_list_succeeds(X5)
& sub(X5,X1) )
=> ( ( '0' = '1'
=> ? [X6] :
( sub(X6,X1)
& true_succeeds(X4,X5,X6) ) )
& ( '0' = '0'
=> ? [X6] :
( sub(X6,X1)
& false_succeeds(X4,X5,X6) ) ) ) ) ) )
| ? [X7,X8] :
( X0 = or(X7,X8)
& X2 = '1'
& eval_succeeds(X8,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( ( literal_list_succeeds(X5)
& sub(X5,X1) )
=> ( ( '1' = '1'
=> ? [X6] :
( sub(X6,X1)
& true_succeeds(X8,X5,X6) ) )
& ( '1' = '0'
=> ? [X6] :
( sub(X6,X1)
& false_succeeds(X8,X5,X6) ) ) ) ) ) )
| ? [X9,X10] :
( X0 = or(X9,X10)
& X2 = '1'
& eval_succeeds(X9,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( ( literal_list_succeeds(X5)
& sub(X5,X1) )
=> ( ( '1' = '1'
=> ? [X6] :
( sub(X6,X1)
& true_succeeds(X9,X5,X6) ) )
& ( '1' = '0'
=> ? [X6] :
( sub(X6,X1)
& false_succeeds(X9,X5,X6) ) ) ) ) ) )
| ? [X11,X12] :
( X0 = and(X11,X12)
& X2 = '0'
& eval_succeeds(X12,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( ( literal_list_succeeds(X5)
& sub(X5,X1) )
=> ( ( '0' = '1'
=> ? [X6] :
( sub(X6,X1)
& true_succeeds(X12,X5,X6) ) )
& ( '0' = '0'
=> ? [X6] :
( sub(X6,X1)
& false_succeeds(X12,X5,X6) ) ) ) ) ) )
| ? [X13,X14] :
( X0 = and(X13,X14)
& X2 = '0'
& eval_succeeds(X13,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( ( literal_list_succeeds(X5)
& sub(X5,X1) )
=> ( ( '0' = '1'
=> ? [X6] :
( sub(X6,X1)
& true_succeeds(X13,X5,X6) ) )
& ( '0' = '0'
=> ? [X6] :
( sub(X6,X1)
& false_succeeds(X13,X5,X6) ) ) ) ) ) )
| ? [X15,X16] :
( X0 = and(X15,X16)
& X2 = '1'
& eval_succeeds(X15,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( ( literal_list_succeeds(X5)
& sub(X5,X1) )
=> ( ( '1' = '1'
=> ? [X6] :
( sub(X6,X1)
& true_succeeds(X15,X5,X6) ) )
& ( '1' = '0'
=> ? [X6] :
( sub(X6,X1)
& false_succeeds(X15,X5,X6) ) ) ) ) )
& eval_succeeds(X16,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( ( literal_list_succeeds(X5)
& sub(X5,X1) )
=> ( ( '1' = '1'
=> ? [X6] :
( sub(X6,X1)
& true_succeeds(X16,X5,X6) ) )
& ( '1' = '0'
=> ? [X6] :
( sub(X6,X1)
& false_succeeds(X16,X5,X6) ) ) ) ) ) )
| ? [X17] :
( X0 = neg(X17)
& X2 = '0'
& eval_succeeds(X17,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( ( literal_list_succeeds(X5)
& sub(X5,X1) )
=> ( ( '1' = '1'
=> ? [X6] :
( sub(X6,X1)
& true_succeeds(X17,X5,X6) ) )
& ( '1' = '0'
=> ? [X6] :
( sub(X6,X1)
& false_succeeds(X17,X5,X6) ) ) ) ) ) )
| ? [X18] :
( X0 = neg(X18)
& X2 = '1'
& eval_succeeds(X18,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( ( literal_list_succeeds(X5)
& sub(X5,X1) )
=> ( ( '0' = '1'
=> ? [X6] :
( sub(X6,X1)
& true_succeeds(X18,X5,X6) ) )
& ( '0' = '0'
=> ? [X6] :
( sub(X6,X1)
& false_succeeds(X18,X5,X6) ) ) ) ) ) )
| ? [X19] :
( X0 = p(X19)
& X2 = '0'
& member_succeeds(neg(p(X19)),X1) )
| ? [X20] :
( X0 = p(X20)
& X2 = '1'
& member_succeeds(p(X20),X1) ) )
=> ( interpretation_succeeds(X1)
=> ! [X5] :
( ( literal_list_succeeds(X5)
& sub(X5,X1) )
=> ( ( X2 = '1'
=> ? [X6] :
( sub(X6,X1)
& true_succeeds(X0,X5,X6) ) )
& ( X2 = '0'
=> ? [X6] :
( sub(X6,X1)
& false_succeeds(X0,X5,X6) ) ) ) ) ) )
=> ! [X0,X1,X2] :
( eval_succeeds(X0,X1,X2)
=> ( interpretation_succeeds(X1)
=> ! [X5] :
( ( literal_list_succeeds(X5)
& sub(X5,X1) )
=> ( ( X2 = '1'
=> ? [X6] :
( sub(X6,X1)
& true_succeeds(X0,X5,X6) ) )
& ( X2 = '0'
=> ? [X6] :
( sub(X6,X1)
& false_succeeds(X0,X5,X6) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',induction) ).
fof(f150,conjecture,
! [X0,X1,X2] :
( eval_succeeds(X0,X1,X2)
=> ( interpretation_succeeds(X1)
=> ! [X3] :
( ( literal_list_succeeds(X3)
& sub(X3,X1) )
=> ( ( X2 = '1'
=> ? [X4] :
( sub(X4,X1)
& true_succeeds(X0,X3,X4) ) )
& ( X2 = '0'
=> ? [X4] :
( sub(X4,X1)
& false_succeeds(X0,X3,X4) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(eval:truefalse)') ).
fof(f151,negated_conjecture,
~ ! [X0,X1,X2] :
( eval_succeeds(X0,X1,X2)
=> ( interpretation_succeeds(X1)
=> ! [X3] :
( ( literal_list_succeeds(X3)
& sub(X3,X1) )
=> ( ( X2 = '1'
=> ? [X4] :
( sub(X4,X1)
& true_succeeds(X0,X3,X4) ) )
& ( X2 = '0'
=> ? [X4] :
( sub(X4,X1)
& false_succeeds(X0,X3,X4) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f150]) ).
fof(f158,plain,
( ! [X0,X1,X2] :
( ( ? [X3,X4] :
( X0 = or(X3,X4)
& X2 = '0'
& eval_succeeds(X3,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( ( literal_list_succeeds(X5)
& sub(X5,X1) )
=> ( ( '0' = '1'
=> ? [X6] :
( sub(X6,X1)
& true_succeeds(X3,X5,X6) ) )
& ( '0' = '0'
=> ? [X7] :
( sub(X7,X1)
& false_succeeds(X3,X5,X7) ) ) ) ) )
& eval_succeeds(X4,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X8] :
( ( literal_list_succeeds(X8)
& sub(X8,X1) )
=> ( ( '0' = '1'
=> ? [X9] :
( sub(X9,X1)
& true_succeeds(X4,X8,X9) ) )
& ( '0' = '0'
=> ? [X10] :
( sub(X10,X1)
& false_succeeds(X4,X8,X10) ) ) ) ) ) )
| ? [X11,X12] :
( or(X11,X12) = X0
& X2 = '1'
& eval_succeeds(X12,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X13] :
( ( literal_list_succeeds(X13)
& sub(X13,X1) )
=> ( ( '1' = '1'
=> ? [X14] :
( sub(X14,X1)
& true_succeeds(X12,X13,X14) ) )
& ( '1' = '0'
=> ? [X15] :
( sub(X15,X1)
& false_succeeds(X12,X13,X15) ) ) ) ) ) )
| ? [X16,X17] :
( or(X16,X17) = X0
& X2 = '1'
& eval_succeeds(X16,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X18] :
( ( literal_list_succeeds(X18)
& sub(X18,X1) )
=> ( ( '1' = '1'
=> ? [X19] :
( sub(X19,X1)
& true_succeeds(X16,X18,X19) ) )
& ( '1' = '0'
=> ? [X20] :
( sub(X20,X1)
& false_succeeds(X16,X18,X20) ) ) ) ) ) )
| ? [X21,X22] :
( and(X21,X22) = X0
& X2 = '0'
& eval_succeeds(X22,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X23] :
( ( literal_list_succeeds(X23)
& sub(X23,X1) )
=> ( ( '0' = '1'
=> ? [X24] :
( sub(X24,X1)
& true_succeeds(X22,X23,X24) ) )
& ( '0' = '0'
=> ? [X25] :
( sub(X25,X1)
& false_succeeds(X22,X23,X25) ) ) ) ) ) )
| ? [X26,X27] :
( and(X26,X27) = X0
& X2 = '0'
& eval_succeeds(X26,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X28] :
( ( literal_list_succeeds(X28)
& sub(X28,X1) )
=> ( ( '0' = '1'
=> ? [X29] :
( sub(X29,X1)
& true_succeeds(X26,X28,X29) ) )
& ( '0' = '0'
=> ? [X30] :
( sub(X30,X1)
& false_succeeds(X26,X28,X30) ) ) ) ) ) )
| ? [X31,X32] :
( and(X31,X32) = X0
& X2 = '1'
& eval_succeeds(X31,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X33] :
( ( literal_list_succeeds(X33)
& sub(X33,X1) )
=> ( ( '1' = '1'
=> ? [X34] :
( sub(X34,X1)
& true_succeeds(X31,X33,X34) ) )
& ( '1' = '0'
=> ? [X35] :
( sub(X35,X1)
& false_succeeds(X31,X33,X35) ) ) ) ) )
& eval_succeeds(X32,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X36] :
( ( literal_list_succeeds(X36)
& sub(X36,X1) )
=> ( ( '1' = '1'
=> ? [X37] :
( sub(X37,X1)
& true_succeeds(X32,X36,X37) ) )
& ( '1' = '0'
=> ? [X38] :
( sub(X38,X1)
& false_succeeds(X32,X36,X38) ) ) ) ) ) )
| ? [X39] :
( neg(X39) = X0
& X2 = '0'
& eval_succeeds(X39,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X40] :
( ( literal_list_succeeds(X40)
& sub(X40,X1) )
=> ( ( '1' = '1'
=> ? [X41] :
( sub(X41,X1)
& true_succeeds(X39,X40,X41) ) )
& ( '1' = '0'
=> ? [X42] :
( sub(X42,X1)
& false_succeeds(X39,X40,X42) ) ) ) ) ) )
| ? [X43] :
( neg(X43) = X0
& X2 = '1'
& eval_succeeds(X43,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X44] :
( ( literal_list_succeeds(X44)
& sub(X44,X1) )
=> ( ( '0' = '1'
=> ? [X45] :
( sub(X45,X1)
& true_succeeds(X43,X44,X45) ) )
& ( '0' = '0'
=> ? [X46] :
( sub(X46,X1)
& false_succeeds(X43,X44,X46) ) ) ) ) ) )
| ? [X47] :
( p(X47) = X0
& X2 = '0'
& member_succeeds(neg(p(X47)),X1) )
| ? [X48] :
( p(X48) = X0
& X2 = '1'
& member_succeeds(p(X48),X1) ) )
=> ( interpretation_succeeds(X1)
=> ! [X49] :
( ( literal_list_succeeds(X49)
& sub(X49,X1) )
=> ( ( X2 = '1'
=> ? [X50] :
( sub(X50,X1)
& true_succeeds(X0,X49,X50) ) )
& ( X2 = '0'
=> ? [X51] :
( sub(X51,X1)
& false_succeeds(X0,X49,X51) ) ) ) ) ) )
=> ! [X52,X53,X54] :
( eval_succeeds(X52,X53,X54)
=> ( interpretation_succeeds(X53)
=> ! [X55] :
( ( literal_list_succeeds(X55)
& sub(X55,X53) )
=> ( ( '1' = X54
=> ? [X56] :
( sub(X56,X53)
& true_succeeds(X52,X55,X56) ) )
& ( '0' = X54
=> ? [X57] :
( sub(X57,X53)
& false_succeeds(X52,X55,X57) ) ) ) ) ) ) ),
inference(rectify,[],[f149]) ).
fof(f159,plain,
~ ! [X0,X1,X2] :
( eval_succeeds(X0,X1,X2)
=> ( interpretation_succeeds(X1)
=> ! [X3] :
( ( literal_list_succeeds(X3)
& sub(X3,X1) )
=> ( ( X2 = '1'
=> ? [X4] :
( sub(X4,X1)
& true_succeeds(X0,X3,X4) ) )
& ( X2 = '0'
=> ? [X5] :
( sub(X5,X1)
& false_succeeds(X0,X3,X5) ) ) ) ) ) ),
inference(rectify,[],[f151]) ).
fof(f203,plain,
! [X0,X1] :
( member_succeeds(X0,X1)
| member_fails(X0,X1)
| ~ member_terminates(X0,X1) ),
inference(ennf_transformation,[],[f68]) ).
fof(f204,plain,
! [X0,X1] :
( member_succeeds(X0,X1)
| member_fails(X0,X1)
| ~ member_terminates(X0,X1) ),
inference(flattening,[],[f203]) ).
fof(f210,plain,
! [X0,X1] :
( sub(X0,X1)
<=> ! [X2] :
( member_succeeds(X2,X1)
| ~ member_succeeds(X2,X0) ) ),
inference(ennf_transformation,[],[f110]) ).
fof(f211,plain,
! [X0,X1] :
( member_terminates(X0,X1)
| ~ list_succeeds(X1) ),
inference(ennf_transformation,[],[f111]) ).
fof(f216,plain,
! [X0,X1,X2] :
( sub(cons(X0,X1),X2)
| ~ sub(X1,X2)
| ~ member_succeeds(X0,X2) ),
inference(ennf_transformation,[],[f116]) ).
fof(f217,plain,
! [X0,X1,X2] :
( sub(cons(X0,X1),X2)
| ~ sub(X1,X2)
| ~ member_succeeds(X0,X2) ),
inference(flattening,[],[f216]) ).
fof(f219,plain,
! [X0] :
( list_succeeds(X0)
| ~ literal_list_succeeds(X0) ),
inference(ennf_transformation,[],[f118]) ).
fof(f220,plain,
! [X0] :
( ( literal_list_succeeds(X0)
& ! [X1] :
( ~ member_succeeds(p(X1),X0)
| ~ member_succeeds(neg(p(X1)),X0) ) )
| ~ interpretation_succeeds(X0) ),
inference(ennf_transformation,[],[f119]) ).
fof(f221,plain,
! [X0] :
( interpretation_succeeds(X0)
| ~ literal_list_succeeds(X0)
| ? [X1] :
( member_succeeds(p(X1),X0)
& member_succeeds(neg(p(X1)),X0) ) ),
inference(ennf_transformation,[],[f120]) ).
fof(f222,plain,
! [X0] :
( interpretation_succeeds(X0)
| ~ literal_list_succeeds(X0)
| ? [X1] :
( member_succeeds(p(X1),X0)
& member_succeeds(neg(p(X1)),X0) ) ),
inference(flattening,[],[f221]) ).
fof(f232,plain,
! [X0,X1,X2] :
( interpretation_succeeds(X2)
| ~ true_succeeds(X0,X1,X2)
| ~ interpretation_succeeds(X1) ),
inference(ennf_transformation,[],[f127]) ).
fof(f233,plain,
! [X0,X1,X2] :
( interpretation_succeeds(X2)
| ~ true_succeeds(X0,X1,X2)
| ~ interpretation_succeeds(X1) ),
inference(flattening,[],[f232]) ).
fof(f238,plain,
! [X0,X1,X2] :
( literal_list_succeeds(X2)
| ~ false_succeeds(X0,X1,X2)
| ~ literal_list_succeeds(X1) ),
inference(ennf_transformation,[],[f130]) ).
fof(f239,plain,
! [X0,X1,X2] :
( literal_list_succeeds(X2)
| ~ false_succeeds(X0,X1,X2)
| ~ literal_list_succeeds(X1) ),
inference(flattening,[],[f238]) ).
fof(f256,plain,
! [X0,X1,X2,X3] :
( eval_succeeds(X0,X2,X3)
| ~ eval_succeeds(X0,X1,X3)
| ~ sub(X1,X2) ),
inference(ennf_transformation,[],[f141]) ).
fof(f257,plain,
! [X0,X1,X2,X3] :
( eval_succeeds(X0,X2,X3)
| ~ eval_succeeds(X0,X1,X3)
| ~ sub(X1,X2) ),
inference(flattening,[],[f256]) ).
fof(f261,plain,
! [X0,X1,X2] :
( ! [X3] :
( X2 = X3
| ~ eval_succeeds(X0,X1,X3) )
| ~ interpretation_succeeds(X1)
| ~ eval_succeeds(X0,X1,X2) ),
inference(ennf_transformation,[],[f144]) ).
fof(f262,plain,
! [X0,X1,X2] :
( ! [X3] :
( X2 = X3
| ~ eval_succeeds(X0,X1,X3) )
| ~ interpretation_succeeds(X1)
| ~ eval_succeeds(X0,X1,X2) ),
inference(flattening,[],[f261]) ).
fof(f267,plain,
( ! [X52,X53,X54] :
( ! [X55] :
( ( ( ? [X56] :
( sub(X56,X53)
& true_succeeds(X52,X55,X56) )
| '1' != X54 )
& ( ? [X57] :
( sub(X57,X53)
& false_succeeds(X52,X55,X57) )
| '0' != X54 ) )
| ~ literal_list_succeeds(X55)
| ~ sub(X55,X53) )
| ~ interpretation_succeeds(X53)
| ~ eval_succeeds(X52,X53,X54) )
| ? [X0,X1,X2] :
( ? [X49] :
( ( ( ! [X50] :
( ~ sub(X50,X1)
| ~ true_succeeds(X0,X49,X50) )
& X2 = '1' )
| ( ! [X51] :
( ~ sub(X51,X1)
| ~ false_succeeds(X0,X49,X51) )
& X2 = '0' ) )
& literal_list_succeeds(X49)
& sub(X49,X1) )
& interpretation_succeeds(X1)
& ( ? [X3,X4] :
( X0 = or(X3,X4)
& X2 = '0'
& eval_succeeds(X3,X1,'0')
& ( ! [X5] :
( ( ( ? [X6] :
( sub(X6,X1)
& true_succeeds(X3,X5,X6) )
| '1' != '0' )
& ( ? [X7] :
( sub(X7,X1)
& false_succeeds(X3,X5,X7) )
| '0' != '0' ) )
| ~ literal_list_succeeds(X5)
| ~ sub(X5,X1) )
| ~ interpretation_succeeds(X1) )
& eval_succeeds(X4,X1,'0')
& ( ! [X8] :
( ( ( ? [X9] :
( sub(X9,X1)
& true_succeeds(X4,X8,X9) )
| '1' != '0' )
& ( ? [X10] :
( sub(X10,X1)
& false_succeeds(X4,X8,X10) )
| '0' != '0' ) )
| ~ literal_list_succeeds(X8)
| ~ sub(X8,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X11,X12] :
( or(X11,X12) = X0
& X2 = '1'
& eval_succeeds(X12,X1,'1')
& ( ! [X13] :
( ( ( ? [X14] :
( sub(X14,X1)
& true_succeeds(X12,X13,X14) )
| '1' != '1' )
& ( ? [X15] :
( sub(X15,X1)
& false_succeeds(X12,X13,X15) )
| '1' != '0' ) )
| ~ literal_list_succeeds(X13)
| ~ sub(X13,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X16,X17] :
( or(X16,X17) = X0
& X2 = '1'
& eval_succeeds(X16,X1,'1')
& ( ! [X18] :
( ( ( ? [X19] :
( sub(X19,X1)
& true_succeeds(X16,X18,X19) )
| '1' != '1' )
& ( ? [X20] :
( sub(X20,X1)
& false_succeeds(X16,X18,X20) )
| '1' != '0' ) )
| ~ literal_list_succeeds(X18)
| ~ sub(X18,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X21,X22] :
( and(X21,X22) = X0
& X2 = '0'
& eval_succeeds(X22,X1,'0')
& ( ! [X23] :
( ( ( ? [X24] :
( sub(X24,X1)
& true_succeeds(X22,X23,X24) )
| '1' != '0' )
& ( ? [X25] :
( sub(X25,X1)
& false_succeeds(X22,X23,X25) )
| '0' != '0' ) )
| ~ literal_list_succeeds(X23)
| ~ sub(X23,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X26,X27] :
( and(X26,X27) = X0
& X2 = '0'
& eval_succeeds(X26,X1,'0')
& ( ! [X28] :
( ( ( ? [X29] :
( sub(X29,X1)
& true_succeeds(X26,X28,X29) )
| '1' != '0' )
& ( ? [X30] :
( sub(X30,X1)
& false_succeeds(X26,X28,X30) )
| '0' != '0' ) )
| ~ literal_list_succeeds(X28)
| ~ sub(X28,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X31,X32] :
( and(X31,X32) = X0
& X2 = '1'
& eval_succeeds(X31,X1,'1')
& ( ! [X33] :
( ( ( ? [X34] :
( sub(X34,X1)
& true_succeeds(X31,X33,X34) )
| '1' != '1' )
& ( ? [X35] :
( sub(X35,X1)
& false_succeeds(X31,X33,X35) )
| '1' != '0' ) )
| ~ literal_list_succeeds(X33)
| ~ sub(X33,X1) )
| ~ interpretation_succeeds(X1) )
& eval_succeeds(X32,X1,'1')
& ( ! [X36] :
( ( ( ? [X37] :
( sub(X37,X1)
& true_succeeds(X32,X36,X37) )
| '1' != '1' )
& ( ? [X38] :
( sub(X38,X1)
& false_succeeds(X32,X36,X38) )
| '1' != '0' ) )
| ~ literal_list_succeeds(X36)
| ~ sub(X36,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X39] :
( neg(X39) = X0
& X2 = '0'
& eval_succeeds(X39,X1,'1')
& ( ! [X40] :
( ( ( ? [X41] :
( sub(X41,X1)
& true_succeeds(X39,X40,X41) )
| '1' != '1' )
& ( ? [X42] :
( sub(X42,X1)
& false_succeeds(X39,X40,X42) )
| '1' != '0' ) )
| ~ literal_list_succeeds(X40)
| ~ sub(X40,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X43] :
( neg(X43) = X0
& X2 = '1'
& eval_succeeds(X43,X1,'0')
& ( ! [X44] :
( ( ( ? [X45] :
( sub(X45,X1)
& true_succeeds(X43,X44,X45) )
| '1' != '0' )
& ( ? [X46] :
( sub(X46,X1)
& false_succeeds(X43,X44,X46) )
| '0' != '0' ) )
| ~ literal_list_succeeds(X44)
| ~ sub(X44,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X47] :
( p(X47) = X0
& X2 = '0'
& member_succeeds(neg(p(X47)),X1) )
| ? [X48] :
( p(X48) = X0
& X2 = '1'
& member_succeeds(p(X48),X1) ) ) ) ),
inference(ennf_transformation,[],[f158]) ).
fof(f268,plain,
( ! [X52,X53,X54] :
( ! [X55] :
( ( ( ? [X56] :
( sub(X56,X53)
& true_succeeds(X52,X55,X56) )
| '1' != X54 )
& ( ? [X57] :
( sub(X57,X53)
& false_succeeds(X52,X55,X57) )
| '0' != X54 ) )
| ~ literal_list_succeeds(X55)
| ~ sub(X55,X53) )
| ~ interpretation_succeeds(X53)
| ~ eval_succeeds(X52,X53,X54) )
| ? [X0,X1,X2] :
( ? [X49] :
( ( ( ! [X50] :
( ~ sub(X50,X1)
| ~ true_succeeds(X0,X49,X50) )
& X2 = '1' )
| ( ! [X51] :
( ~ sub(X51,X1)
| ~ false_succeeds(X0,X49,X51) )
& X2 = '0' ) )
& literal_list_succeeds(X49)
& sub(X49,X1) )
& interpretation_succeeds(X1)
& ( ? [X3,X4] :
( X0 = or(X3,X4)
& X2 = '0'
& eval_succeeds(X3,X1,'0')
& ( ! [X5] :
( ( ( ? [X6] :
( sub(X6,X1)
& true_succeeds(X3,X5,X6) )
| '1' != '0' )
& ( ? [X7] :
( sub(X7,X1)
& false_succeeds(X3,X5,X7) )
| '0' != '0' ) )
| ~ literal_list_succeeds(X5)
| ~ sub(X5,X1) )
| ~ interpretation_succeeds(X1) )
& eval_succeeds(X4,X1,'0')
& ( ! [X8] :
( ( ( ? [X9] :
( sub(X9,X1)
& true_succeeds(X4,X8,X9) )
| '1' != '0' )
& ( ? [X10] :
( sub(X10,X1)
& false_succeeds(X4,X8,X10) )
| '0' != '0' ) )
| ~ literal_list_succeeds(X8)
| ~ sub(X8,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X11,X12] :
( or(X11,X12) = X0
& X2 = '1'
& eval_succeeds(X12,X1,'1')
& ( ! [X13] :
( ( ( ? [X14] :
( sub(X14,X1)
& true_succeeds(X12,X13,X14) )
| '1' != '1' )
& ( ? [X15] :
( sub(X15,X1)
& false_succeeds(X12,X13,X15) )
| '1' != '0' ) )
| ~ literal_list_succeeds(X13)
| ~ sub(X13,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X16,X17] :
( or(X16,X17) = X0
& X2 = '1'
& eval_succeeds(X16,X1,'1')
& ( ! [X18] :
( ( ( ? [X19] :
( sub(X19,X1)
& true_succeeds(X16,X18,X19) )
| '1' != '1' )
& ( ? [X20] :
( sub(X20,X1)
& false_succeeds(X16,X18,X20) )
| '1' != '0' ) )
| ~ literal_list_succeeds(X18)
| ~ sub(X18,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X21,X22] :
( and(X21,X22) = X0
& X2 = '0'
& eval_succeeds(X22,X1,'0')
& ( ! [X23] :
( ( ( ? [X24] :
( sub(X24,X1)
& true_succeeds(X22,X23,X24) )
| '1' != '0' )
& ( ? [X25] :
( sub(X25,X1)
& false_succeeds(X22,X23,X25) )
| '0' != '0' ) )
| ~ literal_list_succeeds(X23)
| ~ sub(X23,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X26,X27] :
( and(X26,X27) = X0
& X2 = '0'
& eval_succeeds(X26,X1,'0')
& ( ! [X28] :
( ( ( ? [X29] :
( sub(X29,X1)
& true_succeeds(X26,X28,X29) )
| '1' != '0' )
& ( ? [X30] :
( sub(X30,X1)
& false_succeeds(X26,X28,X30) )
| '0' != '0' ) )
| ~ literal_list_succeeds(X28)
| ~ sub(X28,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X31,X32] :
( and(X31,X32) = X0
& X2 = '1'
& eval_succeeds(X31,X1,'1')
& ( ! [X33] :
( ( ( ? [X34] :
( sub(X34,X1)
& true_succeeds(X31,X33,X34) )
| '1' != '1' )
& ( ? [X35] :
( sub(X35,X1)
& false_succeeds(X31,X33,X35) )
| '1' != '0' ) )
| ~ literal_list_succeeds(X33)
| ~ sub(X33,X1) )
| ~ interpretation_succeeds(X1) )
& eval_succeeds(X32,X1,'1')
& ( ! [X36] :
( ( ( ? [X37] :
( sub(X37,X1)
& true_succeeds(X32,X36,X37) )
| '1' != '1' )
& ( ? [X38] :
( sub(X38,X1)
& false_succeeds(X32,X36,X38) )
| '1' != '0' ) )
| ~ literal_list_succeeds(X36)
| ~ sub(X36,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X39] :
( neg(X39) = X0
& X2 = '0'
& eval_succeeds(X39,X1,'1')
& ( ! [X40] :
( ( ( ? [X41] :
( sub(X41,X1)
& true_succeeds(X39,X40,X41) )
| '1' != '1' )
& ( ? [X42] :
( sub(X42,X1)
& false_succeeds(X39,X40,X42) )
| '1' != '0' ) )
| ~ literal_list_succeeds(X40)
| ~ sub(X40,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X43] :
( neg(X43) = X0
& X2 = '1'
& eval_succeeds(X43,X1,'0')
& ( ! [X44] :
( ( ( ? [X45] :
( sub(X45,X1)
& true_succeeds(X43,X44,X45) )
| '1' != '0' )
& ( ? [X46] :
( sub(X46,X1)
& false_succeeds(X43,X44,X46) )
| '0' != '0' ) )
| ~ literal_list_succeeds(X44)
| ~ sub(X44,X1) )
| ~ interpretation_succeeds(X1) ) )
| ? [X47] :
( p(X47) = X0
& X2 = '0'
& member_succeeds(neg(p(X47)),X1) )
| ? [X48] :
( p(X48) = X0
& X2 = '1'
& member_succeeds(p(X48),X1) ) ) ) ),
inference(flattening,[],[f267]) ).
fof(f269,plain,
? [X0,X1,X2] :
( ? [X3] :
( ( ( ! [X4] :
( ~ sub(X4,X1)
| ~ true_succeeds(X0,X3,X4) )
& X2 = '1' )
| ( ! [X5] :
( ~ sub(X5,X1)
| ~ false_succeeds(X0,X3,X5) )
& X2 = '0' ) )
& literal_list_succeeds(X3)
& sub(X3,X1) )
& interpretation_succeeds(X1)
& eval_succeeds(X0,X1,X2) ),
inference(ennf_transformation,[],[f159]) ).
fof(f270,plain,
? [X0,X1,X2] :
( ? [X3] :
( ( ( ! [X4] :
( ~ sub(X4,X1)
| ~ true_succeeds(X0,X3,X4) )
& X2 = '1' )
| ( ! [X5] :
( ~ sub(X5,X1)
| ~ false_succeeds(X0,X3,X5) )
& X2 = '0' ) )
& literal_list_succeeds(X3)
& sub(X3,X1) )
& interpretation_succeeds(X1)
& eval_succeeds(X0,X1,X2) ),
inference(flattening,[],[f269]) ).
fof(f286,plain,
'1' != '0',
inference(cnf_transformation,[],[f16]) ).
fof(f296,plain,
! [X0,X1] : p(X0) != neg(X1),
inference(cnf_transformation,[],[f26]) ).
fof(f346,plain,
! [X0,X1] :
( ~ member_terminates(X0,X1)
| member_fails(X0,X1)
| member_succeeds(X0,X1) ),
inference(cnf_transformation,[],[f204]) ).
fof(f423,plain,
! [X2,X3,X0,X1,X4] :
( ~ sP53(X4,X3,X2,X1,X0)
| '0' = X2 ),
inference(cnf_transformation,[],[f74]) ).
fof(f427,plain,
! [X2,X0,X1,X6,X5] :
( ~ sP52(X6,X5,X2,X1,X0)
| '1' = X2 ),
inference(cnf_transformation,[],[f74]) ).
fof(f431,plain,
! [X2,X0,X1,X8,X7] :
( ~ sP51(X8,X7,X2,X1,X0)
| '1' = X2 ),
inference(cnf_transformation,[],[f74]) ).
fof(f435,plain,
! [X2,X10,X0,X1,X9] :
( ~ sP50(X10,X9,X2,X1,X0)
| '0' = X2 ),
inference(cnf_transformation,[],[f74]) ).
fof(f439,plain,
! [X2,X0,X11,X1,X12] :
( ~ sP49(X12,X11,X2,X1,X0)
| '0' = X2 ),
inference(cnf_transformation,[],[f74]) ).
fof(f444,plain,
! [X2,X0,X1,X14,X13] :
( ~ sP48(X14,X13,X2,X1,X0)
| '1' = X2 ),
inference(cnf_transformation,[],[f74]) ).
fof(f448,plain,
! [X2,X0,X1,X15] :
( '0' = X2
| ~ sP47(X15,X2,X1,X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f452,plain,
! [X2,X0,X1,X16] :
( ~ sP46(X16,X2,X1,X0)
| '1' = X2 ),
inference(cnf_transformation,[],[f74]) ).
fof(f454,plain,
! [X2,X0,X1,X17] :
( ~ member_succeeds(neg(p(X17)),X1)
| '0' != X2
| p(X17) != X0
| eval_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f74]) ).
fof(f459,plain,
! [X2,X0,X1] :
( '1' = X2
| '0' = X2
| sP46(sK32(X0,X1,X2),X2,X1,X0)
| sP47(sK33(X0,X1,X2),X2,X1,X0)
| sP48(sK35(X0,X1,X2),sK34(X0,X1,X2),X2,X1,X0)
| sP49(sK37(X0,X1,X2),sK36(X0,X1,X2),X2,X1,X0)
| sP50(sK39(X0,X1,X2),sK38(X0,X1,X2),X2,X1,X0)
| sP51(sK41(X0,X1,X2),sK40(X0,X1,X2),X2,X1,X0)
| sP52(sK43(X0,X1,X2),sK42(X0,X1,X2),X2,X1,X0)
| sP53(sK45(X0,X1,X2),sK44(X0,X1,X2),X2,X1,X0)
| ~ eval_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f74]) ).
fof(f464,plain,
! [X2,X0,X18,X1] :
( ~ member_succeeds(p(X18),X1)
| '1' != X2
| p(X18) != X0
| eval_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f74]) ).
fof(f611,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ false_succeeds(X4,X5,X2)
| ~ false_succeeds(X3,X1,X5)
| or(X3,X4) != X0
| sP123(X5,X4,X3,X2,X1,X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f615,plain,
! [X2,X0,X1,X6,X7] :
( ~ false_succeeds(X7,X1,X2)
| and(X6,X7) != X0
| sP122(X7,X6,X2,X1,X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f618,plain,
! [X2,X0,X1,X8,X9] :
( ~ false_succeeds(X8,X1,X2)
| and(X8,X9) != X0
| false_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f77]) ).
fof(f631,plain,
! [X2,X10,X0,X1] :
( ~ true_succeeds(X10,X1,X2)
| neg(X10) != X0
| false_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f77]) ).
fof(f632,plain,
! [X2,X0,X11,X1] :
( ~ member_fails(p(X11),X1)
| cons(neg(p(X11)),X1) != X2
| p(X11) != X0
| false_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f77]) ).
fof(f633,plain,
! [X2,X0,X1,X6,X7] :
( ~ sP122(X7,X6,X2,X1,X0)
| false_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f77]) ).
fof(f634,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sP123(X5,X4,X3,X2,X1,X0)
| false_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f77]) ).
fof(f694,plain,
! [X2,X3,X0,X1,X4] :
( ~ true_succeeds(X4,X1,X2)
| or(X3,X4) != X0
| sP160(X4,X3,X2,X1,X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f697,plain,
! [X2,X0,X1,X6,X5] :
( ~ true_succeeds(X5,X1,X2)
| or(X5,X6) != X0
| sP159(X6,X5,X2,X1,X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f700,plain,
! [X2,X0,X1,X8,X9,X7] :
( ~ true_succeeds(X8,X9,X2)
| ~ true_succeeds(X7,X1,X9)
| and(X7,X8) != X0
| true_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f80]) ).
fof(f719,plain,
! [X2,X10,X0,X1] :
( ~ false_succeeds(X10,X1,X2)
| neg(X10) != X0
| true_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f80]) ).
fof(f720,plain,
! [X2,X0,X11,X1] :
( ~ member_fails(neg(p(X11)),X1)
| cons(p(X11),X1) != X2
| p(X11) != X0
| true_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f80]) ).
fof(f721,plain,
! [X2,X0,X1,X6,X5] :
( ~ sP159(X6,X5,X2,X1,X0)
| true_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f80]) ).
fof(f722,plain,
! [X2,X3,X0,X1,X4] :
( ~ sP160(X4,X3,X2,X1,X0)
| true_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f80]) ).
fof(f838,plain,
! [X0] :
( neg(p(sK200(X0))) = X0
| p(sK199(X0)) = X0
| ~ literal_succeeds(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f839,plain,
! [X2,X0] :
( p(X2) != X0
| literal_succeeds(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f841,plain,
! [X2,X0] :
( p(X2) != X0
| ~ literal_fails(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f843,plain,
! [X0] :
( neg(p(sK202(X0))) = X0
| p(sK201(X0)) = X0
| literal_fails(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f936,plain,
! [X2,X0,X1] :
( ~ sub(X0,X1)
| member_succeeds(X2,X1)
| ~ member_succeeds(X2,X0) ),
inference(cnf_transformation,[],[f210]) ).
fof(f939,plain,
! [X0,X1] :
( member_terminates(X0,X1)
| ~ list_succeeds(X1) ),
inference(cnf_transformation,[],[f211]) ).
fof(f944,plain,
! [X2,X0,X1] :
( sub(cons(X0,X1),X2)
| ~ sub(X1,X2)
| ~ member_succeeds(X0,X2) ),
inference(cnf_transformation,[],[f217]) ).
fof(f946,plain,
! [X0] :
( ~ literal_list_succeeds(X0)
| list_succeeds(X0) ),
inference(cnf_transformation,[],[f219]) ).
fof(f947,plain,
! [X0,X1] :
( ~ member_succeeds(neg(p(X1)),X0)
| ~ interpretation_succeeds(X0)
| ~ member_succeeds(p(X1),X0) ),
inference(cnf_transformation,[],[f220]) ).
fof(f948,plain,
! [X0] :
( ~ interpretation_succeeds(X0)
| literal_list_succeeds(X0) ),
inference(cnf_transformation,[],[f220]) ).
fof(f949,plain,
! [X0] :
( member_succeeds(neg(p(sK236(X0))),X0)
| ~ literal_list_succeeds(X0)
| interpretation_succeeds(X0) ),
inference(cnf_transformation,[],[f222]) ).
fof(f950,plain,
! [X0] :
( member_succeeds(p(sK236(X0)),X0)
| ~ literal_list_succeeds(X0)
| interpretation_succeeds(X0) ),
inference(cnf_transformation,[],[f222]) ).
fof(f962,plain,
! [X2,X0,X1] :
( ~ true_succeeds(X0,X1,X2)
| ~ interpretation_succeeds(X1)
| interpretation_succeeds(X2) ),
inference(cnf_transformation,[],[f233]) ).
fof(f965,plain,
! [X2,X0,X1] :
( ~ false_succeeds(X0,X1,X2)
| ~ literal_list_succeeds(X1)
| literal_list_succeeds(X2) ),
inference(cnf_transformation,[],[f239]) ).
fof(f978,plain,
! [X2,X3,X0,X1] :
( ~ eval_succeeds(X0,X1,X3)
| ~ sub(X1,X2)
| eval_succeeds(X0,X2,X3) ),
inference(cnf_transformation,[],[f257]) ).
fof(f982,plain,
! [X2,X3,X0,X1] :
( ~ eval_succeeds(X0,X1,X3)
| ~ interpretation_succeeds(X1)
| ~ eval_succeeds(X0,X1,X2)
| X2 = X3 ),
inference(cnf_transformation,[],[f262]) ).
fof(f991,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ interpretation_succeeds(X1)
| ~ sub(X5,X1)
| ~ literal_list_succeeds(X5)
| '0' != '0'
| false_succeeds(X3,X5,sK288(X1,X3,X5))
| ~ sP266(X4,X3,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f992,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ interpretation_succeeds(X1)
| ~ sub(X5,X1)
| ~ literal_list_succeeds(X5)
| '0' != '0'
| sub(sK288(X1,X3,X5),X1)
| ~ sP266(X4,X3,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f995,plain,
! [X2,X3,X0,X1,X8,X4] :
( ~ interpretation_succeeds(X1)
| ~ sub(X8,X1)
| ~ literal_list_succeeds(X8)
| '0' != '0'
| false_succeeds(X4,X8,sK286(X1,X4,X8))
| ~ sP266(X4,X3,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f996,plain,
! [X2,X3,X0,X1,X8,X4] :
( ~ interpretation_succeeds(X1)
| ~ sub(X8,X1)
| ~ literal_list_succeeds(X8)
| '0' != '0'
| sub(sK286(X1,X4,X8),X1)
| ~ sP266(X4,X3,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f997,plain,
! [X2,X0,X11,X1,X12,X13] :
( ~ interpretation_succeeds(X1)
| ~ sub(X13,X1)
| ~ literal_list_succeeds(X13)
| '1' != '1'
| true_succeeds(X12,X13,sK285(X1,X12,X13))
| ~ sP265(X12,X11,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f998,plain,
! [X2,X0,X11,X1,X12,X13] :
( ~ interpretation_succeeds(X1)
| ~ sub(X13,X1)
| ~ literal_list_succeeds(X13)
| '1' != '1'
| sub(sK285(X1,X12,X13),X1)
| ~ sP265(X12,X11,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1001,plain,
! [X2,X0,X1,X18,X16,X17] :
( ~ interpretation_succeeds(X1)
| ~ sub(X18,X1)
| ~ literal_list_succeeds(X18)
| '1' != '1'
| true_succeeds(X16,X18,sK283(X1,X16,X18))
| ~ sP264(X17,X16,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1002,plain,
! [X2,X0,X1,X18,X16,X17] :
( ~ interpretation_succeeds(X1)
| ~ sub(X18,X1)
| ~ literal_list_succeeds(X18)
| '1' != '1'
| sub(sK283(X1,X16,X18),X1)
| ~ sP264(X17,X16,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1007,plain,
! [X2,X21,X0,X1,X22,X23] :
( ~ interpretation_succeeds(X1)
| ~ sub(X23,X1)
| ~ literal_list_succeeds(X23)
| '0' != '0'
| false_succeeds(X22,X23,sK280(X1,X22,X23))
| ~ sP263(X22,X21,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1008,plain,
! [X2,X21,X0,X1,X22,X23] :
( ~ interpretation_succeeds(X1)
| ~ sub(X23,X1)
| ~ literal_list_succeeds(X23)
| '0' != '0'
| sub(sK280(X1,X22,X23),X1)
| ~ sP263(X22,X21,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1011,plain,
! [X2,X28,X0,X1,X26,X27] :
( ~ interpretation_succeeds(X1)
| ~ sub(X28,X1)
| ~ literal_list_succeeds(X28)
| '0' != '0'
| false_succeeds(X26,X28,sK278(X1,X26,X28))
| ~ sP262(X27,X26,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1012,plain,
! [X2,X28,X0,X1,X26,X27] :
( ~ interpretation_succeeds(X1)
| ~ sub(X28,X1)
| ~ literal_list_succeeds(X28)
| '0' != '0'
| sub(sK278(X1,X26,X28),X1)
| ~ sP262(X27,X26,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1013,plain,
! [X31,X2,X0,X1,X32,X33] :
( ~ interpretation_succeeds(X1)
| ~ sub(X33,X1)
| ~ literal_list_succeeds(X33)
| '1' != '1'
| true_succeeds(X31,X33,sK277(X1,X31,X33))
| ~ sP261(X32,X31,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1014,plain,
! [X31,X2,X0,X1,X32,X33] :
( ~ interpretation_succeeds(X1)
| ~ sub(X33,X1)
| ~ literal_list_succeeds(X33)
| '1' != '1'
| sub(sK277(X1,X31,X33),X1)
| ~ sP261(X32,X31,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1017,plain,
! [X31,X2,X0,X36,X1,X32] :
( ~ interpretation_succeeds(X1)
| ~ sub(X36,X1)
| ~ literal_list_succeeds(X36)
| '1' != '1'
| true_succeeds(X32,X36,sK275(X1,X32,X36))
| ~ sP261(X32,X31,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1018,plain,
! [X31,X2,X0,X36,X1,X32] :
( ~ interpretation_succeeds(X1)
| ~ sub(X36,X1)
| ~ literal_list_succeeds(X36)
| '1' != '1'
| sub(sK275(X1,X32,X36),X1)
| ~ sP261(X32,X31,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1021,plain,
! [X40,X2,X39,X0,X1] :
( ~ interpretation_succeeds(X1)
| ~ sub(X40,X1)
| ~ literal_list_succeeds(X40)
| '1' != '1'
| true_succeeds(X39,X40,sK273(X1,X39,X40))
| ~ sP260(X39,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1022,plain,
! [X40,X2,X39,X0,X1] :
( ~ interpretation_succeeds(X1)
| ~ sub(X40,X1)
| ~ literal_list_succeeds(X40)
| '1' != '1'
| sub(sK273(X1,X39,X40),X1)
| ~ sP260(X39,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1027,plain,
! [X2,X0,X1,X44,X43] :
( ~ interpretation_succeeds(X1)
| ~ sub(X44,X1)
| ~ literal_list_succeeds(X44)
| '0' != '0'
| false_succeeds(X43,X44,sK270(X1,X43,X44))
| ~ sP259(X43,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1028,plain,
! [X2,X0,X1,X44,X43] :
( ~ interpretation_succeeds(X1)
| ~ sub(X44,X1)
| ~ literal_list_succeeds(X44)
| '0' != '0'
| sub(sK270(X1,X43,X44),X1)
| ~ sP259(X43,X2,X1,X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1029,plain,
! [X54,X55,X52,X53] :
( '1' != X54
| true_succeeds(X52,X55,sK269(X52,X53,X55))
| ~ sP267(X55,X54,X53,X52) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1030,plain,
! [X54,X55,X52,X53] :
( '1' != X54
| sub(sK269(X52,X53,X55),X53)
| ~ sP267(X55,X54,X53,X52) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1031,plain,
! [X54,X55,X52,X53] :
( '0' != X54
| false_succeeds(X52,X55,sK268(X52,X53,X55))
| ~ sP267(X55,X54,X53,X52) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1032,plain,
! [X54,X55,X52,X53] :
( '0' != X54
| sub(sK268(X52,X53,X55),X53)
| ~ sP267(X55,X54,X53,X52) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1033,plain,
! [X50,X54,X55,X52,X53] :
( '0' = sK241
| ~ true_succeeds(sK239,sK242,X50)
| ~ sub(X50,sK240)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1035,plain,
! [X51,X54,X55,X52,X53] :
( ~ false_succeeds(sK239,sK242,X51)
| ~ sub(X51,sK240)
| '1' = sK241
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1036,plain,
! [X54,X55,X52,X53] :
( '0' = sK241
| '1' = sK241
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1039,plain,
! [X2,X3,X0,X1,X4] :
( ~ sP266(X4,X3,X2,X1,X0)
| '0' = X2 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1040,plain,
! [X2,X3,X0,X1,X4] :
( ~ sP266(X4,X3,X2,X1,X0)
| or(X3,X4) = X0 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1042,plain,
! [X2,X0,X11,X1,X12] :
( ~ sP265(X12,X11,X2,X1,X0)
| '1' = X2 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1043,plain,
! [X2,X0,X11,X1,X12] :
( ~ sP265(X12,X11,X2,X1,X0)
| or(X11,X12) = X0 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1045,plain,
! [X2,X0,X1,X16,X17] :
( ~ sP264(X17,X16,X2,X1,X0)
| '1' = X2 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1046,plain,
! [X2,X0,X1,X16,X17] :
( ~ sP264(X17,X16,X2,X1,X0)
| or(X16,X17) = X0 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1048,plain,
! [X2,X21,X0,X1,X22] :
( ~ sP263(X22,X21,X2,X1,X0)
| '0' = X2 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1049,plain,
! [X2,X21,X0,X1,X22] :
( ~ sP263(X22,X21,X2,X1,X0)
| and(X21,X22) = X0 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1051,plain,
! [X2,X0,X1,X26,X27] :
( ~ sP262(X27,X26,X2,X1,X0)
| '0' = X2 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1052,plain,
! [X2,X0,X1,X26,X27] :
( ~ sP262(X27,X26,X2,X1,X0)
| and(X26,X27) = X0 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1055,plain,
! [X31,X2,X0,X1,X32] :
( ~ sP261(X32,X31,X2,X1,X0)
| '1' = X2 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1056,plain,
! [X31,X2,X0,X1,X32] :
( ~ sP261(X32,X31,X2,X1,X0)
| and(X31,X32) = X0 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1058,plain,
! [X2,X39,X0,X1] :
( ~ sP260(X39,X2,X1,X0)
| '0' = X2 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1059,plain,
! [X2,X39,X0,X1] :
( ~ sP260(X39,X2,X1,X0)
| neg(X39) = X0 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1061,plain,
! [X2,X0,X1,X43] :
( ~ sP259(X43,X2,X1,X0)
| '1' = X2 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1062,plain,
! [X2,X0,X1,X43] :
( ~ sP259(X43,X2,X1,X0)
| neg(X43) = X0 ),
inference(cnf_transformation,[],[f268]) ).
fof(f1064,plain,
! [X54,X55,X52,X53] :
( sK239 = p(sK243)
| '0' = sK241
| sP259(sK245,sK241,sK240,sK239)
| sP260(sK246,sK241,sK240,sK239)
| sP261(sK248,sK247,sK241,sK240,sK239)
| sP262(sK250,sK249,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1066,plain,
! [X54,X55,X52,X53] :
( '1' = sK241
| member_succeeds(neg(p(sK244)),sK240)
| sP259(sK245,sK241,sK240,sK239)
| sP260(sK246,sK241,sK240,sK239)
| sP261(sK248,sK247,sK241,sK240,sK239)
| sP262(sK250,sK249,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1068,plain,
! [X54,X55,X52,X53] :
( '1' = sK241
| sK239 = p(sK244)
| sP259(sK245,sK241,sK240,sK239)
| sP260(sK246,sK241,sK240,sK239)
| sP261(sK248,sK247,sK241,sK240,sK239)
| sP262(sK250,sK249,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1070,plain,
! [X54,X55,X52,X53] :
( member_succeeds(p(sK243),sK240)
| '0' = sK241
| sP259(sK245,sK241,sK240,sK239)
| sP260(sK246,sK241,sK240,sK239)
| sP261(sK248,sK247,sK241,sK240,sK239)
| sP262(sK250,sK249,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1072,plain,
! [X54,X55,X52,X53] :
( interpretation_succeeds(sK240)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1073,plain,
! [X54,X55,X52,X53] :
( literal_list_succeeds(sK242)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1074,plain,
! [X54,X55,X52,X53] :
( sub(sK242,sK240)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(cnf_transformation,[],[f268]) ).
fof(f1075,plain,
! [X4] :
( '0' = sK292
| ~ true_succeeds(sK290,sK293,X4)
| ~ sub(X4,sK291) ),
inference(cnf_transformation,[],[f270]) ).
fof(f1076,plain,
! [X4,X5] :
( ~ false_succeeds(sK290,sK293,X5)
| ~ sub(X5,sK291)
| ~ true_succeeds(sK290,sK293,X4)
| ~ sub(X4,sK291) ),
inference(cnf_transformation,[],[f270]) ).
fof(f1077,plain,
! [X5] :
( ~ false_succeeds(sK290,sK293,X5)
| ~ sub(X5,sK291)
| '1' = sK292 ),
inference(cnf_transformation,[],[f270]) ).
fof(f1079,plain,
sub(sK293,sK291),
inference(cnf_transformation,[],[f270]) ).
fof(f1080,plain,
literal_list_succeeds(sK293),
inference(cnf_transformation,[],[f270]) ).
fof(f1081,plain,
eval_succeeds(sK290,sK291,sK292),
inference(cnf_transformation,[],[f270]) ).
fof(f1082,plain,
interpretation_succeeds(sK291),
inference(cnf_transformation,[],[f270]) ).
fof(f1100,plain,
! [X0,X18,X1] :
( ~ member_succeeds(p(X18),X1)
| p(X18) != X0
| eval_succeeds(X0,X1,'1') ),
inference(equality_resolution,[],[f464]) ).
fof(f1101,plain,
! [X18,X1] :
( eval_succeeds(p(X18),X1,'1')
| ~ member_succeeds(p(X18),X1) ),
inference(equality_resolution,[],[f1100]) ).
fof(f1102,plain,
! [X0,X1,X17] :
( ~ member_succeeds(neg(p(X17)),X1)
| p(X17) != X0
| eval_succeeds(X0,X1,'0') ),
inference(equality_resolution,[],[f454]) ).
fof(f1103,plain,
! [X1,X17] :
( ~ member_succeeds(neg(p(X17)),X1)
| eval_succeeds(p(X17),X1,'0') ),
inference(equality_resolution,[],[f1102]) ).
fof(f1167,plain,
! [X0,X11,X1] :
( ~ member_fails(p(X11),X1)
| p(X11) != X0
| false_succeeds(X0,X1,cons(neg(p(X11)),X1)) ),
inference(equality_resolution,[],[f632]) ).
fof(f1168,plain,
! [X11,X1] :
( false_succeeds(p(X11),X1,cons(neg(p(X11)),X1))
| ~ member_fails(p(X11),X1) ),
inference(equality_resolution,[],[f1167]) ).
fof(f1169,plain,
! [X2,X10,X1] :
( false_succeeds(neg(X10),X1,X2)
| ~ true_succeeds(X10,X1,X2) ),
inference(equality_resolution,[],[f631]) ).
fof(f1170,plain,
! [X2,X1,X8,X9] :
( false_succeeds(and(X8,X9),X1,X2)
| ~ false_succeeds(X8,X1,X2) ),
inference(equality_resolution,[],[f618]) ).
fof(f1171,plain,
! [X2,X1,X6,X7] :
( sP122(X7,X6,X2,X1,and(X6,X7))
| ~ false_succeeds(X7,X1,X2) ),
inference(equality_resolution,[],[f615]) ).
fof(f1172,plain,
! [X2,X3,X1,X4,X5] :
( sP123(X5,X4,X3,X2,X1,or(X3,X4))
| ~ false_succeeds(X3,X1,X5)
| ~ false_succeeds(X4,X5,X2) ),
inference(equality_resolution,[],[f611]) ).
fof(f1191,plain,
! [X0,X11,X1] :
( ~ member_fails(neg(p(X11)),X1)
| p(X11) != X0
| true_succeeds(X0,X1,cons(p(X11),X1)) ),
inference(equality_resolution,[],[f720]) ).
fof(f1192,plain,
! [X11,X1] :
( true_succeeds(p(X11),X1,cons(p(X11),X1))
| ~ member_fails(neg(p(X11)),X1) ),
inference(equality_resolution,[],[f1191]) ).
fof(f1193,plain,
! [X2,X10,X1] :
( true_succeeds(neg(X10),X1,X2)
| ~ false_succeeds(X10,X1,X2) ),
inference(equality_resolution,[],[f719]) ).
fof(f1194,plain,
! [X2,X1,X8,X9,X7] :
( true_succeeds(and(X7,X8),X1,X2)
| ~ true_succeeds(X7,X1,X9)
| ~ true_succeeds(X8,X9,X2) ),
inference(equality_resolution,[],[f700]) ).
fof(f1195,plain,
! [X2,X1,X6,X5] :
( sP159(X6,X5,X2,X1,or(X5,X6))
| ~ true_succeeds(X5,X1,X2) ),
inference(equality_resolution,[],[f697]) ).
fof(f1196,plain,
! [X2,X3,X1,X4] :
( sP160(X4,X3,X2,X1,or(X3,X4))
| ~ true_succeeds(X4,X1,X2) ),
inference(equality_resolution,[],[f694]) ).
fof(f1222,plain,
! [X2] : literal_succeeds(p(X2)),
inference(equality_resolution,[],[f839]) ).
fof(f1224,plain,
! [X2] : ~ literal_fails(p(X2)),
inference(equality_resolution,[],[f841]) ).
fof(f1248,plain,
! [X55,X52,X53] :
( sub(sK268(X52,X53,X55),X53)
| ~ sP267(X55,'0',X53,X52) ),
inference(equality_resolution,[],[f1032]) ).
fof(f1249,plain,
! [X55,X52,X53] :
( false_succeeds(X52,X55,sK268(X52,X53,X55))
| ~ sP267(X55,'0',X53,X52) ),
inference(equality_resolution,[],[f1031]) ).
fof(f1250,plain,
! [X55,X52,X53] :
( sub(sK269(X52,X53,X55),X53)
| ~ sP267(X55,'1',X53,X52) ),
inference(equality_resolution,[],[f1030]) ).
fof(f1251,plain,
! [X55,X52,X53] :
( true_succeeds(X52,X55,sK269(X52,X53,X55))
| ~ sP267(X55,'1',X53,X52) ),
inference(equality_resolution,[],[f1029]) ).
fof(f1252,plain,
! [X2,X3,X0,X1,X4,X5] :
( false_succeeds(X3,X5,sK288(X1,X3,X5))
| ~ sub(X5,X1)
| ~ literal_list_succeeds(X5)
| ~ interpretation_succeeds(X1)
| ~ sP266(X4,X3,X2,X1,X0) ),
inference(trivial_inequality_removal,[],[f991]) ).
fof(f1253,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sP266(X4,X3,X2,X1,X0)
| ~ sub(X5,X1)
| ~ literal_list_succeeds(X5)
| sub(sK288(X1,X3,X5),X1)
| ~ interpretation_succeeds(X1) ),
inference(trivial_inequality_removal,[],[f992]) ).
fof(f1254,plain,
! [X2,X3,X0,X1,X8,X4] :
( false_succeeds(X4,X8,sK286(X1,X4,X8))
| ~ sub(X8,X1)
| ~ literal_list_succeeds(X8)
| ~ interpretation_succeeds(X1)
| ~ sP266(X4,X3,X2,X1,X0) ),
inference(trivial_inequality_removal,[],[f995]) ).
fof(f1255,plain,
! [X2,X3,X0,X1,X8,X4] :
( ~ sP266(X4,X3,X2,X1,X0)
| ~ sub(X8,X1)
| ~ literal_list_succeeds(X8)
| sub(sK286(X1,X4,X8),X1)
| ~ interpretation_succeeds(X1) ),
inference(trivial_inequality_removal,[],[f996]) ).
fof(f1256,plain,
! [X2,X0,X11,X1,X12,X13] :
( true_succeeds(X12,X13,sK285(X1,X12,X13))
| ~ sub(X13,X1)
| ~ literal_list_succeeds(X13)
| ~ interpretation_succeeds(X1)
| ~ sP265(X12,X11,X2,X1,X0) ),
inference(trivial_inequality_removal,[],[f997]) ).
fof(f1257,plain,
! [X2,X0,X11,X1,X12,X13] :
( ~ sP265(X12,X11,X2,X1,X0)
| ~ sub(X13,X1)
| ~ literal_list_succeeds(X13)
| sub(sK285(X1,X12,X13),X1)
| ~ interpretation_succeeds(X1) ),
inference(trivial_inequality_removal,[],[f998]) ).
fof(f1258,plain,
! [X2,X0,X18,X1,X16,X17] :
( true_succeeds(X16,X18,sK283(X1,X16,X18))
| ~ sub(X18,X1)
| ~ literal_list_succeeds(X18)
| ~ interpretation_succeeds(X1)
| ~ sP264(X17,X16,X2,X1,X0) ),
inference(trivial_inequality_removal,[],[f1001]) ).
fof(f1259,plain,
! [X2,X0,X1,X18,X16,X17] :
( ~ sP264(X17,X16,X2,X1,X0)
| ~ sub(X18,X1)
| ~ literal_list_succeeds(X18)
| sub(sK283(X1,X16,X18),X1)
| ~ interpretation_succeeds(X1) ),
inference(trivial_inequality_removal,[],[f1002]) ).
fof(f1260,plain,
! [X2,X21,X0,X1,X22,X23] :
( false_succeeds(X22,X23,sK280(X1,X22,X23))
| ~ sub(X23,X1)
| ~ literal_list_succeeds(X23)
| ~ interpretation_succeeds(X1)
| ~ sP263(X22,X21,X2,X1,X0) ),
inference(trivial_inequality_removal,[],[f1007]) ).
fof(f1261,plain,
! [X2,X21,X0,X1,X22,X23] :
( ~ sP263(X22,X21,X2,X1,X0)
| ~ sub(X23,X1)
| ~ literal_list_succeeds(X23)
| sub(sK280(X1,X22,X23),X1)
| ~ interpretation_succeeds(X1) ),
inference(trivial_inequality_removal,[],[f1008]) ).
fof(f1262,plain,
! [X2,X28,X0,X1,X26,X27] :
( false_succeeds(X26,X28,sK278(X1,X26,X28))
| ~ sub(X28,X1)
| ~ literal_list_succeeds(X28)
| ~ interpretation_succeeds(X1)
| ~ sP262(X27,X26,X2,X1,X0) ),
inference(trivial_inequality_removal,[],[f1011]) ).
fof(f1263,plain,
! [X2,X28,X0,X1,X26,X27] :
( ~ sP262(X27,X26,X2,X1,X0)
| ~ sub(X28,X1)
| ~ literal_list_succeeds(X28)
| sub(sK278(X1,X26,X28),X1)
| ~ interpretation_succeeds(X1) ),
inference(trivial_inequality_removal,[],[f1012]) ).
fof(f1264,plain,
! [X31,X2,X0,X1,X32,X33] :
( true_succeeds(X31,X33,sK277(X1,X31,X33))
| ~ sub(X33,X1)
| ~ literal_list_succeeds(X33)
| ~ interpretation_succeeds(X1)
| ~ sP261(X32,X31,X2,X1,X0) ),
inference(trivial_inequality_removal,[],[f1013]) ).
fof(f1265,plain,
! [X31,X2,X0,X1,X32,X33] :
( ~ sP261(X32,X31,X2,X1,X0)
| ~ sub(X33,X1)
| ~ literal_list_succeeds(X33)
| sub(sK277(X1,X31,X33),X1)
| ~ interpretation_succeeds(X1) ),
inference(trivial_inequality_removal,[],[f1014]) ).
fof(f1266,plain,
! [X31,X2,X0,X36,X1,X32] :
( true_succeeds(X32,X36,sK275(X1,X32,X36))
| ~ sub(X36,X1)
| ~ literal_list_succeeds(X36)
| ~ interpretation_succeeds(X1)
| ~ sP261(X32,X31,X2,X1,X0) ),
inference(trivial_inequality_removal,[],[f1017]) ).
fof(f1267,plain,
! [X31,X2,X0,X36,X1,X32] :
( ~ sP261(X32,X31,X2,X1,X0)
| ~ sub(X36,X1)
| ~ literal_list_succeeds(X36)
| sub(sK275(X1,X32,X36),X1)
| ~ interpretation_succeeds(X1) ),
inference(trivial_inequality_removal,[],[f1018]) ).
fof(f1268,plain,
! [X40,X2,X39,X0,X1] :
( true_succeeds(X39,X40,sK273(X1,X39,X40))
| ~ sub(X40,X1)
| ~ literal_list_succeeds(X40)
| ~ interpretation_succeeds(X1)
| ~ sP260(X39,X2,X1,X0) ),
inference(trivial_inequality_removal,[],[f1021]) ).
fof(f1269,plain,
! [X40,X2,X39,X0,X1] :
( sub(sK273(X1,X39,X40),X1)
| ~ sub(X40,X1)
| ~ literal_list_succeeds(X40)
| ~ interpretation_succeeds(X1)
| ~ sP260(X39,X2,X1,X0) ),
inference(trivial_inequality_removal,[],[f1022]) ).
fof(f1270,plain,
! [X2,X0,X1,X44,X43] :
( false_succeeds(X43,X44,sK270(X1,X43,X44))
| ~ sub(X44,X1)
| ~ literal_list_succeeds(X44)
| ~ interpretation_succeeds(X1)
| ~ sP259(X43,X2,X1,X0) ),
inference(trivial_inequality_removal,[],[f1027]) ).
fof(f1271,plain,
! [X2,X0,X1,X44,X43] :
( sub(sK270(X1,X43,X44),X1)
| ~ sub(X44,X1)
| ~ literal_list_succeeds(X44)
| ~ interpretation_succeeds(X1)
| ~ sP259(X43,X2,X1,X0) ),
inference(trivial_inequality_removal,[],[f1028]) ).
fof(f1272,plain,
! [X54,X55,X52,X53] :
( sK239 = p(sK243)
| '0' = sK241
| sP259(sK245,sK241,sK240,sK239)
| sP261(sK248,sK247,sK241,sK240,sK239)
| sP262(sK250,sK249,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1064,f1058]) ).
fof(f1273,plain,
! [X54,X55,X52,X53] :
( '1' = sK241
| member_succeeds(neg(p(sK244)),sK240)
| sP260(sK246,sK241,sK240,sK239)
| sP261(sK248,sK247,sK241,sK240,sK239)
| sP262(sK250,sK249,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1066,f1061]) ).
fof(f1275,plain,
! [X54,X55,X52,X53] :
( '1' = sK241
| sK239 = p(sK244)
| sP260(sK246,sK241,sK240,sK239)
| sP261(sK248,sK247,sK241,sK240,sK239)
| sP262(sK250,sK249,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1068,f1061]) ).
fof(f1276,plain,
! [X54,X55,X52,X53] :
( member_succeeds(p(sK243),sK240)
| '0' = sK241
| sP259(sK245,sK241,sK240,sK239)
| sP261(sK248,sK247,sK241,sK240,sK239)
| sP262(sK250,sK249,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1070,f1058]) ).
fof(f1352,plain,
! [X2,X0,X1] :
( '1' = X2
| '0' = X2
| sP47(sK33(X0,X1,X2),X2,X1,X0)
| sP48(sK35(X0,X1,X2),sK34(X0,X1,X2),X2,X1,X0)
| sP49(sK37(X0,X1,X2),sK36(X0,X1,X2),X2,X1,X0)
| sP50(sK39(X0,X1,X2),sK38(X0,X1,X2),X2,X1,X0)
| sP51(sK41(X0,X1,X2),sK40(X0,X1,X2),X2,X1,X0)
| sP52(sK43(X0,X1,X2),sK42(X0,X1,X2),X2,X1,X0)
| sP53(sK45(X0,X1,X2),sK44(X0,X1,X2),X2,X1,X0)
| ~ eval_succeeds(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f459,f452]) ).
fof(f1364,plain,
! [X54,X55,X52,X53] :
( sK239 = p(sK243)
| '0' = sK241
| sP259(sK245,sK241,sK240,sK239)
| sP261(sK248,sK247,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1272,f1051]) ).
fof(f1365,plain,
! [X54,X55,X52,X53] :
( '1' = sK241
| member_succeeds(neg(p(sK244)),sK240)
| sP260(sK246,sK241,sK240,sK239)
| sP262(sK250,sK249,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1273,f1055]) ).
fof(f1367,plain,
! [X54,X55,X52,X53] :
( '1' = sK241
| sK239 = p(sK244)
| sP260(sK246,sK241,sK240,sK239)
| sP262(sK250,sK249,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1275,f1055]) ).
fof(f1368,plain,
! [X54,X55,X52,X53] :
( member_succeeds(p(sK243),sK240)
| '0' = sK241
| sP259(sK245,sK241,sK240,sK239)
| sP261(sK248,sK247,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1276,f1051]) ).
fof(f1424,plain,
! [X2,X0,X1] :
( '1' = X2
| '0' = X2
| sP47(sK33(X0,X1,X2),X2,X1,X0)
| sP49(sK37(X0,X1,X2),sK36(X0,X1,X2),X2,X1,X0)
| sP50(sK39(X0,X1,X2),sK38(X0,X1,X2),X2,X1,X0)
| sP51(sK41(X0,X1,X2),sK40(X0,X1,X2),X2,X1,X0)
| sP52(sK43(X0,X1,X2),sK42(X0,X1,X2),X2,X1,X0)
| sP53(sK45(X0,X1,X2),sK44(X0,X1,X2),X2,X1,X0)
| ~ eval_succeeds(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f1352,f444]) ).
fof(f1435,plain,
! [X54,X55,X52,X53] :
( sK239 = p(sK243)
| '0' = sK241
| sP259(sK245,sK241,sK240,sK239)
| sP261(sK248,sK247,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1364,f1048]) ).
fof(f1436,plain,
! [X54,X55,X52,X53] :
( '1' = sK241
| member_succeeds(neg(p(sK244)),sK240)
| sP260(sK246,sK241,sK240,sK239)
| sP262(sK250,sK249,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1365,f1045]) ).
fof(f1438,plain,
! [X54,X55,X52,X53] :
( '1' = sK241
| sK239 = p(sK244)
| sP260(sK246,sK241,sK240,sK239)
| sP262(sK250,sK249,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1367,f1045]) ).
fof(f1439,plain,
! [X54,X55,X52,X53] :
( member_succeeds(p(sK243),sK240)
| '0' = sK241
| sP259(sK245,sK241,sK240,sK239)
| sP261(sK248,sK247,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1368,f1048]) ).
fof(f1495,plain,
! [X2,X0,X1] :
( '1' = X2
| '0' = X2
| sP47(sK33(X0,X1,X2),X2,X1,X0)
| sP49(sK37(X0,X1,X2),sK36(X0,X1,X2),X2,X1,X0)
| sP50(sK39(X0,X1,X2),sK38(X0,X1,X2),X2,X1,X0)
| sP52(sK43(X0,X1,X2),sK42(X0,X1,X2),X2,X1,X0)
| sP53(sK45(X0,X1,X2),sK44(X0,X1,X2),X2,X1,X0)
| ~ eval_succeeds(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f1424,f431]) ).
fof(f1506,plain,
! [X54,X55,X52,X53] :
( sK239 = p(sK243)
| '0' = sK241
| sP259(sK245,sK241,sK240,sK239)
| sP261(sK248,sK247,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1435,f1039]) ).
fof(f1507,plain,
! [X54,X55,X52,X53] :
( '1' = sK241
| member_succeeds(neg(p(sK244)),sK240)
| sP260(sK246,sK241,sK240,sK239)
| sP262(sK250,sK249,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1436,f1042]) ).
fof(f1509,plain,
! [X54,X55,X52,X53] :
( '1' = sK241
| sK239 = p(sK244)
| sP260(sK246,sK241,sK240,sK239)
| sP262(sK250,sK249,sK241,sK240,sK239)
| sP263(sK252,sK251,sK241,sK240,sK239)
| sP266(sK258,sK257,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1438,f1042]) ).
fof(f1510,plain,
! [X54,X55,X52,X53] :
( member_succeeds(p(sK243),sK240)
| '0' = sK241
| sP259(sK245,sK241,sK240,sK239)
| sP261(sK248,sK247,sK241,sK240,sK239)
| sP264(sK254,sK253,sK241,sK240,sK239)
| sP265(sK256,sK255,sK241,sK240,sK239)
| ~ eval_succeeds(X52,X53,X54)
| ~ interpretation_succeeds(X53)
| ~ sub(X55,X53)
| ~ literal_list_succeeds(X55)
| sP267(X55,X54,X53,X52) ),
inference(forward_subsumption_resolution,[],[f1439,f1039]) ).
fof(f1556,plain,
! [X2,X0,X1] :
( '1' = X2
| '0' = X2
| sP47(sK33(X0,X1,X2),X2,X1,X0)
| sP49(sK37(X0,X1,X2),sK36(X0,X1,X2),X2,X1,X0)
| sP50(sK39(X0,X1,X2),sK38(X0,X1,X2),X2,X1,X0)
| sP53(sK45(X0,X1,X2),sK44(X0,X1,X2),X2,X1,X0)
| ~ eval_succeeds(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f1495,f427]) ).
fof(f1578,plain,
! [X2,X0,X1] :
( '1' = X2
| '0' = X2
| sP49(sK37(X0,X1,X2),sK36(X0,X1,X2),X2,X1,X0)
| sP50(sK39(X0,X1,X2),sK38(X0,X1,X2),X2,X1,X0)
| sP53(sK45(X0,X1,X2),sK44(X0,X1,X2),X2,X1,X0)
| ~ eval_succeeds(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f1556,f448]) ).
fof(f1598,plain,
! [X2,X0,X1] :
( '1' = X2
| '0' = X2
| sP50(sK39(X0,X1,X2),sK38(X0,X1,X2),X2,X1,X0)
| sP53(sK45(X0,X1,X2),sK44(X0,X1,X2),X2,X1,X0)
| ~ eval_succeeds(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f1578,f439]) ).
fof(f1618,plain,
! [X2,X0,X1] :
( '1' = X2
| '0' = X2
| sP53(sK45(X0,X1,X2),sK44(X0,X1,X2),X2,X1,X0)
| ~ eval_succeeds(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f1598,f435]) ).
fof(f1638,plain,
! [X2,X0,X1] :
( ~ eval_succeeds(X0,X1,X2)
| '0' = X2
| '1' = X2 ),
inference(forward_subsumption_resolution,[],[f1618,f423]) ).
fof(f1718,definition,
( spl294_1
<=> ! [X4] :
( ~ true_succeeds(sK290,sK293,X4)
| ~ sub(X4,sK291) ) ),
introduced(definition,[new_symbols(definition,[spl294_1])],[avatar_definition]) ).
fof(f1719,plain,
( ! [X4] :
( ~ true_succeeds(sK290,sK293,X4)
| ~ sub(X4,sK291) )
| ~ spl294_1 ),
inference(avatar_component_clause,[],[f1718]) ).
fof(f1721,definition,
( spl294_2
<=> ! [X5] :
( ~ false_succeeds(sK290,sK293,X5)
| ~ sub(X5,sK291) ) ),
introduced(definition,[new_symbols(definition,[spl294_2])],[avatar_definition]) ).
fof(f1722,plain,
( ! [X5] :
( ~ false_succeeds(sK290,sK293,X5)
| ~ sub(X5,sK291) )
| ~ spl294_2 ),
inference(avatar_component_clause,[],[f1721]) ).
fof(f1723,plain,
( spl294_1
| spl294_2 ),
inference(avatar_split_clause,[],[f1076,f1721,f1718]) ).
fof(f1727,definition,
( spl294_3
<=> '1' = sK292 ),
introduced(definition,[new_symbols(definition,[spl294_3])],[avatar_definition]) ).
fof(f1728,plain,
( '1' = sK292
| ~ spl294_3 ),
inference(avatar_component_clause,[],[f1727]) ).
fof(f1729,plain,
( spl294_3
| spl294_2 ),
inference(avatar_split_clause,[],[f1077,f1721,f1727]) ).
fof(f1731,definition,
( spl294_4
<=> '0' = sK292 ),
introduced(definition,[new_symbols(definition,[spl294_4])],[avatar_definition]) ).
fof(f1732,plain,
( '0' = sK292
| ~ spl294_4 ),
inference(avatar_component_clause,[],[f1731]) ).
fof(f1733,plain,
( spl294_1
| spl294_4 ),
inference(avatar_split_clause,[],[f1075,f1731,f1718]) ).
fof(f1741,plain,
( '0' = sK292
| '1' = sK292 ),
inference(resolution,[],[f1638,f1081]) ).
fof(f1746,definition,
( spl294_5
<=> ! [X55,X54,X53,X52] :
( ~ eval_succeeds(X52,X53,X54)
| sP267(X55,X54,X53,X52)
| ~ literal_list_succeeds(X55)
| ~ sub(X55,X53)
| ~ interpretation_succeeds(X53) ) ),
introduced(definition,[new_symbols(definition,[spl294_5])],[avatar_definition]) ).
fof(f1747,plain,
( ! [X54,X55,X52,X53] :
( sP267(X55,X54,X53,X52)
| ~ eval_succeeds(X52,X53,X54)
| ~ literal_list_succeeds(X55)
| ~ sub(X55,X53)
| ~ interpretation_succeeds(X53) )
| ~ spl294_5 ),
inference(avatar_component_clause,[],[f1746]) ).
fof(f1749,definition,
( spl294_6
<=> literal_list_succeeds(sK242) ),
introduced(definition,[new_symbols(definition,[spl294_6])],[avatar_definition]) ).
fof(f1750,plain,
( literal_list_succeeds(sK242)
| ~ spl294_6 ),
inference(avatar_component_clause,[],[f1749]) ).
fof(f1751,plain,
( spl294_5
| spl294_6 ),
inference(avatar_split_clause,[],[f1073,f1749,f1746]) ).
fof(f1753,definition,
( spl294_7
<=> interpretation_succeeds(sK240) ),
introduced(definition,[new_symbols(definition,[spl294_7])],[avatar_definition]) ).
fof(f1754,plain,
( interpretation_succeeds(sK240)
| ~ spl294_7 ),
inference(avatar_component_clause,[],[f1753]) ).
fof(f1755,plain,
( spl294_5
| spl294_7 ),
inference(avatar_split_clause,[],[f1072,f1753,f1746]) ).
fof(f1770,definition,
( spl294_8
<=> sub(sK242,sK240) ),
introduced(definition,[new_symbols(definition,[spl294_8])],[avatar_definition]) ).
fof(f1771,plain,
( sub(sK242,sK240)
| ~ spl294_8 ),
inference(avatar_component_clause,[],[f1770]) ).
fof(f1772,plain,
( spl294_5
| spl294_8 ),
inference(avatar_split_clause,[],[f1074,f1770,f1746]) ).
fof(f1778,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ literal_list_succeeds(X0)
| literal_list_succeeds(sK288(X1,X2,X0))
| ~ sub(X0,X1)
| ~ literal_list_succeeds(X0)
| ~ interpretation_succeeds(X1)
| ~ sP266(X3,X2,X4,X1,X5) ),
inference(resolution,[],[f965,f1252]) ).
fof(f1779,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ literal_list_succeeds(X0)
| literal_list_succeeds(sK288(X1,X2,X0))
| ~ sub(X0,X1)
| ~ interpretation_succeeds(X1)
| ~ sP266(X3,X2,X4,X1,X5) ),
inference(duplicate_literal_removal,[],[f1778]) ).
fof(f1811,definition,
( spl294_9
<=> '1' = sK241 ),
introduced(definition,[new_symbols(definition,[spl294_9])],[avatar_definition]) ).
fof(f1812,plain,
( '1' = sK241
| ~ spl294_9 ),
inference(avatar_component_clause,[],[f1811]) ).
fof(f1814,definition,
( spl294_10
<=> '0' = sK241 ),
introduced(definition,[new_symbols(definition,[spl294_10])],[avatar_definition]) ).
fof(f1815,plain,
( '0' = sK241
| ~ spl294_10 ),
inference(avatar_component_clause,[],[f1814]) ).
fof(f1816,plain,
( spl294_5
| spl294_9
| spl294_10 ),
inference(avatar_split_clause,[],[f1036,f1814,f1811,f1746]) ).
fof(f1822,definition,
( spl294_11
<=> '1' = '0' ),
introduced(definition,[new_symbols(definition,[spl294_11])],[avatar_definition]) ).
fof(f1823,plain,
( '1' != '0'
| spl294_11 ),
inference(avatar_component_clause,[],[f1822]) ).
fof(f1847,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ interpretation_succeeds(X0)
| interpretation_succeeds(sK277(X1,X2,X0))
| ~ sub(X0,X1)
| ~ literal_list_succeeds(X0)
| ~ interpretation_succeeds(X1)
| ~ sP261(X3,X2,X4,X1,X5) ),
inference(resolution,[],[f962,f1264]) ).
fof(f1852,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sP261(X3,X2,X4,X1,X5)
| interpretation_succeeds(sK277(X1,X2,X0))
| ~ sub(X0,X1)
| ~ interpretation_succeeds(X1)
| ~ interpretation_succeeds(X0) ),
inference(forward_subsumption_resolution,[],[f1847,f948]) ).
fof(f1889,definition,
( spl294_20
<=> ! [X50] :
( ~ true_succeeds(sK239,sK242,X50)
| ~ sub(X50,sK240) ) ),
introduced(definition,[new_symbols(definition,[spl294_20])],[avatar_definition]) ).
fof(f1890,plain,
( ! [X50] :
( ~ true_succeeds(sK239,sK242,X50)
| ~ sub(X50,sK240) )
| ~ spl294_20 ),
inference(avatar_component_clause,[],[f1889]) ).
fof(f1891,plain,
( spl294_5
| spl294_20
| spl294_10 ),
inference(avatar_split_clause,[],[f1033,f1814,f1889,f1746]) ).
fof(f1909,plain,
( eval_succeeds(sK290,sK291,'1')
| ~ spl294_3 ),
inference(superposition,[],[f1081,f1728]) ).
fof(f1914,plain,
( spl294_3
| spl294_4 ),
inference(avatar_split_clause,[],[f1741,f1731,f1727]) ).
fof(f1929,definition,
( spl294_23
<=> ! [X51] :
( ~ false_succeeds(sK239,sK242,X51)
| ~ sub(X51,sK240) ) ),
introduced(definition,[new_symbols(definition,[spl294_23])],[avatar_definition]) ).
fof(f1930,plain,
( ! [X51] :
( ~ false_succeeds(sK239,sK242,X51)
| ~ sub(X51,sK240) )
| ~ spl294_23 ),
inference(avatar_component_clause,[],[f1929]) ).
fof(f1931,plain,
( spl294_5
| spl294_9
| spl294_23 ),
inference(avatar_split_clause,[],[f1035,f1929,f1811,f1746]) ).
fof(f1951,plain,
( ! [X0] :
( ~ sub(sK269(sK290,X0,sK293),sK291)
| ~ sP267(sK293,'1',X0,sK290) )
| ~ spl294_1 ),
inference(resolution,[],[f1251,f1719]) ).
fof(f2084,plain,
~ spl294_11,
inference(avatar_split_clause,[],[f286,f1822]) ).
fof(f2284,definition,
( spl294_40
<=> sP265(sK256,sK255,sK241,sK240,sK239) ),
introduced(definition,[new_symbols(definition,[spl294_40])],[avatar_definition]) ).
fof(f2285,plain,
( sP265(sK256,sK255,sK241,sK240,sK239)
| ~ spl294_40 ),
inference(avatar_component_clause,[],[f2284]) ).
fof(f2287,definition,
( spl294_41
<=> sP264(sK254,sK253,sK241,sK240,sK239) ),
introduced(definition,[new_symbols(definition,[spl294_41])],[avatar_definition]) ).
fof(f2288,plain,
( sP264(sK254,sK253,sK241,sK240,sK239)
| ~ spl294_41 ),
inference(avatar_component_clause,[],[f2287]) ).
fof(f2290,definition,
( spl294_42
<=> sP261(sK248,sK247,sK241,sK240,sK239) ),
introduced(definition,[new_symbols(definition,[spl294_42])],[avatar_definition]) ).
fof(f2291,plain,
( sP261(sK248,sK247,sK241,sK240,sK239)
| ~ spl294_42 ),
inference(avatar_component_clause,[],[f2290]) ).
fof(f2293,definition,
( spl294_43
<=> sP259(sK245,sK241,sK240,sK239) ),
introduced(definition,[new_symbols(definition,[spl294_43])],[avatar_definition]) ).
fof(f2294,plain,
( sP259(sK245,sK241,sK240,sK239)
| ~ spl294_43 ),
inference(avatar_component_clause,[],[f2293]) ).
fof(f2296,definition,
( spl294_44
<=> sK239 = p(sK243) ),
introduced(definition,[new_symbols(definition,[spl294_44])],[avatar_definition]) ).
fof(f2297,plain,
( sK239 = p(sK243)
| ~ spl294_44 ),
inference(avatar_component_clause,[],[f2296]) ).
fof(f2298,plain,
( spl294_5
| spl294_40
| spl294_41
| spl294_42
| spl294_43
| spl294_10
| spl294_44 ),
inference(avatar_split_clause,[],[f1506,f2296,f1814,f2293,f2290,f2287,f2284,f1746]) ).
fof(f2325,definition,
( spl294_45
<=> sP266(sK258,sK257,sK241,sK240,sK239) ),
introduced(definition,[new_symbols(definition,[spl294_45])],[avatar_definition]) ).
fof(f2326,plain,
( sP266(sK258,sK257,sK241,sK240,sK239)
| ~ spl294_45 ),
inference(avatar_component_clause,[],[f2325]) ).
fof(f2328,definition,
( spl294_46
<=> sP263(sK252,sK251,sK241,sK240,sK239) ),
introduced(definition,[new_symbols(definition,[spl294_46])],[avatar_definition]) ).
fof(f2329,plain,
( sP263(sK252,sK251,sK241,sK240,sK239)
| ~ spl294_46 ),
inference(avatar_component_clause,[],[f2328]) ).
fof(f2331,definition,
( spl294_47
<=> sP262(sK250,sK249,sK241,sK240,sK239) ),
introduced(definition,[new_symbols(definition,[spl294_47])],[avatar_definition]) ).
fof(f2332,plain,
( sP262(sK250,sK249,sK241,sK240,sK239)
| ~ spl294_47 ),
inference(avatar_component_clause,[],[f2331]) ).
fof(f2334,definition,
( spl294_48
<=> sP260(sK246,sK241,sK240,sK239) ),
introduced(definition,[new_symbols(definition,[spl294_48])],[avatar_definition]) ).
fof(f2335,plain,
( sP260(sK246,sK241,sK240,sK239)
| ~ spl294_48 ),
inference(avatar_component_clause,[],[f2334]) ).
fof(f2337,definition,
( spl294_49
<=> sK239 = p(sK244) ),
introduced(definition,[new_symbols(definition,[spl294_49])],[avatar_definition]) ).
fof(f2338,plain,
( sK239 = p(sK244)
| ~ spl294_49 ),
inference(avatar_component_clause,[],[f2337]) ).
fof(f2348,plain,
( spl294_5
| spl294_45
| spl294_46
| spl294_47
| spl294_48
| spl294_49
| spl294_9 ),
inference(avatar_split_clause,[],[f1509,f1811,f2337,f2334,f2331,f2328,f2325,f1746]) ).
fof(f2399,definition,
( spl294_50
<=> member_succeeds(neg(p(sK244)),sK240) ),
introduced(definition,[new_symbols(definition,[spl294_50])],[avatar_definition]) ).
fof(f2400,plain,
( member_succeeds(neg(p(sK244)),sK240)
| ~ spl294_50 ),
inference(avatar_component_clause,[],[f2399]) ).
fof(f2405,plain,
! [X0,X1] :
( p(X1) != X0
| p(sK199(X0)) = X0
| ~ literal_succeeds(X0) ),
inference(superposition,[],[f296,f838]) ).
fof(f2453,definition,
( spl294_51
<=> member_succeeds(p(sK243),sK240) ),
introduced(definition,[new_symbols(definition,[spl294_51])],[avatar_definition]) ).
fof(f2454,plain,
( member_succeeds(p(sK243),sK240)
| ~ spl294_51 ),
inference(avatar_component_clause,[],[f2453]) ).
fof(f2519,plain,
( spl294_5
| spl294_40
| spl294_41
| spl294_42
| spl294_43
| spl294_10
| spl294_51 ),
inference(avatar_split_clause,[],[f1510,f2453,f1814,f2293,f2290,f2287,f2284,f1746]) ).
fof(f2572,plain,
( ~ sP267(sK293,'1',sK291,sK290)
| ~ sP267(sK293,'1',sK291,sK290)
| ~ spl294_1 ),
inference(resolution,[],[f1250,f1951]) ).
fof(f2577,plain,
( ~ sP267(sK293,'1',sK291,sK290)
| ~ spl294_1 ),
inference(duplicate_literal_removal,[],[f2572]) ).
fof(f2579,plain,
( ~ eval_succeeds(sK290,sK291,'1')
| ~ literal_list_succeeds(sK293)
| ~ sub(sK293,sK291)
| ~ interpretation_succeeds(sK291)
| ~ spl294_1
| ~ spl294_5 ),
inference(resolution,[],[f2577,f1747]) ).
fof(f2581,plain,
( ~ literal_list_succeeds(sK293)
| ~ sub(sK293,sK291)
| ~ interpretation_succeeds(sK291)
| ~ spl294_1
| ~ spl294_3
| ~ spl294_5 ),
inference(forward_subsumption_resolution,[],[f2579,f1909]) ).
fof(f2582,plain,
( ~ sub(sK293,sK291)
| ~ interpretation_succeeds(sK291)
| ~ spl294_1
| ~ spl294_3
| ~ spl294_5 ),
inference(forward_subsumption_resolution,[],[f2581,f1080]) ).
fof(f2583,plain,
( ~ interpretation_succeeds(sK291)
| ~ spl294_1
| ~ spl294_3
| ~ spl294_5 ),
inference(forward_subsumption_resolution,[],[f2582,f1079]) ).
fof(f2584,plain,
( $false
| ~ spl294_1
| ~ spl294_3
| ~ spl294_5 ),
inference(forward_subsumption_resolution,[],[f2583,f1082]) ).
fof(f2585,plain,
( ~ spl294_1
| ~ spl294_3
| ~ spl294_5 ),
inference(avatar_contradiction_clause,[],[f2584]) ).
fof(f2591,plain,
( ! [X0] :
( ~ sub(sK268(sK290,X0,sK293),sK291)
| ~ sP267(sK293,'0',X0,sK290) )
| ~ spl294_2 ),
inference(resolution,[],[f1722,f1249]) ).
fof(f2603,plain,
( eval_succeeds(sK290,sK291,'0')
| ~ spl294_4 ),
inference(superposition,[],[f1081,f1732]) ).
fof(f2613,plain,
( ~ sP267(sK293,'0',sK291,sK290)
| ~ sP267(sK293,'0',sK291,sK290)
| ~ spl294_2 ),
inference(resolution,[],[f2591,f1248]) ).
fof(f2614,plain,
( ~ sP267(sK293,'0',sK291,sK290)
| ~ spl294_2 ),
inference(duplicate_literal_removal,[],[f2613]) ).
fof(f2616,plain,
( ~ eval_succeeds(sK290,sK291,'0')
| ~ literal_list_succeeds(sK293)
| ~ sub(sK293,sK291)
| ~ interpretation_succeeds(sK291)
| ~ spl294_2
| ~ spl294_5 ),
inference(resolution,[],[f2614,f1747]) ).
fof(f2618,plain,
( ~ literal_list_succeeds(sK293)
| ~ sub(sK293,sK291)
| ~ interpretation_succeeds(sK291)
| ~ spl294_2
| ~ spl294_4
| ~ spl294_5 ),
inference(forward_subsumption_resolution,[],[f2616,f2603]) ).
fof(f2619,plain,
( ~ sub(sK293,sK291)
| ~ interpretation_succeeds(sK291)
| ~ spl294_2
| ~ spl294_4
| ~ spl294_5 ),
inference(forward_subsumption_resolution,[],[f2618,f1080]) ).
fof(f2620,plain,
( ~ interpretation_succeeds(sK291)
| ~ spl294_2
| ~ spl294_4
| ~ spl294_5 ),
inference(forward_subsumption_resolution,[],[f2619,f1079]) ).
fof(f2621,plain,
( $false
| ~ spl294_2
| ~ spl294_4
| ~ spl294_5 ),
inference(forward_subsumption_resolution,[],[f2620,f1082]) ).
fof(f2622,plain,
( ~ spl294_2
| ~ spl294_4
| ~ spl294_5 ),
inference(avatar_contradiction_clause,[],[f2621]) ).
fof(f2623,plain,
( member_succeeds(neg(sK239),sK240)
| ~ spl294_49
| ~ spl294_50 ),
inference(forward_demodulation,[],[f2400,f2338]) ).
fof(f2634,plain,
( ! [X0] :
( ~ member_succeeds(X0,sK242)
| member_succeeds(X0,sK240) )
| ~ spl294_8 ),
inference(resolution,[],[f1771,f936]) ).
fof(f2655,plain,
( ! [X0] :
( eval_succeeds(sK239,X0,'1')
| ~ member_succeeds(sK239,X0) )
| ~ spl294_49 ),
inference(superposition,[],[f1101,f2338]) ).
fof(f2657,plain,
( ! [X0] :
( false_succeeds(sK239,X0,cons(neg(sK239),X0))
| ~ member_fails(sK239,X0) )
| ~ spl294_49 ),
inference(superposition,[],[f1168,f2338]) ).
fof(f2662,plain,
( list_succeeds(sK242)
| ~ spl294_6 ),
inference(resolution,[],[f1750,f946]) ).
fof(f2663,plain,
( '1' = '0'
| ~ spl294_9
| ~ spl294_10 ),
inference(superposition,[],[f1815,f1812]) ).
fof(f2667,plain,
( $false
| ~ spl294_9
| ~ spl294_10
| spl294_11 ),
inference(forward_subsumption_resolution,[],[f2663,f1823]) ).
fof(f2668,plain,
( ~ spl294_9
| ~ spl294_10
| spl294_11 ),
inference(avatar_contradiction_clause,[],[f2667]) ).
fof(f2681,plain,
( ! [X0,X1] :
( eval_succeeds(sK239,X1,'1')
| ~ sub(X0,X1)
| ~ member_succeeds(sK239,X0) )
| ~ spl294_49 ),
inference(resolution,[],[f2655,f978]) ).
fof(f2701,plain,
( ~ member_fails(sK239,sK242)
| ~ sub(cons(neg(sK239),sK242),sK240)
| ~ spl294_23
| ~ spl294_49 ),
inference(resolution,[],[f2657,f1930]) ).
fof(f2724,definition,
( spl294_53
<=> sub(cons(neg(sK239),sK242),sK240) ),
introduced(definition,[new_symbols(definition,[spl294_53])],[avatar_definition]) ).
fof(f2725,plain,
( ~ sub(cons(neg(sK239),sK242),sK240)
| spl294_53 ),
inference(avatar_component_clause,[],[f2724]) ).
fof(f2727,definition,
( spl294_54
<=> member_fails(sK239,sK242) ),
introduced(definition,[new_symbols(definition,[spl294_54])],[avatar_definition]) ).
fof(f2728,plain,
( ~ member_fails(sK239,sK242)
| spl294_54 ),
inference(avatar_component_clause,[],[f2727]) ).
fof(f2729,plain,
( ~ spl294_53
| ~ spl294_54
| ~ spl294_23
| ~ spl294_49 ),
inference(avatar_split_clause,[],[f2701,f2337,f1929,f2727,f2724]) ).
fof(f2731,plain,
( ~ sub(sK242,sK240)
| ~ member_succeeds(neg(sK239),sK240)
| spl294_53 ),
inference(resolution,[],[f2725,f944]) ).
fof(f2733,plain,
( ~ member_succeeds(neg(sK239),sK240)
| ~ spl294_8
| spl294_53 ),
inference(forward_subsumption_resolution,[],[f2731,f1771]) ).
fof(f2734,plain,
( $false
| ~ spl294_8
| ~ spl294_49
| ~ spl294_50
| spl294_53 ),
inference(forward_subsumption_resolution,[],[f2733,f2623]) ).
fof(f2735,plain,
( ~ spl294_8
| ~ spl294_49
| ~ spl294_50
| spl294_53 ),
inference(avatar_contradiction_clause,[],[f2734]) ).
fof(f2801,plain,
( member_succeeds(p(sK236(sK242)),sK240)
| ~ literal_list_succeeds(sK242)
| interpretation_succeeds(sK242)
| ~ spl294_8 ),
inference(resolution,[],[f2634,f950]) ).
fof(f2805,plain,
( member_succeeds(p(sK236(sK242)),sK240)
| interpretation_succeeds(sK242)
| ~ spl294_6
| ~ spl294_8 ),
inference(forward_subsumption_resolution,[],[f2801,f1750]) ).
fof(f2811,definition,
( spl294_58
<=> interpretation_succeeds(sK242) ),
introduced(definition,[new_symbols(definition,[spl294_58])],[avatar_definition]) ).
fof(f2812,plain,
( ~ interpretation_succeeds(sK242)
| spl294_58 ),
inference(avatar_component_clause,[],[f2811]) ).
fof(f2820,plain,
( member_succeeds(p(sK236(sK242)),sK240)
| ~ spl294_6
| ~ spl294_8
| spl294_58 ),
inference(backward_subsumption_resolution,[],[f2805,f2812]) ).
fof(f2876,plain,
( spl294_5
| spl294_45
| spl294_46
| spl294_47
| spl294_48
| spl294_50
| spl294_9 ),
inference(avatar_split_clause,[],[f1507,f1811,f2399,f2334,f2331,f2328,f2325,f1746]) ).
fof(f3061,plain,
( ! [X0] :
( ~ member_succeeds(neg(sK239),X0)
| eval_succeeds(sK239,X0,'0') )
| ~ spl294_49 ),
inference(superposition,[],[f1103,f2338]) ).
fof(f3063,plain,
( eval_succeeds(sK239,sK240,'0')
| ~ spl294_49
| ~ spl294_50 ),
inference(resolution,[],[f3061,f2623]) ).
fof(f3068,plain,
( ! [X0] :
( ~ interpretation_succeeds(sK240)
| ~ eval_succeeds(sK239,sK240,X0)
| '0' = X0 )
| ~ spl294_49
| ~ spl294_50 ),
inference(resolution,[],[f3063,f982]) ).
fof(f3070,plain,
( ! [X0] :
( ~ eval_succeeds(sK239,sK240,X0)
| '0' = X0 )
| ~ spl294_7
| ~ spl294_49
| ~ spl294_50 ),
inference(forward_subsumption_resolution,[],[f3068,f1754]) ).
fof(f3091,plain,
! [X0,X1] :
( member_fails(X1,X0)
| ~ list_succeeds(X0)
| member_succeeds(X1,X0) ),
inference(resolution,[],[f939,f346]) ).
fof(f3146,plain,
! [X2,X3,X0,X1] :
( true_succeeds(or(X0,X3),X1,X2)
| ~ true_succeeds(X0,X1,X2) ),
inference(resolution,[],[f1195,f721]) ).
fof(f3276,plain,
! [X0,X1] :
( p(X1) != X0
| p(sK201(X0)) = X0
| literal_fails(X0) ),
inference(superposition,[],[f296,f843]) ).
fof(f3399,plain,
! [X2,X3,X0,X1] :
( false_succeeds(and(X3,X0),X1,X2)
| ~ false_succeeds(X0,X1,X2) ),
inference(resolution,[],[f1171,f633]) ).
fof(f3676,plain,
! [X2,X3,X0,X1] :
( true_succeeds(or(X3,X0),X1,X2)
| ~ true_succeeds(X0,X1,X2) ),
inference(resolution,[],[f1196,f722]) ).
fof(f3860,plain,
! [X0] :
( p(X0) = p(sK199(p(X0)))
| ~ literal_succeeds(p(X0)) ),
inference(equality_resolution,[],[f2405]) ).
fof(f3861,plain,
! [X0] : p(X0) = p(sK199(p(X0))),
inference(forward_subsumption_resolution,[],[f3860,f1222]) ).
fof(f3867,definition,
( spl294_68
<=> sK239 = p(sK199(sK239)) ),
introduced(definition,[new_symbols(definition,[spl294_68])],[avatar_definition]) ).
fof(f3868,plain,
( sK239 = p(sK199(sK239))
| ~ spl294_68 ),
inference(avatar_component_clause,[],[f3867]) ).
fof(f3914,plain,
( ! [X0] :
( ~ member_succeeds(neg(sK239),X0)
| ~ interpretation_succeeds(X0)
| ~ member_succeeds(sK239,X0) )
| ~ spl294_68 ),
inference(superposition,[],[f947,f3868]) ).
fof(f3927,plain,
( ! [X0] :
( true_succeeds(sK239,X0,cons(sK239,X0))
| ~ member_fails(neg(sK239),X0) )
| ~ spl294_68 ),
inference(superposition,[],[f1192,f3868]) ).
fof(f4764,plain,
! [X2,X3,X0,X1,X4] :
( false_succeeds(or(X0,X3),X1,X4)
| ~ false_succeeds(X3,X2,X4)
| ~ false_succeeds(X0,X1,X2) ),
inference(resolution,[],[f1172,f634]) ).
fof(f4883,plain,
( ! [X0] :
( ~ sub(X0,sK240)
| ~ member_succeeds(sK239,X0)
| '1' = '0' )
| ~ spl294_7
| ~ spl294_49
| ~ spl294_50 ),
inference(resolution,[],[f2681,f3070]) ).
fof(f4896,plain,
( ! [X0] :
( ~ sub(X0,sK240)
| ~ member_succeeds(sK239,X0) )
| ~ spl294_7
| spl294_11
| ~ spl294_49
| ~ spl294_50 ),
inference(forward_subsumption_resolution,[],[f4883,f1823]) ).
fof(f4909,plain,
( ~ member_succeeds(sK239,sK242)
| ~ spl294_7
| ~ spl294_8
| spl294_11
| ~ spl294_49
| ~ spl294_50 ),
inference(resolution,[],[f4896,f1771]) ).
fof(f5001,plain,
( ~ literal_list_succeeds(sK242)
| interpretation_succeeds(sK242)
| member_succeeds(neg(p(sK236(sK242))),sK240)
| ~ spl294_8 ),
inference(resolution,[],[f949,f2634]) ).
fof(f5004,plain,
( interpretation_succeeds(sK242)
| member_succeeds(neg(p(sK236(sK242))),sK240)
| ~ spl294_6
| ~ spl294_8 ),
inference(forward_subsumption_resolution,[],[f5001,f1750]) ).
fof(f5006,plain,
( member_succeeds(neg(p(sK236(sK242))),sK240)
| ~ spl294_6
| ~ spl294_8
| spl294_58 ),
inference(forward_subsumption_resolution,[],[f5004,f2812]) ).
fof(f5010,plain,
( ~ interpretation_succeeds(sK240)
| ~ member_succeeds(p(sK236(sK242)),sK240)
| ~ spl294_6
| ~ spl294_8
| spl294_58 ),
inference(resolution,[],[f5006,f947]) ).
fof(f5012,plain,
( ~ member_succeeds(p(sK236(sK242)),sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| spl294_58 ),
inference(forward_subsumption_resolution,[],[f5010,f1754]) ).
fof(f5013,plain,
( $false
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| spl294_58 ),
inference(forward_subsumption_resolution,[],[f5012,f2820]) ).
fof(f5014,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| spl294_58 ),
inference(avatar_contradiction_clause,[],[f5013]) ).
fof(f5027,plain,
( interpretation_succeeds(sK242)
| ~ spl294_58 ),
inference(avatar_component_clause,[],[f2811]) ).
fof(f5486,definition,
( spl294_93
<=> sK239 = p(sK201(sK239)) ),
introduced(definition,[new_symbols(definition,[spl294_93])],[avatar_definition]) ).
fof(f5487,plain,
( sK239 = p(sK201(sK239))
| ~ spl294_93 ),
inference(avatar_component_clause,[],[f5486]) ).
fof(f5573,plain,
( sK239 = p(sK199(sK239))
| ~ spl294_93 ),
inference(superposition,[],[f3861,f5487]) ).
fof(f9563,plain,
( ~ list_succeeds(sK242)
| member_succeeds(sK239,sK242)
| spl294_54 ),
inference(resolution,[],[f3091,f2728]) ).
fof(f9565,plain,
( member_succeeds(sK239,sK242)
| ~ spl294_6
| spl294_54 ),
inference(forward_subsumption_resolution,[],[f9563,f2662]) ).
fof(f9566,plain,
( $false
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| spl294_11
| ~ spl294_49
| ~ spl294_50
| spl294_54 ),
inference(forward_subsumption_resolution,[],[f9565,f4909]) ).
fof(f9567,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| spl294_11
| ~ spl294_49
| ~ spl294_50
| spl294_54 ),
inference(avatar_contradiction_clause,[],[f9566]) ).
fof(f9568,plain,
( sP265(sK256,sK255,'1',sK240,sK239)
| ~ spl294_9
| ~ spl294_40 ),
inference(forward_demodulation,[],[f2285,f1812]) ).
fof(f9571,plain,
( sK239 = or(sK255,sK256)
| ~ spl294_9
| ~ spl294_40 ),
inference(resolution,[],[f9568,f1043]) ).
fof(f9654,plain,
( sP264(sK254,sK253,'1',sK240,sK239)
| ~ spl294_9
| ~ spl294_41 ),
inference(forward_demodulation,[],[f2288,f1812]) ).
fof(f9660,plain,
( sK239 = or(sK253,sK254)
| ~ spl294_9
| ~ spl294_41 ),
inference(resolution,[],[f9654,f1046]) ).
fof(f9780,plain,
( member_succeeds(sK239,sK240)
| ~ spl294_44
| ~ spl294_51 ),
inference(forward_demodulation,[],[f2454,f2297]) ).
fof(f9851,plain,
( ~ literal_fails(sK239)
| ~ spl294_44 ),
inference(superposition,[],[f1224,f2297]) ).
fof(f9868,plain,
( ! [X0] :
( sK239 != X0
| p(sK201(X0)) = X0
| literal_fails(X0) )
| ~ spl294_44 ),
inference(superposition,[],[f3276,f2297]) ).
fof(f10391,plain,
( ~ member_fails(neg(sK239),sK242)
| ~ sub(cons(sK239,sK242),sK240)
| ~ spl294_20
| ~ spl294_68 ),
inference(resolution,[],[f3927,f1890]) ).
fof(f10412,definition,
( spl294_105
<=> sub(cons(sK239,sK242),sK240) ),
introduced(definition,[new_symbols(definition,[spl294_105])],[avatar_definition]) ).
fof(f10413,plain,
( ~ sub(cons(sK239,sK242),sK240)
| spl294_105 ),
inference(avatar_component_clause,[],[f10412]) ).
fof(f10415,definition,
( spl294_106
<=> member_fails(neg(sK239),sK242) ),
introduced(definition,[new_symbols(definition,[spl294_106])],[avatar_definition]) ).
fof(f10416,plain,
( ~ member_fails(neg(sK239),sK242)
| spl294_106 ),
inference(avatar_component_clause,[],[f10415]) ).
fof(f10417,plain,
( ~ spl294_105
| ~ spl294_106
| ~ spl294_20
| ~ spl294_68 ),
inference(avatar_split_clause,[],[f10391,f3867,f1889,f10415,f10412]) ).
fof(f10420,plain,
( ~ sub(sK242,sK240)
| ~ member_succeeds(sK239,sK240)
| spl294_105 ),
inference(resolution,[],[f10413,f944]) ).
fof(f10434,plain,
( ~ member_succeeds(sK239,sK240)
| ~ spl294_8
| spl294_105 ),
inference(forward_subsumption_resolution,[],[f10420,f1771]) ).
fof(f10436,plain,
( $false
| ~ spl294_8
| ~ spl294_44
| ~ spl294_51
| spl294_105 ),
inference(forward_subsumption_resolution,[],[f10434,f9780]) ).
fof(f10437,plain,
( ~ spl294_8
| ~ spl294_44
| ~ spl294_51
| spl294_105 ),
inference(avatar_contradiction_clause,[],[f10436]) ).
fof(f10440,plain,
( ~ list_succeeds(sK242)
| member_succeeds(neg(sK239),sK242)
| spl294_106 ),
inference(resolution,[],[f10416,f3091]) ).
fof(f10443,plain,
( member_succeeds(neg(sK239),sK242)
| ~ spl294_6
| spl294_106 ),
inference(forward_subsumption_resolution,[],[f10440,f2662]) ).
fof(f10444,plain,
( member_succeeds(neg(sK239),sK240)
| ~ spl294_6
| ~ spl294_8
| spl294_106 ),
inference(resolution,[],[f10443,f2634]) ).
fof(f10472,plain,
( ~ interpretation_succeeds(sK240)
| ~ member_succeeds(sK239,sK240)
| ~ spl294_6
| ~ spl294_8
| ~ spl294_68
| spl294_106 ),
inference(resolution,[],[f10444,f3914]) ).
fof(f10489,plain,
( ~ member_succeeds(sK239,sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_68
| spl294_106 ),
inference(forward_subsumption_resolution,[],[f10472,f1754]) ).
fof(f10490,plain,
( $false
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_44
| ~ spl294_51
| ~ spl294_68
| spl294_106 ),
inference(forward_subsumption_resolution,[],[f10489,f9780]) ).
fof(f10491,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_44
| ~ spl294_51
| ~ spl294_68
| spl294_106 ),
inference(avatar_contradiction_clause,[],[f10490]) ).
fof(f10498,plain,
( spl294_68
| ~ spl294_93 ),
inference(avatar_split_clause,[],[f5573,f5486,f3867]) ).
fof(f10806,plain,
( sK239 = p(sK201(sK239))
| literal_fails(sK239)
| ~ spl294_44 ),
inference(equality_resolution,[],[f9868]) ).
fof(f10807,plain,
( sK239 = p(sK201(sK239))
| ~ spl294_44 ),
inference(forward_subsumption_resolution,[],[f10806,f9851]) ).
fof(f10808,plain,
( spl294_93
| ~ spl294_44 ),
inference(avatar_split_clause,[],[f10807,f2296,f5486]) ).
fof(f10809,plain,
( sP260(sK246,'0',sK240,sK239)
| ~ spl294_10
| ~ spl294_48 ),
inference(forward_demodulation,[],[f2335,f1815]) ).
fof(f10848,plain,
( sK239 = neg(sK246)
| ~ spl294_10
| ~ spl294_48 ),
inference(resolution,[],[f10809,f1059]) ).
fof(f10855,plain,
( sP262(sK250,sK249,'0',sK240,sK239)
| ~ spl294_10
| ~ spl294_47 ),
inference(forward_demodulation,[],[f2332,f1815]) ).
fof(f10858,plain,
( sK239 = and(sK249,sK250)
| ~ spl294_10
| ~ spl294_47 ),
inference(resolution,[],[f10855,f1052]) ).
fof(f11007,plain,
( sP263(sK252,sK251,'0',sK240,sK239)
| ~ spl294_10
| ~ spl294_46 ),
inference(forward_demodulation,[],[f2329,f1815]) ).
fof(f11073,plain,
( sK239 = and(sK251,sK252)
| ~ spl294_10
| ~ spl294_46 ),
inference(resolution,[],[f11007,f1049]) ).
fof(f11152,plain,
( sP266(sK258,sK257,'0',sK240,sK239)
| ~ spl294_10
| ~ spl294_45 ),
inference(forward_demodulation,[],[f2326,f1815]) ).
fof(f11217,plain,
( sK239 = or(sK257,sK258)
| ~ spl294_10
| ~ spl294_45 ),
inference(resolution,[],[f11152,f1040]) ).
fof(f11371,plain,
( sP259(sK245,'1',sK240,sK239)
| ~ spl294_9
| ~ spl294_43 ),
inference(forward_demodulation,[],[f2294,f1812]) ).
fof(f11419,plain,
( sK239 = neg(sK245)
| ~ spl294_9
| ~ spl294_43 ),
inference(resolution,[],[f11371,f1062]) ).
fof(f11436,plain,
( sP261(sK248,sK247,'1',sK240,sK239)
| ~ spl294_9
| ~ spl294_42 ),
inference(forward_demodulation,[],[f2291,f1812]) ).
fof(f11440,plain,
( sK239 = and(sK247,sK248)
| ~ spl294_9
| ~ spl294_42 ),
inference(resolution,[],[f11436,f1056]) ).
fof(f11617,plain,
( ! [X0,X1] :
( ~ false_succeeds(sK245,X0,X1)
| true_succeeds(sK239,X0,X1) )
| ~ spl294_9
| ~ spl294_43 ),
inference(superposition,[],[f1193,f11419]) ).
fof(f11780,plain,
( ! [X2,X3,X0,X1] :
( true_succeeds(sK239,X0,sK270(X1,sK245,X0))
| ~ sub(X0,X1)
| ~ literal_list_succeeds(X0)
| ~ interpretation_succeeds(X1)
| ~ sP259(sK245,X2,X1,X3) )
| ~ spl294_9
| ~ spl294_43 ),
inference(resolution,[],[f11617,f1270]) ).
fof(f12410,plain,
( ! [X2,X0,X1] :
( ~ sub(sK242,X0)
| ~ literal_list_succeeds(sK242)
| ~ interpretation_succeeds(X0)
| ~ sP259(sK245,X1,X0,X2)
| ~ sub(sK270(X0,sK245,sK242),sK240) )
| ~ spl294_9
| ~ spl294_20
| ~ spl294_43 ),
inference(resolution,[],[f11780,f1890]) ).
fof(f12428,plain,
( ! [X2,X0,X1] :
( ~ sub(sK270(X0,sK245,sK242),sK240)
| ~ interpretation_succeeds(X0)
| ~ sP259(sK245,X1,X0,X2)
| ~ sub(sK242,X0) )
| ~ spl294_6
| ~ spl294_9
| ~ spl294_20
| ~ spl294_43 ),
inference(forward_subsumption_resolution,[],[f12410,f1750]) ).
fof(f12430,plain,
( ! [X2,X3,X0,X1] :
( ~ interpretation_succeeds(sK240)
| ~ sP259(sK245,X0,sK240,X1)
| ~ sub(sK242,sK240)
| ~ sub(sK242,sK240)
| ~ literal_list_succeeds(sK242)
| ~ interpretation_succeeds(sK240)
| ~ sP259(sK245,X2,sK240,X3) )
| ~ spl294_6
| ~ spl294_9
| ~ spl294_20
| ~ spl294_43 ),
inference(resolution,[],[f12428,f1271]) ).
fof(f12443,plain,
( ! [X2,X3,X0,X1] :
( ~ interpretation_succeeds(sK240)
| ~ sP259(sK245,X0,sK240,X1)
| ~ sub(sK242,sK240)
| ~ literal_list_succeeds(sK242)
| ~ sP259(sK245,X2,sK240,X3) )
| ~ spl294_6
| ~ spl294_9
| ~ spl294_20
| ~ spl294_43 ),
inference(duplicate_literal_removal,[],[f12430]) ).
fof(f12445,plain,
( ! [X2,X3,X0,X1] :
( ~ sP259(sK245,X0,sK240,X1)
| ~ sub(sK242,sK240)
| ~ literal_list_succeeds(sK242)
| ~ sP259(sK245,X2,sK240,X3) )
| ~ spl294_6
| ~ spl294_7
| ~ spl294_9
| ~ spl294_20
| ~ spl294_43 ),
inference(forward_subsumption_resolution,[],[f12443,f1754]) ).
fof(f12447,plain,
( ! [X2,X3,X0,X1] :
( ~ sP259(sK245,X0,sK240,X1)
| ~ literal_list_succeeds(sK242)
| ~ sP259(sK245,X2,sK240,X3) )
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_43 ),
inference(forward_subsumption_resolution,[],[f12445,f1771]) ).
fof(f12449,plain,
( ! [X2,X3,X0,X1] :
( ~ sP259(sK245,X0,sK240,X1)
| ~ sP259(sK245,X2,sK240,X3) )
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_43 ),
inference(forward_subsumption_resolution,[],[f12447,f1750]) ).
fof(f12451,plain,
( $false
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_43 ),
inference(backward_subsumption_resolution,[],[f11371,f12449]) ).
fof(f12452,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_43 ),
inference(avatar_contradiction_clause,[],[f12451]) ).
fof(f12461,plain,
( ! [X0] :
( ~ sub(X0,sK240)
| ~ literal_list_succeeds(X0)
| sub(sK283(sK240,sK253,X0),sK240)
| ~ interpretation_succeeds(sK240) )
| ~ spl294_9
| ~ spl294_41 ),
inference(resolution,[],[f9654,f1259]) ).
fof(f12472,plain,
( ! [X0] :
( sub(sK283(sK240,sK253,X0),sK240)
| ~ literal_list_succeeds(X0)
| ~ sub(X0,sK240) )
| ~ spl294_7
| ~ spl294_9
| ~ spl294_41 ),
inference(forward_subsumption_resolution,[],[f12461,f1754]) ).
fof(f12504,plain,
( ! [X0,X1] :
( ~ true_succeeds(sK253,X0,X1)
| true_succeeds(sK239,X0,X1) )
| ~ spl294_9
| ~ spl294_41 ),
inference(superposition,[],[f3146,f9660]) ).
fof(f12540,plain,
( ! [X2,X3,X0,X1,X4] :
( true_succeeds(sK239,X0,sK283(X1,sK253,X0))
| ~ sub(X0,X1)
| ~ literal_list_succeeds(X0)
| ~ interpretation_succeeds(X1)
| ~ sP264(X2,sK253,X3,X1,X4) )
| ~ spl294_9
| ~ spl294_41 ),
inference(resolution,[],[f12504,f1258]) ).
fof(f12789,plain,
( ! [X2,X3,X0,X1] :
( ~ sub(sK242,X0)
| ~ literal_list_succeeds(sK242)
| ~ interpretation_succeeds(X0)
| ~ sP264(X1,sK253,X2,X0,X3)
| ~ sub(sK283(X0,sK253,sK242),sK240) )
| ~ spl294_9
| ~ spl294_20
| ~ spl294_41 ),
inference(resolution,[],[f12540,f1890]) ).
fof(f12808,plain,
( ! [X2,X3,X0,X1] :
( ~ sP264(X1,sK253,X2,X0,X3)
| ~ interpretation_succeeds(X0)
| ~ sub(sK242,X0)
| ~ sub(sK283(X0,sK253,sK242),sK240) )
| ~ spl294_6
| ~ spl294_9
| ~ spl294_20
| ~ spl294_41 ),
inference(forward_subsumption_resolution,[],[f12789,f1750]) ).
fof(f12809,plain,
( ~ interpretation_succeeds(sK240)
| ~ sub(sK242,sK240)
| ~ sub(sK283(sK240,sK253,sK242),sK240)
| ~ spl294_6
| ~ spl294_9
| ~ spl294_20
| ~ spl294_41 ),
inference(resolution,[],[f12808,f9654]) ).
fof(f12810,plain,
( ~ sub(sK242,sK240)
| ~ sub(sK283(sK240,sK253,sK242),sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_9
| ~ spl294_20
| ~ spl294_41 ),
inference(forward_subsumption_resolution,[],[f12809,f1754]) ).
fof(f12811,plain,
( ~ sub(sK283(sK240,sK253,sK242),sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_41 ),
inference(forward_subsumption_resolution,[],[f12810,f1771]) ).
fof(f12815,plain,
( ~ literal_list_succeeds(sK242)
| ~ sub(sK242,sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_41 ),
inference(resolution,[],[f12811,f12472]) ).
fof(f12831,plain,
( ~ sub(sK242,sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_41 ),
inference(forward_subsumption_resolution,[],[f12815,f1750]) ).
fof(f12832,plain,
( $false
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_41 ),
inference(forward_subsumption_resolution,[],[f12831,f1771]) ).
fof(f12833,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_41 ),
inference(avatar_contradiction_clause,[],[f12832]) ).
fof(f12840,plain,
( ! [X0] :
( ~ sub(X0,sK240)
| ~ literal_list_succeeds(X0)
| sub(sK277(sK240,sK247,X0),sK240)
| ~ interpretation_succeeds(sK240) )
| ~ spl294_9
| ~ spl294_42 ),
inference(resolution,[],[f11436,f1265]) ).
fof(f12841,plain,
( ! [X0] :
( ~ sub(X0,sK240)
| ~ literal_list_succeeds(X0)
| sub(sK275(sK240,sK248,X0),sK240)
| ~ interpretation_succeeds(sK240) )
| ~ spl294_9
| ~ spl294_42 ),
inference(resolution,[],[f11436,f1267]) ).
fof(f12846,plain,
( ! [X0] :
( interpretation_succeeds(sK277(sK240,sK247,X0))
| ~ sub(X0,sK240)
| ~ interpretation_succeeds(sK240)
| ~ interpretation_succeeds(X0) )
| ~ spl294_9
| ~ spl294_42 ),
inference(resolution,[],[f11436,f1852]) ).
fof(f12857,plain,
( ! [X0] :
( interpretation_succeeds(sK277(sK240,sK247,X0))
| ~ sub(X0,sK240)
| ~ interpretation_succeeds(X0) )
| ~ spl294_7
| ~ spl294_9
| ~ spl294_42 ),
inference(forward_subsumption_resolution,[],[f12846,f1754]) ).
fof(f12862,plain,
( ! [X0] :
( sub(sK275(sK240,sK248,X0),sK240)
| ~ literal_list_succeeds(X0)
| ~ sub(X0,sK240) )
| ~ spl294_7
| ~ spl294_9
| ~ spl294_42 ),
inference(forward_subsumption_resolution,[],[f12841,f1754]) ).
fof(f12863,plain,
( ! [X0] :
( sub(sK277(sK240,sK247,X0),sK240)
| ~ literal_list_succeeds(X0)
| ~ sub(X0,sK240) )
| ~ spl294_7
| ~ spl294_9
| ~ spl294_42 ),
inference(forward_subsumption_resolution,[],[f12840,f1754]) ).
fof(f12892,plain,
( ! [X2,X0,X1] :
( ~ true_succeeds(sK248,X2,X1)
| ~ true_succeeds(sK247,X0,X2)
| true_succeeds(sK239,X0,X1) )
| ~ spl294_9
| ~ spl294_42 ),
inference(superposition,[],[f1194,f11440]) ).
fof(f12995,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( true_succeeds(sK239,X0,sK275(X2,sK248,X1))
| ~ true_succeeds(sK247,X0,X1)
| ~ sub(X1,X2)
| ~ literal_list_succeeds(X1)
| ~ interpretation_succeeds(X2)
| ~ sP261(sK248,X3,X4,X2,X5) )
| ~ spl294_9
| ~ spl294_42 ),
inference(resolution,[],[f12892,f1266]) ).
fof(f13138,plain,
( ! [X0] :
( literal_list_succeeds(sK277(sK240,sK247,X0))
| ~ interpretation_succeeds(X0)
| ~ sub(X0,sK240) )
| ~ spl294_7
| ~ spl294_9
| ~ spl294_42 ),
inference(resolution,[],[f12857,f948]) ).
fof(f13472,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ sP261(sK248,X2,X3,X1,X4)
| ~ sub(X0,X1)
| ~ literal_list_succeeds(X0)
| ~ interpretation_succeeds(X1)
| ~ true_succeeds(sK247,sK242,X0)
| ~ sub(sK275(X1,sK248,X0),sK240) )
| ~ spl294_9
| ~ spl294_20
| ~ spl294_42 ),
inference(resolution,[],[f12995,f1890]) ).
fof(f13493,plain,
( ! [X0] :
( ~ sub(X0,sK240)
| ~ literal_list_succeeds(X0)
| ~ interpretation_succeeds(sK240)
| ~ true_succeeds(sK247,sK242,X0)
| ~ sub(sK275(sK240,sK248,X0),sK240) )
| ~ spl294_9
| ~ spl294_20
| ~ spl294_42 ),
inference(resolution,[],[f13472,f11436]) ).
fof(f13494,plain,
( ! [X0] :
( ~ sub(X0,sK240)
| ~ literal_list_succeeds(X0)
| ~ interpretation_succeeds(sK240)
| ~ true_succeeds(sK247,sK242,X0) )
| ~ spl294_7
| ~ spl294_9
| ~ spl294_20
| ~ spl294_42 ),
inference(forward_subsumption_resolution,[],[f13493,f12862]) ).
fof(f13495,plain,
( ! [X0] :
( ~ true_succeeds(sK247,sK242,X0)
| ~ literal_list_succeeds(X0)
| ~ sub(X0,sK240) )
| ~ spl294_7
| ~ spl294_9
| ~ spl294_20
| ~ spl294_42 ),
inference(forward_subsumption_resolution,[],[f13494,f1754]) ).
fof(f13501,plain,
( ! [X2,X3,X0,X1] :
( ~ literal_list_succeeds(sK277(X0,sK247,sK242))
| ~ sub(sK277(X0,sK247,sK242),sK240)
| ~ sub(sK242,X0)
| ~ literal_list_succeeds(sK242)
| ~ interpretation_succeeds(X0)
| ~ sP261(X1,sK247,X2,X0,X3) )
| ~ spl294_7
| ~ spl294_9
| ~ spl294_20
| ~ spl294_42 ),
inference(resolution,[],[f13495,f1264]) ).
fof(f13514,plain,
( ! [X2,X3,X0,X1] :
( ~ sP261(X1,sK247,X2,X0,X3)
| ~ sub(sK277(X0,sK247,sK242),sK240)
| ~ sub(sK242,X0)
| ~ interpretation_succeeds(X0)
| ~ literal_list_succeeds(sK277(X0,sK247,sK242)) )
| ~ spl294_6
| ~ spl294_7
| ~ spl294_9
| ~ spl294_20
| ~ spl294_42 ),
inference(forward_subsumption_resolution,[],[f13501,f1750]) ).
fof(f13521,plain,
( ~ sub(sK277(sK240,sK247,sK242),sK240)
| ~ sub(sK242,sK240)
| ~ interpretation_succeeds(sK240)
| ~ literal_list_succeeds(sK277(sK240,sK247,sK242))
| ~ spl294_6
| ~ spl294_7
| ~ spl294_9
| ~ spl294_20
| ~ spl294_42 ),
inference(resolution,[],[f13514,f11436]) ).
fof(f13522,plain,
( ~ sub(sK277(sK240,sK247,sK242),sK240)
| ~ interpretation_succeeds(sK240)
| ~ literal_list_succeeds(sK277(sK240,sK247,sK242))
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_42 ),
inference(forward_subsumption_resolution,[],[f13521,f1771]) ).
fof(f13523,plain,
( ~ sub(sK277(sK240,sK247,sK242),sK240)
| ~ literal_list_succeeds(sK277(sK240,sK247,sK242))
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_42 ),
inference(forward_subsumption_resolution,[],[f13522,f1754]) ).
fof(f13525,definition,
( spl294_126
<=> literal_list_succeeds(sK277(sK240,sK247,sK242)) ),
introduced(definition,[new_symbols(definition,[spl294_126])],[avatar_definition]) ).
fof(f13526,plain,
( ~ literal_list_succeeds(sK277(sK240,sK247,sK242))
| spl294_126 ),
inference(avatar_component_clause,[],[f13525]) ).
fof(f13528,definition,
( spl294_127
<=> sub(sK277(sK240,sK247,sK242),sK240) ),
introduced(definition,[new_symbols(definition,[spl294_127])],[avatar_definition]) ).
fof(f13529,plain,
( ~ sub(sK277(sK240,sK247,sK242),sK240)
| spl294_127 ),
inference(avatar_component_clause,[],[f13528]) ).
fof(f13530,plain,
( ~ spl294_126
| ~ spl294_127
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_42 ),
inference(avatar_split_clause,[],[f13523,f2290,f1889,f1811,f1770,f1753,f1749,f13528,f13525]) ).
fof(f13534,plain,
( ~ interpretation_succeeds(sK242)
| ~ sub(sK242,sK240)
| ~ spl294_7
| ~ spl294_9
| ~ spl294_42
| spl294_126 ),
inference(resolution,[],[f13526,f13138]) ).
fof(f13540,plain,
( ~ sub(sK242,sK240)
| ~ spl294_7
| ~ spl294_9
| ~ spl294_42
| ~ spl294_58
| spl294_126 ),
inference(forward_subsumption_resolution,[],[f13534,f5027]) ).
fof(f13543,plain,
( $false
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_42
| ~ spl294_58
| spl294_126 ),
inference(forward_subsumption_resolution,[],[f13540,f1771]) ).
fof(f13544,plain,
( ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_42
| ~ spl294_58
| spl294_126 ),
inference(avatar_contradiction_clause,[],[f13543]) ).
fof(f13548,plain,
( ~ literal_list_succeeds(sK242)
| ~ sub(sK242,sK240)
| ~ spl294_7
| ~ spl294_9
| ~ spl294_42
| spl294_127 ),
inference(resolution,[],[f13529,f12863]) ).
fof(f13564,plain,
( ~ sub(sK242,sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_9
| ~ spl294_42
| spl294_127 ),
inference(forward_subsumption_resolution,[],[f13548,f1750]) ).
fof(f13565,plain,
( $false
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_42
| spl294_127 ),
inference(forward_subsumption_resolution,[],[f13564,f1771]) ).
fof(f13566,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_42
| spl294_127 ),
inference(avatar_contradiction_clause,[],[f13565]) ).
fof(f13571,plain,
( ! [X0] :
( ~ sub(X0,sK240)
| ~ literal_list_succeeds(X0)
| sub(sK285(sK240,sK256,X0),sK240)
| ~ interpretation_succeeds(sK240) )
| ~ spl294_9
| ~ spl294_40 ),
inference(resolution,[],[f9568,f1257]) ).
fof(f13582,plain,
( ! [X0] :
( sub(sK285(sK240,sK256,X0),sK240)
| ~ literal_list_succeeds(X0)
| ~ sub(X0,sK240) )
| ~ spl294_7
| ~ spl294_9
| ~ spl294_40 ),
inference(forward_subsumption_resolution,[],[f13571,f1754]) ).
fof(f13617,plain,
( ! [X0,X1] :
( ~ true_succeeds(sK256,X0,X1)
| true_succeeds(sK239,X0,X1) )
| ~ spl294_9
| ~ spl294_40 ),
inference(superposition,[],[f3676,f9571]) ).
fof(f13664,plain,
( ! [X2,X3,X0,X1,X4] :
( true_succeeds(sK239,X0,sK285(X1,sK256,X0))
| ~ sub(X0,X1)
| ~ literal_list_succeeds(X0)
| ~ interpretation_succeeds(X1)
| ~ sP265(sK256,X2,X3,X1,X4) )
| ~ spl294_9
| ~ spl294_40 ),
inference(resolution,[],[f13617,f1256]) ).
fof(f14022,plain,
( ! [X2,X3,X0,X1] :
( ~ sub(sK242,X0)
| ~ literal_list_succeeds(sK242)
| ~ interpretation_succeeds(X0)
| ~ sP265(sK256,X1,X2,X0,X3)
| ~ sub(sK285(X0,sK256,sK242),sK240) )
| ~ spl294_9
| ~ spl294_20
| ~ spl294_40 ),
inference(resolution,[],[f13664,f1890]) ).
fof(f14041,plain,
( ! [X2,X3,X0,X1] :
( ~ sP265(sK256,X1,X2,X0,X3)
| ~ interpretation_succeeds(X0)
| ~ sub(sK242,X0)
| ~ sub(sK285(X0,sK256,sK242),sK240) )
| ~ spl294_6
| ~ spl294_9
| ~ spl294_20
| ~ spl294_40 ),
inference(forward_subsumption_resolution,[],[f14022,f1750]) ).
fof(f14042,plain,
( ~ interpretation_succeeds(sK240)
| ~ sub(sK242,sK240)
| ~ sub(sK285(sK240,sK256,sK242),sK240)
| ~ spl294_6
| ~ spl294_9
| ~ spl294_20
| ~ spl294_40 ),
inference(resolution,[],[f14041,f9568]) ).
fof(f14043,plain,
( ~ sub(sK242,sK240)
| ~ sub(sK285(sK240,sK256,sK242),sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_9
| ~ spl294_20
| ~ spl294_40 ),
inference(forward_subsumption_resolution,[],[f14042,f1754]) ).
fof(f14044,plain,
( ~ sub(sK285(sK240,sK256,sK242),sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_40 ),
inference(forward_subsumption_resolution,[],[f14043,f1771]) ).
fof(f14048,plain,
( ~ literal_list_succeeds(sK242)
| ~ sub(sK242,sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_40 ),
inference(resolution,[],[f14044,f13582]) ).
fof(f14064,plain,
( ~ sub(sK242,sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_40 ),
inference(forward_subsumption_resolution,[],[f14048,f1750]) ).
fof(f14065,plain,
( $false
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_40 ),
inference(forward_subsumption_resolution,[],[f14064,f1771]) ).
fof(f14066,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_40 ),
inference(avatar_contradiction_clause,[],[f14065]) ).
fof(f14085,plain,
( ! [X0,X1] :
( ~ true_succeeds(sK246,X0,X1)
| false_succeeds(sK239,X0,X1) )
| ~ spl294_10
| ~ spl294_48 ),
inference(superposition,[],[f1169,f10848]) ).
fof(f14175,plain,
( ! [X2,X3,X0,X1] :
( false_succeeds(sK239,X0,sK273(X1,sK246,X0))
| ~ sub(X0,X1)
| ~ literal_list_succeeds(X0)
| ~ interpretation_succeeds(X1)
| ~ sP260(sK246,X2,X1,X3) )
| ~ spl294_10
| ~ spl294_48 ),
inference(resolution,[],[f14085,f1268]) ).
fof(f14504,plain,
( ! [X2,X0,X1] :
( ~ sub(sK242,X0)
| ~ literal_list_succeeds(sK242)
| ~ interpretation_succeeds(X0)
| ~ sP260(sK246,X1,X0,X2)
| ~ sub(sK273(X0,sK246,sK242),sK240) )
| ~ spl294_10
| ~ spl294_23
| ~ spl294_48 ),
inference(resolution,[],[f14175,f1930]) ).
fof(f14506,plain,
( ! [X2,X0,X1] :
( ~ sub(sK273(X0,sK246,sK242),sK240)
| ~ interpretation_succeeds(X0)
| ~ sP260(sK246,X1,X0,X2)
| ~ sub(sK242,X0) )
| ~ spl294_6
| ~ spl294_10
| ~ spl294_23
| ~ spl294_48 ),
inference(forward_subsumption_resolution,[],[f14504,f1750]) ).
fof(f14508,plain,
( ! [X2,X3,X0,X1] :
( ~ interpretation_succeeds(sK240)
| ~ sP260(sK246,X0,sK240,X1)
| ~ sub(sK242,sK240)
| ~ sub(sK242,sK240)
| ~ literal_list_succeeds(sK242)
| ~ interpretation_succeeds(sK240)
| ~ sP260(sK246,X2,sK240,X3) )
| ~ spl294_6
| ~ spl294_10
| ~ spl294_23
| ~ spl294_48 ),
inference(resolution,[],[f14506,f1269]) ).
fof(f14521,plain,
( ! [X2,X3,X0,X1] :
( ~ interpretation_succeeds(sK240)
| ~ sP260(sK246,X0,sK240,X1)
| ~ sub(sK242,sK240)
| ~ literal_list_succeeds(sK242)
| ~ sP260(sK246,X2,sK240,X3) )
| ~ spl294_6
| ~ spl294_10
| ~ spl294_23
| ~ spl294_48 ),
inference(duplicate_literal_removal,[],[f14508]) ).
fof(f14523,plain,
( ! [X2,X3,X0,X1] :
( ~ sP260(sK246,X0,sK240,X1)
| ~ sub(sK242,sK240)
| ~ literal_list_succeeds(sK242)
| ~ sP260(sK246,X2,sK240,X3) )
| ~ spl294_6
| ~ spl294_7
| ~ spl294_10
| ~ spl294_23
| ~ spl294_48 ),
inference(forward_subsumption_resolution,[],[f14521,f1754]) ).
fof(f14525,plain,
( ! [X2,X3,X0,X1] :
( ~ sP260(sK246,X0,sK240,X1)
| ~ literal_list_succeeds(sK242)
| ~ sP260(sK246,X2,sK240,X3) )
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_48 ),
inference(forward_subsumption_resolution,[],[f14523,f1771]) ).
fof(f14527,plain,
( ! [X2,X3,X0,X1] :
( ~ sP260(sK246,X0,sK240,X1)
| ~ sP260(sK246,X2,sK240,X3) )
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_48 ),
inference(forward_subsumption_resolution,[],[f14525,f1750]) ).
fof(f14529,plain,
( $false
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_48 ),
inference(backward_subsumption_resolution,[],[f10809,f14527]) ).
fof(f14530,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_48 ),
inference(avatar_contradiction_clause,[],[f14529]) ).
fof(f14536,plain,
( ! [X0] :
( ~ sub(X0,sK240)
| ~ literal_list_succeeds(X0)
| sub(sK278(sK240,sK249,X0),sK240)
| ~ interpretation_succeeds(sK240) )
| ~ spl294_10
| ~ spl294_47 ),
inference(resolution,[],[f10855,f1263]) ).
fof(f14543,plain,
( ! [X0] :
( sub(sK278(sK240,sK249,X0),sK240)
| ~ literal_list_succeeds(X0)
| ~ sub(X0,sK240) )
| ~ spl294_7
| ~ spl294_10
| ~ spl294_47 ),
inference(forward_subsumption_resolution,[],[f14536,f1754]) ).
fof(f14578,plain,
( ! [X0,X1] :
( ~ false_succeeds(sK249,X0,X1)
| false_succeeds(sK239,X0,X1) )
| ~ spl294_10
| ~ spl294_47 ),
inference(superposition,[],[f1170,f10858]) ).
fof(f14613,plain,
( ! [X2,X3,X0,X1,X4] :
( false_succeeds(sK239,X0,sK278(X1,sK249,X0))
| ~ sub(X0,X1)
| ~ literal_list_succeeds(X0)
| ~ interpretation_succeeds(X1)
| ~ sP262(X2,sK249,X3,X1,X4) )
| ~ spl294_10
| ~ spl294_47 ),
inference(resolution,[],[f14578,f1262]) ).
fof(f14883,plain,
( ! [X2,X3,X0,X1] :
( ~ sub(sK242,X0)
| ~ literal_list_succeeds(sK242)
| ~ interpretation_succeeds(X0)
| ~ sP262(X1,sK249,X2,X0,X3)
| ~ sub(sK278(X0,sK249,sK242),sK240) )
| ~ spl294_10
| ~ spl294_23
| ~ spl294_47 ),
inference(resolution,[],[f14613,f1930]) ).
fof(f14885,plain,
( ! [X2,X3,X0,X1] :
( ~ sP262(X1,sK249,X2,X0,X3)
| ~ interpretation_succeeds(X0)
| ~ sub(sK242,X0)
| ~ sub(sK278(X0,sK249,sK242),sK240) )
| ~ spl294_6
| ~ spl294_10
| ~ spl294_23
| ~ spl294_47 ),
inference(forward_subsumption_resolution,[],[f14883,f1750]) ).
fof(f14886,plain,
( ~ interpretation_succeeds(sK240)
| ~ sub(sK242,sK240)
| ~ sub(sK278(sK240,sK249,sK242),sK240)
| ~ spl294_6
| ~ spl294_10
| ~ spl294_23
| ~ spl294_47 ),
inference(resolution,[],[f14885,f10855]) ).
fof(f14887,plain,
( ~ sub(sK242,sK240)
| ~ sub(sK278(sK240,sK249,sK242),sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_10
| ~ spl294_23
| ~ spl294_47 ),
inference(forward_subsumption_resolution,[],[f14886,f1754]) ).
fof(f14888,plain,
( ~ sub(sK278(sK240,sK249,sK242),sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_47 ),
inference(forward_subsumption_resolution,[],[f14887,f1771]) ).
fof(f14892,plain,
( ~ literal_list_succeeds(sK242)
| ~ sub(sK242,sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_47 ),
inference(resolution,[],[f14888,f14543]) ).
fof(f14908,plain,
( ~ sub(sK242,sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_47 ),
inference(forward_subsumption_resolution,[],[f14892,f1750]) ).
fof(f14909,plain,
( $false
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_47 ),
inference(forward_subsumption_resolution,[],[f14908,f1771]) ).
fof(f14910,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_47 ),
inference(avatar_contradiction_clause,[],[f14909]) ).
fof(f14916,plain,
( ! [X0] :
( ~ sub(X0,sK240)
| ~ literal_list_succeeds(X0)
| sub(sK280(sK240,sK252,X0),sK240)
| ~ interpretation_succeeds(sK240) )
| ~ spl294_10
| ~ spl294_46 ),
inference(resolution,[],[f11007,f1261]) ).
fof(f14923,plain,
( ! [X0] :
( sub(sK280(sK240,sK252,X0),sK240)
| ~ literal_list_succeeds(X0)
| ~ sub(X0,sK240) )
| ~ spl294_7
| ~ spl294_10
| ~ spl294_46 ),
inference(forward_subsumption_resolution,[],[f14916,f1754]) ).
fof(f14981,plain,
( ! [X0,X1] :
( ~ false_succeeds(sK252,X0,X1)
| false_succeeds(sK239,X0,X1) )
| ~ spl294_10
| ~ spl294_46 ),
inference(superposition,[],[f3399,f11073]) ).
fof(f15005,plain,
( ! [X2,X3,X0,X1,X4] :
( false_succeeds(sK239,X0,sK280(X1,sK252,X0))
| ~ sub(X0,X1)
| ~ literal_list_succeeds(X0)
| ~ interpretation_succeeds(X1)
| ~ sP263(sK252,X2,X3,X1,X4) )
| ~ spl294_10
| ~ spl294_46 ),
inference(resolution,[],[f14981,f1260]) ).
fof(f15210,plain,
( ! [X2,X3,X0,X1] :
( ~ sub(sK242,X0)
| ~ literal_list_succeeds(sK242)
| ~ interpretation_succeeds(X0)
| ~ sP263(sK252,X1,X2,X0,X3)
| ~ sub(sK280(X0,sK252,sK242),sK240) )
| ~ spl294_10
| ~ spl294_23
| ~ spl294_46 ),
inference(resolution,[],[f15005,f1930]) ).
fof(f15212,plain,
( ! [X2,X3,X0,X1] :
( ~ sP263(sK252,X1,X2,X0,X3)
| ~ interpretation_succeeds(X0)
| ~ sub(sK242,X0)
| ~ sub(sK280(X0,sK252,sK242),sK240) )
| ~ spl294_6
| ~ spl294_10
| ~ spl294_23
| ~ spl294_46 ),
inference(forward_subsumption_resolution,[],[f15210,f1750]) ).
fof(f15213,plain,
( ~ interpretation_succeeds(sK240)
| ~ sub(sK242,sK240)
| ~ sub(sK280(sK240,sK252,sK242),sK240)
| ~ spl294_6
| ~ spl294_10
| ~ spl294_23
| ~ spl294_46 ),
inference(resolution,[],[f15212,f11007]) ).
fof(f15214,plain,
( ~ sub(sK242,sK240)
| ~ sub(sK280(sK240,sK252,sK242),sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_10
| ~ spl294_23
| ~ spl294_46 ),
inference(forward_subsumption_resolution,[],[f15213,f1754]) ).
fof(f15215,plain,
( ~ sub(sK280(sK240,sK252,sK242),sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_46 ),
inference(forward_subsumption_resolution,[],[f15214,f1771]) ).
fof(f15219,plain,
( ~ literal_list_succeeds(sK242)
| ~ sub(sK242,sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_46 ),
inference(resolution,[],[f15215,f14923]) ).
fof(f15235,plain,
( ~ sub(sK242,sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_46 ),
inference(forward_subsumption_resolution,[],[f15219,f1750]) ).
fof(f15236,plain,
( $false
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_46 ),
inference(forward_subsumption_resolution,[],[f15235,f1771]) ).
fof(f15237,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_46 ),
inference(avatar_contradiction_clause,[],[f15236]) ).
fof(f15243,plain,
( ! [X0] :
( ~ sub(X0,sK240)
| ~ literal_list_succeeds(X0)
| sub(sK288(sK240,sK257,X0),sK240)
| ~ interpretation_succeeds(sK240) )
| ~ spl294_10
| ~ spl294_45 ),
inference(resolution,[],[f11152,f1253]) ).
fof(f15244,plain,
( ! [X0] :
( ~ sub(X0,sK240)
| ~ literal_list_succeeds(X0)
| sub(sK286(sK240,sK258,X0),sK240)
| ~ interpretation_succeeds(sK240) )
| ~ spl294_10
| ~ spl294_45 ),
inference(resolution,[],[f11152,f1255]) ).
fof(f15255,plain,
( ! [X0] :
( sub(sK286(sK240,sK258,X0),sK240)
| ~ literal_list_succeeds(X0)
| ~ sub(X0,sK240) )
| ~ spl294_7
| ~ spl294_10
| ~ spl294_45 ),
inference(forward_subsumption_resolution,[],[f15244,f1754]) ).
fof(f15256,plain,
( ! [X0] :
( sub(sK288(sK240,sK257,X0),sK240)
| ~ literal_list_succeeds(X0)
| ~ sub(X0,sK240) )
| ~ spl294_7
| ~ spl294_10
| ~ spl294_45 ),
inference(forward_subsumption_resolution,[],[f15243,f1754]) ).
fof(f15334,plain,
( ! [X2,X0,X1] :
( ~ false_succeeds(sK258,X2,X1)
| false_succeeds(sK239,X0,X1)
| ~ false_succeeds(sK257,X0,X2) )
| ~ spl294_10
| ~ spl294_45 ),
inference(superposition,[],[f4764,f11217]) ).
fof(f15930,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( false_succeeds(sK239,X0,sK286(X1,sK258,X2))
| ~ false_succeeds(sK257,X0,X2)
| ~ sub(X2,X1)
| ~ literal_list_succeeds(X2)
| ~ interpretation_succeeds(X1)
| ~ sP266(sK258,X3,X4,X1,X5) )
| ~ spl294_10
| ~ spl294_45 ),
inference(resolution,[],[f15334,f1254]) ).
fof(f15949,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ sP266(sK258,X2,X3,X1,X4)
| ~ sub(X0,X1)
| ~ literal_list_succeeds(X0)
| ~ interpretation_succeeds(X1)
| ~ false_succeeds(sK257,sK242,X0)
| ~ sub(sK286(X1,sK258,X0),sK240) )
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(resolution,[],[f15930,f1930]) ).
fof(f15951,plain,
( ! [X0] :
( ~ sub(X0,sK240)
| ~ literal_list_succeeds(X0)
| ~ interpretation_succeeds(sK240)
| ~ false_succeeds(sK257,sK242,X0)
| ~ sub(sK286(sK240,sK258,X0),sK240) )
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(resolution,[],[f15949,f11152]) ).
fof(f15952,plain,
( ! [X0] :
( ~ sub(X0,sK240)
| ~ literal_list_succeeds(X0)
| ~ interpretation_succeeds(sK240)
| ~ false_succeeds(sK257,sK242,X0) )
| ~ spl294_7
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(forward_subsumption_resolution,[],[f15951,f15255]) ).
fof(f15953,plain,
( ! [X0] :
( ~ false_succeeds(sK257,sK242,X0)
| ~ literal_list_succeeds(X0)
| ~ sub(X0,sK240) )
| ~ spl294_7
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(forward_subsumption_resolution,[],[f15952,f1754]) ).
fof(f15963,plain,
( ! [X2,X3,X0,X1] :
( ~ literal_list_succeeds(sK288(X0,sK257,sK242))
| ~ sub(sK288(X0,sK257,sK242),sK240)
| ~ sub(sK242,X0)
| ~ literal_list_succeeds(sK242)
| ~ interpretation_succeeds(X0)
| ~ sP266(X1,sK257,X2,X0,X3) )
| ~ spl294_7
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(resolution,[],[f15953,f1252]) ).
fof(f15964,plain,
( ! [X2,X3,X0,X1] :
( ~ sub(sK288(X0,sK257,sK242),sK240)
| ~ sub(sK242,X0)
| ~ literal_list_succeeds(sK242)
| ~ interpretation_succeeds(X0)
| ~ sP266(X1,sK257,X2,X0,X3) )
| ~ spl294_7
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(forward_subsumption_resolution,[],[f15963,f1779]) ).
fof(f15973,plain,
( ! [X2,X3,X0,X1] :
( ~ sP266(X1,sK257,X2,X0,X3)
| ~ sub(sK242,X0)
| ~ interpretation_succeeds(X0)
| ~ sub(sK288(X0,sK257,sK242),sK240) )
| ~ spl294_6
| ~ spl294_7
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(forward_subsumption_resolution,[],[f15964,f1750]) ).
fof(f15977,plain,
( ~ sub(sK242,sK240)
| ~ interpretation_succeeds(sK240)
| ~ sub(sK288(sK240,sK257,sK242),sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(resolution,[],[f15973,f11152]) ).
fof(f15978,plain,
( ~ interpretation_succeeds(sK240)
| ~ sub(sK288(sK240,sK257,sK242),sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(forward_subsumption_resolution,[],[f15977,f1771]) ).
fof(f15979,plain,
( ~ sub(sK288(sK240,sK257,sK242),sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(forward_subsumption_resolution,[],[f15978,f1754]) ).
fof(f15983,plain,
( ~ literal_list_succeeds(sK242)
| ~ sub(sK242,sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(resolution,[],[f15979,f15256]) ).
fof(f15999,plain,
( ~ sub(sK242,sK240)
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(forward_subsumption_resolution,[],[f15983,f1750]) ).
fof(f16000,plain,
( $false
| ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(forward_subsumption_resolution,[],[f15999,f1771]) ).
fof(f16001,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(avatar_contradiction_clause,[],[f16000]) ).
cnf(s797,plain,
( spl294_1
| spl294_2 ),
inference(sat_conversion,[],[f1723]) ).
cnf(s801,plain,
( spl294_2
| spl294_3 ),
inference(sat_conversion,[],[f1729]) ).
cnf(s802,plain,
( spl294_1
| spl294_4 ),
inference(sat_conversion,[],[f1733]) ).
cnf(s809,plain,
( spl294_5
| spl294_6 ),
inference(sat_conversion,[],[f1751]) ).
cnf(s811,plain,
( spl294_5
| spl294_7 ),
inference(sat_conversion,[],[f1755]) ).
cnf(s817,plain,
( spl294_5
| spl294_8 ),
inference(sat_conversion,[],[f1772]) ).
cnf(s841,plain,
( spl294_5
| spl294_9
| spl294_10 ),
inference(sat_conversion,[],[f1816]) ).
cnf(s869,plain,
( spl294_5
| spl294_10
| spl294_20 ),
inference(sat_conversion,[],[f1891]) ).
cnf(s886,plain,
( spl294_3
| spl294_4 ),
inference(sat_conversion,[],[f1914]) ).
cnf(s889,plain,
( spl294_5
| spl294_9
| spl294_23 ),
inference(sat_conversion,[],[f1931]) ).
cnf(s968,plain,
~ spl294_11,
inference(sat_conversion,[],[f2084]) ).
cnf(s1077,plain,
( spl294_5
| spl294_10
| spl294_40
| spl294_41
| spl294_42
| spl294_43
| spl294_44 ),
inference(sat_conversion,[],[f2298]) ).
cnf(s1095,plain,
( spl294_5
| spl294_9
| spl294_45
| spl294_46
| spl294_47
| spl294_48
| spl294_49 ),
inference(sat_conversion,[],[f2348]) ).
cnf(s1197,plain,
( spl294_5
| spl294_10
| spl294_40
| spl294_41
| spl294_42
| spl294_43
| spl294_51 ),
inference(sat_conversion,[],[f2519]) ).
cnf(s1223,plain,
( ~ spl294_1
| ~ spl294_3
| ~ spl294_5 ),
inference(sat_conversion,[],[f2585]) ).
cnf(s1241,plain,
( ~ spl294_2
| ~ spl294_4
| ~ spl294_5 ),
inference(sat_conversion,[],[f2622]) ).
cnf(s1280,plain,
( ~ spl294_9
| ~ spl294_10
| spl294_11 ),
inference(sat_conversion,[],[f2668]) ).
cnf(s1313,plain,
( ~ spl294_23
| ~ spl294_49
| ~ spl294_53
| ~ spl294_54 ),
inference(sat_conversion,[],[f2729]) ).
cnf(s1316,plain,
( ~ spl294_8
| ~ spl294_49
| ~ spl294_50
| spl294_53 ),
inference(sat_conversion,[],[f2735]) ).
cnf(s1371,plain,
( spl294_5
| spl294_9
| spl294_45
| spl294_46
| spl294_47
| spl294_48
| spl294_50 ),
inference(sat_conversion,[],[f2876]) ).
cnf(s2504,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| spl294_58 ),
inference(sat_conversion,[],[f5014]) ).
cnf(s4227,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| spl294_11
| ~ spl294_49
| ~ spl294_50
| spl294_54 ),
inference(sat_conversion,[],[f9567]) ).
cnf(s4540,plain,
( ~ spl294_20
| ~ spl294_68
| ~ spl294_105
| ~ spl294_106 ),
inference(sat_conversion,[],[f10417]) ).
cnf(s4543,plain,
( ~ spl294_8
| ~ spl294_44
| ~ spl294_51
| spl294_105 ),
inference(sat_conversion,[],[f10437]) ).
cnf(s4557,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_44
| ~ spl294_51
| ~ spl294_68
| spl294_106 ),
inference(sat_conversion,[],[f10491]) ).
cnf(s4593,plain,
( spl294_68
| ~ spl294_93 ),
inference(sat_conversion,[],[f10498]) ).
cnf(s4722,plain,
( ~ spl294_44
| spl294_93 ),
inference(sat_conversion,[],[f10808]) ).
cnf(s5510,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_43 ),
inference(sat_conversion,[],[f12452]) ).
cnf(s5717,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_41 ),
inference(sat_conversion,[],[f12833]) ).
cnf(s6062,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_42
| ~ spl294_126
| ~ spl294_127 ),
inference(sat_conversion,[],[f13530]) ).
cnf(s6068,plain,
( ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_42
| ~ spl294_58
| spl294_126 ),
inference(sat_conversion,[],[f13544]) ).
cnf(s6075,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_42
| spl294_127 ),
inference(sat_conversion,[],[f13566]) ).
cnf(s6283,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_9
| ~ spl294_20
| ~ spl294_40 ),
inference(sat_conversion,[],[f14066]) ).
cnf(s6489,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_48 ),
inference(sat_conversion,[],[f14530]) ).
cnf(s6685,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_47 ),
inference(sat_conversion,[],[f14910]) ).
cnf(s6855,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_46 ),
inference(sat_conversion,[],[f15237]) ).
cnf(s7170,plain,
( ~ spl294_6
| ~ spl294_7
| ~ spl294_8
| ~ spl294_10
| ~ spl294_23
| ~ spl294_45 ),
inference(sat_conversion,[],[f16001]) ).
cnf(s7171,plain,
( spl294_9
| spl294_5 ),
inference(rat,[],[s1313,s4227,s1316,s1095,s1371,s6489,s6685,s6855,s7170,s841,s889,s817,s811,s809,s968]) ).
cnf(s7173,plain,
( spl294_42
| spl294_5 ),
inference(rat,[],[s4557,s4540,s4593,s4543,s4722,s1197,s1077,s6283,s5717,s5510,s869,s1280,s817,s811,s809,s7171,s968]) ).
cnf(s7174,plain,
spl294_5,
inference(rat,[],[s6062,s6075,s6068,s7173,s869,s1280,s7171,s2504,s809,s811,s817,s968]) ).
cnf(s7175,plain,
spl294_1,
inference(rat,[],[s1241,s797,s802,s7174]) ).
cnf(s7177,plain,
~ spl294_3,
inference(rat,[],[s1223,s7174,s7175]) ).
cnf(s7178,plain,
spl294_4,
inference(rat,[],[s886,s7177]) ).
cnf(s7179,plain,
spl294_2,
inference(rat,[],[s801,s7177]) ).
cnf(s7180,plain,
$false,
inference(rat,[],[s1241,s7174,s7178,s7179]) ).
fof(f16002,plain,
$false,
inference(avatar_sat_refutation,[],[s7180]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX071+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n001.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 15:03:33 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.02/2.79 % (413108)Detected formulas, will run a generic FOF schedule.
% 14.02/2.79 % (413114)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=56063921:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 14.02/2.79 % (413118)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1845570196:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 14.02/2.79 % (413117)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1144287725:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 14.02/2.79 % (413115)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=3083981953:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 14.02/2.79 % (413113)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=1983360829:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 14.02/2.79 % (413116)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3106491878:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 14.02/2.79 % (413119)dis-21_1_sil=8000:lcm=predicate:random_seed=2310275921: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)
% 14.02/2.79 % (413119)Instruction limit reached!
% 14.02/2.79 % (413119)------------------------------
% 14.02/2.79 % (413119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.79 % (413119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.79 % (413119)CaDiCaL version: 2.1.3
% 14.02/2.79 % (413119)Termination reason: Instruction limit
% 14.02/2.79 % (413119)Termination phase: Saturation
% 14.02/2.79 % (413119)Time elapsed: 0.060 s
% 14.02/2.79 % (413119)Peak memory usage: 90 MB
% 14.02/2.79 % (413119)Instructions burned: 129 (million)
% 14.02/2.79 % (413116)Instruction limit reached!
% 14.02/2.79 % (413116)------------------------------
% 14.02/2.79 % (413116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.79 % (413116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.79 % (413116)CaDiCaL version: 2.1.3
% 14.02/2.79 % (413116)Termination reason: Instruction limit
% 14.02/2.79 % (413116)Termination phase: Saturation
% 14.02/2.79 % (413116)Time elapsed: 0.067 s
% 14.02/2.79 % (413116)Peak memory usage: 90 MB
% 14.02/2.79 % (413116)Instructions burned: 112 (million)
% 14.02/2.79 % (413117)Instruction limit reached!
% 14.02/2.79 % (413117)------------------------------
% 14.02/2.79 % (413117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.79 % (413117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.79 % (413117)CaDiCaL version: 2.1.3
% 14.02/2.79 % (413117)Termination reason: Instruction limit
% 14.02/2.79 % (413117)Termination phase: Saturation
% 14.02/2.79 % (413117)Time elapsed: 0.073 s
% 14.02/2.79 % (413117)Peak memory usage: 89 MB
% 14.02/2.79 % (413117)Instructions burned: 120 (million)
% 14.02/2.79 % (413118)Instruction limit reached!
% 14.02/2.79 % (413118)------------------------------
% 14.02/2.79 % (413118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.02/2.79 % (413118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.02/2.80 % (413118)CaDiCaL version: 2.1.3
% 14.02/2.80 % (413118)Termination reason: Instruction limit
% 14.02/2.80 % (413118)Termination phase: Saturation
% 14.02/2.80 % (413118)Time elapsed: 0.119 s
% 14.02/2.80 % (413118)Peak memory usage: 91 MB
% 14.02/2.80 % (413118)Instructions burned: 139 (million)
% 14.02/2.80 % (413128)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1498056376:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 14.02/2.80 % (413127)lrs+10_1_sil=8000:sp=occurrence:random_seed=497456142:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 14.02/2.80 % (413129)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1377400401:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 14.02/2.80 % (413130)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1531494716:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 14.02/2.80 % (413128)Instruction limit reached!
% 14.02/2.80 % (413128)------------------------------
% 14.02/2.80 % (413128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.68/3.87 % (413128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.68/3.87 % (413128)CaDiCaL version: 2.1.3
% 21.68/3.87 % (413128)Termination reason: Instruction limit
% 21.68/3.87 % (413128)Termination phase: Saturation
% 21.68/3.87 % (413128)Time elapsed: 0.079 s
% 21.68/3.87 % (413128)Peak memory usage: 90 MB
% 21.68/3.87 % (413128)Instructions burned: 157 (million)
% 21.68/3.87 % (413127)Instruction limit reached!
% 21.68/3.87 % (413127)------------------------------
% 21.68/3.87 % (413127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.68/3.87 % (413127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.68/3.87 % (413127)CaDiCaL version: 2.1.3
% 21.68/3.87 % (413127)Termination reason: Instruction limit
% 21.68/3.87 % (413127)Termination phase: Saturation
% 21.68/3.87 % (413127)Time elapsed: 0.180 s
% 21.68/3.87 % (413127)Peak memory usage: 93 MB
% 21.68/3.87 % (413127)Instructions burned: 285 (million)
% 21.68/3.87 % (413130)Instruction limit reached!
% 21.68/3.87 % (413130)------------------------------
% 21.68/3.87 % (413130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.68/3.87 % (413130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.68/3.87 % (413130)CaDiCaL version: 2.1.3
% 21.68/3.87 % (413130)Termination reason: Instruction limit
% 21.68/3.87 % (413130)Termination phase: Saturation
% 21.68/3.87 % (413130)Time elapsed: 0.135 s
% 21.68/3.87 % (413130)Peak memory usage: 93 MB
% 21.68/3.87 % (413130)Instructions burned: 248 (million)
% 21.68/3.87 % (413129)Instruction limit reached!
% 21.68/3.87 % (413129)------------------------------
% 21.68/3.87 % (413129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.68/3.87 % (413129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.68/3.87 % (413129)CaDiCaL version: 2.1.3
% 21.68/3.87 % (413129)Termination reason: Instruction limit
% 21.68/3.87 % (413129)Termination phase: Saturation
% 21.68/3.87 % (413129)Time elapsed: 0.211 s
% 21.68/3.87 % (413129)Peak memory usage: 93 MB
% 21.68/3.87 % (413129)Instructions burned: 326 (million)
% 21.68/3.87 % (413135)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2982968261:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 21.68/3.87 % (413136)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1077985887:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 21.68/3.87 % (413137)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1619898526:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 21.68/3.87 % (413138)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4229599357:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 21.68/3.87 % (413135)Instruction limit reached!
% 21.68/3.87 % (413135)------------------------------
% 21.68/3.87 % (413135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.68/3.87 % (413135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.68/3.87 % (413135)CaDiCaL version: 2.1.3
% 21.68/3.87 % (413135)Termination reason: Instruction limit
% 21.68/3.87 % (413135)Termination phase: Saturation
% 21.68/3.87 % (413135)Time elapsed: 0.152 s
% 21.68/3.87 % (413135)Peak memory usage: 90 MB
% 21.68/3.87 % (413135)Instructions burned: 294 (million)
% 21.68/3.87 % (413137)Instruction limit reached!
% 21.68/3.87 % (413137)------------------------------
% 21.68/3.87 % (413137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.68/3.87 % (413137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.68/3.87 % (413137)CaDiCaL version: 2.1.3
% 21.68/3.87 % (413137)Termination reason: Instruction limit
% 21.68/3.87 % (413137)Termination phase: Saturation
% 21.68/3.87 % (413137)Time elapsed: 0.070 s
% 21.68/3.87 % (413137)Peak memory usage: 91 MB
% 21.68/3.87 % (413137)Instructions burned: 114 (million)
% 21.68/3.87 % (413138)Instruction limit reached!
% 21.68/3.87 % (413138)------------------------------
% 21.68/3.87 % (413138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.68/3.87 % (413138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.68/3.87 % (413138)CaDiCaL version: 2.1.3
% 21.68/3.87 % (413138)Termination reason: Instruction limit
% 21.68/3.87 % (413138)Termination phase: Saturation
% 21.68/3.87 % (413138)Time elapsed: 0.066 s
% 21.68/3.87 % (413138)Peak memory usage: 90 MB
% 21.68/3.87 % (413138)Instructions burned: 129 (million)
% 19.48/6.92 % (413143)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=396370889:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 19.48/6.92 % (413144)lrs+10_1_sil=8000:sp=occurrence:random_seed=2944502024:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 19.48/6.92 % (413145)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1843355672:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 19.48/6.92 % (413143)Instruction limit reached!
% 19.48/6.92 % (413143)------------------------------
% 19.48/6.92 % (413143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.92 % (413143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.92 % (413143)CaDiCaL version: 2.1.3
% 19.48/6.92 % (413143)Termination reason: Instruction limit
% 19.48/6.92 % (413143)Termination phase: Clausification
% 19.48/6.92 % (413143)Time elapsed: 0.109 s
% 19.48/6.92 % (413143)Peak memory usage: 142 MB
% 19.48/6.92 % (413143)Instructions burned: 114 (million)
% 19.48/6.92 % (413149)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1130449960:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 19.48/6.93 % (413145)Instruction limit reached!
% 19.48/6.93 % (413145)------------------------------
% 19.48/6.93 % (413145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.93 % (413145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.93 % (413145)CaDiCaL version: 2.1.3
% 19.48/6.93 % (413145)Termination reason: Instruction limit
% 19.48/6.93 % (413145)Termination phase: Saturation
% 19.48/6.93 % (413145)Time elapsed: 0.228 s
% 19.48/6.93 % (413145)Peak memory usage: 91 MB
% 19.48/6.93 % (413145)Instructions burned: 437 (million)
% 19.48/6.93 % (413151)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2445710990:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 19.48/6.93 % (413151)Instruction limit reached!
% 19.48/6.93 % (413151)------------------------------
% 19.48/6.93 % (413151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.93 % (413151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.93 % (413151)CaDiCaL version: 2.1.3
% 19.48/6.93 % (413151)Termination reason: Instruction limit
% 19.48/6.93 % (413151)Termination phase: Saturation
% 19.48/6.93 % (413151)Time elapsed: 0.070 s
% 19.48/6.93 % (413151)Peak memory usage: 91 MB
% 19.48/6.93 % (413151)Instructions burned: 134 (million)
% 19.48/6.93 % (413144)Instruction limit reached!
% 19.48/6.93 % (413144)------------------------------
% 19.48/6.93 % (413144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.93 % (413144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.93 % (413144)CaDiCaL version: 2.1.3
% 19.48/6.93 % (413144)Termination reason: Instruction limit
% 19.48/6.93 % (413144)Termination phase: Saturation
% 19.48/6.93 % (413144)Time elapsed: 0.571 s
% 19.48/6.93 % (413144)Peak memory usage: 101 MB
% 19.48/6.93 % (413144)Instructions burned: 908 (million)
% 19.48/6.93 % (413153)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3958916950:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 19.48/6.93 % (413154)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1820650214:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 19.48/6.93 % (413153)Instruction limit reached!
% 19.48/6.93 % (413153)------------------------------
% 19.48/6.93 % (413153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.93 % (413153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.93 % (413153)CaDiCaL version: 2.1.3
% 19.48/6.93 % (413153)Termination reason: Instruction limit
% 19.48/6.93 % (413153)Termination phase: Saturation
% 19.48/6.93 % (413153)Time elapsed: 0.241 s
% 19.48/6.93 % (413153)Peak memory usage: 91 MB
% 19.48/6.93 % (413153)Instructions burned: 594 (million)
% 19.48/6.93 % (413157)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=560700609:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 19.48/6.93 % (413157)Instruction limit reached!
% 19.48/6.93 % (413157)------------------------------
% 19.48/6.93 % (413157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.93 % (413157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.93 % (413157)CaDiCaL version: 2.1.3
% 19.48/6.93 % (413157)Termination reason: Instruction limit
% 19.48/6.93 % (413157)Termination phase: Saturation
% 19.48/6.93 % (413157)Time elapsed: 0.077 s
% 19.48/6.93 % (413157)Peak memory usage: 91 MB
% 19.48/6.93 % (413157)Instructions burned: 125 (million)
% 19.48/6.93 % (413136)Instruction limit reached!
% 19.48/6.93 % (413136)------------------------------
% 19.48/6.93 % (413136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.93 % (413136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.93 % (413136)CaDiCaL version: 2.1.3
% 19.48/6.93 % (413136)Termination reason: Instruction limit
% 19.48/6.93 % (413136)Termination phase: Saturation
% 19.48/6.93 % (413136)Time elapsed: 1.496 s
% 19.48/6.93 % (413136)Peak memory usage: 143 MB
% 19.48/6.93 % (413136)Instructions burned: 2350 (million)
% 19.48/6.93 % (413159)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=631214998:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 19.48/6.93 % (413159)Instruction limit reached!
% 19.48/6.93 % (413159)------------------------------
% 19.48/6.93 % (413159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.93 % (413159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.93 % (413159)CaDiCaL version: 2.1.3
% 19.48/6.93 % (413159)Termination reason: Instruction limit
% 19.48/6.93 % (413159)Termination phase: Saturation
% 19.48/6.93 % (413159)Time elapsed: 0.083 s
% 19.48/6.93 % (413159)Peak memory usage: 91 MB
% 19.48/6.93 % (413159)Instructions burned: 135 (million)
% 19.48/6.93 % (413160)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2567874159:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 19.48/6.93 % (413160)Instruction limit reached!
% 19.48/6.93 % (413160)------------------------------
% 19.48/6.93 % (413160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.93 % (413160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.93 % (413160)CaDiCaL version: 2.1.3
% 19.48/6.93 % (413160)Termination reason: Instruction limit
% 19.48/6.93 % (413160)Termination phase: Saturation
% 19.48/6.93 % (413160)Time elapsed: 0.057 s
% 19.48/6.93 % (413160)Peak memory usage: 89 MB
% 19.48/6.93 % (413160)Instructions burned: 141 (million)
% 19.48/6.93 % (413162)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3558589188:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 19.48/6.93 % (413164)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=827726525:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 19.48/6.93 % (413162)Instruction limit reached!
% 19.48/6.93 % (413162)------------------------------
% 19.48/6.93 % (413162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.93 % (413162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.93 % (413162)CaDiCaL version: 2.1.3
% 19.48/6.93 % (413162)Termination reason: Instruction limit
% 19.48/6.93 % (413162)Termination phase: Saturation
% 19.48/6.93 % (413162)Time elapsed: 0.241 s
% 19.48/6.93 % (413162)Peak memory usage: 92 MB
% 19.48/6.93 % (413162)Instructions burned: 432 (million)
% 19.48/6.93 % (413167)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2651441935:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 19.48/6.93 % (413167)Instruction limit reached!
% 19.48/6.93 % (413167)------------------------------
% 19.48/6.93 % (413167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.93 % (413167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.93 % (413167)CaDiCaL version: 2.1.3
% 19.48/6.93 % (413167)Termination reason: Instruction limit
% 19.48/6.93 % (413167)Termination phase: Saturation
% 19.48/6.93 % (413167)Time elapsed: 0.087 s
% 19.48/6.93 % (413167)Peak memory usage: 91 MB
% 19.48/6.93 % (413167)Instructions burned: 151 (million)
% 19.48/6.93 % (413169)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3259472704:i=14155:bd=all_2969 on theBenchmark for (2969ds/14155Mi)
% 19.48/6.93 % (413149)Instruction limit reached!
% 19.48/6.93 % (413149)------------------------------
% 19.48/6.93 % (413149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.93 % (413149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.93 % (413149)CaDiCaL version: 2.1.3
% 19.48/6.93 % (413149)Termination reason: Instruction limit
% 19.48/6.93 % (413149)Termination phase: Saturation
% 19.48/6.93 % (413149)Time elapsed: 3.229 s
% 19.48/6.93 % (413149)Peak memory usage: 165 MB
% 19.48/6.93 % (413149)Instructions burned: 5202 (million)
% 19.48/6.93 % (413171)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3970843349:i=667:av=off:fsr=off_2955 on theBenchmark for (2955ds/667Mi)
% 19.48/6.93 % (413171)Instruction limit reached!
% 19.48/6.93 % (413171)------------------------------
% 19.48/6.93 % (413171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.93 % (413171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.93 % (413171)CaDiCaL version: 2.1.3
% 19.48/6.93 % (413171)Termination reason: Instruction limit
% 19.48/6.93 % (413171)Termination phase: Saturation
% 19.48/6.93 % (413171)Time elapsed: 0.295 s
% 19.48/6.93 % (413171)Peak memory usage: 97 MB
% 19.48/6.93 % (413171)Instructions burned: 668 (million)
% 19.48/6.93 % (413173)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3919908148:s2a=on:i=185:s2at=1.8:fdi=4_2950 on theBenchmark for (2950ds/185Mi)
% 19.48/6.93 % (413173)Instruction limit reached!
% 19.48/6.93 % (413173)------------------------------
% 19.48/6.93 % (413173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.93 % (413173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.93 % (413173)CaDiCaL version: 2.1.3
% 19.48/6.93 % (413173)Termination reason: Instruction limit
% 19.48/6.93 % (413173)Termination phase: Saturation
% 19.48/6.93 % (413173)Time elapsed: 0.102 s
% 19.48/6.93 % (413173)Peak memory usage: 92 MB
% 19.48/6.93 % (413173)Instructions burned: 185 (million)
% 19.48/6.93 % (413175)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=580213228:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2947 on theBenchmark for (2947ds/193Mi)
% 19.48/6.93 % (413175)Instruction limit reached!
% 19.48/6.93 % (413175)------------------------------
% 19.48/6.93 % (413175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.48/6.93 % (413175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.48/6.93 % (413175)CaDiCaL version: 2.1.3
% 19.48/6.93 % (413175)Termination reason: Instruction limit
% 19.48/6.93 % (413175)Termination phase: Saturation
% 19.48/6.93 % (413175)Time elapsed: 0.122 s
% 19.48/6.93 % (413175)Peak memory usage: 91 MB
% 19.48/6.93 % (413175)Instructions burned: 194 (million)
% 19.48/6.93 % (413177)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2949252326:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2945 on theBenchmark for (2945ds/4850Mi)
% 19.48/6.93 % (413164)First to succeed.
% 19.48/6.93 % (413164)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-413108"
% 19.48/6.93 % (413164)Refutation found. Thanks to Tanya!
% 19.48/6.93 % SZS status Theorem for theBenchmark
% 19.48/6.93 % SZS output start Proof for theBenchmark
% See solution above
% 44.70/7.07 % (413164)------------------------------
% 44.70/7.07 % (413164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.70/7.07 % (413164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.70/7.07 % (413164)CaDiCaL version: 2.1.3
% 44.70/7.07 % (413164)Termination reason: Refutation
% 44.70/7.07 % (413164)Time elapsed: 3.330 s
% 44.70/7.07 % (413164)Peak memory usage: 163 MB
% 44.70/7.07 % (413164)Instructions burned: 4889 (million)
% 44.70/7.07 % (413164)------------------------------
% 44.70/7.07 % (413164)------------------------------
% 44.70/7.07 % (413108)Success in time 6.235 s
% 44.70/7.07 % Vampire exiting
%------------------------------------------------------------------------------