%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX066+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 100.03s 31.67s
% Output : Refutation 221.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 79
% Syntax : Number of formulae : 745 ( 41 unt; 53 def)
% Number of atoms : 3448 ( 434 equ)
% Maximal formula atoms : 45 ( 4 avg)
% Number of connectives : 4445 (1742 ~;2208 |; 397 &)
% ( 61 <=>; 37 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 67 ( 64 usr; 47 prp; 0-3 aty)
% Number of functors : 35 ( 35 usr; 8 con; 0-3 aty)
% Number of variables : 823 ( 0 sgn 716 !; 107 ?)
% Comments :
%------------------------------------------------------------------------------
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(f42,axiom,
! [X0] :
( gr(X0)
<=> gr(neg(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id42) ).
fof(f43,axiom,
! [X0,X1] :
( ( gr(X0)
& gr(X1) )
<=> gr(and(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id43) ).
fof(f44,axiom,
! [X0,X1] :
( ( gr(X0)
& gr(X1) )
<=> gr(or(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id44) ).
fof(f50,axiom,
! [X0,X1,X2] :
( false_terminates(X0,X1,X2)
=> ( false_succeeds(X0,X1,X2)
| false_fails(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id50) ).
fof(f52,axiom,
! [X0,X1,X2] :
( true_terminates(X0,X1,X2)
=> ( true_succeeds(X0,X1,X2)
| true_fails(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id52) ).
fof(f79,axiom,
! [X0,X1,X2] :
( false_terminates(X0,X1,X2)
<=> ( ! [X3,X4,X5] :
( $true
& ( X0 != or(X3,X4)
| ( false_terminates(X3,X1,X5)
& ( false_fails(X3,X1,X5)
| false_terminates(X4,X5,X2) ) ) ) )
& ! [X6,X7] :
( $true
& ( X0 != and(X6,X7)
| false_terminates(X7,X1,X2) ) )
& ! [X8,X9] :
( $true
& ( X0 != and(X8,X9)
| false_terminates(X8,X1,X2) ) )
& ! [X10] :
( $true
& ( X0 != neg(X10)
| true_terminates(X10,X1,X2) ) )
& ! [X11] :
( $true
& ( X0 != p(X11)
| ( $true
& ( X2 != cons(neg(p(X11)),X1)
| ( member_terminates(p(X11),X1)
& gr(p(X11))
& gr(X1) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id79) ).
fof(f82,axiom,
! [X0,X1,X2] :
( true_terminates(X0,X1,X2)
<=> ( ! [X3,X4] :
( $true
& ( X0 != or(X3,X4)
| true_terminates(X4,X1,X2) ) )
& ! [X5,X6] :
( $true
& ( X0 != or(X5,X6)
| true_terminates(X5,X1,X2) ) )
& ! [X7,X8,X9] :
( $true
& ( X0 != and(X7,X8)
| ( true_terminates(X7,X1,X9)
& ( true_fails(X7,X1,X9)
| true_terminates(X8,X9,X2) ) ) ) )
& ! [X10] :
( $true
& ( X0 != neg(X10)
| false_terminates(X10,X1,X2) ) )
& ! [X11] :
( $true
& ( X0 != p(X11)
| ( $true
& ( X2 != cons(p(X11),X1)
| ( member_terminates(neg(p(X11)),X1)
& gr(neg(p(X11)))
& gr(X1) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id82) ).
fof(f111,axiom,
! [X0,X1] :
( list_succeeds(X1)
=> member_terminates(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(member:termination)') ).
fof(f118,axiom,
! [X0] :
( literal_list_succeeds(X0)
=> list_succeeds(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(literal_list:list)') ).
fof(f129,axiom,
! [X0,X1,X2] :
( ( true_succeeds(X0,X1,X2)
& literal_list_succeeds(X1) )
=> literal_list_succeeds(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','corollary-(true:literal_list)') ).
fof(f130,axiom,
! [X0,X1,X2] :
( ( false_succeeds(X0,X1,X2)
& literal_list_succeeds(X1) )
=> literal_list_succeeds(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','corollary-(false:literal_list)') ).
fof(f134,axiom,
! [X0,X1,X2] :
( ( true_succeeds(X0,X1,X2)
& gr(X0)
& gr(X1) )
=> gr(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','corollary-(true:gr)') ).
fof(f135,axiom,
! [X0,X1,X2] :
( ( false_succeeds(X0,X1,X2)
& gr(X0)
& gr(X1) )
=> gr(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','corollary-(false:gr)') ).
fof(f136,axiom,
( ! [X0] :
( ( ? [X1,X2] :
( X0 = or(X1,X2)
& formula_succeeds(X1)
& ! [X3,X4] :
( ( gr(X1)
& literal_list_succeeds(X3)
& gr(X3) )
=> ( true_terminates(X1,X3,X4)
& false_terminates(X1,X3,X4) ) )
& formula_succeeds(X2)
& ! [X3,X4] :
( ( gr(X2)
& literal_list_succeeds(X3)
& gr(X3) )
=> ( true_terminates(X2,X3,X4)
& false_terminates(X2,X3,X4) ) ) )
| ? [X5,X6] :
( X0 = and(X5,X6)
& formula_succeeds(X5)
& ! [X3,X4] :
( ( gr(X5)
& literal_list_succeeds(X3)
& gr(X3) )
=> ( true_terminates(X5,X3,X4)
& false_terminates(X5,X3,X4) ) )
& formula_succeeds(X6)
& ! [X3,X4] :
( ( gr(X6)
& literal_list_succeeds(X3)
& gr(X3) )
=> ( true_terminates(X6,X3,X4)
& false_terminates(X6,X3,X4) ) ) )
| ? [X7] :
( X0 = neg(X7)
& formula_succeeds(X7)
& ! [X3,X4] :
( ( gr(X7)
& literal_list_succeeds(X3)
& gr(X3) )
=> ( true_terminates(X7,X3,X4)
& false_terminates(X7,X3,X4) ) ) )
| ? [X8] : X0 = p(X8) )
=> ! [X3,X4] :
( ( gr(X0)
& literal_list_succeeds(X3)
& gr(X3) )
=> ( true_terminates(X0,X3,X4)
& false_terminates(X0,X3,X4) ) ) )
=> ! [X0] :
( formula_succeeds(X0)
=> ! [X3,X4] :
( ( gr(X0)
& literal_list_succeeds(X3)
& gr(X3) )
=> ( true_terminates(X0,X3,X4)
& false_terminates(X0,X3,X4) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',induction) ).
fof(f137,conjecture,
! [X0] :
( formula_succeeds(X0)
=> ! [X1,X2] :
( ( gr(X0)
& literal_list_succeeds(X1)
& gr(X1) )
=> ( true_terminates(X0,X1,X2)
& false_terminates(X0,X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(true:termination)') ).
fof(f138,negated_conjecture,
~ ! [X0] :
( formula_succeeds(X0)
=> ! [X1,X2] :
( ( gr(X0)
& literal_list_succeeds(X1)
& gr(X1) )
=> ( true_terminates(X0,X1,X2)
& false_terminates(X0,X1,X2) ) ) ),
inference(negated_conjecture,[status(cth)],[f137]) ).
fof(f142,plain,
! [X0,X1,X2] :
( false_terminates(X0,X1,X2)
<=> ( ! [X3,X4,X5] :
( X0 != or(X3,X4)
| ( false_terminates(X3,X1,X5)
& ( false_fails(X3,X1,X5)
| false_terminates(X4,X5,X2) ) ) )
& ! [X6,X7] :
( X0 != and(X6,X7)
| false_terminates(X7,X1,X2) )
& ! [X8,X9] :
( X0 != and(X8,X9)
| false_terminates(X8,X1,X2) )
& ! [X10] :
( X0 != neg(X10)
| true_terminates(X10,X1,X2) )
& ! [X11] :
( X0 != p(X11)
| X2 != cons(neg(p(X11)),X1)
| ( member_terminates(p(X11),X1)
& gr(p(X11))
& gr(X1) ) ) ) ),
inference(true_and_false_elimination,[],[f79]) ).
fof(f143,plain,
! [X0,X1,X2] :
( false_terminates(X0,X1,X2)
<=> ( ! [X3,X4,X5] :
( X0 != or(X3,X4)
| ( false_terminates(X3,X1,X5)
& ( false_fails(X3,X1,X5)
| false_terminates(X4,X5,X2) ) ) )
& ! [X6,X7] :
( X0 != and(X6,X7)
| false_terminates(X7,X1,X2) )
& ! [X8,X9] :
( X0 != and(X8,X9)
| false_terminates(X8,X1,X2) )
& ! [X10] :
( X0 != neg(X10)
| true_terminates(X10,X1,X2) )
& ! [X11] :
( X0 != p(X11)
| X2 != cons(neg(p(X11)),X1)
| ( member_terminates(p(X11),X1)
& gr(p(X11))
& gr(X1) ) ) ) ),
inference(flattening,[],[f142]) ).
fof(f144,plain,
! [X0,X1,X2] :
( true_terminates(X0,X1,X2)
<=> ( ! [X3,X4] :
( X0 != or(X3,X4)
| true_terminates(X4,X1,X2) )
& ! [X5,X6] :
( X0 != or(X5,X6)
| true_terminates(X5,X1,X2) )
& ! [X7,X8,X9] :
( X0 != and(X7,X8)
| ( true_terminates(X7,X1,X9)
& ( true_fails(X7,X1,X9)
| true_terminates(X8,X9,X2) ) ) )
& ! [X10] :
( X0 != neg(X10)
| false_terminates(X10,X1,X2) )
& ! [X11] :
( X0 != p(X11)
| X2 != cons(p(X11),X1)
| ( member_terminates(neg(p(X11)),X1)
& gr(neg(p(X11)))
& gr(X1) ) ) ) ),
inference(true_and_false_elimination,[],[f82]) ).
fof(f145,plain,
! [X0,X1,X2] :
( true_terminates(X0,X1,X2)
<=> ( ! [X3,X4] :
( X0 != or(X3,X4)
| true_terminates(X4,X1,X2) )
& ! [X5,X6] :
( X0 != or(X5,X6)
| true_terminates(X5,X1,X2) )
& ! [X7,X8,X9] :
( X0 != and(X7,X8)
| ( true_terminates(X7,X1,X9)
& ( true_fails(X7,X1,X9)
| true_terminates(X8,X9,X2) ) ) )
& ! [X10] :
( X0 != neg(X10)
| false_terminates(X10,X1,X2) )
& ! [X11] :
( X0 != p(X11)
| X2 != cons(p(X11),X1)
| ( member_terminates(neg(p(X11)),X1)
& gr(neg(p(X11)))
& gr(X1) ) ) ) ),
inference(flattening,[],[f144]) ).
fof(f156,plain,
( ! [X0] :
( ( ? [X1,X2] :
( X0 = or(X1,X2)
& formula_succeeds(X1)
& ! [X3,X4] :
( ( gr(X1)
& literal_list_succeeds(X3)
& gr(X3) )
=> ( true_terminates(X1,X3,X4)
& false_terminates(X1,X3,X4) ) )
& formula_succeeds(X2)
& ! [X5,X6] :
( ( gr(X2)
& literal_list_succeeds(X5)
& gr(X5) )
=> ( true_terminates(X2,X5,X6)
& false_terminates(X2,X5,X6) ) ) )
| ? [X7,X8] :
( and(X7,X8) = X0
& formula_succeeds(X7)
& ! [X9,X10] :
( ( gr(X7)
& literal_list_succeeds(X9)
& gr(X9) )
=> ( true_terminates(X7,X9,X10)
& false_terminates(X7,X9,X10) ) )
& formula_succeeds(X8)
& ! [X11,X12] :
( ( gr(X8)
& literal_list_succeeds(X11)
& gr(X11) )
=> ( true_terminates(X8,X11,X12)
& false_terminates(X8,X11,X12) ) ) )
| ? [X13] :
( neg(X13) = X0
& formula_succeeds(X13)
& ! [X14,X15] :
( ( gr(X13)
& literal_list_succeeds(X14)
& gr(X14) )
=> ( true_terminates(X13,X14,X15)
& false_terminates(X13,X14,X15) ) ) )
| ? [X16] : p(X16) = X0 )
=> ! [X17,X18] :
( ( gr(X0)
& literal_list_succeeds(X17)
& gr(X17) )
=> ( true_terminates(X0,X17,X18)
& false_terminates(X0,X17,X18) ) ) )
=> ! [X19] :
( formula_succeeds(X19)
=> ! [X20,X21] :
( ( gr(X19)
& literal_list_succeeds(X20)
& gr(X20) )
=> ( true_terminates(X19,X20,X21)
& false_terminates(X19,X20,X21) ) ) ) ),
inference(rectify,[],[f136]) ).
fof(f163,plain,
! [X0,X1] :
( X0 = X1
| neg(X0) != neg(X1) ),
inference(ennf_transformation,[],[f29]) ).
fof(f164,plain,
! [X0,X1,X2,X3] :
( X1 = X3
| and(X0,X1) != and(X2,X3) ),
inference(ennf_transformation,[],[f32]) ).
fof(f165,plain,
! [X0,X1,X2,X3] :
( X0 = X2
| and(X0,X1) != and(X2,X3) ),
inference(ennf_transformation,[],[f33]) ).
fof(f166,plain,
! [X0,X1,X2,X3] :
( X1 = X3
| or(X0,X1) != or(X2,X3) ),
inference(ennf_transformation,[],[f35]) ).
fof(f167,plain,
! [X0,X1,X2,X3] :
( X0 = X2
| or(X0,X1) != or(X2,X3) ),
inference(ennf_transformation,[],[f36]) ).
fof(f175,plain,
! [X0,X1,X2] :
( false_succeeds(X0,X1,X2)
| false_fails(X0,X1,X2)
| ~ false_terminates(X0,X1,X2) ),
inference(ennf_transformation,[],[f50]) ).
fof(f176,plain,
! [X0,X1,X2] :
( false_succeeds(X0,X1,X2)
| false_fails(X0,X1,X2)
| ~ false_terminates(X0,X1,X2) ),
inference(flattening,[],[f175]) ).
fof(f178,plain,
! [X0,X1,X2] :
( true_succeeds(X0,X1,X2)
| true_fails(X0,X1,X2)
| ~ true_terminates(X0,X1,X2) ),
inference(ennf_transformation,[],[f52]) ).
fof(f179,plain,
! [X0,X1,X2] :
( true_succeeds(X0,X1,X2)
| true_fails(X0,X1,X2)
| ~ true_terminates(X0,X1,X2) ),
inference(flattening,[],[f178]) ).
fof(f213,plain,
! [X0,X1] :
( member_terminates(X0,X1)
| ~ list_succeeds(X1) ),
inference(ennf_transformation,[],[f111]) ).
fof(f221,plain,
! [X0] :
( list_succeeds(X0)
| ~ literal_list_succeeds(X0) ),
inference(ennf_transformation,[],[f118]) ).
fof(f238,plain,
! [X0,X1,X2] :
( literal_list_succeeds(X2)
| ~ true_succeeds(X0,X1,X2)
| ~ literal_list_succeeds(X1) ),
inference(ennf_transformation,[],[f129]) ).
fof(f239,plain,
! [X0,X1,X2] :
( literal_list_succeeds(X2)
| ~ true_succeeds(X0,X1,X2)
| ~ literal_list_succeeds(X1) ),
inference(flattening,[],[f238]) ).
fof(f240,plain,
! [X0,X1,X2] :
( literal_list_succeeds(X2)
| ~ false_succeeds(X0,X1,X2)
| ~ literal_list_succeeds(X1) ),
inference(ennf_transformation,[],[f130]) ).
fof(f241,plain,
! [X0,X1,X2] :
( literal_list_succeeds(X2)
| ~ false_succeeds(X0,X1,X2)
| ~ literal_list_succeeds(X1) ),
inference(flattening,[],[f240]) ).
fof(f246,plain,
! [X0,X1,X2] :
( gr(X2)
| ~ true_succeeds(X0,X1,X2)
| ~ gr(X0)
| ~ gr(X1) ),
inference(ennf_transformation,[],[f134]) ).
fof(f247,plain,
! [X0,X1,X2] :
( gr(X2)
| ~ true_succeeds(X0,X1,X2)
| ~ gr(X0)
| ~ gr(X1) ),
inference(flattening,[],[f246]) ).
fof(f248,plain,
! [X0,X1,X2] :
( gr(X2)
| ~ false_succeeds(X0,X1,X2)
| ~ gr(X0)
| ~ gr(X1) ),
inference(ennf_transformation,[],[f135]) ).
fof(f249,plain,
! [X0,X1,X2] :
( gr(X2)
| ~ false_succeeds(X0,X1,X2)
| ~ gr(X0)
| ~ gr(X1) ),
inference(flattening,[],[f248]) ).
fof(f250,plain,
( ! [X19] :
( ! [X20,X21] :
( ( true_terminates(X19,X20,X21)
& false_terminates(X19,X20,X21) )
| ~ gr(X19)
| ~ literal_list_succeeds(X20)
| ~ gr(X20) )
| ~ formula_succeeds(X19) )
| ? [X0] :
( ? [X17,X18] :
( ( ~ true_terminates(X0,X17,X18)
| ~ false_terminates(X0,X17,X18) )
& gr(X0)
& literal_list_succeeds(X17)
& gr(X17) )
& ( ? [X1,X2] :
( X0 = or(X1,X2)
& formula_succeeds(X1)
& ! [X3,X4] :
( ( true_terminates(X1,X3,X4)
& false_terminates(X1,X3,X4) )
| ~ gr(X1)
| ~ literal_list_succeeds(X3)
| ~ gr(X3) )
& formula_succeeds(X2)
& ! [X5,X6] :
( ( true_terminates(X2,X5,X6)
& false_terminates(X2,X5,X6) )
| ~ gr(X2)
| ~ literal_list_succeeds(X5)
| ~ gr(X5) ) )
| ? [X7,X8] :
( and(X7,X8) = X0
& formula_succeeds(X7)
& ! [X9,X10] :
( ( true_terminates(X7,X9,X10)
& false_terminates(X7,X9,X10) )
| ~ gr(X7)
| ~ literal_list_succeeds(X9)
| ~ gr(X9) )
& formula_succeeds(X8)
& ! [X11,X12] :
( ( true_terminates(X8,X11,X12)
& false_terminates(X8,X11,X12) )
| ~ gr(X8)
| ~ literal_list_succeeds(X11)
| ~ gr(X11) ) )
| ? [X13] :
( neg(X13) = X0
& formula_succeeds(X13)
& ! [X14,X15] :
( ( true_terminates(X13,X14,X15)
& false_terminates(X13,X14,X15) )
| ~ gr(X13)
| ~ literal_list_succeeds(X14)
| ~ gr(X14) ) )
| ? [X16] : p(X16) = X0 ) ) ),
inference(ennf_transformation,[],[f156]) ).
fof(f251,plain,
( ! [X19] :
( ! [X20,X21] :
( ( true_terminates(X19,X20,X21)
& false_terminates(X19,X20,X21) )
| ~ gr(X19)
| ~ literal_list_succeeds(X20)
| ~ gr(X20) )
| ~ formula_succeeds(X19) )
| ? [X0] :
( ? [X17,X18] :
( ( ~ true_terminates(X0,X17,X18)
| ~ false_terminates(X0,X17,X18) )
& gr(X0)
& literal_list_succeeds(X17)
& gr(X17) )
& ( ? [X1,X2] :
( X0 = or(X1,X2)
& formula_succeeds(X1)
& ! [X3,X4] :
( ( true_terminates(X1,X3,X4)
& false_terminates(X1,X3,X4) )
| ~ gr(X1)
| ~ literal_list_succeeds(X3)
| ~ gr(X3) )
& formula_succeeds(X2)
& ! [X5,X6] :
( ( true_terminates(X2,X5,X6)
& false_terminates(X2,X5,X6) )
| ~ gr(X2)
| ~ literal_list_succeeds(X5)
| ~ gr(X5) ) )
| ? [X7,X8] :
( and(X7,X8) = X0
& formula_succeeds(X7)
& ! [X9,X10] :
( ( true_terminates(X7,X9,X10)
& false_terminates(X7,X9,X10) )
| ~ gr(X7)
| ~ literal_list_succeeds(X9)
| ~ gr(X9) )
& formula_succeeds(X8)
& ! [X11,X12] :
( ( true_terminates(X8,X11,X12)
& false_terminates(X8,X11,X12) )
| ~ gr(X8)
| ~ literal_list_succeeds(X11)
| ~ gr(X11) ) )
| ? [X13] :
( neg(X13) = X0
& formula_succeeds(X13)
& ! [X14,X15] :
( ( true_terminates(X13,X14,X15)
& false_terminates(X13,X14,X15) )
| ~ gr(X13)
| ~ literal_list_succeeds(X14)
| ~ gr(X14) ) )
| ? [X16] : p(X16) = X0 ) ) ),
inference(flattening,[],[f250]) ).
fof(f252,plain,
? [X0] :
( ? [X1,X2] :
( ( ~ true_terminates(X0,X1,X2)
| ~ false_terminates(X0,X1,X2) )
& gr(X0)
& literal_list_succeeds(X1)
& gr(X1) )
& formula_succeeds(X0) ),
inference(ennf_transformation,[],[f138]) ).
fof(f253,plain,
? [X0] :
( ? [X1,X2] :
( ( ~ true_terminates(X0,X1,X2)
| ~ false_terminates(X0,X1,X2) )
& gr(X0)
& literal_list_succeeds(X1)
& gr(X1) )
& formula_succeeds(X0) ),
inference(flattening,[],[f252]) ).
fof(f307,definition,
! [X0,X2,X1] :
( sP45(X0,X2,X1)
<=> ! [X11] :
( X0 != p(X11)
| X2 != cons(neg(p(X11)),X1)
| ( member_terminates(p(X11),X1)
& gr(p(X11))
& gr(X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP45])],[predicate_definition_introduction]) ).
fof(f308,definition,
! [X0,X1,X2] :
( sP46(X0,X1,X2)
<=> ! [X3,X4,X5] :
( X0 != or(X3,X4)
| ( false_terminates(X3,X1,X5)
& ( false_fails(X3,X1,X5)
| false_terminates(X4,X5,X2) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP46])],[predicate_definition_introduction]) ).
fof(f309,definition,
! [X2,X1,X0] :
( sP47(X2,X1,X0)
<=> ( sP46(X0,X1,X2)
& ! [X6,X7] :
( X0 != and(X6,X7)
| false_terminates(X7,X1,X2) )
& ! [X8,X9] :
( X0 != and(X8,X9)
| false_terminates(X8,X1,X2) )
& ! [X10] :
( X0 != neg(X10)
| true_terminates(X10,X1,X2) )
& sP45(X0,X2,X1) ) ),
introduced(definition,[new_symbols(definition,[sP47])],[predicate_definition_introduction]) ).
fof(f310,plain,
! [X0,X1,X2] :
( false_terminates(X0,X1,X2)
<=> sP47(X2,X1,X0) ),
inference(definition_folding,[],[f143,f309,f308,f307]) ).
fof(f319,definition,
! [X0,X2,X1] :
( sP54(X0,X2,X1)
<=> ! [X11] :
( X0 != p(X11)
| X2 != cons(p(X11),X1)
| ( member_terminates(neg(p(X11)),X1)
& gr(neg(p(X11)))
& gr(X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP54])],[predicate_definition_introduction]) ).
fof(f320,definition,
! [X0,X1,X2] :
( sP55(X0,X1,X2)
<=> ! [X7,X8,X9] :
( X0 != and(X7,X8)
| ( true_terminates(X7,X1,X9)
& ( true_fails(X7,X1,X9)
| true_terminates(X8,X9,X2) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP55])],[predicate_definition_introduction]) ).
fof(f321,definition,
! [X0,X2,X1] :
( sP56(X0,X2,X1)
<=> ( ! [X3,X4] :
( X0 != or(X3,X4)
| true_terminates(X4,X1,X2) )
& ! [X5,X6] :
( X0 != or(X5,X6)
| true_terminates(X5,X1,X2) )
& sP55(X0,X1,X2)
& ! [X10] :
( X0 != neg(X10)
| false_terminates(X10,X1,X2) )
& sP54(X0,X2,X1) ) ),
introduced(definition,[new_symbols(definition,[sP56])],[predicate_definition_introduction]) ).
fof(f322,plain,
! [X0,X1,X2] :
( true_terminates(X0,X1,X2)
<=> sP56(X0,X2,X1) ),
inference(definition_folding,[],[f145,f321,f320,f319]) ).
fof(f332,definition,
! [X0] :
( ? [X7,X8] :
( and(X7,X8) = X0
& formula_succeeds(X7)
& ! [X9,X10] :
( ( true_terminates(X7,X9,X10)
& false_terminates(X7,X9,X10) )
| ~ gr(X7)
| ~ literal_list_succeeds(X9)
| ~ gr(X9) )
& formula_succeeds(X8)
& ! [X11,X12] :
( ( true_terminates(X8,X11,X12)
& false_terminates(X8,X11,X12) )
| ~ gr(X8)
| ~ literal_list_succeeds(X11)
| ~ gr(X11) ) )
| ~ sP63(X0) ),
introduced(definition,[new_symbols(definition,[sP63])],[predicate_definition_introduction]) ).
fof(f333,definition,
! [X0] :
( ? [X1,X2] :
( X0 = or(X1,X2)
& formula_succeeds(X1)
& ! [X3,X4] :
( ( true_terminates(X1,X3,X4)
& false_terminates(X1,X3,X4) )
| ~ gr(X1)
| ~ literal_list_succeeds(X3)
| ~ gr(X3) )
& formula_succeeds(X2)
& ! [X5,X6] :
( ( true_terminates(X2,X5,X6)
& false_terminates(X2,X5,X6) )
| ~ gr(X2)
| ~ literal_list_succeeds(X5)
| ~ gr(X5) ) )
| ~ sP64(X0) ),
introduced(definition,[new_symbols(definition,[sP64])],[predicate_definition_introduction]) ).
fof(f334,definition,
( ? [X0] :
( ? [X17,X18] :
( ( ~ true_terminates(X0,X17,X18)
| ~ false_terminates(X0,X17,X18) )
& gr(X0)
& literal_list_succeeds(X17)
& gr(X17) )
& ( sP64(X0)
| sP63(X0)
| ? [X13] :
( neg(X13) = X0
& formula_succeeds(X13)
& ! [X14,X15] :
( ( true_terminates(X13,X14,X15)
& false_terminates(X13,X14,X15) )
| ~ gr(X13)
| ~ literal_list_succeeds(X14)
| ~ gr(X14) ) )
| ? [X16] : p(X16) = X0 ) )
| ~ sP65 ),
introduced(definition,[new_symbols(definition,[sP65])],[predicate_definition_introduction]) ).
fof(f335,plain,
( ! [X19] :
( ! [X20,X21] :
( ( true_terminates(X19,X20,X21)
& false_terminates(X19,X20,X21) )
| ~ gr(X19)
| ~ literal_list_succeeds(X20)
| ~ gr(X20) )
| ~ formula_succeeds(X19) )
| sP65 ),
inference(definition_folding,[],[f251,f334,f333,f332]) ).
fof(f339,plain,
! [X0] :
( ( gr(X0)
| ~ gr(neg(X0)) )
& ( gr(neg(X0))
| ~ gr(X0) ) ),
inference(nnf_transformation,[],[f42]) ).
fof(f340,plain,
! [X0,X1] :
( ( ( gr(X0)
& gr(X1) )
| ~ gr(and(X0,X1)) )
& ( gr(and(X0,X1))
| ~ gr(X0)
| ~ gr(X1) ) ),
inference(nnf_transformation,[],[f43]) ).
fof(f341,plain,
! [X0,X1] :
( ( ( gr(X0)
& gr(X1) )
| ~ gr(and(X0,X1)) )
& ( gr(and(X0,X1))
| ~ gr(X0)
| ~ gr(X1) ) ),
inference(flattening,[],[f340]) ).
fof(f342,plain,
! [X0,X1] :
( ( ( gr(X0)
& gr(X1) )
| ~ gr(or(X0,X1)) )
& ( gr(or(X0,X1))
| ~ gr(X0)
| ~ gr(X1) ) ),
inference(nnf_transformation,[],[f44]) ).
fof(f343,plain,
! [X0,X1] :
( ( ( gr(X0)
& gr(X1) )
| ~ gr(or(X0,X1)) )
& ( gr(or(X0,X1))
| ~ gr(X0)
| ~ gr(X1) ) ),
inference(flattening,[],[f342]) ).
fof(f495,plain,
! [X2,X1,X0] :
( ( sP47(X2,X1,X0)
| ~ sP46(X0,X1,X2)
| ? [X6,X7] :
( and(X6,X7) = X0
& ~ false_terminates(X7,X1,X2) )
| ? [X8,X9] :
( and(X8,X9) = X0
& ~ false_terminates(X8,X1,X2) )
| ? [X10] :
( neg(X10) = X0
& ~ true_terminates(X10,X1,X2) )
| ~ sP45(X0,X2,X1) )
& ( ( sP46(X0,X1,X2)
& ! [X6,X7] :
( X0 != and(X6,X7)
| false_terminates(X7,X1,X2) )
& ! [X8,X9] :
( X0 != and(X8,X9)
| false_terminates(X8,X1,X2) )
& ! [X10] :
( X0 != neg(X10)
| true_terminates(X10,X1,X2) )
& sP45(X0,X2,X1) )
| ~ sP47(X2,X1,X0) ) ),
inference(nnf_transformation,[],[f309]) ).
fof(f496,plain,
! [X2,X1,X0] :
( ( sP47(X2,X1,X0)
| ~ sP46(X0,X1,X2)
| ? [X6,X7] :
( and(X6,X7) = X0
& ~ false_terminates(X7,X1,X2) )
| ? [X8,X9] :
( and(X8,X9) = X0
& ~ false_terminates(X8,X1,X2) )
| ? [X10] :
( neg(X10) = X0
& ~ true_terminates(X10,X1,X2) )
| ~ sP45(X0,X2,X1) )
& ( ( sP46(X0,X1,X2)
& ! [X6,X7] :
( X0 != and(X6,X7)
| false_terminates(X7,X1,X2) )
& ! [X8,X9] :
( X0 != and(X8,X9)
| false_terminates(X8,X1,X2) )
& ! [X10] :
( X0 != neg(X10)
| true_terminates(X10,X1,X2) )
& sP45(X0,X2,X1) )
| ~ sP47(X2,X1,X0) ) ),
inference(flattening,[],[f495]) ).
fof(f497,plain,
! [X0,X1,X2] :
( ( sP47(X0,X1,X2)
| ~ sP46(X2,X1,X0)
| ? [X3,X4] :
( and(X3,X4) = X2
& ~ false_terminates(X4,X1,X0) )
| ? [X5,X6] :
( and(X5,X6) = X2
& ~ false_terminates(X5,X1,X0) )
| ? [X7] :
( neg(X7) = X2
& ~ true_terminates(X7,X1,X0) )
| ~ sP45(X2,X0,X1) )
& ( ( sP46(X2,X1,X0)
& ! [X8,X9] :
( and(X8,X9) != X2
| false_terminates(X9,X1,X0) )
& ! [X10,X11] :
( and(X10,X11) != X2
| false_terminates(X10,X1,X0) )
& ! [X12] :
( neg(X12) != X2
| true_terminates(X12,X1,X0) )
& sP45(X2,X0,X1) )
| ~ sP47(X0,X1,X2) ) ),
inference(rectify,[],[f496]) ).
fof(f498,plain,
! [X0,X1,X2] :
( ( sP47(X0,X1,X2)
| ~ sP46(X2,X1,X0)
| ( and(sK153(X0,X1,X2),sK154(X0,X1,X2)) = X2
& ~ false_terminates(sK154(X0,X1,X2),X1,X0) )
| ( and(sK155(X0,X1,X2),sK156(X0,X1,X2)) = X2
& ~ false_terminates(sK155(X0,X1,X2),X1,X0) )
| ( neg(sK157(X0,X1,X2)) = X2
& ~ true_terminates(sK157(X0,X1,X2),X1,X0) )
| ~ sP45(X2,X0,X1) )
& ( ( sP46(X2,X1,X0)
& ! [X8,X9] :
( and(X8,X9) != X2
| false_terminates(X9,X1,X0) )
& ! [X10,X11] :
( and(X10,X11) != X2
| false_terminates(X10,X1,X0) )
& ! [X12] :
( neg(X12) != X2
| true_terminates(X12,X1,X0) )
& sP45(X2,X0,X1) )
| ~ sP47(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK153,sK154,sK155,sK156,sK157]),skolemize(X3,sK153(X0,X1,X2)),skolemize(X4,sK154(X0,X1,X2)),skolemize(X5,sK155(X0,X1,X2)),skolemize(X6,sK156(X0,X1,X2)),skolemize(X7,sK157(X0,X1,X2))],[f497]) ).
fof(f499,plain,
! [X0,X1,X2] :
( ( sP46(X0,X1,X2)
| ? [X3,X4,X5] :
( or(X3,X4) = X0
& ( ~ false_terminates(X3,X1,X5)
| ( ~ false_fails(X3,X1,X5)
& ~ false_terminates(X4,X5,X2) ) ) ) )
& ( ! [X3,X4,X5] :
( X0 != or(X3,X4)
| ( false_terminates(X3,X1,X5)
& ( false_fails(X3,X1,X5)
| false_terminates(X4,X5,X2) ) ) )
| ~ sP46(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f308]) ).
fof(f500,plain,
! [X0,X1,X2] :
( ( sP46(X0,X1,X2)
| ? [X3,X4,X5] :
( or(X3,X4) = X0
& ( ~ false_terminates(X3,X1,X5)
| ( ~ false_fails(X3,X1,X5)
& ~ false_terminates(X4,X5,X2) ) ) ) )
& ( ! [X6,X7,X8] :
( or(X6,X7) != X0
| ( false_terminates(X6,X1,X8)
& ( false_fails(X6,X1,X8)
| false_terminates(X7,X8,X2) ) ) )
| ~ sP46(X0,X1,X2) ) ),
inference(rectify,[],[f499]) ).
fof(f501,plain,
! [X0,X1,X2] :
( ( sP46(X0,X1,X2)
| ( or(sK158(X0,X1,X2),sK159(X0,X1,X2)) = X0
& ( ~ false_terminates(sK158(X0,X1,X2),X1,sK160(X0,X1,X2))
| ( ~ false_fails(sK158(X0,X1,X2),X1,sK160(X0,X1,X2))
& ~ false_terminates(sK159(X0,X1,X2),sK160(X0,X1,X2),X2) ) ) ) )
& ( ! [X6,X7,X8] :
( or(X6,X7) != X0
| ( false_terminates(X6,X1,X8)
& ( false_fails(X6,X1,X8)
| false_terminates(X7,X8,X2) ) ) )
| ~ sP46(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK158,sK159,sK160]),skolemize(X3,sK158(X0,X1,X2)),skolemize(X4,sK159(X0,X1,X2)),skolemize(X5,sK160(X0,X1,X2))],[f500]) ).
fof(f502,plain,
! [X0,X2,X1] :
( ( sP45(X0,X2,X1)
| ? [X11] :
( p(X11) = X0
& cons(neg(p(X11)),X1) = X2
& ( ~ member_terminates(p(X11),X1)
| ~ gr(p(X11))
| ~ gr(X1) ) ) )
& ( ! [X11] :
( X0 != p(X11)
| X2 != cons(neg(p(X11)),X1)
| ( member_terminates(p(X11),X1)
& gr(p(X11))
& gr(X1) ) )
| ~ sP45(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f307]) ).
fof(f503,plain,
! [X0,X1,X2] :
( ( sP45(X0,X1,X2)
| ? [X3] :
( p(X3) = X0
& cons(neg(p(X3)),X2) = X1
& ( ~ member_terminates(p(X3),X2)
| ~ gr(p(X3))
| ~ gr(X2) ) ) )
& ( ! [X4] :
( p(X4) != X0
| cons(neg(p(X4)),X2) != X1
| ( member_terminates(p(X4),X2)
& gr(p(X4))
& gr(X2) ) )
| ~ sP45(X0,X1,X2) ) ),
inference(rectify,[],[f502]) ).
fof(f504,plain,
! [X0,X1,X2] :
( ( sP45(X0,X1,X2)
| ( p(sK161(X0,X1,X2)) = X0
& cons(neg(p(sK161(X0,X1,X2))),X2) = X1
& ( ~ member_terminates(p(sK161(X0,X1,X2)),X2)
| ~ gr(p(sK161(X0,X1,X2)))
| ~ gr(X2) ) ) )
& ( ! [X4] :
( p(X4) != X0
| cons(neg(p(X4)),X2) != X1
| ( member_terminates(p(X4),X2)
& gr(p(X4))
& gr(X2) ) )
| ~ sP45(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK161]),skolemize(X3,sK161(X0,X1,X2))],[f503]) ).
fof(f505,plain,
! [X0,X1,X2] :
( ( false_terminates(X0,X1,X2)
| ~ sP47(X2,X1,X0) )
& ( sP47(X2,X1,X0)
| ~ false_terminates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f310]) ).
fof(f528,plain,
! [X0,X2,X1] :
( ( sP56(X0,X2,X1)
| ? [X3,X4] :
( or(X3,X4) = X0
& ~ true_terminates(X4,X1,X2) )
| ? [X5,X6] :
( or(X5,X6) = X0
& ~ true_terminates(X5,X1,X2) )
| ~ sP55(X0,X1,X2)
| ? [X10] :
( neg(X10) = X0
& ~ false_terminates(X10,X1,X2) )
| ~ sP54(X0,X2,X1) )
& ( ( ! [X3,X4] :
( X0 != or(X3,X4)
| true_terminates(X4,X1,X2) )
& ! [X5,X6] :
( X0 != or(X5,X6)
| true_terminates(X5,X1,X2) )
& sP55(X0,X1,X2)
& ! [X10] :
( X0 != neg(X10)
| false_terminates(X10,X1,X2) )
& sP54(X0,X2,X1) )
| ~ sP56(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f321]) ).
fof(f529,plain,
! [X0,X2,X1] :
( ( sP56(X0,X2,X1)
| ? [X3,X4] :
( or(X3,X4) = X0
& ~ true_terminates(X4,X1,X2) )
| ? [X5,X6] :
( or(X5,X6) = X0
& ~ true_terminates(X5,X1,X2) )
| ~ sP55(X0,X1,X2)
| ? [X10] :
( neg(X10) = X0
& ~ false_terminates(X10,X1,X2) )
| ~ sP54(X0,X2,X1) )
& ( ( ! [X3,X4] :
( X0 != or(X3,X4)
| true_terminates(X4,X1,X2) )
& ! [X5,X6] :
( X0 != or(X5,X6)
| true_terminates(X5,X1,X2) )
& sP55(X0,X1,X2)
& ! [X10] :
( X0 != neg(X10)
| false_terminates(X10,X1,X2) )
& sP54(X0,X2,X1) )
| ~ sP56(X0,X2,X1) ) ),
inference(flattening,[],[f528]) ).
fof(f530,plain,
! [X0,X1,X2] :
( ( sP56(X0,X1,X2)
| ? [X3,X4] :
( or(X3,X4) = X0
& ~ true_terminates(X4,X2,X1) )
| ? [X5,X6] :
( or(X5,X6) = X0
& ~ true_terminates(X5,X2,X1) )
| ~ sP55(X0,X2,X1)
| ? [X7] :
( neg(X7) = X0
& ~ false_terminates(X7,X2,X1) )
| ~ sP54(X0,X1,X2) )
& ( ( ! [X8,X9] :
( or(X8,X9) != X0
| true_terminates(X9,X2,X1) )
& ! [X10,X11] :
( or(X10,X11) != X0
| true_terminates(X10,X2,X1) )
& sP55(X0,X2,X1)
& ! [X12] :
( neg(X12) != X0
| false_terminates(X12,X2,X1) )
& sP54(X0,X1,X2) )
| ~ sP56(X0,X1,X2) ) ),
inference(rectify,[],[f529]) ).
fof(f531,plain,
! [X0,X1,X2] :
( ( sP56(X0,X1,X2)
| ( or(sK180(X0,X1,X2),sK181(X0,X1,X2)) = X0
& ~ true_terminates(sK181(X0,X1,X2),X2,X1) )
| ( or(sK182(X0,X1,X2),sK183(X0,X1,X2)) = X0
& ~ true_terminates(sK182(X0,X1,X2),X2,X1) )
| ~ sP55(X0,X2,X1)
| ( neg(sK184(X0,X1,X2)) = X0
& ~ false_terminates(sK184(X0,X1,X2),X2,X1) )
| ~ sP54(X0,X1,X2) )
& ( ( ! [X8,X9] :
( or(X8,X9) != X0
| true_terminates(X9,X2,X1) )
& ! [X10,X11] :
( or(X10,X11) != X0
| true_terminates(X10,X2,X1) )
& sP55(X0,X2,X1)
& ! [X12] :
( neg(X12) != X0
| false_terminates(X12,X2,X1) )
& sP54(X0,X1,X2) )
| ~ sP56(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK180,sK181,sK182,sK183,sK184]),skolemize(X3,sK180(X0,X1,X2)),skolemize(X4,sK181(X0,X1,X2)),skolemize(X5,sK182(X0,X1,X2)),skolemize(X6,sK183(X0,X1,X2)),skolemize(X7,sK184(X0,X1,X2))],[f530]) ).
fof(f532,plain,
! [X0,X1,X2] :
( ( sP55(X0,X1,X2)
| ? [X7,X8,X9] :
( and(X7,X8) = X0
& ( ~ true_terminates(X7,X1,X9)
| ( ~ true_fails(X7,X1,X9)
& ~ true_terminates(X8,X9,X2) ) ) ) )
& ( ! [X7,X8,X9] :
( X0 != and(X7,X8)
| ( true_terminates(X7,X1,X9)
& ( true_fails(X7,X1,X9)
| true_terminates(X8,X9,X2) ) ) )
| ~ sP55(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f320]) ).
fof(f533,plain,
! [X0,X1,X2] :
( ( sP55(X0,X1,X2)
| ? [X3,X4,X5] :
( and(X3,X4) = X0
& ( ~ true_terminates(X3,X1,X5)
| ( ~ true_fails(X3,X1,X5)
& ~ true_terminates(X4,X5,X2) ) ) ) )
& ( ! [X6,X7,X8] :
( and(X6,X7) != X0
| ( true_terminates(X6,X1,X8)
& ( true_fails(X6,X1,X8)
| true_terminates(X7,X8,X2) ) ) )
| ~ sP55(X0,X1,X2) ) ),
inference(rectify,[],[f532]) ).
fof(f534,plain,
! [X0,X1,X2] :
( ( sP55(X0,X1,X2)
| ( and(sK185(X0,X1,X2),sK186(X0,X1,X2)) = X0
& ( ~ true_terminates(sK185(X0,X1,X2),X1,sK187(X0,X1,X2))
| ( ~ true_fails(sK185(X0,X1,X2),X1,sK187(X0,X1,X2))
& ~ true_terminates(sK186(X0,X1,X2),sK187(X0,X1,X2),X2) ) ) ) )
& ( ! [X6,X7,X8] :
( and(X6,X7) != X0
| ( true_terminates(X6,X1,X8)
& ( true_fails(X6,X1,X8)
| true_terminates(X7,X8,X2) ) ) )
| ~ sP55(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK185,sK186,sK187]),skolemize(X3,sK185(X0,X1,X2)),skolemize(X4,sK186(X0,X1,X2)),skolemize(X5,sK187(X0,X1,X2))],[f533]) ).
fof(f535,plain,
! [X0,X2,X1] :
( ( sP54(X0,X2,X1)
| ? [X11] :
( p(X11) = X0
& cons(p(X11),X1) = X2
& ( ~ member_terminates(neg(p(X11)),X1)
| ~ gr(neg(p(X11)))
| ~ gr(X1) ) ) )
& ( ! [X11] :
( X0 != p(X11)
| X2 != cons(p(X11),X1)
| ( member_terminates(neg(p(X11)),X1)
& gr(neg(p(X11)))
& gr(X1) ) )
| ~ sP54(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f319]) ).
fof(f536,plain,
! [X0,X1,X2] :
( ( sP54(X0,X1,X2)
| ? [X3] :
( p(X3) = X0
& cons(p(X3),X2) = X1
& ( ~ member_terminates(neg(p(X3)),X2)
| ~ gr(neg(p(X3)))
| ~ gr(X2) ) ) )
& ( ! [X4] :
( p(X4) != X0
| cons(p(X4),X2) != X1
| ( member_terminates(neg(p(X4)),X2)
& gr(neg(p(X4)))
& gr(X2) ) )
| ~ sP54(X0,X1,X2) ) ),
inference(rectify,[],[f535]) ).
fof(f537,plain,
! [X0,X1,X2] :
( ( sP54(X0,X1,X2)
| ( p(sK188(X0,X1,X2)) = X0
& cons(p(sK188(X0,X1,X2)),X2) = X1
& ( ~ member_terminates(neg(p(sK188(X0,X1,X2))),X2)
| ~ gr(neg(p(sK188(X0,X1,X2))))
| ~ gr(X2) ) ) )
& ( ! [X4] :
( p(X4) != X0
| cons(p(X4),X2) != X1
| ( member_terminates(neg(p(X4)),X2)
& gr(neg(p(X4)))
& gr(X2) ) )
| ~ sP54(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK188]),skolemize(X3,sK188(X0,X1,X2))],[f536]) ).
fof(f538,plain,
! [X0,X1,X2] :
( ( true_terminates(X0,X1,X2)
| ~ sP56(X0,X2,X1) )
& ( sP56(X0,X2,X1)
| ~ true_terminates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f322]) ).
fof(f630,plain,
( ? [X0] :
( ? [X17,X18] :
( ( ~ true_terminates(X0,X17,X18)
| ~ false_terminates(X0,X17,X18) )
& gr(X0)
& literal_list_succeeds(X17)
& gr(X17) )
& ( sP64(X0)
| sP63(X0)
| ? [X13] :
( neg(X13) = X0
& formula_succeeds(X13)
& ! [X14,X15] :
( ( true_terminates(X13,X14,X15)
& false_terminates(X13,X14,X15) )
| ~ gr(X13)
| ~ literal_list_succeeds(X14)
| ~ gr(X14) ) )
| ? [X16] : p(X16) = X0 ) )
| ~ sP65 ),
inference(nnf_transformation,[],[f334]) ).
fof(f631,plain,
( ? [X0] :
( ? [X1,X2] :
( ( ~ true_terminates(X0,X1,X2)
| ~ false_terminates(X0,X1,X2) )
& gr(X0)
& literal_list_succeeds(X1)
& gr(X1) )
& ( sP64(X0)
| sP63(X0)
| ? [X3] :
( neg(X3) = X0
& formula_succeeds(X3)
& ! [X4,X5] :
( ( true_terminates(X3,X4,X5)
& false_terminates(X3,X4,X5) )
| ~ gr(X3)
| ~ literal_list_succeeds(X4)
| ~ gr(X4) ) )
| ? [X6] : p(X6) = X0 ) )
| ~ sP65 ),
inference(rectify,[],[f630]) ).
fof(f632,plain,
( ( ( ~ true_terminates(sK238,sK239,sK240)
| ~ false_terminates(sK238,sK239,sK240) )
& gr(sK238)
& literal_list_succeeds(sK239)
& gr(sK239)
& ( sP64(sK238)
| sP63(sK238)
| ( sK238 = neg(sK241)
& formula_succeeds(sK241)
& ! [X4,X5] :
( ( true_terminates(sK241,X4,X5)
& false_terminates(sK241,X4,X5) )
| ~ gr(sK241)
| ~ literal_list_succeeds(X4)
| ~ gr(X4) ) )
| sK238 = p(sK242) ) )
| ~ sP65 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK238,sK239,sK240,sK241,sK242]),skolemize(X0,sK238),skolemize(X1,sK239),skolemize(X2,sK240),skolemize(X3,sK241),skolemize(X6,sK242)],[f631]) ).
fof(f633,plain,
! [X0] :
( ? [X1,X2] :
( X0 = or(X1,X2)
& formula_succeeds(X1)
& ! [X3,X4] :
( ( true_terminates(X1,X3,X4)
& false_terminates(X1,X3,X4) )
| ~ gr(X1)
| ~ literal_list_succeeds(X3)
| ~ gr(X3) )
& formula_succeeds(X2)
& ! [X5,X6] :
( ( true_terminates(X2,X5,X6)
& false_terminates(X2,X5,X6) )
| ~ gr(X2)
| ~ literal_list_succeeds(X5)
| ~ gr(X5) ) )
| ~ sP64(X0) ),
inference(nnf_transformation,[],[f333]) ).
fof(f634,plain,
! [X0] :
( ( or(sK243(X0),sK244(X0)) = X0
& formula_succeeds(sK243(X0))
& ! [X3,X4] :
( ( true_terminates(sK243(X0),X3,X4)
& false_terminates(sK243(X0),X3,X4) )
| ~ gr(sK243(X0))
| ~ literal_list_succeeds(X3)
| ~ gr(X3) )
& formula_succeeds(sK244(X0))
& ! [X5,X6] :
( ( true_terminates(sK244(X0),X5,X6)
& false_terminates(sK244(X0),X5,X6) )
| ~ gr(sK244(X0))
| ~ literal_list_succeeds(X5)
| ~ gr(X5) ) )
| ~ sP64(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK243,sK244]),skolemize(X1,sK243(X0)),skolemize(X2,sK244(X0))],[f633]) ).
fof(f635,plain,
! [X0] :
( ? [X7,X8] :
( and(X7,X8) = X0
& formula_succeeds(X7)
& ! [X9,X10] :
( ( true_terminates(X7,X9,X10)
& false_terminates(X7,X9,X10) )
| ~ gr(X7)
| ~ literal_list_succeeds(X9)
| ~ gr(X9) )
& formula_succeeds(X8)
& ! [X11,X12] :
( ( true_terminates(X8,X11,X12)
& false_terminates(X8,X11,X12) )
| ~ gr(X8)
| ~ literal_list_succeeds(X11)
| ~ gr(X11) ) )
| ~ sP63(X0) ),
inference(nnf_transformation,[],[f332]) ).
fof(f636,plain,
! [X0] :
( ? [X1,X2] :
( and(X1,X2) = X0
& formula_succeeds(X1)
& ! [X3,X4] :
( ( true_terminates(X1,X3,X4)
& false_terminates(X1,X3,X4) )
| ~ gr(X1)
| ~ literal_list_succeeds(X3)
| ~ gr(X3) )
& formula_succeeds(X2)
& ! [X5,X6] :
( ( true_terminates(X2,X5,X6)
& false_terminates(X2,X5,X6) )
| ~ gr(X2)
| ~ literal_list_succeeds(X5)
| ~ gr(X5) ) )
| ~ sP63(X0) ),
inference(rectify,[],[f635]) ).
fof(f637,plain,
! [X0] :
( ( and(sK245(X0),sK246(X0)) = X0
& formula_succeeds(sK245(X0))
& ! [X3,X4] :
( ( true_terminates(sK245(X0),X3,X4)
& false_terminates(sK245(X0),X3,X4) )
| ~ gr(sK245(X0))
| ~ literal_list_succeeds(X3)
| ~ gr(X3) )
& formula_succeeds(sK246(X0))
& ! [X5,X6] :
( ( true_terminates(sK246(X0),X5,X6)
& false_terminates(sK246(X0),X5,X6) )
| ~ gr(sK246(X0))
| ~ literal_list_succeeds(X5)
| ~ gr(X5) ) )
| ~ sP63(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK245,sK246]),skolemize(X1,sK245(X0)),skolemize(X2,sK246(X0))],[f636]) ).
fof(f638,plain,
( ! [X0] :
( ! [X1,X2] :
( ( true_terminates(X0,X1,X2)
& false_terminates(X0,X1,X2) )
| ~ gr(X0)
| ~ literal_list_succeeds(X1)
| ~ gr(X1) )
| ~ formula_succeeds(X0) )
| sP65 ),
inference(rectify,[],[f335]) ).
fof(f639,plain,
( ( ~ true_terminates(sK247,sK248,sK249)
| ~ false_terminates(sK247,sK248,sK249) )
& gr(sK247)
& literal_list_succeeds(sK248)
& gr(sK248)
& formula_succeeds(sK247) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK247,sK248,sK249]),skolemize(X0,sK247),skolemize(X1,sK248),skolemize(X2,sK249)],[f253]) ).
fof(f665,plain,
! [X0,X1] : p(X0) != neg(X1),
inference(cnf_transformation,[],[f26]) ).
fof(f666,plain,
! [X2,X0,X1] : p(X0) != and(X1,X2),
inference(cnf_transformation,[],[f27]) ).
fof(f667,plain,
! [X2,X0,X1] : p(X0) != or(X1,X2),
inference(cnf_transformation,[],[f28]) ).
fof(f668,plain,
! [X0,X1] :
( X0 = X1
| neg(X0) != neg(X1) ),
inference(cnf_transformation,[],[f163]) ).
fof(f669,plain,
! [X2,X0,X1] : neg(X0) != and(X1,X2),
inference(cnf_transformation,[],[f30]) ).
fof(f670,plain,
! [X2,X0,X1] : neg(X0) != or(X1,X2),
inference(cnf_transformation,[],[f31]) ).
fof(f671,plain,
! [X2,X3,X0,X1] :
( X1 = X3
| and(X0,X1) != and(X2,X3) ),
inference(cnf_transformation,[],[f164]) ).
fof(f672,plain,
! [X2,X3,X0,X1] :
( X0 = X2
| and(X0,X1) != and(X2,X3) ),
inference(cnf_transformation,[],[f165]) ).
fof(f673,plain,
! [X2,X3,X0,X1] : and(X0,X1) != or(X2,X3),
inference(cnf_transformation,[],[f34]) ).
fof(f674,plain,
! [X2,X3,X0,X1] :
( X1 = X3
| or(X0,X1) != or(X2,X3) ),
inference(cnf_transformation,[],[f166]) ).
fof(f675,plain,
! [X2,X3,X0,X1] :
( X0 = X2
| or(X0,X1) != or(X2,X3) ),
inference(cnf_transformation,[],[f167]) ).
fof(f684,plain,
! [X0] :
( gr(neg(X0))
| ~ gr(X0) ),
inference(cnf_transformation,[],[f339]) ).
fof(f685,plain,
! [X0] :
( gr(X0)
| ~ gr(neg(X0)) ),
inference(cnf_transformation,[],[f339]) ).
fof(f687,plain,
! [X0,X1] :
( gr(X1)
| ~ gr(and(X0,X1)) ),
inference(cnf_transformation,[],[f341]) ).
fof(f688,plain,
! [X0,X1] :
( gr(X0)
| ~ gr(and(X0,X1)) ),
inference(cnf_transformation,[],[f341]) ).
fof(f690,plain,
! [X0,X1] :
( gr(X1)
| ~ gr(or(X0,X1)) ),
inference(cnf_transformation,[],[f343]) ).
fof(f691,plain,
! [X0,X1] :
( gr(X0)
| ~ gr(or(X0,X1)) ),
inference(cnf_transformation,[],[f343]) ).
fof(f697,plain,
! [X2,X0,X1] :
( false_succeeds(X0,X1,X2)
| false_fails(X0,X1,X2)
| ~ false_terminates(X0,X1,X2) ),
inference(cnf_transformation,[],[f176]) ).
fof(f699,plain,
! [X2,X0,X1] :
( true_succeeds(X0,X1,X2)
| true_fails(X0,X1,X2)
| ~ true_terminates(X0,X1,X2) ),
inference(cnf_transformation,[],[f179]) ).
fof(f1002,plain,
! [X2,X0,X1] :
( sP47(X0,X1,X2)
| ~ sP46(X2,X1,X0)
| ~ false_terminates(sK154(X0,X1,X2),X1,X0)
| ~ false_terminates(sK155(X0,X1,X2),X1,X0)
| neg(sK157(X0,X1,X2)) = X2
| ~ sP45(X2,X0,X1) ),
inference(cnf_transformation,[],[f498]) ).
fof(f1004,plain,
! [X2,X0,X1] :
( sP47(X0,X1,X2)
| ~ sP46(X2,X1,X0)
| ~ false_terminates(sK154(X0,X1,X2),X1,X0)
| and(sK155(X0,X1,X2),sK156(X0,X1,X2)) = X2
| neg(sK157(X0,X1,X2)) = X2
| ~ sP45(X2,X0,X1) ),
inference(cnf_transformation,[],[f498]) ).
fof(f1006,plain,
! [X2,X0,X1] :
( sP47(X0,X1,X2)
| ~ sP46(X2,X1,X0)
| and(sK153(X0,X1,X2),sK154(X0,X1,X2)) = X2
| ~ false_terminates(sK155(X0,X1,X2),X1,X0)
| neg(sK157(X0,X1,X2)) = X2
| ~ sP45(X2,X0,X1) ),
inference(cnf_transformation,[],[f498]) ).
fof(f1007,plain,
! [X2,X0,X1] :
( sP47(X0,X1,X2)
| ~ sP46(X2,X1,X0)
| and(sK153(X0,X1,X2),sK154(X0,X1,X2)) = X2
| and(sK155(X0,X1,X2),sK156(X0,X1,X2)) = X2
| ~ true_terminates(sK157(X0,X1,X2),X1,X0)
| ~ sP45(X2,X0,X1) ),
inference(cnf_transformation,[],[f498]) ).
fof(f1008,plain,
! [X2,X0,X1] :
( sP47(X0,X1,X2)
| ~ sP46(X2,X1,X0)
| and(sK153(X0,X1,X2),sK154(X0,X1,X2)) = X2
| and(sK155(X0,X1,X2),sK156(X0,X1,X2)) = X2
| neg(sK157(X0,X1,X2)) = X2
| ~ sP45(X2,X0,X1) ),
inference(cnf_transformation,[],[f498]) ).
fof(f1011,plain,
! [X2,X0,X1] :
( sP46(X0,X1,X2)
| ~ false_terminates(sK158(X0,X1,X2),X1,sK160(X0,X1,X2))
| ~ false_terminates(sK159(X0,X1,X2),sK160(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f501]) ).
fof(f1012,plain,
! [X2,X0,X1] :
( sP46(X0,X1,X2)
| ~ false_terminates(sK158(X0,X1,X2),X1,sK160(X0,X1,X2))
| ~ false_fails(sK158(X0,X1,X2),X1,sK160(X0,X1,X2)) ),
inference(cnf_transformation,[],[f501]) ).
fof(f1013,plain,
! [X2,X0,X1] :
( sP46(X0,X1,X2)
| or(sK158(X0,X1,X2),sK159(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f501]) ).
fof(f1017,plain,
! [X2,X0,X1] :
( sP45(X0,X1,X2)
| ~ member_terminates(p(sK161(X0,X1,X2)),X2)
| ~ gr(p(sK161(X0,X1,X2)))
| ~ gr(X2) ),
inference(cnf_transformation,[],[f504]) ).
fof(f1019,plain,
! [X2,X0,X1] :
( sP45(X0,X1,X2)
| p(sK161(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f504]) ).
fof(f1021,plain,
! [X2,X0,X1] :
( false_terminates(X0,X1,X2)
| ~ sP47(X2,X1,X0) ),
inference(cnf_transformation,[],[f505]) ).
fof(f1074,plain,
! [X2,X0,X1] :
( sP56(X0,X1,X2)
| ~ true_terminates(sK181(X0,X1,X2),X2,X1)
| ~ true_terminates(sK182(X0,X1,X2),X2,X1)
| ~ sP55(X0,X2,X1)
| neg(sK184(X0,X1,X2)) = X0
| ~ sP54(X0,X1,X2) ),
inference(cnf_transformation,[],[f531]) ).
fof(f1076,plain,
! [X2,X0,X1] :
( sP56(X0,X1,X2)
| ~ true_terminates(sK181(X0,X1,X2),X2,X1)
| or(sK182(X0,X1,X2),sK183(X0,X1,X2)) = X0
| ~ sP55(X0,X2,X1)
| neg(sK184(X0,X1,X2)) = X0
| ~ sP54(X0,X1,X2) ),
inference(cnf_transformation,[],[f531]) ).
fof(f1078,plain,
! [X2,X0,X1] :
( sP56(X0,X1,X2)
| or(sK180(X0,X1,X2),sK181(X0,X1,X2)) = X0
| ~ true_terminates(sK182(X0,X1,X2),X2,X1)
| ~ sP55(X0,X2,X1)
| neg(sK184(X0,X1,X2)) = X0
| ~ sP54(X0,X1,X2) ),
inference(cnf_transformation,[],[f531]) ).
fof(f1079,plain,
! [X2,X0,X1] :
( sP56(X0,X1,X2)
| or(sK180(X0,X1,X2),sK181(X0,X1,X2)) = X0
| or(sK182(X0,X1,X2),sK183(X0,X1,X2)) = X0
| ~ sP55(X0,X2,X1)
| ~ false_terminates(sK184(X0,X1,X2),X2,X1)
| ~ sP54(X0,X1,X2) ),
inference(cnf_transformation,[],[f531]) ).
fof(f1080,plain,
! [X2,X0,X1] :
( sP56(X0,X1,X2)
| or(sK180(X0,X1,X2),sK181(X0,X1,X2)) = X0
| or(sK182(X0,X1,X2),sK183(X0,X1,X2)) = X0
| ~ sP55(X0,X2,X1)
| neg(sK184(X0,X1,X2)) = X0
| ~ sP54(X0,X1,X2) ),
inference(cnf_transformation,[],[f531]) ).
fof(f1083,plain,
! [X2,X0,X1] :
( sP55(X0,X1,X2)
| ~ true_terminates(sK185(X0,X1,X2),X1,sK187(X0,X1,X2))
| ~ true_terminates(sK186(X0,X1,X2),sK187(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f534]) ).
fof(f1084,plain,
! [X2,X0,X1] :
( sP55(X0,X1,X2)
| ~ true_terminates(sK185(X0,X1,X2),X1,sK187(X0,X1,X2))
| ~ true_fails(sK185(X0,X1,X2),X1,sK187(X0,X1,X2)) ),
inference(cnf_transformation,[],[f534]) ).
fof(f1085,plain,
! [X2,X0,X1] :
( sP55(X0,X1,X2)
| and(sK185(X0,X1,X2),sK186(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f534]) ).
fof(f1089,plain,
! [X2,X0,X1] :
( sP54(X0,X1,X2)
| ~ member_terminates(neg(p(sK188(X0,X1,X2))),X2)
| ~ gr(neg(p(sK188(X0,X1,X2))))
| ~ gr(X2) ),
inference(cnf_transformation,[],[f537]) ).
fof(f1091,plain,
! [X2,X0,X1] :
( sP54(X0,X1,X2)
| p(sK188(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f537]) ).
fof(f1093,plain,
! [X2,X0,X1] :
( true_terminates(X0,X1,X2)
| ~ sP56(X0,X2,X1) ),
inference(cnf_transformation,[],[f538]) ).
fof(f1218,plain,
! [X0,X1] :
( member_terminates(X0,X1)
| ~ list_succeeds(X1) ),
inference(cnf_transformation,[],[f213]) ).
fof(f1225,plain,
! [X0] :
( list_succeeds(X0)
| ~ literal_list_succeeds(X0) ),
inference(cnf_transformation,[],[f221]) ).
fof(f1243,plain,
! [X2,X0,X1] :
( literal_list_succeeds(X2)
| ~ true_succeeds(X0,X1,X2)
| ~ literal_list_succeeds(X1) ),
inference(cnf_transformation,[],[f239]) ).
fof(f1244,plain,
! [X2,X0,X1] :
( literal_list_succeeds(X2)
| ~ false_succeeds(X0,X1,X2)
| ~ literal_list_succeeds(X1) ),
inference(cnf_transformation,[],[f241]) ).
fof(f1249,plain,
! [X2,X0,X1] :
( gr(X2)
| ~ true_succeeds(X0,X1,X2)
| ~ gr(X0)
| ~ gr(X1) ),
inference(cnf_transformation,[],[f247]) ).
fof(f1250,plain,
! [X2,X0,X1] :
( gr(X2)
| ~ false_succeeds(X0,X1,X2)
| ~ gr(X0)
| ~ gr(X1) ),
inference(cnf_transformation,[],[f249]) ).
fof(f1251,plain,
! [X4,X5] :
( sP64(sK238)
| sP63(sK238)
| false_terminates(sK241,X4,X5)
| ~ gr(sK241)
| ~ literal_list_succeeds(X4)
| ~ gr(X4)
| sK238 = p(sK242)
| ~ sP65 ),
inference(cnf_transformation,[],[f632]) ).
fof(f1252,plain,
! [X4,X5] :
( sP64(sK238)
| sP63(sK238)
| true_terminates(sK241,X4,X5)
| ~ gr(sK241)
| ~ literal_list_succeeds(X4)
| ~ gr(X4)
| sK238 = p(sK242)
| ~ sP65 ),
inference(cnf_transformation,[],[f632]) ).
fof(f1254,plain,
( sP64(sK238)
| sP63(sK238)
| sK238 = neg(sK241)
| sK238 = p(sK242)
| ~ sP65 ),
inference(cnf_transformation,[],[f632]) ).
fof(f1255,plain,
( gr(sK239)
| ~ sP65 ),
inference(cnf_transformation,[],[f632]) ).
fof(f1256,plain,
( literal_list_succeeds(sK239)
| ~ sP65 ),
inference(cnf_transformation,[],[f632]) ).
fof(f1257,plain,
( gr(sK238)
| ~ sP65 ),
inference(cnf_transformation,[],[f632]) ).
fof(f1258,plain,
( ~ true_terminates(sK238,sK239,sK240)
| ~ false_terminates(sK238,sK239,sK240)
| ~ sP65 ),
inference(cnf_transformation,[],[f632]) ).
fof(f1259,plain,
! [X0,X6,X5] :
( false_terminates(sK244(X0),X5,X6)
| ~ gr(sK244(X0))
| ~ literal_list_succeeds(X5)
| ~ gr(X5)
| ~ sP64(X0) ),
inference(cnf_transformation,[],[f634]) ).
fof(f1260,plain,
! [X0,X6,X5] :
( true_terminates(sK244(X0),X5,X6)
| ~ gr(sK244(X0))
| ~ literal_list_succeeds(X5)
| ~ gr(X5)
| ~ sP64(X0) ),
inference(cnf_transformation,[],[f634]) ).
fof(f1262,plain,
! [X3,X0,X4] :
( false_terminates(sK243(X0),X3,X4)
| ~ gr(sK243(X0))
| ~ literal_list_succeeds(X3)
| ~ gr(X3)
| ~ sP64(X0) ),
inference(cnf_transformation,[],[f634]) ).
fof(f1263,plain,
! [X3,X0,X4] :
( true_terminates(sK243(X0),X3,X4)
| ~ gr(sK243(X0))
| ~ literal_list_succeeds(X3)
| ~ gr(X3)
| ~ sP64(X0) ),
inference(cnf_transformation,[],[f634]) ).
fof(f1265,plain,
! [X0] :
( or(sK243(X0),sK244(X0)) = X0
| ~ sP64(X0) ),
inference(cnf_transformation,[],[f634]) ).
fof(f1266,plain,
! [X0,X6,X5] :
( false_terminates(sK246(X0),X5,X6)
| ~ gr(sK246(X0))
| ~ literal_list_succeeds(X5)
| ~ gr(X5)
| ~ sP63(X0) ),
inference(cnf_transformation,[],[f637]) ).
fof(f1267,plain,
! [X0,X6,X5] :
( true_terminates(sK246(X0),X5,X6)
| ~ gr(sK246(X0))
| ~ literal_list_succeeds(X5)
| ~ gr(X5)
| ~ sP63(X0) ),
inference(cnf_transformation,[],[f637]) ).
fof(f1269,plain,
! [X3,X0,X4] :
( false_terminates(sK245(X0),X3,X4)
| ~ gr(sK245(X0))
| ~ literal_list_succeeds(X3)
| ~ gr(X3)
| ~ sP63(X0) ),
inference(cnf_transformation,[],[f637]) ).
fof(f1270,plain,
! [X3,X0,X4] :
( true_terminates(sK245(X0),X3,X4)
| ~ gr(sK245(X0))
| ~ literal_list_succeeds(X3)
| ~ gr(X3)
| ~ sP63(X0) ),
inference(cnf_transformation,[],[f637]) ).
fof(f1272,plain,
! [X0] :
( and(sK245(X0),sK246(X0)) = X0
| ~ sP63(X0) ),
inference(cnf_transformation,[],[f637]) ).
fof(f1273,plain,
! [X2,X0,X1] :
( false_terminates(X0,X1,X2)
| ~ gr(X0)
| ~ literal_list_succeeds(X1)
| ~ gr(X1)
| ~ formula_succeeds(X0)
| sP65 ),
inference(cnf_transformation,[],[f638]) ).
fof(f1274,plain,
! [X2,X0,X1] :
( true_terminates(X0,X1,X2)
| ~ gr(X0)
| ~ literal_list_succeeds(X1)
| ~ gr(X1)
| ~ formula_succeeds(X0)
| sP65 ),
inference(cnf_transformation,[],[f638]) ).
fof(f1275,plain,
formula_succeeds(sK247),
inference(cnf_transformation,[],[f639]) ).
fof(f1276,plain,
gr(sK248),
inference(cnf_transformation,[],[f639]) ).
fof(f1277,plain,
literal_list_succeeds(sK248),
inference(cnf_transformation,[],[f639]) ).
fof(f1278,plain,
gr(sK247),
inference(cnf_transformation,[],[f639]) ).
fof(f1279,plain,
( ~ true_terminates(sK247,sK248,sK249)
| ~ false_terminates(sK247,sK248,sK249) ),
inference(cnf_transformation,[],[f639]) ).
fof(f1441,definition,
( spl250_1
<=> false_terminates(sK247,sK248,sK249) ),
introduced(definition,[new_symbols(definition,[spl250_1])],[avatar_definition]) ).
fof(f1443,plain,
( ~ false_terminates(sK247,sK248,sK249)
| spl250_1 ),
inference(avatar_component_clause,[],[f1441]) ).
fof(f1445,definition,
( spl250_2
<=> true_terminates(sK247,sK248,sK249) ),
introduced(definition,[new_symbols(definition,[spl250_2])],[avatar_definition]) ).
fof(f1447,plain,
( ~ true_terminates(sK247,sK248,sK249)
| spl250_2 ),
inference(avatar_component_clause,[],[f1445]) ).
fof(f1448,plain,
( ~ spl250_1
| ~ spl250_2 ),
inference(avatar_split_clause,[],[f1279,f1445,f1441]) ).
fof(f1450,plain,
( ~ gr(sK247)
| ~ literal_list_succeeds(sK248)
| ~ gr(sK248)
| ~ formula_succeeds(sK247)
| sP65
| spl250_1 ),
inference(resolution,[],[f1443,f1273]) ).
fof(f1456,plain,
( ~ literal_list_succeeds(sK248)
| ~ gr(sK248)
| ~ formula_succeeds(sK247)
| sP65
| spl250_1 ),
inference(forward_subsumption_resolution,[],[f1450,f1278]) ).
fof(f1457,plain,
( ~ gr(sK248)
| ~ formula_succeeds(sK247)
| sP65
| spl250_1 ),
inference(forward_subsumption_resolution,[],[f1456,f1277]) ).
fof(f1458,plain,
( ~ formula_succeeds(sK247)
| sP65
| spl250_1 ),
inference(forward_subsumption_resolution,[],[f1457,f1276]) ).
fof(f1459,plain,
( sP65
| spl250_1 ),
inference(forward_subsumption_resolution,[],[f1458,f1275]) ).
fof(f1528,definition,
( spl250_6
<=> sK238 = p(sK242) ),
introduced(definition,[new_symbols(definition,[spl250_6])],[avatar_definition]) ).
fof(f1529,plain,
( sK238 != p(sK242)
| spl250_6 ),
inference(avatar_component_clause,[],[f1528]) ).
fof(f1530,plain,
( sK238 = p(sK242)
| ~ spl250_6 ),
inference(avatar_component_clause,[],[f1528]) ).
fof(f1532,definition,
( spl250_7
<=> gr(sK241) ),
introduced(definition,[new_symbols(definition,[spl250_7])],[avatar_definition]) ).
fof(f1533,plain,
( gr(sK241)
| ~ spl250_7 ),
inference(avatar_component_clause,[],[f1532]) ).
fof(f1534,plain,
( ~ gr(sK241)
| spl250_7 ),
inference(avatar_component_clause,[],[f1532]) ).
fof(f1539,definition,
( spl250_9
<=> sP63(sK238) ),
introduced(definition,[new_symbols(definition,[spl250_9])],[avatar_definition]) ).
fof(f1540,plain,
( ~ sP63(sK238)
| spl250_9 ),
inference(avatar_component_clause,[],[f1539]) ).
fof(f1541,plain,
( sP63(sK238)
| ~ spl250_9 ),
inference(avatar_component_clause,[],[f1539]) ).
fof(f1543,definition,
( spl250_10
<=> sP64(sK238) ),
introduced(definition,[new_symbols(definition,[spl250_10])],[avatar_definition]) ).
fof(f1544,plain,
( ~ sP64(sK238)
| spl250_10 ),
inference(avatar_component_clause,[],[f1543]) ).
fof(f1545,plain,
( sP64(sK238)
| ~ spl250_10 ),
inference(avatar_component_clause,[],[f1543]) ).
fof(f1763,plain,
( gr(sK239)
| spl250_1 ),
inference(resolution,[],[f1459,f1255]) ).
fof(f1764,plain,
( literal_list_succeeds(sK239)
| spl250_1 ),
inference(resolution,[],[f1459,f1256]) ).
fof(f1765,plain,
( gr(sK238)
| spl250_1 ),
inference(resolution,[],[f1459,f1257]) ).
fof(f1766,plain,
( ~ true_terminates(sK238,sK239,sK240)
| ~ false_terminates(sK238,sK239,sK240)
| spl250_1 ),
inference(resolution,[],[f1459,f1258]) ).
fof(f1768,definition,
( spl250_32
<=> false_terminates(sK238,sK239,sK240) ),
introduced(definition,[new_symbols(definition,[spl250_32])],[avatar_definition]) ).
fof(f1770,plain,
( ~ false_terminates(sK238,sK239,sK240)
| spl250_32 ),
inference(avatar_component_clause,[],[f1768]) ).
fof(f1772,definition,
( spl250_33
<=> true_terminates(sK238,sK239,sK240) ),
introduced(definition,[new_symbols(definition,[spl250_33])],[avatar_definition]) ).
fof(f1773,plain,
( true_terminates(sK238,sK239,sK240)
| ~ spl250_33 ),
inference(avatar_component_clause,[],[f1772]) ).
fof(f1774,plain,
( ~ true_terminates(sK238,sK239,sK240)
| spl250_33 ),
inference(avatar_component_clause,[],[f1772]) ).
fof(f1775,plain,
( ~ spl250_32
| ~ spl250_33
| spl250_1 ),
inference(avatar_split_clause,[],[f1766,f1441,f1772,f1768]) ).
fof(f1777,definition,
( spl250_34
<=> sK238 = neg(sK241) ),
introduced(definition,[new_symbols(definition,[spl250_34])],[avatar_definition]) ).
fof(f1779,plain,
( sK238 = neg(sK241)
| ~ spl250_34 ),
inference(avatar_component_clause,[],[f1777]) ).
fof(f1786,plain,
( ~ sP56(sK238,sK240,sK239)
| spl250_33 ),
inference(resolution,[],[f1774,f1093]) ).
fof(f1796,plain,
( gr(neg(sK238))
| spl250_1 ),
inference(resolution,[],[f1765,f684]) ).
fof(f2005,definition,
( spl250_59
<=> sP65 ),
introduced(definition,[new_symbols(definition,[spl250_59])],[avatar_definition]) ).
fof(f2006,plain,
( ~ sP65
| spl250_59 ),
inference(avatar_component_clause,[],[f2005]) ).
fof(f2007,plain,
( sP65
| ~ spl250_59 ),
inference(avatar_component_clause,[],[f2005]) ).
fof(f2013,definition,
( spl250_61
<=> gr(sK239) ),
introduced(definition,[new_symbols(definition,[spl250_61])],[avatar_definition]) ).
fof(f2014,plain,
( gr(sK239)
| ~ spl250_61 ),
inference(avatar_component_clause,[],[f2013]) ).
fof(f2017,definition,
( spl250_62
<=> literal_list_succeeds(sK239) ),
introduced(definition,[new_symbols(definition,[spl250_62])],[avatar_definition]) ).
fof(f2018,plain,
( literal_list_succeeds(sK239)
| ~ spl250_62 ),
inference(avatar_component_clause,[],[f2017]) ).
fof(f2021,definition,
( spl250_63
<=> gr(sK238) ),
introduced(definition,[new_symbols(definition,[spl250_63])],[avatar_definition]) ).
fof(f2022,plain,
( gr(sK238)
| ~ spl250_63 ),
inference(avatar_component_clause,[],[f2021]) ).
fof(f2023,plain,
( ~ gr(sK238)
| spl250_63 ),
inference(avatar_component_clause,[],[f2021]) ).
fof(f2136,definition,
( spl250_71
<=> gr(neg(sK238)) ),
introduced(definition,[new_symbols(definition,[spl250_71])],[avatar_definition]) ).
fof(f2138,plain,
( gr(neg(sK238))
| ~ spl250_71 ),
inference(avatar_component_clause,[],[f2136]) ).
fof(f2156,plain,
( ~ true_terminates(sK181(sK238,sK240,sK239),sK239,sK240)
| ~ true_terminates(sK182(sK238,sK240,sK239),sK239,sK240)
| ~ sP55(sK238,sK239,sK240)
| sK238 = neg(sK184(sK238,sK240,sK239))
| ~ sP54(sK238,sK240,sK239)
| spl250_33 ),
inference(resolution,[],[f1786,f1074]) ).
fof(f2158,plain,
( ~ true_terminates(sK181(sK238,sK240,sK239),sK239,sK240)
| sK238 = or(sK182(sK238,sK240,sK239),sK183(sK238,sK240,sK239))
| ~ sP55(sK238,sK239,sK240)
| sK238 = neg(sK184(sK238,sK240,sK239))
| ~ sP54(sK238,sK240,sK239)
| spl250_33 ),
inference(resolution,[],[f1786,f1076]) ).
fof(f2162,plain,
( sK238 = or(sK180(sK238,sK240,sK239),sK181(sK238,sK240,sK239))
| sK238 = or(sK182(sK238,sK240,sK239),sK183(sK238,sK240,sK239))
| ~ sP55(sK238,sK239,sK240)
| sK238 = neg(sK184(sK238,sK240,sK239))
| ~ sP54(sK238,sK240,sK239)
| spl250_33 ),
inference(resolution,[],[f1786,f1080]) ).
fof(f2165,definition,
( spl250_75
<=> sP54(sK238,sK240,sK239) ),
introduced(definition,[new_symbols(definition,[spl250_75])],[avatar_definition]) ).
fof(f2166,plain,
( sP54(sK238,sK240,sK239)
| ~ spl250_75 ),
inference(avatar_component_clause,[],[f2165]) ).
fof(f2167,plain,
( ~ sP54(sK238,sK240,sK239)
| spl250_75 ),
inference(avatar_component_clause,[],[f2165]) ).
fof(f2169,definition,
( spl250_76
<=> sK238 = neg(sK184(sK238,sK240,sK239)) ),
introduced(definition,[new_symbols(definition,[spl250_76])],[avatar_definition]) ).
fof(f2171,plain,
( sK238 = neg(sK184(sK238,sK240,sK239))
| ~ spl250_76 ),
inference(avatar_component_clause,[],[f2169]) ).
fof(f2173,definition,
( spl250_77
<=> sP55(sK238,sK239,sK240) ),
introduced(definition,[new_symbols(definition,[spl250_77])],[avatar_definition]) ).
fof(f2174,plain,
( sP55(sK238,sK239,sK240)
| ~ spl250_77 ),
inference(avatar_component_clause,[],[f2173]) ).
fof(f2175,plain,
( ~ sP55(sK238,sK239,sK240)
| spl250_77 ),
inference(avatar_component_clause,[],[f2173]) ).
fof(f2177,definition,
( spl250_78
<=> sK238 = or(sK182(sK238,sK240,sK239),sK183(sK238,sK240,sK239)) ),
introduced(definition,[new_symbols(definition,[spl250_78])],[avatar_definition]) ).
fof(f2178,plain,
( sK238 != or(sK182(sK238,sK240,sK239),sK183(sK238,sK240,sK239))
| spl250_78 ),
inference(avatar_component_clause,[],[f2177]) ).
fof(f2179,plain,
( sK238 = or(sK182(sK238,sK240,sK239),sK183(sK238,sK240,sK239))
| ~ spl250_78 ),
inference(avatar_component_clause,[],[f2177]) ).
fof(f2181,definition,
( spl250_79
<=> sK238 = or(sK180(sK238,sK240,sK239),sK181(sK238,sK240,sK239)) ),
introduced(definition,[new_symbols(definition,[spl250_79])],[avatar_definition]) ).
fof(f2182,plain,
( sK238 != or(sK180(sK238,sK240,sK239),sK181(sK238,sK240,sK239))
| spl250_79 ),
inference(avatar_component_clause,[],[f2181]) ).
fof(f2183,plain,
( sK238 = or(sK180(sK238,sK240,sK239),sK181(sK238,sK240,sK239))
| ~ spl250_79 ),
inference(avatar_component_clause,[],[f2181]) ).
fof(f2184,plain,
( ~ spl250_75
| spl250_76
| ~ spl250_77
| spl250_78
| spl250_79
| spl250_33 ),
inference(avatar_split_clause,[],[f2162,f1772,f2181,f2177,f2173,f2169,f2165]) ).
fof(f2191,definition,
( spl250_81
<=> true_terminates(sK182(sK238,sK240,sK239),sK239,sK240) ),
introduced(definition,[new_symbols(definition,[spl250_81])],[avatar_definition]) ).
fof(f2192,plain,
( true_terminates(sK182(sK238,sK240,sK239),sK239,sK240)
| ~ spl250_81 ),
inference(avatar_component_clause,[],[f2191]) ).
fof(f2193,plain,
( ~ true_terminates(sK182(sK238,sK240,sK239),sK239,sK240)
| spl250_81 ),
inference(avatar_component_clause,[],[f2191]) ).
fof(f2197,definition,
( spl250_82
<=> true_terminates(sK181(sK238,sK240,sK239),sK239,sK240) ),
introduced(definition,[new_symbols(definition,[spl250_82])],[avatar_definition]) ).
fof(f2199,plain,
( ~ true_terminates(sK181(sK238,sK240,sK239),sK239,sK240)
| spl250_82 ),
inference(avatar_component_clause,[],[f2197]) ).
fof(f2200,plain,
( ~ spl250_75
| spl250_76
| ~ spl250_77
| spl250_78
| ~ spl250_82
| spl250_33 ),
inference(avatar_split_clause,[],[f2158,f1772,f2197,f2177,f2173,f2169,f2165]) ).
fof(f2202,plain,
( ~ spl250_75
| spl250_76
| ~ spl250_77
| ~ spl250_81
| ~ spl250_82
| spl250_33 ),
inference(avatar_split_clause,[],[f2156,f1772,f2197,f2191,f2173,f2169,f2165]) ).
fof(f2214,plain,
( sK238 != sK238
| sP64(sK238)
| sP63(sK238)
| sK238 = neg(sK241)
| ~ sP65
| spl250_6 ),
inference(superposition,[],[f1529,f1254]) ).
fof(f2215,plain,
( sP64(sK238)
| sP63(sK238)
| sK238 = neg(sK241)
| ~ sP65
| spl250_6 ),
inference(trivial_inequality_removal,[],[f2214]) ).
fof(f2219,plain,
( sP64(sK238)
| sP63(sK238)
| sK238 = neg(sK241)
| spl250_6
| ~ spl250_59 ),
inference(forward_subsumption_resolution,[],[f2215,f2007]) ).
fof(f2221,plain,
( spl250_34
| spl250_9
| spl250_10
| spl250_6
| ~ spl250_59 ),
inference(avatar_split_clause,[],[f2219,f2005,f1528,f1543,f1539,f1777]) ).
fof(f2230,plain,
( ~ gr(sK238)
| gr(sK241)
| ~ spl250_34 ),
inference(superposition,[],[f685,f1779]) ).
fof(f2304,plain,
( ~ gr(sK238)
| spl250_7
| ~ spl250_34 ),
inference(forward_subsumption_resolution,[],[f2230,f1534]) ).
fof(f2305,plain,
( ~ spl250_63
| spl250_7
| ~ spl250_34 ),
inference(avatar_split_clause,[],[f2304,f1777,f1532,f2021]) ).
fof(f2317,plain,
( ~ sP65
| spl250_63 ),
inference(resolution,[],[f2023,f1257]) ).
fof(f2333,plain,
( $false
| ~ spl250_59
| spl250_63 ),
inference(forward_subsumption_resolution,[],[f2317,f2007]) ).
fof(f2334,plain,
( ~ spl250_59
| spl250_63 ),
inference(avatar_contradiction_clause,[],[f2333]) ).
fof(f2398,plain,
( ~ gr(sK247)
| ~ literal_list_succeeds(sK248)
| ~ gr(sK248)
| ~ formula_succeeds(sK247)
| sP65
| spl250_2 ),
inference(resolution,[],[f1447,f1274]) ).
fof(f2404,plain,
( ~ literal_list_succeeds(sK248)
| ~ gr(sK248)
| ~ formula_succeeds(sK247)
| sP65
| spl250_2 ),
inference(forward_subsumption_resolution,[],[f2398,f1278]) ).
fof(f2405,plain,
( ~ gr(sK248)
| ~ formula_succeeds(sK247)
| sP65
| spl250_2 ),
inference(forward_subsumption_resolution,[],[f2404,f1277]) ).
fof(f2406,plain,
( ~ formula_succeeds(sK247)
| sP65
| spl250_2 ),
inference(forward_subsumption_resolution,[],[f2405,f1276]) ).
fof(f2407,plain,
( sP65
| spl250_2 ),
inference(forward_subsumption_resolution,[],[f2406,f1275]) ).
fof(f2410,plain,
( spl250_71
| spl250_1 ),
inference(avatar_split_clause,[],[f1796,f1441,f2136]) ).
fof(f2412,plain,
( spl250_61
| spl250_1 ),
inference(avatar_split_clause,[],[f1763,f1441,f2013]) ).
fof(f2413,plain,
( spl250_62
| spl250_1 ),
inference(avatar_split_clause,[],[f1764,f1441,f2017]) ).
fof(f2414,plain,
( $false
| spl250_1
| spl250_59 ),
inference(forward_subsumption_resolution,[],[f1459,f2006]) ).
fof(f2415,plain,
( spl250_1
| spl250_59 ),
inference(avatar_contradiction_clause,[],[f2414]) ).
fof(f2416,plain,
( spl250_59
| spl250_2 ),
inference(avatar_split_clause,[],[f2407,f1445,f2005]) ).
fof(f2438,plain,
( gr(neg(sK238))
| ~ spl250_63 ),
inference(resolution,[],[f2022,f684]) ).
fof(f2468,plain,
( spl250_71
| ~ spl250_63 ),
inference(avatar_split_clause,[],[f2438,f2021,f2136]) ).
fof(f2551,plain,
( ! [X0,X1] :
( true_terminates(sK246(sK238),X0,X1)
| ~ gr(sK246(sK238))
| ~ literal_list_succeeds(X0)
| ~ gr(X0) )
| ~ spl250_9 ),
inference(resolution,[],[f1541,f1267]) ).
fof(f2556,plain,
( sK238 = and(sK245(sK238),sK246(sK238))
| ~ spl250_9 ),
inference(resolution,[],[f1541,f1272]) ).
fof(f2558,definition,
( spl250_104
<=> gr(sK245(sK238)) ),
introduced(definition,[new_symbols(definition,[spl250_104])],[avatar_definition]) ).
fof(f2559,plain,
( gr(sK245(sK238))
| ~ spl250_104 ),
inference(avatar_component_clause,[],[f2558]) ).
fof(f2560,plain,
( ~ gr(sK245(sK238))
| spl250_104 ),
inference(avatar_component_clause,[],[f2558]) ).
fof(f2570,definition,
( spl250_107
<=> gr(sK246(sK238)) ),
introduced(definition,[new_symbols(definition,[spl250_107])],[avatar_definition]) ).
fof(f2571,plain,
( gr(sK246(sK238))
| ~ spl250_107 ),
inference(avatar_component_clause,[],[f2570]) ).
fof(f2572,plain,
( ~ gr(sK246(sK238))
| spl250_107 ),
inference(avatar_component_clause,[],[f2570]) ).
fof(f2574,definition,
( spl250_108
<=> ! [X0,X1] :
( true_terminates(sK246(sK238),X0,X1)
| ~ gr(X0)
| ~ literal_list_succeeds(X0) ) ),
introduced(definition,[new_symbols(definition,[spl250_108])],[avatar_definition]) ).
fof(f2575,plain,
( ! [X0,X1] :
( true_terminates(sK246(sK238),X0,X1)
| ~ gr(X0)
| ~ literal_list_succeeds(X0) )
| ~ spl250_108 ),
inference(avatar_component_clause,[],[f2574]) ).
fof(f2576,plain,
( ~ spl250_107
| spl250_108
| ~ spl250_9 ),
inference(avatar_split_clause,[],[f2551,f1539,f2574,f2570]) ).
fof(f2585,plain,
( ! [X0] : p(X0) != sK238
| ~ spl250_9 ),
inference(superposition,[],[f666,f2556]) ).
fof(f2586,plain,
( ! [X0] : neg(X0) != sK238
| ~ spl250_9 ),
inference(superposition,[],[f669,f2556]) ).
fof(f2588,plain,
( ! [X0,X1] :
( and(X0,X1) != sK238
| sK246(sK238) = X1 )
| ~ spl250_9 ),
inference(superposition,[],[f671,f2556]) ).
fof(f2590,plain,
( ! [X0,X1] :
( and(X0,X1) != sK238
| sK245(sK238) = X0 )
| ~ spl250_9 ),
inference(superposition,[],[f672,f2556]) ).
fof(f2591,plain,
( ! [X0,X1] : or(X0,X1) != sK238
| ~ spl250_9 ),
inference(superposition,[],[f673,f2556]) ).
fof(f2593,plain,
( ~ gr(sK238)
| gr(sK246(sK238))
| ~ spl250_9 ),
inference(superposition,[],[f687,f2556]) ).
fof(f2594,plain,
( ~ gr(sK238)
| gr(sK245(sK238))
| ~ spl250_9 ),
inference(superposition,[],[f688,f2556]) ).
fof(f2651,plain,
( gr(sK245(sK238))
| ~ spl250_9
| ~ spl250_63 ),
inference(forward_subsumption_resolution,[],[f2594,f2022]) ).
fof(f2652,plain,
( gr(sK246(sK238))
| ~ spl250_9
| ~ spl250_63 ),
inference(forward_subsumption_resolution,[],[f2593,f2022]) ).
fof(f2654,plain,
( $false
| ~ spl250_9
| ~ spl250_63
| spl250_104 ),
inference(forward_subsumption_resolution,[],[f2651,f2560]) ).
fof(f2655,plain,
( ~ spl250_9
| ~ spl250_63
| spl250_104 ),
inference(avatar_contradiction_clause,[],[f2654]) ).
fof(f2656,plain,
( $false
| ~ spl250_9
| ~ spl250_63
| spl250_107 ),
inference(forward_subsumption_resolution,[],[f2652,f2572]) ).
fof(f2657,plain,
( ~ spl250_9
| ~ spl250_63
| spl250_107 ),
inference(avatar_contradiction_clause,[],[f2656]) ).
fof(f3419,plain,
( sK238 = p(sK188(sK238,sK240,sK239))
| spl250_75 ),
inference(resolution,[],[f2167,f1091]) ).
fof(f3421,plain,
( $false
| ~ spl250_9
| spl250_75 ),
inference(forward_subsumption_resolution,[],[f3419,f2585]) ).
fof(f3422,plain,
( ~ spl250_9
| spl250_75 ),
inference(avatar_contradiction_clause,[],[f3421]) ).
fof(f4968,plain,
( gr(sK239)
| ~ spl250_59 ),
inference(resolution,[],[f2007,f1255]) ).
fof(f4969,plain,
( literal_list_succeeds(sK239)
| ~ spl250_59 ),
inference(resolution,[],[f2007,f1256]) ).
fof(f4971,plain,
( ~ true_terminates(sK238,sK239,sK240)
| ~ false_terminates(sK238,sK239,sK240)
| ~ spl250_59 ),
inference(resolution,[],[f2007,f1258]) ).
fof(f12336,plain,
( spl250_62
| ~ spl250_59 ),
inference(avatar_split_clause,[],[f4969,f2005,f2017]) ).
fof(f12337,plain,
( spl250_61
| ~ spl250_59 ),
inference(avatar_split_clause,[],[f4968,f2005,f2013]) ).
fof(f12378,plain,
( ! [X0] :
( sP64(sK238)
| sP63(sK238)
| false_terminates(sK241,sK239,X0)
| ~ gr(sK241)
| ~ literal_list_succeeds(sK239)
| sK238 = p(sK242)
| ~ sP65 )
| ~ spl250_61 ),
inference(resolution,[],[f2014,f1251]) ).
fof(f12379,plain,
( ! [X0] :
( sP64(sK238)
| sP63(sK238)
| true_terminates(sK241,sK239,X0)
| ~ gr(sK241)
| ~ literal_list_succeeds(sK239)
| sK238 = p(sK242)
| ~ sP65 )
| ~ spl250_61 ),
inference(resolution,[],[f2014,f1252]) ).
fof(f12405,plain,
( list_succeeds(sK239)
| ~ spl250_62 ),
inference(resolution,[],[f2018,f1225]) ).
fof(f12438,plain,
( sP56(sK238,sK240,sK239)
| sK238 = or(sK180(sK238,sK240,sK239),sK181(sK238,sK240,sK239))
| sK238 = or(sK182(sK238,sK240,sK239),sK183(sK238,sK240,sK239))
| ~ sP55(sK238,sK239,sK240)
| sK238 = neg(sK184(sK238,sK240,sK239))
| ~ spl250_75 ),
inference(resolution,[],[f2166,f1080]) ).
fof(f12475,plain,
( sK238 = and(sK185(sK238,sK239,sK240),sK186(sK238,sK239,sK240))
| spl250_77 ),
inference(resolution,[],[f2175,f1085]) ).
fof(f12495,plain,
( ! [X0] : p(X0) != sK238
| spl250_77 ),
inference(superposition,[],[f666,f12475]) ).
fof(f12496,plain,
( ! [X0] : neg(X0) != sK238
| spl250_77 ),
inference(superposition,[],[f669,f12475]) ).
fof(f12533,plain,
( sK238 != sK238
| sK246(sK238) = sK186(sK238,sK239,sK240)
| ~ spl250_9
| spl250_77 ),
inference(superposition,[],[f2588,f12475]) ).
fof(f12534,plain,
( sK238 != sK238
| sK245(sK238) = sK185(sK238,sK239,sK240)
| ~ spl250_9
| spl250_77 ),
inference(superposition,[],[f2590,f12475]) ).
fof(f12537,plain,
( sK245(sK238) = sK185(sK238,sK239,sK240)
| ~ spl250_9
| spl250_77 ),
inference(trivial_inequality_removal,[],[f12534]) ).
fof(f12538,plain,
( sK246(sK238) = sK186(sK238,sK239,sK240)
| ~ spl250_9
| spl250_77 ),
inference(trivial_inequality_removal,[],[f12533]) ).
fof(f12587,plain,
( ~ true_terminates(sK245(sK238),sK239,sK187(sK238,sK239,sK240))
| sP55(sK238,sK239,sK240)
| ~ true_terminates(sK186(sK238,sK239,sK240),sK187(sK238,sK239,sK240),sK240)
| ~ spl250_9
| spl250_77 ),
inference(superposition,[],[f1083,f12537]) ).
fof(f12588,plain,
( ~ true_fails(sK245(sK238),sK239,sK187(sK238,sK239,sK240))
| sP55(sK238,sK239,sK240)
| ~ true_terminates(sK245(sK238),sK239,sK187(sK238,sK239,sK240))
| ~ spl250_9
| spl250_77 ),
inference(superposition,[],[f1084,f12537]) ).
fof(f12593,plain,
( ~ true_fails(sK245(sK238),sK239,sK187(sK238,sK239,sK240))
| ~ true_terminates(sK245(sK238),sK239,sK187(sK238,sK239,sK240))
| ~ spl250_9
| spl250_77 ),
inference(forward_subsumption_resolution,[],[f12588,f2175]) ).
fof(f12594,plain,
( ~ true_terminates(sK245(sK238),sK239,sK187(sK238,sK239,sK240))
| ~ true_terminates(sK186(sK238,sK239,sK240),sK187(sK238,sK239,sK240),sK240)
| ~ spl250_9
| spl250_77 ),
inference(forward_subsumption_resolution,[],[f12587,f2175]) ).
fof(f12598,definition,
( spl250_590
<=> true_fails(sK245(sK238),sK239,sK187(sK238,sK239,sK240)) ),
introduced(definition,[new_symbols(definition,[spl250_590])],[avatar_definition]) ).
fof(f12600,plain,
( ~ true_fails(sK245(sK238),sK239,sK187(sK238,sK239,sK240))
| spl250_590 ),
inference(avatar_component_clause,[],[f12598]) ).
fof(f12602,definition,
( spl250_591
<=> true_terminates(sK245(sK238),sK239,sK187(sK238,sK239,sK240)) ),
introduced(definition,[new_symbols(definition,[spl250_591])],[avatar_definition]) ).
fof(f12603,plain,
( true_terminates(sK245(sK238),sK239,sK187(sK238,sK239,sK240))
| ~ spl250_591 ),
inference(avatar_component_clause,[],[f12602]) ).
fof(f12604,plain,
( ~ true_terminates(sK245(sK238),sK239,sK187(sK238,sK239,sK240))
| spl250_591 ),
inference(avatar_component_clause,[],[f12602]) ).
fof(f12606,plain,
( ~ spl250_591
| ~ spl250_590
| ~ spl250_9
| spl250_77 ),
inference(avatar_split_clause,[],[f12593,f2173,f1539,f12598,f12602]) ).
fof(f12607,plain,
( ~ true_terminates(sK246(sK238),sK187(sK238,sK239,sK240),sK240)
| ~ true_terminates(sK245(sK238),sK239,sK187(sK238,sK239,sK240))
| ~ spl250_9
| spl250_77 ),
inference(forward_demodulation,[],[f12594,f12538]) ).
fof(f12609,definition,
( spl250_592
<=> true_terminates(sK246(sK238),sK187(sK238,sK239,sK240),sK240) ),
introduced(definition,[new_symbols(definition,[spl250_592])],[avatar_definition]) ).
fof(f12611,plain,
( ~ true_terminates(sK246(sK238),sK187(sK238,sK239,sK240),sK240)
| spl250_592 ),
inference(avatar_component_clause,[],[f12609]) ).
fof(f12612,plain,
( ~ spl250_591
| ~ spl250_592
| ~ spl250_9
| spl250_77 ),
inference(avatar_split_clause,[],[f12607,f2173,f1539,f12609,f12602]) ).
fof(f12613,plain,
( ~ gr(sK245(sK238))
| ~ literal_list_succeeds(sK239)
| ~ gr(sK239)
| ~ sP63(sK238)
| spl250_591 ),
inference(resolution,[],[f12604,f1270]) ).
fof(f12623,plain,
( ~ literal_list_succeeds(sK239)
| ~ gr(sK239)
| ~ sP63(sK238)
| ~ spl250_104
| spl250_591 ),
inference(forward_subsumption_resolution,[],[f12613,f2559]) ).
fof(f12626,plain,
( ~ gr(sK239)
| ~ sP63(sK238)
| ~ spl250_62
| ~ spl250_104
| spl250_591 ),
inference(forward_subsumption_resolution,[],[f12623,f2018]) ).
fof(f12627,plain,
( ~ sP63(sK238)
| ~ spl250_61
| ~ spl250_62
| ~ spl250_104
| spl250_591 ),
inference(forward_subsumption_resolution,[],[f12626,f2014]) ).
fof(f12628,plain,
( $false
| ~ spl250_9
| ~ spl250_61
| ~ spl250_62
| ~ spl250_104
| spl250_591 ),
inference(forward_subsumption_resolution,[],[f12627,f1541]) ).
fof(f12629,plain,
( ~ spl250_9
| ~ spl250_61
| ~ spl250_62
| ~ spl250_104
| spl250_591 ),
inference(avatar_contradiction_clause,[],[f12628]) ).
fof(f12631,plain,
( true_succeeds(sK245(sK238),sK239,sK187(sK238,sK239,sK240))
| true_fails(sK245(sK238),sK239,sK187(sK238,sK239,sK240))
| ~ spl250_591 ),
inference(resolution,[],[f12603,f699]) ).
fof(f12632,plain,
( true_succeeds(sK245(sK238),sK239,sK187(sK238,sK239,sK240))
| spl250_590
| ~ spl250_591 ),
inference(forward_subsumption_resolution,[],[f12631,f12600]) ).
fof(f12639,plain,
( literal_list_succeeds(sK187(sK238,sK239,sK240))
| ~ literal_list_succeeds(sK239)
| spl250_590
| ~ spl250_591 ),
inference(resolution,[],[f12632,f1243]) ).
fof(f12642,plain,
( gr(sK187(sK238,sK239,sK240))
| ~ gr(sK245(sK238))
| ~ gr(sK239)
| spl250_590
| ~ spl250_591 ),
inference(resolution,[],[f12632,f1249]) ).
fof(f12648,plain,
( gr(sK187(sK238,sK239,sK240))
| ~ gr(sK239)
| ~ spl250_104
| spl250_590
| ~ spl250_591 ),
inference(forward_subsumption_resolution,[],[f12642,f2559]) ).
fof(f12650,plain,
( literal_list_succeeds(sK187(sK238,sK239,sK240))
| ~ spl250_62
| spl250_590
| ~ spl250_591 ),
inference(forward_subsumption_resolution,[],[f12639,f2018]) ).
fof(f12654,plain,
( gr(sK187(sK238,sK239,sK240))
| ~ spl250_61
| ~ spl250_104
| spl250_590
| ~ spl250_591 ),
inference(forward_subsumption_resolution,[],[f12648,f2014]) ).
fof(f12678,plain,
( ~ gr(sK187(sK238,sK239,sK240))
| ~ literal_list_succeeds(sK187(sK238,sK239,sK240))
| ~ spl250_108
| spl250_592 ),
inference(resolution,[],[f12611,f2575]) ).
fof(f12686,plain,
( ~ literal_list_succeeds(sK187(sK238,sK239,sK240))
| ~ spl250_61
| ~ spl250_104
| ~ spl250_108
| spl250_590
| ~ spl250_591
| spl250_592 ),
inference(forward_subsumption_resolution,[],[f12678,f12654]) ).
fof(f12688,plain,
( $false
| ~ spl250_61
| ~ spl250_62
| ~ spl250_104
| ~ spl250_108
| spl250_590
| ~ spl250_591
| spl250_592 ),
inference(forward_subsumption_resolution,[],[f12686,f12650]) ).
fof(f12689,plain,
( ~ spl250_61
| ~ spl250_62
| ~ spl250_104
| ~ spl250_108
| spl250_590
| ~ spl250_591
| spl250_592 ),
inference(avatar_contradiction_clause,[],[f12688]) ).
fof(f12696,plain,
( sK238 = or(sK180(sK238,sK240,sK239),sK181(sK238,sK240,sK239))
| sK238 = or(sK182(sK238,sK240,sK239),sK183(sK238,sK240,sK239))
| ~ sP55(sK238,sK239,sK240)
| sK238 = neg(sK184(sK238,sK240,sK239))
| spl250_33
| ~ spl250_75 ),
inference(forward_subsumption_resolution,[],[f12438,f1786]) ).
fof(f12700,plain,
( sK238 = or(sK180(sK238,sK240,sK239),sK181(sK238,sK240,sK239))
| ~ sP55(sK238,sK239,sK240)
| sK238 = neg(sK184(sK238,sK240,sK239))
| ~ spl250_9
| spl250_33
| ~ spl250_75 ),
inference(forward_subsumption_resolution,[],[f12696,f2591]) ).
fof(f12704,plain,
( ~ sP55(sK238,sK239,sK240)
| sK238 = neg(sK184(sK238,sK240,sK239))
| ~ spl250_9
| spl250_33
| ~ spl250_75 ),
inference(forward_subsumption_resolution,[],[f12700,f2591]) ).
fof(f12708,plain,
( sK238 = neg(sK184(sK238,sK240,sK239))
| ~ spl250_9
| spl250_33
| ~ spl250_75
| ~ spl250_77 ),
inference(forward_subsumption_resolution,[],[f12704,f2174]) ).
fof(f12712,plain,
( $false
| ~ spl250_9
| spl250_33
| ~ spl250_75
| ~ spl250_77 ),
inference(forward_subsumption_resolution,[],[f12708,f2586]) ).
fof(f12713,plain,
( ~ spl250_9
| spl250_33
| ~ spl250_75
| ~ spl250_77 ),
inference(avatar_contradiction_clause,[],[f12712]) ).
fof(f12716,plain,
( ~ false_terminates(sK238,sK239,sK240)
| ~ spl250_33
| ~ spl250_59 ),
inference(forward_subsumption_resolution,[],[f4971,f1773]) ).
fof(f12721,plain,
( ~ spl250_32
| ~ spl250_33
| ~ spl250_59 ),
inference(avatar_split_clause,[],[f12716,f2005,f1772,f1768]) ).
fof(f12730,definition,
( spl250_593
<=> sP56(sK238,sK240,sK239) ),
introduced(definition,[new_symbols(definition,[spl250_593])],[avatar_definition]) ).
fof(f12731,plain,
( ~ sP56(sK238,sK240,sK239)
| spl250_593 ),
inference(avatar_component_clause,[],[f12730]) ).
fof(f12781,plain,
( ~ sP47(sK240,sK239,sK238)
| spl250_32 ),
inference(resolution,[],[f1770,f1021]) ).
fof(f12838,plain,
( ~ sP46(sK238,sK239,sK240)
| ~ false_terminates(sK154(sK240,sK239,sK238),sK239,sK240)
| ~ false_terminates(sK155(sK240,sK239,sK238),sK239,sK240)
| sK238 = neg(sK157(sK240,sK239,sK238))
| ~ sP45(sK238,sK240,sK239)
| spl250_32 ),
inference(resolution,[],[f12781,f1002]) ).
fof(f12840,plain,
( ~ sP46(sK238,sK239,sK240)
| ~ false_terminates(sK154(sK240,sK239,sK238),sK239,sK240)
| sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| sK238 = neg(sK157(sK240,sK239,sK238))
| ~ sP45(sK238,sK240,sK239)
| spl250_32 ),
inference(resolution,[],[f12781,f1004]) ).
fof(f12842,plain,
( ~ sP46(sK238,sK239,sK240)
| sK238 = and(sK153(sK240,sK239,sK238),sK154(sK240,sK239,sK238))
| ~ false_terminates(sK155(sK240,sK239,sK238),sK239,sK240)
| sK238 = neg(sK157(sK240,sK239,sK238))
| ~ sP45(sK238,sK240,sK239)
| spl250_32 ),
inference(resolution,[],[f12781,f1006]) ).
fof(f12844,plain,
( ~ sP46(sK238,sK239,sK240)
| sK238 = and(sK153(sK240,sK239,sK238),sK154(sK240,sK239,sK238))
| sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| sK238 = neg(sK157(sK240,sK239,sK238))
| ~ sP45(sK238,sK240,sK239)
| spl250_32 ),
inference(resolution,[],[f12781,f1008]) ).
fof(f12846,plain,
( ~ sP46(sK238,sK239,sK240)
| sK238 = and(sK153(sK240,sK239,sK238),sK154(sK240,sK239,sK238))
| sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| ~ sP45(sK238,sK240,sK239)
| ~ spl250_9
| spl250_32 ),
inference(forward_subsumption_resolution,[],[f12844,f2586]) ).
fof(f12848,definition,
( spl250_598
<=> sP45(sK238,sK240,sK239) ),
introduced(definition,[new_symbols(definition,[spl250_598])],[avatar_definition]) ).
fof(f12849,plain,
( sP45(sK238,sK240,sK239)
| ~ spl250_598 ),
inference(avatar_component_clause,[],[f12848]) ).
fof(f12850,plain,
( ~ sP45(sK238,sK240,sK239)
| spl250_598 ),
inference(avatar_component_clause,[],[f12848]) ).
fof(f12856,definition,
( spl250_600
<=> sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238)) ),
introduced(definition,[new_symbols(definition,[spl250_600])],[avatar_definition]) ).
fof(f12857,plain,
( sK238 != and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| spl250_600 ),
inference(avatar_component_clause,[],[f12856]) ).
fof(f12858,plain,
( sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| ~ spl250_600 ),
inference(avatar_component_clause,[],[f12856]) ).
fof(f12860,definition,
( spl250_601
<=> sK238 = and(sK153(sK240,sK239,sK238),sK154(sK240,sK239,sK238)) ),
introduced(definition,[new_symbols(definition,[spl250_601])],[avatar_definition]) ).
fof(f12861,plain,
( sK238 != and(sK153(sK240,sK239,sK238),sK154(sK240,sK239,sK238))
| spl250_601 ),
inference(avatar_component_clause,[],[f12860]) ).
fof(f12862,plain,
( sK238 = and(sK153(sK240,sK239,sK238),sK154(sK240,sK239,sK238))
| ~ spl250_601 ),
inference(avatar_component_clause,[],[f12860]) ).
fof(f12864,definition,
( spl250_602
<=> sP46(sK238,sK239,sK240) ),
introduced(definition,[new_symbols(definition,[spl250_602])],[avatar_definition]) ).
fof(f12865,plain,
( sP46(sK238,sK239,sK240)
| ~ spl250_602 ),
inference(avatar_component_clause,[],[f12864]) ).
fof(f12866,plain,
( ~ sP46(sK238,sK239,sK240)
| spl250_602 ),
inference(avatar_component_clause,[],[f12864]) ).
fof(f12868,plain,
( ~ sP46(sK238,sK239,sK240)
| sK238 = and(sK153(sK240,sK239,sK238),sK154(sK240,sK239,sK238))
| ~ false_terminates(sK155(sK240,sK239,sK238),sK239,sK240)
| ~ sP45(sK238,sK240,sK239)
| ~ spl250_9
| spl250_32 ),
inference(forward_subsumption_resolution,[],[f12842,f2586]) ).
fof(f12870,definition,
( spl250_603
<=> false_terminates(sK155(sK240,sK239,sK238),sK239,sK240) ),
introduced(definition,[new_symbols(definition,[spl250_603])],[avatar_definition]) ).
fof(f12872,plain,
( ~ false_terminates(sK155(sK240,sK239,sK238),sK239,sK240)
| spl250_603 ),
inference(avatar_component_clause,[],[f12870]) ).
fof(f12874,plain,
( ~ sP46(sK238,sK239,sK240)
| ~ false_terminates(sK154(sK240,sK239,sK238),sK239,sK240)
| sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| ~ sP45(sK238,sK240,sK239)
| ~ spl250_9
| spl250_32 ),
inference(forward_subsumption_resolution,[],[f12840,f2586]) ).
fof(f12876,definition,
( spl250_604
<=> false_terminates(sK154(sK240,sK239,sK238),sK239,sK240) ),
introduced(definition,[new_symbols(definition,[spl250_604])],[avatar_definition]) ).
fof(f12878,plain,
( ~ false_terminates(sK154(sK240,sK239,sK238),sK239,sK240)
| spl250_604 ),
inference(avatar_component_clause,[],[f12876]) ).
fof(f12880,plain,
( ~ sP46(sK238,sK239,sK240)
| ~ false_terminates(sK154(sK240,sK239,sK238),sK239,sK240)
| ~ false_terminates(sK155(sK240,sK239,sK238),sK239,sK240)
| ~ sP45(sK238,sK240,sK239)
| ~ spl250_9
| spl250_32 ),
inference(forward_subsumption_resolution,[],[f12838,f2586]) ).
fof(f12882,plain,
( ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602
| ~ spl250_9
| spl250_32 ),
inference(avatar_split_clause,[],[f12846,f1768,f1539,f12864,f12860,f12856,f12848]) ).
fof(f12883,plain,
( ~ spl250_598
| ~ spl250_603
| spl250_601
| ~ spl250_602
| ~ spl250_9
| spl250_32 ),
inference(avatar_split_clause,[],[f12868,f1768,f1539,f12864,f12860,f12870,f12848]) ).
fof(f12884,plain,
( ~ spl250_598
| spl250_600
| ~ spl250_604
| ~ spl250_602
| ~ spl250_9
| spl250_32 ),
inference(avatar_split_clause,[],[f12874,f1768,f1539,f12864,f12876,f12856,f12848]) ).
fof(f12885,plain,
( ~ spl250_598
| ~ spl250_603
| ~ spl250_604
| ~ spl250_602
| ~ spl250_9
| spl250_32 ),
inference(avatar_split_clause,[],[f12880,f1768,f1539,f12864,f12876,f12870,f12848]) ).
fof(f12956,plain,
( ~ member_terminates(p(sK161(sK238,sK240,sK239)),sK239)
| ~ gr(p(sK161(sK238,sK240,sK239)))
| ~ gr(sK239)
| spl250_598 ),
inference(resolution,[],[f12850,f1017]) ).
fof(f12962,plain,
( ~ member_terminates(p(sK161(sK238,sK240,sK239)),sK239)
| ~ gr(p(sK161(sK238,sK240,sK239)))
| ~ spl250_61
| spl250_598 ),
inference(forward_subsumption_resolution,[],[f12956,f2014]) ).
fof(f12964,definition,
( spl250_611
<=> gr(p(sK161(sK238,sK240,sK239))) ),
introduced(definition,[new_symbols(definition,[spl250_611])],[avatar_definition]) ).
fof(f12966,plain,
( ~ gr(p(sK161(sK238,sK240,sK239)))
| spl250_611 ),
inference(avatar_component_clause,[],[f12964]) ).
fof(f12968,definition,
( spl250_612
<=> member_terminates(p(sK161(sK238,sK240,sK239)),sK239) ),
introduced(definition,[new_symbols(definition,[spl250_612])],[avatar_definition]) ).
fof(f12970,plain,
( ~ member_terminates(p(sK161(sK238,sK240,sK239)),sK239)
| spl250_612 ),
inference(avatar_component_clause,[],[f12968]) ).
fof(f12971,plain,
( ~ spl250_611
| ~ spl250_612
| ~ spl250_61
| spl250_598 ),
inference(avatar_split_clause,[],[f12962,f12848,f2013,f12968,f12964]) ).
fof(f12979,plain,
( sP47(sK240,sK239,sK238)
| ~ sP46(sK238,sK239,sK240)
| sK238 = and(sK153(sK240,sK239,sK238),sK154(sK240,sK239,sK238))
| sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| sK238 = neg(sK157(sK240,sK239,sK238))
| ~ spl250_598 ),
inference(resolution,[],[f12849,f1008]) ).
fof(f12980,plain,
( ~ false_terminates(sK158(sK238,sK239,sK240),sK239,sK160(sK238,sK239,sK240))
| ~ false_terminates(sK159(sK238,sK239,sK240),sK160(sK238,sK239,sK240),sK240)
| spl250_602 ),
inference(resolution,[],[f12866,f1011]) ).
fof(f12982,plain,
( sK238 = or(sK158(sK238,sK239,sK240),sK159(sK238,sK239,sK240))
| spl250_602 ),
inference(resolution,[],[f12866,f1013]) ).
fof(f12984,plain,
( $false
| ~ spl250_9
| spl250_602 ),
inference(forward_subsumption_resolution,[],[f12982,f2591]) ).
fof(f12985,plain,
( ~ spl250_9
| spl250_602 ),
inference(avatar_contradiction_clause,[],[f12984]) ).
fof(f12991,definition,
( spl250_614
<=> false_terminates(sK158(sK238,sK239,sK240),sK239,sK160(sK238,sK239,sK240)) ),
introduced(definition,[new_symbols(definition,[spl250_614])],[avatar_definition]) ).
fof(f12992,plain,
( false_terminates(sK158(sK238,sK239,sK240),sK239,sK160(sK238,sK239,sK240))
| ~ spl250_614 ),
inference(avatar_component_clause,[],[f12991]) ).
fof(f12993,plain,
( ~ false_terminates(sK158(sK238,sK239,sK240),sK239,sK160(sK238,sK239,sK240))
| spl250_614 ),
inference(avatar_component_clause,[],[f12991]) ).
fof(f12996,definition,
( spl250_615
<=> false_terminates(sK159(sK238,sK239,sK240),sK160(sK238,sK239,sK240),sK240) ),
introduced(definition,[new_symbols(definition,[spl250_615])],[avatar_definition]) ).
fof(f12998,plain,
( ~ false_terminates(sK159(sK238,sK239,sK240),sK160(sK238,sK239,sK240),sK240)
| spl250_615 ),
inference(avatar_component_clause,[],[f12996]) ).
fof(f12999,plain,
( ~ spl250_615
| ~ spl250_614
| spl250_602 ),
inference(avatar_split_clause,[],[f12980,f12864,f12991,f12996]) ).
fof(f13004,plain,
( ! [X0] : p(X0) != sK238
| ~ spl250_601 ),
inference(superposition,[],[f666,f12862]) ).
fof(f13005,plain,
( ! [X0] : neg(X0) != sK238
| ~ spl250_601 ),
inference(superposition,[],[f669,f12862]) ).
fof(f13010,plain,
( ! [X0,X1] : or(X0,X1) != sK238
| ~ spl250_601 ),
inference(superposition,[],[f673,f12862]) ).
fof(f13042,plain,
( sK238 != sK238
| sK246(sK238) = sK154(sK240,sK239,sK238)
| ~ spl250_9
| ~ spl250_601 ),
inference(superposition,[],[f2588,f12862]) ).
fof(f13047,plain,
( sK246(sK238) = sK154(sK240,sK239,sK238)
| ~ spl250_9
| ~ spl250_601 ),
inference(trivial_inequality_removal,[],[f13042]) ).
fof(f13116,plain,
( ~ false_terminates(sK246(sK238),sK239,sK240)
| ~ spl250_9
| ~ spl250_601
| spl250_604 ),
inference(superposition,[],[f12878,f13047]) ).
fof(f13133,plain,
( ~ gr(sK246(sK238))
| ~ literal_list_succeeds(sK239)
| ~ gr(sK239)
| ~ sP63(sK238)
| ~ spl250_9
| ~ spl250_601
| spl250_604 ),
inference(resolution,[],[f13116,f1266]) ).
fof(f13143,plain,
( ~ literal_list_succeeds(sK239)
| ~ gr(sK239)
| ~ sP63(sK238)
| ~ spl250_9
| ~ spl250_107
| ~ spl250_601
| spl250_604 ),
inference(forward_subsumption_resolution,[],[f13133,f2571]) ).
fof(f13146,plain,
( ~ gr(sK239)
| ~ sP63(sK238)
| ~ spl250_9
| ~ spl250_62
| ~ spl250_107
| ~ spl250_601
| spl250_604 ),
inference(forward_subsumption_resolution,[],[f13143,f2018]) ).
fof(f13147,plain,
( ~ sP63(sK238)
| ~ spl250_9
| ~ spl250_61
| ~ spl250_62
| ~ spl250_107
| ~ spl250_601
| spl250_604 ),
inference(forward_subsumption_resolution,[],[f13146,f2014]) ).
fof(f13148,plain,
( $false
| ~ spl250_9
| ~ spl250_61
| ~ spl250_62
| ~ spl250_107
| ~ spl250_601
| spl250_604 ),
inference(forward_subsumption_resolution,[],[f13147,f1541]) ).
fof(f13149,plain,
( ~ spl250_9
| ~ spl250_61
| ~ spl250_62
| ~ spl250_107
| ~ spl250_601
| spl250_604 ),
inference(avatar_contradiction_clause,[],[f13148]) ).
fof(f13166,plain,
( ! [X0] : p(X0) != sK238
| ~ spl250_600 ),
inference(superposition,[],[f666,f12858]) ).
fof(f13167,plain,
( ! [X0] : neg(X0) != sK238
| ~ spl250_600 ),
inference(superposition,[],[f669,f12858]) ).
fof(f13172,plain,
( ! [X0,X1] : or(X0,X1) != sK238
| ~ spl250_600 ),
inference(superposition,[],[f673,f12858]) ).
fof(f13205,plain,
( sK238 != sK238
| sK245(sK238) = sK155(sK240,sK239,sK238)
| ~ spl250_9
| ~ spl250_600 ),
inference(superposition,[],[f2590,f12858]) ).
fof(f13208,plain,
( sK245(sK238) = sK155(sK240,sK239,sK238)
| ~ spl250_9
| ~ spl250_600 ),
inference(trivial_inequality_removal,[],[f13205]) ).
fof(f13252,plain,
( ~ false_terminates(sK245(sK238),sK239,sK240)
| ~ spl250_9
| ~ spl250_600
| spl250_603 ),
inference(superposition,[],[f12872,f13208]) ).
fof(f13268,plain,
( ~ gr(sK245(sK238))
| ~ literal_list_succeeds(sK239)
| ~ gr(sK239)
| ~ sP63(sK238)
| ~ spl250_9
| ~ spl250_600
| spl250_603 ),
inference(resolution,[],[f13252,f1269]) ).
fof(f13278,plain,
( ~ literal_list_succeeds(sK239)
| ~ gr(sK239)
| ~ sP63(sK238)
| ~ spl250_9
| ~ spl250_104
| ~ spl250_600
| spl250_603 ),
inference(forward_subsumption_resolution,[],[f13268,f2559]) ).
fof(f13281,plain,
( ~ gr(sK239)
| ~ sP63(sK238)
| ~ spl250_9
| ~ spl250_62
| ~ spl250_104
| ~ spl250_600
| spl250_603 ),
inference(forward_subsumption_resolution,[],[f13278,f2018]) ).
fof(f13282,plain,
( ~ sP63(sK238)
| ~ spl250_9
| ~ spl250_61
| ~ spl250_62
| ~ spl250_104
| ~ spl250_600
| spl250_603 ),
inference(forward_subsumption_resolution,[],[f13281,f2014]) ).
fof(f13283,plain,
( $false
| ~ spl250_9
| ~ spl250_61
| ~ spl250_62
| ~ spl250_104
| ~ spl250_600
| spl250_603 ),
inference(forward_subsumption_resolution,[],[f13282,f1541]) ).
fof(f13284,plain,
( ~ spl250_9
| ~ spl250_61
| ~ spl250_62
| ~ spl250_104
| ~ spl250_600
| spl250_603 ),
inference(avatar_contradiction_clause,[],[f13283]) ).
fof(f14079,plain,
( sK238 != sK238
| sP64(sK238)
| sP63(sK238)
| sK238 = p(sK242)
| ~ sP65
| ~ spl250_601 ),
inference(superposition,[],[f13005,f1254]) ).
fof(f14080,plain,
( sP64(sK238)
| sP63(sK238)
| sK238 = p(sK242)
| ~ sP65
| ~ spl250_601 ),
inference(trivial_inequality_removal,[],[f14079]) ).
fof(f14407,plain,
( sK238 = or(sK243(sK238),sK244(sK238))
| ~ spl250_10 ),
inference(resolution,[],[f1545,f1265]) ).
fof(f14408,plain,
( $false
| ~ spl250_10
| ~ spl250_601 ),
inference(forward_subsumption_resolution,[],[f14407,f13010]) ).
fof(f14409,plain,
( ~ spl250_10
| ~ spl250_601 ),
inference(avatar_contradiction_clause,[],[f14408]) ).
fof(f14411,definition,
( spl250_691
<=> gr(sK243(sK238)) ),
introduced(definition,[new_symbols(definition,[spl250_691])],[avatar_definition]) ).
fof(f14412,plain,
( gr(sK243(sK238))
| ~ spl250_691 ),
inference(avatar_component_clause,[],[f14411]) ).
fof(f14413,plain,
( ~ gr(sK243(sK238))
| spl250_691 ),
inference(avatar_component_clause,[],[f14411]) ).
fof(f14423,definition,
( spl250_694
<=> gr(sK244(sK238)) ),
introduced(definition,[new_symbols(definition,[spl250_694])],[avatar_definition]) ).
fof(f14424,plain,
( gr(sK244(sK238))
| ~ spl250_694 ),
inference(avatar_component_clause,[],[f14423]) ).
fof(f14425,plain,
( ~ gr(sK244(sK238))
| spl250_694 ),
inference(avatar_component_clause,[],[f14423]) ).
fof(f14438,plain,
( sP63(sK238)
| sK238 = p(sK242)
| ~ sP65
| spl250_10
| ~ spl250_601 ),
inference(forward_subsumption_resolution,[],[f14080,f1544]) ).
fof(f14463,plain,
( sK238 = p(sK242)
| ~ sP65
| spl250_9
| spl250_10
| ~ spl250_601 ),
inference(forward_subsumption_resolution,[],[f14438,f1540]) ).
fof(f14479,plain,
( ~ sP65
| spl250_9
| spl250_10
| ~ spl250_601 ),
inference(forward_subsumption_resolution,[],[f14463,f13004]) ).
fof(f14494,plain,
( $false
| spl250_9
| spl250_10
| ~ spl250_59
| ~ spl250_601 ),
inference(forward_subsumption_resolution,[],[f14479,f2007]) ).
fof(f14495,plain,
( spl250_9
| spl250_10
| ~ spl250_59
| ~ spl250_601 ),
inference(avatar_contradiction_clause,[],[f14494]) ).
fof(f14833,plain,
( sK238 != sK238
| sP64(sK238)
| sP63(sK238)
| sK238 = neg(sK241)
| ~ sP65
| ~ spl250_600 ),
inference(superposition,[],[f13166,f1254]) ).
fof(f14834,plain,
( sP64(sK238)
| sP63(sK238)
| sK238 = neg(sK241)
| ~ sP65
| ~ spl250_600 ),
inference(trivial_inequality_removal,[],[f14833]) ).
fof(f14840,plain,
( sP63(sK238)
| sK238 = neg(sK241)
| ~ sP65
| spl250_10
| ~ spl250_600 ),
inference(forward_subsumption_resolution,[],[f14834,f1544]) ).
fof(f14865,plain,
( sK238 = neg(sK241)
| ~ sP65
| spl250_9
| spl250_10
| ~ spl250_600 ),
inference(forward_subsumption_resolution,[],[f14840,f1540]) ).
fof(f14866,plain,
( ~ sP65
| spl250_9
| spl250_10
| ~ spl250_600 ),
inference(forward_subsumption_resolution,[],[f14865,f13167]) ).
fof(f14867,plain,
( $false
| spl250_9
| spl250_10
| ~ spl250_59
| ~ spl250_600 ),
inference(forward_subsumption_resolution,[],[f14866,f2007]) ).
fof(f14868,plain,
( spl250_9
| spl250_10
| ~ spl250_59
| ~ spl250_600 ),
inference(avatar_contradiction_clause,[],[f14867]) ).
fof(f15007,plain,
( sK238 = or(sK243(sK238),sK244(sK238))
| ~ spl250_10 ),
inference(resolution,[],[f1545,f1265]) ).
fof(f15008,plain,
( $false
| ~ spl250_10
| ~ spl250_600 ),
inference(forward_subsumption_resolution,[],[f15007,f13172]) ).
fof(f15009,plain,
( ~ spl250_10
| ~ spl250_600 ),
inference(avatar_contradiction_clause,[],[f15008]) ).
fof(f15010,plain,
( ~ sP46(sK238,sK239,sK240)
| sK238 = and(sK153(sK240,sK239,sK238),sK154(sK240,sK239,sK238))
| sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| sK238 = neg(sK157(sK240,sK239,sK238))
| spl250_32
| ~ spl250_598 ),
inference(forward_subsumption_resolution,[],[f12979,f12781]) ).
fof(f15014,plain,
( sK238 = and(sK153(sK240,sK239,sK238),sK154(sK240,sK239,sK238))
| sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| sK238 = neg(sK157(sK240,sK239,sK238))
| spl250_32
| ~ spl250_598
| ~ spl250_602 ),
inference(forward_subsumption_resolution,[],[f15010,f12865]) ).
fof(f15018,plain,
( sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| sK238 = neg(sK157(sK240,sK239,sK238))
| spl250_32
| ~ spl250_598
| spl250_601
| ~ spl250_602 ),
inference(forward_subsumption_resolution,[],[f15014,f12861]) ).
fof(f15022,plain,
( sK238 = neg(sK157(sK240,sK239,sK238))
| spl250_32
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(forward_subsumption_resolution,[],[f15018,f12857]) ).
fof(f15030,plain,
( ! [X0] : p(X0) != sK238
| spl250_32
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(superposition,[],[f665,f15022]) ).
fof(f15034,plain,
( ! [X0,X1] : or(X0,X1) != sK238
| spl250_32
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(superposition,[],[f670,f15022]) ).
fof(f15075,plain,
( ! [X0] : p(X0) != sK238
| ~ spl250_10 ),
inference(superposition,[],[f667,f15007]) ).
fof(f15076,plain,
( ! [X0] : neg(X0) != sK238
| ~ spl250_10 ),
inference(superposition,[],[f670,f15007]) ).
fof(f15077,plain,
( ! [X0,X1] : and(X0,X1) != sK238
| ~ spl250_10 ),
inference(superposition,[],[f673,f15007]) ).
fof(f15079,plain,
( ! [X0,X1] :
( or(X0,X1) != sK238
| sK244(sK238) = X1 )
| ~ spl250_10 ),
inference(superposition,[],[f674,f15007]) ).
fof(f15081,plain,
( ! [X0,X1] :
( or(X0,X1) != sK238
| sK243(sK238) = X0 )
| ~ spl250_10 ),
inference(superposition,[],[f675,f15007]) ).
fof(f15083,plain,
( ~ gr(sK238)
| gr(sK244(sK238))
| ~ spl250_10 ),
inference(superposition,[],[f690,f15007]) ).
fof(f15084,plain,
( ~ gr(sK238)
| gr(sK243(sK238))
| ~ spl250_10 ),
inference(superposition,[],[f691,f15007]) ).
fof(f15116,plain,
( gr(sK243(sK238))
| ~ spl250_10
| ~ spl250_63 ),
inference(forward_subsumption_resolution,[],[f15084,f2022]) ).
fof(f15117,plain,
( gr(sK244(sK238))
| ~ spl250_10
| ~ spl250_63 ),
inference(forward_subsumption_resolution,[],[f15083,f2022]) ).
fof(f15118,plain,
( $false
| ~ spl250_10
| ~ spl250_63
| spl250_691 ),
inference(forward_subsumption_resolution,[],[f15116,f14413]) ).
fof(f15119,plain,
( ~ spl250_10
| ~ spl250_63
| spl250_691 ),
inference(avatar_contradiction_clause,[],[f15118]) ).
fof(f15120,plain,
( $false
| ~ spl250_10
| ~ spl250_63
| spl250_694 ),
inference(forward_subsumption_resolution,[],[f15117,f14425]) ).
fof(f15121,plain,
( ~ spl250_10
| ~ spl250_63
| spl250_694 ),
inference(avatar_contradiction_clause,[],[f15120]) ).
fof(f15428,plain,
( sK238 != sK238
| ~ spl250_10
| spl250_32
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(superposition,[],[f15034,f15007]) ).
fof(f15429,plain,
( $false
| ~ spl250_10
| spl250_32
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(trivial_inequality_removal,[],[f15428]) ).
fof(f15430,plain,
( ~ spl250_10
| spl250_32
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(avatar_contradiction_clause,[],[f15429]) ).
fof(f15494,plain,
( ! [X0] : p(X0) != sK238
| ~ spl250_79 ),
inference(superposition,[],[f667,f2183]) ).
fof(f15495,plain,
( ! [X0] : neg(X0) != sK238
| ~ spl250_79 ),
inference(superposition,[],[f670,f2183]) ).
fof(f15498,plain,
( ! [X0,X1] :
( or(X0,X1) != sK238
| sK181(sK238,sK240,sK239) = X1 )
| ~ spl250_79 ),
inference(superposition,[],[f674,f2183]) ).
fof(f15781,plain,
( sK238 != sK238
| sK181(sK238,sK240,sK239) = sK244(sK238)
| ~ spl250_10
| ~ spl250_79 ),
inference(superposition,[],[f15498,f15007]) ).
fof(f15782,plain,
( sK181(sK238,sK240,sK239) = sK244(sK238)
| ~ spl250_10
| ~ spl250_79 ),
inference(trivial_inequality_removal,[],[f15781]) ).
fof(f15830,plain,
( ~ true_terminates(sK244(sK238),sK239,sK240)
| ~ spl250_10
| ~ spl250_79
| spl250_82 ),
inference(superposition,[],[f2199,f15782]) ).
fof(f15842,plain,
( ~ gr(sK244(sK238))
| ~ literal_list_succeeds(sK239)
| ~ gr(sK239)
| ~ sP64(sK238)
| ~ spl250_10
| ~ spl250_79
| spl250_82 ),
inference(resolution,[],[f15830,f1260]) ).
fof(f15850,plain,
( ~ literal_list_succeeds(sK239)
| ~ gr(sK239)
| ~ sP64(sK238)
| ~ spl250_10
| ~ spl250_79
| spl250_82
| ~ spl250_694 ),
inference(forward_subsumption_resolution,[],[f15842,f14424]) ).
fof(f15851,plain,
( ~ gr(sK239)
| ~ sP64(sK238)
| ~ spl250_10
| ~ spl250_62
| ~ spl250_79
| spl250_82
| ~ spl250_694 ),
inference(forward_subsumption_resolution,[],[f15850,f2018]) ).
fof(f15852,plain,
( ~ sP64(sK238)
| ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| ~ spl250_79
| spl250_82
| ~ spl250_694 ),
inference(forward_subsumption_resolution,[],[f15851,f2014]) ).
fof(f15853,plain,
( $false
| ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| ~ spl250_79
| spl250_82
| ~ spl250_694 ),
inference(forward_subsumption_resolution,[],[f15852,f1545]) ).
fof(f15854,plain,
( ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| ~ spl250_79
| spl250_82
| ~ spl250_694 ),
inference(avatar_contradiction_clause,[],[f15853]) ).
fof(f15855,plain,
( $false
| ~ spl250_10
| ~ spl250_76 ),
inference(forward_subsumption_resolution,[],[f2171,f15076]) ).
fof(f15856,plain,
( ~ spl250_10
| ~ spl250_76 ),
inference(avatar_contradiction_clause,[],[f15855]) ).
fof(f15900,plain,
( ! [X0] : p(X0) != sK238
| ~ spl250_78 ),
inference(superposition,[],[f667,f2179]) ).
fof(f15901,plain,
( ! [X0] : neg(X0) != sK238
| ~ spl250_78 ),
inference(superposition,[],[f670,f2179]) ).
fof(f15906,plain,
( ! [X0,X1] :
( or(X0,X1) != sK238
| sK182(sK238,sK240,sK239) = X0 )
| ~ spl250_78 ),
inference(superposition,[],[f675,f2179]) ).
fof(f16178,plain,
( sK238 != sK238
| sK182(sK238,sK240,sK239) = sK243(sK238)
| ~ spl250_10
| ~ spl250_78 ),
inference(superposition,[],[f15906,f15007]) ).
fof(f16179,plain,
( sK182(sK238,sK240,sK239) = sK243(sK238)
| ~ spl250_10
| ~ spl250_78 ),
inference(trivial_inequality_removal,[],[f16178]) ).
fof(f16233,plain,
( ~ true_terminates(sK243(sK238),sK239,sK240)
| ~ spl250_10
| ~ spl250_78
| spl250_81 ),
inference(superposition,[],[f2193,f16179]) ).
fof(f16249,plain,
( ~ gr(sK243(sK238))
| ~ literal_list_succeeds(sK239)
| ~ gr(sK239)
| ~ sP64(sK238)
| ~ spl250_10
| ~ spl250_78
| spl250_81 ),
inference(resolution,[],[f16233,f1263]) ).
fof(f16257,plain,
( ~ literal_list_succeeds(sK239)
| ~ gr(sK239)
| ~ sP64(sK238)
| ~ spl250_10
| ~ spl250_78
| spl250_81
| ~ spl250_691 ),
inference(forward_subsumption_resolution,[],[f16249,f14412]) ).
fof(f16258,plain,
( ~ gr(sK239)
| ~ sP64(sK238)
| ~ spl250_10
| ~ spl250_62
| ~ spl250_78
| spl250_81
| ~ spl250_691 ),
inference(forward_subsumption_resolution,[],[f16257,f2018]) ).
fof(f16259,plain,
( ~ sP64(sK238)
| ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| ~ spl250_78
| spl250_81
| ~ spl250_691 ),
inference(forward_subsumption_resolution,[],[f16258,f2014]) ).
fof(f16260,plain,
( $false
| ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| ~ spl250_78
| spl250_81
| ~ spl250_691 ),
inference(forward_subsumption_resolution,[],[f16259,f1545]) ).
fof(f16261,plain,
( ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| ~ spl250_78
| spl250_81
| ~ spl250_691 ),
inference(avatar_contradiction_clause,[],[f16260]) ).
fof(f16262,plain,
( true_terminates(sK243(sK238),sK239,sK240)
| ~ spl250_10
| ~ spl250_78
| ~ spl250_81 ),
inference(forward_demodulation,[],[f2192,f16179]) ).
fof(f16539,plain,
( sK238 = or(sK180(sK238,sK240,sK239),sK181(sK238,sK240,sK239))
| ~ true_terminates(sK182(sK238,sK240,sK239),sK239,sK240)
| ~ sP55(sK238,sK239,sK240)
| sK238 = neg(sK184(sK238,sK240,sK239))
| ~ sP54(sK238,sK240,sK239)
| spl250_593 ),
inference(resolution,[],[f12731,f1078]) ).
fof(f17245,plain,
( ~ member_terminates(neg(p(sK188(sK238,sK240,sK239))),sK239)
| ~ gr(neg(p(sK188(sK238,sK240,sK239))))
| ~ gr(sK239)
| spl250_75 ),
inference(resolution,[],[f2167,f1089]) ).
fof(f17247,plain,
( sK238 = p(sK188(sK238,sK240,sK239))
| spl250_75 ),
inference(resolution,[],[f2167,f1091]) ).
fof(f17249,plain,
( $false
| ~ spl250_10
| spl250_75 ),
inference(forward_subsumption_resolution,[],[f17247,f15075]) ).
fof(f17250,plain,
( ~ spl250_10
| spl250_75 ),
inference(avatar_contradiction_clause,[],[f17249]) ).
fof(f17251,plain,
( ~ member_terminates(neg(p(sK188(sK238,sK240,sK239))),sK239)
| ~ gr(neg(p(sK188(sK238,sK240,sK239))))
| ~ spl250_61
| spl250_75 ),
inference(forward_subsumption_resolution,[],[f17245,f2014]) ).
fof(f17253,definition,
( spl250_840
<=> gr(neg(p(sK188(sK238,sK240,sK239)))) ),
introduced(definition,[new_symbols(definition,[spl250_840])],[avatar_definition]) ).
fof(f17255,plain,
( ~ gr(neg(p(sK188(sK238,sK240,sK239))))
| spl250_840 ),
inference(avatar_component_clause,[],[f17253]) ).
fof(f17257,definition,
( spl250_841
<=> member_terminates(neg(p(sK188(sK238,sK240,sK239))),sK239) ),
introduced(definition,[new_symbols(definition,[spl250_841])],[avatar_definition]) ).
fof(f17259,plain,
( ~ member_terminates(neg(p(sK188(sK238,sK240,sK239))),sK239)
| spl250_841 ),
inference(avatar_component_clause,[],[f17257]) ).
fof(f17260,plain,
( ~ spl250_840
| ~ spl250_841
| ~ spl250_61
| spl250_75 ),
inference(avatar_split_clause,[],[f17251,f2165,f2013,f17257,f17253]) ).
fof(f17270,plain,
( ~ true_terminates(sK182(sK238,sK240,sK239),sK239,sK240)
| ~ sP55(sK238,sK239,sK240)
| sK238 = neg(sK184(sK238,sK240,sK239))
| ~ sP54(sK238,sK240,sK239)
| spl250_79
| spl250_593 ),
inference(forward_subsumption_resolution,[],[f16539,f2182]) ).
fof(f17287,plain,
( ~ true_terminates(sK182(sK238,sK240,sK239),sK239,sK240)
| sK238 = neg(sK184(sK238,sK240,sK239))
| ~ sP54(sK238,sK240,sK239)
| ~ spl250_77
| spl250_79
| spl250_593 ),
inference(forward_subsumption_resolution,[],[f17270,f2174]) ).
fof(f17300,plain,
( ~ true_terminates(sK182(sK238,sK240,sK239),sK239,sK240)
| ~ sP54(sK238,sK240,sK239)
| ~ spl250_10
| ~ spl250_77
| spl250_79
| spl250_593 ),
inference(forward_subsumption_resolution,[],[f17287,f15076]) ).
fof(f17313,plain,
( ~ true_terminates(sK182(sK238,sK240,sK239),sK239,sK240)
| ~ spl250_10
| ~ spl250_75
| ~ spl250_77
| spl250_79
| spl250_593 ),
inference(forward_subsumption_resolution,[],[f17300,f2166]) ).
fof(f17326,plain,
( ~ true_terminates(sK243(sK238),sK239,sK240)
| ~ spl250_10
| ~ spl250_75
| ~ spl250_77
| ~ spl250_78
| spl250_79
| spl250_593 ),
inference(forward_demodulation,[],[f17313,f16179]) ).
fof(f17339,plain,
( $false
| ~ spl250_10
| ~ spl250_75
| ~ spl250_77
| ~ spl250_78
| spl250_79
| ~ spl250_81
| spl250_593 ),
inference(forward_subsumption_resolution,[],[f17326,f16262]) ).
fof(f17340,plain,
( ~ spl250_10
| ~ spl250_75
| ~ spl250_77
| ~ spl250_78
| spl250_79
| ~ spl250_81
| spl250_593 ),
inference(avatar_contradiction_clause,[],[f17339]) ).
fof(f17426,plain,
( ~ false_terminates(sK158(sK238,sK239,sK240),sK239,sK160(sK238,sK239,sK240))
| ~ false_fails(sK158(sK238,sK239,sK240),sK239,sK160(sK238,sK239,sK240))
| spl250_602 ),
inference(resolution,[],[f12866,f1012]) ).
fof(f17427,plain,
( sK238 = or(sK158(sK238,sK239,sK240),sK159(sK238,sK239,sK240))
| spl250_602 ),
inference(resolution,[],[f12866,f1013]) ).
fof(f17433,plain,
( ! [X0] : p(X0) != sK238
| spl250_602 ),
inference(superposition,[],[f667,f17427]) ).
fof(f17434,plain,
( ! [X0] : neg(X0) != sK238
| spl250_602 ),
inference(superposition,[],[f670,f17427]) ).
fof(f17474,plain,
( sK238 != sK238
| sK159(sK238,sK239,sK240) = sK244(sK238)
| ~ spl250_10
| spl250_602 ),
inference(superposition,[],[f15079,f17427]) ).
fof(f17475,plain,
( sK238 != sK238
| sK158(sK238,sK239,sK240) = sK243(sK238)
| ~ spl250_10
| spl250_602 ),
inference(superposition,[],[f15081,f17427]) ).
fof(f17480,plain,
( sK158(sK238,sK239,sK240) = sK243(sK238)
| ~ spl250_10
| spl250_602 ),
inference(trivial_inequality_removal,[],[f17475]) ).
fof(f17481,plain,
( sK159(sK238,sK239,sK240) = sK244(sK238)
| ~ spl250_10
| spl250_602 ),
inference(trivial_inequality_removal,[],[f17474]) ).
fof(f17526,plain,
( ~ false_terminates(sK243(sK238),sK239,sK160(sK238,sK239,sK240))
| ~ spl250_10
| spl250_602
| spl250_614 ),
inference(superposition,[],[f12993,f17480]) ).
fof(f17543,plain,
( ~ gr(sK243(sK238))
| ~ literal_list_succeeds(sK239)
| ~ gr(sK239)
| ~ sP64(sK238)
| ~ spl250_10
| spl250_602
| spl250_614 ),
inference(resolution,[],[f17526,f1262]) ).
fof(f17553,plain,
( ~ literal_list_succeeds(sK239)
| ~ gr(sK239)
| ~ sP64(sK238)
| ~ spl250_10
| spl250_602
| spl250_614
| ~ spl250_691 ),
inference(forward_subsumption_resolution,[],[f17543,f14412]) ).
fof(f17556,plain,
( ~ gr(sK239)
| ~ sP64(sK238)
| ~ spl250_10
| ~ spl250_62
| spl250_602
| spl250_614
| ~ spl250_691 ),
inference(forward_subsumption_resolution,[],[f17553,f2018]) ).
fof(f17557,plain,
( ~ sP64(sK238)
| ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| spl250_602
| spl250_614
| ~ spl250_691 ),
inference(forward_subsumption_resolution,[],[f17556,f2014]) ).
fof(f17558,plain,
( $false
| ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| spl250_602
| spl250_614
| ~ spl250_691 ),
inference(forward_subsumption_resolution,[],[f17557,f1545]) ).
fof(f17559,plain,
( ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| spl250_602
| spl250_614
| ~ spl250_691 ),
inference(avatar_contradiction_clause,[],[f17558]) ).
fof(f17561,plain,
( false_terminates(sK243(sK238),sK239,sK160(sK238,sK239,sK240))
| ~ spl250_10
| spl250_602
| ~ spl250_614 ),
inference(forward_demodulation,[],[f12992,f17480]) ).
fof(f17562,plain,
( ~ false_terminates(sK244(sK238),sK160(sK238,sK239,sK240),sK240)
| ~ spl250_10
| spl250_602
| spl250_615 ),
inference(forward_demodulation,[],[f12998,f17481]) ).
fof(f17563,plain,
( ~ false_terminates(sK243(sK238),sK239,sK160(sK238,sK239,sK240))
| ~ false_fails(sK158(sK238,sK239,sK240),sK239,sK160(sK238,sK239,sK240))
| ~ spl250_10
| spl250_602 ),
inference(forward_demodulation,[],[f17426,f17480]) ).
fof(f17566,definition,
( spl250_845
<=> false_fails(sK243(sK238),sK239,sK160(sK238,sK239,sK240)) ),
introduced(definition,[new_symbols(definition,[spl250_845])],[avatar_definition]) ).
fof(f17568,plain,
( ~ false_fails(sK243(sK238),sK239,sK160(sK238,sK239,sK240))
| spl250_845 ),
inference(avatar_component_clause,[],[f17566]) ).
fof(f17570,definition,
( spl250_846
<=> false_terminates(sK243(sK238),sK239,sK160(sK238,sK239,sK240)) ),
introduced(definition,[new_symbols(definition,[spl250_846])],[avatar_definition]) ).
fof(f17571,plain,
( false_terminates(sK243(sK238),sK239,sK160(sK238,sK239,sK240))
| ~ spl250_846 ),
inference(avatar_component_clause,[],[f17570]) ).
fof(f17578,plain,
( spl250_846
| ~ spl250_10
| spl250_602
| ~ spl250_614 ),
inference(avatar_split_clause,[],[f17561,f12991,f12864,f1543,f17570]) ).
fof(f17579,plain,
( ~ false_fails(sK243(sK238),sK239,sK160(sK238,sK239,sK240))
| ~ false_terminates(sK243(sK238),sK239,sK160(sK238,sK239,sK240))
| ~ spl250_10
| spl250_602 ),
inference(forward_demodulation,[],[f17563,f17480]) ).
fof(f17581,plain,
( ~ spl250_846
| ~ spl250_845
| ~ spl250_10
| spl250_602 ),
inference(avatar_split_clause,[],[f17579,f12864,f1543,f17566,f17570]) ).
fof(f17583,plain,
( false_succeeds(sK243(sK238),sK239,sK160(sK238,sK239,sK240))
| false_fails(sK243(sK238),sK239,sK160(sK238,sK239,sK240))
| ~ spl250_846 ),
inference(resolution,[],[f17571,f697]) ).
fof(f17584,plain,
( false_succeeds(sK243(sK238),sK239,sK160(sK238,sK239,sK240))
| spl250_845
| ~ spl250_846 ),
inference(forward_subsumption_resolution,[],[f17583,f17568]) ).
fof(f17591,plain,
( literal_list_succeeds(sK160(sK238,sK239,sK240))
| ~ literal_list_succeeds(sK239)
| spl250_845
| ~ spl250_846 ),
inference(resolution,[],[f17584,f1244]) ).
fof(f17594,plain,
( gr(sK160(sK238,sK239,sK240))
| ~ gr(sK243(sK238))
| ~ gr(sK239)
| spl250_845
| ~ spl250_846 ),
inference(resolution,[],[f17584,f1250]) ).
fof(f17600,plain,
( gr(sK160(sK238,sK239,sK240))
| ~ gr(sK239)
| ~ spl250_691
| spl250_845
| ~ spl250_846 ),
inference(forward_subsumption_resolution,[],[f17594,f14412]) ).
fof(f17602,plain,
( literal_list_succeeds(sK160(sK238,sK239,sK240))
| ~ spl250_62
| spl250_845
| ~ spl250_846 ),
inference(forward_subsumption_resolution,[],[f17591,f2018]) ).
fof(f17606,plain,
( gr(sK160(sK238,sK239,sK240))
| ~ spl250_61
| ~ spl250_691
| spl250_845
| ~ spl250_846 ),
inference(forward_subsumption_resolution,[],[f17600,f2014]) ).
fof(f17608,plain,
( ~ gr(sK244(sK238))
| ~ literal_list_succeeds(sK160(sK238,sK239,sK240))
| ~ gr(sK160(sK238,sK239,sK240))
| ~ sP64(sK238)
| ~ spl250_10
| spl250_602
| spl250_615 ),
inference(resolution,[],[f17562,f1259]) ).
fof(f17618,plain,
( ~ literal_list_succeeds(sK160(sK238,sK239,sK240))
| ~ gr(sK160(sK238,sK239,sK240))
| ~ sP64(sK238)
| ~ spl250_10
| spl250_602
| spl250_615
| ~ spl250_694 ),
inference(forward_subsumption_resolution,[],[f17608,f14424]) ).
fof(f17621,plain,
( ~ gr(sK160(sK238,sK239,sK240))
| ~ sP64(sK238)
| ~ spl250_10
| ~ spl250_62
| spl250_602
| spl250_615
| ~ spl250_694
| spl250_845
| ~ spl250_846 ),
inference(forward_subsumption_resolution,[],[f17618,f17602]) ).
fof(f17622,plain,
( ~ sP64(sK238)
| ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| spl250_602
| spl250_615
| ~ spl250_691
| ~ spl250_694
| spl250_845
| ~ spl250_846 ),
inference(forward_subsumption_resolution,[],[f17621,f17606]) ).
fof(f17623,plain,
( $false
| ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| spl250_602
| spl250_615
| ~ spl250_691
| ~ spl250_694
| spl250_845
| ~ spl250_846 ),
inference(forward_subsumption_resolution,[],[f17622,f1545]) ).
fof(f17624,plain,
( ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| spl250_602
| spl250_615
| ~ spl250_691
| ~ spl250_694
| spl250_845
| ~ spl250_846 ),
inference(avatar_contradiction_clause,[],[f17623]) ).
fof(f17670,plain,
( ~ list_succeeds(sK239)
| spl250_612 ),
inference(resolution,[],[f12970,f1218]) ).
fof(f17676,plain,
( $false
| ~ spl250_62
| spl250_612 ),
inference(forward_subsumption_resolution,[],[f17670,f12405]) ).
fof(f17677,plain,
( ~ spl250_62
| spl250_612 ),
inference(avatar_contradiction_clause,[],[f17676]) ).
fof(f17727,plain,
( ~ gr(sK238)
| sP45(sK238,sK240,sK239)
| spl250_611 ),
inference(superposition,[],[f12966,f1019]) ).
fof(f17728,plain,
( sP45(sK238,sK240,sK239)
| ~ spl250_63
| spl250_611 ),
inference(forward_subsumption_resolution,[],[f17727,f2022]) ).
fof(f17729,plain,
( $false
| ~ spl250_63
| spl250_598
| spl250_611 ),
inference(forward_subsumption_resolution,[],[f17728,f12850]) ).
fof(f17730,plain,
( ~ spl250_63
| spl250_598
| spl250_611 ),
inference(avatar_contradiction_clause,[],[f17729]) ).
fof(f17731,plain,
( ~ spl250_593
| spl250_33 ),
inference(avatar_split_clause,[],[f1786,f1772,f12730]) ).
fof(f17917,plain,
( sK238 = and(sK185(sK238,sK239,sK240),sK186(sK238,sK239,sK240))
| spl250_77 ),
inference(resolution,[],[f2175,f1085]) ).
fof(f17919,plain,
( $false
| ~ spl250_10
| spl250_77 ),
inference(forward_subsumption_resolution,[],[f17917,f15077]) ).
fof(f17920,plain,
( ~ spl250_10
| spl250_77 ),
inference(avatar_contradiction_clause,[],[f17919]) ).
fof(f18065,plain,
( sK238 != sK238
| sP64(sK238)
| sP63(sK238)
| sK238 = neg(sK241)
| ~ sP65
| ~ spl250_78 ),
inference(superposition,[],[f15900,f1254]) ).
fof(f18066,plain,
( sP64(sK238)
| sP63(sK238)
| sK238 = neg(sK241)
| ~ sP65
| ~ spl250_78 ),
inference(trivial_inequality_removal,[],[f18065]) ).
fof(f18072,plain,
( sP63(sK238)
| sK238 = neg(sK241)
| ~ sP65
| spl250_10
| ~ spl250_78 ),
inference(forward_subsumption_resolution,[],[f18066,f1544]) ).
fof(f18073,plain,
( sK238 = neg(sK241)
| ~ sP65
| spl250_9
| spl250_10
| ~ spl250_78 ),
inference(forward_subsumption_resolution,[],[f18072,f1540]) ).
fof(f18074,plain,
( ~ sP65
| spl250_9
| spl250_10
| ~ spl250_78 ),
inference(forward_subsumption_resolution,[],[f18073,f15901]) ).
fof(f18075,plain,
( $false
| spl250_9
| spl250_10
| ~ spl250_59
| ~ spl250_78 ),
inference(forward_subsumption_resolution,[],[f18074,f2007]) ).
fof(f18076,plain,
( spl250_9
| spl250_10
| ~ spl250_59
| ~ spl250_78 ),
inference(avatar_contradiction_clause,[],[f18075]) ).
fof(f18307,plain,
( sK238 != sK238
| sP64(sK238)
| sP63(sK238)
| sK238 = neg(sK241)
| ~ sP65
| ~ spl250_79 ),
inference(superposition,[],[f15494,f1254]) ).
fof(f18308,plain,
( sP64(sK238)
| sP63(sK238)
| sK238 = neg(sK241)
| ~ sP65
| ~ spl250_79 ),
inference(trivial_inequality_removal,[],[f18307]) ).
fof(f18314,plain,
( sP63(sK238)
| sK238 = neg(sK241)
| ~ sP65
| spl250_10
| ~ spl250_79 ),
inference(forward_subsumption_resolution,[],[f18308,f1544]) ).
fof(f18315,plain,
( sK238 = neg(sK241)
| ~ sP65
| spl250_9
| spl250_10
| ~ spl250_79 ),
inference(forward_subsumption_resolution,[],[f18314,f1540]) ).
fof(f18316,plain,
( ~ sP65
| spl250_9
| spl250_10
| ~ spl250_79 ),
inference(forward_subsumption_resolution,[],[f18315,f15495]) ).
fof(f18317,plain,
( $false
| spl250_9
| spl250_10
| ~ spl250_59
| ~ spl250_79 ),
inference(forward_subsumption_resolution,[],[f18316,f2007]) ).
fof(f18318,plain,
( spl250_9
| spl250_10
| ~ spl250_59
| ~ spl250_79 ),
inference(avatar_contradiction_clause,[],[f18317]) ).
fof(f18323,plain,
( ! [X0] : p(X0) != sK238
| ~ spl250_76 ),
inference(superposition,[],[f665,f2171]) ).
fof(f18325,plain,
( ! [X0] :
( neg(X0) != sK238
| sK184(sK238,sK240,sK239) = X0 )
| ~ spl250_76 ),
inference(superposition,[],[f668,f2171]) ).
fof(f18559,plain,
( sK238 != sK238
| ~ spl250_6
| ~ spl250_76 ),
inference(superposition,[],[f18323,f1530]) ).
fof(f18568,plain,
( $false
| ~ spl250_6
| ~ spl250_76 ),
inference(trivial_inequality_removal,[],[f18559]) ).
fof(f18569,plain,
( ~ spl250_6
| ~ spl250_76 ),
inference(avatar_contradiction_clause,[],[f18568]) ).
fof(f18606,plain,
( ! [X0] :
( sP63(sK238)
| true_terminates(sK241,sK239,X0)
| ~ gr(sK241)
| ~ literal_list_succeeds(sK239)
| sK238 = p(sK242)
| ~ sP65 )
| spl250_10
| ~ spl250_61 ),
inference(forward_subsumption_resolution,[],[f12379,f1544]) ).
fof(f18607,plain,
( ! [X0] :
( sP63(sK238)
| false_terminates(sK241,sK239,X0)
| ~ gr(sK241)
| ~ literal_list_succeeds(sK239)
| sK238 = p(sK242)
| ~ sP65 )
| spl250_10
| ~ spl250_61 ),
inference(forward_subsumption_resolution,[],[f12378,f1544]) ).
fof(f18624,plain,
( ! [X0] :
( true_terminates(sK241,sK239,X0)
| ~ gr(sK241)
| ~ literal_list_succeeds(sK239)
| sK238 = p(sK242)
| ~ sP65 )
| spl250_9
| spl250_10
| ~ spl250_61 ),
inference(forward_subsumption_resolution,[],[f18606,f1540]) ).
fof(f18625,plain,
( ! [X0] :
( false_terminates(sK241,sK239,X0)
| ~ gr(sK241)
| ~ literal_list_succeeds(sK239)
| sK238 = p(sK242)
| ~ sP65 )
| spl250_9
| spl250_10
| ~ spl250_61 ),
inference(forward_subsumption_resolution,[],[f18607,f1540]) ).
fof(f18642,plain,
( ! [X0] :
( true_terminates(sK241,sK239,X0)
| ~ literal_list_succeeds(sK239)
| sK238 = p(sK242)
| ~ sP65 )
| ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_61 ),
inference(forward_subsumption_resolution,[],[f18624,f1533]) ).
fof(f18643,plain,
( ! [X0] :
( false_terminates(sK241,sK239,X0)
| ~ literal_list_succeeds(sK239)
| sK238 = p(sK242)
| ~ sP65 )
| ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_61 ),
inference(forward_subsumption_resolution,[],[f18625,f1533]) ).
fof(f18660,plain,
( ! [X0] :
( true_terminates(sK241,sK239,X0)
| sK238 = p(sK242)
| ~ sP65 )
| ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_61
| ~ spl250_62 ),
inference(forward_subsumption_resolution,[],[f18642,f2018]) ).
fof(f18661,plain,
( ! [X0] :
( false_terminates(sK241,sK239,X0)
| sK238 = p(sK242)
| ~ sP65 )
| ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_61
| ~ spl250_62 ),
inference(forward_subsumption_resolution,[],[f18643,f2018]) ).
fof(f18679,plain,
( ! [X0] :
( false_terminates(sK241,sK239,X0)
| ~ sP65 )
| ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_61
| ~ spl250_62
| ~ spl250_76 ),
inference(forward_subsumption_resolution,[],[f18661,f18323]) ).
fof(f18695,plain,
( ! [X0] : false_terminates(sK241,sK239,X0)
| ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_76 ),
inference(forward_subsumption_resolution,[],[f18679,f2007]) ).
fof(f18729,plain,
( ! [X0] :
( neg(X0) != sK238
| sK241 = X0 )
| ~ spl250_34 ),
inference(superposition,[],[f668,f1779]) ).
fof(f18863,plain,
( sP63(sK238)
| sK238 = neg(sK241)
| sK238 = p(sK242)
| ~ sP65
| spl250_10 ),
inference(resolution,[],[f1544,f1254]) ).
fof(f19558,plain,
( sK238 != sK238
| sK241 = sK184(sK238,sK240,sK239)
| ~ spl250_34
| ~ spl250_76 ),
inference(superposition,[],[f18325,f1779]) ).
fof(f19561,plain,
( sK241 = sK184(sK238,sK240,sK239)
| ~ spl250_34
| ~ spl250_76 ),
inference(trivial_inequality_removal,[],[f19558]) ).
fof(f19710,plain,
( ~ false_terminates(sK241,sK239,sK240)
| sP56(sK238,sK240,sK239)
| sK238 = or(sK180(sK238,sK240,sK239),sK181(sK238,sK240,sK239))
| sK238 = or(sK182(sK238,sK240,sK239),sK183(sK238,sK240,sK239))
| ~ sP55(sK238,sK239,sK240)
| ~ sP54(sK238,sK240,sK239)
| ~ spl250_34
| ~ spl250_76 ),
inference(superposition,[],[f1079,f19561]) ).
fof(f19712,plain,
( sP56(sK238,sK240,sK239)
| sK238 = or(sK180(sK238,sK240,sK239),sK181(sK238,sK240,sK239))
| sK238 = or(sK182(sK238,sK240,sK239),sK183(sK238,sK240,sK239))
| ~ sP55(sK238,sK239,sK240)
| ~ sP54(sK238,sK240,sK239)
| ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_76 ),
inference(forward_subsumption_resolution,[],[f19710,f18695]) ).
fof(f19715,plain,
( sK238 = or(sK180(sK238,sK240,sK239),sK181(sK238,sK240,sK239))
| sK238 = or(sK182(sK238,sK240,sK239),sK183(sK238,sK240,sK239))
| ~ sP55(sK238,sK239,sK240)
| ~ sP54(sK238,sK240,sK239)
| ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_76
| spl250_593 ),
inference(forward_subsumption_resolution,[],[f19712,f12731]) ).
fof(f19716,plain,
( sK238 = or(sK182(sK238,sK240,sK239),sK183(sK238,sK240,sK239))
| ~ sP55(sK238,sK239,sK240)
| ~ sP54(sK238,sK240,sK239)
| ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_76
| spl250_79
| spl250_593 ),
inference(forward_subsumption_resolution,[],[f19715,f2182]) ).
fof(f19717,plain,
( ~ sP55(sK238,sK239,sK240)
| ~ sP54(sK238,sK240,sK239)
| ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_76
| spl250_78
| spl250_79
| spl250_593 ),
inference(forward_subsumption_resolution,[],[f19716,f2178]) ).
fof(f19718,plain,
( ~ sP55(sK238,sK239,sK240)
| ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_75
| ~ spl250_76
| spl250_78
| spl250_79
| spl250_593 ),
inference(forward_subsumption_resolution,[],[f19717,f2166]) ).
fof(f19719,plain,
( ~ spl250_77
| ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_75
| ~ spl250_76
| spl250_78
| spl250_79
| spl250_593 ),
inference(avatar_split_clause,[],[f19718,f12730,f2181,f2177,f2169,f2165,f2017,f2013,f2005,f1777,f1543,f1539,f1532,f2173]) ).
fof(f19888,plain,
( ! [X0] :
( true_terminates(sK241,sK239,X0)
| ~ sP65 )
| spl250_6
| ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_61
| ~ spl250_62 ),
inference(forward_subsumption_resolution,[],[f18660,f1529]) ).
fof(f19902,plain,
( ! [X0] : true_terminates(sK241,sK239,X0)
| spl250_6
| ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62 ),
inference(forward_subsumption_resolution,[],[f19888,f2007]) ).
fof(f20381,plain,
( sK238 != sK238
| sK241 = sK157(sK240,sK239,sK238)
| spl250_32
| ~ spl250_34
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(superposition,[],[f18729,f15022]) ).
fof(f20403,plain,
( sK241 = sK157(sK240,sK239,sK238)
| spl250_32
| ~ spl250_34
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(trivial_inequality_removal,[],[f20381]) ).
fof(f20469,plain,
( ~ true_terminates(sK241,sK239,sK240)
| sP47(sK240,sK239,sK238)
| ~ sP46(sK238,sK239,sK240)
| sK238 = and(sK153(sK240,sK239,sK238),sK154(sK240,sK239,sK238))
| sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| ~ sP45(sK238,sK240,sK239)
| spl250_32
| ~ spl250_34
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(superposition,[],[f1007,f20403]) ).
fof(f20471,plain,
( sP47(sK240,sK239,sK238)
| ~ sP46(sK238,sK239,sK240)
| sK238 = and(sK153(sK240,sK239,sK238),sK154(sK240,sK239,sK238))
| sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| ~ sP45(sK238,sK240,sK239)
| spl250_6
| ~ spl250_7
| spl250_9
| spl250_10
| spl250_32
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(forward_subsumption_resolution,[],[f20469,f19902]) ).
fof(f20476,plain,
( ~ sP46(sK238,sK239,sK240)
| sK238 = and(sK153(sK240,sK239,sK238),sK154(sK240,sK239,sK238))
| sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| ~ sP45(sK238,sK240,sK239)
| spl250_6
| ~ spl250_7
| spl250_9
| spl250_10
| spl250_32
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(forward_subsumption_resolution,[],[f20471,f12781]) ).
fof(f20477,plain,
( sK238 = and(sK153(sK240,sK239,sK238),sK154(sK240,sK239,sK238))
| sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| ~ sP45(sK238,sK240,sK239)
| spl250_6
| ~ spl250_7
| spl250_9
| spl250_10
| spl250_32
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(forward_subsumption_resolution,[],[f20476,f12865]) ).
fof(f20478,plain,
( sK238 = and(sK155(sK240,sK239,sK238),sK156(sK240,sK239,sK238))
| ~ sP45(sK238,sK240,sK239)
| spl250_6
| ~ spl250_7
| spl250_9
| spl250_10
| spl250_32
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(forward_subsumption_resolution,[],[f20477,f12861]) ).
fof(f20479,plain,
( ~ sP45(sK238,sK240,sK239)
| spl250_6
| ~ spl250_7
| spl250_9
| spl250_10
| spl250_32
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(forward_subsumption_resolution,[],[f20478,f12857]) ).
fof(f20480,plain,
( $false
| spl250_6
| ~ spl250_7
| spl250_9
| spl250_10
| spl250_32
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(forward_subsumption_resolution,[],[f20479,f12849]) ).
fof(f20481,plain,
( spl250_6
| ~ spl250_7
| spl250_9
| spl250_10
| spl250_32
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(avatar_contradiction_clause,[],[f20480]) ).
fof(f20523,plain,
( sK238 = neg(sK241)
| sK238 = p(sK242)
| ~ sP65
| spl250_9
| spl250_10 ),
inference(forward_subsumption_resolution,[],[f18863,f1540]) ).
fof(f20578,plain,
( $false
| ~ spl250_6
| spl250_32
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(forward_subsumption_resolution,[],[f1530,f15030]) ).
fof(f20579,plain,
( ~ spl250_6
| spl250_32
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(avatar_contradiction_clause,[],[f20578]) ).
fof(f20739,plain,
( ~ list_succeeds(sK239)
| spl250_841 ),
inference(resolution,[],[f17259,f1218]) ).
fof(f20745,plain,
( $false
| ~ spl250_62
| spl250_841 ),
inference(forward_subsumption_resolution,[],[f20739,f12405]) ).
fof(f20746,plain,
( ~ spl250_62
| spl250_841 ),
inference(avatar_contradiction_clause,[],[f20745]) ).
fof(f20763,plain,
( ~ gr(neg(sK238))
| sP54(sK238,sK240,sK239)
| spl250_840 ),
inference(superposition,[],[f17255,f1091]) ).
fof(f20764,plain,
( sP54(sK238,sK240,sK239)
| ~ spl250_71
| spl250_840 ),
inference(forward_subsumption_resolution,[],[f20763,f2138]) ).
fof(f20765,plain,
( $false
| ~ spl250_71
| spl250_75
| spl250_840 ),
inference(forward_subsumption_resolution,[],[f20764,f2167]) ).
fof(f20766,plain,
( ~ spl250_71
| spl250_75
| spl250_840 ),
inference(avatar_contradiction_clause,[],[f20765]) ).
fof(f21817,plain,
( sK238 = p(sK242)
| ~ sP65
| spl250_9
| spl250_10
| spl250_77 ),
inference(forward_subsumption_resolution,[],[f20523,f12496]) ).
fof(f21829,plain,
( ~ sP65
| spl250_9
| spl250_10
| spl250_77 ),
inference(forward_subsumption_resolution,[],[f21817,f12495]) ).
fof(f21844,plain,
( $false
| spl250_9
| spl250_10
| ~ spl250_59
| spl250_77 ),
inference(forward_subsumption_resolution,[],[f21829,f2007]) ).
fof(f21845,plain,
( spl250_9
| spl250_10
| ~ spl250_59
| spl250_77 ),
inference(avatar_contradiction_clause,[],[f21844]) ).
fof(f21858,plain,
( sK238 = p(sK242)
| ~ sP65
| spl250_9
| spl250_10
| spl250_602 ),
inference(forward_subsumption_resolution,[],[f20523,f17434]) ).
fof(f21869,plain,
( ~ sP65
| spl250_9
| spl250_10
| spl250_602 ),
inference(forward_subsumption_resolution,[],[f21858,f17433]) ).
fof(f21882,plain,
( $false
| spl250_9
| spl250_10
| ~ spl250_59
| spl250_602 ),
inference(forward_subsumption_resolution,[],[f21869,f2007]) ).
fof(f21883,plain,
( spl250_9
| spl250_10
| ~ spl250_59
| spl250_602 ),
inference(avatar_contradiction_clause,[],[f21882]) ).
cnf(s1,plain,
( ~ spl250_1
| ~ spl250_2 ),
inference(sat_conversion,[],[f1448]) ).
cnf(s20,plain,
( spl250_1
| ~ spl250_32
| ~ spl250_33 ),
inference(sat_conversion,[],[f1775]) ).
cnf(s56,plain,
( spl250_33
| ~ spl250_75
| spl250_76
| ~ spl250_77
| spl250_78
| spl250_79 ),
inference(sat_conversion,[],[f2184]) ).
cnf(s60,plain,
( spl250_33
| ~ spl250_75
| spl250_76
| ~ spl250_77
| spl250_78
| ~ spl250_82 ),
inference(sat_conversion,[],[f2200]) ).
cnf(s62,plain,
( spl250_33
| ~ spl250_75
| spl250_76
| ~ spl250_77
| ~ spl250_81
| ~ spl250_82 ),
inference(sat_conversion,[],[f2202]) ).
cnf(s64,plain,
( spl250_6
| spl250_9
| spl250_10
| spl250_34
| ~ spl250_59 ),
inference(sat_conversion,[],[f2221]) ).
cnf(s74,plain,
( spl250_7
| ~ spl250_34
| ~ spl250_63 ),
inference(sat_conversion,[],[f2305]) ).
cnf(s77,plain,
( ~ spl250_59
| spl250_63 ),
inference(sat_conversion,[],[f2334]) ).
cnf(s89,plain,
( spl250_1
| spl250_71 ),
inference(sat_conversion,[],[f2410]) ).
cnf(s91,plain,
( spl250_1
| spl250_61 ),
inference(sat_conversion,[],[f2412]) ).
cnf(s92,plain,
( spl250_1
| spl250_62 ),
inference(sat_conversion,[],[f2413]) ).
cnf(s93,plain,
( spl250_1
| spl250_59 ),
inference(sat_conversion,[],[f2415]) ).
cnf(s94,plain,
( spl250_2
| spl250_59 ),
inference(sat_conversion,[],[f2416]) ).
cnf(s96,plain,
( ~ spl250_63
| spl250_71 ),
inference(sat_conversion,[],[f2468]) ).
cnf(s102,plain,
( ~ spl250_9
| ~ spl250_107
| spl250_108 ),
inference(sat_conversion,[],[f2576]) ).
cnf(s107,plain,
( ~ spl250_9
| ~ spl250_63
| spl250_104 ),
inference(sat_conversion,[],[f2655]) ).
cnf(s108,plain,
( ~ spl250_9
| ~ spl250_63
| spl250_107 ),
inference(sat_conversion,[],[f2657]) ).
cnf(s161,plain,
( ~ spl250_9
| spl250_75 ),
inference(sat_conversion,[],[f3422]) ).
cnf(s526,plain,
( ~ spl250_59
| spl250_62 ),
inference(sat_conversion,[],[f12336]) ).
cnf(s527,plain,
( ~ spl250_59
| spl250_61 ),
inference(sat_conversion,[],[f12337]) ).
cnf(s536,plain,
( ~ spl250_9
| spl250_77
| ~ spl250_590
| ~ spl250_591 ),
inference(sat_conversion,[],[f12606]) ).
cnf(s537,plain,
( ~ spl250_9
| spl250_77
| ~ spl250_591
| ~ spl250_592 ),
inference(sat_conversion,[],[f12612]) ).
cnf(s539,plain,
( ~ spl250_9
| ~ spl250_61
| ~ spl250_62
| ~ spl250_104
| spl250_591 ),
inference(sat_conversion,[],[f12629]) ).
cnf(s542,plain,
( ~ spl250_61
| ~ spl250_62
| ~ spl250_104
| ~ spl250_108
| spl250_590
| ~ spl250_591
| spl250_592 ),
inference(sat_conversion,[],[f12689]) ).
cnf(s546,plain,
( ~ spl250_9
| spl250_33
| ~ spl250_75
| ~ spl250_77 ),
inference(sat_conversion,[],[f12713]) ).
cnf(s549,plain,
( ~ spl250_32
| ~ spl250_33
| ~ spl250_59 ),
inference(sat_conversion,[],[f12721]) ).
cnf(s562,plain,
( ~ spl250_9
| spl250_32
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(sat_conversion,[],[f12882]) ).
cnf(s563,plain,
( ~ spl250_9
| spl250_32
| ~ spl250_598
| spl250_601
| ~ spl250_602
| ~ spl250_603 ),
inference(sat_conversion,[],[f12883]) ).
cnf(s564,plain,
( ~ spl250_9
| spl250_32
| ~ spl250_598
| spl250_600
| ~ spl250_602
| ~ spl250_604 ),
inference(sat_conversion,[],[f12884]) ).
cnf(s565,plain,
( ~ spl250_9
| spl250_32
| ~ spl250_598
| ~ spl250_602
| ~ spl250_603
| ~ spl250_604 ),
inference(sat_conversion,[],[f12885]) ).
cnf(s570,plain,
( ~ spl250_61
| spl250_598
| ~ spl250_611
| ~ spl250_612 ),
inference(sat_conversion,[],[f12971]) ).
cnf(s571,plain,
( ~ spl250_9
| spl250_602 ),
inference(sat_conversion,[],[f12985]) ).
cnf(s573,plain,
( spl250_602
| ~ spl250_614
| ~ spl250_615 ),
inference(sat_conversion,[],[f12999]) ).
cnf(s575,plain,
( ~ spl250_9
| ~ spl250_61
| ~ spl250_62
| ~ spl250_107
| ~ spl250_601
| spl250_604 ),
inference(sat_conversion,[],[f13149]) ).
cnf(s578,plain,
( ~ spl250_9
| ~ spl250_61
| ~ spl250_62
| ~ spl250_104
| ~ spl250_600
| spl250_603 ),
inference(sat_conversion,[],[f13284]) ).
cnf(s638,plain,
( ~ spl250_10
| ~ spl250_601 ),
inference(sat_conversion,[],[f14409]) ).
cnf(s648,plain,
( spl250_9
| spl250_10
| ~ spl250_59
| ~ spl250_601 ),
inference(sat_conversion,[],[f14495]) ).
cnf(s666,plain,
( spl250_9
| spl250_10
| ~ spl250_59
| ~ spl250_600 ),
inference(sat_conversion,[],[f14868]) ).
cnf(s667,plain,
( ~ spl250_10
| ~ spl250_600 ),
inference(sat_conversion,[],[f15009]) ).
cnf(s668,plain,
( ~ spl250_10
| ~ spl250_63
| spl250_691 ),
inference(sat_conversion,[],[f15119]) ).
cnf(s669,plain,
( ~ spl250_10
| ~ spl250_63
| spl250_694 ),
inference(sat_conversion,[],[f15121]) ).
cnf(s697,plain,
( ~ spl250_10
| spl250_32
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(sat_conversion,[],[f15430]) ).
cnf(s722,plain,
( ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| ~ spl250_79
| spl250_82
| ~ spl250_694 ),
inference(sat_conversion,[],[f15854]) ).
cnf(s723,plain,
( ~ spl250_10
| ~ spl250_76 ),
inference(sat_conversion,[],[f15856]) ).
cnf(s738,plain,
( ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| ~ spl250_78
| spl250_81
| ~ spl250_691 ),
inference(sat_conversion,[],[f16261]) ).
cnf(s778,plain,
( ~ spl250_10
| spl250_75 ),
inference(sat_conversion,[],[f17250]) ).
cnf(s779,plain,
( ~ spl250_61
| spl250_75
| ~ spl250_840
| ~ spl250_841 ),
inference(sat_conversion,[],[f17260]) ).
cnf(s789,plain,
( ~ spl250_10
| ~ spl250_75
| ~ spl250_77
| ~ spl250_78
| spl250_79
| ~ spl250_81
| spl250_593 ),
inference(sat_conversion,[],[f17340]) ).
cnf(s800,plain,
( ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| spl250_602
| spl250_614
| ~ spl250_691 ),
inference(sat_conversion,[],[f17559]) ).
cnf(s804,plain,
( ~ spl250_10
| spl250_602
| ~ spl250_614
| spl250_846 ),
inference(sat_conversion,[],[f17578]) ).
cnf(s805,plain,
( ~ spl250_10
| spl250_602
| ~ spl250_845
| ~ spl250_846 ),
inference(sat_conversion,[],[f17581]) ).
cnf(s807,plain,
( ~ spl250_10
| ~ spl250_61
| ~ spl250_62
| spl250_602
| spl250_615
| ~ spl250_691
| ~ spl250_694
| spl250_845
| ~ spl250_846 ),
inference(sat_conversion,[],[f17624]) ).
cnf(s811,plain,
( ~ spl250_62
| spl250_612 ),
inference(sat_conversion,[],[f17677]) ).
cnf(s815,plain,
( ~ spl250_63
| spl250_598
| spl250_611 ),
inference(sat_conversion,[],[f17730]) ).
cnf(s816,plain,
( spl250_33
| ~ spl250_593 ),
inference(sat_conversion,[],[f17731]) ).
cnf(s822,plain,
( ~ spl250_10
| spl250_77 ),
inference(sat_conversion,[],[f17920]) ).
cnf(s824,plain,
( spl250_9
| spl250_10
| ~ spl250_59
| ~ spl250_78 ),
inference(sat_conversion,[],[f18076]) ).
cnf(s826,plain,
( spl250_9
| spl250_10
| ~ spl250_59
| ~ spl250_79 ),
inference(sat_conversion,[],[f18318]) ).
cnf(s836,plain,
( ~ spl250_6
| ~ spl250_76 ),
inference(sat_conversion,[],[f18569]) ).
cnf(s899,plain,
( ~ spl250_7
| spl250_9
| spl250_10
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_75
| ~ spl250_76
| ~ spl250_77
| spl250_78
| spl250_79
| spl250_593 ),
inference(sat_conversion,[],[f19719]) ).
cnf(s935,plain,
( spl250_6
| ~ spl250_7
| spl250_9
| spl250_10
| spl250_32
| ~ spl250_34
| ~ spl250_59
| ~ spl250_61
| ~ spl250_62
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(sat_conversion,[],[f20481]) ).
cnf(s941,plain,
( ~ spl250_6
| spl250_32
| ~ spl250_598
| spl250_600
| spl250_601
| ~ spl250_602 ),
inference(sat_conversion,[],[f20579]) ).
cnf(s955,plain,
( ~ spl250_62
| spl250_841 ),
inference(sat_conversion,[],[f20746]) ).
cnf(s956,plain,
( ~ spl250_71
| spl250_75
| spl250_840 ),
inference(sat_conversion,[],[f20766]) ).
cnf(s1020,plain,
( spl250_9
| spl250_10
| ~ spl250_59
| spl250_77 ),
inference(sat_conversion,[],[f21845]) ).
cnf(s1027,plain,
( spl250_9
| spl250_10
| ~ spl250_59
| spl250_602 ),
inference(sat_conversion,[],[f21883]) ).
cnf(s1054,plain,
( spl250_78
| spl250_33
| ~ spl250_10
| spl250_1 ),
inference(rat,[],[s722,s60,s56,s92,s91,s822,s778,s723,s669,s77,s93]) ).
cnf(s1055,plain,
( spl250_33
| ~ spl250_10
| spl250_1 ),
inference(rat,[],[s722,s62,s789,s738,s1054,s816,s92,s91,s822,s778,s723,s669,s668,s77,s93]) ).
cnf(s1056,plain,
( spl250_598
| spl250_1 ),
inference(rat,[],[s570,s815,s91,s77,s93,s811,s92]) ).
cnf(s1057,plain,
( spl250_615
| ~ spl250_846
| ~ spl250_62
| ~ spl250_61
| ~ spl250_10
| ~ spl250_691
| ~ spl250_694
| spl250_602 ),
inference(rat,[],[s805,s807]) ).
cnf(s1058,plain,
( spl250_602
| ~ spl250_10
| spl250_1 ),
inference(rat,[],[s1057,s804,s573,s800,s92,s91,s669,s668,s77,s93]) ).
cnf(s1059,plain,
( ~ spl250_10
| spl250_1 ),
inference(rat,[],[s697,s20,s1058,s1055,s638,s667,s1056]) ).
cnf(s1060,plain,
( spl250_600
| spl250_32
| ~ spl250_9
| spl250_1 ),
inference(rat,[],[s575,s564,s562,s92,s91,s1056,s571,s108,s77,s93]) ).
cnf(s1061,plain,
( spl250_32
| ~ spl250_9
| spl250_1 ),
inference(rat,[],[s575,s563,s565,s578,s1060,s92,s91,s1056,s571,s108,s107,s77,s93]) ).
cnf(s1062,plain,
( ~ spl250_9
| spl250_1 ),
inference(rat,[],[s542,s536,s537,s546,s549,s1061,s539,s102,s107,s108,s161,s92,s91,s77,s93]) ).
cnf(s1063,plain,
( ~ spl250_75
| spl250_6
| spl250_1 ),
inference(rat,[],[s56,s899,s826,s824,s1020,s816,s549,s935,s74,s77,s64,s91,s92,s1056,s666,s648,s1027,s1062,s1059,s93]) ).
cnf(s1064,plain,
( spl250_75
| spl250_1 ),
inference(rat,[],[s779,s956,s91,s89,s955,s92]) ).
cnf(s1065,plain,
spl250_1,
inference(rat,[],[s549,s56,s941,s836,s1063,s1064,s1020,s1027,s666,s824,s826,s648,s1062,s1059,s1056,s93]) ).
cnf(s1066,plain,
~ spl250_2,
inference(rat,[],[s1,s1065]) ).
cnf(s1070,plain,
spl250_59,
inference(rat,[],[s94,s1066]) ).
cnf(s1071,plain,
spl250_61,
inference(rat,[],[s527,s1070]) ).
cnf(s1072,plain,
spl250_62,
inference(rat,[],[s526,s1070]) ).
cnf(s1073,plain,
spl250_63,
inference(rat,[],[s77,s1070]) ).
cnf(s1074,plain,
spl250_841,
inference(rat,[],[s955,s1072]) ).
cnf(s1077,plain,
spl250_612,
inference(rat,[],[s811,s1072]) ).
cnf(s1078,plain,
spl250_71,
inference(rat,[],[s96,s1073]) ).
cnf(s1079,plain,
( spl250_602
| ~ spl250_10 ),
inference(rat,[],[s1057,s804,s573,s800,s669,s668,s1072,s1071,s1073]) ).
cnf(s1080,plain,
spl250_598,
inference(rat,[],[s570,s815,s1071,s1077,s1073]) ).
cnf(s1081,plain,
( spl250_78
| ~ spl250_10 ),
inference(rat,[],[s722,s60,s56,s822,s778,s723,s669,s549,s697,s1079,s667,s638,s1072,s1071,s1070,s1080,s1073]) ).
cnf(s1082,plain,
~ spl250_10,
inference(rat,[],[s722,s62,s789,s738,s1081,s816,s549,s697,s1079,s668,s669,s638,s667,s723,s778,s822,s1072,s1071,s1070,s1080,s1073]) ).
cnf(s1083,plain,
( spl250_600
| spl250_32
| ~ spl250_9 ),
inference(rat,[],[s575,s564,s562,s571,s108,s1072,s1071,s1080,s1073]) ).
cnf(s1084,plain,
( spl250_32
| ~ spl250_9 ),
inference(rat,[],[s575,s563,s565,s578,s1083,s571,s108,s107,s1072,s1071,s1080,s1073]) ).
cnf(s1085,plain,
~ spl250_9,
inference(rat,[],[s542,s536,s537,s546,s549,s1084,s539,s102,s107,s108,s161,s1071,s1072,s1070,s1073]) ).
cnf(s1086,plain,
~ spl250_601,
inference(rat,[],[s648,s1082,s1070,s1085]) ).
cnf(s1087,plain,
~ spl250_79,
inference(rat,[],[s826,s1082,s1070,s1085]) ).
cnf(s1088,plain,
~ spl250_78,
inference(rat,[],[s824,s1082,s1070,s1085]) ).
cnf(s1089,plain,
~ spl250_600,
inference(rat,[],[s666,s1082,s1070,s1085]) ).
cnf(s1090,plain,
spl250_602,
inference(rat,[],[s1027,s1082,s1070,s1085]) ).
cnf(s1091,plain,
spl250_77,
inference(rat,[],[s1020,s1082,s1070,s1085]) ).
cnf(s1092,plain,
( ~ spl250_75
| spl250_6 ),
inference(rat,[],[s899,s56,s816,s549,s935,s74,s64,s1082,s1085,s1070,s1071,s1072,s1091,s1088,s1087,s1090,s1086,s1089,s1080,s1073]) ).
cnf(s1093,plain,
spl250_75,
inference(rat,[],[s779,s956,s1071,s1074,s1078]) ).
cnf(s1094,plain,
spl250_6,
inference(rat,[],[s1092,s1093]) ).
cnf(s1098,plain,
~ spl250_76,
inference(rat,[],[s836,s1094]) ).
cnf(s1100,plain,
spl250_32,
inference(rat,[],[s941,s1090,s1086,s1089,s1080,s1094]) ).
cnf(s1101,plain,
spl250_33,
inference(rat,[],[s56,s1093,s1087,s1091,s1088,s1098]) ).
cnf(s1102,plain,
$false,
inference(rat,[],[s549,s1070,s1101,s1100]) ).
fof(f21892,plain,
$false,
inference(avatar_sat_refutation,[],[s1102]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX066+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n002.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 15:01:56 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running first-order theorem proving
% 0.08/0.24 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
% 14.68/2.50 % (416675)Detected formulas, will run a generic FOF schedule.
% 14.68/2.50 % (416686)dis-21_1_sil=8000:lcm=predicate:random_seed=1716357827:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 14.68/2.50 % (416686)Instruction limit reached!
% 14.68/2.50 % (416686)------------------------------
% 14.68/2.50 % (416686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.68/2.50 % (416686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.68/2.50 % (416686)CaDiCaL version: 2.1.3
% 14.68/2.50 % (416686)Termination reason: Instruction limit
% 14.68/2.50 % (416686)Termination phase: Saturation
% 14.68/2.50 % (416686)Time elapsed: 0.038 s
% 14.68/2.50 % (416686)Peak memory usage: 90 MB
% 14.68/2.50 % (416686)Instructions burned: 132 (million)
% 14.68/2.50 % (416683)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=555995820:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 14.68/2.50 % (416685)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1044872623:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 14.68/2.50 % (416682)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=935244649:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 14.68/2.50 % (416681)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=3987591076:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 14.68/2.50 % (416684)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1471046503:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 14.68/2.50 % (416680)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=3288087956:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 14.68/2.50 % (416683)Refutation not found, incomplete strategy
% 14.68/2.50 % (416683)------------------------------
% 14.68/2.50 % (416683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.68/2.50 % (416683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.68/2.50 % (416683)CaDiCaL version: 2.1.3
% 14.68/2.50 % (416683)Termination reason: Refutation not found, incomplete strategy
% 14.68/2.50 % (416683)Time elapsed: 0.008 s
% 14.68/2.50 % (416683)Peak memory usage: 88 MB
% 14.68/2.50 % (416683)Instructions burned: 12 (million)
% 14.68/2.50 % (416684)Instruction limit reached!
% 14.68/2.50 % (416684)------------------------------
% 14.68/2.50 % (416684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.68/2.50 % (416684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.68/2.50 % (416684)CaDiCaL version: 2.1.3
% 14.68/2.50 % (416684)Termination reason: Instruction limit
% 14.68/2.50 % (416684)Termination phase: Saturation
% 14.68/2.50 % (416684)Time elapsed: 0.070 s
% 14.68/2.50 % (416684)Peak memory usage: 89 MB
% 14.68/2.50 % (416684)Instructions burned: 120 (million)
% 14.68/2.50 % (416685)Instruction limit reached!
% 14.68/2.50 % (416685)------------------------------
% 14.68/2.50 % (416685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.68/2.50 % (416685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.68/2.50 % (416685)CaDiCaL version: 2.1.3
% 14.68/2.50 % (416685)Termination reason: Instruction limit
% 14.68/2.50 % (416685)Termination phase: Saturation
% 14.68/2.50 % (416685)Time elapsed: 0.093 s
% 14.68/2.50 % (416685)Peak memory usage: 90 MB
% 14.68/2.50 % (416685)Instructions burned: 139 (million)
% 14.68/2.50 % (416688)lrs+10_1_sil=8000:sp=occurrence:random_seed=3680024801:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 14.68/2.50 % (416688)Instruction limit reached!
% 14.68/2.50 % (416688)------------------------------
% 14.68/2.50 % (416688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.68/2.50 % (416688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.68/2.50 % (416688)CaDiCaL version: 2.1.3
% 14.68/2.50 % (416688)Termination reason: Instruction limit
% 14.68/2.50 % (416688)Termination phase: Saturation
% 14.68/2.50 % (416688)Time elapsed: 0.099 s
% 14.68/2.50 % (416688)Peak memory usage: 93 MB
% 14.68/2.50 % (416688)Instructions burned: 288 (million)
% 14.68/2.50 % (416695)lrs+10_1_sil=32000:urr=on:br=off:random_seed=737984312:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 19.63/3.25 % (416683)------------------------------
% 19.63/3.25 % (416683)------------------------------
% 19.63/3.25 % (416696)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2806727633:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 19.63/3.25 % (416695)Instruction limit reached!
% 19.63/3.25 % (416695)------------------------------
% 19.63/3.25 % (416695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.25 % (416695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.25 % (416695)CaDiCaL version: 2.1.3
% 19.63/3.25 % (416695)Termination reason: Instruction limit
% 19.63/3.25 % (416695)Termination phase: Saturation
% 19.63/3.25 % (416695)Time elapsed: 0.081 s
% 19.63/3.25 % (416695)Peak memory usage: 93 MB
% 19.63/3.25 % (416695)Instructions burned: 158 (million)
% 19.63/3.25 % (416698)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=2391315651:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 19.63/3.25 % (416698)Instruction limit reached!
% 19.63/3.25 % (416698)------------------------------
% 19.63/3.25 % (416698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.25 % (416698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.25 % (416698)CaDiCaL version: 2.1.3
% 19.63/3.25 % (416698)Termination reason: Instruction limit
% 19.63/3.25 % (416698)Termination phase: Saturation
% 19.63/3.25 % (416698)Time elapsed: 0.071 s
% 19.63/3.25 % (416698)Peak memory usage: 96 MB
% 19.63/3.25 % (416698)Instructions burned: 251 (million)
% 19.63/3.25 % (416701)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4114155977:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 19.63/3.25 % (416696)Instruction limit reached!
% 19.63/3.25 % (416696)------------------------------
% 19.63/3.25 % (416696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.25 % (416696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.25 % (416696)CaDiCaL version: 2.1.3
% 19.63/3.25 % (416696)Termination reason: Instruction limit
% 19.63/3.25 % (416696)Termination phase: Saturation
% 19.63/3.25 % (416696)Time elapsed: 0.163 s
% 19.63/3.25 % (416696)Peak memory usage: 90 MB
% 19.63/3.25 % (416696)Instructions burned: 327 (million)
% 19.63/3.25 % (416701)Refutation not found, incomplete strategy
% 19.63/3.25 % (416701)------------------------------
% 19.63/3.25 % (416701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.25 % (416701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.25 % (416701)CaDiCaL version: 2.1.3
% 19.63/3.25 % (416701)Termination reason: Refutation not found, incomplete strategy
% 19.63/3.25 % (416701)Time elapsed: 0.015 s
% 19.63/3.25 % (416701)Peak memory usage: 89 MB
% 19.63/3.25 % (416701)Instructions burned: 27 (million)
% 19.63/3.25 % (416702)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=97270166:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 19.63/3.25 % (416705)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2596651984:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 19.63/3.25 % (416705)Instruction limit reached!
% 19.63/3.25 % (416705)------------------------------
% 19.63/3.25 % (416705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.25 % (416705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.25 % (416705)CaDiCaL version: 2.1.3
% 19.63/3.25 % (416705)Termination reason: Instruction limit
% 19.63/3.25 % (416705)Termination phase: Saturation
% 19.63/3.25 % (416705)Time elapsed: 0.041 s
% 19.63/3.25 % (416705)Peak memory usage: 91 MB
% 19.63/3.25 % (416705)Instructions burned: 115 (million)
% 19.63/3.25 % (416706)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3545798544:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 19.63/3.25 % (416706)Instruction limit reached!
% 19.63/3.25 % (416706)------------------------------
% 19.63/3.25 % (416706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.25 % (416706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.25 % (416706)CaDiCaL version: 2.1.3
% 19.63/3.25 % (416706)Termination reason: Instruction limit
% 19.63/3.25 % (416706)Termination phase: Saturation
% 19.63/3.25 % (416706)Time elapsed: 0.067 s
% 45.29/6.87 % (416706)Peak memory usage: 90 MB
% 45.29/6.87 % (416706)Instructions burned: 128 (million)
% 45.29/6.87 % (416701)------------------------------
% 45.29/6.87 % (416701)------------------------------
% 45.29/6.87 % (416709)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3021390807:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 45.29/6.87 % (416709)Instruction limit reached!
% 45.29/6.87 % (416709)------------------------------
% 45.29/6.87 % (416709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.29/6.87 % (416709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.29/6.87 % (416709)CaDiCaL version: 2.1.3
% 45.29/6.87 % (416709)Termination reason: Instruction limit
% 45.29/6.87 % (416709)Termination phase: Saturation
% 45.29/6.87 % (416709)Time elapsed: 0.027 s
% 45.29/6.87 % (416709)Peak memory usage: 90 MB
% 45.29/6.87 % (416709)Instructions burned: 115 (million)
% 45.29/6.87 % (416711)lrs+10_1_sil=8000:sp=occurrence:random_seed=3327767671:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 45.29/6.87 % (416712)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=790732567:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 45.29/6.87 % (416714)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3189529095:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 45.29/6.87 % (416712)Refutation not found, incomplete strategy
% 45.29/6.87 % (416712)------------------------------
% 45.29/6.87 % (416712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.29/6.87 % (416712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.29/6.87 % (416712)CaDiCaL version: 2.1.3
% 45.29/6.87 % (416712)Termination reason: Refutation not found, incomplete strategy
% 45.29/6.87 % (416712)Time elapsed: 0.019 s
% 45.29/6.87 % (416712)Peak memory usage: 90 MB
% 45.29/6.87 % (416712)Instructions burned: 35 (million)
% 45.29/6.87 % (416712)------------------------------
% 45.29/6.87 % (416712)------------------------------
% 45.29/6.87 % (416718)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1220626223:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 45.29/6.87 % (416718)Instruction limit reached!
% 45.29/6.87 % (416718)------------------------------
% 45.29/6.87 % (416718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.29/6.87 % (416718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.29/6.87 % (416718)CaDiCaL version: 2.1.3
% 45.29/6.87 % (416718)Termination reason: Instruction limit
% 45.29/6.87 % (416718)Termination phase: Saturation
% 45.29/6.87 % (416718)Time elapsed: 0.067 s
% 45.29/6.87 % (416718)Peak memory usage: 92 MB
% 45.29/6.87 % (416718)Instructions burned: 135 (million)
% 45.29/6.87 % (416711)Instruction limit reached!
% 45.29/6.87 % (416711)------------------------------
% 45.29/6.87 % (416711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.29/6.87 % (416711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.29/6.87 % (416711)CaDiCaL version: 2.1.3
% 45.29/6.87 % (416711)Termination reason: Instruction limit
% 45.29/6.87 % (416711)Termination phase: Saturation
% 45.29/6.87 % (416711)Time elapsed: 0.565 s
% 45.29/6.87 % (416711)Peak memory usage: 101 MB
% 45.29/6.87 % (416711)Instructions burned: 908 (million)
% 45.29/6.87 % (416720)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2371423749:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 45.29/6.87 % (416720)Refutation not found, incomplete strategy
% 45.29/6.87 % (416720)------------------------------
% 45.29/6.87 % (416720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.29/6.87 % (416720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.29/6.87 % (416720)CaDiCaL version: 2.1.3
% 45.29/6.87 % (416720)Termination reason: Refutation not found, incomplete strategy
% 45.29/6.87 % (416720)Time elapsed: 0.019 s
% 45.29/6.87 % (416720)Peak memory usage: 89 MB
% 45.29/6.87 % (416720)Instructions burned: 37 (million)
% 45.29/6.87 % (416721)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3763702477:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 45.29/6.87 % (416720)------------------------------
% 45.29/6.87 % (416720)------------------------------
% 45.29/6.87 % (416724)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=164030659:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 65.14/9.64 % (416724)Instruction limit reached!
% 65.14/9.64 % (416724)------------------------------
% 65.14/9.64 % (416724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.14/9.64 % (416724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.14/9.64 % (416724)CaDiCaL version: 2.1.3
% 65.14/9.64 % (416724)Termination reason: Instruction limit
% 65.14/9.64 % (416724)Termination phase: Saturation
% 65.14/9.64 % (416724)Time elapsed: 0.073 s
% 65.14/9.64 % (416724)Peak memory usage: 92 MB
% 65.14/9.64 % (416724)Instructions burned: 126 (million)
% 65.14/9.64 % (416702)Instruction limit reached!
% 65.14/9.64 % (416702)------------------------------
% 65.14/9.64 % (416702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.14/9.64 % (416702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.14/9.64 % (416702)CaDiCaL version: 2.1.3
% 65.14/9.64 % (416702)Termination reason: Instruction limit
% 65.14/9.64 % (416702)Termination phase: Saturation
% 65.14/9.64 % (416702)Time elapsed: 1.576 s
% 65.14/9.64 % (416702)Peak memory usage: 143 MB
% 65.14/9.64 % (416702)Instructions burned: 2351 (million)
% 65.14/9.64 % (416726)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3793082921:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 65.14/9.64 % (416726)Instruction limit reached!
% 65.14/9.64 % (416726)------------------------------
% 65.14/9.64 % (416726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.14/9.64 % (416726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.14/9.64 % (416726)CaDiCaL version: 2.1.3
% 65.14/9.64 % (416726)Termination reason: Instruction limit
% 65.14/9.64 % (416726)Termination phase: Saturation
% 65.14/9.64 % (416726)Time elapsed: 0.083 s
% 65.14/9.64 % (416726)Peak memory usage: 91 MB
% 65.14/9.64 % (416726)Instructions burned: 134 (million)
% 65.14/9.64 % (416727)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1920845683:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 65.14/9.64 % (416727)Refutation not found, incomplete strategy
% 65.14/9.64 % (416727)------------------------------
% 65.14/9.64 % (416727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.14/9.64 % (416727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.14/9.64 % (416727)CaDiCaL version: 2.1.3
% 65.14/9.64 % (416727)Termination reason: Refutation not found, incomplete strategy
% 65.14/9.64 % (416727)Time elapsed: 0.013 s
% 65.14/9.64 % (416727)Peak memory usage: 89 MB
% 65.14/9.64 % (416727)Instructions burned: 24 (million)
% 65.14/9.64 % (416729)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3013942779:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 65.14/9.64 % (416729)Refutation not found, incomplete strategy
% 65.14/9.64 % (416729)------------------------------
% 65.14/9.64 % (416729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.14/9.64 % (416729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.14/9.64 % (416729)CaDiCaL version: 2.1.3
% 65.14/9.64 % (416729)Termination reason: Refutation not found, incomplete strategy
% 65.14/9.64 % (416729)Time elapsed: 0.028 s
% 65.14/9.64 % (416729)Peak memory usage: 89 MB
% 65.14/9.64 % (416729)Instructions burned: 51 (million)
% 65.14/9.64 % (416727)------------------------------
% 65.14/9.64 % (416727)------------------------------
% 65.14/9.64 % (416714)Instruction limit reached!
% 65.14/9.64 % (416714)------------------------------
% 65.14/9.64 % (416714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.14/9.64 % (416714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.14/9.64 % (416714)CaDiCaL version: 2.1.3
% 65.14/9.64 % (416714)Termination reason: Instruction limit
% 65.14/9.64 % (416714)Termination phase: Saturation
% 65.14/9.64 % (416714)Time elapsed: 1.693 s
% 65.14/9.64 % (416714)Peak memory usage: 160 MB
% 65.14/9.64 % (416714)Instructions burned: 5204 (million)
% 65.14/9.64 % (416733)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=2044900279:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 65.14/9.64 % (416729)------------------------------
% 101.25/14.74 % (416729)------------------------------
% 101.25/14.74 % (416732)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=63839781:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 101.25/14.74 % (416733)Instruction limit reached!
% 101.25/14.74 % (416733)------------------------------
% 101.25/14.74 % (416733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.25/14.74 % (416733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.25/14.74 % (416733)CaDiCaL version: 2.1.3
% 101.25/14.74 % (416733)Termination reason: Instruction limit
% 101.25/14.74 % (416733)Termination phase: Saturation
% 101.25/14.74 % (416733)Time elapsed: 0.045 s
% 101.25/14.74 % (416733)Peak memory usage: 93 MB
% 101.25/14.74 % (416733)Instructions burned: 153 (million)
% 101.25/14.74 % (416736)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1415857351:i=14155:bd=all_2971 on theBenchmark for (2971ds/14155Mi)
% 101.25/14.74 % (416737)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=469135315:i=667:av=off:fsr=off_2971 on theBenchmark for (2971ds/667Mi)
% 101.25/14.74 % (416737)Instruction limit reached!
% 101.25/14.74 % (416737)------------------------------
% 101.25/14.74 % (416737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.25/14.74 % (416737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.25/14.74 % (416737)CaDiCaL version: 2.1.3
% 101.25/14.74 % (416737)Termination reason: Instruction limit
% 101.25/14.74 % (416737)Termination phase: Saturation
% 101.25/14.74 % (416737)Time elapsed: 0.169 s
% 101.25/14.74 % (416737)Peak memory usage: 96 MB
% 101.25/14.74 % (416737)Instructions burned: 671 (million)
% 101.25/14.74 % (416740)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=3408522615:s2a=on:i=185:s2at=1.8:fdi=4_2968 on theBenchmark for (2968ds/185Mi)
% 101.25/14.74 % (416740)Instruction limit reached!
% 101.25/14.74 % (416740)------------------------------
% 101.25/14.74 % (416740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.25/14.74 % (416740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.25/14.74 % (416740)CaDiCaL version: 2.1.3
% 101.25/14.74 % (416740)Termination reason: Instruction limit
% 101.25/14.74 % (416740)Termination phase: Saturation
% 101.25/14.74 % (416740)Time elapsed: 0.047 s
% 101.25/14.74 % (416740)Peak memory usage: 91 MB
% 101.25/14.74 % (416740)Instructions burned: 189 (million)
% 101.25/14.74 % (416742)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2135263479:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2966 on theBenchmark for (2966ds/193Mi)
% 101.25/14.74 % (416742)Instruction limit reached!
% 101.25/14.74 % (416742)------------------------------
% 101.25/14.74 % (416742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.25/14.74 % (416742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.25/14.74 % (416742)CaDiCaL version: 2.1.3
% 101.25/14.74 % (416742)Termination reason: Instruction limit
% 101.25/14.74 % (416742)Termination phase: Saturation
% 101.25/14.74 % (416742)Time elapsed: 0.128 s
% 101.25/14.74 % (416742)Peak memory usage: 92 MB
% 101.25/14.74 % (416742)Instructions burned: 194 (million)
% 101.25/14.74 % (416744)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=859615701:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2963 on theBenchmark for (2963ds/4850Mi)
% 101.25/14.74 % (416732)Instruction limit reached!
% 101.25/14.74 % (416732)------------------------------
% 101.25/14.74 % (416732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.25/14.74 % (416732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.25/14.74 % (416732)CaDiCaL version: 2.1.3
% 101.25/14.74 % (416732)Termination reason: Instruction limit
% 101.25/14.74 % (416732)Termination phase: Saturation
% 101.25/14.74 % (416732)Time elapsed: 3.606 s
% 101.25/14.74 % (416732)Peak memory usage: 153 MB
% 101.25/14.74 % (416732)Instructions burned: 6060 (million)
% 101.25/14.74 % (416744)Instruction limit reached!
% 101.25/14.74 % (416744)------------------------------
% 101.25/14.74 % (416744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.25/14.74 % (416744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.25/14.74 % (416744)CaDiCaL version: 2.1.3
% 101.25/14.74 % (416744)Termination reason: Instruction limit
% 121.82/17.70 % (416744)Termination phase: Saturation
% 121.82/17.70 % (416744)Time elapsed: 2.628 s
% 121.82/17.70 % (416744)Peak memory usage: 146 MB
% 121.82/17.70 % (416744)Instructions burned: 4850 (million)
% 121.82/17.70 % (416746)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3547480117:i=12111:sd=1:ss=included_2935 on theBenchmark for (2935ds/12111Mi)
% 121.82/17.70 % (416747)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1060609246:i=319:kws=precedence:fsr=off_2935 on theBenchmark for (2935ds/319Mi)
% 121.82/17.70 % (416747)Instruction limit reached!
% 121.82/17.70 % (416747)------------------------------
% 121.82/17.70 % (416747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.82/17.70 % (416747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.82/17.70 % (416747)CaDiCaL version: 2.1.3
% 121.82/17.70 % (416747)Termination reason: Instruction limit
% 121.82/17.70 % (416747)Termination phase: Saturation
% 121.82/17.70 % (416747)Time elapsed: 0.134 s
% 121.82/17.70 % (416747)Peak memory usage: 92 MB
% 121.82/17.70 % (416747)Instructions burned: 322 (million)
% 121.82/17.70 % (416750)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=965046975:i=2064:ep=RST_2932 on theBenchmark for (2932ds/2064Mi)
% 121.82/17.70 % (416736)Instruction limit reached!
% 121.82/17.70 % (416736)------------------------------
% 121.82/17.70 % (416736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.82/17.70 % (416736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.82/17.70 % (416736)CaDiCaL version: 2.1.3
% 121.82/17.70 % (416736)Termination reason: Instruction limit
% 121.82/17.70 % (416736)Termination phase: Saturation
% 121.82/17.70 % (416736)Time elapsed: 4.243 s
% 121.82/17.70 % (416736)Peak memory usage: 288 MB
% 121.82/17.70 % (416736)Instructions burned: 14157 (million)
% 121.82/17.70 % (416752)dis-1011_128_sil=32000:random_seed=500022989:i=3706:ep=RST:av=off_2927 on theBenchmark for (2927ds/3706Mi)
% 121.82/17.70 % (416750)Instruction limit reached!
% 121.82/17.70 % (416750)------------------------------
% 121.82/17.70 % (416750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.82/17.70 % (416750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.82/17.70 % (416750)CaDiCaL version: 2.1.3
% 121.82/17.70 % (416750)Termination reason: Instruction limit
% 121.82/17.70 % (416750)Termination phase: Saturation
% 121.82/17.70 % (416750)Time elapsed: 0.934 s
% 121.82/17.70 % (416750)Peak memory usage: 106 MB
% 121.82/17.70 % (416750)Instructions burned: 2065 (million)
% 121.82/17.70 % (416754)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=391150930:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2921 on theBenchmark for (2921ds/757Mi)
% 121.82/17.70 % (416754)Refutation not found, incomplete strategy
% 121.82/17.70 % (416754)------------------------------
% 121.82/17.70 % (416754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.82/17.70 % (416754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.82/17.70 % (416754)CaDiCaL version: 2.1.3
% 121.82/17.70 % (416754)Termination reason: Refutation not found, incomplete strategy
% 121.82/17.70 % (416754)Time elapsed: 0.020 s
% 121.82/17.70 % (416754)Peak memory usage: 89 MB
% 121.82/17.70 % (416754)Instructions burned: 39 (million)
% 121.82/17.70 % (416754)------------------------------
% 121.82/17.70 % (416754)------------------------------
% 121.82/17.70 % (416756)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2632614826:i=13913:ss=axioms:sgt=8_2917 on theBenchmark for (2917ds/13913Mi)
% 121.82/17.70 % (416752)Instruction limit reached!
% 121.82/17.70 % (416752)------------------------------
% 121.82/17.70 % (416752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.82/17.70 % (416752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.82/17.70 % (416752)CaDiCaL version: 2.1.3
% 121.82/17.70 % (416752)Termination reason: Instruction limit
% 121.82/17.70 % (416752)Termination phase: Saturation
% 121.82/17.70 % (416752)Time elapsed: 1.152 s
% 121.82/17.70 % (416752)Peak memory usage: 108 MB
% 121.82/17.70 % (416752)Instructions burned: 3707 (million)
% 121.82/17.70 % (416758)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=593252767:i=9925:aac=none_2914 on theBenchmark for (2914ds/9925Mi)
% 121.82/17.70 % (416721)Instruction limit reached!
% 121.82/17.70 % (416721)------------------------------
% 121.82/17.70 % (416721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.19/20.60 % (416721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.19/20.60 % (416721)CaDiCaL version: 2.1.3
% 143.19/20.60 % (416721)Termination reason: Instruction limit
% 143.19/20.60 % (416721)Termination phase: Saturation
% 143.19/20.60 % (416721)Time elapsed: 7.502 s
% 143.19/20.60 % (416721)Peak memory usage: 246 MB
% 143.19/20.60 % (416721)Instructions burned: 13193 (million)
% 143.19/20.60 % (416760)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4008826158:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2907 on theBenchmark for (2907ds/2479Mi)
% 143.19/20.60 % (416760)Refutation not found, incomplete strategy
% 143.19/20.60 % (416760)------------------------------
% 143.19/20.60 % (416760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.19/20.60 % (416760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.19/20.60 % (416760)CaDiCaL version: 2.1.3
% 143.19/20.60 % (416760)Termination reason: Refutation not found, incomplete strategy
% 143.19/20.60 % (416760)Time elapsed: 0.015 s
% 143.19/20.60 % (416760)Peak memory usage: 89 MB
% 143.19/20.60 % (416760)Instructions burned: 25 (million)
% 143.19/20.60 % (416760)------------------------------
% 143.19/20.60 % (416760)------------------------------
% 143.19/20.60 % (416771)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3189815834:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2903 on theBenchmark for (2903ds/440Mi)
% 143.19/20.60 % (416771)Instruction limit reached!
% 143.19/20.60 % (416771)------------------------------
% 143.19/20.60 % (416771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.19/20.60 % (416771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.19/20.60 % (416771)CaDiCaL version: 2.1.3
% 143.19/20.60 % (416771)Termination reason: Instruction limit
% 143.19/20.60 % (416771)Termination phase: Saturation
% 143.19/20.60 % (416771)Time elapsed: 0.257 s
% 143.19/20.60 % (416771)Peak memory usage: 94 MB
% 143.19/20.60 % (416771)Instructions burned: 441 (million)
% 143.19/20.60 % (416880)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1435266875:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2899 on theBenchmark for (2899ds/11145Mi)
% 143.19/20.60 % (416756)Instruction limit reached!
% 143.19/20.60 % (416756)------------------------------
% 143.19/20.60 % (416756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.19/20.60 % (416756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.19/20.60 % (416756)CaDiCaL version: 2.1.3
% 143.19/20.60 % (416756)Termination reason: Instruction limit
% 143.19/20.60 % (416756)Termination phase: Saturation
% 143.19/20.60 % (416756)Time elapsed: 5.111 s
% 143.19/20.60 % (416756)Peak memory usage: 245 MB
% 143.19/20.60 % (416756)Instructions burned: 13914 (million)
% 143.19/20.60 % (417190)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=2675590473:cts=off:i=3034:av=off:er=known:fsd=on_2864 on theBenchmark for (2864ds/3034Mi)
% 143.19/20.60 % (416746)Instruction limit reached!
% 143.19/20.60 % (416746)------------------------------
% 143.19/20.60 % (416746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.19/20.60 % (416746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.19/20.60 % (416746)CaDiCaL version: 2.1.3
% 143.19/20.60 % (416746)Termination reason: Instruction limit
% 143.19/20.60 % (416746)Termination phase: Saturation
% 143.19/20.60 % (416746)Time elapsed: 7.089 s
% 143.19/20.60 % (416746)Peak memory usage: 267 MB
% 143.19/20.60 % (416746)Instructions burned: 12112 (million)
% 143.19/20.60 % (417192)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2793823095:st=2:s2a=on:i=524:s2at=2:ss=axioms_2862 on theBenchmark for (2862ds/524Mi)
% 143.19/20.60 % (417192)Instruction limit reached!
% 143.19/20.60 % (417192)------------------------------
% 143.19/20.60 % (417192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.19/20.60 % (417192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.19/20.60 % (417192)CaDiCaL version: 2.1.3
% 143.19/20.60 % (417192)Termination reason: Instruction limit
% 143.19/20.60 % (417192)Termination phase: Saturation
% 143.19/20.60 % (417192)Time elapsed: 0.251 s
% 143.19/20.60 % (417192)Peak memory usage: 104 MB
% 143.19/20.60 % (417192)Instructions burned: 525 (million)
% 143.19/20.60 % (417194)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3801039134:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2858 on theBenchmark for (2858ds/1016Mi)
% 175.36/25.17 % (417190)Instruction limit reached!
% 175.36/25.17 % (417190)------------------------------
% 175.36/25.17 % (417190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.36/25.17 % (417190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.36/25.17 % (417190)CaDiCaL version: 2.1.3
% 175.36/25.17 % (417190)Termination reason: Instruction limit
% 175.36/25.17 % (417190)Termination phase: Saturation
% 175.36/25.17 % (417190)Time elapsed: 0.979 s
% 175.36/25.17 % (417190)Peak memory usage: 151 MB
% 175.36/25.17 % (417190)Instructions burned: 3036 (million)
% 175.36/25.17 % (416758)Instruction limit reached!
% 175.36/25.17 % (416758)------------------------------
% 175.36/25.17 % (416758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.36/25.17 % (416758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.36/25.17 % (416758)CaDiCaL version: 2.1.3
% 175.36/25.17 % (416758)Termination reason: Instruction limit
% 175.36/25.17 % (416758)Termination phase: Saturation
% 175.36/25.17 % (416758)Time elapsed: 6.064 s
% 175.36/25.17 % (416758)Peak memory usage: 201 MB
% 175.36/25.17 % (416758)Instructions burned: 9926 (million)
% 175.36/25.17 % (417196)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=161525053:i=14123:bd=preordered:ins=4_2853 on theBenchmark for (2853ds/14123Mi)
% 175.36/25.17 % (417197)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1807528096:i=5781:kws=precedence:bd=all:rawr=on_2852 on theBenchmark for (2852ds/5781Mi)
% 175.36/25.17 % (417194)Instruction limit reached!
% 175.36/25.17 % (417194)------------------------------
% 175.36/25.17 % (417194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.36/25.17 % (417194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.36/25.17 % (417194)CaDiCaL version: 2.1.3
% 175.36/25.17 % (417194)Termination reason: Instruction limit
% 175.36/25.17 % (417194)Termination phase: Saturation
% 175.36/25.17 % (417194)Time elapsed: 0.616 s
% 175.36/25.17 % (417194)Peak memory usage: 127 MB
% 175.36/25.17 % (417194)Instructions burned: 1016 (million)
% 175.36/25.17 % (417200)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2681674494:i=2448:gtgl=5:bd=preordered:gtg=all_2850 on theBenchmark for (2850ds/2448Mi)
% 175.36/25.17 % (417200)Instruction limit reached!
% 175.36/25.17 % (417200)------------------------------
% 175.36/25.17 % (417200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.36/25.17 % (417200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.36/25.17 % (417200)CaDiCaL version: 2.1.3
% 175.36/25.17 % (417200)Termination reason: Instruction limit
% 175.36/25.17 % (417200)Termination phase: Saturation
% 175.36/25.17 % (417200)Time elapsed: 1.371 s
% 175.36/25.17 % (417200)Peak memory usage: 149 MB
% 175.36/25.17 % (417200)Instructions burned: 2450 (million)
% 175.36/25.17 % (417203)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1730404943:i=3223:kws=precedence:fgj=on:av=off_2835 on theBenchmark for (2835ds/3223Mi)
% 175.36/25.17 % (417197)Instruction limit reached!
% 175.36/25.17 % (417197)------------------------------
% 175.36/25.17 % (417197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.36/25.17 % (417197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.36/25.17 % (417197)CaDiCaL version: 2.1.3
% 175.36/25.17 % (417197)Termination reason: Instruction limit
% 175.36/25.17 % (417197)Termination phase: Saturation
% 175.36/25.17 % (417197)Time elapsed: 2.185 s
% 175.36/25.17 % (417197)Peak memory usage: 98 MB
% 175.36/25.17 % (417197)Instructions burned: 5783 (million)
% 175.36/25.17 % (417205)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1642448716:st=5.6:i=2033:sd=3:ss=axioms_2829 on theBenchmark for (2829ds/2033Mi)
% 175.36/25.17 % (416880)Instruction limit reached!
% 175.36/25.17 % (416880)------------------------------
% 175.36/25.17 % (416880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.36/25.17 % (416880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.36/25.17 % (416880)CaDiCaL version: 2.1.3
% 175.36/25.17 % (416880)Termination reason: Instruction limit
% 175.36/25.17 % (416880)Termination phase: Saturation
% 175.36/25.17 % (416880)Time elapsed: 7.066 s
% 175.36/25.17 % (416880)Peak memory usage: 234 MB
% 175.36/25.17 % (416880)Instructions burned: 11146 (million)
% 100.03/31.67 % (417207)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2508127984:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2827 on theBenchmark for (2827ds/2055Mi)
% 100.03/31.67 % (417205)Refutation not found, incomplete strategy
% 100.03/31.67 % (417205)------------------------------
% 100.03/31.67 % (417205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417205)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417205)Termination reason: Refutation not found, incomplete strategy
% 100.03/31.67 % (417205)Time elapsed: 0.650 s
% 100.03/31.67 % (417205)Peak memory usage: 132 MB
% 100.03/31.67 % (417205)Instructions burned: 996 (million)
% 100.03/31.67 % (417205)------------------------------
% 100.03/31.67 % (417205)------------------------------
% 100.03/31.67 % (417209)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=4038309711:i=21611:sd=3:ss=axioms_2818 on theBenchmark for (2818ds/21611Mi)
% 100.03/31.67 % (417203)Instruction limit reached!
% 100.03/31.67 % (417203)------------------------------
% 100.03/31.67 % (417203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417203)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417203)Termination reason: Instruction limit
% 100.03/31.67 % (417203)Termination phase: Saturation
% 100.03/31.67 % (417203)Time elapsed: 2.106 s
% 100.03/31.67 % (417203)Peak memory usage: 144 MB
% 100.03/31.67 % (417203)Instructions burned: 3224 (million)
% 100.03/31.67 % (417207)Instruction limit reached!
% 100.03/31.67 % (417207)------------------------------
% 100.03/31.67 % (417207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417207)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417207)Termination reason: Instruction limit
% 100.03/31.67 % (417207)Termination phase: Saturation
% 100.03/31.67 % (417207)Time elapsed: 1.333 s
% 100.03/31.67 % (417207)Peak memory usage: 138 MB
% 100.03/31.67 % (417207)Instructions burned: 2056 (million)
% 100.03/31.67 % (417211)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2213606455:i=4835:sd=13:ss=axioms:sgt=23_2812 on theBenchmark for (2812ds/4835Mi)
% 100.03/31.67 % (417212)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=753082145:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2812 on theBenchmark for (2812ds/797Mi)
% 100.03/31.67 % (417196)Instruction limit reached!
% 100.03/31.67 % (417196)------------------------------
% 100.03/31.67 % (417196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417196)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417196)Termination reason: Instruction limit
% 100.03/31.67 % (417196)Termination phase: Saturation
% 100.03/31.67 % (417196)Time elapsed: 4.531 s
% 100.03/31.67 % (417196)Peak memory usage: 205 MB
% 100.03/31.67 % (417196)Instructions burned: 14123 (million)
% 100.03/31.67 % (417215)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2294243155:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2806 on theBenchmark for (2806ds/2326Mi)
% 100.03/31.67 % (417212)Instruction limit reached!
% 100.03/31.67 % (417212)------------------------------
% 100.03/31.67 % (417212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417212)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417212)Termination reason: Instruction limit
% 100.03/31.67 % (417212)Termination phase: Saturation
% 100.03/31.67 % (417212)Time elapsed: 0.513 s
% 100.03/31.67 % (417212)Peak memory usage: 102 MB
% 100.03/31.67 % (417212)Instructions burned: 798 (million)
% 100.03/31.67 % (417217)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=23317866:i=6038:nm=6_2805 on theBenchmark for (2805ds/6038Mi)
% 100.03/31.67 % (417215)Instruction limit reached!
% 100.03/31.67 % (417215)------------------------------
% 100.03/31.67 % (417215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417215)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417215)Termination reason: Instruction limit
% 100.03/31.67 % (417215)Termination phase: Saturation
% 100.03/31.67 % (417215)Time elapsed: 0.737 s
% 100.03/31.67 % (417215)Peak memory usage: 109 MB
% 100.03/31.67 % (417215)Instructions burned: 2328 (million)
% 100.03/31.67 % (417219)lrs+10_1_sil=32000:sp=occurrence:random_seed=2657835174:st=2:i=33334:sd=3:ss=included:sgt=32_2798 on theBenchmark for (2798ds/33334Mi)
% 100.03/31.67 % (417211)Instruction limit reached!
% 100.03/31.67 % (417211)------------------------------
% 100.03/31.67 % (417211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417211)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417211)Termination reason: Instruction limit
% 100.03/31.67 % (417211)Termination phase: Saturation
% 100.03/31.67 % (417211)Time elapsed: 2.618 s
% 100.03/31.67 % (417211)Peak memory usage: 130 MB
% 100.03/31.67 % (417211)Instructions burned: 4835 (million)
% 100.03/31.67 % (417217)Instruction limit reached!
% 100.03/31.67 % (417217)------------------------------
% 100.03/31.67 % (417217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417217)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417217)Termination reason: Instruction limit
% 100.03/31.67 % (417217)Termination phase: Saturation
% 100.03/31.67 % (417217)Time elapsed: 1.969 s
% 100.03/31.67 % (417217)Peak memory usage: 193 MB
% 100.03/31.67 % (417217)Instructions burned: 6038 (million)
% 100.03/31.67 % (417222)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3959062036:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2784 on theBenchmark for (2784ds/1008Mi)
% 100.03/31.67 % (417223)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=1081568346:i=8327:s2at=5:bd=preordered_2783 on theBenchmark for (2783ds/8327Mi)
% 100.03/31.67 % (417222)Instruction limit reached!
% 100.03/31.67 % (417222)------------------------------
% 100.03/31.67 % (417222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417222)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417222)Termination reason: Instruction limit
% 100.03/31.67 % (417222)Termination phase: Saturation
% 100.03/31.67 % (417222)Time elapsed: 0.435 s
% 100.03/31.67 % (417222)Peak memory usage: 94 MB
% 100.03/31.67 % (417222)Instructions burned: 1010 (million)
% 100.03/31.67 % (417226)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=2782575224:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2778 on theBenchmark for (2778ds/1083Mi)
% 100.03/31.67 % (417226)Instruction limit reached!
% 100.03/31.67 % (417226)------------------------------
% 100.03/31.67 % (417226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417226)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417226)Termination reason: Instruction limit
% 100.03/31.67 % (417226)Termination phase: Saturation
% 100.03/31.67 % (417226)Time elapsed: 0.410 s
% 100.03/31.67 % (417226)Peak memory usage: 96 MB
% 100.03/31.67 % (417226)Instructions burned: 1083 (million)
% 100.03/31.67 % (417228)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1059746474:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2772 on theBenchmark for (2772ds/1084Mi)
% 100.03/31.67 % (417228)Instruction limit reached!
% 100.03/31.67 % (417228)------------------------------
% 100.03/31.67 % (417228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417228)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417228)Termination reason: Instruction limit
% 100.03/31.67 % (417228)Termination phase: Saturation
% 100.03/31.67 % (417228)Time elapsed: 0.559 s
% 100.03/31.67 % (417228)Peak memory usage: 95 MB
% 100.03/31.67 % (417228)Instructions burned: 1084 (million)
% 100.03/31.67 % (417230)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2313307380:i=6995:s2at=5:gtg=all_2765 on theBenchmark for (2765ds/6995Mi)
% 100.03/31.67 % (417223)Instruction limit reached!
% 100.03/31.67 % (417223)------------------------------
% 100.03/31.67 % (417223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417223)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417223)Termination reason: Instruction limit
% 100.03/31.67 % (417223)Termination phase: Saturation
% 100.03/31.67 % (417223)Time elapsed: 2.995 s
% 100.03/31.67 % (417223)Peak memory usage: 193 MB
% 100.03/31.67 % (417223)Instructions burned: 8331 (million)
% 100.03/31.67 % (417325)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=111558682:st=2:i=6225:sd=15:ss=axioms_2752 on theBenchmark for (2752ds/6225Mi)
% 100.03/31.67 % (417325)Instruction limit reached!
% 100.03/31.67 % (417325)------------------------------
% 100.03/31.67 % (417325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417325)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417325)Termination reason: Instruction limit
% 100.03/31.67 % (417325)Termination phase: Saturation
% 100.03/31.67 % (417325)Time elapsed: 2.343 s
% 100.03/31.67 % (417325)Peak memory usage: 211 MB
% 100.03/31.67 % (417325)Instructions burned: 6226 (million)
% 100.03/31.67 % (417542)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3642150772:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2727 on theBenchmark for (2727ds/3372Mi)
% 100.03/31.67 % (417230)Instruction limit reached!
% 100.03/31.67 % (417230)------------------------------
% 100.03/31.67 % (417230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417230)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417230)Termination reason: Instruction limit
% 100.03/31.67 % (417230)Termination phase: Saturation
% 100.03/31.67 % (417230)Time elapsed: 4.783 s
% 100.03/31.67 % (417230)Peak memory usage: 165 MB
% 100.03/31.67 % (417230)Instructions burned: 6996 (million)
% 100.03/31.67 % (417652)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=3781046299:st=2.3:i=26457:sd=10:ss=included:sgt=8_2715 on theBenchmark for (2715ds/26457Mi)
% 100.03/31.67 % (417542)Instruction limit reached!
% 100.03/31.67 % (417542)------------------------------
% 100.03/31.67 % (417542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.03/31.67 % (417542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.03/31.67 % (417542)CaDiCaL version: 2.1.3
% 100.03/31.67 % (417542)Termination reason: Instruction limit
% 100.03/31.67 % (417542)Termination phase: Saturation
% 100.03/31.67 % (417542)Time elapsed: 1.399 s
% 100.03/31.67 % (417542)Peak memory usage: 149 MB
% 100.03/31.67 % (417542)Instructions burned: 3375 (million)
% 100.03/31.67 % (417701)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=1976779645:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2711 on theBenchmark for (2711ds/13494Mi)
% 100.03/31.67 % (417652)First to succeed.
% 100.03/31.67 % (417652)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-416675"
% 100.03/31.67 % (417652)Refutation found. Thanks to Tanya!
% 100.03/31.67 % SZS status Theorem for theBenchmark
% 100.03/31.67 % SZS output start Proof for theBenchmark
% See solution above
% 221.71/31.87 % (417652)------------------------------
% 221.71/31.87 % (417652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 221.71/31.87 % (417652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.71/31.87 % (417652)CaDiCaL version: 2.1.3
% 221.71/31.87 % (417652)Termination reason: Refutation
% 221.71/31.87 % (417652)Time elapsed: 2.334 s
% 221.71/31.87 % (417652)Peak memory usage: 157 MB
% 221.71/31.87 % (417652)Instructions burned: 3861 (million)
% 221.71/31.87 % (417652)------------------------------
% 221.71/31.87 % (417652)------------------------------
% 221.71/31.87 % (416675)Success in time 31.239 s
% 221.71/31.87 % Vampire exiting
%------------------------------------------------------------------------------