%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX067+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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:48 PM UTC 2026
% Result : Theorem 69.53s 19.35s
% Output : Refutation 131.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 57
% Syntax : Number of formulae : 549 ( 50 unt; 40 def)
% Number of atoms : 2267 ( 492 equ)
% Maximal formula atoms : 55 ( 4 avg)
% Number of connectives : 2816 (1098 ~;1339 |; 306 &)
% ( 43 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 49 ( 46 usr; 29 prp; 0-3 aty)
% Number of functors : 39 ( 39 usr; 10 con; 0-3 aty)
% Number of variables : 821 ( 0 sgn 728 !; 93 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f16,axiom,
'1' != '0',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id16) ).
fof(f26,axiom,
! [X0,X1] : p(X0) != neg(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id26) ).
fof(f27,axiom,
! [X0,X1,X2] : p(X0) != and(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id27) ).
fof(f28,axiom,
! [X0,X1,X2] : p(X0) != or(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id28) ).
fof(f29,axiom,
! [X0,X1] :
( neg(X0) = neg(X1)
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id29) ).
fof(f30,axiom,
! [X0,X1,X2] : neg(X0) != and(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id30) ).
fof(f31,axiom,
! [X0,X1,X2] : neg(X0) != or(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id31) ).
fof(f32,axiom,
! [X0,X1,X2,X3] :
( and(X0,X1) = and(X2,X3)
=> X1 = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id32) ).
fof(f33,axiom,
! [X0,X1,X2,X3] :
( and(X0,X1) = and(X2,X3)
=> X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id33) ).
fof(f34,axiom,
! [X0,X1,X2,X3] : and(X0,X1) != or(X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id34) ).
fof(f35,axiom,
! [X0,X1,X2,X3] :
( or(X0,X1) = or(X2,X3)
=> X1 = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id35) ).
fof(f36,axiom,
! [X0,X1,X2,X3] :
( or(X0,X1) = or(X2,X3)
=> X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id36) ).
fof(f76,axiom,
! [X0,X1,X2] :
( eval_terminates(X0,X1,X2)
<=> ( ! [X3,X4] :
( $true
& ( X0 != or(X3,X4)
| ( $true
& ( X2 != '0'
| ( eval_terminates(X3,X1,'0')
& ( eval_fails(X3,X1,'0')
| eval_terminates(X4,X1,'0') ) ) ) ) ) )
& ! [X5,X6] :
( $true
& ( X0 != or(X5,X6)
| ( $true
& ( X2 != '1'
| eval_terminates(X6,X1,'1') ) ) ) )
& ! [X7,X8] :
( $true
& ( X0 != or(X7,X8)
| ( $true
& ( X2 != '1'
| eval_terminates(X7,X1,'1') ) ) ) )
& ! [X9,X10] :
( $true
& ( X0 != and(X9,X10)
| ( $true
& ( X2 != '0'
| eval_terminates(X10,X1,'0') ) ) ) )
& ! [X11,X12] :
( $true
& ( X0 != and(X11,X12)
| ( $true
& ( X2 != '0'
| eval_terminates(X11,X1,'0') ) ) ) )
& ! [X13,X14] :
( $true
& ( X0 != and(X13,X14)
| ( $true
& ( X2 != '1'
| ( eval_terminates(X13,X1,'1')
& ( eval_fails(X13,X1,'1')
| eval_terminates(X14,X1,'1') ) ) ) ) ) )
& ! [X15] :
( $true
& ( X0 != neg(X15)
| ( $true
& ( X2 != '0'
| eval_terminates(X15,X1,'1') ) ) ) )
& ! [X16] :
( $true
& ( X0 != neg(X16)
| ( $true
& ( X2 != '1'
| eval_terminates(X16,X1,'0') ) ) ) )
& ! [X17] :
( $true
& ( X0 != p(X17)
| ( $true
& ( X2 != '0'
| member_terminates(neg(p(X17)),X1) ) ) ) )
& ! [X18] :
( $true
& ( X0 != p(X18)
| ( $true
& ( X2 != '1'
| member_terminates(p(X18),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id76) ).
fof(f104,axiom,
! [X0,X1] :
( member_succeeds(X0,X1)
<=> ( ? [X2,X3] :
( X1 = cons(X2,X3)
& member_succeeds(X0,X3) )
| ? [X4] : X1 = cons(X0,X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id104) ).
fof(f111,axiom,
! [X0,X1] :
( list_succeeds(X1)
=> member_terminates(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(member:termination)') ).
fof(f139,axiom,
( ! [X0] :
( ( ? [X1,X2] :
( X0 = or(X1,X2)
& formula_succeeds(X1)
& ! [X3,X4] :
( list_succeeds(X3)
=> eval_terminates(X1,X3,X4) )
& formula_succeeds(X2)
& ! [X3,X4] :
( list_succeeds(X3)
=> eval_terminates(X2,X3,X4) ) )
| ? [X5,X6] :
( X0 = and(X5,X6)
& formula_succeeds(X5)
& ! [X3,X4] :
( list_succeeds(X3)
=> eval_terminates(X5,X3,X4) )
& formula_succeeds(X6)
& ! [X3,X4] :
( list_succeeds(X3)
=> eval_terminates(X6,X3,X4) ) )
| ? [X7] :
( X0 = neg(X7)
& formula_succeeds(X7)
& ! [X3,X4] :
( list_succeeds(X3)
=> eval_terminates(X7,X3,X4) ) )
| ? [X8] : X0 = p(X8) )
=> ! [X3,X4] :
( list_succeeds(X3)
=> eval_terminates(X0,X3,X4) ) )
=> ! [X0] :
( formula_succeeds(X0)
=> ! [X3,X4] :
( list_succeeds(X3)
=> eval_terminates(X0,X3,X4) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',induction) ).
fof(f140,conjecture,
! [X0] :
( formula_succeeds(X0)
=> ! [X1,X2] :
( list_succeeds(X1)
=> eval_terminates(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(eval:termination)') ).
fof(f141,negated_conjecture,
~ ! [X0] :
( formula_succeeds(X0)
=> ! [X1,X2] :
( list_succeeds(X1)
=> eval_terminates(X0,X1,X2) ) ),
inference(negated_conjecture,[status(cth)],[f140]) ).
fof(f143,plain,
! [X0,X1,X2] :
( eval_terminates(X0,X1,X2)
<=> ( ! [X3,X4] :
( X0 != or(X3,X4)
| X2 != '0'
| ( eval_terminates(X3,X1,'0')
& ( eval_fails(X3,X1,'0')
| eval_terminates(X4,X1,'0') ) ) )
& ! [X5,X6] :
( X0 != or(X5,X6)
| X2 != '1'
| eval_terminates(X6,X1,'1') )
& ! [X7,X8] :
( X0 != or(X7,X8)
| X2 != '1'
| eval_terminates(X7,X1,'1') )
& ! [X9,X10] :
( X0 != and(X9,X10)
| X2 != '0'
| eval_terminates(X10,X1,'0') )
& ! [X11,X12] :
( X0 != and(X11,X12)
| X2 != '0'
| eval_terminates(X11,X1,'0') )
& ! [X13,X14] :
( X0 != and(X13,X14)
| X2 != '1'
| ( eval_terminates(X13,X1,'1')
& ( eval_fails(X13,X1,'1')
| eval_terminates(X14,X1,'1') ) ) )
& ! [X15] :
( X0 != neg(X15)
| X2 != '0'
| eval_terminates(X15,X1,'1') )
& ! [X16] :
( X0 != neg(X16)
| X2 != '1'
| eval_terminates(X16,X1,'0') )
& ! [X17] :
( X0 != p(X17)
| X2 != '0'
| member_terminates(neg(p(X17)),X1) )
& ! [X18] :
( X0 != p(X18)
| X2 != '1'
| member_terminates(p(X18),X1) ) ) ),
inference(true_and_false_elimination,[],[f76]) ).
fof(f144,plain,
! [X0,X1,X2] :
( eval_terminates(X0,X1,X2)
<=> ( ! [X3,X4] :
( X0 != or(X3,X4)
| X2 != '0'
| ( eval_terminates(X3,X1,'0')
& ( eval_fails(X3,X1,'0')
| eval_terminates(X4,X1,'0') ) ) )
& ! [X5,X6] :
( X0 != or(X5,X6)
| X2 != '1'
| eval_terminates(X6,X1,'1') )
& ! [X7,X8] :
( X0 != or(X7,X8)
| X2 != '1'
| eval_terminates(X7,X1,'1') )
& ! [X9,X10] :
( X0 != and(X9,X10)
| X2 != '0'
| eval_terminates(X10,X1,'0') )
& ! [X11,X12] :
( X0 != and(X11,X12)
| X2 != '0'
| eval_terminates(X11,X1,'0') )
& ! [X13,X14] :
( X0 != and(X13,X14)
| X2 != '1'
| ( eval_terminates(X13,X1,'1')
& ( eval_fails(X13,X1,'1')
| eval_terminates(X14,X1,'1') ) ) )
& ! [X15] :
( X0 != neg(X15)
| X2 != '0'
| eval_terminates(X15,X1,'1') )
& ! [X16] :
( X0 != neg(X16)
| X2 != '1'
| eval_terminates(X16,X1,'0') )
& ! [X17] :
( X0 != p(X17)
| X2 != '0'
| member_terminates(neg(p(X17)),X1) )
& ! [X18] :
( X0 != p(X18)
| X2 != '1'
| member_terminates(p(X18),X1) ) ) ),
inference(flattening,[],[f143]) ).
fof(f159,plain,
( ! [X0] :
( ( ? [X1,X2] :
( X0 = or(X1,X2)
& formula_succeeds(X1)
& ! [X3,X4] :
( list_succeeds(X3)
=> eval_terminates(X1,X3,X4) )
& formula_succeeds(X2)
& ! [X5,X6] :
( list_succeeds(X5)
=> eval_terminates(X2,X5,X6) ) )
| ? [X7,X8] :
( and(X7,X8) = X0
& formula_succeeds(X7)
& ! [X9,X10] :
( list_succeeds(X9)
=> eval_terminates(X7,X9,X10) )
& formula_succeeds(X8)
& ! [X11,X12] :
( list_succeeds(X11)
=> eval_terminates(X8,X11,X12) ) )
| ? [X13] :
( neg(X13) = X0
& formula_succeeds(X13)
& ! [X14,X15] :
( list_succeeds(X14)
=> eval_terminates(X13,X14,X15) ) )
| ? [X16] : p(X16) = X0 )
=> ! [X17,X18] :
( list_succeeds(X17)
=> eval_terminates(X0,X17,X18) ) )
=> ! [X19] :
( formula_succeeds(X19)
=> ! [X20,X21] :
( list_succeeds(X20)
=> eval_terminates(X19,X20,X21) ) ) ),
inference(rectify,[],[f139]) ).
fof(f164,plain,
! [X0,X1] :
( X0 = X1
| neg(X0) != neg(X1) ),
inference(ennf_transformation,[],[f29]) ).
fof(f165,plain,
! [X0,X1,X2,X3] :
( X1 = X3
| and(X0,X1) != and(X2,X3) ),
inference(ennf_transformation,[],[f32]) ).
fof(f166,plain,
! [X0,X1,X2,X3] :
( X0 = X2
| and(X0,X1) != and(X2,X3) ),
inference(ennf_transformation,[],[f33]) ).
fof(f167,plain,
! [X0,X1,X2,X3] :
( X1 = X3
| or(X0,X1) != or(X2,X3) ),
inference(ennf_transformation,[],[f35]) ).
fof(f168,plain,
! [X0,X1,X2,X3] :
( X0 = X2
| or(X0,X1) != or(X2,X3) ),
inference(ennf_transformation,[],[f36]) ).
fof(f211,plain,
! [X0,X1] :
( member_terminates(X0,X1)
| ~ list_succeeds(X1) ),
inference(ennf_transformation,[],[f111]) ).
fof(f254,plain,
( ! [X19] :
( ! [X20,X21] :
( eval_terminates(X19,X20,X21)
| ~ list_succeeds(X20) )
| ~ formula_succeeds(X19) )
| ? [X0] :
( ? [X17,X18] :
( ~ eval_terminates(X0,X17,X18)
& list_succeeds(X17) )
& ( ? [X1,X2] :
( X0 = or(X1,X2)
& formula_succeeds(X1)
& ! [X3,X4] :
( eval_terminates(X1,X3,X4)
| ~ list_succeeds(X3) )
& formula_succeeds(X2)
& ! [X5,X6] :
( eval_terminates(X2,X5,X6)
| ~ list_succeeds(X5) ) )
| ? [X7,X8] :
( and(X7,X8) = X0
& formula_succeeds(X7)
& ! [X9,X10] :
( eval_terminates(X7,X9,X10)
| ~ list_succeeds(X9) )
& formula_succeeds(X8)
& ! [X11,X12] :
( eval_terminates(X8,X11,X12)
| ~ list_succeeds(X11) ) )
| ? [X13] :
( neg(X13) = X0
& formula_succeeds(X13)
& ! [X14,X15] :
( eval_terminates(X13,X14,X15)
| ~ list_succeeds(X14) ) )
| ? [X16] : p(X16) = X0 ) ) ),
inference(ennf_transformation,[],[f159]) ).
fof(f255,plain,
? [X0] :
( ? [X1,X2] :
( ~ eval_terminates(X0,X1,X2)
& list_succeeds(X1) )
& formula_succeeds(X0) ),
inference(ennf_transformation,[],[f141]) ).
fof(f270,definition,
! [X0,X2,X1] :
( sP11(X0,X2,X1)
<=> ? [X18] :
( X0 = p(X18)
& X2 = '1'
& member_succeeds(p(X18),X1) ) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f290,definition,
! [X0,X2,X1] :
( sP29(X0,X2,X1)
<=> ! [X13,X14] :
( X0 != and(X13,X14)
| X2 != '1'
| ( eval_terminates(X13,X1,'1')
& ( eval_fails(X13,X1,'1')
| eval_terminates(X14,X1,'1') ) ) ) ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f291,definition,
! [X0,X2,X1] :
( sP30(X0,X2,X1)
<=> ! [X3,X4] :
( X0 != or(X3,X4)
| X2 != '0'
| ( eval_terminates(X3,X1,'0')
& ( eval_fails(X3,X1,'0')
| eval_terminates(X4,X1,'0') ) ) ) ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f292,definition,
! [X0,X2,X1] :
( sP31(X0,X2,X1)
<=> ! [X18] :
( X0 != p(X18)
| X2 != '1'
| member_terminates(p(X18),X1) ) ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f293,definition,
! [X0,X2,X1] :
( sP32(X0,X2,X1)
<=> ! [X17] :
( X0 != p(X17)
| X2 != '0'
| member_terminates(neg(p(X17)),X1) ) ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f294,definition,
! [X0,X2,X1] :
( sP33(X0,X2,X1)
<=> ! [X16] :
( X0 != neg(X16)
| X2 != '1'
| eval_terminates(X16,X1,'0') ) ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f295,definition,
! [X0,X2,X1] :
( sP34(X0,X2,X1)
<=> ! [X15] :
( X0 != neg(X15)
| X2 != '0'
| eval_terminates(X15,X1,'1') ) ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f296,definition,
! [X0,X2,X1] :
( sP35(X0,X2,X1)
<=> ! [X11,X12] :
( X0 != and(X11,X12)
| X2 != '0'
| eval_terminates(X11,X1,'0') ) ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f297,definition,
! [X0,X2,X1] :
( sP36(X0,X2,X1)
<=> ! [X9,X10] :
( X0 != and(X9,X10)
| X2 != '0'
| eval_terminates(X10,X1,'0') ) ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f298,definition,
! [X0,X2,X1] :
( sP37(X0,X2,X1)
<=> ! [X7,X8] :
( X0 != or(X7,X8)
| X2 != '1'
| eval_terminates(X7,X1,'1') ) ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f299,definition,
! [X1,X2,X0] :
( sP38(X1,X2,X0)
<=> ( sP30(X0,X2,X1)
& ! [X5,X6] :
( X0 != or(X5,X6)
| X2 != '1'
| eval_terminates(X6,X1,'1') )
& sP37(X0,X2,X1)
& sP36(X0,X2,X1)
& sP35(X0,X2,X1)
& sP29(X0,X2,X1)
& sP34(X0,X2,X1)
& sP33(X0,X2,X1)
& sP32(X0,X2,X1)
& sP31(X0,X2,X1) ) ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f300,plain,
! [X0,X1,X2] :
( eval_terminates(X0,X1,X2)
<=> sP38(X1,X2,X0) ),
inference(definition_folding,[],[f144,f299,f298,f297,f296,f295,f294,f293,f292,f291,f290]) ).
fof(f334,definition,
! [X0] :
( ? [X7,X8] :
( and(X7,X8) = X0
& formula_succeeds(X7)
& ! [X9,X10] :
( eval_terminates(X7,X9,X10)
| ~ list_succeeds(X9) )
& formula_succeeds(X8)
& ! [X11,X12] :
( eval_terminates(X8,X11,X12)
| ~ list_succeeds(X11) ) )
| ~ sP63(X0) ),
introduced(definition,[new_symbols(definition,[sP63])],[predicate_definition_introduction]) ).
fof(f335,definition,
! [X0] :
( ? [X1,X2] :
( X0 = or(X1,X2)
& formula_succeeds(X1)
& ! [X3,X4] :
( eval_terminates(X1,X3,X4)
| ~ list_succeeds(X3) )
& formula_succeeds(X2)
& ! [X5,X6] :
( eval_terminates(X2,X5,X6)
| ~ list_succeeds(X5) ) )
| ~ sP64(X0) ),
introduced(definition,[new_symbols(definition,[sP64])],[predicate_definition_introduction]) ).
fof(f336,plain,
( ! [X19] :
( ! [X20,X21] :
( eval_terminates(X19,X20,X21)
| ~ list_succeeds(X20) )
| ~ formula_succeeds(X19) )
| ? [X0] :
( ? [X17,X18] :
( ~ eval_terminates(X0,X17,X18)
& list_succeeds(X17) )
& ( sP64(X0)
| sP63(X0)
| ? [X13] :
( neg(X13) = X0
& formula_succeeds(X13)
& ! [X14,X15] :
( eval_terminates(X13,X14,X15)
| ~ list_succeeds(X14) ) )
| ? [X16] : p(X16) = X0 ) ) ),
inference(definition_folding,[],[f254,f335,f334]) ).
fof(f400,plain,
! [X0,X2,X1] :
( ( sP11(X0,X2,X1)
| ! [X18] :
( p(X18) != X0
| '1' != X2
| ~ member_succeeds(p(X18),X1) ) )
& ( ? [X18] :
( X0 = p(X18)
& X2 = '1'
& member_succeeds(p(X18),X1) )
| ~ sP11(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f270]) ).
fof(f401,plain,
! [X0,X1,X2] :
( ( sP11(X0,X1,X2)
| ! [X3] :
( p(X3) != X0
| '1' != X1
| ~ member_succeeds(p(X3),X2) ) )
& ( ? [X4] :
( p(X4) = X0
& '1' = X1
& member_succeeds(p(X4),X2) )
| ~ sP11(X0,X1,X2) ) ),
inference(rectify,[],[f400]) ).
fof(f402,plain,
! [X0,X1,X2] :
( ( sP11(X0,X1,X2)
| ! [X3] :
( p(X3) != X0
| '1' != X1
| ~ member_succeeds(p(X3),X2) ) )
& ( ( p(sK97(X0,X1,X2)) = X0
& '1' = X1
& member_succeeds(p(sK97(X0,X1,X2)),X2) )
| ~ sP11(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK97]),skolemize(X4,sK97(X0,X1,X2))],[f401]) ).
fof(f442,plain,
! [X1,X2,X0] :
( ( sP38(X1,X2,X0)
| ~ sP30(X0,X2,X1)
| ? [X5,X6] :
( or(X5,X6) = X0
& '1' = X2
& ~ eval_terminates(X6,X1,'1') )
| ~ sP37(X0,X2,X1)
| ~ sP36(X0,X2,X1)
| ~ sP35(X0,X2,X1)
| ~ sP29(X0,X2,X1)
| ~ sP34(X0,X2,X1)
| ~ sP33(X0,X2,X1)
| ~ sP32(X0,X2,X1)
| ~ sP31(X0,X2,X1) )
& ( ( sP30(X0,X2,X1)
& ! [X5,X6] :
( X0 != or(X5,X6)
| X2 != '1'
| eval_terminates(X6,X1,'1') )
& sP37(X0,X2,X1)
& sP36(X0,X2,X1)
& sP35(X0,X2,X1)
& sP29(X0,X2,X1)
& sP34(X0,X2,X1)
& sP33(X0,X2,X1)
& sP32(X0,X2,X1)
& sP31(X0,X2,X1) )
| ~ sP38(X1,X2,X0) ) ),
inference(nnf_transformation,[],[f299]) ).
fof(f443,plain,
! [X1,X2,X0] :
( ( sP38(X1,X2,X0)
| ~ sP30(X0,X2,X1)
| ? [X5,X6] :
( or(X5,X6) = X0
& '1' = X2
& ~ eval_terminates(X6,X1,'1') )
| ~ sP37(X0,X2,X1)
| ~ sP36(X0,X2,X1)
| ~ sP35(X0,X2,X1)
| ~ sP29(X0,X2,X1)
| ~ sP34(X0,X2,X1)
| ~ sP33(X0,X2,X1)
| ~ sP32(X0,X2,X1)
| ~ sP31(X0,X2,X1) )
& ( ( sP30(X0,X2,X1)
& ! [X5,X6] :
( X0 != or(X5,X6)
| X2 != '1'
| eval_terminates(X6,X1,'1') )
& sP37(X0,X2,X1)
& sP36(X0,X2,X1)
& sP35(X0,X2,X1)
& sP29(X0,X2,X1)
& sP34(X0,X2,X1)
& sP33(X0,X2,X1)
& sP32(X0,X2,X1)
& sP31(X0,X2,X1) )
| ~ sP38(X1,X2,X0) ) ),
inference(flattening,[],[f442]) ).
fof(f444,plain,
! [X0,X1,X2] :
( ( sP38(X0,X1,X2)
| ~ sP30(X2,X1,X0)
| ? [X3,X4] :
( or(X3,X4) = X2
& '1' = X1
& ~ eval_terminates(X4,X0,'1') )
| ~ sP37(X2,X1,X0)
| ~ sP36(X2,X1,X0)
| ~ sP35(X2,X1,X0)
| ~ sP29(X2,X1,X0)
| ~ sP34(X2,X1,X0)
| ~ sP33(X2,X1,X0)
| ~ sP32(X2,X1,X0)
| ~ sP31(X2,X1,X0) )
& ( ( sP30(X2,X1,X0)
& ! [X5,X6] :
( or(X5,X6) != X2
| '1' != X1
| eval_terminates(X6,X0,'1') )
& sP37(X2,X1,X0)
& sP36(X2,X1,X0)
& sP35(X2,X1,X0)
& sP29(X2,X1,X0)
& sP34(X2,X1,X0)
& sP33(X2,X1,X0)
& sP32(X2,X1,X0)
& sP31(X2,X1,X0) )
| ~ sP38(X0,X1,X2) ) ),
inference(rectify,[],[f443]) ).
fof(f445,plain,
! [X0,X1,X2] :
( ( sP38(X0,X1,X2)
| ~ sP30(X2,X1,X0)
| ( or(sK118(X0,X1,X2),sK119(X0,X1,X2)) = X2
& '1' = X1
& ~ eval_terminates(sK119(X0,X1,X2),X0,'1') )
| ~ sP37(X2,X1,X0)
| ~ sP36(X2,X1,X0)
| ~ sP35(X2,X1,X0)
| ~ sP29(X2,X1,X0)
| ~ sP34(X2,X1,X0)
| ~ sP33(X2,X1,X0)
| ~ sP32(X2,X1,X0)
| ~ sP31(X2,X1,X0) )
& ( ( sP30(X2,X1,X0)
& ! [X5,X6] :
( or(X5,X6) != X2
| '1' != X1
| eval_terminates(X6,X0,'1') )
& sP37(X2,X1,X0)
& sP36(X2,X1,X0)
& sP35(X2,X1,X0)
& sP29(X2,X1,X0)
& sP34(X2,X1,X0)
& sP33(X2,X1,X0)
& sP32(X2,X1,X0)
& sP31(X2,X1,X0) )
| ~ sP38(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK118,sK119]),skolemize(X3,sK118(X0,X1,X2)),skolemize(X4,sK119(X0,X1,X2))],[f444]) ).
fof(f446,plain,
! [X0,X2,X1] :
( ( sP37(X0,X2,X1)
| ? [X7,X8] :
( or(X7,X8) = X0
& '1' = X2
& ~ eval_terminates(X7,X1,'1') ) )
& ( ! [X7,X8] :
( X0 != or(X7,X8)
| X2 != '1'
| eval_terminates(X7,X1,'1') )
| ~ sP37(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f298]) ).
fof(f447,plain,
! [X0,X1,X2] :
( ( sP37(X0,X1,X2)
| ? [X3,X4] :
( or(X3,X4) = X0
& '1' = X1
& ~ eval_terminates(X3,X2,'1') ) )
& ( ! [X5,X6] :
( or(X5,X6) != X0
| '1' != X1
| eval_terminates(X5,X2,'1') )
| ~ sP37(X0,X1,X2) ) ),
inference(rectify,[],[f446]) ).
fof(f448,plain,
! [X0,X1,X2] :
( ( sP37(X0,X1,X2)
| ( or(sK120(X0,X1,X2),sK121(X0,X1,X2)) = X0
& '1' = X1
& ~ eval_terminates(sK120(X0,X1,X2),X2,'1') ) )
& ( ! [X5,X6] :
( or(X5,X6) != X0
| '1' != X1
| eval_terminates(X5,X2,'1') )
| ~ sP37(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK120,sK121]),skolemize(X3,sK120(X0,X1,X2)),skolemize(X4,sK121(X0,X1,X2))],[f447]) ).
fof(f449,plain,
! [X0,X2,X1] :
( ( sP36(X0,X2,X1)
| ? [X9,X10] :
( and(X9,X10) = X0
& '0' = X2
& ~ eval_terminates(X10,X1,'0') ) )
& ( ! [X9,X10] :
( X0 != and(X9,X10)
| X2 != '0'
| eval_terminates(X10,X1,'0') )
| ~ sP36(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f297]) ).
fof(f450,plain,
! [X0,X1,X2] :
( ( sP36(X0,X1,X2)
| ? [X3,X4] :
( and(X3,X4) = X0
& '0' = X1
& ~ eval_terminates(X4,X2,'0') ) )
& ( ! [X5,X6] :
( and(X5,X6) != X0
| '0' != X1
| eval_terminates(X6,X2,'0') )
| ~ sP36(X0,X1,X2) ) ),
inference(rectify,[],[f449]) ).
fof(f451,plain,
! [X0,X1,X2] :
( ( sP36(X0,X1,X2)
| ( and(sK122(X0,X1,X2),sK123(X0,X1,X2)) = X0
& '0' = X1
& ~ eval_terminates(sK123(X0,X1,X2),X2,'0') ) )
& ( ! [X5,X6] :
( and(X5,X6) != X0
| '0' != X1
| eval_terminates(X6,X2,'0') )
| ~ sP36(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK122,sK123]),skolemize(X3,sK122(X0,X1,X2)),skolemize(X4,sK123(X0,X1,X2))],[f450]) ).
fof(f452,plain,
! [X0,X2,X1] :
( ( sP35(X0,X2,X1)
| ? [X11,X12] :
( and(X11,X12) = X0
& '0' = X2
& ~ eval_terminates(X11,X1,'0') ) )
& ( ! [X11,X12] :
( X0 != and(X11,X12)
| X2 != '0'
| eval_terminates(X11,X1,'0') )
| ~ sP35(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f296]) ).
fof(f453,plain,
! [X0,X1,X2] :
( ( sP35(X0,X1,X2)
| ? [X3,X4] :
( and(X3,X4) = X0
& '0' = X1
& ~ eval_terminates(X3,X2,'0') ) )
& ( ! [X5,X6] :
( and(X5,X6) != X0
| '0' != X1
| eval_terminates(X5,X2,'0') )
| ~ sP35(X0,X1,X2) ) ),
inference(rectify,[],[f452]) ).
fof(f454,plain,
! [X0,X1,X2] :
( ( sP35(X0,X1,X2)
| ( and(sK124(X0,X1,X2),sK125(X0,X1,X2)) = X0
& '0' = X1
& ~ eval_terminates(sK124(X0,X1,X2),X2,'0') ) )
& ( ! [X5,X6] :
( and(X5,X6) != X0
| '0' != X1
| eval_terminates(X5,X2,'0') )
| ~ sP35(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK124,sK125]),skolemize(X3,sK124(X0,X1,X2)),skolemize(X4,sK125(X0,X1,X2))],[f453]) ).
fof(f455,plain,
! [X0,X2,X1] :
( ( sP34(X0,X2,X1)
| ? [X15] :
( neg(X15) = X0
& '0' = X2
& ~ eval_terminates(X15,X1,'1') ) )
& ( ! [X15] :
( X0 != neg(X15)
| X2 != '0'
| eval_terminates(X15,X1,'1') )
| ~ sP34(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f295]) ).
fof(f456,plain,
! [X0,X1,X2] :
( ( sP34(X0,X1,X2)
| ? [X3] :
( neg(X3) = X0
& '0' = X1
& ~ eval_terminates(X3,X2,'1') ) )
& ( ! [X4] :
( neg(X4) != X0
| '0' != X1
| eval_terminates(X4,X2,'1') )
| ~ sP34(X0,X1,X2) ) ),
inference(rectify,[],[f455]) ).
fof(f457,plain,
! [X0,X1,X2] :
( ( sP34(X0,X1,X2)
| ( neg(sK126(X0,X1,X2)) = X0
& '0' = X1
& ~ eval_terminates(sK126(X0,X1,X2),X2,'1') ) )
& ( ! [X4] :
( neg(X4) != X0
| '0' != X1
| eval_terminates(X4,X2,'1') )
| ~ sP34(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK126]),skolemize(X3,sK126(X0,X1,X2))],[f456]) ).
fof(f458,plain,
! [X0,X2,X1] :
( ( sP33(X0,X2,X1)
| ? [X16] :
( neg(X16) = X0
& '1' = X2
& ~ eval_terminates(X16,X1,'0') ) )
& ( ! [X16] :
( X0 != neg(X16)
| X2 != '1'
| eval_terminates(X16,X1,'0') )
| ~ sP33(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f294]) ).
fof(f459,plain,
! [X0,X1,X2] :
( ( sP33(X0,X1,X2)
| ? [X3] :
( neg(X3) = X0
& '1' = X1
& ~ eval_terminates(X3,X2,'0') ) )
& ( ! [X4] :
( neg(X4) != X0
| '1' != X1
| eval_terminates(X4,X2,'0') )
| ~ sP33(X0,X1,X2) ) ),
inference(rectify,[],[f458]) ).
fof(f460,plain,
! [X0,X1,X2] :
( ( sP33(X0,X1,X2)
| ( neg(sK127(X0,X1,X2)) = X0
& '1' = X1
& ~ eval_terminates(sK127(X0,X1,X2),X2,'0') ) )
& ( ! [X4] :
( neg(X4) != X0
| '1' != X1
| eval_terminates(X4,X2,'0') )
| ~ sP33(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK127]),skolemize(X3,sK127(X0,X1,X2))],[f459]) ).
fof(f461,plain,
! [X0,X2,X1] :
( ( sP32(X0,X2,X1)
| ? [X17] :
( p(X17) = X0
& '0' = X2
& ~ member_terminates(neg(p(X17)),X1) ) )
& ( ! [X17] :
( X0 != p(X17)
| X2 != '0'
| member_terminates(neg(p(X17)),X1) )
| ~ sP32(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f293]) ).
fof(f462,plain,
! [X0,X1,X2] :
( ( sP32(X0,X1,X2)
| ? [X3] :
( p(X3) = X0
& '0' = X1
& ~ member_terminates(neg(p(X3)),X2) ) )
& ( ! [X4] :
( p(X4) != X0
| '0' != X1
| member_terminates(neg(p(X4)),X2) )
| ~ sP32(X0,X1,X2) ) ),
inference(rectify,[],[f461]) ).
fof(f463,plain,
! [X0,X1,X2] :
( ( sP32(X0,X1,X2)
| ( p(sK128(X0,X1,X2)) = X0
& '0' = X1
& ~ member_terminates(neg(p(sK128(X0,X1,X2))),X2) ) )
& ( ! [X4] :
( p(X4) != X0
| '0' != X1
| member_terminates(neg(p(X4)),X2) )
| ~ sP32(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK128]),skolemize(X3,sK128(X0,X1,X2))],[f462]) ).
fof(f464,plain,
! [X0,X2,X1] :
( ( sP31(X0,X2,X1)
| ? [X18] :
( p(X18) = X0
& '1' = X2
& ~ member_terminates(p(X18),X1) ) )
& ( ! [X18] :
( X0 != p(X18)
| X2 != '1'
| member_terminates(p(X18),X1) )
| ~ sP31(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f292]) ).
fof(f465,plain,
! [X0,X1,X2] :
( ( sP31(X0,X1,X2)
| ? [X3] :
( p(X3) = X0
& '1' = X1
& ~ member_terminates(p(X3),X2) ) )
& ( ! [X4] :
( p(X4) != X0
| '1' != X1
| member_terminates(p(X4),X2) )
| ~ sP31(X0,X1,X2) ) ),
inference(rectify,[],[f464]) ).
fof(f466,plain,
! [X0,X1,X2] :
( ( sP31(X0,X1,X2)
| ( p(sK129(X0,X1,X2)) = X0
& '1' = X1
& ~ member_terminates(p(sK129(X0,X1,X2)),X2) ) )
& ( ! [X4] :
( p(X4) != X0
| '1' != X1
| member_terminates(p(X4),X2) )
| ~ sP31(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK129]),skolemize(X3,sK129(X0,X1,X2))],[f465]) ).
fof(f467,plain,
! [X0,X2,X1] :
( ( sP30(X0,X2,X1)
| ? [X3,X4] :
( or(X3,X4) = X0
& '0' = X2
& ( ~ eval_terminates(X3,X1,'0')
| ( ~ eval_fails(X3,X1,'0')
& ~ eval_terminates(X4,X1,'0') ) ) ) )
& ( ! [X3,X4] :
( X0 != or(X3,X4)
| X2 != '0'
| ( eval_terminates(X3,X1,'0')
& ( eval_fails(X3,X1,'0')
| eval_terminates(X4,X1,'0') ) ) )
| ~ sP30(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f291]) ).
fof(f468,plain,
! [X0,X1,X2] :
( ( sP30(X0,X1,X2)
| ? [X3,X4] :
( or(X3,X4) = X0
& '0' = X1
& ( ~ eval_terminates(X3,X2,'0')
| ( ~ eval_fails(X3,X2,'0')
& ~ eval_terminates(X4,X2,'0') ) ) ) )
& ( ! [X5,X6] :
( or(X5,X6) != X0
| '0' != X1
| ( eval_terminates(X5,X2,'0')
& ( eval_fails(X5,X2,'0')
| eval_terminates(X6,X2,'0') ) ) )
| ~ sP30(X0,X1,X2) ) ),
inference(rectify,[],[f467]) ).
fof(f469,plain,
! [X0,X1,X2] :
( ( sP30(X0,X1,X2)
| ( or(sK130(X0,X1,X2),sK131(X0,X1,X2)) = X0
& '0' = X1
& ( ~ eval_terminates(sK130(X0,X1,X2),X2,'0')
| ( ~ eval_fails(sK130(X0,X1,X2),X2,'0')
& ~ eval_terminates(sK131(X0,X1,X2),X2,'0') ) ) ) )
& ( ! [X5,X6] :
( or(X5,X6) != X0
| '0' != X1
| ( eval_terminates(X5,X2,'0')
& ( eval_fails(X5,X2,'0')
| eval_terminates(X6,X2,'0') ) ) )
| ~ sP30(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK130,sK131]),skolemize(X3,sK130(X0,X1,X2)),skolemize(X4,sK131(X0,X1,X2))],[f468]) ).
fof(f470,plain,
! [X0,X2,X1] :
( ( sP29(X0,X2,X1)
| ? [X13,X14] :
( and(X13,X14) = X0
& '1' = X2
& ( ~ eval_terminates(X13,X1,'1')
| ( ~ eval_fails(X13,X1,'1')
& ~ eval_terminates(X14,X1,'1') ) ) ) )
& ( ! [X13,X14] :
( X0 != and(X13,X14)
| X2 != '1'
| ( eval_terminates(X13,X1,'1')
& ( eval_fails(X13,X1,'1')
| eval_terminates(X14,X1,'1') ) ) )
| ~ sP29(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f290]) ).
fof(f471,plain,
! [X0,X1,X2] :
( ( sP29(X0,X1,X2)
| ? [X3,X4] :
( and(X3,X4) = X0
& '1' = X1
& ( ~ eval_terminates(X3,X2,'1')
| ( ~ eval_fails(X3,X2,'1')
& ~ eval_terminates(X4,X2,'1') ) ) ) )
& ( ! [X5,X6] :
( and(X5,X6) != X0
| '1' != X1
| ( eval_terminates(X5,X2,'1')
& ( eval_fails(X5,X2,'1')
| eval_terminates(X6,X2,'1') ) ) )
| ~ sP29(X0,X1,X2) ) ),
inference(rectify,[],[f470]) ).
fof(f472,plain,
! [X0,X1,X2] :
( ( sP29(X0,X1,X2)
| ( and(sK132(X0,X1,X2),sK133(X0,X1,X2)) = X0
& '1' = X1
& ( ~ eval_terminates(sK132(X0,X1,X2),X2,'1')
| ( ~ eval_fails(sK132(X0,X1,X2),X2,'1')
& ~ eval_terminates(sK133(X0,X1,X2),X2,'1') ) ) ) )
& ( ! [X5,X6] :
( and(X5,X6) != X0
| '1' != X1
| ( eval_terminates(X5,X2,'1')
& ( eval_fails(X5,X2,'1')
| eval_terminates(X6,X2,'1') ) ) )
| ~ sP29(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK132,sK133]),skolemize(X3,sK132(X0,X1,X2)),skolemize(X4,sK133(X0,X1,X2))],[f471]) ).
fof(f473,plain,
! [X0,X1,X2] :
( ( eval_terminates(X0,X1,X2)
| ~ sP38(X1,X2,X0) )
& ( sP38(X1,X2,X0)
| ~ eval_terminates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f300]) ).
fof(f609,plain,
! [X0,X1] :
( ( member_succeeds(X0,X1)
| ( ! [X2,X3] :
( cons(X2,X3) != X1
| ~ member_succeeds(X0,X3) )
& ! [X4] : cons(X0,X4) != X1 ) )
& ( ? [X2,X3] :
( X1 = cons(X2,X3)
& member_succeeds(X0,X3) )
| ? [X4] : X1 = cons(X0,X4)
| ~ member_succeeds(X0,X1) ) ),
inference(nnf_transformation,[],[f104]) ).
fof(f610,plain,
! [X0,X1] :
( ( member_succeeds(X0,X1)
| ( ! [X2,X3] :
( cons(X2,X3) != X1
| ~ member_succeeds(X0,X3) )
& ! [X4] : cons(X0,X4) != X1 ) )
& ( ? [X2,X3] :
( X1 = cons(X2,X3)
& member_succeeds(X0,X3) )
| ? [X4] : X1 = cons(X0,X4)
| ~ member_succeeds(X0,X1) ) ),
inference(flattening,[],[f609]) ).
fof(f611,plain,
! [X0,X1] :
( ( member_succeeds(X0,X1)
| ( ! [X2,X3] :
( cons(X2,X3) != X1
| ~ member_succeeds(X0,X3) )
& ! [X4] : cons(X0,X4) != X1 ) )
& ( ? [X5,X6] :
( cons(X5,X6) = X1
& member_succeeds(X0,X6) )
| ? [X7] : cons(X0,X7) = X1
| ~ member_succeeds(X0,X1) ) ),
inference(rectify,[],[f610]) ).
fof(f612,plain,
! [X0,X1] :
( ( member_succeeds(X0,X1)
| ( ! [X2,X3] :
( cons(X2,X3) != X1
| ~ member_succeeds(X0,X3) )
& ! [X4] : cons(X0,X4) != X1 ) )
& ( ( cons(sK221(X0,X1),sK222(X0,X1)) = X1
& member_succeeds(X0,sK222(X0,X1)) )
| cons(X0,sK223(X0,X1)) = X1
| ~ member_succeeds(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK221,sK222,sK223]),skolemize(X5,sK221(X0,X1)),skolemize(X6,sK222(X0,X1)),skolemize(X7,sK223(X0,X1))],[f611]) ).
fof(f635,plain,
! [X0] :
( ? [X1,X2] :
( X0 = or(X1,X2)
& formula_succeeds(X1)
& ! [X3,X4] :
( eval_terminates(X1,X3,X4)
| ~ list_succeeds(X3) )
& formula_succeeds(X2)
& ! [X5,X6] :
( eval_terminates(X2,X5,X6)
| ~ list_succeeds(X5) ) )
| ~ sP64(X0) ),
inference(nnf_transformation,[],[f335]) ).
fof(f636,plain,
! [X0] :
( ( or(sK237(X0),sK238(X0)) = X0
& formula_succeeds(sK237(X0))
& ! [X3,X4] :
( eval_terminates(sK237(X0),X3,X4)
| ~ list_succeeds(X3) )
& formula_succeeds(sK238(X0))
& ! [X5,X6] :
( eval_terminates(sK238(X0),X5,X6)
| ~ list_succeeds(X5) ) )
| ~ sP64(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK237,sK238]),skolemize(X1,sK237(X0)),skolemize(X2,sK238(X0))],[f635]) ).
fof(f637,plain,
! [X0] :
( ? [X7,X8] :
( and(X7,X8) = X0
& formula_succeeds(X7)
& ! [X9,X10] :
( eval_terminates(X7,X9,X10)
| ~ list_succeeds(X9) )
& formula_succeeds(X8)
& ! [X11,X12] :
( eval_terminates(X8,X11,X12)
| ~ list_succeeds(X11) ) )
| ~ sP63(X0) ),
inference(nnf_transformation,[],[f334]) ).
fof(f638,plain,
! [X0] :
( ? [X1,X2] :
( and(X1,X2) = X0
& formula_succeeds(X1)
& ! [X3,X4] :
( eval_terminates(X1,X3,X4)
| ~ list_succeeds(X3) )
& formula_succeeds(X2)
& ! [X5,X6] :
( eval_terminates(X2,X5,X6)
| ~ list_succeeds(X5) ) )
| ~ sP63(X0) ),
inference(rectify,[],[f637]) ).
fof(f639,plain,
! [X0] :
( ( and(sK239(X0),sK240(X0)) = X0
& formula_succeeds(sK239(X0))
& ! [X3,X4] :
( eval_terminates(sK239(X0),X3,X4)
| ~ list_succeeds(X3) )
& formula_succeeds(sK240(X0))
& ! [X5,X6] :
( eval_terminates(sK240(X0),X5,X6)
| ~ list_succeeds(X5) ) )
| ~ sP63(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK239,sK240]),skolemize(X1,sK239(X0)),skolemize(X2,sK240(X0))],[f638]) ).
fof(f640,plain,
( ! [X0] :
( ! [X1,X2] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1) )
| ~ formula_succeeds(X0) )
| ? [X3] :
( ? [X4,X5] :
( ~ eval_terminates(X3,X4,X5)
& list_succeeds(X4) )
& ( sP64(X3)
| sP63(X3)
| ? [X6] :
( neg(X6) = X3
& formula_succeeds(X6)
& ! [X7,X8] :
( eval_terminates(X6,X7,X8)
| ~ list_succeeds(X7) ) )
| ? [X9] : p(X9) = X3 ) ) ),
inference(rectify,[],[f336]) ).
fof(f641,plain,
( ! [X0] :
( ! [X1,X2] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1) )
| ~ formula_succeeds(X0) )
| ( ~ eval_terminates(sK241,sK242,sK243)
& list_succeeds(sK242)
& ( sP64(sK241)
| sP63(sK241)
| ( sK241 = neg(sK244)
& formula_succeeds(sK244)
& ! [X7,X8] :
( eval_terminates(sK244,X7,X8)
| ~ list_succeeds(X7) ) )
| sK241 = p(sK245) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK241,sK242,sK243,sK244,sK245]),skolemize(X3,sK241),skolemize(X4,sK242),skolemize(X5,sK243),skolemize(X6,sK244),skolemize(X9,sK245)],[f640]) ).
fof(f642,plain,
( ~ eval_terminates(sK246,sK247,sK248)
& list_succeeds(sK247)
& formula_succeeds(sK246) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK246,sK247,sK248]),skolemize(X0,sK246),skolemize(X1,sK247),skolemize(X2,sK248)],[f255]) ).
fof(f658,plain,
'1' != '0',
inference(cnf_transformation,[],[f16]) ).
fof(f668,plain,
! [X0,X1] : p(X0) != neg(X1),
inference(cnf_transformation,[],[f26]) ).
fof(f669,plain,
! [X2,X0,X1] : p(X0) != and(X1,X2),
inference(cnf_transformation,[],[f27]) ).
fof(f670,plain,
! [X2,X0,X1] : p(X0) != or(X1,X2),
inference(cnf_transformation,[],[f28]) ).
fof(f671,plain,
! [X0,X1] :
( X0 = X1
| neg(X0) != neg(X1) ),
inference(cnf_transformation,[],[f164]) ).
fof(f672,plain,
! [X2,X0,X1] : neg(X0) != and(X1,X2),
inference(cnf_transformation,[],[f30]) ).
fof(f673,plain,
! [X2,X0,X1] : neg(X0) != or(X1,X2),
inference(cnf_transformation,[],[f31]) ).
fof(f674,plain,
! [X2,X3,X0,X1] :
( X1 = X3
| and(X0,X1) != and(X2,X3) ),
inference(cnf_transformation,[],[f165]) ).
fof(f675,plain,
! [X2,X3,X0,X1] :
( X0 = X2
| and(X0,X1) != and(X2,X3) ),
inference(cnf_transformation,[],[f166]) ).
fof(f676,plain,
! [X2,X3,X0,X1] : and(X0,X1) != or(X2,X3),
inference(cnf_transformation,[],[f34]) ).
fof(f677,plain,
! [X2,X3,X0,X1] :
( X1 = X3
| or(X0,X1) != or(X2,X3) ),
inference(cnf_transformation,[],[f167]) ).
fof(f678,plain,
! [X2,X3,X0,X1] :
( X0 = X2
| or(X0,X1) != or(X2,X3) ),
inference(cnf_transformation,[],[f168]) ).
fof(f831,plain,
! [X2,X0,X1] :
( p(sK97(X0,X1,X2)) = X0
| ~ sP11(X0,X1,X2) ),
inference(cnf_transformation,[],[f402]) ).
fof(f832,plain,
! [X2,X3,X0,X1] :
( sP11(X0,X1,X2)
| p(X3) != X0
| '1' != X1
| ~ member_succeeds(p(X3),X2) ),
inference(cnf_transformation,[],[f402]) ).
fof(f908,plain,
! [X2,X0,X1] :
( sP38(X0,X1,X2)
| ~ sP30(X2,X1,X0)
| ~ eval_terminates(sK119(X0,X1,X2),X0,'1')
| ~ sP37(X2,X1,X0)
| ~ sP36(X2,X1,X0)
| ~ sP35(X2,X1,X0)
| ~ sP29(X2,X1,X0)
| ~ sP34(X2,X1,X0)
| ~ sP33(X2,X1,X0)
| ~ sP32(X2,X1,X0)
| ~ sP31(X2,X1,X0) ),
inference(cnf_transformation,[],[f445]) ).
fof(f909,plain,
! [X2,X0,X1] :
( sP38(X0,X1,X2)
| ~ sP30(X2,X1,X0)
| '1' = X1
| ~ sP37(X2,X1,X0)
| ~ sP36(X2,X1,X0)
| ~ sP35(X2,X1,X0)
| ~ sP29(X2,X1,X0)
| ~ sP34(X2,X1,X0)
| ~ sP33(X2,X1,X0)
| ~ sP32(X2,X1,X0)
| ~ sP31(X2,X1,X0) ),
inference(cnf_transformation,[],[f445]) ).
fof(f910,plain,
! [X2,X0,X1] :
( sP38(X0,X1,X2)
| ~ sP30(X2,X1,X0)
| or(sK118(X0,X1,X2),sK119(X0,X1,X2)) = X2
| ~ sP37(X2,X1,X0)
| ~ sP36(X2,X1,X0)
| ~ sP35(X2,X1,X0)
| ~ sP29(X2,X1,X0)
| ~ sP34(X2,X1,X0)
| ~ sP33(X2,X1,X0)
| ~ sP32(X2,X1,X0)
| ~ sP31(X2,X1,X0) ),
inference(cnf_transformation,[],[f445]) ).
fof(f912,plain,
! [X2,X0,X1] :
( sP37(X0,X1,X2)
| ~ eval_terminates(sK120(X0,X1,X2),X2,'1') ),
inference(cnf_transformation,[],[f448]) ).
fof(f913,plain,
! [X2,X0,X1] :
( sP37(X0,X1,X2)
| '1' = X1 ),
inference(cnf_transformation,[],[f448]) ).
fof(f914,plain,
! [X2,X0,X1] :
( sP37(X0,X1,X2)
| or(sK120(X0,X1,X2),sK121(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f448]) ).
fof(f916,plain,
! [X2,X0,X1] :
( sP36(X0,X1,X2)
| ~ eval_terminates(sK123(X0,X1,X2),X2,'0') ),
inference(cnf_transformation,[],[f451]) ).
fof(f917,plain,
! [X2,X0,X1] :
( sP36(X0,X1,X2)
| '0' = X1 ),
inference(cnf_transformation,[],[f451]) ).
fof(f918,plain,
! [X2,X0,X1] :
( sP36(X0,X1,X2)
| and(sK122(X0,X1,X2),sK123(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f451]) ).
fof(f920,plain,
! [X2,X0,X1] :
( sP35(X0,X1,X2)
| ~ eval_terminates(sK124(X0,X1,X2),X2,'0') ),
inference(cnf_transformation,[],[f454]) ).
fof(f921,plain,
! [X2,X0,X1] :
( sP35(X0,X1,X2)
| '0' = X1 ),
inference(cnf_transformation,[],[f454]) ).
fof(f922,plain,
! [X2,X0,X1] :
( sP35(X0,X1,X2)
| and(sK124(X0,X1,X2),sK125(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f454]) ).
fof(f924,plain,
! [X2,X0,X1] :
( sP34(X0,X1,X2)
| ~ eval_terminates(sK126(X0,X1,X2),X2,'1') ),
inference(cnf_transformation,[],[f457]) ).
fof(f925,plain,
! [X2,X0,X1] :
( sP34(X0,X1,X2)
| '0' = X1 ),
inference(cnf_transformation,[],[f457]) ).
fof(f926,plain,
! [X2,X0,X1] :
( sP34(X0,X1,X2)
| neg(sK126(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f457]) ).
fof(f928,plain,
! [X2,X0,X1] :
( sP33(X0,X1,X2)
| ~ eval_terminates(sK127(X0,X1,X2),X2,'0') ),
inference(cnf_transformation,[],[f460]) ).
fof(f929,plain,
! [X2,X0,X1] :
( sP33(X0,X1,X2)
| '1' = X1 ),
inference(cnf_transformation,[],[f460]) ).
fof(f930,plain,
! [X2,X0,X1] :
( sP33(X0,X1,X2)
| neg(sK127(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f460]) ).
fof(f932,plain,
! [X2,X0,X1] :
( sP32(X0,X1,X2)
| ~ member_terminates(neg(p(sK128(X0,X1,X2))),X2) ),
inference(cnf_transformation,[],[f463]) ).
fof(f936,plain,
! [X2,X0,X1] :
( sP31(X0,X1,X2)
| ~ member_terminates(p(sK129(X0,X1,X2)),X2) ),
inference(cnf_transformation,[],[f466]) ).
fof(f937,plain,
! [X2,X0,X1] :
( sP31(X0,X1,X2)
| '1' = X1 ),
inference(cnf_transformation,[],[f466]) ).
fof(f941,plain,
! [X2,X0,X1] :
( sP30(X0,X1,X2)
| ~ eval_terminates(sK130(X0,X1,X2),X2,'0')
| ~ eval_terminates(sK131(X0,X1,X2),X2,'0') ),
inference(cnf_transformation,[],[f469]) ).
fof(f943,plain,
! [X2,X0,X1] :
( sP30(X0,X1,X2)
| '0' = X1 ),
inference(cnf_transformation,[],[f469]) ).
fof(f944,plain,
! [X2,X0,X1] :
( sP30(X0,X1,X2)
| or(sK130(X0,X1,X2),sK131(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f469]) ).
fof(f947,plain,
! [X2,X0,X1] :
( sP29(X0,X1,X2)
| ~ eval_terminates(sK132(X0,X1,X2),X2,'1')
| ~ eval_terminates(sK133(X0,X1,X2),X2,'1') ),
inference(cnf_transformation,[],[f472]) ).
fof(f949,plain,
! [X2,X0,X1] :
( sP29(X0,X1,X2)
| '1' = X1 ),
inference(cnf_transformation,[],[f472]) ).
fof(f950,plain,
! [X2,X0,X1] :
( sP29(X0,X1,X2)
| and(sK132(X0,X1,X2),sK133(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f472]) ).
fof(f952,plain,
! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ sP38(X1,X2,X0) ),
inference(cnf_transformation,[],[f473]) ).
fof(f1201,plain,
! [X0,X1,X4] :
( member_succeeds(X0,X1)
| cons(X0,X4) != X1 ),
inference(cnf_transformation,[],[f612]) ).
fof(f1224,plain,
! [X0,X1] :
( member_terminates(X0,X1)
| ~ list_succeeds(X1) ),
inference(cnf_transformation,[],[f211]) ).
fof(f1261,plain,
! [X0,X6,X5] :
( eval_terminates(sK238(X0),X5,X6)
| ~ list_succeeds(X5)
| ~ sP64(X0) ),
inference(cnf_transformation,[],[f636]) ).
fof(f1263,plain,
! [X3,X0,X4] :
( eval_terminates(sK237(X0),X3,X4)
| ~ list_succeeds(X3)
| ~ sP64(X0) ),
inference(cnf_transformation,[],[f636]) ).
fof(f1265,plain,
! [X0] :
( or(sK237(X0),sK238(X0)) = X0
| ~ sP64(X0) ),
inference(cnf_transformation,[],[f636]) ).
fof(f1266,plain,
! [X0,X6,X5] :
( eval_terminates(sK240(X0),X5,X6)
| ~ list_succeeds(X5)
| ~ sP63(X0) ),
inference(cnf_transformation,[],[f639]) ).
fof(f1268,plain,
! [X3,X0,X4] :
( eval_terminates(sK239(X0),X3,X4)
| ~ list_succeeds(X3)
| ~ sP63(X0) ),
inference(cnf_transformation,[],[f639]) ).
fof(f1270,plain,
! [X0] :
( and(sK239(X0),sK240(X0)) = X0
| ~ sP63(X0) ),
inference(cnf_transformation,[],[f639]) ).
fof(f1271,plain,
! [X2,X0,X1,X8,X7] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| eval_terminates(sK244,X7,X8)
| ~ list_succeeds(X7)
| sK241 = p(sK245) ),
inference(cnf_transformation,[],[f641]) ).
fof(f1273,plain,
! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| sK241 = neg(sK244)
| sK241 = p(sK245) ),
inference(cnf_transformation,[],[f641]) ).
fof(f1274,plain,
! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| list_succeeds(sK242) ),
inference(cnf_transformation,[],[f641]) ).
fof(f1275,plain,
! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| ~ eval_terminates(sK241,sK242,sK243) ),
inference(cnf_transformation,[],[f641]) ).
fof(f1276,plain,
formula_succeeds(sK246),
inference(cnf_transformation,[],[f642]) ).
fof(f1277,plain,
list_succeeds(sK247),
inference(cnf_transformation,[],[f642]) ).
fof(f1278,plain,
~ eval_terminates(sK246,sK247,sK248),
inference(cnf_transformation,[],[f642]) ).
fof(f1310,plain,
! [X2,X3,X1] :
( sP11(p(X3),X1,X2)
| '1' != X1
| ~ member_succeeds(p(X3),X2) ),
inference(equality_resolution,[],[f832]) ).
fof(f1311,plain,
! [X2,X3] :
( sP11(p(X3),'1',X2)
| ~ member_succeeds(p(X3),X2) ),
inference(equality_resolution,[],[f1310]) ).
fof(f1430,plain,
! [X0,X4] : member_succeeds(X0,cons(X0,X4)),
inference(equality_resolution,[],[f1201]) ).
fof(f1441,plain,
( ~ list_succeeds(sK247)
| ~ formula_succeeds(sK246)
| sP64(sK241)
| sP63(sK241)
| sK241 = neg(sK244)
| sK241 = p(sK245) ),
inference(resolution,[],[f1278,f1273]) ).
fof(f1442,plain,
( ~ list_succeeds(sK247)
| ~ formula_succeeds(sK246)
| list_succeeds(sK242) ),
inference(resolution,[],[f1278,f1274]) ).
fof(f1443,plain,
( ~ list_succeeds(sK247)
| ~ formula_succeeds(sK246)
| ~ eval_terminates(sK241,sK242,sK243) ),
inference(resolution,[],[f1278,f1275]) ).
fof(f1445,plain,
( ~ formula_succeeds(sK246)
| ~ eval_terminates(sK241,sK242,sK243) ),
inference(forward_subsumption_resolution,[],[f1443,f1277]) ).
fof(f1446,plain,
( ~ formula_succeeds(sK246)
| list_succeeds(sK242) ),
inference(forward_subsumption_resolution,[],[f1442,f1277]) ).
fof(f1447,plain,
( ~ formula_succeeds(sK246)
| sP64(sK241)
| sP63(sK241)
| sK241 = neg(sK244)
| sK241 = p(sK245) ),
inference(forward_subsumption_resolution,[],[f1441,f1277]) ).
fof(f1450,plain,
~ eval_terminates(sK241,sK242,sK243),
inference(forward_subsumption_resolution,[],[f1445,f1276]) ).
fof(f1451,plain,
list_succeeds(sK242),
inference(forward_subsumption_resolution,[],[f1446,f1276]) ).
fof(f1452,plain,
( sP64(sK241)
| sP63(sK241)
| sK241 = neg(sK244)
| sK241 = p(sK245) ),
inference(forward_subsumption_resolution,[],[f1447,f1276]) ).
fof(f1456,definition,
( spl249_1
<=> sK241 = p(sK245) ),
introduced(definition,[new_symbols(definition,[spl249_1])],[avatar_definition]) ).
fof(f1457,plain,
( sK241 = p(sK245)
| ~ spl249_1 ),
inference(avatar_component_clause,[],[f1456]) ).
fof(f1459,definition,
( spl249_2
<=> sK241 = neg(sK244) ),
introduced(definition,[new_symbols(definition,[spl249_2])],[avatar_definition]) ).
fof(f1460,plain,
( sK241 = neg(sK244)
| ~ spl249_2 ),
inference(avatar_component_clause,[],[f1459]) ).
fof(f1462,definition,
( spl249_3
<=> sP63(sK241) ),
introduced(definition,[new_symbols(definition,[spl249_3])],[avatar_definition]) ).
fof(f1463,plain,
( sP63(sK241)
| ~ spl249_3 ),
inference(avatar_component_clause,[],[f1462]) ).
fof(f1465,definition,
( spl249_4
<=> sP64(sK241) ),
introduced(definition,[new_symbols(definition,[spl249_4])],[avatar_definition]) ).
fof(f1466,plain,
( sP64(sK241)
| ~ spl249_4 ),
inference(avatar_component_clause,[],[f1465]) ).
fof(f1467,plain,
( spl249_1
| spl249_2
| spl249_3
| spl249_4 ),
inference(avatar_split_clause,[],[f1452,f1465,f1462,f1459,f1456]) ).
fof(f1479,plain,
! [X0] : member_terminates(X0,sK242),
inference(resolution,[],[f1451,f1224]) ).
fof(f1486,plain,
! [X2,X3,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| eval_terminates(sK244,sK242,X3)
| sK241 = p(sK245) ),
inference(resolution,[],[f1451,f1271]) ).
fof(f1508,plain,
~ sP38(sK242,sK243,sK241),
inference(resolution,[],[f1450,f952]) ).
fof(f1712,plain,
! [X0,X1] : sP31(X0,X1,sK242),
inference(resolution,[],[f1479,f936]) ).
fof(f1719,plain,
! [X0,X1] : sP32(X0,X1,sK242),
inference(resolution,[],[f1479,f932]) ).
fof(f1839,definition,
( spl249_31
<=> ! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ formula_succeeds(X0)
| ~ list_succeeds(X1) ) ),
introduced(definition,[new_symbols(definition,[spl249_31])],[avatar_definition]) ).
fof(f1840,plain,
( ! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ formula_succeeds(X0)
| ~ list_succeeds(X1) )
| ~ spl249_31 ),
inference(avatar_component_clause,[],[f1839]) ).
fof(f3120,definition,
( spl249_75
<=> '1' = sK243 ),
introduced(definition,[new_symbols(definition,[spl249_75])],[avatar_definition]) ).
fof(f3121,plain,
( '1' = sK243
| ~ spl249_75 ),
inference(avatar_component_clause,[],[f3120]) ).
fof(f6299,plain,
( ! [X0] :
( sP11(sK241,'1',X0)
| ~ member_succeeds(sK241,X0) )
| ~ spl249_1 ),
inference(superposition,[],[f1311,f1457]) ).
fof(f7032,plain,
( ! [X0] :
( ~ member_succeeds(sK241,X0)
| sK241 = p(sK97(sK241,'1',X0)) )
| ~ spl249_1 ),
inference(resolution,[],[f6299,f831]) ).
fof(f7065,plain,
( ! [X0] : sK241 = p(sK97(sK241,'1',cons(sK241,X0)))
| ~ spl249_1 ),
inference(resolution,[],[f7032,f1430]) ).
fof(f7093,plain,
( ! [X1] : neg(X1) != sK241
| ~ spl249_1 ),
inference(superposition,[],[f668,f7065]) ).
fof(f7095,plain,
( ! [X2,X1] : or(X1,X2) != sK241
| ~ spl249_1 ),
inference(superposition,[],[f670,f7065]) ).
fof(f8188,plain,
( ~ sP30(sK241,sK243,sK242)
| ~ eval_terminates(sK119(sK242,sK243,sK241),sK242,'1')
| ~ sP37(sK241,sK243,sK242)
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ sP32(sK241,sK243,sK242)
| ~ sP31(sK241,sK243,sK242) ),
inference(resolution,[],[f1508,f908]) ).
fof(f8189,plain,
( ~ sP30(sK241,sK243,sK242)
| '1' = sK243
| ~ sP37(sK241,sK243,sK242)
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ sP32(sK241,sK243,sK242)
| ~ sP31(sK241,sK243,sK242) ),
inference(resolution,[],[f1508,f909]) ).
fof(f8190,plain,
( ~ sP30(sK241,sK243,sK242)
| sK241 = or(sK118(sK242,sK243,sK241),sK119(sK242,sK243,sK241))
| ~ sP37(sK241,sK243,sK242)
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ sP32(sK241,sK243,sK242)
| ~ sP31(sK241,sK243,sK242) ),
inference(resolution,[],[f1508,f910]) ).
fof(f8191,plain,
( ~ sP30(sK241,sK243,sK242)
| ~ sP37(sK241,sK243,sK242)
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ sP32(sK241,sK243,sK242)
| ~ sP31(sK241,sK243,sK242)
| ~ spl249_1 ),
inference(forward_subsumption_resolution,[],[f8190,f7095]) ).
fof(f8192,plain,
( ~ sP30(sK241,sK243,sK242)
| '1' = sK243
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ sP32(sK241,sK243,sK242)
| ~ sP31(sK241,sK243,sK242) ),
inference(forward_subsumption_resolution,[],[f8189,f913]) ).
fof(f8193,plain,
( ~ sP30(sK241,sK243,sK242)
| ~ eval_terminates(sK119(sK242,sK243,sK241),sK242,'1')
| ~ sP37(sK241,sK243,sK242)
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ sP31(sK241,sK243,sK242) ),
inference(forward_subsumption_resolution,[],[f8188,f1719]) ).
fof(f8194,plain,
( ~ sP30(sK241,sK243,sK242)
| ~ sP37(sK241,sK243,sK242)
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ sP31(sK241,sK243,sK242)
| ~ spl249_1 ),
inference(forward_subsumption_resolution,[],[f8191,f1719]) ).
fof(f8195,plain,
( ~ sP30(sK241,sK243,sK242)
| '1' = sK243
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ sP32(sK241,sK243,sK242)
| ~ sP31(sK241,sK243,sK242) ),
inference(forward_subsumption_resolution,[],[f8192,f949]) ).
fof(f8196,plain,
( ~ sP30(sK241,sK243,sK242)
| ~ eval_terminates(sK119(sK242,sK243,sK241),sK242,'1')
| ~ sP37(sK241,sK243,sK242)
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242) ),
inference(forward_subsumption_resolution,[],[f8193,f1712]) ).
fof(f8197,plain,
( ~ sP30(sK241,sK243,sK242)
| ~ sP37(sK241,sK243,sK242)
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ spl249_1 ),
inference(forward_subsumption_resolution,[],[f8194,f1712]) ).
fof(f8198,plain,
( ~ sP30(sK241,sK243,sK242)
| '1' = sK243
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP32(sK241,sK243,sK242)
| ~ sP31(sK241,sK243,sK242) ),
inference(forward_subsumption_resolution,[],[f8195,f929]) ).
fof(f8200,definition,
( spl249_180
<=> sP33(sK241,sK243,sK242) ),
introduced(definition,[new_symbols(definition,[spl249_180])],[avatar_definition]) ).
fof(f8201,plain,
( ~ sP33(sK241,sK243,sK242)
| spl249_180 ),
inference(avatar_component_clause,[],[f8200]) ).
fof(f8203,definition,
( spl249_181
<=> sP34(sK241,sK243,sK242) ),
introduced(definition,[new_symbols(definition,[spl249_181])],[avatar_definition]) ).
fof(f8204,plain,
( ~ sP34(sK241,sK243,sK242)
| spl249_181 ),
inference(avatar_component_clause,[],[f8203]) ).
fof(f8206,definition,
( spl249_182
<=> sP29(sK241,sK243,sK242) ),
introduced(definition,[new_symbols(definition,[spl249_182])],[avatar_definition]) ).
fof(f8207,plain,
( ~ sP29(sK241,sK243,sK242)
| spl249_182 ),
inference(avatar_component_clause,[],[f8206]) ).
fof(f8209,definition,
( spl249_183
<=> sP35(sK241,sK243,sK242) ),
introduced(definition,[new_symbols(definition,[spl249_183])],[avatar_definition]) ).
fof(f8210,plain,
( ~ sP35(sK241,sK243,sK242)
| spl249_183 ),
inference(avatar_component_clause,[],[f8209]) ).
fof(f8212,definition,
( spl249_184
<=> sP36(sK241,sK243,sK242) ),
introduced(definition,[new_symbols(definition,[spl249_184])],[avatar_definition]) ).
fof(f8213,plain,
( ~ sP36(sK241,sK243,sK242)
| spl249_184 ),
inference(avatar_component_clause,[],[f8212]) ).
fof(f8215,definition,
( spl249_185
<=> sP37(sK241,sK243,sK242) ),
introduced(definition,[new_symbols(definition,[spl249_185])],[avatar_definition]) ).
fof(f8216,plain,
( ~ sP37(sK241,sK243,sK242)
| spl249_185 ),
inference(avatar_component_clause,[],[f8215]) ).
fof(f8218,definition,
( spl249_186
<=> eval_terminates(sK119(sK242,sK243,sK241),sK242,'1') ),
introduced(definition,[new_symbols(definition,[spl249_186])],[avatar_definition]) ).
fof(f8219,plain,
( ~ eval_terminates(sK119(sK242,sK243,sK241),sK242,'1')
| spl249_186 ),
inference(avatar_component_clause,[],[f8218]) ).
fof(f8221,definition,
( spl249_187
<=> sP30(sK241,sK243,sK242) ),
introduced(definition,[new_symbols(definition,[spl249_187])],[avatar_definition]) ).
fof(f8222,plain,
( ~ sP30(sK241,sK243,sK242)
| spl249_187 ),
inference(avatar_component_clause,[],[f8221]) ).
fof(f8223,plain,
( ~ spl249_180
| ~ spl249_181
| ~ spl249_182
| ~ spl249_183
| ~ spl249_184
| ~ spl249_185
| ~ spl249_186
| ~ spl249_187 ),
inference(avatar_split_clause,[],[f8196,f8221,f8218,f8215,f8212,f8209,f8206,f8203,f8200]) ).
fof(f8224,plain,
( ~ spl249_180
| ~ spl249_181
| ~ spl249_182
| ~ spl249_183
| ~ spl249_184
| ~ spl249_185
| ~ spl249_187
| ~ spl249_1 ),
inference(avatar_split_clause,[],[f8197,f1456,f8221,f8215,f8212,f8209,f8206,f8203,f8200]) ).
fof(f8225,plain,
( ~ sP30(sK241,sK243,sK242)
| '1' = sK243
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP32(sK241,sK243,sK242) ),
inference(forward_subsumption_resolution,[],[f8198,f937]) ).
fof(f8226,plain,
( ~ sP30(sK241,sK243,sK242)
| '1' = sK243
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242) ),
inference(forward_subsumption_resolution,[],[f8225,f1719]) ).
fof(f8227,plain,
( ~ spl249_181
| ~ spl249_183
| ~ spl249_184
| spl249_75
| ~ spl249_187 ),
inference(avatar_split_clause,[],[f8226,f8221,f3120,f8212,f8209,f8203]) ).
fof(f8229,plain,
( '0' = sK243
| spl249_181 ),
inference(resolution,[],[f8204,f925]) ).
fof(f8230,plain,
( sK241 = neg(sK126(sK241,sK243,sK242))
| spl249_181 ),
inference(resolution,[],[f8204,f926]) ).
fof(f8232,plain,
( $false
| ~ spl249_1
| spl249_181 ),
inference(forward_subsumption_resolution,[],[f8230,f7093]) ).
fof(f8233,plain,
( ~ spl249_1
| spl249_181 ),
inference(avatar_contradiction_clause,[],[f8232]) ).
fof(f8236,definition,
( spl249_188
<=> ! [X3] : eval_terminates(sK244,sK242,X3) ),
introduced(definition,[new_symbols(definition,[spl249_188])],[avatar_definition]) ).
fof(f8237,plain,
( ! [X3] : eval_terminates(sK244,sK242,X3)
| ~ spl249_188 ),
inference(avatar_component_clause,[],[f8236]) ).
fof(f8238,plain,
( spl249_1
| spl249_188
| spl249_3
| spl249_4
| spl249_31 ),
inference(avatar_split_clause,[],[f1486,f1839,f1465,f1462,f8236,f1456]) ).
fof(f8267,plain,
( ! [X0] : p(X0) != sK241
| ~ spl249_2 ),
inference(superposition,[],[f668,f1460]) ).
fof(f8410,plain,
( ~ sP34(sK241,'0',sK242)
| spl249_181 ),
inference(superposition,[],[f8204,f8229]) ).
fof(f8726,plain,
( ~ formula_succeeds(sK246)
| ~ list_succeeds(sK247)
| ~ spl249_31 ),
inference(resolution,[],[f1840,f1278]) ).
fof(f8729,plain,
( ~ list_succeeds(sK247)
| ~ spl249_31 ),
inference(forward_subsumption_resolution,[],[f8726,f1276]) ).
fof(f8736,plain,
( $false
| ~ spl249_31 ),
inference(forward_subsumption_resolution,[],[f8729,f1277]) ).
fof(f8737,plain,
~ spl249_31,
inference(avatar_contradiction_clause,[],[f8736]) ).
fof(f8877,plain,
( ~ eval_terminates(sK130(sK241,sK243,sK242),sK242,'0')
| ~ eval_terminates(sK131(sK241,sK243,sK242),sK242,'0')
| spl249_187 ),
inference(resolution,[],[f8222,f941]) ).
fof(f8879,plain,
( '0' = sK243
| spl249_187 ),
inference(resolution,[],[f8222,f943]) ).
fof(f8880,plain,
( sK241 = or(sK130(sK241,sK243,sK242),sK131(sK241,sK243,sK242))
| spl249_187 ),
inference(resolution,[],[f8222,f944]) ).
fof(f8883,plain,
( ~ eval_terminates(sK130(sK241,'0',sK242),sK242,'0')
| ~ eval_terminates(sK131(sK241,sK243,sK242),sK242,'0')
| spl249_187 ),
inference(forward_demodulation,[],[f8877,f8879]) ).
fof(f8885,plain,
( ~ eval_terminates(sK131(sK241,'0',sK242),sK242,'0')
| ~ eval_terminates(sK130(sK241,'0',sK242),sK242,'0')
| spl249_187 ),
inference(forward_demodulation,[],[f8883,f8879]) ).
fof(f8887,definition,
( spl249_233
<=> eval_terminates(sK130(sK241,'0',sK242),sK242,'0') ),
introduced(definition,[new_symbols(definition,[spl249_233])],[avatar_definition]) ).
fof(f8888,plain,
( ~ eval_terminates(sK130(sK241,'0',sK242),sK242,'0')
| spl249_233 ),
inference(avatar_component_clause,[],[f8887]) ).
fof(f8894,definition,
( spl249_235
<=> eval_terminates(sK131(sK241,'0',sK242),sK242,'0') ),
introduced(definition,[new_symbols(definition,[spl249_235])],[avatar_definition]) ).
fof(f8895,plain,
( ~ eval_terminates(sK131(sK241,'0',sK242),sK242,'0')
| spl249_235 ),
inference(avatar_component_clause,[],[f8894]) ).
fof(f8896,plain,
( ~ spl249_233
| ~ spl249_235
| spl249_187 ),
inference(avatar_split_clause,[],[f8885,f8221,f8894,f8887]) ).
fof(f8907,plain,
( ! [X0] : p(X0) != sK241
| spl249_187 ),
inference(superposition,[],[f670,f8880]) ).
fof(f8908,plain,
( ! [X0] : neg(X0) != sK241
| spl249_187 ),
inference(superposition,[],[f673,f8880]) ).
fof(f9129,plain,
( sK241 != sK241
| ~ spl249_1
| spl249_187 ),
inference(superposition,[],[f8907,f1457]) ).
fof(f9136,plain,
( $false
| ~ spl249_1
| spl249_187 ),
inference(trivial_inequality_removal,[],[f9129]) ).
fof(f9137,plain,
( ~ spl249_1
| spl249_187 ),
inference(avatar_contradiction_clause,[],[f9136]) ).
fof(f9141,plain,
( '0' = sK243
| spl249_184 ),
inference(resolution,[],[f8213,f917]) ).
fof(f9142,plain,
( sK241 = and(sK122(sK241,sK243,sK242),sK123(sK241,sK243,sK242))
| spl249_184 ),
inference(resolution,[],[f8213,f918]) ).
fof(f9149,plain,
( ! [X0] : p(X0) != sK241
| spl249_184 ),
inference(superposition,[],[f669,f9142]) ).
fof(f9150,plain,
( ! [X0] : neg(X0) != sK241
| spl249_184 ),
inference(superposition,[],[f672,f9142]) ).
fof(f9265,plain,
( '0' = sK243
| spl249_183 ),
inference(resolution,[],[f8210,f921]) ).
fof(f9266,plain,
( sK241 = and(sK124(sK241,sK243,sK242),sK125(sK241,sK243,sK242))
| spl249_183 ),
inference(resolution,[],[f8210,f922]) ).
fof(f9273,plain,
( ! [X0] : p(X0) != sK241
| spl249_183 ),
inference(superposition,[],[f669,f9266]) ).
fof(f9274,plain,
( ! [X0] : neg(X0) != sK241
| spl249_183 ),
inference(superposition,[],[f672,f9266]) ).
fof(f9401,plain,
( ! [X0] :
( neg(X0) != sK241
| sK244 = X0 )
| ~ spl249_2 ),
inference(superposition,[],[f671,f1460]) ).
fof(f9436,plain,
( sK241 = neg(sK126(sK241,sK243,sK242))
| spl249_181 ),
inference(resolution,[],[f8204,f926]) ).
fof(f9439,plain,
( sK241 = neg(sK126(sK241,'0',sK242))
| spl249_181 ),
inference(forward_demodulation,[],[f9436,f8229]) ).
fof(f9463,plain,
( ! [X0,X1] : and(X0,X1) != sK241
| spl249_181 ),
inference(superposition,[],[f672,f9439]) ).
fof(f9464,plain,
( ! [X0,X1] : or(X0,X1) != sK241
| spl249_181 ),
inference(superposition,[],[f673,f9439]) ).
fof(f9901,plain,
( sK241 != sK241
| sK244 = sK126(sK241,'0',sK242)
| ~ spl249_2
| spl249_181 ),
inference(superposition,[],[f9401,f9439]) ).
fof(f9938,plain,
( sK244 = sK126(sK241,'0',sK242)
| ~ spl249_2
| spl249_181 ),
inference(trivial_inequality_removal,[],[f9901]) ).
fof(f9988,plain,
( ~ eval_terminates(sK244,sK242,'1')
| sP34(sK241,'0',sK242)
| ~ spl249_2
| spl249_181 ),
inference(superposition,[],[f924,f9938]) ).
fof(f9990,plain,
( sP34(sK241,'0',sK242)
| ~ spl249_2
| spl249_181
| ~ spl249_188 ),
inference(forward_subsumption_resolution,[],[f9988,f8237]) ).
fof(f9993,plain,
( $false
| ~ spl249_2
| spl249_181
| ~ spl249_188 ),
inference(forward_subsumption_resolution,[],[f9990,f8410]) ).
fof(f9994,plain,
( ~ spl249_2
| spl249_181
| ~ spl249_188 ),
inference(avatar_contradiction_clause,[],[f9993]) ).
fof(f10000,plain,
( sK241 = and(sK239(sK241),sK240(sK241))
| ~ spl249_3 ),
inference(resolution,[],[f1463,f1270]) ).
fof(f10001,plain,
( $false
| ~ spl249_3
| spl249_181 ),
inference(forward_subsumption_resolution,[],[f10000,f9463]) ).
fof(f10002,plain,
( ~ spl249_3
| spl249_181 ),
inference(avatar_contradiction_clause,[],[f10001]) ).
fof(f10007,plain,
( sK241 = or(sK237(sK241),sK238(sK241))
| ~ spl249_4 ),
inference(resolution,[],[f1466,f1265]) ).
fof(f10008,plain,
( $false
| ~ spl249_4
| spl249_181 ),
inference(forward_subsumption_resolution,[],[f10007,f9464]) ).
fof(f10009,plain,
( ~ spl249_4
| spl249_181 ),
inference(avatar_contradiction_clause,[],[f10008]) ).
fof(f10215,plain,
( ! [X2,X0,X1] :
( sK241 != sK241
| eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| sK241 = p(sK245) )
| spl249_187 ),
inference(superposition,[],[f8908,f1273]) ).
fof(f10216,plain,
( ! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| sK241 = p(sK245) )
| spl249_187 ),
inference(trivial_inequality_removal,[],[f10215]) ).
fof(f10221,plain,
( ! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241) )
| ~ spl249_2
| spl249_187 ),
inference(forward_subsumption_resolution,[],[f10216,f8267]) ).
fof(f10246,plain,
( spl249_3
| spl249_4
| spl249_31
| ~ spl249_2
| spl249_187 ),
inference(avatar_split_clause,[],[f10221,f8221,f1459,f1839,f1465,f1462]) ).
fof(f10255,plain,
( ~ sP36(sK241,'0',sK242)
| spl249_184 ),
inference(superposition,[],[f8213,f9141]) ).
fof(f10423,plain,
( ! [X2,X0,X1] :
( sK241 != sK241
| eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| sK241 = p(sK245) )
| spl249_184 ),
inference(superposition,[],[f9150,f1273]) ).
fof(f10424,plain,
( ! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| sK241 = p(sK245) )
| spl249_184 ),
inference(trivial_inequality_removal,[],[f10423]) ).
fof(f10429,plain,
( ! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241) )
| ~ spl249_2
| spl249_184 ),
inference(forward_subsumption_resolution,[],[f10424,f8267]) ).
fof(f10454,plain,
( spl249_3
| spl249_4
| spl249_31
| ~ spl249_2
| spl249_184 ),
inference(avatar_split_clause,[],[f10429,f8212,f1459,f1839,f1465,f1462]) ).
fof(f10455,plain,
( ~ eval_terminates(sK119(sK242,'1',sK241),sK242,'1')
| ~ spl249_75
| spl249_186 ),
inference(forward_demodulation,[],[f8219,f3121]) ).
fof(f10456,plain,
( ~ sP30(sK241,sK243,sK242)
| sK241 = or(sK118(sK242,sK243,sK241),sK119(sK242,sK243,sK241))
| ~ sP37(sK241,sK243,sK242)
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ sP31(sK241,sK243,sK242) ),
inference(forward_subsumption_resolution,[],[f8190,f1719]) ).
fof(f10457,plain,
( ~ sP30(sK241,sK243,sK242)
| sK241 = or(sK118(sK242,sK243,sK241),sK119(sK242,sK243,sK241))
| ~ sP37(sK241,sK243,sK242)
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242) ),
inference(forward_subsumption_resolution,[],[f10456,f1712]) ).
fof(f10458,plain,
( ~ sP30(sK241,'1',sK242)
| sK241 = or(sK118(sK242,sK243,sK241),sK119(sK242,sK243,sK241))
| ~ sP37(sK241,sK243,sK242)
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ spl249_75 ),
inference(forward_demodulation,[],[f10457,f3121]) ).
fof(f10459,plain,
( sK241 = or(sK118(sK242,'1',sK241),sK119(sK242,'1',sK241))
| ~ sP30(sK241,'1',sK242)
| ~ sP37(sK241,sK243,sK242)
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ spl249_75 ),
inference(forward_demodulation,[],[f10458,f3121]) ).
fof(f10460,plain,
( ~ sP37(sK241,'1',sK242)
| sK241 = or(sK118(sK242,'1',sK241),sK119(sK242,'1',sK241))
| ~ sP30(sK241,'1',sK242)
| ~ sP36(sK241,sK243,sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ spl249_75 ),
inference(forward_demodulation,[],[f10459,f3121]) ).
fof(f10461,plain,
( ~ sP36(sK241,'1',sK242)
| ~ sP37(sK241,'1',sK242)
| sK241 = or(sK118(sK242,'1',sK241),sK119(sK242,'1',sK241))
| ~ sP30(sK241,'1',sK242)
| ~ sP35(sK241,sK243,sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ spl249_75 ),
inference(forward_demodulation,[],[f10460,f3121]) ).
fof(f10462,plain,
( ~ sP35(sK241,'1',sK242)
| ~ sP36(sK241,'1',sK242)
| ~ sP37(sK241,'1',sK242)
| sK241 = or(sK118(sK242,'1',sK241),sK119(sK242,'1',sK241))
| ~ sP30(sK241,'1',sK242)
| ~ sP29(sK241,sK243,sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ spl249_75 ),
inference(forward_demodulation,[],[f10461,f3121]) ).
fof(f10463,plain,
( ~ sP29(sK241,'1',sK242)
| ~ sP35(sK241,'1',sK242)
| ~ sP36(sK241,'1',sK242)
| ~ sP37(sK241,'1',sK242)
| sK241 = or(sK118(sK242,'1',sK241),sK119(sK242,'1',sK241))
| ~ sP30(sK241,'1',sK242)
| ~ sP34(sK241,sK243,sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ spl249_75 ),
inference(forward_demodulation,[],[f10462,f3121]) ).
fof(f10464,plain,
( ~ sP34(sK241,'1',sK242)
| ~ sP29(sK241,'1',sK242)
| ~ sP35(sK241,'1',sK242)
| ~ sP36(sK241,'1',sK242)
| ~ sP37(sK241,'1',sK242)
| sK241 = or(sK118(sK242,'1',sK241),sK119(sK242,'1',sK241))
| ~ sP30(sK241,'1',sK242)
| ~ sP33(sK241,sK243,sK242)
| ~ spl249_75 ),
inference(forward_demodulation,[],[f10463,f3121]) ).
fof(f10465,plain,
( ~ sP33(sK241,'1',sK242)
| ~ sP34(sK241,'1',sK242)
| ~ sP29(sK241,'1',sK242)
| ~ sP35(sK241,'1',sK242)
| ~ sP36(sK241,'1',sK242)
| ~ sP37(sK241,'1',sK242)
| sK241 = or(sK118(sK242,'1',sK241),sK119(sK242,'1',sK241))
| ~ sP30(sK241,'1',sK242)
| ~ spl249_75 ),
inference(forward_demodulation,[],[f10464,f3121]) ).
fof(f10467,definition,
( spl249_258
<=> sP30(sK241,'1',sK242) ),
introduced(definition,[new_symbols(definition,[spl249_258])],[avatar_definition]) ).
fof(f10468,plain,
( ~ sP30(sK241,'1',sK242)
| spl249_258 ),
inference(avatar_component_clause,[],[f10467]) ).
fof(f10470,definition,
( spl249_259
<=> sK241 = or(sK118(sK242,'1',sK241),sK119(sK242,'1',sK241)) ),
introduced(definition,[new_symbols(definition,[spl249_259])],[avatar_definition]) ).
fof(f10471,plain,
( sK241 = or(sK118(sK242,'1',sK241),sK119(sK242,'1',sK241))
| ~ spl249_259 ),
inference(avatar_component_clause,[],[f10470]) ).
fof(f10473,definition,
( spl249_260
<=> sP37(sK241,'1',sK242) ),
introduced(definition,[new_symbols(definition,[spl249_260])],[avatar_definition]) ).
fof(f10474,plain,
( ~ sP37(sK241,'1',sK242)
| spl249_260 ),
inference(avatar_component_clause,[],[f10473]) ).
fof(f10476,definition,
( spl249_261
<=> sP36(sK241,'1',sK242) ),
introduced(definition,[new_symbols(definition,[spl249_261])],[avatar_definition]) ).
fof(f10477,plain,
( ~ sP36(sK241,'1',sK242)
| spl249_261 ),
inference(avatar_component_clause,[],[f10476]) ).
fof(f10479,definition,
( spl249_262
<=> sP35(sK241,'1',sK242) ),
introduced(definition,[new_symbols(definition,[spl249_262])],[avatar_definition]) ).
fof(f10480,plain,
( ~ sP35(sK241,'1',sK242)
| spl249_262 ),
inference(avatar_component_clause,[],[f10479]) ).
fof(f10482,definition,
( spl249_263
<=> sP29(sK241,'1',sK242) ),
introduced(definition,[new_symbols(definition,[spl249_263])],[avatar_definition]) ).
fof(f10483,plain,
( ~ sP29(sK241,'1',sK242)
| spl249_263 ),
inference(avatar_component_clause,[],[f10482]) ).
fof(f10485,definition,
( spl249_264
<=> sP34(sK241,'1',sK242) ),
introduced(definition,[new_symbols(definition,[spl249_264])],[avatar_definition]) ).
fof(f10486,plain,
( ~ sP34(sK241,'1',sK242)
| spl249_264 ),
inference(avatar_component_clause,[],[f10485]) ).
fof(f10488,definition,
( spl249_265
<=> sP33(sK241,'1',sK242) ),
introduced(definition,[new_symbols(definition,[spl249_265])],[avatar_definition]) ).
fof(f10489,plain,
( ~ sP33(sK241,'1',sK242)
| spl249_265 ),
inference(avatar_component_clause,[],[f10488]) ).
fof(f10490,plain,
( ~ spl249_258
| spl249_259
| ~ spl249_260
| ~ spl249_261
| ~ spl249_262
| ~ spl249_263
| ~ spl249_264
| ~ spl249_265
| ~ spl249_75 ),
inference(avatar_split_clause,[],[f10465,f3120,f10488,f10485,f10482,f10479,f10476,f10473,f10470,f10467]) ).
fof(f10999,plain,
( '1' = '0'
| spl249_258 ),
inference(resolution,[],[f10468,f943]) ).
fof(f11022,plain,
( $false
| spl249_258 ),
inference(forward_subsumption_resolution,[],[f10999,f658]) ).
fof(f11023,plain,
spl249_258,
inference(avatar_contradiction_clause,[],[f11022]) ).
fof(f12050,plain,
( sK241 = or(sK120(sK241,'1',sK242),sK121(sK241,'1',sK242))
| spl249_260 ),
inference(resolution,[],[f10474,f914]) ).
fof(f12100,plain,
( ! [X0] : p(X0) != sK241
| spl249_260 ),
inference(superposition,[],[f670,f12050]) ).
fof(f12101,plain,
( ! [X0] : neg(X0) != sK241
| spl249_260 ),
inference(superposition,[],[f673,f12050]) ).
fof(f13233,plain,
( ! [X2,X0,X1] :
( sK241 != sK241
| eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| sK241 = p(sK245) )
| spl249_260 ),
inference(superposition,[],[f12101,f1273]) ).
fof(f13234,plain,
( ! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| sK241 = p(sK245) )
| spl249_260 ),
inference(trivial_inequality_removal,[],[f13233]) ).
fof(f13239,plain,
( ! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241) )
| ~ spl249_2
| spl249_260 ),
inference(forward_subsumption_resolution,[],[f13234,f8267]) ).
fof(f13264,plain,
( spl249_3
| spl249_4
| spl249_31
| ~ spl249_2
| spl249_260 ),
inference(avatar_split_clause,[],[f13239,f10473,f1459,f1839,f1465,f1462]) ).
fof(f13268,plain,
( sK241 = neg(sK127(sK241,'1',sK242))
| spl249_265 ),
inference(resolution,[],[f10489,f930]) ).
fof(f13316,plain,
( ! [X0] : p(X0) != sK241
| spl249_265 ),
inference(superposition,[],[f668,f13268]) ).
fof(f13350,plain,
( sK241 != sK241
| sK244 = sK127(sK241,'1',sK242)
| ~ spl249_2
| spl249_265 ),
inference(superposition,[],[f9401,f13268]) ).
fof(f13354,plain,
( sK244 = sK127(sK241,'1',sK242)
| ~ spl249_2
| spl249_265 ),
inference(trivial_inequality_removal,[],[f13350]) ).
fof(f13411,plain,
( ~ eval_terminates(sK244,sK242,'0')
| sP33(sK241,'1',sK242)
| ~ spl249_2
| spl249_265 ),
inference(superposition,[],[f928,f13354]) ).
fof(f13413,plain,
( sP33(sK241,'1',sK242)
| ~ spl249_2
| ~ spl249_188
| spl249_265 ),
inference(forward_subsumption_resolution,[],[f13411,f8237]) ).
fof(f13417,plain,
( $false
| ~ spl249_2
| ~ spl249_188
| spl249_265 ),
inference(forward_subsumption_resolution,[],[f13413,f10489]) ).
fof(f13418,plain,
( ~ spl249_2
| ~ spl249_188
| spl249_265 ),
inference(avatar_contradiction_clause,[],[f13417]) ).
fof(f13429,plain,
( '1' = '0'
| spl249_261 ),
inference(resolution,[],[f10477,f917]) ).
fof(f13450,plain,
( $false
| spl249_261 ),
inference(forward_subsumption_resolution,[],[f13429,f658]) ).
fof(f13451,plain,
spl249_261,
inference(avatar_contradiction_clause,[],[f13450]) ).
fof(f13462,plain,
( '1' = '0'
| spl249_262 ),
inference(resolution,[],[f10480,f921]) ).
fof(f13483,plain,
( $false
| spl249_262 ),
inference(forward_subsumption_resolution,[],[f13462,f658]) ).
fof(f13484,plain,
spl249_262,
inference(avatar_contradiction_clause,[],[f13483]) ).
fof(f13494,plain,
( ~ eval_terminates(sK132(sK241,'1',sK242),sK242,'1')
| ~ eval_terminates(sK133(sK241,'1',sK242),sK242,'1')
| spl249_263 ),
inference(resolution,[],[f10483,f947]) ).
fof(f13497,plain,
( sK241 = and(sK132(sK241,'1',sK242),sK133(sK241,'1',sK242))
| spl249_263 ),
inference(resolution,[],[f10483,f950]) ).
fof(f13521,definition,
( spl249_338
<=> eval_terminates(sK132(sK241,'1',sK242),sK242,'1') ),
introduced(definition,[new_symbols(definition,[spl249_338])],[avatar_definition]) ).
fof(f13522,plain,
( ~ eval_terminates(sK132(sK241,'1',sK242),sK242,'1')
| spl249_338 ),
inference(avatar_component_clause,[],[f13521]) ).
fof(f13525,definition,
( spl249_339
<=> eval_terminates(sK133(sK241,'1',sK242),sK242,'1') ),
introduced(definition,[new_symbols(definition,[spl249_339])],[avatar_definition]) ).
fof(f13526,plain,
( ~ eval_terminates(sK133(sK241,'1',sK242),sK242,'1')
| spl249_339 ),
inference(avatar_component_clause,[],[f13525]) ).
fof(f13527,plain,
( ~ spl249_339
| ~ spl249_338
| spl249_263 ),
inference(avatar_split_clause,[],[f13494,f10482,f13521,f13525]) ).
fof(f13556,plain,
( ! [X0] : p(X0) != sK241
| spl249_263 ),
inference(superposition,[],[f669,f13497]) ).
fof(f13557,plain,
( ! [X0] : neg(X0) != sK241
| spl249_263 ),
inference(superposition,[],[f672,f13497]) ).
fof(f13727,plain,
( ! [X2,X0,X1] :
( sK241 != sK241
| eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| sK241 = p(sK245) )
| spl249_263 ),
inference(superposition,[],[f13557,f1273]) ).
fof(f13728,plain,
( ! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| sK241 = p(sK245) )
| spl249_263 ),
inference(trivial_inequality_removal,[],[f13727]) ).
fof(f13733,plain,
( ! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241) )
| ~ spl249_2
| spl249_263 ),
inference(forward_subsumption_resolution,[],[f13728,f8267]) ).
fof(f13758,plain,
( spl249_3
| spl249_4
| spl249_31
| ~ spl249_2
| spl249_263 ),
inference(avatar_split_clause,[],[f13733,f10482,f1459,f1839,f1465,f1462]) ).
fof(f13760,plain,
( '1' = '0'
| spl249_264 ),
inference(resolution,[],[f10486,f925]) ).
fof(f13781,plain,
( $false
| spl249_264 ),
inference(forward_subsumption_resolution,[],[f13760,f658]) ).
fof(f13782,plain,
spl249_264,
inference(avatar_contradiction_clause,[],[f13781]) ).
fof(f13812,plain,
( ! [X0] : neg(X0) != sK241
| ~ spl249_259 ),
inference(superposition,[],[f673,f10471]) ).
fof(f13813,plain,
( ! [X0,X1] : and(X0,X1) != sK241
| ~ spl249_259 ),
inference(superposition,[],[f676,f10471]) ).
fof(f14159,plain,
( ! [X2,X0,X1] :
( sK241 != sK241
| eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| sK241 = p(sK245) )
| ~ spl249_259 ),
inference(superposition,[],[f13812,f1273]) ).
fof(f14160,plain,
( ! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| sK241 = p(sK245) )
| ~ spl249_259 ),
inference(trivial_inequality_removal,[],[f14159]) ).
fof(f14165,plain,
( ! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241) )
| ~ spl249_2
| ~ spl249_259 ),
inference(forward_subsumption_resolution,[],[f14160,f8267]) ).
fof(f14211,plain,
( spl249_3
| spl249_4
| spl249_31
| ~ spl249_2
| ~ spl249_259 ),
inference(avatar_split_clause,[],[f14165,f10470,f1459,f1839,f1465,f1462]) ).
fof(f14233,plain,
( ~ sP35(sK241,'0',sK242)
| spl249_183 ),
inference(superposition,[],[f8210,f9265]) ).
fof(f14458,plain,
( ! [X2,X0,X1] :
( sK241 != sK241
| eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| sK241 = p(sK245) )
| spl249_183 ),
inference(superposition,[],[f9274,f1273]) ).
fof(f14459,plain,
( ! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241)
| sK241 = p(sK245) )
| spl249_183 ),
inference(trivial_inequality_removal,[],[f14458]) ).
fof(f14464,plain,
( ! [X2,X0,X1] :
( eval_terminates(X0,X1,X2)
| ~ list_succeeds(X1)
| ~ formula_succeeds(X0)
| sP64(sK241)
| sP63(sK241) )
| ~ spl249_2
| spl249_183 ),
inference(forward_subsumption_resolution,[],[f14459,f8267]) ).
fof(f14489,plain,
( spl249_3
| spl249_4
| spl249_31
| ~ spl249_2
| spl249_183 ),
inference(avatar_split_clause,[],[f14464,f8209,f1459,f1839,f1465,f1462]) ).
fof(f14799,plain,
( sK241 != sK241
| ~ spl249_1
| spl249_184 ),
inference(superposition,[],[f9149,f1457]) ).
fof(f14806,plain,
( $false
| ~ spl249_1
| spl249_184 ),
inference(trivial_inequality_removal,[],[f14799]) ).
fof(f14807,plain,
( ~ spl249_1
| spl249_184 ),
inference(avatar_contradiction_clause,[],[f14806]) ).
fof(f15013,plain,
( sK241 != sK241
| ~ spl249_1
| spl249_183 ),
inference(superposition,[],[f9273,f1457]) ).
fof(f15020,plain,
( $false
| ~ spl249_1
| spl249_183 ),
inference(trivial_inequality_removal,[],[f15013]) ).
fof(f15021,plain,
( ~ spl249_1
| spl249_183 ),
inference(avatar_contradiction_clause,[],[f15020]) ).
fof(f15024,plain,
( ~ sP37(sK241,'1',sK242)
| ~ spl249_75
| spl249_185 ),
inference(forward_demodulation,[],[f8216,f3121]) ).
fof(f15027,plain,
( ~ spl249_260
| ~ spl249_75
| spl249_185 ),
inference(avatar_split_clause,[],[f15024,f8215,f3120,f10473]) ).
fof(f15035,plain,
( ~ sP33(sK241,'1',sK242)
| ~ spl249_75
| spl249_180 ),
inference(forward_demodulation,[],[f8201,f3121]) ).
fof(f15198,plain,
( sK241 != sK241
| ~ spl249_1
| spl249_265 ),
inference(superposition,[],[f13316,f1457]) ).
fof(f15205,plain,
( $false
| ~ spl249_1
| spl249_265 ),
inference(trivial_inequality_removal,[],[f15198]) ).
fof(f15206,plain,
( ~ spl249_1
| spl249_265 ),
inference(avatar_contradiction_clause,[],[f15205]) ).
fof(f15209,plain,
( ~ spl249_265
| ~ spl249_75
| spl249_180 ),
inference(avatar_split_clause,[],[f15035,f8200,f3120,f10488]) ).
fof(f15210,plain,
( ~ sP29(sK241,'1',sK242)
| ~ spl249_75
| spl249_182 ),
inference(forward_demodulation,[],[f8207,f3121]) ).
fof(f15423,plain,
( sK241 != sK241
| ~ spl249_1
| spl249_263 ),
inference(superposition,[],[f13556,f1457]) ).
fof(f15430,plain,
( $false
| ~ spl249_1
| spl249_263 ),
inference(trivial_inequality_removal,[],[f15423]) ).
fof(f15431,plain,
( ~ spl249_1
| spl249_263 ),
inference(avatar_contradiction_clause,[],[f15430]) ).
fof(f15434,plain,
( ~ spl249_263
| ~ spl249_75
| spl249_182 ),
inference(avatar_split_clause,[],[f15210,f8206,f3120,f10482]) ).
fof(f15590,plain,
( sK241 != sK241
| ~ spl249_1
| spl249_260 ),
inference(superposition,[],[f12100,f1457]) ).
fof(f15597,plain,
( $false
| ~ spl249_1
| spl249_260 ),
inference(trivial_inequality_removal,[],[f15590]) ).
fof(f15598,plain,
( ~ spl249_1
| spl249_260 ),
inference(avatar_contradiction_clause,[],[f15597]) ).
fof(f15605,plain,
( sK241 = or(sK237(sK241),sK238(sK241))
| ~ spl249_4 ),
inference(resolution,[],[f1466,f1265]) ).
fof(f15611,plain,
( ! [X0] : neg(X0) != sK241
| ~ spl249_4 ),
inference(superposition,[],[f673,f15605]) ).
fof(f15612,plain,
( ! [X0,X1] : and(X0,X1) != sK241
| ~ spl249_4 ),
inference(superposition,[],[f676,f15605]) ).
fof(f15614,plain,
( ! [X0,X1] :
( or(X0,X1) != sK241
| sK238(sK241) = X1 )
| ~ spl249_4 ),
inference(superposition,[],[f677,f15605]) ).
fof(f15616,plain,
( ! [X0,X1] :
( or(X0,X1) != sK241
| sK237(sK241) = X0 )
| ~ spl249_4 ),
inference(superposition,[],[f678,f15605]) ).
fof(f15799,plain,
( sK241 != sK241
| sK237(sK241) = sK118(sK242,'1',sK241)
| ~ spl249_4
| ~ spl249_259 ),
inference(superposition,[],[f15616,f10471]) ).
fof(f15839,plain,
( sK237(sK241) = sK118(sK242,'1',sK241)
| ~ spl249_4
| ~ spl249_259 ),
inference(trivial_inequality_removal,[],[f15799]) ).
fof(f15900,plain,
( sK241 = or(sK237(sK241),sK119(sK242,'1',sK241))
| ~ spl249_4
| ~ spl249_259 ),
inference(superposition,[],[f10471,f15839]) ).
fof(f16037,plain,
( sK241 != sK241
| sK238(sK241) = sK119(sK242,'1',sK241)
| ~ spl249_4
| ~ spl249_259 ),
inference(superposition,[],[f15614,f15900]) ).
fof(f16038,plain,
( sK238(sK241) = sK119(sK242,'1',sK241)
| ~ spl249_4
| ~ spl249_259 ),
inference(trivial_inequality_removal,[],[f16037]) ).
fof(f16100,plain,
( ~ eval_terminates(sK238(sK241),sK242,'1')
| ~ spl249_4
| ~ spl249_75
| spl249_186
| ~ spl249_259 ),
inference(superposition,[],[f10455,f16038]) ).
fof(f16190,plain,
( ~ list_succeeds(sK242)
| ~ sP64(sK241)
| ~ spl249_4
| ~ spl249_75
| spl249_186
| ~ spl249_259 ),
inference(resolution,[],[f16100,f1261]) ).
fof(f16220,plain,
( ~ sP64(sK241)
| ~ spl249_4
| ~ spl249_75
| spl249_186
| ~ spl249_259 ),
inference(forward_subsumption_resolution,[],[f16190,f1451]) ).
fof(f16228,plain,
( $false
| ~ spl249_4
| ~ spl249_75
| spl249_186
| ~ spl249_259 ),
inference(forward_subsumption_resolution,[],[f16220,f1466]) ).
fof(f16229,plain,
( ~ spl249_4
| ~ spl249_75
| spl249_186
| ~ spl249_259 ),
inference(avatar_contradiction_clause,[],[f16228]) ).
fof(f16284,plain,
( sK241 = or(sK120(sK241,'1',sK242),sK121(sK241,'1',sK242))
| spl249_260 ),
inference(resolution,[],[f10474,f914]) ).
fof(f16374,plain,
( sK241 != sK241
| sK237(sK241) = sK120(sK241,'1',sK242)
| ~ spl249_4
| spl249_260 ),
inference(superposition,[],[f15616,f16284]) ).
fof(f16375,plain,
( sK237(sK241) = sK120(sK241,'1',sK242)
| ~ spl249_4
| spl249_260 ),
inference(trivial_inequality_removal,[],[f16374]) ).
fof(f16442,plain,
( ~ eval_terminates(sK237(sK241),sK242,'1')
| sP37(sK241,'1',sK242)
| ~ spl249_4
| spl249_260 ),
inference(superposition,[],[f912,f16375]) ).
fof(f16445,plain,
( ~ eval_terminates(sK237(sK241),sK242,'1')
| ~ spl249_4
| spl249_260 ),
inference(forward_subsumption_resolution,[],[f16442,f10474]) ).
fof(f16494,plain,
( ~ list_succeeds(sK242)
| ~ sP64(sK241)
| ~ spl249_4
| spl249_260 ),
inference(resolution,[],[f16445,f1263]) ).
fof(f16524,plain,
( ~ sP64(sK241)
| ~ spl249_4
| spl249_260 ),
inference(forward_subsumption_resolution,[],[f16494,f1451]) ).
fof(f16532,plain,
( $false
| ~ spl249_4
| spl249_260 ),
inference(forward_subsumption_resolution,[],[f16524,f1466]) ).
fof(f16533,plain,
( ~ spl249_4
| spl249_260 ),
inference(avatar_contradiction_clause,[],[f16532]) ).
fof(f16724,plain,
( sK241 = neg(sK127(sK241,'1',sK242))
| spl249_265 ),
inference(resolution,[],[f10489,f930]) ).
fof(f16744,plain,
( $false
| ~ spl249_4
| spl249_265 ),
inference(forward_subsumption_resolution,[],[f16724,f15611]) ).
fof(f16745,plain,
( ~ spl249_4
| spl249_265 ),
inference(avatar_contradiction_clause,[],[f16744]) ).
fof(f16758,plain,
( sK241 = and(sK132(sK241,'1',sK242),sK133(sK241,'1',sK242))
| spl249_263 ),
inference(resolution,[],[f10483,f950]) ).
fof(f16778,plain,
( $false
| ~ spl249_4
| spl249_263 ),
inference(forward_subsumption_resolution,[],[f16758,f15612]) ).
fof(f16779,plain,
( ~ spl249_4
| spl249_263 ),
inference(avatar_contradiction_clause,[],[f16778]) ).
fof(f16808,plain,
( sK241 = and(sK124(sK241,sK243,sK242),sK125(sK241,sK243,sK242))
| spl249_183 ),
inference(resolution,[],[f8210,f922]) ).
fof(f16811,plain,
( $false
| ~ spl249_4
| spl249_183 ),
inference(forward_subsumption_resolution,[],[f16808,f15612]) ).
fof(f16812,plain,
( ~ spl249_4
| spl249_183 ),
inference(avatar_contradiction_clause,[],[f16811]) ).
fof(f16820,plain,
( sK241 = and(sK122(sK241,sK243,sK242),sK123(sK241,sK243,sK242))
| spl249_184 ),
inference(resolution,[],[f8213,f918]) ).
fof(f16823,plain,
( $false
| ~ spl249_4
| spl249_184 ),
inference(forward_subsumption_resolution,[],[f16820,f15612]) ).
fof(f16824,plain,
( ~ spl249_4
| spl249_184 ),
inference(avatar_contradiction_clause,[],[f16823]) ).
fof(f16833,plain,
( sK241 = or(sK130(sK241,sK243,sK242),sK131(sK241,sK243,sK242))
| spl249_187 ),
inference(resolution,[],[f8222,f944]) ).
fof(f16836,plain,
( sK241 = or(sK130(sK241,'0',sK242),sK131(sK241,'0',sK242))
| spl249_187 ),
inference(forward_demodulation,[],[f16833,f8879]) ).
fof(f16860,plain,
( ! [X0,X1] : and(X0,X1) != sK241
| spl249_187 ),
inference(superposition,[],[f676,f16836]) ).
fof(f16899,plain,
( sK241 != sK241
| sK238(sK241) = sK131(sK241,'0',sK242)
| ~ spl249_4
| spl249_187 ),
inference(superposition,[],[f15614,f16836]) ).
fof(f16900,plain,
( sK241 != sK241
| sK237(sK241) = sK130(sK241,'0',sK242)
| ~ spl249_4
| spl249_187 ),
inference(superposition,[],[f15616,f16836]) ).
fof(f16901,plain,
( sK237(sK241) = sK130(sK241,'0',sK242)
| ~ spl249_4
| spl249_187 ),
inference(trivial_inequality_removal,[],[f16900]) ).
fof(f16902,plain,
( sK238(sK241) = sK131(sK241,'0',sK242)
| ~ spl249_4
| spl249_187 ),
inference(trivial_inequality_removal,[],[f16899]) ).
fof(f16977,plain,
( ~ eval_terminates(sK237(sK241),sK242,'0')
| ~ spl249_4
| spl249_187
| spl249_233 ),
inference(superposition,[],[f8888,f16901]) ).
fof(f18100,plain,
( ~ list_succeeds(sK242)
| ~ sP64(sK241)
| ~ spl249_4
| spl249_187
| spl249_233 ),
inference(resolution,[],[f16977,f1263]) ).
fof(f18127,plain,
( ~ sP64(sK241)
| ~ spl249_4
| spl249_187
| spl249_233 ),
inference(forward_subsumption_resolution,[],[f18100,f1451]) ).
fof(f18132,plain,
( $false
| ~ spl249_4
| spl249_187
| spl249_233 ),
inference(forward_subsumption_resolution,[],[f18127,f1466]) ).
fof(f18133,plain,
( ~ spl249_4
| spl249_187
| spl249_233 ),
inference(avatar_contradiction_clause,[],[f18132]) ).
fof(f18135,plain,
( ~ eval_terminates(sK238(sK241),sK242,'0')
| ~ spl249_4
| spl249_187
| spl249_235 ),
inference(forward_demodulation,[],[f8895,f16902]) ).
fof(f19454,plain,
( ~ list_succeeds(sK242)
| ~ sP64(sK241)
| ~ spl249_4
| spl249_187
| spl249_235 ),
inference(resolution,[],[f18135,f1261]) ).
fof(f19481,plain,
( ~ sP64(sK241)
| ~ spl249_4
| spl249_187
| spl249_235 ),
inference(forward_subsumption_resolution,[],[f19454,f1451]) ).
fof(f19486,plain,
( $false
| ~ spl249_4
| spl249_187
| spl249_235 ),
inference(forward_subsumption_resolution,[],[f19481,f1466]) ).
fof(f19487,plain,
( ~ spl249_4
| spl249_187
| spl249_235 ),
inference(avatar_contradiction_clause,[],[f19486]) ).
fof(f19761,plain,
( sK241 = and(sK239(sK241),sK240(sK241))
| ~ spl249_3 ),
inference(resolution,[],[f1463,f1270]) ).
fof(f19762,plain,
( $false
| ~ spl249_3
| ~ spl249_259 ),
inference(forward_subsumption_resolution,[],[f19761,f13813]) ).
fof(f19763,plain,
( ~ spl249_3
| ~ spl249_259 ),
inference(avatar_contradiction_clause,[],[f19762]) ).
fof(f19766,plain,
( $false
| ~ spl249_3
| spl249_187 ),
inference(forward_subsumption_resolution,[],[f19761,f16860]) ).
fof(f19767,plain,
( ~ spl249_3
| spl249_187 ),
inference(avatar_contradiction_clause,[],[f19766]) ).
fof(f19788,plain,
( ! [X0] : neg(X0) != sK241
| ~ spl249_3 ),
inference(superposition,[],[f672,f19761]) ).
fof(f19790,plain,
( ! [X0,X1] :
( and(X0,X1) != sK241
| sK240(sK241) = X1 )
| ~ spl249_3 ),
inference(superposition,[],[f674,f19761]) ).
fof(f19792,plain,
( ! [X0,X1] :
( and(X0,X1) != sK241
| sK239(sK241) = X0 )
| ~ spl249_3 ),
inference(superposition,[],[f675,f19761]) ).
fof(f19793,plain,
( ! [X0,X1] : or(X0,X1) != sK241
| ~ spl249_3 ),
inference(superposition,[],[f676,f19761]) ).
fof(f21446,plain,
( sK241 = neg(sK127(sK241,'1',sK242))
| spl249_265 ),
inference(resolution,[],[f10489,f930]) ).
fof(f21466,plain,
( $false
| ~ spl249_3
| spl249_265 ),
inference(forward_subsumption_resolution,[],[f21446,f19788]) ).
fof(f21467,plain,
( ~ spl249_3
| spl249_265 ),
inference(avatar_contradiction_clause,[],[f21466]) ).
fof(f21481,plain,
( sK241 = and(sK132(sK241,'1',sK242),sK133(sK241,'1',sK242))
| spl249_263 ),
inference(resolution,[],[f10483,f950]) ).
fof(f21571,plain,
( sK241 != sK241
| sK240(sK241) = sK133(sK241,'1',sK242)
| ~ spl249_3
| spl249_263 ),
inference(superposition,[],[f19790,f21481]) ).
fof(f21572,plain,
( sK241 != sK241
| sK239(sK241) = sK132(sK241,'1',sK242)
| ~ spl249_3
| spl249_263 ),
inference(superposition,[],[f19792,f21481]) ).
fof(f21573,plain,
( sK239(sK241) = sK132(sK241,'1',sK242)
| ~ spl249_3
| spl249_263 ),
inference(trivial_inequality_removal,[],[f21572]) ).
fof(f21574,plain,
( sK240(sK241) = sK133(sK241,'1',sK242)
| ~ spl249_3
| spl249_263 ),
inference(trivial_inequality_removal,[],[f21571]) ).
fof(f21673,plain,
( ~ eval_terminates(sK239(sK241),sK242,'1')
| ~ spl249_3
| spl249_263
| spl249_338 ),
inference(superposition,[],[f13522,f21573]) ).
fof(f21698,plain,
( ~ list_succeeds(sK242)
| ~ sP63(sK241)
| ~ spl249_3
| spl249_263
| spl249_338 ),
inference(resolution,[],[f21673,f1268]) ).
fof(f21728,plain,
( ~ sP63(sK241)
| ~ spl249_3
| spl249_263
| spl249_338 ),
inference(forward_subsumption_resolution,[],[f21698,f1451]) ).
fof(f21736,plain,
( $false
| ~ spl249_3
| spl249_263
| spl249_338 ),
inference(forward_subsumption_resolution,[],[f21728,f1463]) ).
fof(f21737,plain,
( ~ spl249_3
| spl249_263
| spl249_338 ),
inference(avatar_contradiction_clause,[],[f21736]) ).
fof(f21745,plain,
( ~ eval_terminates(sK240(sK241),sK242,'1')
| ~ spl249_3
| spl249_263
| spl249_339 ),
inference(forward_demodulation,[],[f13526,f21574]) ).
fof(f29117,plain,
( ~ list_succeeds(sK242)
| ~ sP63(sK241)
| ~ spl249_3
| spl249_263
| spl249_339 ),
inference(resolution,[],[f21745,f1266]) ).
fof(f29158,plain,
( ~ sP63(sK241)
| ~ spl249_3
| spl249_263
| spl249_339 ),
inference(forward_subsumption_resolution,[],[f29117,f1451]) ).
fof(f29166,plain,
( $false
| ~ spl249_3
| spl249_263
| spl249_339 ),
inference(forward_subsumption_resolution,[],[f29158,f1463]) ).
fof(f29167,plain,
( ~ spl249_3
| spl249_263
| spl249_339 ),
inference(avatar_contradiction_clause,[],[f29166]) ).
fof(f29177,plain,
( sK241 = or(sK120(sK241,'1',sK242),sK121(sK241,'1',sK242))
| spl249_260 ),
inference(resolution,[],[f10474,f914]) ).
fof(f29197,plain,
( $false
| ~ spl249_3
| spl249_260 ),
inference(forward_subsumption_resolution,[],[f29177,f19793]) ).
fof(f29198,plain,
( ~ spl249_3
| spl249_260 ),
inference(avatar_contradiction_clause,[],[f29197]) ).
fof(f29252,plain,
( sK241 = and(sK124(sK241,sK243,sK242),sK125(sK241,sK243,sK242))
| spl249_183 ),
inference(resolution,[],[f8210,f922]) ).
fof(f29255,plain,
( sK241 = and(sK124(sK241,'0',sK242),sK125(sK241,'0',sK242))
| spl249_183 ),
inference(forward_demodulation,[],[f29252,f9265]) ).
fof(f29319,plain,
( sK241 != sK241
| sK239(sK241) = sK124(sK241,'0',sK242)
| ~ spl249_3
| spl249_183 ),
inference(superposition,[],[f19792,f29255]) ).
fof(f29325,plain,
( sK239(sK241) = sK124(sK241,'0',sK242)
| ~ spl249_3
| spl249_183 ),
inference(trivial_inequality_removal,[],[f29319]) ).
fof(f29400,plain,
( ~ eval_terminates(sK239(sK241),sK242,'0')
| sP35(sK241,'0',sK242)
| ~ spl249_3
| spl249_183 ),
inference(superposition,[],[f920,f29325]) ).
fof(f29403,plain,
( ~ eval_terminates(sK239(sK241),sK242,'0')
| ~ spl249_3
| spl249_183 ),
inference(forward_subsumption_resolution,[],[f29400,f14233]) ).
fof(f29472,plain,
( ~ list_succeeds(sK242)
| ~ sP63(sK241)
| ~ spl249_3
| spl249_183 ),
inference(resolution,[],[f29403,f1268]) ).
fof(f29510,plain,
( ~ sP63(sK241)
| ~ spl249_3
| spl249_183 ),
inference(forward_subsumption_resolution,[],[f29472,f1451]) ).
fof(f29515,plain,
( $false
| ~ spl249_3
| spl249_183 ),
inference(forward_subsumption_resolution,[],[f29510,f1463]) ).
fof(f29516,plain,
( ~ spl249_3
| spl249_183 ),
inference(avatar_contradiction_clause,[],[f29515]) ).
fof(f29552,plain,
( sK241 = and(sK122(sK241,sK243,sK242),sK123(sK241,sK243,sK242))
| spl249_184 ),
inference(resolution,[],[f8213,f918]) ).
fof(f29555,plain,
( sK241 = and(sK122(sK241,'0',sK242),sK123(sK241,'0',sK242))
| spl249_184 ),
inference(forward_demodulation,[],[f29552,f9141]) ).
fof(f29618,plain,
( sK241 != sK241
| sK240(sK241) = sK123(sK241,'0',sK242)
| ~ spl249_3
| spl249_184 ),
inference(superposition,[],[f19790,f29555]) ).
fof(f29626,plain,
( sK240(sK241) = sK123(sK241,'0',sK242)
| ~ spl249_3
| spl249_184 ),
inference(trivial_inequality_removal,[],[f29618]) ).
fof(f29680,plain,
( ~ eval_terminates(sK240(sK241),sK242,'0')
| sP36(sK241,'0',sK242)
| ~ spl249_3
| spl249_184 ),
inference(superposition,[],[f916,f29626]) ).
fof(f29683,plain,
( ~ eval_terminates(sK240(sK241),sK242,'0')
| ~ spl249_3
| spl249_184 ),
inference(forward_subsumption_resolution,[],[f29680,f10255]) ).
fof(f29772,plain,
( ~ list_succeeds(sK242)
| ~ sP63(sK241)
| ~ spl249_3
| spl249_184 ),
inference(resolution,[],[f29683,f1266]) ).
fof(f29810,plain,
( ~ sP63(sK241)
| ~ spl249_3
| spl249_184 ),
inference(forward_subsumption_resolution,[],[f29772,f1451]) ).
fof(f29815,plain,
( $false
| ~ spl249_3
| spl249_184 ),
inference(forward_subsumption_resolution,[],[f29810,f1463]) ).
fof(f29816,plain,
( ~ spl249_3
| spl249_184 ),
inference(avatar_contradiction_clause,[],[f29815]) ).
cnf(s1,plain,
( spl249_1
| spl249_2
| spl249_3
| spl249_4 ),
inference(sat_conversion,[],[f1467]) ).
cnf(s148,plain,
( ~ spl249_180
| ~ spl249_181
| ~ spl249_182
| ~ spl249_183
| ~ spl249_184
| ~ spl249_185
| ~ spl249_186
| ~ spl249_187 ),
inference(sat_conversion,[],[f8223]) ).
cnf(s149,plain,
( ~ spl249_1
| ~ spl249_180
| ~ spl249_181
| ~ spl249_182
| ~ spl249_183
| ~ spl249_184
| ~ spl249_185
| ~ spl249_187 ),
inference(sat_conversion,[],[f8224]) ).
cnf(s150,plain,
( spl249_75
| ~ spl249_181
| ~ spl249_183
| ~ spl249_184
| ~ spl249_187 ),
inference(sat_conversion,[],[f8227]) ).
cnf(s151,plain,
( ~ spl249_1
| spl249_181 ),
inference(sat_conversion,[],[f8233]) ).
cnf(s152,plain,
( spl249_1
| spl249_3
| spl249_4
| spl249_31
| spl249_188 ),
inference(sat_conversion,[],[f8238]) ).
cnf(s190,plain,
~ spl249_31,
inference(sat_conversion,[],[f8737]) ).
cnf(s210,plain,
( spl249_187
| ~ spl249_233
| ~ spl249_235 ),
inference(sat_conversion,[],[f8896]) ).
cnf(s212,plain,
( ~ spl249_1
| spl249_187 ),
inference(sat_conversion,[],[f9137]) ).
cnf(s228,plain,
( ~ spl249_2
| spl249_181
| ~ spl249_188 ),
inference(sat_conversion,[],[f9994]) ).
cnf(s230,plain,
( ~ spl249_3
| spl249_181 ),
inference(sat_conversion,[],[f10002]) ).
cnf(s231,plain,
( ~ spl249_4
| spl249_181 ),
inference(sat_conversion,[],[f10009]) ).
cnf(s234,plain,
( ~ spl249_2
| spl249_3
| spl249_4
| spl249_31
| spl249_187 ),
inference(sat_conversion,[],[f10246]) ).
cnf(s237,plain,
( ~ spl249_2
| spl249_3
| spl249_4
| spl249_31
| spl249_184 ),
inference(sat_conversion,[],[f10454]) ).
cnf(s238,plain,
( ~ spl249_75
| ~ spl249_258
| spl249_259
| ~ spl249_260
| ~ spl249_261
| ~ spl249_262
| ~ spl249_263
| ~ spl249_264
| ~ spl249_265 ),
inference(sat_conversion,[],[f10490]) ).
cnf(s254,plain,
spl249_258,
inference(sat_conversion,[],[f11023]) ).
cnf(s291,plain,
( ~ spl249_2
| spl249_3
| spl249_4
| spl249_31
| spl249_260 ),
inference(sat_conversion,[],[f13264]) ).
cnf(s292,plain,
( ~ spl249_2
| ~ spl249_188
| spl249_265 ),
inference(sat_conversion,[],[f13418]) ).
cnf(s293,plain,
spl249_261,
inference(sat_conversion,[],[f13451]) ).
cnf(s294,plain,
spl249_262,
inference(sat_conversion,[],[f13484]) ).
cnf(s296,plain,
( spl249_263
| ~ spl249_338
| ~ spl249_339 ),
inference(sat_conversion,[],[f13527]) ).
cnf(s303,plain,
( ~ spl249_2
| spl249_3
| spl249_4
| spl249_31
| spl249_263 ),
inference(sat_conversion,[],[f13758]) ).
cnf(s304,plain,
spl249_264,
inference(sat_conversion,[],[f13782]) ).
cnf(s310,plain,
( ~ spl249_2
| spl249_3
| spl249_4
| spl249_31
| ~ spl249_259 ),
inference(sat_conversion,[],[f14211]) ).
cnf(s313,plain,
( ~ spl249_2
| spl249_3
| spl249_4
| spl249_31
| spl249_183 ),
inference(sat_conversion,[],[f14489]) ).
cnf(s321,plain,
( ~ spl249_1
| spl249_184 ),
inference(sat_conversion,[],[f14807]) ).
cnf(s323,plain,
( ~ spl249_1
| spl249_183 ),
inference(sat_conversion,[],[f15021]) ).
cnf(s325,plain,
( ~ spl249_75
| spl249_185
| ~ spl249_260 ),
inference(sat_conversion,[],[f15027]) ).
cnf(s326,plain,
( ~ spl249_1
| spl249_265 ),
inference(sat_conversion,[],[f15206]) ).
cnf(s328,plain,
( ~ spl249_75
| spl249_180
| ~ spl249_265 ),
inference(sat_conversion,[],[f15209]) ).
cnf(s329,plain,
( ~ spl249_1
| spl249_263 ),
inference(sat_conversion,[],[f15431]) ).
cnf(s331,plain,
( ~ spl249_75
| spl249_182
| ~ spl249_263 ),
inference(sat_conversion,[],[f15434]) ).
cnf(s332,plain,
( ~ spl249_1
| spl249_260 ),
inference(sat_conversion,[],[f15598]) ).
cnf(s342,plain,
( ~ spl249_4
| ~ spl249_75
| spl249_186
| ~ spl249_259 ),
inference(sat_conversion,[],[f16229]) ).
cnf(s345,plain,
( ~ spl249_4
| spl249_260 ),
inference(sat_conversion,[],[f16533]) ).
cnf(s346,plain,
( ~ spl249_4
| spl249_265 ),
inference(sat_conversion,[],[f16745]) ).
cnf(s347,plain,
( ~ spl249_4
| spl249_263 ),
inference(sat_conversion,[],[f16779]) ).
cnf(s351,plain,
( ~ spl249_4
| spl249_183 ),
inference(sat_conversion,[],[f16812]) ).
cnf(s352,plain,
( ~ spl249_4
| spl249_184 ),
inference(sat_conversion,[],[f16824]) ).
cnf(s363,plain,
( ~ spl249_4
| spl249_187
| spl249_233 ),
inference(sat_conversion,[],[f18133]) ).
cnf(s402,plain,
( ~ spl249_4
| spl249_187
| spl249_235 ),
inference(sat_conversion,[],[f19487]) ).
cnf(s405,plain,
( ~ spl249_3
| ~ spl249_259 ),
inference(sat_conversion,[],[f19763]) ).
cnf(s407,plain,
( ~ spl249_3
| spl249_187 ),
inference(sat_conversion,[],[f19767]) ).
cnf(s439,plain,
( ~ spl249_3
| spl249_265 ),
inference(sat_conversion,[],[f21467]) ).
cnf(s443,plain,
( ~ spl249_3
| spl249_263
| spl249_338 ),
inference(sat_conversion,[],[f21737]) ).
cnf(s613,plain,
( ~ spl249_3
| spl249_263
| spl249_339 ),
inference(sat_conversion,[],[f29167]) ).
cnf(s616,plain,
( ~ spl249_3
| spl249_260 ),
inference(sat_conversion,[],[f29198]) ).
cnf(s619,plain,
( ~ spl249_3
| spl249_183 ),
inference(sat_conversion,[],[f29516]) ).
cnf(s622,plain,
( ~ spl249_3
| spl249_184 ),
inference(sat_conversion,[],[f29816]) ).
cnf(s631,plain,
( ~ spl249_75
| spl249_259
| ~ spl249_260
| ~ spl249_263
| ~ spl249_265 ),
inference(rat,[],[s238,s304,s294,s293,s254]) ).
cnf(s637,plain,
( spl249_1
| spl249_3
| spl249_4
| spl249_188 ),
inference(rat,[],[s152,s190]) ).
cnf(s643,plain,
( spl249_187
| ~ spl249_4 ),
inference(rat,[],[s210,s363,s402]) ).
cnf(s644,plain,
~ spl249_4,
inference(rat,[],[s148,s342,s631,s325,s328,s331,s150,s643,s231,s345,s346,s347,s351,s352]) ).
cnf(s645,plain,
( spl249_263
| ~ spl249_3 ),
inference(rat,[],[s296,s443,s613]) ).
cnf(s646,plain,
~ spl249_3,
inference(rat,[],[s645,s631,s150,s230,s405,s407,s439,s616,s619,s622]) ).
cnf(s648,plain,
spl249_1,
inference(rat,[],[s150,s631,s292,s228,s234,s237,s291,s303,s310,s313,s637,s1,s646,s190,s644]) ).
cnf(s649,plain,
spl249_260,
inference(rat,[],[s332,s648]) ).
cnf(s650,plain,
spl249_263,
inference(rat,[],[s329,s648]) ).
cnf(s651,plain,
spl249_265,
inference(rat,[],[s326,s648]) ).
cnf(s652,plain,
spl249_183,
inference(rat,[],[s323,s648]) ).
cnf(s653,plain,
spl249_184,
inference(rat,[],[s321,s648]) ).
cnf(s654,plain,
spl249_187,
inference(rat,[],[s212,s648]) ).
cnf(s657,plain,
spl249_181,
inference(rat,[],[s151,s648]) ).
cnf(s659,plain,
spl249_75,
inference(rat,[],[s150,s657,s653,s652,s654]) ).
cnf(s660,plain,
spl249_180,
inference(rat,[],[s328,s651,s659]) ).
cnf(s661,plain,
spl249_185,
inference(rat,[],[s325,s649,s659]) ).
cnf(s664,plain,
spl249_182,
inference(rat,[],[s331,s650,s659]) ).
cnf(s665,plain,
$false,
inference(rat,[],[s149,s654,s661,s653,s652,s648,s657,s664,s660]) ).
fof(f29817,plain,
$false,
inference(avatar_sat_refutation,[],[s665]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWX067+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.26 % Computer : n002.cluster.edu
% 0.09/0.26 % Model : x86_64 x86_64
% 0.09/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.26 % Memory : 8046.5625MB
% 0.09/0.26 % OS : Linux 6.8.0-71-generic
% 0.09/0.26 % CPULimit : 300
% 0.09/0.26 % WCLimit : 300
% 0.09/0.26 % DateTime : Mon Sep 28 15:00:37 UTC 2026
% 0.09/0.26 % CPUTime :
% 0.09/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.26/0.32 Running first-order theorem proving
% 0.26/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.81/4.01 % (415988)Detected formulas, will run a generic FOF schedule.
% 20.81/4.01 % (416001)dis-21_1_sil=8000:lcm=predicate:random_seed=3520993851: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)
% 20.81/4.01 % (415999)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1794277833:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 20.81/4.01 % (416001)Instruction limit reached!
% 20.81/4.01 % (416001)------------------------------
% 20.81/4.01 % (416001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.81/4.01 % (416001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.81/4.01 % (416001)CaDiCaL version: 2.1.3
% 20.81/4.01 % (416001)Termination reason: Instruction limit
% 20.81/4.01 % (416001)Termination phase: Saturation
% 20.81/4.01 % (416001)Time elapsed: 0.049 s
% 20.81/4.01 % (416001)Peak memory usage: 90 MB
% 20.81/4.01 % (416001)Instructions burned: 129 (million)
% 20.81/4.01 % (415998)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3401182919:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 20.81/4.01 % (415995)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=33589989:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 20.81/4.01 % (415996)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=1637195075:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 20.81/4.01 % (415997)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=2727912410:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 20.81/4.01 % (415998)Refutation not found, incomplete strategy
% 20.81/4.01 % (415998)------------------------------
% 20.81/4.01 % (415998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.81/4.01 % (415998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.81/4.01 % (415998)CaDiCaL version: 2.1.3
% 20.81/4.01 % (415998)Termination reason: Refutation not found, incomplete strategy
% 20.81/4.01 % (415998)Time elapsed: 0.013 s
% 20.81/4.01 % (415998)Peak memory usage: 89 MB
% 20.81/4.01 % (415998)Instructions burned: 12 (million)
% 20.81/4.01 % (416000)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2460735737:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 20.81/4.01 % (415999)Instruction limit reached!
% 20.81/4.01 % (415999)------------------------------
% 20.81/4.01 % (415999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.81/4.01 % (415999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.81/4.01 % (415999)CaDiCaL version: 2.1.3
% 20.81/4.01 % (415999)Termination reason: Instruction limit
% 20.81/4.01 % (415999)Termination phase: Saturation
% 20.81/4.01 % (415999)Time elapsed: 0.116 s
% 20.81/4.01 % (415999)Peak memory usage: 89 MB
% 20.81/4.01 % (415999)Instructions burned: 119 (million)
% 20.81/4.01 % (416000)Instruction limit reached!
% 20.81/4.01 % (416000)------------------------------
% 20.81/4.01 % (416000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.81/4.01 % (416000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.81/4.01 % (416000)CaDiCaL version: 2.1.3
% 20.81/4.01 % (416000)Termination reason: Instruction limit
% 20.81/4.01 % (416000)Termination phase: Saturation
% 20.81/4.01 % (416000)Time elapsed: 0.154 s
% 20.81/4.01 % (416000)Peak memory usage: 91 MB
% 20.81/4.01 % (416000)Instructions burned: 139 (million)
% 20.81/4.01 % (416004)lrs+10_1_sil=8000:sp=occurrence:random_seed=676881527:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 20.81/4.01 % (416010)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3699369120:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 20.81/4.01 % (416004)Instruction limit reached!
% 20.81/4.01 % (416004)------------------------------
% 20.81/4.01 % (416004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.81/4.01 % (416004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.81/4.01 % (416004)CaDiCaL version: 2.1.3
% 20.81/4.01 % (416004)Termination reason: Instruction limit
% 20.81/4.01 % (416004)Termination phase: Saturation
% 20.81/4.01 % (416004)Time elapsed: 0.157 s
% 32.91/5.64 % (416004)Peak memory usage: 93 MB
% 32.91/5.64 % (416004)Instructions burned: 287 (million)
% 32.91/5.64 % (415998)------------------------------
% 32.91/5.64 % (415998)------------------------------
% 32.91/5.64 % (416010)Instruction limit reached!
% 32.91/5.64 % (416010)------------------------------
% 32.91/5.64 % (416010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.91/5.64 % (416010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.91/5.64 % (416010)CaDiCaL version: 2.1.3
% 32.91/5.64 % (416010)Termination reason: Instruction limit
% 32.91/5.64 % (416010)Termination phase: Saturation
% 32.91/5.64 % (416010)Time elapsed: 0.144 s
% 32.91/5.64 % (416010)Peak memory usage: 92 MB
% 32.91/5.64 % (416010)Instructions burned: 158 (million)
% 32.91/5.64 % (416012)lrs+1011_1_sil=32000:sp=occurrence:random_seed=484600000:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 32.91/5.64 % (416014)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=1691750324:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 32.91/5.64 % (416015)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=48061349:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 32.91/5.64 % (416014)Instruction limit reached!
% 32.91/5.64 % (416014)------------------------------
% 32.91/5.64 % (416014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.91/5.64 % (416014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.91/5.64 % (416014)CaDiCaL version: 2.1.3
% 32.91/5.64 % (416014)Termination reason: Instruction limit
% 32.91/5.64 % (416014)Termination phase: Saturation
% 32.91/5.64 % (416014)Time elapsed: 0.120 s
% 32.91/5.64 % (416014)Peak memory usage: 93 MB
% 32.91/5.64 % (416014)Instructions burned: 249 (million)
% 32.91/5.64 % (416015)Refutation not found, incomplete strategy
% 32.91/5.64 % (416015)------------------------------
% 32.91/5.64 % (416015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.91/5.64 % (416015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.91/5.64 % (416015)CaDiCaL version: 2.1.3
% 32.91/5.64 % (416015)Termination reason: Refutation not found, incomplete strategy
% 32.91/5.64 % (416015)Time elapsed: 0.025 s
% 32.91/5.64 % (416015)Peak memory usage: 89 MB
% 32.91/5.64 % (416015)Instructions burned: 25 (million)
% 32.91/5.64 % (416017)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2231687576:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 32.91/5.64 % (416012)Instruction limit reached!
% 32.91/5.64 % (416012)------------------------------
% 32.91/5.64 % (416012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.91/5.64 % (416012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.91/5.64 % (416012)CaDiCaL version: 2.1.3
% 32.91/5.64 % (416012)Termination reason: Instruction limit
% 32.91/5.64 % (416012)Termination phase: Saturation
% 32.91/5.64 % (416012)Time elapsed: 0.338 s
% 32.91/5.64 % (416012)Peak memory usage: 92 MB
% 32.91/5.64 % (416012)Instructions burned: 325 (million)
% 32.91/5.64 % (416020)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1503711391:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 32.91/5.64 % (416020)Instruction limit reached!
% 32.91/5.64 % (416020)------------------------------
% 32.91/5.64 % (416020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.91/5.64 % (416020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.91/5.64 % (416020)CaDiCaL version: 2.1.3
% 32.91/5.64 % (416020)Termination reason: Instruction limit
% 32.91/5.64 % (416020)Termination phase: Saturation
% 32.91/5.64 % (416020)Time elapsed: 0.117 s
% 32.91/5.64 % (416020)Peak memory usage: 91 MB
% 32.91/5.64 % (416020)Instructions burned: 113 (million)
% 32.91/5.64 % (416022)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3098902101:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 32.91/5.64 % (416015)------------------------------
% 32.91/5.64 % (416015)------------------------------
% 32.91/5.64 % (416022)Instruction limit reached!
% 32.91/5.64 % (416022)------------------------------
% 32.91/5.64 % (416022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.91/5.64 % (416022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.91/5.64 % (416022)CaDiCaL version: 2.1.3
% 32.91/5.64 % (416022)Termination reason: Instruction limit
% 74.26/11.40 % (416022)Termination phase: Saturation
% 74.26/11.40 % (416022)Time elapsed: 0.056 s
% 74.26/11.40 % (416022)Peak memory usage: 89 MB
% 74.26/11.40 % (416022)Instructions burned: 128 (million)
% 74.26/11.40 % (416024)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2023809052:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 74.26/11.40 % (416026)lrs+10_1_sil=8000:sp=occurrence:random_seed=1613481706:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 74.26/11.40 % (416024)Instruction limit reached!
% 74.26/11.40 % (416024)------------------------------
% 74.26/11.40 % (416024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.26/11.40 % (416024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.26/11.40 % (416024)CaDiCaL version: 2.1.3
% 74.26/11.40 % (416024)Termination reason: Instruction limit
% 74.26/11.40 % (416024)Termination phase: Property scanning
% 74.26/11.40 % (416024)Time elapsed: 0.116 s
% 74.26/11.40 % (416024)Peak memory usage: 108 MB
% 74.26/11.40 % (416024)Instructions burned: 114 (million)
% 74.26/11.40 % (416027)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3569779031:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 74.26/11.40 % (416027)Refutation not found, incomplete strategy
% 74.26/11.40 % (416027)------------------------------
% 74.26/11.40 % (416027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.26/11.40 % (416027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.26/11.40 % (416027)CaDiCaL version: 2.1.3
% 74.26/11.40 % (416027)Termination reason: Refutation not found, incomplete strategy
% 74.26/11.40 % (416027)Time elapsed: 0.035 s
% 74.26/11.40 % (416027)Peak memory usage: 90 MB
% 74.26/11.40 % (416027)Instructions burned: 37 (million)
% 74.26/11.40 % (416031)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2335296712:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 74.26/11.40 % (416026)Instruction limit reached!
% 74.26/11.40 % (416026)------------------------------
% 74.26/11.40 % (416026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.26/11.40 % (416026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.26/11.40 % (416026)CaDiCaL version: 2.1.3
% 74.26/11.40 % (416026)Termination reason: Instruction limit
% 74.26/11.40 % (416026)Termination phase: Saturation
% 74.26/11.40 % (416026)Time elapsed: 0.468 s
% 74.26/11.40 % (416026)Peak memory usage: 101 MB
% 74.26/11.40 % (416026)Instructions burned: 909 (million)
% 74.26/11.40 % (416027)------------------------------
% 74.26/11.40 % (416027)------------------------------
% 74.26/11.40 % (416033)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3376065715:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2979 on theBenchmark for (2979ds/134Mi)
% 74.26/11.40 % (416033)Instruction limit reached!
% 74.26/11.40 % (416033)------------------------------
% 74.26/11.40 % (416033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.26/11.40 % (416033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.26/11.40 % (416033)CaDiCaL version: 2.1.3
% 74.26/11.40 % (416033)Termination reason: Instruction limit
% 74.26/11.40 % (416033)Termination phase: Saturation
% 74.26/11.40 % (416033)Time elapsed: 0.045 s
% 74.26/11.40 % (416033)Peak memory usage: 91 MB
% 74.26/11.40 % (416033)Instructions burned: 135 (million)
% 74.26/11.40 % (416034)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1096164498:st=8:i=592:sd=3:ep=RST:ss=axioms_2979 on theBenchmark for (2979ds/592Mi)
% 74.26/11.40 % (416034)Refutation not found, incomplete strategy
% 74.26/11.40 % (416034)------------------------------
% 74.26/11.40 % (416034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.26/11.40 % (416034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.26/11.40 % (416034)CaDiCaL version: 2.1.3
% 74.26/11.40 % (416034)Termination reason: Refutation not found, incomplete strategy
% 74.26/11.40 % (416034)Time elapsed: 0.032 s
% 74.26/11.40 % (416034)Peak memory usage: 89 MB
% 74.26/11.40 % (416034)Instructions burned: 36 (million)
% 74.26/11.40 % (416036)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2986770724:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 74.26/11.40 % (416034)------------------------------
% 74.26/11.40 % (416034)------------------------------
% 74.26/11.40 % (416039)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=1108463599:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/125Mi)
% 116.22/17.27 % (416039)Instruction limit reached!
% 116.22/17.27 % (416039)------------------------------
% 116.22/17.27 % (416039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.22/17.27 % (416039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.22/17.27 % (416039)CaDiCaL version: 2.1.3
% 116.22/17.27 % (416039)Termination reason: Instruction limit
% 116.22/17.27 % (416039)Termination phase: Saturation
% 116.22/17.27 % (416039)Time elapsed: 0.123 s
% 116.22/17.27 % (416039)Peak memory usage: 92 MB
% 116.22/17.27 % (416039)Instructions burned: 125 (million)
% 116.22/17.27 % (416017)Instruction limit reached!
% 116.22/17.27 % (416017)------------------------------
% 116.22/17.27 % (416017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.22/17.27 % (416017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.22/17.27 % (416017)CaDiCaL version: 2.1.3
% 116.22/17.27 % (416017)Termination reason: Instruction limit
% 116.22/17.27 % (416017)Termination phase: Saturation
% 116.22/17.27 % (416017)Time elapsed: 2.523 s
% 116.22/17.27 % (416017)Peak memory usage: 143 MB
% 116.22/17.27 % (416017)Instructions burned: 2350 (million)
% 116.22/17.27 % (416041)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=467835224:i=134:gtgl=5:slsql=off:gtg=exists_sym_2967 on theBenchmark for (2967ds/134Mi)
% 116.22/17.27 % (416041)Instruction limit reached!
% 116.22/17.27 % (416041)------------------------------
% 116.22/17.27 % (416041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.22/17.27 % (416041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.22/17.27 % (416041)CaDiCaL version: 2.1.3
% 116.22/17.27 % (416041)Termination reason: Instruction limit
% 116.22/17.27 % (416041)Termination phase: Saturation
% 116.22/17.27 % (416041)Time elapsed: 0.143 s
% 116.22/17.27 % (416041)Peak memory usage: 91 MB
% 116.22/17.27 % (416041)Instructions burned: 134 (million)
% 116.22/17.27 % (416042)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3322713329:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/141Mi)
% 116.22/17.27 % (416042)Refutation not found, incomplete strategy
% 116.22/17.27 % (416042)------------------------------
% 116.22/17.27 % (416042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.22/17.27 % (416042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.22/17.27 % (416042)CaDiCaL version: 2.1.3
% 116.22/17.27 % (416042)Termination reason: Refutation not found, incomplete strategy
% 116.22/17.27 % (416042)Time elapsed: 0.012 s
% 116.22/17.27 % (416042)Peak memory usage: 89 MB
% 116.22/17.27 % (416042)Instructions burned: 18 (million)
% 116.22/17.27 % (416044)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2554860697:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2963 on theBenchmark for (2963ds/431Mi)
% 116.22/17.27 % (416042)------------------------------
% 116.22/17.27 % (416042)------------------------------
% 116.22/17.27 % (416044)Instruction limit reached!
% 116.22/17.27 % (416044)------------------------------
% 116.22/17.27 % (416044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.22/17.27 % (416044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.22/17.27 % (416044)CaDiCaL version: 2.1.3
% 116.22/17.27 % (416044)Termination reason: Instruction limit
% 116.22/17.27 % (416044)Termination phase: Saturation
% 116.22/17.27 % (416044)Time elapsed: 0.367 s
% 116.22/17.27 % (416044)Peak memory usage: 92 MB
% 116.22/17.27 % (416044)Instructions burned: 432 (million)
% 116.22/17.27 % (416049)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=3693385188:i=6060:aac=none:ins=25_2958 on theBenchmark for (2958ds/6060Mi)
% 116.22/17.27 % (416050)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=4163091208:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2956 on theBenchmark for (2956ds/150Mi)
% 116.22/17.27 % (416050)Instruction limit reached!
% 116.22/17.27 % (416050)------------------------------
% 116.22/17.27 % (416050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.22/17.27 % (416050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.22/17.27 % (416050)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416050)Termination reason: Instruction limit
% 69.53/19.35 % (416050)Termination phase: Saturation
% 69.53/19.35 % (416050)Time elapsed: 0.145 s
% 69.53/19.35 % (416050)Peak memory usage: 92 MB
% 69.53/19.35 % (416050)Instructions burned: 150 (million)
% 69.53/19.35 % (416053)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2398721533:i=14155:bd=all_2952 on theBenchmark for (2952ds/14155Mi)
% 69.53/19.35 % (416031)Instruction limit reached!
% 69.53/19.35 % (416031)------------------------------
% 69.53/19.35 % (416031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.53/19.35 % (416031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.53/19.35 % (416031)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416031)Termination reason: Instruction limit
% 69.53/19.35 % (416031)Termination phase: Saturation
% 69.53/19.35 % (416031)Time elapsed: 5.118 s
% 69.53/19.35 % (416031)Peak memory usage: 157 MB
% 69.53/19.35 % (416031)Instructions burned: 5203 (million)
% 69.53/19.35 % (416055)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2515206013:i=667:av=off:fsr=off_2929 on theBenchmark for (2929ds/667Mi)
% 69.53/19.35 % (416055)Instruction limit reached!
% 69.53/19.35 % (416055)------------------------------
% 69.53/19.35 % (416055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.53/19.35 % (416055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.53/19.35 % (416055)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416055)Termination reason: Instruction limit
% 69.53/19.35 % (416055)Termination phase: Saturation
% 69.53/19.35 % (416055)Time elapsed: 0.525 s
% 69.53/19.35 % (416055)Peak memory usage: 94 MB
% 69.53/19.35 % (416055)Instructions burned: 668 (million)
% 69.53/19.35 % (416057)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=1427849974:s2a=on:i=185:s2at=1.8:fdi=4_2921 on theBenchmark for (2921ds/185Mi)
% 69.53/19.35 % (416057)Instruction limit reached!
% 69.53/19.35 % (416057)------------------------------
% 69.53/19.35 % (416057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.53/19.35 % (416057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.53/19.35 % (416057)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416057)Termination reason: Instruction limit
% 69.53/19.35 % (416057)Termination phase: Saturation
% 69.53/19.35 % (416057)Time elapsed: 0.157 s
% 69.53/19.35 % (416057)Peak memory usage: 92 MB
% 69.53/19.35 % (416057)Instructions burned: 185 (million)
% 69.53/19.35 % (416059)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2881030990:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2916 on theBenchmark for (2916ds/193Mi)
% 69.53/19.35 % (416059)Instruction limit reached!
% 69.53/19.35 % (416059)------------------------------
% 69.53/19.35 % (416059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.53/19.35 % (416059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.53/19.35 % (416059)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416059)Termination reason: Instruction limit
% 69.53/19.35 % (416059)Termination phase: Saturation
% 69.53/19.35 % (416059)Time elapsed: 0.205 s
% 69.53/19.35 % (416059)Peak memory usage: 93 MB
% 69.53/19.35 % (416059)Instructions burned: 194 (million)
% 69.53/19.35 % (416036)Instruction limit reached!
% 69.53/19.35 % (416036)------------------------------
% 69.53/19.35 % (416036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.53/19.35 % (416036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.53/19.35 % (416036)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416036)Termination reason: Instruction limit
% 69.53/19.35 % (416036)Termination phase: Saturation
% 69.53/19.35 % (416036)Time elapsed: 6.587 s
% 69.53/19.35 % (416036)Peak memory usage: 229 MB
% 69.53/19.35 % (416036)Instructions burned: 13194 (million)
% 69.53/19.35 % (416061)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1821626646:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2911 on theBenchmark for (2911ds/4850Mi)
% 69.53/19.35 % (416062)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2327882844:i=12111:sd=1:ss=included_2909 on theBenchmark for (2909ds/12111Mi)
% 69.53/19.35 % (416049)Instruction limit reached!
% 69.53/19.35 % (416049)------------------------------
% 69.53/19.35 % (416049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.53/19.35 % (416049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.53/19.35 % (416049)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416049)Termination reason: Instruction limit
% 69.53/19.35 % (416049)Termination phase: Saturation
% 69.53/19.35 % (416049)Time elapsed: 6.014 s
% 69.53/19.35 % (416049)Peak memory usage: 154 MB
% 69.53/19.35 % (416049)Instructions burned: 6060 (million)
% 69.53/19.35 % (416065)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1155652031:i=319:kws=precedence:fsr=off_2895 on theBenchmark for (2895ds/319Mi)
% 69.53/19.35 % (416065)Instruction limit reached!
% 69.53/19.35 % (416065)------------------------------
% 69.53/19.35 % (416065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.53/19.35 % (416065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.53/19.35 % (416065)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416065)Termination reason: Instruction limit
% 69.53/19.35 % (416065)Termination phase: Saturation
% 69.53/19.35 % (416065)Time elapsed: 0.273 s
% 69.53/19.35 % (416065)Peak memory usage: 93 MB
% 69.53/19.35 % (416065)Instructions burned: 319 (million)
% 69.53/19.35 % (416067)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=615764298:i=2064:ep=RST_2889 on theBenchmark for (2889ds/2064Mi)
% 69.53/19.35 % (416067)Instruction limit reached!
% 69.53/19.35 % (416067)------------------------------
% 69.53/19.35 % (416067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.53/19.35 % (416067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.53/19.35 % (416067)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416067)Termination reason: Instruction limit
% 69.53/19.35 % (416067)Termination phase: Saturation
% 69.53/19.35 % (416067)Time elapsed: 1.473 s
% 69.53/19.35 % (416067)Peak memory usage: 96 MB
% 69.53/19.35 % (416067)Instructions burned: 2064 (million)
% 69.53/19.35 % (416069)dis-1011_128_sil=32000:random_seed=887060385:i=3706:ep=RST:av=off_2871 on theBenchmark for (2871ds/3706Mi)
% 69.53/19.35 % (416061)Instruction limit reached!
% 69.53/19.35 % (416061)------------------------------
% 69.53/19.35 % (416061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.53/19.35 % (416061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.53/19.35 % (416061)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416061)Termination reason: Instruction limit
% 69.53/19.35 % (416061)Termination phase: Saturation
% 69.53/19.35 % (416061)Time elapsed: 4.664 s
% 69.53/19.35 % (416061)Peak memory usage: 143 MB
% 69.53/19.35 % (416061)Instructions burned: 4850 (million)
% 69.53/19.35 % (416071)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3080000830:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2861 on theBenchmark for (2861ds/757Mi)
% 69.53/19.35 % (416071)Instruction limit reached!
% 69.53/19.35 % (416071)------------------------------
% 69.53/19.35 % (416071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.53/19.35 % (416071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.53/19.35 % (416071)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416071)Termination reason: Instruction limit
% 69.53/19.35 % (416071)Termination phase: Saturation
% 69.53/19.35 % (416071)Time elapsed: 0.650 s
% 69.53/19.35 % (416071)Peak memory usage: 120 MB
% 69.53/19.35 % (416071)Instructions burned: 758 (million)
% 69.53/19.35 % (416075)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3061250085:i=13913:ss=axioms:sgt=8_2852 on theBenchmark for (2852ds/13913Mi)
% 69.53/19.35 % (416062)Instruction limit reached!
% 69.53/19.35 % (416062)------------------------------
% 69.53/19.35 % (416062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.53/19.35 % (416062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.53/19.35 % (416062)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416062)Termination reason: Instruction limit
% 69.53/19.35 % (416062)Termination phase: Saturation
% 69.53/19.35 % (416062)Time elapsed: 5.817 s
% 69.53/19.35 % (416062)Peak memory usage: 199 MB
% 69.53/19.35 % (416062)Instructions burned: 12113 (million)
% 69.53/19.35 % (416077)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=238970030:i=9925:aac=none_2848 on theBenchmark for (2848ds/9925Mi)
% 69.53/19.35 % (416069)Instruction limit reached!
% 69.53/19.35 % (416069)------------------------------
% 69.53/19.35 % (416069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.53/19.35 % (416069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.53/19.35 % (416069)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416069)Termination reason: Instruction limit
% 69.53/19.35 % (416069)Termination phase: Saturation
% 69.53/19.35 % (416069)Time elapsed: 3.247 s
% 69.53/19.35 % (416069)Peak memory usage: 107 MB
% 69.53/19.35 % (416069)Instructions burned: 3706 (million)
% 69.53/19.35 % (416079)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1620986568:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2836 on theBenchmark for (2836ds/2479Mi)
% 69.53/19.35 % (416053)Instruction limit reached!
% 69.53/19.35 % (416053)------------------------------
% 69.53/19.35 % (416053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.53/19.35 % (416053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.53/19.35 % (416053)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416053)Termination reason: Instruction limit
% 69.53/19.35 % (416053)Termination phase: Saturation
% 69.53/19.35 % (416053)Time elapsed: 12.452 s
% 69.53/19.35 % (416053)Peak memory usage: 193 MB
% 69.53/19.35 % (416053)Instructions burned: 14155 (million)
% 69.53/19.35 % (416081)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3200867452:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2825 on theBenchmark for (2825ds/440Mi)
% 69.53/19.35 % (416077)First to succeed.
% 69.53/19.35 % (416077)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-415988"
% 69.53/19.35 % (416081)Instruction limit reached!
% 69.53/19.35 % (416081)------------------------------
% 69.53/19.35 % (416081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.53/19.35 % (416081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.53/19.35 % (416081)CaDiCaL version: 2.1.3
% 69.53/19.35 % (416081)Termination reason: Instruction limit
% 69.53/19.35 % (416081)Termination phase: Saturation
% 69.53/19.35 % (416081)Time elapsed: 0.428 s
% 69.53/19.35 % (416081)Peak memory usage: 94 MB
% 69.53/19.35 % (416081)Instructions burned: 441 (million)
% 69.53/19.35 % (416077)Refutation found. Thanks to Tanya!
% 69.53/19.35 % SZS status Theorem for theBenchmark
% 69.53/19.35 % SZS output start Proof for theBenchmark
% See solution above
% 131.50/19.58 % (416077)------------------------------
% 131.50/19.58 % (416077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.50/19.58 % (416077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.50/19.58 % (416077)CaDiCaL version: 2.1.3
% 131.50/19.58 % (416077)Termination reason: Refutation
% 131.50/19.58 % (416077)Time elapsed: 2.730 s
% 131.50/19.58 % (416077)Peak memory usage: 165 MB
% 131.50/19.58 % (416077)Instructions burned: 4951 (million)
% 131.50/19.58 % (416077)------------------------------
% 131.50/19.58 % (416077)------------------------------
% 131.50/19.58 % (415988)Success in time 18.421 s
% 131.50/19.58 % Vampire exiting
%------------------------------------------------------------------------------