%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET039-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:39:44 PM UTC 2026
% Result : Unsatisfiable 74.71s 11.68s
% Output : Refutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 19
% Syntax : Number of formulae : 62 ( 16 unt; 0 def)
% Number of atoms : 181 ( 42 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 239 ( 120 ~; 119 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-2 aty)
% Number of variables : 168 ( 168 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X2,X0,X1] :
( ~ member(X0,non_ordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',non_ordered_pair1) ).
fof(f6,axiom,
! [X2,X0,X1] :
( member(X0,non_ordered_pair(X1,X2))
| ~ little_set(X0)
| X0 != X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',non_ordered_pair2) ).
fof(f8,axiom,
! [X0,X1] : little_set(non_ordered_pair(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',non_ordered_pair4) ).
fof(f9,axiom,
! [X0] : singleton_set(X0) = non_ordered_pair(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set) ).
fof(f79,axiom,
! [X2,X0,X1] :
( ~ subset(X0,X1)
| ~ member(X2,X0)
| member(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subset1) ).
fof(f88,axiom,
! [X0,X1] :
( ~ relation(X0)
| ~ member(X1,X0)
| ordered_pair_predicate(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',relation1) ).
fof(f120,axiom,
! [X0,X1] :
( member(f27(X0,X1),X1)
| ~ member(X0,range_of(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',range_of2) ).
fof(f121,axiom,
! [X0,X1] :
( ~ member(X0,range_of(X1))
| X0 = second(f27(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',range_of3) ).
fof(f122,plain,
! [X0,X1] :
( second(f27(X0,X1)) = X0
| ~ member(X0,range_of(X1)) ),
inference(reorient_equations,[],[f121]) ).
fof(f123,axiom,
! [X2,X0,X1] :
( member(X0,range_of(X1))
| ~ little_set(X0)
| ~ ordered_pair_predicate(X2)
| ~ member(X2,X1)
| X0 != second(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',range_of4) ).
fof(f124,plain,
! [X2,X0,X1] :
( member(X0,range_of(X1))
| ~ little_set(X0)
| ~ ordered_pair_predicate(X2)
| ~ member(X2,X1)
| second(X2) != X0 ),
inference(reorient_equations,[],[f123]) ).
fof(f153,axiom,
! [X2,X3,X0,X1,X4,X5] :
( member(X0,compose(X1,X2))
| ~ little_set(X0)
| ~ little_set(X3)
| ~ little_set(X4)
| ~ little_set(X5)
| X0 != ordered_pair(X3,X4)
| ~ member(ordered_pair(X3,X5),X1)
| ~ member(ordered_pair(X5,X4),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compose7) ).
fof(f154,plain,
! [X2,X3,X0,X1,X4,X5] :
( member(X0,compose(X1,X2))
| ~ little_set(X0)
| ~ little_set(X3)
| ~ little_set(X4)
| ~ little_set(X5)
| ordered_pair(X3,X4) != X0
| ~ member(ordered_pair(X3,X5),X1)
| ~ member(ordered_pair(X5,X4),X2) ),
inference(reorient_equations,[],[f153]) ).
fof(f168,axiom,
! [X0,X1] :
( second(ordered_pair(X0,X1)) = X1
| ~ little_set(X1)
| ~ little_set(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',property_of_second) ).
fof(f171,axiom,
! [X0] :
( member(X0,singleton_set(X0))
| ~ little_set(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',property_of_singleton_sets) ).
fof(f172,axiom,
! [X0,X1] : little_set(ordered_pair(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pairs_are_small1) ).
fof(f175,axiom,
! [X0,X1] : subset(apply(X0,X1),sigma(image(singleton_set(X1),X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',image_and_apply1) ).
fof(f177,axiom,
! [X0,X1] :
( little_set(apply(X0,X1))
| ~ function(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',function_values_are_small) ).
fof(f178,axiom,
! [X0,X1] : relation(compose(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_is_a_relation) ).
fof(f179,axiom,
! [X0,X1] : subset(range_of(compose(X0,X1)),range_of(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',range_of_composition) ).
fof(f186,axiom,
function(a_function),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_function) ).
fof(f188,negated_conjecture,
~ subset(apply(another_function,apply(a_function,a)),apply(compose(another_function,a_function),a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_apply_for_composition1) ).
fof(f193,plain,
! [X2,X3,X1,X4,X5] :
( member(ordered_pair(X3,X4),compose(X1,X2))
| ~ little_set(ordered_pair(X3,X4))
| ~ little_set(X3)
| ~ little_set(X4)
| ~ little_set(X5)
| ~ member(ordered_pair(X3,X5),X1)
| ~ member(ordered_pair(X5,X4),X2) ),
inference(equality_resolution,[],[f154]) ).
fof(f195,plain,
! [X2,X1] :
( member(X1,non_ordered_pair(X1,X2))
| ~ little_set(X1) ),
inference(equality_resolution,[],[f6]) ).
fof(f200,plain,
! [X2,X1] :
( member(second(X2),range_of(X1))
| ~ little_set(second(X2))
| ~ ordered_pair_predicate(X2)
| ~ member(X2,X1) ),
inference(equality_resolution,[],[f124]) ).
fof(f202,plain,
! [X2,X0,X1] :
( member(X0,range_of(X1))
| ~ member(X0,range_of(compose(X1,X2))) ),
inference(resolution,[],[f179,f79]) ).
fof(f217,plain,
! [X2,X0,X1] :
( f27(X0,non_ordered_pair(X1,X2)) = X2
| f27(X0,non_ordered_pair(X1,X2)) = X1
| ~ member(X0,range_of(non_ordered_pair(X1,X2))) ),
inference(resolution,[],[f5,f120]) ).
fof(f337,plain,
! [X2,X0,X1] :
( ordered_pair_predicate(X0)
| ~ member(X0,compose(X1,X2)) ),
inference(resolution,[],[f88,f178]) ).
fof(f514,plain,
! [X2,X0,X1] :
( X1 != X2
| f27(X0,non_ordered_pair(X1,X2)) = X1
| ~ member(X0,range_of(non_ordered_pair(X1,X2))) ),
inference(equality_factoring,[],[f217]) ).
fof(f521,plain,
! [X0,X1] :
( f27(X0,non_ordered_pair(X1,X1)) = X1
| ~ member(X0,range_of(non_ordered_pair(X1,X1))) ),
inference(equality_resolution,[],[f514]) ).
fof(f522,plain,
! [X0,X1] :
( f27(X0,singleton_set(X1)) = X1
| ~ member(X0,range_of(non_ordered_pair(X1,X1))) ),
inference(forward_demodulation,[],[f521,f9]) ).
fof(f523,plain,
! [X0,X1] :
( f27(X0,singleton_set(X1)) = X1
| ~ member(X0,range_of(singleton_set(X1))) ),
inference(forward_demodulation,[],[f522,f9]) ).
fof(f528,plain,
! [X0,X1] :
( second(X0) = X1
| ~ member(X1,range_of(singleton_set(X0)))
| ~ member(X1,range_of(singleton_set(X0))) ),
inference(superposition,[],[f122,f523]) ).
fof(f531,plain,
! [X0,X1] :
( ~ member(X1,range_of(singleton_set(X0)))
| second(X0) = X1 ),
inference(duplicate_literal_removal,[],[f528]) ).
fof(f537,plain,
! [X2,X0,X1] :
( ~ member(X1,range_of(compose(singleton_set(X0),X2)))
| second(X0) = X1 ),
inference(resolution,[],[f531,f202]) ).
fof(f577,plain,
! [X2,X0,X1] :
( second(X1) = second(X0)
| ~ little_set(second(X1))
| ~ ordered_pair_predicate(X1)
| ~ member(X1,compose(singleton_set(X0),X2)) ),
inference(resolution,[],[f537,f200]) ).
fof(f582,plain,
! [X2,X0,X1] :
( ~ little_set(second(X1))
| second(X1) = second(X0)
| ~ member(X1,compose(singleton_set(X0),X2)) ),
inference(forward_subsumption_resolution,[],[f577,f337]) ).
fof(f609,plain,
! [X2,X3,X0,X1] :
( ~ little_set(X0)
| second(X2) = X0
| ~ member(ordered_pair(X1,X0),compose(singleton_set(X2),X3))
| ~ little_set(X0)
| ~ little_set(X1) ),
inference(superposition,[],[f582,f168]) ).
fof(f611,plain,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X1,X0),compose(singleton_set(X2),X3))
| second(X2) = X0
| ~ little_set(X0)
| ~ little_set(X1) ),
inference(duplicate_literal_removal,[],[f609]) ).
fof(f614,plain,
! [X2,X3,X0,X1,X4] :
( second(X0) = X1
| ~ little_set(X1)
| ~ little_set(X2)
| ~ little_set(ordered_pair(X2,X1))
| ~ little_set(X2)
| ~ little_set(X1)
| ~ little_set(X3)
| ~ member(ordered_pair(X2,X3),singleton_set(X0))
| ~ member(ordered_pair(X3,X1),X4) ),
inference(resolution,[],[f611,f193]) ).
fof(f616,plain,
! [X2,X3,X0,X1,X4] :
( second(X0) = X1
| ~ little_set(X1)
| ~ little_set(X2)
| ~ little_set(ordered_pair(X2,X1))
| ~ little_set(X3)
| ~ member(ordered_pair(X2,X3),singleton_set(X0))
| ~ member(ordered_pair(X3,X1),X4) ),
inference(duplicate_literal_removal,[],[f614]) ).
fof(f617,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(ordered_pair(X2,X3),singleton_set(X0))
| ~ little_set(X1)
| ~ little_set(X2)
| ~ little_set(X3)
| second(X0) = X1
| ~ member(ordered_pair(X3,X1),X4) ),
inference(forward_subsumption_resolution,[],[f616,f172]) ).
fof(f641,plain,
! [X2,X3,X0,X1] :
( ~ little_set(X0)
| ~ little_set(X1)
| ~ little_set(X2)
| second(ordered_pair(X1,X2)) = X0
| ~ member(ordered_pair(X2,X0),X3)
| ~ little_set(ordered_pair(X1,X2)) ),
inference(resolution,[],[f617,f171]) ).
fof(f642,plain,
! [X2,X3,X0,X1] :
( ~ little_set(X0)
| ~ little_set(X1)
| ~ little_set(X2)
| second(ordered_pair(X1,X2)) = X0
| ~ member(ordered_pair(X2,X0),X3) ),
inference(forward_subsumption_resolution,[],[f641,f172]) ).
fof(f647,plain,
! [X2,X3,X0,X1] :
( ~ little_set(X0)
| ~ little_set(X1)
| ~ little_set(X2)
| X0 = X2
| ~ member(ordered_pair(X2,X0),X3) ),
inference(forward_subsumption_demodulation,[],[f642,f168]) ).
fof(f648,plain,
! [X2,X3,X0] :
( ~ little_set(X0)
| ~ little_set(X2)
| X0 = X2
| ~ member(ordered_pair(X2,X0),X3) ),
inference(condensation,[],[f647]) ).
fof(f661,plain,
! [X2,X3,X0,X1] :
( ~ function(X1)
| apply(X1,X2) = X0
| ~ member(ordered_pair(X0,apply(X1,X2)),X3)
| ~ little_set(X0) ),
inference(resolution,[],[f648,f177]) ).
fof(f684,plain,
! [X2,X0,X1] :
( ~ little_set(X1)
| ~ member(ordered_pair(X1,apply(a_function,X0)),X2)
| apply(a_function,X0) = X1 ),
inference(resolution,[],[f661,f186]) ).
fof(f687,plain,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(non_ordered_pair(X0,X1),apply(a_function,X2)),X3)
| non_ordered_pair(X0,X1) = apply(a_function,X2) ),
inference(resolution,[],[f684,f8]) ).
fof(f704,plain,
! [X2,X0,X1] :
( non_ordered_pair(X0,X1) = apply(a_function,X2)
| ~ little_set(ordered_pair(non_ordered_pair(X0,X1),apply(a_function,X2))) ),
inference(resolution,[],[f687,f171]) ).
fof(f726,plain,
! [X2,X0,X1] : non_ordered_pair(X0,X1) = apply(a_function,X2),
inference(forward_subsumption_resolution,[],[f704,f172]) ).
fof(f733,plain,
! [X2,X3,X0,X1] :
( ~ member(X1,apply(a_function,X0))
| X1 = X2
| X1 = X3 ),
inference(superposition,[],[f5,f726]) ).
fof(f734,plain,
! [X0] : little_set(apply(a_function,X0)),
inference(superposition,[],[f8,f726]) ).
fof(f738,plain,
! [X0,X1] :
( member(X1,apply(a_function,X0))
| ~ little_set(X1) ),
inference(superposition,[],[f195,f726]) ).
fof(f745,plain,
! [X0,X1] : ~ subset(apply(another_function,non_ordered_pair(X0,X1)),apply(compose(another_function,a_function),a)),
inference(superposition,[],[f188,f726]) ).
fof(f778,plain,
! [X3,X0,X1] :
( ~ member(X1,apply(a_function,X0))
| X1 = X3 ),
inference(condensation,[],[f733]) ).
fof(f898,plain,
! [X0,X1] :
( ~ little_set(X0)
| X0 = X1 ),
inference(resolution,[],[f738,f778]) ).
fof(f914,plain,
! [X0,X1] : apply(a_function,X0) = X1,
inference(resolution,[],[f898,f734]) ).
fof(f1065,plain,
! [X2,X0,X1] : subset(apply(X1,X2),apply(a_function,X0)),
inference(superposition,[],[f175,f914]) ).
fof(f1141,plain,
! [X0] : ~ subset(apply(a_function,X0),apply(compose(another_function,a_function),a)),
inference(superposition,[],[f745,f914]) ).
fof(f1260,plain,
! [X0,X1] : ~ subset(apply(a_function,X1),apply(a_function,X0)),
inference(superposition,[],[f1141,f914]) ).
fof(f1261,plain,
$false,
inference(forward_subsumption_resolution,[],[f1260,f1065]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET039-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.33 % Computer : n012.cluster.edu
% 0.07/0.33 % Model : x86_64 x86_64
% 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33 % Memory : 8046.5625MB
% 0.07/0.33 % OS : Linux 6.8.0-71-generic
% 0.07/0.33 % CPULimit : 300
% 0.07/0.33 % WCLimit : 300
% 0.07/0.33 % DateTime : Mon Sep 28 00:18:50 UTC 2026
% 0.10/0.34 % CPUTime :
% 0.10/0.34 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 Running first-order theorem proving
% 0.10/0.36 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
% 12.39/2.45 % (2900460)Input is clausal, will run a generic CNF schedule.
% 12.39/2.45 % (2900466)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=2965936055:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.39/2.45 % (2900467)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=97249327:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.39/2.45 % (2900470)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3648488632:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.39/2.45 % (2900468)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1242080366:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.39/2.45 % (2900470)Instruction limit reached!
% 12.39/2.45 % (2900470)------------------------------
% 12.39/2.45 % (2900470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.39/2.45 % (2900470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.45 % (2900470)CaDiCaL version: 2.1.3
% 12.39/2.45 % (2900470)Termination reason: Instruction limit
% 12.39/2.45 % (2900470)Termination phase: Saturation
% 12.39/2.45 % (2900470)Time elapsed: 0.026 s
% 12.39/2.45 % (2900470)Peak memory usage: 88 MB
% 12.39/2.45 % (2900470)Instructions burned: 119 (million)
% 12.39/2.45 % (2900469)lrs+10_1_sil=8000:sp=occurrence:random_seed=3713252887:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.39/2.45 % (2900471)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1921005761:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.39/2.45 % (2900472)dis-21_1_sil=8000:lcm=predicate:random_seed=1644244634: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)
% 12.39/2.45 % (2900469)Instruction limit reached!
% 12.39/2.45 % (2900469)------------------------------
% 12.39/2.45 % (2900469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.39/2.45 % (2900469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.45 % (2900469)CaDiCaL version: 2.1.3
% 12.39/2.45 % (2900469)Termination reason: Instruction limit
% 12.39/2.45 % (2900469)Termination phase: Saturation
% 12.39/2.45 % (2900469)Time elapsed: 0.036 s
% 12.39/2.45 % (2900469)Peak memory usage: 90 MB
% 12.39/2.45 % (2900469)Instructions burned: 109 (million)
% 12.39/2.45 % (2900472)Instruction limit reached!
% 12.39/2.45 % (2900472)------------------------------
% 12.39/2.45 % (2900472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.39/2.45 % (2900472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.45 % (2900472)CaDiCaL version: 2.1.3
% 12.39/2.45 % (2900472)Termination reason: Instruction limit
% 12.39/2.45 % (2900472)Termination phase: Saturation
% 12.39/2.45 % (2900472)Time elapsed: 0.063 s
% 12.39/2.45 % (2900472)Peak memory usage: 88 MB
% 12.39/2.45 % (2900472)Instructions burned: 119 (million)
% 12.39/2.45 % (2900471)Instruction limit reached!
% 12.39/2.45 % (2900471)------------------------------
% 12.39/2.45 % (2900471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.39/2.45 % (2900471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.45 % (2900471)CaDiCaL version: 2.1.3
% 12.39/2.45 % (2900471)Termination reason: Instruction limit
% 12.39/2.45 % (2900471)Termination phase: Saturation
% 12.39/2.45 % (2900471)Time elapsed: 0.069 s
% 12.39/2.45 % (2900471)Peak memory usage: 88 MB
% 12.39/2.45 % (2900471)Instructions burned: 182 (million)
% 12.39/2.45 % (2900477)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=415928528:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 12.39/2.45 % (2900477)Refutation not found, incomplete strategy
% 12.39/2.45 % (2900477)------------------------------
% 12.39/2.45 % (2900477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.39/2.45 % (2900477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.45 % (2900477)CaDiCaL version: 2.1.3
% 12.39/2.45 % (2900477)Termination reason: Refutation not found, incomplete strategy
% 12.39/2.45 % (2900477)Time elapsed: 0.002 s
% 12.39/2.45 % (2900477)Peak memory usage: 88 MB
% 12.39/2.45 % (2900477)Instructions burned: 5 (million)
% 12.39/2.45 % (2900485)lrs+10_64_to=lpo:sil=8000:random_seed=4172528935:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 20.43/3.65 % (2900483)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1109447919: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)
% 20.43/3.65 % (2900485)Instruction limit reached!
% 20.43/3.65 % (2900485)------------------------------
% 20.43/3.65 % (2900485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.43/3.65 % (2900485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.43/3.65 % (2900485)CaDiCaL version: 2.1.3
% 20.43/3.65 % (2900485)Termination reason: Instruction limit
% 20.43/3.65 % (2900485)Termination phase: Saturation
% 20.43/3.65 % (2900485)Time elapsed: 0.047 s
% 20.43/3.65 % (2900485)Peak memory usage: 91 MB
% 20.43/3.65 % (2900485)Instructions burned: 126 (million)
% 20.43/3.65 % (2900484)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3720222511:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 20.43/3.65 % (2900483)Instruction limit reached!
% 20.43/3.65 % (2900483)------------------------------
% 20.43/3.65 % (2900483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.43/3.65 % (2900483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.43/3.65 % (2900483)CaDiCaL version: 2.1.3
% 20.43/3.65 % (2900483)Termination reason: Instruction limit
% 20.43/3.65 % (2900483)Termination phase: Saturation
% 20.43/3.65 % (2900483)Time elapsed: 0.092 s
% 20.43/3.65 % (2900483)Peak memory usage: 90 MB
% 20.43/3.65 % (2900483)Instructions burned: 191 (million)
% 20.43/3.65 % (2900477)------------------------------
% 20.43/3.65 % (2900477)------------------------------
% 20.43/3.65 % (2900484)Instruction limit reached!
% 20.43/3.65 % (2900484)------------------------------
% 20.43/3.65 % (2900484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.43/3.65 % (2900484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.43/3.65 % (2900484)CaDiCaL version: 2.1.3
% 20.43/3.65 % (2900484)Termination reason: Instruction limit
% 20.43/3.65 % (2900484)Termination phase: Saturation
% 20.43/3.65 % (2900484)Time elapsed: 0.075 s
% 20.43/3.65 % (2900484)Peak memory usage: 88 MB
% 20.43/3.65 % (2900484)Instructions burned: 220 (million)
% 20.43/3.65 % (2900490)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3849843976:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 20.43/3.65 % (2900493)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=308222897:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 20.43/3.65 % (2900492)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3076769462:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 20.43/3.65 % (2900490)Instruction limit reached!
% 20.43/3.65 % (2900490)------------------------------
% 20.43/3.65 % (2900490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.43/3.65 % (2900490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.43/3.65 % (2900490)CaDiCaL version: 2.1.3
% 20.43/3.65 % (2900490)Termination reason: Instruction limit
% 20.43/3.65 % (2900490)Termination phase: Saturation
% 20.43/3.65 % (2900490)Time elapsed: 0.076 s
% 20.43/3.65 % (2900490)Peak memory usage: 89 MB
% 20.43/3.65 % (2900490)Instructions burned: 196 (million)
% 20.43/3.65 % (2900495)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=3063354928:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 20.43/3.65 % (2900492)Instruction limit reached!
% 20.43/3.65 % (2900492)------------------------------
% 20.43/3.65 % (2900492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.43/3.65 % (2900492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.43/3.65 % (2900492)CaDiCaL version: 2.1.3
% 20.43/3.65 % (2900492)Termination reason: Instruction limit
% 20.43/3.65 % (2900492)Termination phase: Saturation
% 20.43/3.65 % (2900492)Time elapsed: 0.086 s
% 20.43/3.65 % (2900492)Peak memory usage: 91 MB
% 20.43/3.65 % (2900492)Instructions burned: 157 (million)
% 20.43/3.65 % (2900495)Instruction limit reached!
% 20.43/3.65 % (2900495)------------------------------
% 20.43/3.65 % (2900495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.43/3.65 % (2900495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.18/5.27 % (2900495)CaDiCaL version: 2.1.3
% 32.18/5.27 % (2900495)Termination reason: Instruction limit
% 32.18/5.27 % (2900495)Termination phase: Saturation
% 32.18/5.27 % (2900495)Time elapsed: 0.056 s
% 32.18/5.27 % (2900495)Peak memory usage: 89 MB
% 32.18/5.27 % (2900495)Instructions burned: 107 (million)
% 32.18/5.27 % (2900499)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=864541764:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 32.18/5.27 % (2900499)Instruction limit reached!
% 32.18/5.27 % (2900499)------------------------------
% 32.18/5.27 % (2900499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.18/5.27 % (2900499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.18/5.27 % (2900499)CaDiCaL version: 2.1.3
% 32.18/5.27 % (2900499)Termination reason: Instruction limit
% 32.18/5.27 % (2900499)Termination phase: Saturation
% 32.18/5.27 % (2900499)Time elapsed: 0.064 s
% 32.18/5.27 % (2900499)Peak memory usage: 90 MB
% 32.18/5.27 % (2900499)Instructions burned: 107 (million)
% 32.18/5.27 % (2900501)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3958619133:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 32.18/5.27 % (2900502)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1431852339:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 32.18/5.27 % (2900501)Instruction limit reached!
% 32.18/5.27 % (2900501)------------------------------
% 32.18/5.27 % (2900501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.18/5.27 % (2900501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.18/5.27 % (2900501)CaDiCaL version: 2.1.3
% 32.18/5.27 % (2900501)Termination reason: Instruction limit
% 32.18/5.27 % (2900501)Termination phase: Saturation
% 32.18/5.27 % (2900501)Time elapsed: 0.144 s
% 32.18/5.27 % (2900501)Peak memory usage: 90 MB
% 32.18/5.27 % (2900501)Instructions burned: 242 (million)
% 32.18/5.27 % (2900504)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4220187487:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 32.18/5.27 % (2900504)Instruction limit reached!
% 32.18/5.27 % (2900504)------------------------------
% 32.18/5.27 % (2900504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.18/5.27 % (2900504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.18/5.27 % (2900504)CaDiCaL version: 2.1.3
% 32.18/5.27 % (2900504)Termination reason: Instruction limit
% 32.18/5.27 % (2900504)Termination phase: Saturation
% 32.18/5.27 % (2900504)Time elapsed: 0.085 s
% 32.18/5.27 % (2900504)Peak memory usage: 90 MB
% 32.18/5.27 % (2900504)Instructions burned: 134 (million)
% 32.18/5.27 % (2900507)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=423875300:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 32.18/5.27 % (2900509)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3120624401:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 32.18/5.27 % (2900507)Instruction limit reached!
% 32.18/5.27 % (2900507)------------------------------
% 32.18/5.27 % (2900507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.18/5.27 % (2900507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.18/5.27 % (2900507)CaDiCaL version: 2.1.3
% 32.18/5.27 % (2900507)Termination reason: Instruction limit
% 32.18/5.27 % (2900507)Termination phase: Saturation
% 32.18/5.27 % (2900507)Time elapsed: 0.238 s
% 32.18/5.27 % (2900507)Peak memory usage: 93 MB
% 32.18/5.27 % (2900507)Instructions burned: 501 (million)
% 32.18/5.27 % (2900509)Instruction limit reached!
% 32.18/5.27 % (2900509)------------------------------
% 32.18/5.27 % (2900509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.18/5.27 % (2900509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.18/5.27 % (2900509)CaDiCaL version: 2.1.3
% 32.18/5.27 % (2900509)Termination reason: Instruction limit
% 32.18/5.27 % (2900509)Termination phase: Saturation
% 32.18/5.27 % (2900509)Time elapsed: 0.108 s
% 32.18/5.27 % (2900509)Peak memory usage: 90 MB
% 32.18/5.27 % (2900509)Instructions burned: 193 (million)
% 32.18/5.27 % (2900514)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3638591944:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 54.83/8.46 % (2900515)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1420877737:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 54.83/8.46 % (2900515)Instruction limit reached!
% 54.83/8.46 % (2900515)------------------------------
% 54.83/8.46 % (2900515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.83/8.46 % (2900515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.83/8.46 % (2900515)CaDiCaL version: 2.1.3
% 54.83/8.46 % (2900515)Termination reason: Instruction limit
% 54.83/8.46 % (2900515)Termination phase: Saturation
% 54.83/8.46 % (2900515)Time elapsed: 0.087 s
% 54.83/8.46 % (2900515)Peak memory usage: 89 MB
% 54.83/8.46 % (2900515)Instructions burned: 156 (million)
% 54.83/8.46 % (2900514)Instruction limit reached!
% 54.83/8.46 % (2900514)------------------------------
% 54.83/8.46 % (2900514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.83/8.46 % (2900514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.83/8.46 % (2900514)CaDiCaL version: 2.1.3
% 54.83/8.46 % (2900514)Termination reason: Instruction limit
% 54.83/8.46 % (2900514)Termination phase: Saturation
% 54.83/8.46 % (2900514)Time elapsed: 0.146 s
% 54.83/8.46 % (2900514)Peak memory usage: 91 MB
% 54.83/8.46 % (2900514)Instructions burned: 264 (million)
% 54.83/8.46 % (2900519)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3921065194:i=3256:kws=precedence:bd=preordered:av=off_2980 on theBenchmark for (2980ds/3256Mi)
% 54.83/8.46 % (2900521)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1325189265:i=537:av=off:ss=included_2980 on theBenchmark for (2980ds/537Mi)
% 54.83/8.46 % (2900521)Instruction limit reached!
% 54.83/8.46 % (2900521)------------------------------
% 54.83/8.46 % (2900521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.83/8.46 % (2900521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.83/8.46 % (2900521)CaDiCaL version: 2.1.3
% 54.83/8.46 % (2900521)Termination reason: Instruction limit
% 54.83/8.46 % (2900521)Termination phase: Saturation
% 54.83/8.46 % (2900521)Time elapsed: 0.169 s
% 54.83/8.46 % (2900521)Peak memory usage: 88 MB
% 54.83/8.46 % (2900521)Instructions burned: 539 (million)
% 54.83/8.46 % (2900493)Instruction limit reached!
% 54.83/8.46 % (2900493)------------------------------
% 54.83/8.46 % (2900493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.83/8.46 % (2900493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.83/8.46 % (2900493)CaDiCaL version: 2.1.3
% 54.83/8.46 % (2900493)Termination reason: Instruction limit
% 54.83/8.46 % (2900493)Termination phase: Saturation
% 54.83/8.46 % (2900493)Time elapsed: 1.880 s
% 54.83/8.46 % (2900493)Peak memory usage: 151 MB
% 54.83/8.46 % (2900493)Instructions burned: 3395 (million)
% 54.83/8.46 % (2900526)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2980151951:i=180:bd=preordered:av=off_2976 on theBenchmark for (2976ds/180Mi)
% 54.83/8.46 % (2900526)Instruction limit reached!
% 54.83/8.46 % (2900526)------------------------------
% 54.83/8.46 % (2900526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.83/8.46 % (2900526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.83/8.46 % (2900526)CaDiCaL version: 2.1.3
% 54.83/8.46 % (2900526)Termination reason: Instruction limit
% 54.83/8.46 % (2900526)Termination phase: Saturation
% 54.83/8.46 % (2900526)Time elapsed: 0.098 s
% 54.83/8.46 % (2900526)Peak memory usage: 90 MB
% 54.83/8.46 % (2900526)Instructions burned: 180 (million)
% 54.83/8.46 % (2900527)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1972327950:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2974 on theBenchmark for (2974ds/10307Mi)
% 54.83/8.46 % (2900529)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=2018202104:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi)
% 54.83/8.46 % (2900529)Instruction limit reached!
% 54.83/8.46 % (2900529)------------------------------
% 54.83/8.46 % (2900529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.83/8.46 % (2900529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.83/8.46 % (2900529)CaDiCaL version: 2.1.3
% 74.71/11.67 % (2900529)Termination reason: Instruction limit
% 74.71/11.67 % (2900529)Termination phase: Saturation
% 74.71/11.67 % (2900529)Time elapsed: 0.147 s
% 74.71/11.67 % (2900529)Peak memory usage: 90 MB
% 74.71/11.67 % (2900529)Instructions burned: 414 (million)
% 74.71/11.67 % (2900532)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3357782209:s2pl=no:i=8478:s2at=4:nm=6_2969 on theBenchmark for (2969ds/8478Mi)
% 74.71/11.67 % (2900502)Instruction limit reached!
% 74.71/11.67 % (2900502)------------------------------
% 74.71/11.67 % (2900502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.67 % (2900502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.67 % (2900502)CaDiCaL version: 2.1.3
% 74.71/11.67 % (2900502)Termination reason: Instruction limit
% 74.71/11.67 % (2900502)Termination phase: Saturation
% 74.71/11.67 % (2900502)Time elapsed: 2.499 s
% 74.71/11.67 % (2900502)Peak memory usage: 163 MB
% 74.71/11.67 % (2900502)Instructions burned: 5209 (million)
% 74.71/11.67 % (2900536)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=1402929980:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2964 on theBenchmark for (2964ds/303Mi)
% 74.71/11.67 % (2900536)Instruction limit reached!
% 74.71/11.67 % (2900536)------------------------------
% 74.71/11.67 % (2900536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.67 % (2900536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.67 % (2900536)CaDiCaL version: 2.1.3
% 74.71/11.67 % (2900536)Termination reason: Instruction limit
% 74.71/11.67 % (2900536)Termination phase: Saturation
% 74.71/11.67 % (2900536)Time elapsed: 0.117 s
% 74.71/11.67 % (2900536)Peak memory usage: 92 MB
% 74.71/11.67 % (2900536)Instructions burned: 306 (million)
% 74.71/11.67 % (2900519)Instruction limit reached!
% 74.71/11.67 % (2900519)------------------------------
% 74.71/11.67 % (2900519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.67 % (2900519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.67 % (2900519)CaDiCaL version: 2.1.3
% 74.71/11.67 % (2900519)Termination reason: Instruction limit
% 74.71/11.67 % (2900519)Termination phase: Saturation
% 74.71/11.67 % (2900519)Time elapsed: 1.838 s
% 74.71/11.67 % (2900519)Peak memory usage: 149 MB
% 74.71/11.67 % (2900519)Instructions burned: 3257 (million)
% 74.71/11.67 % (2900538)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2521988986:st=4:i=720:sd=3:fsr=off:ss=axioms_2961 on theBenchmark for (2961ds/720Mi)
% 74.71/11.67 % (2900539)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1447122129:i=598:bs=on:bd=preordered:av=off:ss=axioms_2960 on theBenchmark for (2960ds/598Mi)
% 74.71/11.67 % (2900539)Instruction limit reached!
% 74.71/11.67 % (2900539)------------------------------
% 74.71/11.67 % (2900539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.67 % (2900539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.67 % (2900539)CaDiCaL version: 2.1.3
% 74.71/11.67 % (2900539)Termination reason: Instruction limit
% 74.71/11.67 % (2900539)Termination phase: Saturation
% 74.71/11.67 % (2900539)Time elapsed: 0.216 s
% 74.71/11.67 % (2900539)Peak memory usage: 94 MB
% 74.71/11.67 % (2900539)Instructions burned: 598 (million)
% 74.71/11.67 % (2900538)Instruction limit reached!
% 74.71/11.67 % (2900538)------------------------------
% 74.71/11.67 % (2900538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.67 % (2900538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.67 % (2900538)CaDiCaL version: 2.1.3
% 74.71/11.67 % (2900538)Termination reason: Instruction limit
% 74.71/11.67 % (2900538)Termination phase: Saturation
% 74.71/11.67 % (2900538)Time elapsed: 0.358 s
% 74.71/11.67 % (2900538)Peak memory usage: 97 MB
% 74.71/11.67 % (2900538)Instructions burned: 720 (million)
% 74.71/11.67 % (2900546)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1920153705:i=2989:sd=3:ss=axioms:sgt=60_2956 on theBenchmark for (2956ds/2989Mi)
% 74.71/11.67 % (2900547)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=227069416:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2955 on theBenchmark for (2955ds/1997Mi)
% 74.71/11.68 % (2900547)Instruction limit reached!
% 74.71/11.68 % (2900547)------------------------------
% 74.71/11.68 % (2900547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.68 % (2900547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.68 % (2900547)CaDiCaL version: 2.1.3
% 74.71/11.68 % (2900547)Termination reason: Instruction limit
% 74.71/11.68 % (2900547)Termination phase: Saturation
% 74.71/11.68 % (2900547)Time elapsed: 1.139 s
% 74.71/11.68 % (2900547)Peak memory usage: 138 MB
% 74.71/11.68 % (2900547)Instructions burned: 1998 (million)
% 74.71/11.68 % (2900554)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=1656644562:i=2088:bd=preordered:av=off_2942 on theBenchmark for (2942ds/2088Mi)
% 74.71/11.68 % (2900546)Instruction limit reached!
% 74.71/11.68 % (2900546)------------------------------
% 74.71/11.68 % (2900546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.68 % (2900546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.68 % (2900546)CaDiCaL version: 2.1.3
% 74.71/11.68 % (2900546)Termination reason: Instruction limit
% 74.71/11.68 % (2900546)Termination phase: Saturation
% 74.71/11.68 % (2900546)Time elapsed: 1.531 s
% 74.71/11.68 % (2900546)Peak memory usage: 144 MB
% 74.71/11.68 % (2900546)Instructions burned: 2989 (million)
% 74.71/11.68 % (2900556)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3904623699:i=1098:nicw=on_2939 on theBenchmark for (2939ds/1098Mi)
% 74.71/11.68 % (2900556)Instruction limit reached!
% 74.71/11.68 % (2900556)------------------------------
% 74.71/11.68 % (2900556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.68 % (2900556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.68 % (2900556)CaDiCaL version: 2.1.3
% 74.71/11.68 % (2900556)Termination reason: Instruction limit
% 74.71/11.68 % (2900556)Termination phase: Saturation
% 74.71/11.68 % (2900556)Time elapsed: 0.512 s
% 74.71/11.68 % (2900556)Peak memory usage: 109 MB
% 74.71/11.68 % (2900556)Instructions burned: 1099 (million)
% 74.71/11.68 % (2900554)Instruction limit reached!
% 74.71/11.68 % (2900554)------------------------------
% 74.71/11.68 % (2900554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.68 % (2900554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.68 % (2900554)CaDiCaL version: 2.1.3
% 74.71/11.68 % (2900554)Termination reason: Instruction limit
% 74.71/11.68 % (2900554)Termination phase: Saturation
% 74.71/11.68 % (2900554)Time elapsed: 1.012 s
% 74.71/11.68 % (2900554)Peak memory usage: 139 MB
% 74.71/11.68 % (2900554)Instructions burned: 2088 (million)
% 74.71/11.68 % (2900558)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3953453472:i=433:bd=preordered_2931 on theBenchmark for (2931ds/433Mi)
% 74.71/11.68 % (2900558)Instruction limit reached!
% 74.71/11.68 % (2900558)------------------------------
% 74.71/11.68 % (2900558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.68 % (2900558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.68 % (2900558)CaDiCaL version: 2.1.3
% 74.71/11.68 % (2900558)Termination reason: Instruction limit
% 74.71/11.68 % (2900558)Termination phase: Saturation
% 74.71/11.68 % (2900558)Time elapsed: 0.165 s
% 74.71/11.68 % (2900558)Peak memory usage: 92 MB
% 74.71/11.68 % (2900558)Instructions burned: 433 (million)
% 74.71/11.68 % (2900560)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4137606207:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2930 on theBenchmark for (2930ds/2942Mi)
% 74.71/11.68 % (2900561)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3893235055:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2928 on theBenchmark for (2928ds/6922Mi)
% 74.71/11.68 % (2900532)Instruction limit reached!
% 74.71/11.68 % (2900532)------------------------------
% 74.71/11.68 % (2900532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.68 % (2900532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.68 % (2900532)CaDiCaL version: 2.1.3
% 74.71/11.68 % (2900532)Termination reason: Instruction limit
% 74.71/11.68 % (2900532)Termination phase: Saturation
% 74.71/11.68 % (2900532)Time elapsed: 4.666 s
% 74.71/11.68 % (2900532)Peak memory usage: 175 MB
% 74.71/11.68 % (2900532)Instructions burned: 8478 (million)
% 74.71/11.68 % (2900564)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=1013521959:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2921 on theBenchmark for (2921ds/596Mi)
% 74.71/11.68 % (2900564)Instruction limit reached!
% 74.71/11.68 % (2900564)------------------------------
% 74.71/11.68 % (2900564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.68 % (2900564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.68 % (2900564)CaDiCaL version: 2.1.3
% 74.71/11.68 % (2900564)Termination reason: Instruction limit
% 74.71/11.68 % (2900564)Termination phase: Saturation
% 74.71/11.68 % (2900564)Time elapsed: 0.270 s
% 74.71/11.68 % (2900564)Peak memory usage: 96 MB
% 74.71/11.68 % (2900564)Instructions burned: 596 (million)
% 74.71/11.68 % (2900527)Instruction limit reached!
% 74.71/11.68 % (2900527)------------------------------
% 74.71/11.68 % (2900527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.68 % (2900527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.68 % (2900527)CaDiCaL version: 2.1.3
% 74.71/11.68 % (2900527)Termination reason: Instruction limit
% 74.71/11.68 % (2900527)Termination phase: Saturation
% 74.71/11.68 % (2900527)Time elapsed: 5.692 s
% 74.71/11.68 % (2900527)Peak memory usage: 180 MB
% 74.71/11.68 % (2900527)Instructions burned: 10308 (million)
% 74.71/11.68 % (2900566)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=3836189618:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2916 on theBenchmark for (2916ds/4123Mi)
% 74.71/11.68 % (2900567)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=454376922:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2915 on theBenchmark for (2915ds/16411Mi)
% 74.71/11.68 % (2900560)Instruction limit reached!
% 74.71/11.68 % (2900560)------------------------------
% 74.71/11.68 % (2900560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.68 % (2900560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.68 % (2900560)CaDiCaL version: 2.1.3
% 74.71/11.68 % (2900560)Termination reason: Instruction limit
% 74.71/11.68 % (2900560)Termination phase: Saturation
% 74.71/11.68 % (2900560)Time elapsed: 1.423 s
% 74.71/11.68 % (2900560)Peak memory usage: 143 MB
% 74.71/11.68 % (2900560)Instructions burned: 2942 (million)
% 74.71/11.68 % (2900570)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=650086504:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2913 on theBenchmark for (2913ds/1670Mi)
% 74.71/11.68 % (2900570)Instruction limit reached!
% 74.71/11.68 % (2900570)------------------------------
% 74.71/11.68 % (2900570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.68 % (2900570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.68 % (2900570)CaDiCaL version: 2.1.3
% 74.71/11.68 % (2900570)Termination reason: Instruction limit
% 74.71/11.68 % (2900570)Termination phase: Saturation
% 74.71/11.68 % (2900570)Time elapsed: 0.907 s
% 74.71/11.68 % (2900570)Peak memory usage: 136 MB
% 74.71/11.68 % (2900570)Instructions burned: 1670 (million)
% 74.71/11.68 % (2900578)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=611467810:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2902 on theBenchmark for (2902ds/1722Mi)
% 74.71/11.68 % (2900578)First to succeed.
% 74.71/11.68 % (2900578)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2900460"
% 74.71/11.68 % (2900566)Instruction limit reached!
% 74.71/11.68 % (2900566)------------------------------
% 74.71/11.68 % (2900566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.71/11.68 % (2900566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.71/11.68 % (2900566)CaDiCaL version: 2.1.3
% 74.71/11.68 % (2900566)Termination reason: Instruction limit
% 74.71/11.68 % (2900566)Termination phase: Saturation
% 74.71/11.68 % (2900566)Time elapsed: 2.362 s
% 74.71/11.68 % (2900566)Peak memory usage: 161 MB
% 74.71/11.68 % (2900566)Instructions burned: 4124 (million)
% 74.71/11.68 % (2900578)Refutation found. Thanks to Tanya!
% 74.71/11.68 % SZS status Unsatisfiable for theBenchmark
% 74.71/11.68 % SZS output start Proof for theBenchmark
% See solution above
% 0.10/11.81 % (2900578)------------------------------
% 0.10/11.81 % (2900578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.10/11.81 % (2900578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.10/11.81 % (2900578)CaDiCaL version: 2.1.3
% 0.10/11.81 % (2900578)Termination reason: Refutation
% 0.10/11.81 % (2900578)Time elapsed: 0.743 s
% 0.10/11.81 % (2900578)Peak memory usage: 132 MB
% 0.10/11.81 % (2900578)Instructions burned: 1217 (million)
% 0.10/11.81 % (2900578)------------------------------
% 0.10/11.81 % (2900578)------------------------------
% 0.10/11.81 % (2900460)Success in time 11.053 s
% 0.10/11.81 % Vampire exiting
%------------------------------------------------------------------------------