%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET037-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 : n016.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 4.93s 1.63s
% Output : Refutation 6.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 24
% Syntax : Number of formulae : 99 ( 27 unt; 9 def)
% Number of atoms : 260 ( 50 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 319 ( 158 ~; 155 |; 0 &)
% ( 6 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 7 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-2 aty)
% Number of variables : 37 ( 0 sgn 37 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [X0] : singleton_set(X0) = non_ordered_pair(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set) ).
fof(f10,axiom,
! [X0,X1] : ordered_pair(X0,X1) = non_ordered_pair(singleton_set(X0),non_ordered_pair(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair) ).
fof(f11,axiom,
! [X0] :
( little_set(f2(X0))
| ~ ordered_pair_predicate(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair_predicate1) ).
fof(f12,axiom,
! [X0] :
( little_set(f3(X0))
| ~ ordered_pair_predicate(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair_predicate2) ).
fof(f13,axiom,
! [X0] :
( ~ ordered_pair_predicate(X0)
| X0 = ordered_pair(f2(X0),f3(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair_predicate3) ).
fof(f14,plain,
! [X0] :
( ~ ordered_pair_predicate(X0)
| ordered_pair(f2(X0),f3(X0)) = X0 ),
inference(reorient_equations,[],[f13]) ).
fof(f40,axiom,
! [X0,X1] :
( ~ member(X0,domain_of(X1))
| ordered_pair_predicate(f8(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain1) ).
fof(f41,axiom,
! [X0,X1] :
( member(f8(X0,X1),X1)
| ~ member(X0,domain_of(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain2) ).
fof(f42,axiom,
! [X0,X1] :
( ~ member(X0,domain_of(X1))
| X0 = first(f8(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain3) ).
fof(f43,plain,
! [X0,X1] :
( ~ member(X0,domain_of(X1))
| first(f8(X0,X1)) = X0 ),
inference(reorient_equations,[],[f42]) ).
fof(f167,axiom,
! [X0,X1] :
( ~ little_set(X0)
| ~ little_set(X1)
| first(ordered_pair(X0,X1)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',property_of_first) ).
fof(f168,axiom,
! [X0,X1] :
( ~ little_set(X0)
| ~ little_set(X1)
| second(ordered_pair(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',property_of_second) ).
fof(f183,axiom,
! [X2,X0,X1] :
( ~ little_set(X0)
| ~ little_set(X1)
| ~ function(X2)
| ~ member(ordered_pair(X0,X1),X2)
| apply(X2,X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',apply_for_functions1) ).
fof(f184,axiom,
function(a_function),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_function) ).
fof(f185,axiom,
member(a,domain_of(a_function)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',member_of_function_domain) ).
fof(f186,axiom,
apply(a_function,a) = b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',applying_the_function) ).
fof(f187,negated_conjecture,
~ member(ordered_pair(a,b),a_function),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_ordered_pair_in_function) ).
fof(f189,plain,
! [X0,X1] : ordered_pair(X0,X1) = non_ordered_pair(non_ordered_pair(X0,X0),non_ordered_pair(X0,X1)),
inference(definition_unfolding,[],[f10,f9]) ).
fof(f191,plain,
! [X0] :
( ~ ordered_pair_predicate(X0)
| non_ordered_pair(non_ordered_pair(f2(X0),f2(X0)),non_ordered_pair(f2(X0),f3(X0))) = X0 ),
inference(definition_unfolding,[],[f14,f189]) ).
fof(f218,plain,
! [X0,X1] :
( ~ little_set(X1)
| ~ little_set(X0)
| first(non_ordered_pair(non_ordered_pair(X0,X0),non_ordered_pair(X0,X1))) = X0 ),
inference(definition_unfolding,[],[f167,f189]) ).
fof(f219,plain,
! [X0,X1] :
( ~ little_set(X1)
| ~ little_set(X0)
| second(non_ordered_pair(non_ordered_pair(X0,X0),non_ordered_pair(X0,X1))) = X1 ),
inference(definition_unfolding,[],[f168,f189]) ).
fof(f224,plain,
! [X2,X0,X1] :
( ~ member(non_ordered_pair(non_ordered_pair(X0,X0),non_ordered_pair(X0,X1)),X2)
| ~ little_set(X1)
| ~ function(X2)
| ~ little_set(X0)
| apply(X2,X0) = X1 ),
inference(definition_unfolding,[],[f183,f189]) ).
fof(f225,plain,
~ member(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b)),a_function),
inference(definition_unfolding,[],[f187,f189]) ).
fof(f240,definition,
sF0 = non_ordered_pair(a,a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f241,plain,
non_ordered_pair(a,a) = sF0,
inference(reorient_equations,[],[f240]) ).
fof(f242,definition,
sF1 = non_ordered_pair(a,b),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f243,plain,
non_ordered_pair(a,b) = sF1,
inference(reorient_equations,[],[f242]) ).
fof(f244,definition,
sF2 = non_ordered_pair(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f245,plain,
non_ordered_pair(sF0,sF1) = sF2,
inference(reorient_equations,[],[f244]) ).
fof(f246,plain,
~ member(sF2,a_function),
inference(definition_folding,[],[f225,f245,f243,f241]) ).
fof(f300,plain,
a = first(f8(a,a_function)),
inference(resolution,[],[f43,f185]) ).
fof(f375,definition,
( spl3_9
<=> ordered_pair_predicate(f8(a,a_function)) ),
introduced(definition,[new_symbols(definition,[spl3_9])],[avatar_definition]) ).
fof(f376,plain,
( ordered_pair_predicate(f8(a,a_function))
| ~ spl3_9 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f377,plain,
( ~ ordered_pair_predicate(f8(a,a_function))
| spl3_9 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f434,plain,
ordered_pair_predicate(f8(a,a_function)),
inference(resolution,[],[f40,f185]) ).
fof(f435,plain,
( $false
| spl3_9 ),
inference(forward_subsumption_resolution,[],[f434,f377]) ).
fof(f436,plain,
spl3_9,
inference(avatar_contradiction_clause,[],[f435]) ).
fof(f917,plain,
( f8(a,a_function) = non_ordered_pair(non_ordered_pair(f2(f8(a,a_function)),f2(f8(a,a_function))),non_ordered_pair(f2(f8(a,a_function)),f3(f8(a,a_function))))
| ~ spl3_9 ),
inference(resolution,[],[f191,f376]) ).
fof(f1233,plain,
( ! [X0] :
( ~ member(f8(a,a_function),X0)
| ~ little_set(f3(f8(a,a_function)))
| ~ function(X0)
| ~ little_set(f2(f8(a,a_function)))
| f3(f8(a,a_function)) = apply(X0,f2(f8(a,a_function))) )
| ~ spl3_9 ),
inference(superposition,[],[f224,f917]) ).
fof(f1285,definition,
( spl3_53
<=> little_set(f2(f8(a,a_function))) ),
introduced(definition,[new_symbols(definition,[spl3_53])],[avatar_definition]) ).
fof(f1286,plain,
( little_set(f2(f8(a,a_function)))
| ~ spl3_53 ),
inference(avatar_component_clause,[],[f1285]) ).
fof(f1287,plain,
( ~ little_set(f2(f8(a,a_function)))
| spl3_53 ),
inference(avatar_component_clause,[],[f1285]) ).
fof(f1289,definition,
( spl3_54
<=> little_set(f3(f8(a,a_function))) ),
introduced(definition,[new_symbols(definition,[spl3_54])],[avatar_definition]) ).
fof(f1290,plain,
( little_set(f3(f8(a,a_function)))
| ~ spl3_54 ),
inference(avatar_component_clause,[],[f1289]) ).
fof(f1291,plain,
( ~ little_set(f3(f8(a,a_function)))
| spl3_54 ),
inference(avatar_component_clause,[],[f1289]) ).
fof(f1293,definition,
( spl3_55
<=> sF2 = f8(a,a_function) ),
introduced(definition,[new_symbols(definition,[spl3_55])],[avatar_definition]) ).
fof(f1294,plain,
( sF2 = f8(a,a_function)
| ~ spl3_55 ),
inference(avatar_component_clause,[],[f1293]) ).
fof(f1295,plain,
( sF2 != f8(a,a_function)
| spl3_55 ),
inference(avatar_component_clause,[],[f1293]) ).
fof(f1298,definition,
( spl3_56
<=> a = f2(f8(a,a_function)) ),
introduced(definition,[new_symbols(definition,[spl3_56])],[avatar_definition]) ).
fof(f1300,plain,
( a = f2(f8(a,a_function))
| ~ spl3_56 ),
inference(avatar_component_clause,[],[f1298]) ).
fof(f1333,definition,
( spl3_64
<=> ! [X0] :
( ~ member(f8(a,a_function),X0)
| f3(f8(a,a_function)) = apply(X0,f2(f8(a,a_function)))
| ~ function(X0) ) ),
introduced(definition,[new_symbols(definition,[spl3_64])],[avatar_definition]) ).
fof(f1334,plain,
( ! [X0] :
( ~ member(f8(a,a_function),X0)
| f3(f8(a,a_function)) = apply(X0,f2(f8(a,a_function)))
| ~ function(X0) )
| ~ spl3_64 ),
inference(avatar_component_clause,[],[f1333]) ).
fof(f1335,plain,
( ~ spl3_53
| ~ spl3_54
| spl3_64
| ~ spl3_9 ),
inference(avatar_split_clause,[],[f1233,f375,f1333,f1289,f1285]) ).
fof(f1388,plain,
( ~ ordered_pair_predicate(f8(a,a_function))
| spl3_53 ),
inference(resolution,[],[f1287,f11]) ).
fof(f1389,plain,
( $false
| ~ spl3_9
| spl3_53 ),
inference(forward_subsumption_resolution,[],[f1388,f376]) ).
fof(f1390,plain,
( ~ spl3_9
| spl3_53 ),
inference(avatar_contradiction_clause,[],[f1389]) ).
fof(f1577,plain,
( ~ ordered_pair_predicate(f8(a,a_function))
| spl3_54 ),
inference(resolution,[],[f12,f1291]) ).
fof(f1591,plain,
( $false
| ~ spl3_9
| spl3_54 ),
inference(forward_subsumption_resolution,[],[f1577,f376]) ).
fof(f1592,plain,
( ~ spl3_9
| spl3_54 ),
inference(avatar_contradiction_clause,[],[f1591]) ).
fof(f1593,plain,
( ! [X0] :
( ~ little_set(X0)
| first(non_ordered_pair(non_ordered_pair(X0,X0),non_ordered_pair(X0,f3(f8(a,a_function))))) = X0 )
| ~ spl3_54 ),
inference(resolution,[],[f1290,f218]) ).
fof(f1594,plain,
( ! [X0] :
( ~ little_set(X0)
| f3(f8(a,a_function)) = second(non_ordered_pair(non_ordered_pair(X0,X0),non_ordered_pair(X0,f3(f8(a,a_function))))) )
| ~ spl3_54 ),
inference(resolution,[],[f1290,f219]) ).
fof(f1609,plain,
( f3(f8(a,a_function)) = second(non_ordered_pair(non_ordered_pair(f2(f8(a,a_function)),f2(f8(a,a_function))),non_ordered_pair(f2(f8(a,a_function)),f3(f8(a,a_function)))))
| ~ spl3_53
| ~ spl3_54 ),
inference(resolution,[],[f1594,f1286]) ).
fof(f1622,plain,
( f3(f8(a,a_function)) = second(f8(a,a_function))
| ~ spl3_9
| ~ spl3_53
| ~ spl3_54 ),
inference(forward_demodulation,[],[f1609,f917]) ).
fof(f1631,plain,
( f3(f8(a,a_function)) = apply(a_function,f2(f8(a,a_function)))
| ~ function(a_function)
| ~ member(a,domain_of(a_function))
| ~ spl3_64 ),
inference(resolution,[],[f1334,f41]) ).
fof(f1638,plain,
( f3(f8(a,a_function)) = apply(a_function,f2(f8(a,a_function)))
| ~ member(a,domain_of(a_function))
| ~ spl3_64 ),
inference(forward_subsumption_resolution,[],[f1631,f184]) ).
fof(f1642,plain,
( f3(f8(a,a_function)) = apply(a_function,f2(f8(a,a_function)))
| ~ spl3_64 ),
inference(forward_subsumption_resolution,[],[f1638,f185]) ).
fof(f1652,plain,
( second(f8(a,a_function)) = apply(a_function,f2(f8(a,a_function)))
| ~ spl3_9
| ~ spl3_53
| ~ spl3_54
| ~ spl3_64 ),
inference(forward_demodulation,[],[f1642,f1622]) ).
fof(f1939,plain,
( f2(f8(a,a_function)) = first(non_ordered_pair(non_ordered_pair(f2(f8(a,a_function)),f2(f8(a,a_function))),non_ordered_pair(f2(f8(a,a_function)),f3(f8(a,a_function)))))
| ~ spl3_53
| ~ spl3_54 ),
inference(resolution,[],[f1593,f1286]) ).
fof(f1962,plain,
( first(f8(a,a_function)) = f2(f8(a,a_function))
| ~ spl3_9
| ~ spl3_53
| ~ spl3_54 ),
inference(forward_demodulation,[],[f1939,f917]) ).
fof(f1968,plain,
( a = f2(f8(a,a_function))
| ~ spl3_9
| ~ spl3_53
| ~ spl3_54 ),
inference(forward_demodulation,[],[f1962,f300]) ).
fof(f1970,plain,
( spl3_56
| ~ spl3_9
| ~ spl3_53
| ~ spl3_54 ),
inference(avatar_split_clause,[],[f1968,f1289,f1285,f375,f1298]) ).
fof(f1972,plain,
( f8(a,a_function) = non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,f3(f8(a,a_function))))
| ~ spl3_9
| ~ spl3_56 ),
inference(superposition,[],[f917,f1300]) ).
fof(f1977,plain,
( apply(a_function,a) = second(f8(a,a_function))
| ~ spl3_9
| ~ spl3_53
| ~ spl3_54
| ~ spl3_56
| ~ spl3_64 ),
inference(superposition,[],[f1652,f1300]) ).
fof(f1982,plain,
( b = second(f8(a,a_function))
| ~ spl3_9
| ~ spl3_53
| ~ spl3_54
| ~ spl3_56
| ~ spl3_64 ),
inference(forward_demodulation,[],[f1977,f186]) ).
fof(f1984,plain,
( f8(a,a_function) = non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,second(f8(a,a_function))))
| ~ spl3_9
| ~ spl3_53
| ~ spl3_54
| ~ spl3_56 ),
inference(forward_demodulation,[],[f1972,f1622]) ).
fof(f1985,plain,
( non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b)) = f8(a,a_function)
| ~ spl3_9
| ~ spl3_53
| ~ spl3_54
| ~ spl3_56
| ~ spl3_64 ),
inference(forward_demodulation,[],[f1984,f1982]) ).
fof(f1986,plain,
( f8(a,a_function) = non_ordered_pair(non_ordered_pair(a,a),sF1)
| ~ spl3_9
| ~ spl3_53
| ~ spl3_54
| ~ spl3_56
| ~ spl3_64 ),
inference(forward_demodulation,[],[f1985,f243]) ).
fof(f1987,plain,
( non_ordered_pair(sF0,sF1) = f8(a,a_function)
| ~ spl3_9
| ~ spl3_53
| ~ spl3_54
| ~ spl3_56
| ~ spl3_64 ),
inference(forward_demodulation,[],[f1986,f241]) ).
fof(f1988,plain,
( sF2 = f8(a,a_function)
| ~ spl3_9
| ~ spl3_53
| ~ spl3_54
| ~ spl3_56
| ~ spl3_64 ),
inference(forward_demodulation,[],[f1987,f245]) ).
fof(f1989,plain,
( $false
| ~ spl3_9
| ~ spl3_53
| ~ spl3_54
| spl3_55
| ~ spl3_56
| ~ spl3_64 ),
inference(forward_subsumption_resolution,[],[f1988,f1295]) ).
fof(f1990,plain,
( ~ spl3_9
| ~ spl3_53
| ~ spl3_54
| spl3_55
| ~ spl3_56
| ~ spl3_64 ),
inference(avatar_contradiction_clause,[],[f1989]) ).
fof(f2018,plain,
( member(sF2,a_function)
| ~ member(a,domain_of(a_function))
| ~ spl3_55 ),
inference(superposition,[],[f41,f1294]) ).
fof(f2019,plain,
( ~ member(a,domain_of(a_function))
| ~ spl3_55 ),
inference(forward_subsumption_resolution,[],[f2018,f246]) ).
fof(f2032,plain,
( $false
| ~ spl3_55 ),
inference(forward_subsumption_resolution,[],[f2019,f185]) ).
fof(f2033,plain,
~ spl3_55,
inference(avatar_contradiction_clause,[],[f2032]) ).
cnf(s9,plain,
spl3_9,
inference(sat_conversion,[],[f436]) ).
cnf(s44,plain,
( ~ spl3_9
| ~ spl3_53
| ~ spl3_54
| spl3_64 ),
inference(sat_conversion,[],[f1335]) ).
cnf(s53,plain,
( ~ spl3_9
| spl3_53 ),
inference(sat_conversion,[],[f1390]) ).
cnf(s56,plain,
( ~ spl3_9
| spl3_54 ),
inference(sat_conversion,[],[f1592]) ).
cnf(s66,plain,
( ~ spl3_9
| ~ spl3_53
| ~ spl3_54
| spl3_56 ),
inference(sat_conversion,[],[f1970]) ).
cnf(s67,plain,
( ~ spl3_9
| ~ spl3_53
| ~ spl3_54
| spl3_55
| ~ spl3_56
| ~ spl3_64 ),
inference(sat_conversion,[],[f1990]) ).
cnf(s68,plain,
~ spl3_55,
inference(sat_conversion,[],[f2033]) ).
cnf(s69,plain,
( ~ spl3_9
| ~ spl3_53
| ~ spl3_54
| ~ spl3_56
| ~ spl3_64 ),
inference(rat,[],[s67,s68]) ).
cnf(s70,plain,
spl3_54,
inference(rat,[],[s56,s9]) ).
cnf(s71,plain,
spl3_53,
inference(rat,[],[s53,s9]) ).
cnf(s72,plain,
spl3_56,
inference(rat,[],[s66,s70,s9,s71]) ).
cnf(s75,plain,
spl3_64,
inference(rat,[],[s44,s9,s70,s71]) ).
cnf(s79,plain,
$false,
inference(rat,[],[s69,s71,s70,s9,s75,s72]) ).
fof(f2041,plain,
$false,
inference(avatar_sat_refutation,[],[s79]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET037-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.12/0.37 % Computer : n016.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 28 00:23:02 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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
% 4.93/1.63 % (3146055)Input is clausal, will run a generic CNF schedule.
% 4.93/1.63 % (3146060)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=4250587222:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.93/1.63 % (3146062)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2468595253:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.93/1.63 % (3146063)lrs+10_1_sil=8000:sp=occurrence:random_seed=3497402969:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.93/1.63 % (3146061)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=173152411:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.93/1.63 % (3146066)dis-21_1_sil=8000:lcm=predicate:random_seed=2735314582: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)
% 4.93/1.63 % (3146064)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=184483576:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.93/1.63 % (3146065)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1794482035:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.93/1.63 % (3146064)Instruction limit reached!
% 4.93/1.63 % (3146064)------------------------------
% 4.93/1.63 % (3146064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.93/1.63 % (3146064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.93/1.63 % (3146064)CaDiCaL version: 2.1.3
% 4.93/1.63 % (3146064)Termination reason: Instruction limit
% 4.93/1.63 % (3146064)Termination phase: Saturation
% 4.93/1.63 % (3146064)Time elapsed: 0.069 s
% 4.93/1.63 % (3146064)Peak memory usage: 88 MB
% 4.93/1.63 % (3146064)Instructions burned: 116 (million)
% 4.93/1.63 % (3146063)Instruction limit reached!
% 4.93/1.63 % (3146063)------------------------------
% 4.93/1.63 % (3146063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.93/1.63 % (3146063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.93/1.63 % (3146063)CaDiCaL version: 2.1.3
% 4.93/1.63 % (3146063)Termination reason: Instruction limit
% 4.93/1.63 % (3146063)Termination phase: Saturation
% 4.93/1.63 % (3146063)Time elapsed: 0.070 s
% 4.93/1.63 % (3146063)Peak memory usage: 89 MB
% 4.93/1.63 % (3146063)Instructions burned: 107 (million)
% 4.93/1.63 % (3146066)Instruction limit reached!
% 4.93/1.63 % (3146066)------------------------------
% 4.93/1.63 % (3146066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.93/1.63 % (3146066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.93/1.63 % (3146066)CaDiCaL version: 2.1.3
% 4.93/1.63 % (3146066)Termination reason: Instruction limit
% 4.93/1.63 % (3146066)Termination phase: Saturation
% 4.93/1.63 % (3146066)Time elapsed: 0.072 s
% 4.93/1.63 % (3146066)Peak memory usage: 89 MB
% 4.93/1.63 % (3146066)Instructions burned: 117 (million)
% 4.93/1.63 % (3146065)Instruction limit reached!
% 4.93/1.63 % (3146065)------------------------------
% 4.93/1.63 % (3146065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.93/1.63 % (3146065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.93/1.63 % (3146065)CaDiCaL version: 2.1.3
% 4.93/1.63 % (3146065)Termination reason: Instruction limit
% 4.93/1.63 % (3146065)Termination phase: Saturation
% 4.93/1.63 % (3146065)Time elapsed: 0.126 s
% 4.93/1.63 % (3146065)Peak memory usage: 90 MB
% 4.93/1.63 % (3146065)Instructions burned: 180 (million)
% 4.93/1.63 % (3146077)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1807647207:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 4.93/1.63 % (3146075)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=2762095802:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 4.93/1.63 % (3146076)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3521488250: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)
% 4.93/1.63 % (3146077)Refutation not found, incomplete strategy
% 4.93/1.63 % (3146077)------------------------------
% 4.93/1.63 % (3146077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.93/1.63 % (3146077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.93/1.63 % (3146077)CaDiCaL version: 2.1.3
% 4.93/1.63 % (3146077)Termination reason: Refutation not found, incomplete strategy
% 4.93/1.63 % (3146077)Time elapsed: 0.004 s
% 4.93/1.63 % (3146077)Peak memory usage: 88 MB
% 4.93/1.63 % (3146077)Instructions burned: 4 (million)
% 4.93/1.63 % (3146078)lrs+10_64_to=lpo:sil=8000:random_seed=2587320998:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 4.93/1.63 % (3146075)Instruction limit reached!
% 4.93/1.63 % (3146075)------------------------------
% 4.93/1.63 % (3146075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.93/1.63 % (3146075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.93/1.63 % (3146075)CaDiCaL version: 2.1.3
% 4.93/1.63 % (3146075)Termination reason: Instruction limit
% 4.93/1.63 % (3146075)Termination phase: Saturation
% 4.93/1.63 % (3146075)Time elapsed: 0.083 s
% 4.93/1.63 % (3146075)Peak memory usage: 89 MB
% 4.93/1.63 % (3146075)Instructions burned: 143 (million)
% 4.93/1.63 % (3146076)Instruction limit reached!
% 4.93/1.63 % (3146076)------------------------------
% 4.93/1.63 % (3146076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.93/1.63 % (3146076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.93/1.63 % (3146076)CaDiCaL version: 2.1.3
% 4.93/1.63 % (3146076)Termination reason: Instruction limit
% 4.93/1.63 % (3146076)Termination phase: Saturation
% 4.93/1.63 % (3146076)Time elapsed: 0.103 s
% 4.93/1.63 % (3146076)Peak memory usage: 90 MB
% 4.93/1.63 % (3146076)Instructions burned: 190 (million)
% 4.93/1.63 % (3146078)Instruction limit reached!
% 4.93/1.63 % (3146078)------------------------------
% 4.93/1.63 % (3146078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.93/1.63 % (3146078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.93/1.63 % (3146078)CaDiCaL version: 2.1.3
% 4.93/1.63 % (3146078)Termination reason: Instruction limit
% 4.93/1.63 % (3146078)Termination phase: Saturation
% 4.93/1.63 % (3146078)Time elapsed: 0.074 s
% 4.93/1.63 % (3146078)Peak memory usage: 90 MB
% 4.93/1.63 % (3146078)Instructions burned: 127 (million)
% 4.93/1.63 % (3146060)First to succeed.
% 4.93/1.63 % (3146060)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3146055"
% 4.93/1.63 % (3146077)------------------------------
% 4.93/1.63 % (3146077)------------------------------
% 4.93/1.63 % (3146083)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=229962922:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 4.93/1.63 % (3146084)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=332928783:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 4.93/1.63 % (3146085)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3184074593:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 4.93/1.63 % (3146060)Refutation found. Thanks to Tanya!
% 4.93/1.63 % SZS status Unsatisfiable for theBenchmark
% 4.93/1.63 % SZS output start Proof for theBenchmark
% See solution above
% 6.07/1.82 % (3146060)------------------------------
% 6.07/1.82 % (3146060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.82 % (3146060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.82 % (3146060)CaDiCaL version: 2.1.3
% 6.07/1.82 % (3146060)Termination reason: Refutation
% 6.07/1.82 % (3146060)Time elapsed: 0.483 s
% 6.07/1.82 % (3146060)Peak memory usage: 133 MB
% 6.07/1.82 % (3146060)Instructions burned: 1279 (million)
% 6.07/1.82 % (3146060)------------------------------
% 6.07/1.82 % (3146060)------------------------------
% 6.07/1.82 % (3146055)Success in time 0.773 s
% 6.07/1.82 % Vampire exiting
%------------------------------------------------------------------------------