%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COL093-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 : n018.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:55 AM UTC 2026
% Result : Unsatisfiable 10.55s 2.55s
% Output : Refutation 12.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 23
% Syntax : Number of formulae : 89 ( 18 unt; 9 def)
% Number of atoms : 178 ( 29 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 175 ( 86 ~; 82 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 8 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-3 aty)
% Number of variables : 55 ( 0 sgn 55 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f159,axiom,
! [X0,X1] : combS != comb_app(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s_app) ).
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(f201,axiom,
! [X0] :
( ~ member(pair(combS,X0),parcontract)
| X0 = combS ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s_parcontractE2) ).
fof(f202,plain,
! [X0] :
( ~ member(pair(combS,X0),parcontract)
| combS = X0 ),
inference(reorient_equations,[],[f201]) ).
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(f204,axiom,
! [X2,X0,X1] :
( ~ ap_parcontractE_c1(X0,X1,X2)
| member(comb_app(X0,X1),comb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE2) ).
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(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(f222,axiom,
member(pair(comb_app(combS,p),r),parcontract),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_parcontractD_h1) ).
fof(f223,negated_conjecture,
! [X0] :
( r != comb_app(combS,X0)
| ~ member(pair(p,X0),parcontract) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_parcontractD_c1) ).
fof(f224,plain,
! [X0] :
( comb_app(combS,X0) != r
| ~ member(pair(p,X0),parcontract) ),
inference(reorient_equations,[],[f223]) ).
fof(f235,definition,
! [X0] : sF0(X0) = comb_app(combS,X0),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f236,plain,
! [X0] : comb_app(combS,X0) = sF0(X0),
inference(reorient_equations,[],[f235]) ).
fof(f237,definition,
! [X0] : sF1(X0) = pair(p,X0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f238,plain,
! [X0] : pair(p,X0) = sF1(X0),
inference(reorient_equations,[],[f237]) ).
fof(f239,plain,
! [X0] :
( r != sF0(X0)
| ~ member(sF1(X0),parcontract) ),
inference(definition_folding,[],[f224,f238,f236]) ).
fof(f258,plain,
( member(sF1(p),parcontract)
| ~ member(p,comb) ),
inference(superposition,[],[f193,f238]) ).
fof(f260,definition,
( spl2_5
<=> member(p,comb) ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
fof(f262,plain,
( ~ member(p,comb)
| spl2_5 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f264,definition,
( spl2_6
<=> member(sF1(p),parcontract) ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
fof(f267,plain,
( ~ spl2_5
| spl2_6 ),
inference(avatar_split_clause,[],[f258,f264,f260]) ).
fof(f268,plain,
! [X0,X1] :
( member(sF1(ap_parcontractE_sk2s(X0,p,X1)),parcontract)
| ~ ap_parcontractE_c4(X0,p,X1) ),
inference(superposition,[],[f219,f238]) ).
fof(f272,plain,
( ap_parcontractE_c1(combS,p,r)
| ap_parcontractE_c2(combS,p,r)
| ap_parcontractE_c3(combS,p,r)
| ap_parcontractE_c4(combS,p,r) ),
inference(resolution,[],[f203,f222]) ).
fof(f278,definition,
( spl2_7
<=> ap_parcontractE_c4(combS,p,r) ),
introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition]) ).
fof(f280,plain,
( ap_parcontractE_c4(combS,p,r)
| ~ spl2_7 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f282,definition,
( spl2_8
<=> ap_parcontractE_c3(combS,p,r) ),
introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition]) ).
fof(f284,plain,
( ap_parcontractE_c3(combS,p,r)
| ~ spl2_8 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f286,definition,
( spl2_9
<=> ap_parcontractE_c2(combS,p,r) ),
introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition]) ).
fof(f288,plain,
( ap_parcontractE_c2(combS,p,r)
| ~ spl2_9 ),
inference(avatar_component_clause,[],[f286]) ).
fof(f290,definition,
( spl2_10
<=> ap_parcontractE_c1(combS,p,r) ),
introduced(definition,[new_symbols(definition,[spl2_10])],[avatar_definition]) ).
fof(f292,plain,
( ap_parcontractE_c1(combS,p,r)
| ~ spl2_10 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f293,plain,
( spl2_7
| spl2_8
| spl2_9
| spl2_10 ),
inference(avatar_split_clause,[],[f272,f290,f286,f282,f278]) ).
fof(f295,plain,
! [X0] :
( ~ member(sF0(X0),comb)
| member(X0,comb) ),
inference(superposition,[],[f164,f236]) ).
fof(f296,plain,
( r = comb_app(ap_parcontractE_sk2q(combS,p,r),ap_parcontractE_sk2s(combS,p,r))
| ~ spl2_7 ),
inference(resolution,[],[f221,f280]) ).
fof(f306,definition,
( spl2_12
<=> member(r,comb) ),
introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition]) ).
fof(f307,plain,
( member(r,comb)
| ~ spl2_12 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f308,plain,
( ~ member(r,comb)
| spl2_12 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f336,plain,
! [X0,X1] :
( ~ ap_parcontractE_c4(combS,X0,X1)
| combS = ap_parcontractE_sk2q(combS,X0,X1) ),
inference(resolution,[],[f202,f218]) ).
fof(f337,plain,
( combS = ap_parcontractE_sk2q(combS,p,r)
| ~ spl2_7 ),
inference(resolution,[],[f336,f280]) ).
fof(f338,plain,
( r = comb_app(combS,ap_parcontractE_sk2s(combS,p,r))
| ~ spl2_7 ),
inference(superposition,[],[f296,f337]) ).
fof(f341,plain,
( r = sF0(ap_parcontractE_sk2s(combS,p,r))
| ~ spl2_7 ),
inference(forward_demodulation,[],[f338,f236]) ).
fof(f343,plain,
( r != r
| ~ member(sF1(ap_parcontractE_sk2s(combS,p,r)),parcontract)
| ~ spl2_7 ),
inference(superposition,[],[f239,f341]) ).
fof(f344,plain,
( ~ member(sF1(ap_parcontractE_sk2s(combS,p,r)),parcontract)
| ~ spl2_7 ),
inference(trivial_inequality_removal,[],[f343]) ).
fof(f347,plain,
( ~ ap_parcontractE_c4(combS,p,r)
| ~ spl2_7 ),
inference(resolution,[],[f344,f268]) ).
fof(f348,plain,
( $false
| ~ spl2_7 ),
inference(forward_subsumption_resolution,[],[f347,f280]) ).
fof(f349,plain,
~ spl2_7,
inference(avatar_contradiction_clause,[],[f348]) ).
fof(f350,plain,
( combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,p,r)),ap_parcontractE_sk1q(combS,p,r))
| ~ spl2_8 ),
inference(resolution,[],[f284,f217]) ).
fof(f351,plain,
( $false
| ~ spl2_8 ),
inference(forward_subsumption_resolution,[],[f350,f159]) ).
fof(f352,plain,
~ spl2_8,
inference(avatar_contradiction_clause,[],[f351]) ).
fof(f353,plain,
( combS = comb_app(combK,r)
| ~ spl2_9 ),
inference(resolution,[],[f288,f210]) ).
fof(f354,plain,
( $false
| ~ spl2_9 ),
inference(forward_subsumption_resolution,[],[f353,f159]) ).
fof(f355,plain,
~ spl2_9,
inference(avatar_contradiction_clause,[],[f354]) ).
fof(f356,plain,
( member(comb_app(combS,p),comb)
| ~ spl2_10 ),
inference(resolution,[],[f292,f204]) ).
fof(f357,plain,
( comb_app(combS,p) = r
| ~ spl2_10 ),
inference(resolution,[],[f292,f206]) ).
fof(f358,plain,
( r = sF0(p)
| ~ spl2_10 ),
inference(forward_demodulation,[],[f357,f236]) ).
fof(f359,plain,
( member(sF0(p),comb)
| ~ spl2_10 ),
inference(forward_demodulation,[],[f356,f236]) ).
fof(f360,plain,
( member(r,comb)
| ~ spl2_10 ),
inference(forward_demodulation,[],[f359,f358]) ).
fof(f361,plain,
( $false
| ~ spl2_10
| spl2_12 ),
inference(forward_subsumption_resolution,[],[f360,f308]) ).
fof(f362,plain,
( ~ spl2_10
| spl2_12 ),
inference(avatar_contradiction_clause,[],[f361]) ).
fof(f365,plain,
( r != r
| ~ member(sF1(p),parcontract)
| ~ spl2_10 ),
inference(superposition,[],[f239,f358]) ).
fof(f366,plain,
( ~ member(sF1(p),parcontract)
| ~ spl2_10 ),
inference(trivial_inequality_removal,[],[f365]) ).
fof(f367,plain,
( ~ spl2_6
| ~ spl2_10 ),
inference(avatar_split_clause,[],[f366,f290,f264]) ).
fof(f395,plain,
( ~ member(r,comb)
| member(p,comb)
| ~ spl2_10 ),
inference(superposition,[],[f295,f358]) ).
fof(f396,plain,
( member(p,comb)
| ~ spl2_10
| ~ spl2_12 ),
inference(forward_subsumption_resolution,[],[f395,f307]) ).
fof(f397,plain,
( $false
| spl2_5
| ~ spl2_10
| ~ spl2_12 ),
inference(forward_subsumption_resolution,[],[f396,f262]) ).
fof(f398,plain,
( spl2_5
| ~ spl2_10
| ~ spl2_12 ),
inference(avatar_contradiction_clause,[],[f397]) ).
cnf(s5,plain,
( ~ spl2_5
| spl2_6 ),
inference(sat_conversion,[],[f267]) ).
cnf(s6,plain,
( spl2_7
| spl2_8
| spl2_9
| spl2_10 ),
inference(sat_conversion,[],[f293]) ).
cnf(s11,plain,
~ spl2_7,
inference(sat_conversion,[],[f349]) ).
cnf(s12,plain,
~ spl2_8,
inference(sat_conversion,[],[f352]) ).
cnf(s13,plain,
~ spl2_9,
inference(sat_conversion,[],[f355]) ).
cnf(s14,plain,
( ~ spl2_10
| spl2_12 ),
inference(sat_conversion,[],[f362]) ).
cnf(s15,plain,
( ~ spl2_6
| ~ spl2_10 ),
inference(sat_conversion,[],[f367]) ).
cnf(s16,plain,
( spl2_5
| ~ spl2_10
| ~ spl2_12 ),
inference(sat_conversion,[],[f398]) ).
cnf(s17,plain,
spl2_10,
inference(rat,[],[s6,s13,s12,s11]) ).
cnf(s18,plain,
~ spl2_6,
inference(rat,[],[s15,s17]) ).
cnf(s19,plain,
spl2_12,
inference(rat,[],[s14,s17]) ).
cnf(s20,plain,
spl2_5,
inference(rat,[],[s16,s17,s19]) ).
cnf(s21,plain,
$false,
inference(rat,[],[s5,s18,s20]) ).
fof(f399,plain,
$false,
inference(avatar_sat_refutation,[],[s21]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : COL093-2 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.26 % Computer : n018.cluster.edu
% 0.11/0.26 % Model : x86_64 x86_64
% 0.11/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.26 % Memory : 8046.5625MB
% 0.11/0.26 % OS : Linux 6.8.0-71-generic
% 0.11/0.26 % CPULimit : 300
% 0.11/0.26 % WCLimit : 300
% 0.11/0.26 % DateTime : Mon Sep 28 21:37:55 UTC 2026
% 0.11/0.27 % CPUTime :
% 0.11/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.32 Running first-order theorem proving
% 0.25/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.55/2.55 % (3817714)Input is clausal, will run a generic CNF schedule.
% 10.55/2.55 % (3817724)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1014577984:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.55/2.55 % (3817721)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3094507682:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.55/2.55 % (3817722)lrs+10_1_sil=8000:sp=occurrence:random_seed=1045423523:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.55/2.55 % (3817720)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3134144829:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.55/2.55 % (3817719)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=1378654185:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.55/2.55 % (3817722)Refutation not found, incomplete strategy
% 10.55/2.55 % (3817722)------------------------------
% 10.55/2.55 % (3817722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.55 % (3817722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.55 % (3817722)CaDiCaL version: 2.1.3
% 10.55/2.55 % (3817722)Termination reason: Refutation not found, incomplete strategy
% 10.55/2.55 % (3817722)Time elapsed: 0.003 s
% 10.55/2.55 % (3817722)Peak memory usage: 87 MB
% 10.55/2.55 % (3817722)Instructions burned: 1 (million)
% 10.55/2.55 % (3817723)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=515993947:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.55/2.55 % (3817723)Refutation not found, incomplete strategy
% 10.55/2.55 % (3817723)------------------------------
% 10.55/2.55 % (3817723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.55 % (3817723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.55 % (3817723)CaDiCaL version: 2.1.3
% 10.55/2.55 % (3817723)Termination reason: Refutation not found, incomplete strategy
% 10.55/2.55 % (3817723)Time elapsed: 0.005 s
% 10.55/2.55 % (3817723)Peak memory usage: 88 MB
% 10.55/2.55 % (3817723)Instructions burned: 3 (million)
% 10.55/2.55 % (3817725)dis-21_1_sil=8000:lcm=predicate:random_seed=1081401510: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)
% 10.55/2.55 % (3817725)Instruction limit reached!
% 10.55/2.55 % (3817725)------------------------------
% 10.55/2.55 % (3817725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.55 % (3817725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.55 % (3817725)CaDiCaL version: 2.1.3
% 10.55/2.55 % (3817725)Termination reason: Instruction limit
% 10.55/2.55 % (3817725)Termination phase: Saturation
% 10.55/2.55 % (3817725)Time elapsed: 0.070 s
% 10.55/2.55 % (3817725)Peak memory usage: 89 MB
% 10.55/2.55 % (3817725)Instructions burned: 117 (million)
% 10.55/2.55 % (3817724)Instruction limit reached!
% 10.55/2.55 % (3817724)------------------------------
% 10.55/2.55 % (3817724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.55 % (3817724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.55 % (3817724)CaDiCaL version: 2.1.3
% 10.55/2.55 % (3817724)Termination reason: Instruction limit
% 10.55/2.55 % (3817724)Termination phase: Saturation
% 10.55/2.55 % (3817724)Time elapsed: 0.190 s
% 10.55/2.55 % (3817724)Peak memory usage: 90 MB
% 10.55/2.55 % (3817724)Instructions burned: 180 (million)
% 10.55/2.55 % (3817735)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=2170505066:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 10.55/2.55 % (3817735)Refutation not found, incomplete strategy
% 10.55/2.55 % (3817735)------------------------------
% 10.55/2.55 % (3817735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.55 % (3817735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.55 % (3817735)CaDiCaL version: 2.1.3
% 10.55/2.55 % (3817735)Termination reason: Refutation not found, incomplete strategy
% 10.55/2.55 % (3817735)Time elapsed: 0.006 s
% 10.55/2.55 % (3817735)Peak memory usage: 88 MB
% 10.55/2.55 % (3817735)Instructions burned: 8 (million)
% 10.55/2.55 % (3817722)------------------------------
% 10.55/2.55 % (3817722)------------------------------
% 10.55/2.55 % (3817736)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3093273614:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 10.55/2.55 % (3817723)------------------------------
% 10.55/2.55 % (3817723)------------------------------
% 10.55/2.55 % (3817735)------------------------------
% 10.55/2.55 % (3817735)------------------------------
% 10.55/2.55 % (3817736)Instruction limit reached!
% 10.55/2.55 % (3817736)------------------------------
% 10.55/2.55 % (3817736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.55 % (3817736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.55 % (3817736)CaDiCaL version: 2.1.3
% 10.55/2.55 % (3817736)Termination reason: Instruction limit
% 10.55/2.55 % (3817736)Termination phase: Saturation
% 10.55/2.55 % (3817736)Time elapsed: 0.168 s
% 10.55/2.55 % (3817736)Peak memory usage: 91 MB
% 10.55/2.55 % (3817736)Instructions burned: 190 (million)
% 10.55/2.55 % (3817738)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2236343395:st=4:i=219:sd=3:ss=axioms_2993 on theBenchmark for (2993ds/219Mi)
% 10.55/2.55 % (3817738)Refutation not found, incomplete strategy
% 10.55/2.55 % (3817738)------------------------------
% 10.55/2.55 % (3817738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.55 % (3817738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.55 % (3817738)CaDiCaL version: 2.1.3
% 10.55/2.55 % (3817738)Termination reason: Refutation not found, incomplete strategy
% 10.55/2.55 % (3817738)Time elapsed: 0.010 s
% 10.55/2.55 % (3817738)Peak memory usage: 88 MB
% 10.55/2.55 % (3817738)Instructions burned: 8 (million)
% 10.55/2.55 % (3817740)lrs+10_64_to=lpo:sil=8000:random_seed=313746856:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 10.55/2.55 % (3817742)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3825389943:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 10.55/2.55 % (3817741)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=546225228:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi)
% 10.55/2.55 % (3817740)Instruction limit reached!
% 10.55/2.55 % (3817740)------------------------------
% 10.55/2.55 % (3817740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.55 % (3817740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.55 % (3817740)CaDiCaL version: 2.1.3
% 10.55/2.55 % (3817740)Termination reason: Instruction limit
% 10.55/2.55 % (3817740)Termination phase: Saturation
% 10.55/2.55 % (3817740)Time elapsed: 0.129 s
% 10.55/2.55 % (3817740)Peak memory usage: 90 MB
% 10.55/2.55 % (3817740)Instructions burned: 126 (million)
% 10.55/2.55 % (3817742)Instruction limit reached!
% 10.55/2.55 % (3817742)------------------------------
% 10.55/2.55 % (3817742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.55 % (3817742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.55 % (3817742)CaDiCaL version: 2.1.3
% 10.55/2.55 % (3817742)Termination reason: Instruction limit
% 10.55/2.55 % (3817742)Termination phase: Saturation
% 10.55/2.55 % (3817742)Time elapsed: 0.084 s
% 10.55/2.55 % (3817742)Peak memory usage: 91 MB
% 10.55/2.55 % (3817742)Instructions burned: 157 (million)
% 10.55/2.55 % (3817719)First to succeed.
% 10.55/2.55 % (3817719)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3817714"
% 10.55/2.55 % (3817741)Instruction limit reached!
% 10.55/2.55 % (3817741)------------------------------
% 10.55/2.55 % (3817741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.55 % (3817741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.55 % (3817741)CaDiCaL version: 2.1.3
% 10.55/2.55 % (3817741)Termination reason: Instruction limit
% 10.55/2.55 % (3817741)Termination phase: Saturation
% 10.55/2.55 % (3817741)Time elapsed: 0.205 s
% 10.55/2.55 % (3817741)Peak memory usage: 90 MB
% 10.55/2.55 % (3817741)Instructions burned: 195 (million)
% 10.55/2.55 % (3817738)------------------------------
% 10.55/2.55 % (3817738)------------------------------
% 10.55/2.55 % (3817747)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=109763836:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 10.55/2.55 % (3817748)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=2333354407:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 10.55/2.55 % (3817748)Instruction limit reached!
% 10.55/2.55 % (3817748)------------------------------
% 10.55/2.55 % (3817748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.55 % (3817748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.55 % (3817748)CaDiCaL version: 2.1.3
% 10.55/2.55 % (3817748)Termination reason: Instruction limit
% 10.55/2.55 % (3817748)Termination phase: Saturation
% 10.55/2.55 % (3817748)Time elapsed: 0.056 s
% 10.55/2.55 % (3817748)Peak memory usage: 90 MB
% 10.55/2.55 % (3817748)Instructions burned: 107 (million)
% 10.55/2.55 % (3817721)Also succeeded, but the first one will report.
% 10.55/2.55 % (3817749)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2890666315:i=107_2987 on theBenchmark for (2987ds/107Mi)
% 10.55/2.55 % (3817751)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=578654089:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 10.55/2.55 % (3817719)Refutation found. Thanks to Tanya!
% 10.55/2.55 % SZS status Unsatisfiable for theBenchmark
% 10.55/2.55 % SZS output start Proof for theBenchmark
% See solution above
% 12.17/2.76 % (3817719)------------------------------
% 12.17/2.76 % (3817719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.17/2.76 % (3817719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.76 % (3817719)CaDiCaL version: 2.1.3
% 12.17/2.76 % (3817719)Termination reason: Refutation
% 12.17/2.76 % (3817719)Time elapsed: 0.943 s
% 12.17/2.76 % (3817719)Peak memory usage: 131 MB
% 12.17/2.76 % (3817719)Instructions burned: 1006 (million)
% 12.17/2.76 % (3817719)------------------------------
% 12.17/2.76 % (3817719)------------------------------
% 12.17/2.76 % (3817714)Success in time 1.617 s
% 12.17/2.76 % Vampire exiting
%------------------------------------------------------------------------------