%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT036-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 11:45:53 AM UTC 2026
% Result : Unsatisfiable 9.94s 2.58s
% Output : Refutation 9.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 20
% Syntax : Number of formulae : 70 ( 70 unt; 10 def)
% Number of atoms : 70 ( 69 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 18 ( 18 ~; 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 : 16 ( 16 usr; 13 con; 0-2 aty)
% Number of variables : 12 ( 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,X1),join(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dist_join) ).
fof(f18,axiom,
! [X0,X1] : k(join(X0,X1)) = meet(k(X0),k(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',k_on_join) ).
fof(f19,axiom,
! [X0,X1] : k(meet(X0,X1)) = join(k(X0),k(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',k_on_meet) ).
fof(f24,axiom,
join(k(k(aa)),join(aa,k(aa))) = join(aa,k(aa)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lhs1) ).
fof(f25,plain,
join(aa,k(aa)) = join(k(k(aa)),join(aa,k(aa))),
inference(reorient_equations,[],[f24]) ).
fof(f26,axiom,
join(k(k(k(bb))),join(aa,k(aa))) = join(aa,k(aa)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lhs2) ).
fof(f27,plain,
join(aa,k(aa)) = join(k(k(k(bb))),join(aa,k(aa))),
inference(reorient_equations,[],[f26]) ).
fof(f28,axiom,
join(k(k(aa)),join(k(aa),join(k(bb),k(cc)))) = join(k(aa),join(k(bb),k(cc))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lhs3) ).
fof(f29,plain,
join(k(aa),join(k(bb),k(cc))) = join(k(k(aa)),join(k(aa),join(k(bb),k(cc)))),
inference(reorient_equations,[],[f28]) ).
fof(f30,axiom,
join(k(k(k(bb))),join(k(aa),join(k(bb),k(cc)))) = join(k(aa),join(k(bb),k(cc))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lhs4) ).
fof(f31,plain,
join(k(aa),join(k(bb),k(cc))) = join(k(k(k(bb))),join(k(aa),join(k(bb),k(cc)))),
inference(reorient_equations,[],[f30]) ).
fof(f32,negated_conjecture,
join(k(k(join(aa,k(bb)))),join(meet(aa,k(meet(bb,cc))),k(aa))) != join(meet(aa,k(meet(bb,cc))),k(aa)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rhs) ).
fof(f33,plain,
join(meet(aa,k(meet(bb,cc))),k(aa)) != join(k(k(join(aa,k(bb)))),join(meet(aa,k(meet(bb,cc))),k(aa))),
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF0 = meet(bb,cc),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f35,plain,
meet(bb,cc) = sF0,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF1 = k(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f37,plain,
k(sF0) = sF1,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF2 = meet(aa,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f39,plain,
meet(aa,sF1) = sF2,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF3 = k(aa),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f41,plain,
k(aa) = sF3,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF4 = join(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f43,plain,
join(sF2,sF3) = sF4,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF5 = k(bb),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f45,plain,
k(bb) = sF5,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF6 = join(aa,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f47,plain,
join(aa,sF5) = sF6,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF7 = k(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f49,plain,
k(sF6) = sF7,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF8 = k(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f51,plain,
k(sF7) = sF8,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF9 = join(sF8,sF4),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f53,plain,
join(sF8,sF4) = sF9,
inference(reorient_equations,[],[f52]) ).
fof(f54,plain,
sF4 != sF9,
inference(definition_folding,[],[f33,f53,f43,f41,f39,f37,f35,f51,f49,f47,f45,f43,f41,f39,f37,f35]) ).
fof(f55,plain,
join(aa,k(aa)) = join(join(aa,k(aa)),k(k(k(bb)))),
inference(forward_demodulation,[],[f27,f6]) ).
fof(f56,plain,
join(aa,k(aa)) = join(join(aa,k(aa)),k(k(aa))),
inference(forward_demodulation,[],[f25,f6]) ).
fof(f57,plain,
k(meet(bb,cc)) = sF1,
inference(forward_demodulation,[],[f37,f35]) ).
fof(f58,plain,
sF4 = join(sF2,k(aa)),
inference(forward_demodulation,[],[f43,f41]) ).
fof(f59,plain,
join(aa,k(bb)) = sF6,
inference(forward_demodulation,[],[f47,f45]) ).
fof(f60,plain,
sF8 = k(k(sF6)),
inference(forward_demodulation,[],[f51,f49]) ).
fof(f61,plain,
sF9 = join(sF4,sF8),
inference(forward_demodulation,[],[f53,f6]) ).
fof(f62,plain,
join(aa,k(aa)) = join(aa,join(k(aa),k(k(k(bb))))),
inference(forward_demodulation,[],[f55,f8]) ).
fof(f63,plain,
join(aa,k(aa)) = join(aa,join(k(aa),k(k(aa)))),
inference(forward_demodulation,[],[f56,f8]) ).
fof(f64,plain,
join(k(bb),k(cc)) = sF1,
inference(forward_demodulation,[],[f57,f19]) ).
fof(f65,plain,
sF4 = join(k(aa),sF2),
inference(forward_demodulation,[],[f58,f6]) ).
fof(f66,plain,
k(k(join(aa,k(bb)))) = sF8,
inference(forward_demodulation,[],[f60,f59]) ).
fof(f67,plain,
sF4 = join(k(aa),meet(aa,sF1)),
inference(forward_demodulation,[],[f65,f39]) ).
fof(f68,plain,
sF8 = k(meet(k(aa),k(k(bb)))),
inference(forward_demodulation,[],[f66,f18]) ).
fof(f69,plain,
sF4 = meet(join(k(aa),aa),join(k(aa),sF1)),
inference(forward_demodulation,[],[f67,f9]) ).
fof(f70,plain,
sF8 = join(k(k(aa)),k(k(k(bb)))),
inference(forward_demodulation,[],[f68,f19]) ).
fof(f71,plain,
sF4 = meet(join(k(aa),aa),join(k(aa),join(k(bb),k(cc)))),
inference(forward_demodulation,[],[f69,f64]) ).
fof(f72,plain,
sF4 = meet(join(aa,k(aa)),join(k(aa),join(k(bb),k(cc)))),
inference(forward_demodulation,[],[f71,f6]) ).
fof(f73,plain,
sF4 != join(sF4,sF8),
inference(superposition,[],[f54,f61]) ).
fof(f74,plain,
sF4 != join(sF4,join(k(k(aa)),k(k(k(bb))))),
inference(forward_demodulation,[],[f73,f70]) ).
fof(f75,plain,
sF4 != join(join(k(k(aa)),k(k(k(bb)))),sF4),
inference(forward_demodulation,[],[f74,f6]) ).
fof(f76,plain,
sF4 != join(k(k(aa)),join(k(k(k(bb))),sF4)),
inference(forward_demodulation,[],[f75,f8]) ).
fof(f77,plain,
meet(join(aa,k(aa)),join(k(aa),join(k(bb),k(cc)))) != join(k(k(aa)),join(k(k(k(bb))),meet(join(aa,k(aa)),join(k(aa),join(k(bb),k(cc)))))),
inference(forward_demodulation,[],[f76,f72]) ).
fof(f78,plain,
meet(join(aa,k(aa)),join(k(aa),join(k(bb),k(cc)))) != join(k(k(aa)),meet(join(k(k(k(bb))),join(aa,k(aa))),join(k(k(k(bb))),join(k(aa),join(k(bb),k(cc)))))),
inference(forward_demodulation,[],[f77,f9]) ).
fof(f79,plain,
meet(join(aa,k(aa)),join(k(aa),join(k(bb),k(cc)))) != meet(join(k(k(aa)),join(k(k(k(bb))),join(aa,k(aa)))),join(k(k(aa)),join(k(k(k(bb))),join(k(aa),join(k(bb),k(cc)))))),
inference(forward_demodulation,[],[f78,f9]) ).
fof(f80,plain,
meet(join(aa,k(aa)),join(k(aa),join(k(bb),k(cc)))) != meet(join(k(k(aa)),join(k(k(k(bb))),join(aa,k(aa)))),join(k(k(aa)),join(k(aa),join(k(bb),k(cc))))),
inference(forward_demodulation,[],[f79,f31]) ).
fof(f81,plain,
meet(join(aa,k(aa)),join(k(aa),join(k(bb),k(cc)))) != meet(join(k(k(aa)),join(k(k(k(bb))),join(aa,k(aa)))),join(k(aa),join(k(bb),k(cc)))),
inference(forward_demodulation,[],[f80,f29]) ).
fof(f82,plain,
meet(join(aa,k(aa)),join(k(aa),join(k(bb),k(cc)))) != meet(join(k(k(aa)),join(join(aa,k(aa)),k(k(k(bb))))),join(k(aa),join(k(bb),k(cc)))),
inference(forward_demodulation,[],[f81,f6]) ).
fof(f83,plain,
meet(join(aa,k(aa)),join(k(aa),join(k(bb),k(cc)))) != meet(join(k(k(aa)),join(aa,join(k(aa),k(k(k(bb)))))),join(k(aa),join(k(bb),k(cc)))),
inference(forward_demodulation,[],[f82,f8]) ).
fof(f84,plain,
meet(join(aa,k(aa)),join(k(aa),join(k(bb),k(cc)))) != meet(join(k(k(aa)),join(aa,k(aa))),join(k(aa),join(k(bb),k(cc)))),
inference(forward_demodulation,[],[f83,f62]) ).
fof(f85,plain,
meet(join(aa,k(aa)),join(k(aa),join(k(bb),k(cc)))) != meet(join(join(aa,k(aa)),k(k(aa))),join(k(aa),join(k(bb),k(cc)))),
inference(forward_demodulation,[],[f84,f6]) ).
fof(f86,plain,
meet(join(aa,k(aa)),join(k(aa),join(k(bb),k(cc)))) != meet(join(aa,join(k(aa),k(k(aa)))),join(k(aa),join(k(bb),k(cc)))),
inference(forward_demodulation,[],[f85,f8]) ).
fof(f87,plain,
meet(join(aa,k(aa)),join(k(aa),join(k(bb),k(cc)))) != meet(join(aa,k(aa)),join(k(aa),join(k(bb),k(cc)))),
inference(forward_demodulation,[],[f86,f63]) ).
fof(f88,plain,
$false,
inference(trivial_inequality_removal,[],[f87]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT036-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.43 % Computer : n014.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sun Sep 27 13:57:32 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.48 Running first-order theorem proving
% 0.22/0.48 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
% 8.95/2.36 % (833872)Input is clausal, will run a generic CNF schedule.
% 8.95/2.36 % (833891)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1008665544:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.95/2.36 % (833893)dis-21_1_sil=8000:lcm=predicate:random_seed=1172358497: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)
% 8.95/2.36 % (833893)Refutation not found, incomplete strategy
% 8.95/2.36 % (833893)------------------------------
% 8.95/2.36 % (833893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.36 % (833893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.36 % (833893)CaDiCaL version: 2.1.3
% 8.95/2.36 % (833893)Termination reason: Refutation not found, incomplete strategy
% 8.95/2.36 % (833893)Time elapsed: 0.002 s
% 8.95/2.36 % (833893)Peak memory usage: 88 MB
% 8.95/2.36 % (833893)Instructions burned: 1 (million)
% 8.95/2.36 % (833892)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1952115313:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.95/2.36 % (833891)Instruction limit reached!
% 8.95/2.36 % (833891)------------------------------
% 8.95/2.36 % (833891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.36 % (833891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.36 % (833891)CaDiCaL version: 2.1.3
% 8.95/2.36 % (833891)Termination reason: Instruction limit
% 8.95/2.36 % (833891)Termination phase: Saturation
% 8.95/2.36 % (833891)Time elapsed: 0.060 s
% 8.95/2.36 % (833891)Peak memory usage: 89 MB
% 8.95/2.36 % (833891)Instructions burned: 116 (million)
% 8.95/2.36 % (833889)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3934305197:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.95/2.36 % (833890)lrs+10_1_sil=8000:sp=occurrence:random_seed=59114184:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.95/2.36 % (833888)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3555174211:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.95/2.36 % (833887)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=2769791042:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.95/2.36 % (833890)Instruction limit reached!
% 8.95/2.36 % (833890)------------------------------
% 8.95/2.36 % (833890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.36 % (833890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.36 % (833890)CaDiCaL version: 2.1.3
% 8.95/2.36 % (833890)Termination reason: Instruction limit
% 8.95/2.36 % (833890)Termination phase: Saturation
% 8.95/2.36 % (833890)Time elapsed: 0.104 s
% 8.95/2.36 % (833890)Peak memory usage: 88 MB
% 8.95/2.36 % (833890)Instructions burned: 107 (million)
% 8.95/2.36 % (833892)Instruction limit reached!
% 8.95/2.36 % (833892)------------------------------
% 8.95/2.36 % (833892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.36 % (833892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.36 % (833892)CaDiCaL version: 2.1.3
% 8.95/2.36 % (833892)Termination reason: Instruction limit
% 8.95/2.36 % (833892)Termination phase: Saturation
% 8.95/2.36 % (833892)Time elapsed: 0.171 s
% 8.95/2.36 % (833892)Peak memory usage: 89 MB
% 8.95/2.36 % (833892)Instructions burned: 180 (million)
% 8.95/2.36 % (833903)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=672248105:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 8.95/2.36 % (833904)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1626896818:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 8.95/2.36 % (833893)------------------------------
% 8.95/2.36 % (833893)------------------------------
% 8.95/2.36 % (833905)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3669179385:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 8.95/2.36 % (833903)Instruction limit reached!
% 8.95/2.36 % (833903)------------------------------
% 8.95/2.36 % (833903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.36 % (833903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.36 % (833903)CaDiCaL version: 2.1.3
% 8.95/2.36 % (833903)Termination reason: Instruction limit
% 8.95/2.36 % (833903)Termination phase: Saturation
% 8.95/2.36 % (833903)Time elapsed: 0.137 s
% 8.95/2.36 % (833903)Peak memory usage: 89 MB
% 8.95/2.36 % (833903)Instructions burned: 143 (million)
% 8.95/2.36 % (833904)Instruction limit reached!
% 8.95/2.36 % (833904)------------------------------
% 8.95/2.36 % (833904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.36 % (833904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.36 % (833904)CaDiCaL version: 2.1.3
% 8.95/2.36 % (833904)Termination reason: Instruction limit
% 8.95/2.36 % (833904)Termination phase: Saturation
% 8.95/2.36 % (833904)Time elapsed: 0.184 s
% 8.95/2.36 % (833904)Peak memory usage: 89 MB
% 8.95/2.36 % (833904)Instructions burned: 190 (million)
% 8.95/2.36 % (833908)lrs+10_64_to=lpo:sil=8000:random_seed=463119582:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 8.95/2.36 % (833911)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1917897550:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 8.95/2.36 % (833905)Instruction limit reached!
% 8.95/2.36 % (833905)------------------------------
% 8.95/2.36 % (833905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.36 % (833905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.36 % (833905)CaDiCaL version: 2.1.3
% 8.95/2.36 % (833905)Termination reason: Instruction limit
% 8.95/2.36 % (833905)Termination phase: Saturation
% 8.95/2.36 % (833905)Time elapsed: 0.222 s
% 8.95/2.36 % (833905)Peak memory usage: 90 MB
% 8.95/2.36 % (833905)Instructions burned: 220 (million)
% 8.95/2.36 % (833908)Instruction limit reached!
% 8.95/2.36 % (833908)------------------------------
% 8.95/2.36 % (833908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.36 % (833908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.36 % (833908)CaDiCaL version: 2.1.3
% 8.95/2.36 % (833908)Termination reason: Instruction limit
% 8.95/2.36 % (833908)Termination phase: Saturation
% 8.95/2.36 % (833908)Time elapsed: 0.126 s
% 8.95/2.36 % (833908)Peak memory usage: 88 MB
% 8.95/2.36 % (833908)Instructions burned: 127 (million)
% 8.95/2.36 % (833913)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3114711272:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi)
% 8.95/2.36 % (833911)Instruction limit reached!
% 8.95/2.36 % (833911)------------------------------
% 8.95/2.36 % (833911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.36 % (833911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.36 % (833911)CaDiCaL version: 2.1.3
% 8.95/2.36 % (833911)Termination reason: Instruction limit
% 8.95/2.36 % (833911)Termination phase: Saturation
% 8.95/2.36 % (833911)Time elapsed: 0.197 s
% 8.95/2.36 % (833911)Peak memory usage: 89 MB
% 8.95/2.36 % (833911)Instructions burned: 194 (million)
% 8.95/2.36 % (833916)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1141510360:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 8.95/2.36 % (833917)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=3328472782:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 8.95/2.36 % (833917)First to succeed.
% 8.95/2.36 % (833917)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-833872"
% 8.95/2.36 % (833913)Instruction limit reached!
% 8.95/2.36 % (833913)------------------------------
% 8.95/2.36 % (833913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.36 % (833913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.36 % (833913)CaDiCaL version: 2.1.3
% 8.95/2.36 % (833913)Termination reason: Instruction limit
% 8.95/2.36 % (833913)Termination phase: Saturation
% 8.95/2.36 % (833913)Time elapsed: 0.159 s
% 8.95/2.36 % (833913)Peak memory usage: 91 MB
% 8.95/2.36 % (833913)Instructions burned: 157 (million)
% 8.95/2.36 % (833920)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1519830567:i=107_2990 on theBenchmark for (2990ds/107Mi)
% 8.95/2.36 % (833920)Instruction limit reached!
% 8.95/2.36 % (833920)------------------------------
% 9.94/2.58 % (833920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.94/2.58 % (833920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.94/2.58 % (833920)CaDiCaL version: 2.1.3
% 9.94/2.58 % (833920)Termination reason: Instruction limit
% 9.94/2.58 % (833920)Termination phase: Saturation
% 9.94/2.58 % (833920)Time elapsed: 0.107 s
% 9.94/2.58 % (833920)Peak memory usage: 88 MB
% 9.94/2.58 % (833920)Instructions burned: 107 (million)
% 9.94/2.58 % (833917)Refutation found. Thanks to Tanya!
% 9.94/2.58 % SZS status Unsatisfiable for theBenchmark
% 9.94/2.58 % SZS output start Proof for theBenchmark
% See solution above
% 9.94/2.58 % (833917)------------------------------
% 9.94/2.58 % (833917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.94/2.58 % (833917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.94/2.58 % (833917)CaDiCaL version: 2.1.3
% 9.94/2.58 % (833917)Termination reason: Refutation
% 9.94/2.58 % (833917)Time elapsed: 0.004 s
% 9.94/2.58 % (833917)Peak memory usage: 89 MB
% 9.94/2.58 % (833917)Instructions burned: 6 (million)
% 9.94/2.58 % (833917)------------------------------
% 9.94/2.58 % (833917)------------------------------
% 9.94/2.58 % (833872)Success in time 1.294 s
% 9.94/2.58 % Vampire exiting
%------------------------------------------------------------------------------