%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COL096-2 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:37:56 AM UTC 2026
% Result : Unsatisfiable 16.95s 3.01s
% Output : Refutation 18.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 40
% Syntax : Number of formulae : 170 ( 27 unt; 15 def)
% Number of atoms : 389 ( 40 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 427 ( 208 ~; 204 |; 0 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 22 ( 20 usr; 16 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 8 con; 0-3 aty)
% Number of variables : 103 ( 0 sgn 103 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f158,axiom,
! [X0,X1] : combK != comb_app(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',k_app) ).
fof(f160,axiom,
! [X2,X3,X0,X1] :
( comb_app(X0,X1) != comb_app(X2,X3)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',app_app1) ).
fof(f161,axiom,
! [X2,X3,X0,X1] :
( comb_app(X0,X1) != comb_app(X2,X3)
| X1 = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',app_app2) ).
fof(f163,axiom,
! [X0,X1] :
( ~ member(comb_app(X0,X1),comb)
| member(X0,comb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_E1) ).
fof(f164,axiom,
! [X0,X1] :
( ~ member(comb_app(X0,X1),comb)
| member(X1,comb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_E2) ).
fof(f193,axiom,
! [X0] :
( member(pair(X0,X0),parcontract)
| ~ member(X0,comb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',parcontract_intros1) ).
fof(f195,axiom,
! [X2,X0,X1] :
( member(pair(comb_app(comb_app(comb_app(combS,X0),X1),X2),comb_app(comb_app(X0,X2),comb_app(X1,X2))),parcontract)
| ~ member(X1,comb)
| ~ member(X2,comb)
| ~ member(X0,comb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',parcontract_intros3) ).
fof(f196,axiom,
! [X2,X3,X0,X1] :
( member(pair(comb_app(X0,X2),comb_app(X1,X3)),parcontract)
| ~ member(pair(X2,X3),parcontract)
| ~ member(pair(X0,X1),parcontract) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',parcontract_intros4) ).
fof(f203,axiom,
! [X2,X0,X1] :
( ~ member(pair(comb_app(X0,X1),X2),parcontract)
| ap_parcontractE_c1(X0,X1,X2)
| ap_parcontractE_c2(X0,X1,X2)
| ap_parcontractE_c3(X0,X1,X2)
| ap_parcontractE_c4(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE1) ).
fof(f205,axiom,
! [X2,X0,X1] :
( ~ ap_parcontractE_c1(X0,X1,X2)
| X2 = comb_app(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE3) ).
fof(f206,plain,
! [X2,X0,X1] :
( ~ ap_parcontractE_c1(X0,X1,X2)
| comb_app(X0,X1) = X2 ),
inference(reorient_equations,[],[f205]) ).
fof(f209,axiom,
! [X2,X0,X1] :
( ~ ap_parcontractE_c2(X0,X1,X2)
| X0 = comb_app(combK,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE6) ).
fof(f210,plain,
! [X2,X0,X1] :
( ~ ap_parcontractE_c2(X0,X1,X2)
| comb_app(combK,X2) = X0 ),
inference(reorient_equations,[],[f209]) ).
fof(f214,axiom,
! [X2,X0,X1] :
( ~ ap_parcontractE_c3(X0,X1,X2)
| X2 = comb_app(comb_app(ap_parcontractE_sk1p(X0,X1,X2),X1),comb_app(ap_parcontractE_sk1q(X0,X1,X2),X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE10) ).
fof(f215,plain,
! [X2,X0,X1] :
( ~ ap_parcontractE_c3(X0,X1,X2)
| comb_app(comb_app(ap_parcontractE_sk1p(X0,X1,X2),X1),comb_app(ap_parcontractE_sk1q(X0,X1,X2),X1)) = X2 ),
inference(reorient_equations,[],[f214]) ).
fof(f216,axiom,
! [X2,X0,X1] :
( ~ ap_parcontractE_c3(X0,X1,X2)
| X0 = comb_app(comb_app(combS,ap_parcontractE_sk1p(X0,X1,X2)),ap_parcontractE_sk1q(X0,X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE11) ).
fof(f217,plain,
! [X2,X0,X1] :
( ~ ap_parcontractE_c3(X0,X1,X2)
| comb_app(comb_app(combS,ap_parcontractE_sk1p(X0,X1,X2)),ap_parcontractE_sk1q(X0,X1,X2)) = X0 ),
inference(reorient_equations,[],[f216]) ).
fof(f218,axiom,
! [X2,X0,X1] :
( member(pair(X0,ap_parcontractE_sk2q(X0,X1,X2)),parcontract)
| ~ ap_parcontractE_c4(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE12) ).
fof(f219,axiom,
! [X2,X0,X1] :
( member(pair(X1,ap_parcontractE_sk2s(X0,X1,X2)),parcontract)
| ~ ap_parcontractE_c4(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE13) ).
fof(f220,axiom,
! [X2,X0,X1] :
( ~ ap_parcontractE_c4(X0,X1,X2)
| X2 = comb_app(ap_parcontractE_sk2q(X0,X1,X2),ap_parcontractE_sk2s(X0,X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE14) ).
fof(f221,plain,
! [X2,X0,X1] :
( ~ ap_parcontractE_c4(X0,X1,X2)
| comb_app(ap_parcontractE_sk2q(X0,X1,X2),ap_parcontractE_sk2s(X0,X1,X2)) = X2 ),
inference(reorient_equations,[],[f220]) ).
fof(f228,axiom,
! [X2,X0,X1] :
( ~ member(pair(comb_app(comb_app(combS,X0),X1),X2),parcontract)
| X2 = comb_app(comb_app(combS,s2_parcontractD_sk1p(X0,X1,X2)),s2_parcontractD_sk1q(X0,X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_parcontractD_1) ).
fof(f229,plain,
! [X2,X0,X1] :
( ~ member(pair(comb_app(comb_app(combS,X0),X1),X2),parcontract)
| comb_app(comb_app(combS,s2_parcontractD_sk1p(X0,X1,X2)),s2_parcontractD_sk1q(X0,X1,X2)) = X2 ),
inference(reorient_equations,[],[f228]) ).
fof(f230,axiom,
! [X2,X0,X1] :
( ~ member(pair(comb_app(comb_app(combS,X0),X1),X2),parcontract)
| member(pair(X0,s2_parcontractD_sk1p(X0,X1,X2)),parcontract) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_parcontractD_2) ).
fof(f231,axiom,
! [X2,X0,X1] :
( ~ member(pair(comb_app(comb_app(combS,X0),X1),X2),parcontract)
| member(pair(X1,s2_parcontractD_sk1q(X0,X1,X2)),parcontract) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_parcontractD_3) ).
fof(f238,axiom,
! [X0,X1] :
( ~ member(pair(X0,X1),parcontract)
| member(X1,comb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',parcontract_combD2) ).
fof(f239,axiom,
member(p,comb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diamond_parcontract_3h1) ).
fof(f240,axiom,
member(q,comb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diamond_parcontract_3h2) ).
fof(f241,axiom,
member(r,comb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diamond_parcontract_3h3) ).
fof(f242,negated_conjecture,
member(pair(comb_app(comb_app(comb_app(combS,p),q),r),yp),parcontract),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diamond_parcontract_3c1) ).
fof(f243,negated_conjecture,
! [X0] :
( ~ member(pair(comb_app(comb_app(p,r),comb_app(q,r)),X0),parcontract)
| ~ member(pair(yp,X0),parcontract) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diamond_parcontract_3c2) ).
fof(f278,plain,
! [X2,X3,X0,X1] :
( member(pair(X0,s2_parcontractD_sk1p(X0,X1,ap_parcontractE_sk2q(comb_app(comb_app(combS,X0),X1),X2,X3))),parcontract)
| ~ ap_parcontractE_c4(comb_app(comb_app(combS,X0),X1),X2,X3) ),
inference(resolution,[],[f230,f218]) ).
fof(f279,plain,
( ap_parcontractE_c1(comb_app(comb_app(combS,p),q),r,yp)
| ap_parcontractE_c2(comb_app(comb_app(combS,p),q),r,yp)
| ap_parcontractE_c3(comb_app(comb_app(combS,p),q),r,yp)
| ap_parcontractE_c4(comb_app(comb_app(combS,p),q),r,yp) ),
inference(resolution,[],[f203,f242]) ).
fof(f283,definition,
( spl0_5
<=> ap_parcontractE_c4(comb_app(comb_app(combS,p),q),r,yp) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f285,plain,
( ap_parcontractE_c4(comb_app(comb_app(combS,p),q),r,yp)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f287,definition,
( spl0_6
<=> ap_parcontractE_c3(comb_app(comb_app(combS,p),q),r,yp) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f289,plain,
( ap_parcontractE_c3(comb_app(comb_app(combS,p),q),r,yp)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f291,definition,
( spl0_7
<=> ap_parcontractE_c2(comb_app(comb_app(combS,p),q),r,yp) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f293,plain,
( ap_parcontractE_c2(comb_app(comb_app(combS,p),q),r,yp)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f295,definition,
( spl0_8
<=> ap_parcontractE_c1(comb_app(comb_app(combS,p),q),r,yp) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f297,plain,
( ap_parcontractE_c1(comb_app(comb_app(combS,p),q),r,yp)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f298,plain,
( spl0_5
| spl0_6
| spl0_7
| spl0_8 ),
inference(avatar_split_clause,[],[f279,f295,f291,f287,f283]) ).
fof(f300,plain,
! [X2,X3,X0,X1] :
( member(pair(X0,s2_parcontractD_sk1q(X1,X0,ap_parcontractE_sk2q(comb_app(comb_app(combS,X1),X0),X2,X3))),parcontract)
| ~ ap_parcontractE_c4(comb_app(comb_app(combS,X1),X0),X2,X3) ),
inference(resolution,[],[f231,f218]) ).
fof(f309,plain,
( ~ member(comb_app(comb_app(p,r),comb_app(q,r)),comb)
| ~ member(pair(yp,comb_app(comb_app(p,r),comb_app(q,r))),parcontract) ),
inference(resolution,[],[f193,f243]) ).
fof(f313,plain,
~ member(pair(yp,comb_app(comb_app(p,r),comb_app(q,r))),parcontract),
inference(forward_subsumption_resolution,[],[f309,f238]) ).
fof(f315,plain,
! [X2,X3,X0,X1] :
( ~ ap_parcontractE_c4(comb_app(comb_app(combS,X0),X1),X2,X3)
| ap_parcontractE_sk2q(comb_app(comb_app(combS,X0),X1),X2,X3) = comb_app(comb_app(combS,s2_parcontractD_sk1p(X0,X1,ap_parcontractE_sk2q(comb_app(comb_app(combS,X0),X1),X2,X3))),s2_parcontractD_sk1q(X0,X1,ap_parcontractE_sk2q(comb_app(comb_app(combS,X0),X1),X2,X3))) ),
inference(resolution,[],[f229,f218]) ).
fof(f345,plain,
( ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp) = comb_app(comb_app(combS,s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp))),s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)))
| ~ spl0_5 ),
inference(resolution,[],[f315,f285]) ).
fof(f346,plain,
( yp = comb_app(ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp),ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp))
| ~ spl0_5 ),
inference(resolution,[],[f221,f285]) ).
fof(f348,plain,
( ~ member(yp,comb)
| member(ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp),comb)
| ~ spl0_5 ),
inference(superposition,[],[f164,f346]) ).
fof(f349,plain,
( ~ member(yp,comb)
| member(ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp),comb)
| ~ spl0_5 ),
inference(superposition,[],[f163,f346]) ).
fof(f354,definition,
( spl0_9
<=> member(ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp),comb) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f355,plain,
( member(ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp),comb)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f358,definition,
( spl0_10
<=> member(ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp),comb) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f359,plain,
( member(ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp),comb)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f370,definition,
( spl0_13
<=> member(yp,comb) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f371,plain,
( member(yp,comb)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f372,plain,
( ~ member(yp,comb)
| spl0_13 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f373,plain,
( spl0_9
| ~ spl0_13
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f349,f283,f370,f354]) ).
fof(f374,plain,
( spl0_10
| ~ spl0_13
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f348,f283,f370,f358]) ).
fof(f415,plain,
( ! [X0] :
( member(pair(comb_app(ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp),X0),comb_app(comb_app(s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),X0),comb_app(s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),X0))),parcontract)
| ~ member(s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),comb)
| ~ member(X0,comb)
| ~ member(s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),comb) )
| ~ spl0_5 ),
inference(superposition,[],[f195,f345]) ).
fof(f436,definition,
( spl0_14
<=> member(s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),comb) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f438,plain,
( ~ member(s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),comb)
| spl0_14 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f440,definition,
( spl0_15
<=> member(comb_app(combS,s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp))),comb) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f441,plain,
( member(comb_app(combS,s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp))),comb)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f440]) ).
fof(f453,definition,
( spl0_18
<=> member(s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),comb) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f455,plain,
( ~ member(s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),comb)
| spl0_18 ),
inference(avatar_component_clause,[],[f453]) ).
fof(f457,definition,
( spl0_19
<=> ! [X0] :
( member(pair(comb_app(ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp),X0),comb_app(comb_app(s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),X0),comb_app(s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),X0))),parcontract)
| ~ member(X0,comb) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f458,plain,
( ! [X0] :
( member(pair(comb_app(ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp),X0),comb_app(comb_app(s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),X0),comb_app(s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),X0))),parcontract)
| ~ member(X0,comb) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f459,plain,
( ~ spl0_18
| ~ spl0_14
| spl0_19
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f415,f283,f457,f436,f453]) ).
fof(f481,plain,
member(yp,comb),
inference(resolution,[],[f238,f242]) ).
fof(f495,plain,
( $false
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f481,f372]) ).
fof(f496,plain,
spl0_13,
inference(avatar_contradiction_clause,[],[f495]) ).
fof(f689,plain,
( comb_app(comb_app(combS,p),q) = comb_app(combK,yp)
| ~ spl0_7 ),
inference(resolution,[],[f293,f210]) ).
fof(f709,plain,
( ! [X0,X1] :
( comb_app(X0,X1) != comb_app(combK,yp)
| comb_app(combS,p) = X0 )
| ~ spl0_7 ),
inference(superposition,[],[f160,f689]) ).
fof(f770,plain,
( combK = comb_app(combS,p)
| ~ spl0_7 ),
inference(equality_resolution,[],[f709]) ).
fof(f771,plain,
( $false
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f770,f158]) ).
fof(f772,plain,
~ spl0_7,
inference(avatar_contradiction_clause,[],[f771]) ).
fof(f773,plain,
( comb_app(comb_app(comb_app(combS,p),q),r) = yp
| ~ spl0_8 ),
inference(resolution,[],[f297,f206]) ).
fof(f776,plain,
( member(pair(yp,comb_app(comb_app(p,r),comb_app(q,r))),parcontract)
| ~ member(q,comb)
| ~ member(r,comb)
| ~ member(p,comb)
| ~ spl0_8 ),
inference(superposition,[],[f195,f773]) ).
fof(f791,plain,
( ~ member(q,comb)
| ~ member(r,comb)
| ~ member(p,comb)
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f776,f313]) ).
fof(f794,plain,
( ~ member(r,comb)
| ~ member(p,comb)
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f791,f240]) ).
fof(f795,plain,
( ~ member(p,comb)
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f794,f241]) ).
fof(f796,plain,
( $false
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f795,f239]) ).
fof(f797,plain,
~ spl0_8,
inference(avatar_contradiction_clause,[],[f796]) ).
fof(f800,plain,
( ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp) = comb_app(comb_app(combS,s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp))),s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)))
| ~ spl0_5 ),
inference(resolution,[],[f285,f315]) ).
fof(f834,plain,
! [X0,X1] :
( ~ member(pair(yp,comb_app(X1,X0)),parcontract)
| ~ member(pair(comb_app(p,r),X1),parcontract)
| ~ member(pair(comb_app(q,r),X0),parcontract) ),
inference(resolution,[],[f196,f243]) ).
fof(f907,plain,
( ~ member(ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp),comb)
| member(comb_app(combS,s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp))),comb)
| ~ spl0_5 ),
inference(superposition,[],[f163,f800]) ).
fof(f908,plain,
( ~ member(ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp),comb)
| member(s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),comb)
| ~ spl0_5 ),
inference(superposition,[],[f164,f800]) ).
fof(f950,plain,
( member(s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),comb)
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f908,f355]) ).
fof(f951,plain,
( member(comb_app(combS,s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp))),comb)
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f907,f355]) ).
fof(f952,plain,
( $false
| ~ spl0_5
| ~ spl0_9
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f950,f438]) ).
fof(f953,plain,
( ~ spl0_5
| ~ spl0_9
| spl0_14 ),
inference(avatar_contradiction_clause,[],[f952]) ).
fof(f954,plain,
( spl0_15
| ~ spl0_5
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f951,f354,f283,f440]) ).
fof(f955,plain,
( comb_app(comb_app(combS,p),q) = comb_app(comb_app(combS,ap_parcontractE_sk1p(comb_app(comb_app(combS,p),q),r,yp)),ap_parcontractE_sk1q(comb_app(comb_app(combS,p),q),r,yp))
| ~ spl0_6 ),
inference(resolution,[],[f289,f217]) ).
fof(f967,plain,
( ! [X0,X1] :
( comb_app(X0,X1) != comb_app(comb_app(combS,p),q)
| comb_app(combS,ap_parcontractE_sk1p(comb_app(comb_app(combS,p),q),r,yp)) = X0 )
| ~ spl0_6 ),
inference(superposition,[],[f160,f955]) ).
fof(f969,plain,
( ! [X0,X1] :
( comb_app(X0,X1) != comb_app(comb_app(combS,p),q)
| ap_parcontractE_sk1q(comb_app(comb_app(combS,p),q),r,yp) = X1 )
| ~ spl0_6 ),
inference(superposition,[],[f161,f955]) ).
fof(f1013,plain,
( q = ap_parcontractE_sk1q(comb_app(comb_app(combS,p),q),r,yp)
| ~ spl0_6 ),
inference(equality_resolution,[],[f969]) ).
fof(f1015,plain,
( comb_app(combS,p) = comb_app(combS,ap_parcontractE_sk1p(comb_app(comb_app(combS,p),q),r,yp))
| ~ spl0_6 ),
inference(equality_resolution,[],[f967]) ).
fof(f1038,plain,
( ! [X0,X1] :
( comb_app(X0,X1) != comb_app(combS,p)
| ap_parcontractE_sk1p(comb_app(comb_app(combS,p),q),r,yp) = X1 )
| ~ spl0_6 ),
inference(superposition,[],[f161,f1015]) ).
fof(f1102,plain,
( p = ap_parcontractE_sk1p(comb_app(comb_app(combS,p),q),r,yp)
| ~ spl0_6 ),
inference(equality_resolution,[],[f1038]) ).
fof(f1488,plain,
( yp = comb_app(comb_app(ap_parcontractE_sk1p(comb_app(comb_app(combS,p),q),r,yp),r),comb_app(ap_parcontractE_sk1q(comb_app(comb_app(combS,p),q),r,yp),r))
| ~ spl0_6 ),
inference(resolution,[],[f215,f289]) ).
fof(f1489,plain,
( yp = comb_app(comb_app(ap_parcontractE_sk1p(comb_app(comb_app(combS,p),q),r,yp),r),comb_app(q,r))
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1488,f1013]) ).
fof(f1490,plain,
( yp = comb_app(comb_app(p,r),comb_app(q,r))
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1489,f1102]) ).
fof(f1491,plain,
( ! [X0] :
( ~ member(pair(yp,X0),parcontract)
| ~ member(pair(yp,X0),parcontract) )
| ~ spl0_6 ),
inference(superposition,[],[f243,f1490]) ).
fof(f1533,plain,
( ! [X0] : ~ member(pair(yp,X0),parcontract)
| ~ spl0_6 ),
inference(duplicate_literal_removal,[],[f1491]) ).
fof(f1627,plain,
( ~ member(yp,comb)
| ~ spl0_6 ),
inference(resolution,[],[f1533,f193]) ).
fof(f1641,plain,
( $false
| ~ spl0_6
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f1627,f371]) ).
fof(f1642,plain,
( ~ spl0_6
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f1641]) ).
fof(f1668,plain,
( yp = comb_app(ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp),ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp))
| ~ spl0_5 ),
inference(resolution,[],[f285,f221]) ).
fof(f1708,plain,
( member(s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),comb)
| ~ spl0_15 ),
inference(resolution,[],[f441,f164]) ).
fof(f1710,plain,
( $false
| ~ spl0_15
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1708,f455]) ).
fof(f1711,plain,
( ~ spl0_15
| spl0_18 ),
inference(avatar_contradiction_clause,[],[f1710]) ).
fof(f1722,plain,
( member(pair(yp,comb_app(comb_app(s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp)),comb_app(s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp)))),parcontract)
| ~ member(ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp),comb)
| ~ spl0_5
| ~ spl0_19 ),
inference(superposition,[],[f458,f1668]) ).
fof(f1723,plain,
( member(pair(yp,comb_app(comb_app(s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp)),comb_app(s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp)))),parcontract)
| ~ spl0_5
| ~ spl0_10
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1722,f359]) ).
fof(f1724,plain,
( ~ member(pair(comb_app(p,r),comb_app(s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp))),parcontract)
| ~ member(pair(comb_app(q,r),comb_app(s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp))),parcontract)
| ~ spl0_5
| ~ spl0_10
| ~ spl0_19 ),
inference(resolution,[],[f1723,f834]) ).
fof(f1727,definition,
( spl0_87
<=> member(pair(comb_app(q,r),comb_app(s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp))),parcontract) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f1729,plain,
( ~ member(pair(comb_app(q,r),comb_app(s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp))),parcontract)
| spl0_87 ),
inference(avatar_component_clause,[],[f1727]) ).
fof(f1731,definition,
( spl0_88
<=> member(pair(comb_app(p,r),comb_app(s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp))),parcontract) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f1733,plain,
( ~ member(pair(comb_app(p,r),comb_app(s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp)),ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp))),parcontract)
| spl0_88 ),
inference(avatar_component_clause,[],[f1731]) ).
fof(f1734,plain,
( ~ spl0_87
| ~ spl0_88
| ~ spl0_5
| ~ spl0_10
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f1724,f457,f358,f283,f1731,f1727]) ).
fof(f1735,plain,
( ~ member(pair(r,ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp)),parcontract)
| ~ member(pair(q,s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp))),parcontract)
| spl0_87 ),
inference(resolution,[],[f1729,f196]) ).
fof(f1737,definition,
( spl0_89
<=> member(pair(q,s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp))),parcontract) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f1739,plain,
( ~ member(pair(q,s2_parcontractD_sk1q(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp))),parcontract)
| spl0_89 ),
inference(avatar_component_clause,[],[f1737]) ).
fof(f1741,definition,
( spl0_90
<=> member(pair(r,ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp)),parcontract) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f1742,plain,
( member(pair(r,ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp)),parcontract)
| ~ spl0_90 ),
inference(avatar_component_clause,[],[f1741]) ).
fof(f1743,plain,
( ~ member(pair(r,ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp)),parcontract)
| spl0_90 ),
inference(avatar_component_clause,[],[f1741]) ).
fof(f1744,plain,
( ~ spl0_89
| ~ spl0_90
| spl0_87 ),
inference(avatar_split_clause,[],[f1735,f1727,f1741,f1737]) ).
fof(f1745,plain,
( ~ ap_parcontractE_c4(comb_app(comb_app(combS,p),q),r,yp)
| spl0_89 ),
inference(resolution,[],[f1739,f300]) ).
fof(f1746,plain,
( $false
| ~ spl0_5
| spl0_89 ),
inference(forward_subsumption_resolution,[],[f1745,f285]) ).
fof(f1747,plain,
( ~ spl0_5
| spl0_89 ),
inference(avatar_contradiction_clause,[],[f1746]) ).
fof(f1818,plain,
( ~ ap_parcontractE_c4(comb_app(comb_app(combS,p),q),r,yp)
| spl0_90 ),
inference(resolution,[],[f1743,f219]) ).
fof(f1819,plain,
( $false
| ~ spl0_5
| spl0_90 ),
inference(forward_subsumption_resolution,[],[f1818,f285]) ).
fof(f1820,plain,
( ~ spl0_5
| spl0_90 ),
inference(avatar_contradiction_clause,[],[f1819]) ).
fof(f1840,plain,
( ~ member(pair(r,ap_parcontractE_sk2s(comb_app(comb_app(combS,p),q),r,yp)),parcontract)
| ~ member(pair(p,s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp))),parcontract)
| spl0_88 ),
inference(resolution,[],[f1733,f196]) ).
fof(f1841,plain,
( ~ member(pair(p,s2_parcontractD_sk1p(p,q,ap_parcontractE_sk2q(comb_app(comb_app(combS,p),q),r,yp))),parcontract)
| spl0_88
| ~ spl0_90 ),
inference(forward_subsumption_resolution,[],[f1840,f1742]) ).
fof(f1842,plain,
( ~ ap_parcontractE_c4(comb_app(comb_app(combS,p),q),r,yp)
| spl0_88
| ~ spl0_90 ),
inference(resolution,[],[f1841,f278]) ).
fof(f1843,plain,
( $false
| ~ spl0_5
| spl0_88
| ~ spl0_90 ),
inference(forward_subsumption_resolution,[],[f1842,f285]) ).
fof(f1844,plain,
( ~ spl0_5
| spl0_88
| ~ spl0_90 ),
inference(avatar_contradiction_clause,[],[f1843]) ).
cnf(s5,plain,
( spl0_5
| spl0_6
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f298]) ).
cnf(s8,plain,
( ~ spl0_5
| spl0_9
| ~ spl0_13 ),
inference(sat_conversion,[],[f373]) ).
cnf(s9,plain,
( ~ spl0_5
| spl0_10
| ~ spl0_13 ),
inference(sat_conversion,[],[f374]) ).
cnf(s13,plain,
( ~ spl0_5
| ~ spl0_14
| ~ spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f459]) ).
cnf(s15,plain,
spl0_13,
inference(sat_conversion,[],[f496]) ).
cnf(s32,plain,
~ spl0_7,
inference(sat_conversion,[],[f772]) ).
cnf(s34,plain,
~ spl0_8,
inference(sat_conversion,[],[f797]) ).
cnf(s43,plain,
( ~ spl0_5
| ~ spl0_9
| spl0_14 ),
inference(sat_conversion,[],[f953]) ).
cnf(s44,plain,
( ~ spl0_5
| ~ spl0_9
| spl0_15 ),
inference(sat_conversion,[],[f954]) ).
cnf(s68,plain,
( ~ spl0_6
| ~ spl0_13 ),
inference(sat_conversion,[],[f1642]) ).
cnf(s71,plain,
( ~ spl0_15
| spl0_18 ),
inference(sat_conversion,[],[f1711]) ).
cnf(s73,plain,
( ~ spl0_5
| ~ spl0_10
| ~ spl0_19
| ~ spl0_87
| ~ spl0_88 ),
inference(sat_conversion,[],[f1734]) ).
cnf(s74,plain,
( spl0_87
| ~ spl0_89
| ~ spl0_90 ),
inference(sat_conversion,[],[f1744]) ).
cnf(s75,plain,
( ~ spl0_5
| spl0_89 ),
inference(sat_conversion,[],[f1747]) ).
cnf(s77,plain,
( ~ spl0_5
| spl0_90 ),
inference(sat_conversion,[],[f1820]) ).
cnf(s79,plain,
( ~ spl0_5
| spl0_88
| ~ spl0_90 ),
inference(sat_conversion,[],[f1844]) ).
cnf(s81,plain,
~ spl0_6,
inference(rat,[],[s68,s15]) ).
cnf(s82,plain,
( ~ spl0_5
| spl0_10 ),
inference(rat,[],[s9,s15]) ).
cnf(s83,plain,
( ~ spl0_5
| spl0_9 ),
inference(rat,[],[s8,s15]) ).
cnf(s84,plain,
spl0_5,
inference(rat,[],[s5,s34,s32,s81]) ).
cnf(s85,plain,
spl0_90,
inference(rat,[],[s77,s84]) ).
cnf(s86,plain,
spl0_89,
inference(rat,[],[s75,s84]) ).
cnf(s87,plain,
spl0_10,
inference(rat,[],[s82,s84]) ).
cnf(s88,plain,
spl0_9,
inference(rat,[],[s83,s84]) ).
cnf(s89,plain,
spl0_88,
inference(rat,[],[s79,s84,s85]) ).
cnf(s90,plain,
spl0_87,
inference(rat,[],[s74,s85,s86]) ).
cnf(s91,plain,
~ spl0_19,
inference(rat,[],[s73,s89,s90,s84,s87]) ).
cnf(s92,plain,
spl0_15,
inference(rat,[],[s44,s84,s88]) ).
cnf(s93,plain,
spl0_14,
inference(rat,[],[s43,s84,s88]) ).
cnf(s96,plain,
spl0_18,
inference(rat,[],[s71,s92]) ).
cnf(s97,plain,
$false,
inference(rat,[],[s13,s91,s84,s96,s93]) ).
fof(f1845,plain,
$false,
inference(avatar_sat_refutation,[],[s97]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COL096-2 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.19 % Computer : n015.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Mon Sep 28 21:38:02 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 Running first-order theorem proving
% 0.10/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.97/2.80 % (3061226)Input is clausal, will run a generic CNF schedule.
% 15.97/2.80 % (3061235)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3481626282:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 15.97/2.80 % (3061235)Instruction limit reached!
% 15.97/2.80 % (3061235)------------------------------
% 15.97/2.80 % (3061235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.97/2.80 % (3061235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.97/2.80 % (3061235)CaDiCaL version: 2.1.3
% 15.97/2.80 % (3061235)Termination reason: Instruction limit
% 15.97/2.80 % (3061235)Termination phase: Saturation
% 15.97/2.80 % (3061235)Time elapsed: 0.039 s
% 15.97/2.80 % (3061235)Peak memory usage: 88 MB
% 15.97/2.80 % (3061235)Instructions burned: 115 (million)
% 15.97/2.80 % (3061232)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=762585286:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 15.97/2.80 % (3061231)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=3575237225:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 15.97/2.80 % (3061234)lrs+10_1_sil=8000:sp=occurrence:random_seed=1845893914:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 15.97/2.80 % (3061233)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1698537182:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 15.97/2.80 % (3061237)dis-21_1_sil=8000:lcm=predicate:random_seed=3664971552:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 15.97/2.80 % (3061236)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=518734983:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 15.97/2.80 % (3061237)Instruction limit reached!
% 15.97/2.80 % (3061237)------------------------------
% 15.97/2.80 % (3061237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.97/2.80 % (3061237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.97/2.80 % (3061237)CaDiCaL version: 2.1.3
% 15.97/2.80 % (3061237)Termination reason: Instruction limit
% 15.97/2.80 % (3061237)Termination phase: Saturation
% 15.97/2.80 % (3061237)Time elapsed: 0.063 s
% 15.97/2.80 % (3061237)Peak memory usage: 89 MB
% 15.97/2.80 % (3061237)Instructions burned: 117 (million)
% 15.97/2.80 % (3061234)Instruction limit reached!
% 15.97/2.80 % (3061234)------------------------------
% 15.97/2.80 % (3061234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.97/2.80 % (3061234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.97/2.80 % (3061234)CaDiCaL version: 2.1.3
% 15.97/2.80 % (3061234)Termination reason: Instruction limit
% 15.97/2.80 % (3061234)Termination phase: Saturation
% 15.97/2.80 % (3061234)Time elapsed: 0.101 s
% 15.97/2.80 % (3061234)Peak memory usage: 89 MB
% 15.97/2.80 % (3061234)Instructions burned: 107 (million)
% 15.97/2.80 % (3061236)Instruction limit reached!
% 15.97/2.80 % (3061236)------------------------------
% 15.97/2.80 % (3061236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.97/2.80 % (3061236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.97/2.80 % (3061236)CaDiCaL version: 2.1.3
% 15.97/2.80 % (3061236)Termination reason: Instruction limit
% 15.97/2.80 % (3061236)Termination phase: Saturation
% 15.97/2.80 % (3061236)Time elapsed: 0.178 s
% 15.97/2.80 % (3061236)Peak memory usage: 89 MB
% 15.97/2.80 % (3061236)Instructions burned: 180 (million)
% 15.97/2.80 % (3061249)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1233412224:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 15.97/2.80 % (3061249)Refutation not found, incomplete strategy
% 15.97/2.80 % (3061249)------------------------------
% 15.97/2.80 % (3061249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.97/2.80 % (3061249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.97/2.80 % (3061249)CaDiCaL version: 2.1.3
% 15.97/2.80 % (3061249)Termination reason: Refutation not found, incomplete strategy
% 15.97/2.80 % (3061249)Time elapsed: 0.004 s
% 15.97/2.80 % (3061249)Peak memory usage: 88 MB
% 15.97/2.80 % (3061249)Instructions burned: 2 (million)
% 15.97/2.80 % (3061254)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2318371279:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 16.95/3.01 % (3061256)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=530192838:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 16.95/3.01 % (3061256)Refutation not found, incomplete strategy
% 16.95/3.01 % (3061256)------------------------------
% 16.95/3.01 % (3061256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.01 % (3061256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.01 % (3061256)CaDiCaL version: 2.1.3
% 16.95/3.01 % (3061256)Termination reason: Refutation not found, incomplete strategy
% 16.95/3.01 % (3061256)Time elapsed: 0.009 s
% 16.95/3.01 % (3061256)Peak memory usage: 88 MB
% 16.95/3.01 % (3061256)Instructions burned: 7 (million)
% 16.95/3.01 % (3061254)Instruction limit reached!
% 16.95/3.01 % (3061254)------------------------------
% 16.95/3.01 % (3061254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.01 % (3061254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.01 % (3061254)CaDiCaL version: 2.1.3
% 16.95/3.01 % (3061254)Termination reason: Instruction limit
% 16.95/3.01 % (3061254)Termination phase: Saturation
% 16.95/3.01 % (3061254)Time elapsed: 0.093 s
% 16.95/3.01 % (3061254)Peak memory usage: 91 MB
% 16.95/3.01 % (3061254)Instructions burned: 190 (million)
% 16.95/3.01 % (3061264)lrs+10_64_to=lpo:sil=8000:random_seed=4218313467:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 16.95/3.01 % (3061270)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=799777416:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 16.95/3.01 % (3061249)------------------------------
% 16.95/3.01 % (3061249)------------------------------
% 16.95/3.01 % (3061270)Instruction limit reached!
% 16.95/3.01 % (3061270)------------------------------
% 16.95/3.01 % (3061270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.01 % (3061270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.01 % (3061270)CaDiCaL version: 2.1.3
% 16.95/3.01 % (3061270)Termination reason: Instruction limit
% 16.95/3.01 % (3061270)Termination phase: Saturation
% 16.95/3.01 % (3061270)Time elapsed: 0.100 s
% 16.95/3.01 % (3061270)Peak memory usage: 90 MB
% 16.95/3.01 % (3061270)Instructions burned: 194 (million)
% 16.95/3.01 % (3061264)Instruction limit reached!
% 16.95/3.01 % (3061264)------------------------------
% 16.95/3.01 % (3061264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.01 % (3061264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.01 % (3061264)CaDiCaL version: 2.1.3
% 16.95/3.01 % (3061264)Termination reason: Instruction limit
% 16.95/3.01 % (3061264)Termination phase: Saturation
% 16.95/3.01 % (3061264)Time elapsed: 0.129 s
% 16.95/3.01 % (3061264)Peak memory usage: 90 MB
% 16.95/3.01 % (3061264)Instructions burned: 127 (million)
% 16.95/3.01 % (3061256)------------------------------
% 16.95/3.01 % (3061256)------------------------------
% 16.95/3.01 % (3061277)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2298858985:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 16.95/3.01 % (3061279)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=653556878:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 16.95/3.01 % (3061278)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2901877781:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 16.95/3.01 % (3061280)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=117069326:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 16.95/3.01 % (3061279)Instruction limit reached!
% 16.95/3.01 % (3061279)------------------------------
% 16.95/3.01 % (3061279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.01 % (3061279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.01 % (3061279)CaDiCaL version: 2.1.3
% 16.95/3.01 % (3061279)Termination reason: Instruction limit
% 16.95/3.01 % (3061279)Termination phase: Saturation
% 16.95/3.01 % (3061279)Time elapsed: 0.053 s
% 16.95/3.01 % (3061279)Peak memory usage: 90 MB
% 16.95/3.01 % (3061279)Instructions burned: 107 (million)
% 16.95/3.01 % (3061277)Instruction limit reached!
% 16.95/3.01 % (3061277)------------------------------
% 16.95/3.01 % (3061277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.01 % (3061277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.01 % (3061277)CaDiCaL version: 2.1.3
% 16.95/3.01 % (3061277)Termination reason: Instruction limit
% 16.95/3.01 % (3061277)Termination phase: Saturation
% 16.95/3.01 % (3061277)Time elapsed: 0.145 s
% 16.95/3.01 % (3061277)Peak memory usage: 91 MB
% 16.95/3.01 % (3061277)Instructions burned: 157 (million)
% 16.95/3.01 % (3061280)Instruction limit reached!
% 16.95/3.01 % (3061280)------------------------------
% 16.95/3.01 % (3061280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.01 % (3061280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.01 % (3061280)CaDiCaL version: 2.1.3
% 16.95/3.01 % (3061280)Termination reason: Instruction limit
% 16.95/3.01 % (3061280)Termination phase: Saturation
% 16.95/3.01 % (3061280)Time elapsed: 0.114 s
% 16.95/3.01 % (3061280)Peak memory usage: 89 MB
% 16.95/3.01 % (3061280)Instructions burned: 107 (million)
% 16.95/3.01 % (3061290)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2379263962:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2989 on theBenchmark for (2989ds/242Mi)
% 16.95/3.01 % (3061292)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2264342806:cond=fast:i=5208:av=off_2988 on theBenchmark for (2988ds/5208Mi)
% 16.95/3.01 % (3061290)Instruction limit reached!
% 16.95/3.01 % (3061290)------------------------------
% 16.95/3.01 % (3061290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.01 % (3061290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.01 % (3061290)CaDiCaL version: 2.1.3
% 16.95/3.01 % (3061290)Termination reason: Instruction limit
% 16.95/3.01 % (3061290)Termination phase: Saturation
% 16.95/3.01 % (3061290)Time elapsed: 0.134 s
% 16.95/3.01 % (3061290)Peak memory usage: 89 MB
% 16.95/3.01 % (3061290)Instructions burned: 243 (million)
% 16.95/3.01 % (3061294)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=271955589:i=134:sd=2:doe=on:ss=axioms:sgt=14_2987 on theBenchmark for (2987ds/134Mi)
% 16.95/3.01 % (3061294)Refutation not found, incomplete strategy
% 16.95/3.01 % (3061294)------------------------------
% 16.95/3.01 % (3061294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.01 % (3061294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.01 % (3061294)CaDiCaL version: 2.1.3
% 16.95/3.01 % (3061294)Termination reason: Refutation not found, incomplete strategy
% 16.95/3.01 % (3061294)Time elapsed: 0.004 s
% 16.95/3.01 % (3061294)Peak memory usage: 88 MB
% 16.95/3.01 % (3061294)Instructions burned: 2 (million)
% 16.95/3.01 % (3061303)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=984671214:i=499:bd=all_2985 on theBenchmark for (2985ds/499Mi)
% 16.95/3.01 % (3061294)------------------------------
% 16.95/3.01 % (3061294)------------------------------
% 16.95/3.01 % (3061303)Instruction limit reached!
% 16.95/3.01 % (3061303)------------------------------
% 16.95/3.01 % (3061303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.01 % (3061303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.01 % (3061303)CaDiCaL version: 2.1.3
% 16.95/3.01 % (3061303)Termination reason: Instruction limit
% 16.95/3.01 % (3061303)Termination phase: Saturation
% 16.95/3.01 % (3061303)Time elapsed: 0.253 s
% 16.95/3.01 % (3061303)Peak memory usage: 95 MB
% 16.95/3.01 % (3061303)Instructions burned: 501 (million)
% 16.95/3.01 % (3061311)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2368367803:i=191:fgj=on:bd=all_2981 on theBenchmark for (2981ds/191Mi)
% 16.95/3.01 % (3061312)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1030737701:i=264:kws=precedence:fsr=off_2980 on theBenchmark for (2980ds/264Mi)
% 16.95/3.01 % (3061278)First to succeed.
% 16.95/3.01 % (3061278)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3061226"
% 16.95/3.01 % (3061311)Instruction limit reached!
% 16.95/3.01 % (3061311)------------------------------
% 16.95/3.01 % (3061311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.01 % (3061311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.01 % (3061311)CaDiCaL version: 2.1.3
% 16.95/3.01 % (3061311)Termination reason: Instruction limit
% 16.95/3.01 % (3061311)Termination phase: Saturation
% 16.95/3.01 % (3061311)Time elapsed: 0.197 s
% 16.95/3.01 % (3061311)Peak memory usage: 91 MB
% 16.95/3.01 % (3061311)Instructions burned: 191 (million)
% 16.95/3.01 % (3061312)Instruction limit reached!
% 16.95/3.01 % (3061312)------------------------------
% 16.95/3.01 % (3061312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.01 % (3061312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.01 % (3061312)CaDiCaL version: 2.1.3
% 16.95/3.01 % (3061312)Termination reason: Instruction limit
% 16.95/3.01 % (3061312)Termination phase: Saturation
% 16.95/3.01 % (3061312)Time elapsed: 0.267 s
% 16.95/3.01 % (3061312)Peak memory usage: 92 MB
% 16.95/3.01 % (3061312)Instructions burned: 264 (million)
% 16.95/3.01 % (3061278)Refutation found. Thanks to Tanya!
% 16.95/3.01 % SZS status Unsatisfiable for theBenchmark
% 16.95/3.01 % SZS output start Proof for theBenchmark
% See solution above
% 18.48/3.16 % (3061278)------------------------------
% 18.48/3.16 % (3061278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.48/3.16 % (3061278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.48/3.16 % (3061278)CaDiCaL version: 2.1.3
% 18.48/3.16 % (3061278)Termination reason: Refutation
% 18.48/3.16 % (3061278)Time elapsed: 1.215 s
% 18.48/3.16 % (3061278)Peak memory usage: 133 MB
% 18.48/3.16 % (3061278)Instructions burned: 1394 (million)
% 18.48/3.16 % (3061278)------------------------------
% 18.48/3.16 % (3061278)------------------------------
% 18.48/3.16 % (3061226)Success in time 2.566 s
% 18.48/3.16 % Vampire exiting
%------------------------------------------------------------------------------