%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ROB014-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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 12:36:16 PM UTC 2026
% Result : Unsatisfiable 8.61s 2.19s
% Output : Refutation 8.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 13
% Syntax : Number of formulae : 67 ( 67 unt; 7 def)
% Number of atoms : 67 ( 66 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 10 con; 0-2 aty)
% Number of variables : 21 ( 21 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : add(X0,X1) = add(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_add) ).
fof(f2,axiom,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(X0,add(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_add) ).
fof(f3,axiom,
! [X0,X1] : negate(add(negate(add(X0,X1)),negate(add(X0,negate(X1))))) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',robbins_axiom) ).
fof(f4,axiom,
! [X0] : multiply(one,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',one_times_x) ).
fof(f8,axiom,
negate(add(negate(e),negate(add(d,negate(e))))) = d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condition) ).
fof(f9,plain,
d = negate(add(negate(e),negate(add(d,negate(e))))),
inference(reorient_equations,[],[f8]) ).
fof(f10,negated_conjecture,
negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))) != negate(e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_base_step) ).
fof(f11,plain,
negate(e) != negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))),
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF0 = negate(e),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f13,plain,
negate(e) = sF0,
inference(reorient_equations,[],[f12]) ).
fof(f14,definition,
sF1 = add(d,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f15,plain,
add(d,sF0) = sF1,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF2 = negate(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f17,plain,
negate(sF1) = sF2,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF3 = add(d,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f19,plain,
add(d,sF2) = sF3,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF4 = multiply(one,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f21,plain,
multiply(one,sF3) = sF4,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF5 = add(e,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f23,plain,
add(e,sF4) = sF5,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF6 = negate(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f25,plain,
negate(sF5) = sF6,
inference(reorient_equations,[],[f24]) ).
fof(f26,plain,
sF0 != sF6,
inference(definition_folding,[],[f11,f25,f23,f21,f19,f17,f15,f13,f13]) ).
fof(f27,plain,
negate(e) != sF6,
inference(backward_demodulation,[],[f26,f13]) ).
fof(f28,plain,
add(d,negate(e)) = sF1,
inference(forward_demodulation,[],[f15,f13]) ).
fof(f29,plain,
sF3 = sF4,
inference(forward_demodulation,[],[f21,f4]) ).
fof(f30,plain,
d = negate(add(negate(e),negate(sF1))),
inference(backward_demodulation,[],[f9,f28]) ).
fof(f31,plain,
sF5 = add(e,sF3),
inference(backward_demodulation,[],[f23,f29]) ).
fof(f32,plain,
d = negate(add(negate(e),sF2)),
inference(forward_demodulation,[],[f30,f17]) ).
fof(f33,plain,
d = negate(add(sF2,negate(e))),
inference(forward_demodulation,[],[f32,f1]) ).
fof(f39,plain,
d = negate(add(negate(add(d,e)),negate(sF1))),
inference(superposition,[],[f3,f28]) ).
fof(f42,plain,
d = negate(add(negate(sF1),negate(add(d,e)))),
inference(forward_demodulation,[],[f39,f1]) ).
fof(f43,plain,
d = negate(add(negate(sF1),negate(add(e,d)))),
inference(forward_demodulation,[],[f42,f1]) ).
fof(f44,plain,
d = negate(add(sF2,negate(add(e,d)))),
inference(forward_demodulation,[],[f43,f17]) ).
fof(f46,plain,
! [X0] : add(d,add(negate(e),X0)) = add(sF1,X0),
inference(superposition,[],[f2,f28]) ).
fof(f64,plain,
! [X0,X1] : negate(add(negate(add(X0,X1)),negate(add(X1,negate(X0))))) = X1,
inference(superposition,[],[f3,f1]) ).
fof(f65,plain,
! [X0,X1] : negate(add(negate(add(X1,X0)),negate(add(negate(X0),X1)))) = X1,
inference(superposition,[],[f3,f1]) ).
fof(f66,plain,
! [X2,X0,X1] : add(X0,add(X1,X2)) = add(X1,add(X2,X0)),
inference(superposition,[],[f2,f1]) ).
fof(f75,plain,
sF2 = negate(add(negate(add(sF2,e)),d)),
inference(superposition,[],[f3,f33]) ).
fof(f79,plain,
sF2 = negate(add(d,negate(add(sF2,e)))),
inference(forward_demodulation,[],[f75,f1]) ).
fof(f80,plain,
sF2 = negate(add(d,negate(add(e,sF2)))),
inference(forward_demodulation,[],[f79,f1]) ).
fof(f95,plain,
! [X0] : negate(add(negate(add(X0,sF1)),negate(add(sF2,X0)))) = X0,
inference(superposition,[],[f65,f17]) ).
fof(f343,plain,
! [X0] : add(sF1,X0) = add(d,add(X0,negate(e))),
inference(superposition,[],[f46,f1]) ).
fof(f516,plain,
sF2 = negate(add(negate(add(sF2,add(e,d))),d)),
inference(superposition,[],[f3,f44]) ).
fof(f530,plain,
sF2 = negate(add(d,negate(add(sF2,add(e,d))))),
inference(forward_demodulation,[],[f516,f1]) ).
fof(f533,plain,
sF2 = negate(add(d,negate(add(e,add(d,sF2))))),
inference(forward_demodulation,[],[f530,f66]) ).
fof(f535,plain,
sF2 = negate(add(d,negate(add(e,sF3)))),
inference(forward_demodulation,[],[f533,f19]) ).
fof(f537,plain,
sF2 = negate(add(d,negate(sF5))),
inference(forward_demodulation,[],[f535,f31]) ).
fof(f539,plain,
sF2 = negate(add(d,sF6)),
inference(forward_demodulation,[],[f537,f25]) ).
fof(f545,plain,
! [X0] : negate(add(negate(add(add(d,sF6),X0)),negate(add(X0,sF2)))) = X0,
inference(superposition,[],[f64,f539]) ).
fof(f550,plain,
! [X0] : negate(add(negate(add(X0,sF2)),negate(add(add(d,sF6),X0)))) = X0,
inference(forward_demodulation,[],[f545,f1]) ).
fof(f554,plain,
! [X0] : negate(add(negate(add(X0,sF2)),negate(add(d,add(sF6,X0))))) = X0,
inference(forward_demodulation,[],[f550,f2]) ).
fof(f1009,plain,
d = negate(add(negate(add(d,add(e,sF2))),sF2)),
inference(superposition,[],[f3,f80]) ).
fof(f1030,plain,
d = negate(add(sF2,negate(add(d,add(e,sF2))))),
inference(forward_demodulation,[],[f1009,f1]) ).
fof(f1035,plain,
d = negate(add(sF2,negate(add(e,add(sF2,d))))),
inference(forward_demodulation,[],[f1030,f66]) ).
fof(f1038,plain,
d = negate(add(sF2,negate(add(e,add(d,sF2))))),
inference(forward_demodulation,[],[f1035,f1]) ).
fof(f1041,plain,
d = negate(add(sF2,negate(add(e,sF3)))),
inference(forward_demodulation,[],[f1038,f19]) ).
fof(f1044,plain,
d = negate(add(sF2,negate(sF5))),
inference(forward_demodulation,[],[f1041,f31]) ).
fof(f1047,plain,
d = negate(add(sF2,sF6)),
inference(forward_demodulation,[],[f1044,f25]) ).
fof(f1422,plain,
sF6 = negate(add(negate(add(sF6,sF1)),d)),
inference(superposition,[],[f95,f1047]) ).
fof(f1456,plain,
sF6 = negate(add(d,negate(add(sF6,sF1)))),
inference(forward_demodulation,[],[f1422,f1]) ).
fof(f1471,plain,
sF6 = negate(add(d,negate(add(sF1,sF6)))),
inference(forward_demodulation,[],[f1456,f1]) ).
fof(f2329,plain,
negate(e) = negate(add(negate(add(negate(e),sF2)),negate(add(sF1,sF6)))),
inference(superposition,[],[f554,f343]) ).
fof(f2366,plain,
negate(e) = negate(add(negate(add(sF2,negate(e))),negate(add(sF1,sF6)))),
inference(forward_demodulation,[],[f2329,f1]) ).
fof(f2378,plain,
negate(e) = negate(add(d,negate(add(sF1,sF6)))),
inference(forward_demodulation,[],[f2366,f33]) ).
fof(f2383,plain,
negate(e) = sF6,
inference(backward_demodulation,[],[f1471,f2378]) ).
fof(f2384,plain,
$false,
inference(forward_subsumption_resolution,[],[f2383,f27]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ROB014-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n006.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 23:26:26 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.71/2.00 % (3442622)Input is clausal, will run a generic CNF schedule.
% 6.71/2.00 % (3442671)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3779069646:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.71/2.00 % (3442669)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=3874099463:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.71/2.00 % (3442675)dis-21_1_sil=8000:lcm=predicate:random_seed=1229487171: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)
% 6.71/2.00 % (3442670)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2404209589:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.71/2.00 % (3442672)lrs+10_1_sil=8000:sp=occurrence:random_seed=1007381921:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.71/2.00 % (3442674)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3120812413:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.71/2.00 % (3442675)Refutation not found, incomplete strategy
% 6.71/2.00 % (3442675)------------------------------
% 6.71/2.00 % (3442675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.71/2.00 % (3442675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/2.00 % (3442675)CaDiCaL version: 2.1.3
% 6.71/2.00 % (3442675)Termination reason: Refutation not found, incomplete strategy
% 6.71/2.00 % (3442675)Time elapsed: 0.001 s
% 6.71/2.00 % (3442675)Peak memory usage: 88 MB
% 6.71/2.00 % (3442673)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1605011090:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.71/2.00 % (3442672)Instruction limit reached!
% 6.71/2.00 % (3442672)------------------------------
% 6.71/2.00 % (3442672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.71/2.00 % (3442672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/2.00 % (3442672)CaDiCaL version: 2.1.3
% 6.71/2.00 % (3442672)Termination reason: Instruction limit
% 6.71/2.00 % (3442672)Termination phase: Saturation
% 6.71/2.00 % (3442672)Time elapsed: 0.062 s
% 6.71/2.00 % (3442672)Peak memory usage: 89 MB
% 6.71/2.00 % (3442672)Instructions burned: 107 (million)
% 6.71/2.00 % (3442673)Instruction limit reached!
% 6.71/2.00 % (3442673)------------------------------
% 6.71/2.00 % (3442673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.71/2.00 % (3442673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/2.00 % (3442673)CaDiCaL version: 2.1.3
% 6.71/2.00 % (3442673)Termination reason: Instruction limit
% 6.71/2.00 % (3442673)Termination phase: Saturation
% 6.71/2.00 % (3442673)Time elapsed: 0.068 s
% 6.71/2.00 % (3442673)Peak memory usage: 89 MB
% 6.71/2.00 % (3442673)Instructions burned: 114 (million)
% 6.71/2.00 % (3442674)Instruction limit reached!
% 6.71/2.00 % (3442674)------------------------------
% 6.71/2.00 % (3442674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.71/2.00 % (3442674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/2.00 % (3442674)CaDiCaL version: 2.1.3
% 6.71/2.00 % (3442674)Termination reason: Instruction limit
% 6.71/2.00 % (3442674)Termination phase: Saturation
% 6.71/2.00 % (3442674)Time elapsed: 0.093 s
% 6.71/2.00 % (3442674)Peak memory usage: 89 MB
% 6.71/2.00 % (3442674)Instructions burned: 181 (million)
% 6.71/2.00 % (3442686)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=3610897843:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 6.71/2.00 % (3442695)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=578073023:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 6.71/2.00 % (3442694)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2856170151: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)
% 6.71/2.00 % (3442675)------------------------------
% 6.71/2.00 % (3442675)------------------------------
% 6.71/2.00 % (3442686)Instruction limit reached!
% 6.71/2.00 % (3442686)------------------------------
% 6.71/2.00 % (3442686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.71/2.00 % (3442686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/2.00 % (3442686)CaDiCaL version: 2.1.3
% 6.71/2.00 % (3442686)Termination reason: Instruction limit
% 6.71/2.00 % (3442686)Termination phase: Saturation
% 6.71/2.00 % (3442686)Time elapsed: 0.077 s
% 6.71/2.00 % (3442686)Peak memory usage: 89 MB
% 6.71/2.00 % (3442686)Instructions burned: 143 (million)
% 6.71/2.00 % (3442694)Instruction limit reached!
% 6.71/2.00 % (3442694)------------------------------
% 6.71/2.00 % (3442694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.71/2.00 % (3442694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/2.00 % (3442694)CaDiCaL version: 2.1.3
% 6.71/2.00 % (3442694)Termination reason: Instruction limit
% 6.71/2.00 % (3442694)Termination phase: Saturation
% 6.71/2.00 % (3442694)Time elapsed: 0.110 s
% 6.71/2.00 % (3442694)Peak memory usage: 90 MB
% 6.71/2.00 % (3442694)Instructions burned: 189 (million)
% 6.71/2.00 % (3442695)Instruction limit reached!
% 6.71/2.00 % (3442695)------------------------------
% 6.71/2.00 % (3442695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.71/2.00 % (3442695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/2.00 % (3442695)CaDiCaL version: 2.1.3
% 6.71/2.00 % (3442695)Termination reason: Instruction limit
% 6.71/2.00 % (3442695)Termination phase: Saturation
% 6.71/2.00 % (3442695)Time elapsed: 0.120 s
% 6.71/2.00 % (3442695)Peak memory usage: 90 MB
% 6.71/2.00 % (3442695)Instructions burned: 220 (million)
% 6.71/2.00 % (3442728)lrs+10_64_to=lpo:sil=8000:random_seed=4293438677:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 6.71/2.00 % (3442729)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2122993348:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 6.71/2.00 % (3442730)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3640406251:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 6.71/2.00 % (3442728)Instruction limit reached!
% 6.71/2.00 % (3442728)------------------------------
% 6.71/2.00 % (3442728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.71/2.00 % (3442728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/2.00 % (3442728)CaDiCaL version: 2.1.3
% 6.71/2.00 % (3442728)Termination reason: Instruction limit
% 6.71/2.00 % (3442728)Termination phase: Saturation
% 6.71/2.00 % (3442728)Time elapsed: 0.065 s
% 6.71/2.00 % (3442728)Peak memory usage: 88 MB
% 6.71/2.00 % (3442728)Instructions burned: 127 (million)
% 6.71/2.00 % (3442731)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3234915499:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 6.71/2.00 % (3442730)Instruction limit reached!
% 6.71/2.00 % (3442730)------------------------------
% 6.71/2.00 % (3442730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.71/2.00 % (3442730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/2.00 % (3442730)CaDiCaL version: 2.1.3
% 6.71/2.00 % (3442730)Termination reason: Instruction limit
% 6.71/2.00 % (3442730)Termination phase: Saturation
% 6.71/2.00 % (3442730)Time elapsed: 0.051 s
% 6.71/2.00 % (3442730)Peak memory usage: 91 MB
% 6.71/2.00 % (3442730)Instructions burned: 159 (million)
% 6.71/2.00 % (3442729)Instruction limit reached!
% 6.71/2.00 % (3442729)------------------------------
% 6.71/2.00 % (3442729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.71/2.00 % (3442729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/2.00 % (3442729)CaDiCaL version: 2.1.3
% 6.71/2.00 % (3442729)Termination reason: Instruction limit
% 6.71/2.00 % (3442729)Termination phase: Saturation
% 6.71/2.00 % (3442729)Time elapsed: 0.106 s
% 6.71/2.00 % (3442729)Peak memory usage: 90 MB
% 6.71/2.00 % (3442729)Instructions burned: 194 (million)
% 6.71/2.00 % (3442737)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2820133826:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 6.71/2.00 % (3442735)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=1364489535:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 6.71/2.00 % (3442737)Instruction limit reached!
% 6.71/2.00 % (3442737)------------------------------
% 6.71/2.00 % (3442737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.61/2.19 % (3442737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.61/2.19 % (3442737)CaDiCaL version: 2.1.3
% 8.61/2.19 % (3442737)Termination reason: Instruction limit
% 8.61/2.19 % (3442737)Termination phase: Saturation
% 8.61/2.19 % (3442737)Time elapsed: 0.033 s
% 8.61/2.19 % (3442737)Peak memory usage: 88 MB
% 8.61/2.19 % (3442737)Instructions burned: 109 (million)
% 8.61/2.19 % (3442738)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3610689363:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 8.61/2.19 % (3442735)Instruction limit reached!
% 8.61/2.19 % (3442735)------------------------------
% 8.61/2.19 % (3442735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.61/2.19 % (3442735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.61/2.19 % (3442735)CaDiCaL version: 2.1.3
% 8.61/2.19 % (3442735)Termination reason: Instruction limit
% 8.61/2.19 % (3442735)Termination phase: Saturation
% 8.61/2.19 % (3442735)Time elapsed: 0.057 s
% 8.61/2.19 % (3442735)Peak memory usage: 89 MB
% 8.61/2.19 % (3442735)Instructions burned: 108 (million)
% 8.61/2.19 % (3442741)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3892230286:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 8.61/2.19 % (3442671)First to succeed.
% 8.61/2.19 % (3442671)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3442622"
% 8.61/2.19 % (3442738)Instruction limit reached!
% 8.61/2.19 % (3442738)------------------------------
% 8.61/2.19 % (3442738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.61/2.19 % (3442738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.61/2.19 % (3442738)CaDiCaL version: 2.1.3
% 8.61/2.19 % (3442738)Termination reason: Instruction limit
% 8.61/2.19 % (3442738)Termination phase: Saturation
% 8.61/2.19 % (3442738)Time elapsed: 0.124 s
% 8.61/2.19 % (3442738)Peak memory usage: 89 MB
% 8.61/2.19 % (3442738)Instructions burned: 243 (million)
% 8.61/2.19 % (3442743)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=174618351:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 8.61/2.19 % (3442743)Instruction limit reached!
% 8.61/2.19 % (3442743)------------------------------
% 8.61/2.19 % (3442743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.61/2.19 % (3442743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.61/2.19 % (3442743)CaDiCaL version: 2.1.3
% 8.61/2.19 % (3442743)Termination reason: Instruction limit
% 8.61/2.19 % (3442743)Termination phase: Saturation
% 8.61/2.19 % (3442743)Time elapsed: 0.070 s
% 8.61/2.19 % (3442743)Peak memory usage: 88 MB
% 8.61/2.19 % (3442743)Instructions burned: 135 (million)
% 8.61/2.19 % (3442670)Also succeeded, but the first one will report.
% 8.61/2.19 % (3442745)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1215529302:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 8.61/2.19 % (3442747)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=432453465:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 8.61/2.19 % (3442671)Refutation found. Thanks to Tanya!
% 8.61/2.19 % SZS status Unsatisfiable for theBenchmark
% 8.61/2.19 % SZS output start Proof for theBenchmark
% See solution above
% 8.61/2.20 % (3442671)------------------------------
% 8.61/2.20 % (3442671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.61/2.20 % (3442671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.61/2.20 % (3442671)CaDiCaL version: 2.1.3
% 8.61/2.20 % (3442671)Termination reason: Refutation
% 8.61/2.20 % (3442671)Time elapsed: 0.781 s
% 8.61/2.20 % (3442671)Peak memory usage: 135 MB
% 8.61/2.20 % (3442671)Instructions burned: 1590 (million)
% 8.61/2.20 % (3442671)------------------------------
% 8.61/2.20 % (3442671)------------------------------
% 8.61/2.20 % (3442622)Success in time 1.146 s
% 8.61/2.20 % Vampire exiting
%------------------------------------------------------------------------------