%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET035-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 : n010.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:43 PM UTC 2026
% Result : Unsatisfiable 34.95s 10.61s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 19
% Syntax : Number of formulae : 61 ( 13 unt; 0 def)
% Number of atoms : 177 ( 43 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 231 ( 115 ~; 116 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-2 aty)
% Number of variables : 175 ( 175 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( little_set(X0)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2) ).
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(f7,axiom,
! [X2,X0,X1] :
( member(X0,non_ordered_pair(X1,X2))
| ~ little_set(X0)
| X0 != X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',non_ordered_pair3) ).
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] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subset(X0,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(f170,axiom,
! [X0] :
( ~ ordered_pair_predicate(X0)
| little_set(second(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',second_component_is_small) ).
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(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(f183,axiom,
maps(function2,c,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',another_mapping) ).
fof(f184,negated_conjecture,
~ maps(compose(function2,function1),a,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_maps_for_composition) ).
fof(f188,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(f189,plain,
! [X2,X1] :
( member(X2,non_ordered_pair(X1,X2))
| ~ little_set(X2) ),
inference(equality_resolution,[],[f7]) ).
fof(f195,plain,
! [X2,X1] :
( ~ ordered_pair_predicate(X2)
| ~ little_set(second(X2))
| member(second(X2),range_of(X1))
| ~ member(X2,X1) ),
inference(equality_resolution,[],[f124]) ).
fof(f209,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,[],[f120,f5]) ).
fof(f239,plain,
! [X2,X0,X1] :
( ordered_pair_predicate(X0)
| ~ member(X0,compose(X1,X2)) ),
inference(resolution,[],[f88,f178]) ).
fof(f242,plain,
! [X2,X3,X0,X1] :
( ~ member(X0,compose(X1,X2))
| ~ little_set(second(X0))
| member(second(X0),range_of(X3))
| ~ member(X0,X3) ),
inference(resolution,[],[f239,f195]) ).
fof(f243,plain,
! [X2,X0,X1] :
( little_set(second(X0))
| ~ member(X0,compose(X1,X2)) ),
inference(resolution,[],[f239,f170]) ).
fof(f245,plain,
! [X2,X3,X0,X1] :
( member(second(X0),range_of(X3))
| ~ member(X0,compose(X1,X2))
| ~ member(X0,X3) ),
inference(forward_subsumption_resolution,[],[f242,f243]) ).
fof(f263,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,[],[f209]) ).
fof(f266,plain,
! [X0,X1] :
( f27(X0,non_ordered_pair(X1,X1)) = X1
| ~ member(X0,range_of(non_ordered_pair(X1,X1))) ),
inference(equality_resolution,[],[f263]) ).
fof(f267,plain,
! [X0,X1] :
( f27(X0,singleton_set(X1)) = X1
| ~ member(X0,range_of(non_ordered_pair(X1,X1))) ),
inference(forward_demodulation,[],[f266,f9]) ).
fof(f268,plain,
! [X0,X1] :
( f27(X0,singleton_set(X1)) = X1
| ~ member(X0,range_of(singleton_set(X1))) ),
inference(forward_demodulation,[],[f267,f9]) ).
fof(f269,plain,
! [X0,X1] :
( second(X0) = X1
| ~ member(X1,range_of(singleton_set(X0)))
| ~ member(X1,range_of(singleton_set(X0))) ),
inference(superposition,[],[f122,f268]) ).
fof(f272,plain,
! [X0,X1] :
( ~ member(X1,range_of(singleton_set(X0)))
| second(X0) = X1 ),
inference(duplicate_literal_removal,[],[f269]) ).
fof(f273,plain,
! [X2,X0,X1] :
( ~ subset(X2,range_of(singleton_set(X0)))
| ~ member(X1,X2)
| second(X0) = X1 ),
inference(resolution,[],[f272,f79]) ).
fof(f311,plain,
! [X2,X0,X1] :
( ~ member(X0,range_of(compose(singleton_set(X1),X2)))
| second(X1) = X0 ),
inference(resolution,[],[f273,f179]) ).
fof(f315,plain,
! [X2,X3,X0,X1,X4] :
( second(X1) = second(X0)
| ~ member(X1,compose(X2,X3))
| ~ member(X1,compose(singleton_set(X0),X4)) ),
inference(resolution,[],[f311,f245]) ).
fof(f319,plain,
! [X0,X1,X4] :
( ~ member(X1,compose(singleton_set(X0),X4))
| second(X1) = second(X0) ),
inference(condensation,[],[f315]) ).
fof(f321,plain,
! [X2,X3,X0,X1,X4] :
( second(X2) = second(ordered_pair(X0,X1))
| ~ little_set(ordered_pair(X0,X1))
| ~ little_set(X0)
| ~ little_set(X1)
| ~ little_set(X3)
| ~ member(ordered_pair(X0,X3),singleton_set(X2))
| ~ member(ordered_pair(X3,X1),X4) ),
inference(resolution,[],[f319,f188]) ).
fof(f325,plain,
! [X2,X3,X0,X1,X4] :
( second(X2) = second(ordered_pair(X0,X1))
| ~ little_set(X0)
| ~ little_set(X1)
| ~ little_set(X3)
| ~ member(ordered_pair(X0,X3),singleton_set(X2))
| ~ member(ordered_pair(X3,X1),X4) ),
inference(forward_subsumption_resolution,[],[f321,f172]) ).
fof(f326,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(ordered_pair(X0,X3),singleton_set(X2))
| ~ little_set(X0)
| ~ little_set(X1)
| ~ little_set(X3)
| second(X2) = X1
| ~ member(ordered_pair(X3,X1),X4) ),
inference(forward_subsumption_demodulation,[],[f325,f168]) ).
fof(f327,plain,
! [X2,X3,X0,X1] :
( ~ little_set(X0)
| ~ little_set(X1)
| ~ little_set(X2)
| second(ordered_pair(X0,X2)) = X1
| ~ member(ordered_pair(X2,X1),X3)
| ~ little_set(ordered_pair(X0,X2)) ),
inference(resolution,[],[f326,f171]) ).
fof(f329,plain,
! [X2,X3,X0,X1] :
( ~ little_set(X0)
| ~ little_set(X1)
| ~ little_set(X2)
| second(ordered_pair(X0,X2)) = X1
| ~ member(ordered_pair(X2,X1),X3) ),
inference(forward_subsumption_resolution,[],[f327,f172]) ).
fof(f330,plain,
! [X2,X3,X0,X1] :
( ~ little_set(X0)
| ~ little_set(X1)
| ~ little_set(X2)
| X1 = X2
| ~ member(ordered_pair(X2,X1),X3) ),
inference(forward_subsumption_demodulation,[],[f329,f168]) ).
fof(f331,plain,
! [X2,X3,X1] :
( ~ little_set(X1)
| ~ little_set(X2)
| X1 = X2
| ~ member(ordered_pair(X2,X1),X3) ),
inference(condensation,[],[f330]) ).
fof(f332,plain,
! [X2,X3,X0,X1] :
( ~ little_set(X0)
| X0 = X1
| ~ member(ordered_pair(X0,X1),X2)
| ~ member(X1,X3) ),
inference(resolution,[],[f331,f1]) ).
fof(f338,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(ordered_pair(non_ordered_pair(X0,X1),X2),X3)
| non_ordered_pair(X0,X1) = X2
| ~ member(X2,X4) ),
inference(resolution,[],[f332,f8]) ).
fof(f363,plain,
! [X2,X3,X0,X1] :
( non_ordered_pair(X0,X1) = X2
| ~ member(X2,X3)
| ~ little_set(ordered_pair(non_ordered_pair(X0,X1),X2)) ),
inference(resolution,[],[f338,f171]) ).
fof(f366,plain,
! [X2,X3,X0,X1] :
( ~ member(X2,X3)
| non_ordered_pair(X0,X1) = X2 ),
inference(forward_subsumption_resolution,[],[f363,f172]) ).
fof(f373,plain,
! [X2,X0,X1] :
( ~ little_set(X2)
| non_ordered_pair(X0,X1) = X2 ),
inference(resolution,[],[f366,f171]) ).
fof(f415,plain,
! [X2,X3,X0,X1] : non_ordered_pair(X0,X1) = non_ordered_pair(X2,X3),
inference(resolution,[],[f373,f8]) ).
fof(f430,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(X2,non_ordered_pair(X0,X1))
| X2 = X3
| X2 = X4 ),
inference(superposition,[],[f5,f415]) ).
fof(f439,plain,
! [X2,X0,X1,X4] :
( ~ member(X2,non_ordered_pair(X0,X1))
| X2 = X4 ),
inference(condensation,[],[f430]) ).
fof(f444,plain,
! [X0,X1] :
( ~ little_set(X0)
| X0 = X1 ),
inference(resolution,[],[f439,f189]) ).
fof(f452,plain,
! [X2,X0,X1] : non_ordered_pair(X0,X1) = X2,
inference(resolution,[],[f444,f8]) ).
fof(f456,plain,
! [X3,X0] : X0 = X3,
inference(superposition,[],[f452,f452]) ).
fof(f763,plain,
! [X0] : ~ maps(X0,a,d),
inference(superposition,[],[f184,f456]) ).
fof(f793,plain,
! [X0] : maps(function2,X0,d),
inference(superposition,[],[f183,f456]) ).
fof(f875,plain,
$false,
inference(resolution,[],[f793,f763]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET035-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n010.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Mon Sep 28 00:17:47 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/0.43 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
% 11.02/2.43 % (1451912)Input is clausal, will run a generic CNF schedule.
% 11.02/2.43 % (1451923)dis-21_1_sil=8000:lcm=predicate:random_seed=1945001190: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)
% 11.02/2.43 % (1451922)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3686082485:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.02/2.43 % (1451921)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=174733787:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.02/2.43 % (1451920)lrs+10_1_sil=8000:sp=occurrence:random_seed=2300406589:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.02/2.43 % (1451918)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1839690965:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.02/2.43 % (1451917)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=937224766:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.02/2.43 % (1451919)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=257051951:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.02/2.43 % (1451920)Refutation not found, incomplete strategy
% 11.02/2.43 % (1451920)------------------------------
% 11.02/2.43 % (1451920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.02/2.43 % (1451920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.02/2.43 % (1451920)CaDiCaL version: 2.1.3
% 11.02/2.43 % (1451920)Termination reason: Refutation not found, incomplete strategy
% 11.02/2.43 % (1451920)Time elapsed: 0.001 s
% 11.02/2.43 % (1451920)Peak memory usage: 88 MB
% 11.02/2.43 % (1451920)Instructions burned: 1 (million)
% 11.02/2.43 % (1451923)Instruction limit reached!
% 11.02/2.43 % (1451923)------------------------------
% 11.02/2.43 % (1451923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.02/2.43 % (1451923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.02/2.43 % (1451923)CaDiCaL version: 2.1.3
% 11.02/2.43 % (1451923)Termination reason: Instruction limit
% 11.02/2.43 % (1451923)Termination phase: Saturation
% 11.02/2.43 % (1451923)Time elapsed: 0.075 s
% 11.02/2.43 % (1451923)Peak memory usage: 89 MB
% 11.02/2.43 % (1451923)Instructions burned: 118 (million)
% 11.02/2.43 % (1451921)Instruction limit reached!
% 11.02/2.43 % (1451921)------------------------------
% 11.02/2.43 % (1451921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.02/2.43 % (1451921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.02/2.43 % (1451921)CaDiCaL version: 2.1.3
% 11.02/2.43 % (1451921)Termination reason: Instruction limit
% 11.02/2.43 % (1451921)Termination phase: Saturation
% 11.02/2.43 % (1451921)Time elapsed: 0.059 s
% 11.02/2.43 % (1451921)Peak memory usage: 88 MB
% 11.02/2.43 % (1451921)Instructions burned: 114 (million)
% 11.02/2.43 % (1451922)Instruction limit reached!
% 11.02/2.43 % (1451922)------------------------------
% 11.02/2.43 % (1451922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.02/2.43 % (1451922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.02/2.43 % (1451922)CaDiCaL version: 2.1.3
% 11.02/2.43 % (1451922)Termination reason: Instruction limit
% 11.02/2.43 % (1451922)Termination phase: Saturation
% 11.02/2.43 % (1451922)Time elapsed: 0.069 s
% 11.02/2.43 % (1451922)Peak memory usage: 90 MB
% 11.02/2.43 % (1451922)Instructions burned: 184 (million)
% 11.02/2.43 % (1451933)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=449704402:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.02/2.43 % (1451931)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=1569755608:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.02/2.43 % (1451932)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=836257415: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)
% 11.02/2.43 % (1451920)------------------------------
% 11.02/2.43 % (1451920)------------------------------
% 11.02/2.43 % (1451933)Instruction limit reached!
% 11.02/2.43 % (1451933)------------------------------
% 18.78/3.58 % (1451933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.78/3.58 % (1451933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.78/3.58 % (1451933)CaDiCaL version: 2.1.3
% 18.78/3.58 % (1451933)Termination reason: Instruction limit
% 18.78/3.58 % (1451933)Termination phase: Saturation
% 18.78/3.58 % (1451933)Time elapsed: 0.080 s
% 18.78/3.58 % (1451933)Peak memory usage: 90 MB
% 18.78/3.58 % (1451933)Instructions burned: 220 (million)
% 18.78/3.58 % (1451931)Instruction limit reached!
% 18.78/3.58 % (1451931)------------------------------
% 18.78/3.58 % (1451931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.78/3.58 % (1451931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.78/3.58 % (1451931)CaDiCaL version: 2.1.3
% 18.78/3.58 % (1451931)Termination reason: Instruction limit
% 18.78/3.58 % (1451931)Termination phase: Saturation
% 18.78/3.58 % (1451931)Time elapsed: 0.097 s
% 18.78/3.58 % (1451931)Peak memory usage: 89 MB
% 18.78/3.58 % (1451931)Instructions burned: 144 (million)
% 18.78/3.58 % (1451932)Instruction limit reached!
% 18.78/3.58 % (1451932)------------------------------
% 18.78/3.58 % (1451932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.78/3.58 % (1451932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.78/3.58 % (1451932)CaDiCaL version: 2.1.3
% 18.78/3.58 % (1451932)Termination reason: Instruction limit
% 18.78/3.58 % (1451932)Termination phase: Saturation
% 18.78/3.58 % (1451932)Time elapsed: 0.102 s
% 18.78/3.58 % (1451932)Peak memory usage: 91 MB
% 18.78/3.58 % (1451932)Instructions burned: 190 (million)
% 18.78/3.58 % (1451938)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=837585080:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 18.78/3.58 % (1451937)lrs+10_64_to=lpo:sil=8000:random_seed=325690368:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 18.78/3.58 % (1451939)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2891841653:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 18.78/3.58 % (1451938)Instruction limit reached!
% 18.78/3.58 % (1451938)------------------------------
% 18.78/3.58 % (1451938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.78/3.58 % (1451938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.78/3.58 % (1451938)CaDiCaL version: 2.1.3
% 18.78/3.58 % (1451938)Termination reason: Instruction limit
% 18.78/3.58 % (1451938)Termination phase: Saturation
% 18.78/3.58 % (1451938)Time elapsed: 0.073 s
% 18.78/3.58 % (1451938)Peak memory usage: 90 MB
% 18.78/3.58 % (1451938)Instructions burned: 195 (million)
% 18.78/3.58 % (1451937)Instruction limit reached!
% 18.78/3.58 % (1451937)------------------------------
% 18.78/3.58 % (1451937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.78/3.58 % (1451937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.78/3.58 % (1451937)CaDiCaL version: 2.1.3
% 18.78/3.58 % (1451937)Termination reason: Instruction limit
% 18.78/3.58 % (1451937)Termination phase: Saturation
% 18.78/3.58 % (1451937)Time elapsed: 0.076 s
% 18.78/3.58 % (1451937)Peak memory usage: 90 MB
% 18.78/3.58 % (1451937)Instructions burned: 127 (million)
% 18.78/3.58 % (1451940)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1816763445:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 18.78/3.58 % (1451939)Instruction limit reached!
% 18.78/3.58 % (1451939)------------------------------
% 18.78/3.58 % (1451939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.78/3.58 % (1451939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.78/3.58 % (1451939)CaDiCaL version: 2.1.3
% 18.78/3.58 % (1451939)Termination reason: Instruction limit
% 18.78/3.58 % (1451939)Termination phase: Saturation
% 18.78/3.58 % (1451939)Time elapsed: 0.104 s
% 18.78/3.58 % (1451939)Peak memory usage: 91 MB
% 18.78/3.58 % (1451939)Instructions burned: 157 (million)
% 18.78/3.58 % (1451944)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=6046812:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 18.78/3.58 % (1451944)Instruction limit reached!
% 18.78/3.58 % (1451944)------------------------------
% 18.78/3.58 % (1451944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.78/3.58 % (1451944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.62/4.98 % (1451944)CaDiCaL version: 2.1.3
% 28.62/4.98 % (1451944)Termination reason: Instruction limit
% 28.62/4.98 % (1451944)Termination phase: Saturation
% 28.62/4.98 % (1451944)Time elapsed: 0.030 s
% 28.62/4.98 % (1451944)Peak memory usage: 89 MB
% 28.62/4.98 % (1451944)Instructions burned: 110 (million)
% 28.62/4.98 % (1451946)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3874766807:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 28.62/4.98 % (1451947)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3147491146:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 28.62/4.98 % (1451946)Instruction limit reached!
% 28.62/4.98 % (1451946)------------------------------
% 28.62/4.98 % (1451946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.62/4.98 % (1451946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.62/4.98 % (1451946)CaDiCaL version: 2.1.3
% 28.62/4.98 % (1451946)Termination reason: Instruction limit
% 28.62/4.98 % (1451946)Termination phase: Saturation
% 28.62/4.98 % (1451946)Time elapsed: 0.071 s
% 28.62/4.98 % (1451946)Peak memory usage: 90 MB
% 28.62/4.98 % (1451946)Instructions burned: 108 (million)
% 28.62/4.98 % (1451949)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2741997040:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 28.62/4.98 % (1451947)Instruction limit reached!
% 28.62/4.98 % (1451947)------------------------------
% 28.62/4.98 % (1451947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.62/4.98 % (1451947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.62/4.98 % (1451947)CaDiCaL version: 2.1.3
% 28.62/4.98 % (1451947)Termination reason: Instruction limit
% 28.62/4.98 % (1451947)Termination phase: Saturation
% 28.62/4.98 % (1451947)Time elapsed: 0.167 s
% 28.62/4.98 % (1451947)Peak memory usage: 90 MB
% 28.62/4.98 % (1451947)Instructions burned: 242 (million)
% 28.62/4.98 % (1451953)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3698509895:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 28.62/4.98 % (1451953)Instruction limit reached!
% 28.62/4.98 % (1451953)------------------------------
% 28.62/4.98 % (1451953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.62/4.98 % (1451953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.62/4.98 % (1451953)CaDiCaL version: 2.1.3
% 28.62/4.98 % (1451953)Termination reason: Instruction limit
% 28.62/4.98 % (1451953)Termination phase: Saturation
% 28.62/4.98 % (1451953)Time elapsed: 0.098 s
% 28.62/4.98 % (1451953)Peak memory usage: 89 MB
% 28.62/4.98 % (1451953)Instructions burned: 135 (million)
% 28.62/4.98 % (1451954)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3954668127:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 28.62/4.98 % (1451956)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1350183415:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 28.62/4.98 % (1451956)Instruction limit reached!
% 28.62/4.98 % (1451956)------------------------------
% 28.62/4.98 % (1451956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.62/4.98 % (1451956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.62/4.98 % (1451956)CaDiCaL version: 2.1.3
% 28.62/4.98 % (1451956)Termination reason: Instruction limit
% 28.62/4.98 % (1451956)Termination phase: Saturation
% 28.62/4.98 % (1451956)Time elapsed: 0.111 s
% 28.62/4.98 % (1451956)Peak memory usage: 93 MB
% 28.62/4.98 % (1451956)Instructions burned: 192 (million)
% 28.62/4.98 % (1451954)Instruction limit reached!
% 28.62/4.98 % (1451954)------------------------------
% 28.62/4.98 % (1451954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.62/4.98 % (1451954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.62/4.98 % (1451954)CaDiCaL version: 2.1.3
% 28.62/4.98 % (1451954)Termination reason: Instruction limit
% 28.62/4.98 % (1451954)Termination phase: Saturation
% 28.62/4.98 % (1451954)Time elapsed: 0.272 s
% 28.62/4.98 % (1451954)Peak memory usage: 95 MB
% 28.62/4.98 % (1451954)Instructions burned: 501 (million)
% 28.62/4.98 % (1451959)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1766534847:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 48.34/7.75 % (1451960)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1637512295:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 48.34/7.75 % (1451959)Instruction limit reached!
% 48.34/7.75 % (1451959)------------------------------
% 48.34/7.75 % (1451959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.34/7.75 % (1451959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.34/7.75 % (1451959)CaDiCaL version: 2.1.3
% 48.34/7.75 % (1451959)Termination reason: Instruction limit
% 48.34/7.75 % (1451959)Termination phase: Saturation
% 48.34/7.75 % (1451959)Time elapsed: 0.161 s
% 48.34/7.75 % (1451959)Peak memory usage: 92 MB
% 48.34/7.75 % (1451959)Instructions burned: 264 (million)
% 48.34/7.75 % (1451960)Instruction limit reached!
% 48.34/7.75 % (1451960)------------------------------
% 48.34/7.75 % (1451960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.34/7.75 % (1451960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.34/7.75 % (1451960)CaDiCaL version: 2.1.3
% 48.34/7.75 % (1451960)Termination reason: Instruction limit
% 48.34/7.75 % (1451960)Termination phase: Saturation
% 48.34/7.75 % (1451960)Time elapsed: 0.106 s
% 48.34/7.75 % (1451960)Peak memory usage: 90 MB
% 48.34/7.75 % (1451960)Instructions burned: 156 (million)
% 48.34/7.75 % (1451963)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=1652327224:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi)
% 48.34/7.75 % (1451964)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1280693471:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 48.34/7.75 % (1451964)Instruction limit reached!
% 48.34/7.75 % (1451964)------------------------------
% 48.34/7.75 % (1451964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.34/7.75 % (1451964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.34/7.75 % (1451964)CaDiCaL version: 2.1.3
% 48.34/7.75 % (1451964)Termination reason: Instruction limit
% 48.34/7.75 % (1451964)Termination phase: Saturation
% 48.34/7.75 % (1451964)Time elapsed: 0.310 s
% 48.34/7.75 % (1451964)Peak memory usage: 91 MB
% 48.34/7.75 % (1451964)Instructions burned: 539 (million)
% 48.34/7.75 % (1451967)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3150222280:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi)
% 48.34/7.75 % (1451967)Instruction limit reached!
% 48.34/7.75 % (1451967)------------------------------
% 48.34/7.75 % (1451967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.34/7.75 % (1451967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.34/7.75 % (1451967)CaDiCaL version: 2.1.3
% 48.34/7.75 % (1451967)Termination reason: Instruction limit
% 48.34/7.75 % (1451967)Termination phase: Saturation
% 48.34/7.75 % (1451967)Time elapsed: 0.101 s
% 48.34/7.75 % (1451967)Peak memory usage: 91 MB
% 48.34/7.75 % (1451967)Instructions burned: 181 (million)
% 48.34/7.75 % (1451949)Instruction limit reached!
% 48.34/7.75 % (1451949)------------------------------
% 48.34/7.75 % (1451949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.34/7.75 % (1451949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.34/7.75 % (1451949)CaDiCaL version: 2.1.3
% 48.34/7.75 % (1451949)Termination reason: Instruction limit
% 48.34/7.75 % (1451949)Termination phase: Saturation
% 48.34/7.75 % (1451949)Time elapsed: 1.680 s
% 48.34/7.75 % (1451949)Peak memory usage: 160 MB
% 48.34/7.75 % (1451949)Instructions burned: 5211 (million)
% 48.34/7.75 % (1451969)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=1504763159:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi)
% 48.34/7.75 % (1451970)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=317667793:i=412:gtgl=4:gtg=exists_all_2974 on theBenchmark for (2974ds/412Mi)
% 48.34/7.75 % (1451940)Instruction limit reached!
% 48.34/7.75 % (1451940)------------------------------
% 48.34/7.75 % (1451940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.34/7.75 % (1451940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.34/7.75 % (1451940)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451940)Termination reason: Instruction limit
% 34.95/10.61 % (1451940)Termination phase: Saturation
% 34.95/10.61 % (1451940)Time elapsed: 2.048 s
% 34.95/10.61 % (1451940)Peak memory usage: 149 MB
% 34.95/10.61 % (1451940)Instructions burned: 3395 (million)
% 34.95/10.61 % (1451970)Instruction limit reached!
% 34.95/10.61 % (1451970)------------------------------
% 34.95/10.61 % (1451970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451970)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451970)Termination reason: Instruction limit
% 34.95/10.61 % (1451970)Termination phase: Saturation
% 34.95/10.61 % (1451970)Time elapsed: 0.107 s
% 34.95/10.61 % (1451970)Peak memory usage: 90 MB
% 34.95/10.61 % (1451970)Instructions burned: 415 (million)
% 34.95/10.61 % (1451973)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=2761319603:s2pl=no:i=8478:s2at=4:nm=6_2972 on theBenchmark for (2972ds/8478Mi)
% 34.95/10.61 % (1451974)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=970831592:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2972 on theBenchmark for (2972ds/303Mi)
% 34.95/10.61 % (1451974)Instruction limit reached!
% 34.95/10.61 % (1451974)------------------------------
% 34.95/10.61 % (1451974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451974)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451974)Termination reason: Instruction limit
% 34.95/10.61 % (1451974)Termination phase: Saturation
% 34.95/10.61 % (1451974)Time elapsed: 0.091 s
% 34.95/10.61 % (1451974)Peak memory usage: 93 MB
% 34.95/10.61 % (1451974)Instructions burned: 306 (million)
% 34.95/10.61 % (1451977)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1332994503:st=4:i=720:sd=3:fsr=off:ss=axioms_2969 on theBenchmark for (2969ds/720Mi)
% 34.95/10.61 % (1451977)Instruction limit reached!
% 34.95/10.61 % (1451977)------------------------------
% 34.95/10.61 % (1451977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451977)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451977)Termination reason: Instruction limit
% 34.95/10.61 % (1451977)Termination phase: Saturation
% 34.95/10.61 % (1451977)Time elapsed: 0.199 s
% 34.95/10.61 % (1451977)Peak memory usage: 97 MB
% 34.95/10.61 % (1451977)Instructions burned: 723 (million)
% 34.95/10.61 % (1451979)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=4013759547:i=598:bs=on:bd=preordered:av=off:ss=axioms_2966 on theBenchmark for (2966ds/598Mi)
% 34.95/10.61 % (1451979)Instruction limit reached!
% 34.95/10.61 % (1451979)------------------------------
% 34.95/10.61 % (1451979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451979)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451979)Termination reason: Instruction limit
% 34.95/10.61 % (1451979)Termination phase: Saturation
% 34.95/10.61 % (1451979)Time elapsed: 0.305 s
% 34.95/10.61 % (1451979)Peak memory usage: 96 MB
% 34.95/10.61 % (1451979)Instructions burned: 599 (million)
% 34.95/10.61 % (1451963)Instruction limit reached!
% 34.95/10.61 % (1451963)------------------------------
% 34.95/10.61 % (1451963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451963)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451963)Termination reason: Instruction limit
% 34.95/10.61 % (1451963)Termination phase: Saturation
% 34.95/10.61 % (1451963)Time elapsed: 2.069 s
% 34.95/10.61 % (1451963)Peak memory usage: 144 MB
% 34.95/10.61 % (1451963)Instructions burned: 3257 (million)
% 34.95/10.61 % (1451982)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3016282007:i=2989:sd=3:ss=axioms:sgt=60_2961 on theBenchmark for (2961ds/2989Mi)
% 34.95/10.61 % (1451983)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=192586890:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2960 on theBenchmark for (2960ds/1997Mi)
% 34.95/10.61 % (1451983)Instruction limit reached!
% 34.95/10.61 % (1451983)------------------------------
% 34.95/10.61 % (1451983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451983)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451983)Termination reason: Instruction limit
% 34.95/10.61 % (1451983)Termination phase: Saturation
% 34.95/10.61 % (1451983)Time elapsed: 1.276 s
% 34.95/10.61 % (1451983)Peak memory usage: 138 MB
% 34.95/10.61 % (1451983)Instructions burned: 1997 (million)
% 34.95/10.61 % (1451986)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=1018802688:i=2088:bd=preordered:av=off_2946 on theBenchmark for (2946ds/2088Mi)
% 34.95/10.61 % (1451982)Instruction limit reached!
% 34.95/10.61 % (1451982)------------------------------
% 34.95/10.61 % (1451982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451982)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451982)Termination reason: Instruction limit
% 34.95/10.61 % (1451982)Termination phase: Saturation
% 34.95/10.61 % (1451982)Time elapsed: 1.833 s
% 34.95/10.61 % (1451982)Peak memory usage: 143 MB
% 34.95/10.61 % (1451982)Instructions burned: 2990 (million)
% 34.95/10.61 % (1451988)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3318243535:i=1098:nicw=on_2941 on theBenchmark for (2941ds/1098Mi)
% 34.95/10.61 % (1451973)Instruction limit reached!
% 34.95/10.61 % (1451973)------------------------------
% 34.95/10.61 % (1451973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451973)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451973)Termination reason: Instruction limit
% 34.95/10.61 % (1451973)Termination phase: Saturation
% 34.95/10.61 % (1451973)Time elapsed: 3.546 s
% 34.95/10.61 % (1451973)Peak memory usage: 170 MB
% 34.95/10.61 % (1451973)Instructions burned: 8479 (million)
% 34.95/10.61 % (1451988)Instruction limit reached!
% 34.95/10.61 % (1451988)------------------------------
% 34.95/10.61 % (1451988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451988)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451988)Termination reason: Instruction limit
% 34.95/10.61 % (1451988)Termination phase: Saturation
% 34.95/10.61 % (1451988)Time elapsed: 0.544 s
% 34.95/10.61 % (1451988)Peak memory usage: 110 MB
% 34.95/10.61 % (1451988)Instructions burned: 1100 (million)
% 34.95/10.61 % (1451990)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=590975463:i=433:bd=preordered_2935 on theBenchmark for (2935ds/433Mi)
% 34.95/10.61 % (1451990)Instruction limit reached!
% 34.95/10.61 % (1451990)------------------------------
% 34.95/10.61 % (1451990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451990)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451990)Termination reason: Instruction limit
% 34.95/10.61 % (1451990)Termination phase: Saturation
% 34.95/10.61 % (1451990)Time elapsed: 0.149 s
% 34.95/10.61 % (1451990)Peak memory usage: 92 MB
% 34.95/10.61 % (1451990)Instructions burned: 434 (million)
% 34.95/10.61 % (1451992)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2511161409:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2934 on theBenchmark for (2934ds/2942Mi)
% 34.95/10.61 % (1451993)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=634397172:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2933 on theBenchmark for (2933ds/6922Mi)
% 34.95/10.61 % (1451986)Instruction limit reached!
% 34.95/10.61 % (1451986)------------------------------
% 34.95/10.61 % (1451986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451986)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451986)Termination reason: Instruction limit
% 34.95/10.61 % (1451986)Termination phase: Saturation
% 34.95/10.61 % (1451986)Time elapsed: 1.324 s
% 34.95/10.61 % (1451986)Peak memory usage: 137 MB
% 34.95/10.61 % (1451986)Instructions burned: 2089 (million)
% 34.95/10.61 % (1451996)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=2772586834:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2931 on theBenchmark for (2931ds/596Mi)
% 34.95/10.61 % (1451996)Instruction limit reached!
% 34.95/10.61 % (1451996)------------------------------
% 34.95/10.61 % (1451996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451996)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451996)Termination reason: Instruction limit
% 34.95/10.61 % (1451996)Termination phase: Saturation
% 34.95/10.61 % (1451996)Time elapsed: 0.282 s
% 34.95/10.61 % (1451996)Peak memory usage: 96 MB
% 34.95/10.61 % (1451996)Instructions burned: 597 (million)
% 34.95/10.61 % (1451998)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=130682440:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2926 on theBenchmark for (2926ds/4123Mi)
% 34.95/10.61 % (1451969)Instruction limit reached!
% 34.95/10.61 % (1451969)------------------------------
% 34.95/10.61 % (1451969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451969)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451969)Termination reason: Instruction limit
% 34.95/10.61 % (1451969)Termination phase: Saturation
% 34.95/10.61 % (1451969)Time elapsed: 5.767 s
% 34.95/10.61 % (1451969)Peak memory usage: 181 MB
% 34.95/10.61 % (1451969)Instructions burned: 10307 (million)
% 34.95/10.61 % (1451992)Instruction limit reached!
% 34.95/10.61 % (1451992)------------------------------
% 34.95/10.61 % (1451992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451992)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451992)Termination reason: Instruction limit
% 34.95/10.61 % (1451992)Termination phase: Saturation
% 34.95/10.61 % (1451992)Time elapsed: 1.838 s
% 34.95/10.61 % (1451992)Peak memory usage: 143 MB
% 34.95/10.61 % (1451992)Instructions burned: 2943 (million)
% 34.95/10.61 % (1452000)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1748263252:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2915 on theBenchmark for (2915ds/16411Mi)
% 34.95/10.61 % (1452001)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=4091131991:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2914 on theBenchmark for (2914ds/1670Mi)
% 34.95/10.61 % (1451993)Instruction limit reached!
% 34.95/10.61 % (1451993)------------------------------
% 34.95/10.61 % (1451993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.95/10.61 % (1451993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.95/10.61 % (1451993)CaDiCaL version: 2.1.3
% 34.95/10.61 % (1451993)Termination reason: Instruction limit
% 34.95/10.61 % (1451993)Termination phase: Saturation
% 34.95/10.61 % (1451993)Time elapsed: 2.114 s
% 34.95/10.61 % (1451993)Peak memory usage: 189 MB
% 34.95/10.61 % (1451993)Instructions burned: 6926 (million)
% 34.95/10.61 % (1452004)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=3725423940:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2910 on theBenchmark for (2910ds/1722Mi)
% 34.95/10.61 % (1452004)First to succeed.
% 34.95/10.61 % (1452004)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1451912"
% 34.95/10.61 % (1452004)Refutation found. Thanks to Tanya!
% 34.95/10.61 % SZS status Unsatisfiable for theBenchmark
% 34.95/10.61 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/10.70 % (1452004)------------------------------
% 0.18/10.70 % (1452004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/10.70 % (1452004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/10.70 % (1452004)CaDiCaL version: 2.1.3
% 0.18/10.70 % (1452004)Termination reason: Refutation
% 0.18/10.70 % (1452004)Time elapsed: 0.471 s
% 0.18/10.70 % (1452004)Peak memory usage: 130 MB
% 0.18/10.70 % (1452004)Instructions burned: 1075 (million)
% 0.18/10.70 % (1452004)------------------------------
% 0.18/10.70 % (1452004)------------------------------
% 0.18/10.70 % (1451912)Success in time 9.73 s
% 0.18/10.70 % Vampire exiting
%------------------------------------------------------------------------------