%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU284+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:48:09 PM UTC 2026
% Result : Theorem 26.65s 4.65s
% Output : Refutation 27.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 6
% Syntax : Number of formulae : 68 ( 9 unt; 3 def)
% Number of atoms : 240 ( 90 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 274 ( 102 ~; 105 |; 57 &)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 3 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 1 con; 0-2 aty)
% Number of variables : 110 ( 0 sgn 84 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f215,axiom,
! [X0] :
( ( ! [X1,X2,X3] :
( ( in(X1,X0)
& X2 = singleton(X1)
& X3 = singleton(X1) )
=> X2 = X3 )
& ! [X1] :
~ ( in(X1,X0)
& ! [X2] : X2 != singleton(X1) ) )
=> ? [X1] :
( relation(X1)
& function(X1)
& relation_dom(X1) = X0
& ! [X2] :
( in(X2,X0)
=> apply(X1,X2) = singleton(X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s2_funct_1__e16_22__wellord2__1) ).
fof(f216,conjecture,
! [X0] :
? [X1] :
( relation(X1)
& function(X1)
& relation_dom(X1) = X0
& ! [X2] :
( in(X2,X0)
=> apply(X1,X2) = singleton(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_funct_1__e16_22__wellord2) ).
fof(f217,negated_conjecture,
~ ! [X0] :
? [X1] :
( relation(X1)
& function(X1)
& relation_dom(X1) = X0
& ! [X2] :
( in(X2,X0)
=> apply(X1,X2) = singleton(X2) ) ),
inference(negated_conjecture,[status(cth)],[f216]) ).
fof(f345,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f387,plain,
! [X0] :
( ( ! [X1,X2,X3] :
( ( in(X1,X0)
& X2 = singleton(X1)
& X3 = singleton(X1) )
=> X2 = X3 )
& ! [X4] :
~ ( in(X4,X0)
& ! [X5] : singleton(X4) != X5 ) )
=> ? [X6] :
( relation(X6)
& function(X6)
& relation_dom(X6) = X0
& ! [X7] :
( in(X7,X0)
=> singleton(X7) = apply(X6,X7) ) ) ),
inference(rectify,[],[f215]) ).
fof(f568,plain,
! [X0] :
( ? [X6] :
( relation(X6)
& function(X6)
& relation_dom(X6) = X0
& ! [X7] :
( singleton(X7) = apply(X6,X7)
| ~ in(X7,X0) ) )
| ? [X1,X2,X3] :
( X2 != X3
& in(X1,X0)
& X2 = singleton(X1)
& X3 = singleton(X1) )
| ? [X4] :
( in(X4,X0)
& ! [X5] : singleton(X4) != X5 ) ),
inference(ennf_transformation,[],[f387]) ).
fof(f569,plain,
! [X0] :
( ? [X6] :
( relation(X6)
& function(X6)
& relation_dom(X6) = X0
& ! [X7] :
( singleton(X7) = apply(X6,X7)
| ~ in(X7,X0) ) )
| ? [X1,X2,X3] :
( X2 != X3
& in(X1,X0)
& X2 = singleton(X1)
& X3 = singleton(X1) )
| ? [X4] :
( in(X4,X0)
& ! [X5] : singleton(X4) != X5 ) ),
inference(flattening,[],[f568]) ).
fof(f570,plain,
? [X0] :
! [X1] :
( ~ relation(X1)
| ~ function(X1)
| relation_dom(X1) != X0
| ? [X2] :
( singleton(X2) != apply(X1,X2)
& in(X2,X0) ) ),
inference(ennf_transformation,[],[f217]) ).
fof(f771,definition,
! [X0] :
( ? [X1,X2,X3] :
( X2 != X3
& in(X1,X0)
& X2 = singleton(X1)
& X3 = singleton(X1) )
| ~ sP10(X0) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f772,plain,
! [X0] :
( ? [X6] :
( relation(X6)
& function(X6)
& relation_dom(X6) = X0
& ! [X7] :
( singleton(X7) = apply(X6,X7)
| ~ in(X7,X0) ) )
| sP10(X0)
| ? [X4] :
( in(X4,X0)
& ! [X5] : singleton(X4) != X5 ) ),
inference(definition_folding,[],[f569,f771]) ).
fof(f1041,plain,
! [X0] :
( ? [X1,X2,X3] :
( X2 != X3
& in(X1,X0)
& X2 = singleton(X1)
& X3 = singleton(X1) )
| ~ sP10(X0) ),
inference(nnf_transformation,[],[f771]) ).
fof(f1042,plain,
! [X0] :
( ( sK184(X0) != sK185(X0)
& in(sK183(X0),X0)
& sK184(X0) = singleton(sK183(X0))
& sK185(X0) = singleton(sK183(X0)) )
| ~ sP10(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK183,sK184,sK185]),skolemize(X1,sK183(X0)),skolemize(X2,sK184(X0)),skolemize(X3,sK185(X0))],[f1041]) ).
fof(f1043,plain,
! [X0] :
( ? [X1] :
( relation(X1)
& function(X1)
& relation_dom(X1) = X0
& ! [X2] :
( singleton(X2) = apply(X1,X2)
| ~ in(X2,X0) ) )
| sP10(X0)
| ? [X3] :
( in(X3,X0)
& ! [X4] : singleton(X3) != X4 ) ),
inference(rectify,[],[f772]) ).
fof(f1044,plain,
! [X0] :
( ( relation(sK186(X0))
& function(sK186(X0))
& relation_dom(sK186(X0)) = X0
& ! [X2] :
( singleton(X2) = apply(sK186(X0),X2)
| ~ in(X2,X0) ) )
| sP10(X0)
| ( in(sK187(X0),X0)
& ! [X4] : singleton(sK187(X0)) != X4 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK186,sK187]),skolemize(X1,sK186(X0)),skolemize(X3,sK187(X0))],[f1043]) ).
fof(f1045,plain,
! [X1] :
( ~ relation(X1)
| ~ function(X1)
| relation_dom(X1) != sK188
| ( singleton(sK189(X1)) != apply(X1,sK189(X1))
& in(sK189(X1),sK188) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK188,sK189]),skolemize(X0,sK188),skolemize(X2,sK189(X1))],[f570]) ).
fof(f1694,plain,
! [X0] :
( sK185(X0) = singleton(sK183(X0))
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f1042]) ).
fof(f1695,plain,
! [X0] :
( sK184(X0) = singleton(sK183(X0))
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f1042]) ).
fof(f1697,plain,
! [X0] :
( sK184(X0) != sK185(X0)
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f1042]) ).
fof(f1698,plain,
! [X2,X0,X4] :
( singleton(X2) = apply(sK186(X0),X2)
| ~ in(X2,X0)
| sP10(X0)
| singleton(sK187(X0)) != X4 ),
inference(cnf_transformation,[],[f1044]) ).
fof(f1700,plain,
! [X0,X4] :
( relation_dom(sK186(X0)) = X0
| sP10(X0)
| singleton(sK187(X0)) != X4 ),
inference(cnf_transformation,[],[f1044]) ).
fof(f1702,plain,
! [X0,X4] :
( function(sK186(X0))
| sP10(X0)
| singleton(sK187(X0)) != X4 ),
inference(cnf_transformation,[],[f1044]) ).
fof(f1704,plain,
! [X0,X4] :
( relation(sK186(X0))
| sP10(X0)
| singleton(sK187(X0)) != X4 ),
inference(cnf_transformation,[],[f1044]) ).
fof(f1706,plain,
! [X1] :
( relation_dom(X1) != sK188
| ~ function(X1)
| ~ relation(X1)
| in(sK189(X1),sK188) ),
inference(cnf_transformation,[],[f1045]) ).
fof(f1707,plain,
! [X1] :
( ~ relation(X1)
| ~ function(X1)
| relation_dom(X1) != sK188
| singleton(sK189(X1)) != apply(X1,sK189(X1)) ),
inference(cnf_transformation,[],[f1045]) ).
fof(f1915,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f345]) ).
fof(f2142,plain,
! [X0] :
( sK184(X0) = unordered_pair(sK183(X0),sK183(X0))
| ~ sP10(X0) ),
inference(definition_unfolding,[],[f1695,f1915]) ).
fof(f2143,plain,
! [X0] :
( sK185(X0) = unordered_pair(sK183(X0),sK183(X0))
| ~ sP10(X0) ),
inference(definition_unfolding,[],[f1694,f1915]) ).
fof(f2144,plain,
! [X0,X4] :
( relation(sK186(X0))
| sP10(X0)
| unordered_pair(sK187(X0),sK187(X0)) != X4 ),
inference(definition_unfolding,[],[f1704,f1915]) ).
fof(f2145,plain,
! [X0,X4] :
( function(sK186(X0))
| sP10(X0)
| unordered_pair(sK187(X0),sK187(X0)) != X4 ),
inference(definition_unfolding,[],[f1702,f1915]) ).
fof(f2146,plain,
! [X0,X4] :
( relation_dom(sK186(X0)) = X0
| sP10(X0)
| unordered_pair(sK187(X0),sK187(X0)) != X4 ),
inference(definition_unfolding,[],[f1700,f1915]) ).
fof(f2148,plain,
! [X2,X0,X4] :
( apply(sK186(X0),X2) = unordered_pair(X2,X2)
| ~ in(X2,X0)
| sP10(X0)
| unordered_pair(sK187(X0),sK187(X0)) != X4 ),
inference(definition_unfolding,[],[f1698,f1915,f1915]) ).
fof(f2149,plain,
! [X1] :
( apply(X1,sK189(X1)) != unordered_pair(sK189(X1),sK189(X1))
| ~ function(X1)
| relation_dom(X1) != sK188
| ~ relation(X1) ),
inference(definition_unfolding,[],[f1707,f1915]) ).
fof(f2333,plain,
! [X0] :
( relation(sK186(X0))
| sP10(X0) ),
inference(equality_resolution,[],[f2144]) ).
fof(f2334,plain,
! [X0] :
( function(sK186(X0))
| sP10(X0) ),
inference(equality_resolution,[],[f2145]) ).
fof(f2335,plain,
! [X0] :
( relation_dom(sK186(X0)) = X0
| sP10(X0) ),
inference(equality_resolution,[],[f2146]) ).
fof(f2336,plain,
! [X2,X0] :
( apply(sK186(X0),X2) = unordered_pair(X2,X2)
| ~ in(X2,X0)
| sP10(X0) ),
inference(equality_resolution,[],[f2148]) ).
fof(f2547,plain,
! [X0] :
( sK188 != X0
| ~ function(sK186(X0))
| ~ relation(sK186(X0))
| in(sK189(sK186(X0)),sK188)
| sP10(X0) ),
inference(superposition,[],[f1706,f2335]) ).
fof(f2548,plain,
! [X0] :
( sK188 != X0
| ~ relation(sK186(X0))
| in(sK189(sK186(X0)),sK188)
| sP10(X0) ),
inference(forward_subsumption_resolution,[],[f2547,f2334]) ).
fof(f2549,plain,
! [X0] :
( sK188 != X0
| in(sK189(sK186(X0)),sK188)
| sP10(X0) ),
inference(forward_subsumption_resolution,[],[f2548,f2333]) ).
fof(f2550,plain,
( in(sK189(sK186(sK188)),sK188)
| sP10(sK188) ),
inference(equality_resolution,[],[f2549]) ).
fof(f2552,definition,
( spl213_13
<=> sP10(sK188) ),
introduced(definition,[new_symbols(definition,[spl213_13])],[avatar_definition]) ).
fof(f2554,plain,
( sP10(sK188)
| ~ spl213_13 ),
inference(avatar_component_clause,[],[f2552]) ).
fof(f2556,definition,
( spl213_14
<=> in(sK189(sK186(sK188)),sK188) ),
introduced(definition,[new_symbols(definition,[spl213_14])],[avatar_definition]) ).
fof(f2558,plain,
( in(sK189(sK186(sK188)),sK188)
| ~ spl213_14 ),
inference(avatar_component_clause,[],[f2556]) ).
fof(f2559,plain,
( spl213_13
| spl213_14 ),
inference(avatar_split_clause,[],[f2550,f2556,f2552]) ).
fof(f2581,plain,
! [X0,X1] :
( apply(X1,sK189(X1)) != apply(sK186(X0),sK189(X1))
| ~ function(X1)
| relation_dom(X1) != sK188
| ~ relation(X1)
| ~ in(sK189(X1),X0)
| sP10(X0) ),
inference(superposition,[],[f2149,f2336]) ).
fof(f2611,plain,
! [X0] :
( ~ function(sK186(X0))
| relation_dom(sK186(X0)) != sK188
| ~ relation(sK186(X0))
| ~ in(sK189(sK186(X0)),X0)
| sP10(X0) ),
inference(equality_resolution,[],[f2581]) ).
fof(f2613,plain,
! [X0] :
( relation_dom(sK186(X0)) != sK188
| ~ relation(sK186(X0))
| ~ in(sK189(sK186(X0)),X0)
| sP10(X0) ),
inference(forward_subsumption_resolution,[],[f2611,f2334]) ).
fof(f2615,plain,
! [X0] :
( relation_dom(sK186(X0)) != sK188
| ~ in(sK189(sK186(X0)),X0)
| sP10(X0) ),
inference(forward_subsumption_resolution,[],[f2613,f2333]) ).
fof(f2618,plain,
! [X0] :
( sK188 != X0
| ~ in(sK189(sK186(X0)),X0)
| sP10(X0)
| sP10(X0) ),
inference(superposition,[],[f2615,f2335]) ).
fof(f2619,plain,
! [X0] :
( sK188 != X0
| ~ in(sK189(sK186(X0)),X0)
| sP10(X0) ),
inference(duplicate_literal_removal,[],[f2618]) ).
fof(f2620,plain,
( ~ in(sK189(sK186(sK188)),sK188)
| sP10(sK188) ),
inference(equality_resolution,[],[f2619]) ).
fof(f2679,plain,
( sK185(sK188) = unordered_pair(sK183(sK188),sK183(sK188))
| ~ spl213_13 ),
inference(unit_resulting_resolution,[],[f2143,f2554]) ).
fof(f2728,plain,
! [X0] :
( sK184(X0) = sK185(X0)
| ~ sP10(X0)
| ~ sP10(X0) ),
inference(superposition,[],[f2143,f2142]) ).
fof(f2729,plain,
( sK185(sK188) = sK184(sK188)
| ~ sP10(sK188)
| ~ spl213_13 ),
inference(superposition,[],[f2679,f2142]) ).
fof(f2745,plain,
! [X0] :
( sK184(X0) = sK185(X0)
| ~ sP10(X0) ),
inference(duplicate_literal_removal,[],[f2728]) ).
fof(f2752,plain,
( ~ sP10(sK188)
| ~ spl213_13 ),
inference(forward_subsumption_resolution,[],[f2729,f1697]) ).
fof(f2753,plain,
! [X0] : ~ sP10(X0),
inference(forward_subsumption_resolution,[],[f2745,f1697]) ).
fof(f2757,plain,
( $false
| ~ spl213_13 ),
inference(forward_subsumption_resolution,[],[f2752,f2554]) ).
fof(f2758,plain,
~ spl213_13,
inference(avatar_contradiction_clause,[],[f2757]) ).
fof(f2768,plain,
( sP10(sK188)
| ~ spl213_14 ),
inference(forward_subsumption_resolution,[],[f2620,f2558]) ).
fof(f2769,plain,
( $false
| ~ spl213_14 ),
inference(forward_subsumption_resolution,[],[f2768,f2753]) ).
fof(f2770,plain,
~ spl213_14,
inference(avatar_contradiction_clause,[],[f2769]) ).
cnf(s11,plain,
( spl213_13
| spl213_14 ),
inference(sat_conversion,[],[f2559]) ).
cnf(s12,plain,
~ spl213_13,
inference(sat_conversion,[],[f2758]) ).
cnf(s13,plain,
~ spl213_14,
inference(sat_conversion,[],[f2770]) ).
cnf(s14,plain,
$false,
inference(rat,[],[s11,s13,s12]) ).
fof(f2771,plain,
$false,
inference(avatar_sat_refutation,[],[s14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU284+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n015.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Mon Sep 28 04:32:46 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.44 Running first-order theorem proving
% 0.12/0.44 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.64/2.58 % (2258013)Detected formulas, will run a generic FOF schedule.
% 11.64/2.58 % (2258023)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3817449284:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.64/2.58 % (2258021)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4028957193:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.64/2.58 % (2258020)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2318534775:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.64/2.58 % (2258018)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=841090343:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.64/2.58 % (2258022)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3670448776:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.64/2.58 % (2258019)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2883531287:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.64/2.58 % (2258023)Instruction limit reached!
% 11.64/2.58 % (2258023)------------------------------
% 11.64/2.58 % (2258023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.64/2.58 % (2258023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/2.58 % (2258023)CaDiCaL version: 2.1.3
% 11.64/2.58 % (2258023)Termination reason: Instruction limit
% 11.64/2.58 % (2258023)Termination phase: Saturation
% 11.64/2.58 % (2258023)Time elapsed: 0.053 s
% 11.64/2.58 % (2258023)Peak memory usage: 91 MB
% 11.64/2.58 % (2258023)Instructions burned: 140 (million)
% 11.64/2.58 % (2258024)dis-21_1_sil=8000:lcm=predicate:random_seed=4198813137:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.64/2.58 % (2258021)Instruction limit reached!
% 11.64/2.58 % (2258021)------------------------------
% 11.64/2.58 % (2258021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.64/2.58 % (2258021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/2.58 % (2258021)CaDiCaL version: 2.1.3
% 11.64/2.58 % (2258021)Termination reason: Instruction limit
% 11.64/2.58 % (2258021)Termination phase: Saturation
% 11.64/2.58 % (2258021)Time elapsed: 0.066 s
% 11.64/2.58 % (2258021)Peak memory usage: 90 MB
% 11.64/2.58 % (2258021)Instructions burned: 110 (million)
% 11.64/2.58 % (2258024)Instruction limit reached!
% 11.64/2.58 % (2258024)------------------------------
% 11.64/2.58 % (2258024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.64/2.58 % (2258024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/2.58 % (2258024)CaDiCaL version: 2.1.3
% 11.64/2.58 % (2258024)Termination reason: Instruction limit
% 11.64/2.58 % (2258024)Termination phase: Saturation
% 11.64/2.58 % (2258024)Time elapsed: 0.063 s
% 11.64/2.58 % (2258024)Peak memory usage: 90 MB
% 11.64/2.58 % (2258024)Instructions burned: 130 (million)
% 11.64/2.58 % (2258022)Instruction limit reached!
% 11.64/2.58 % (2258022)------------------------------
% 11.64/2.58 % (2258022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.64/2.58 % (2258022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/2.58 % (2258022)CaDiCaL version: 2.1.3
% 11.64/2.58 % (2258022)Termination reason: Instruction limit
% 11.64/2.58 % (2258022)Termination phase: Saturation
% 11.64/2.58 % (2258022)Time elapsed: 0.074 s
% 11.64/2.58 % (2258022)Peak memory usage: 89 MB
% 11.64/2.58 % (2258022)Instructions burned: 119 (million)
% 11.64/2.58 % (2258032)lrs+10_1_sil=8000:sp=occurrence:random_seed=4211836254:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.64/2.58 % (2258032)Instruction limit reached!
% 11.64/2.58 % (2258032)------------------------------
% 11.64/2.58 % (2258032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.64/2.58 % (2258032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/2.58 % (2258032)CaDiCaL version: 2.1.3
% 11.64/2.58 % (2258032)Termination reason: Instruction limit
% 11.64/2.58 % (2258032)Termination phase: Saturation
% 11.64/2.58 % (2258032)Time elapsed: 0.104 s
% 11.64/2.58 % (2258032)Peak memory usage: 94 MB
% 11.64/2.58 % (2258032)Instructions burned: 288 (million)
% 17.99/3.40 % (2258034)lrs+1011_1_sil=32000:sp=occurrence:random_seed=500599858:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 17.99/3.40 % (2258033)lrs+10_1_sil=32000:urr=on:br=off:random_seed=808773025:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 17.99/3.40 % (2258035)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2056851572:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 17.99/3.40 % (2258033)Instruction limit reached!
% 17.99/3.40 % (2258033)------------------------------
% 17.99/3.40 % (2258033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.40 % (2258033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.40 % (2258033)CaDiCaL version: 2.1.3
% 17.99/3.40 % (2258033)Termination reason: Instruction limit
% 17.99/3.40 % (2258033)Termination phase: Saturation
% 17.99/3.40 % (2258033)Time elapsed: 0.088 s
% 17.99/3.40 % (2258033)Peak memory usage: 90 MB
% 17.99/3.40 % (2258033)Instructions burned: 159 (million)
% 17.99/3.40 % (2258040)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=520586182:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 17.99/3.40 % (2258035)Instruction limit reached!
% 17.99/3.40 % (2258035)------------------------------
% 17.99/3.40 % (2258035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.40 % (2258035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.40 % (2258035)CaDiCaL version: 2.1.3
% 17.99/3.40 % (2258035)Termination reason: Instruction limit
% 17.99/3.40 % (2258035)Termination phase: Saturation
% 17.99/3.40 % (2258035)Time elapsed: 0.139 s
% 17.99/3.40 % (2258035)Peak memory usage: 93 MB
% 17.99/3.40 % (2258035)Instructions burned: 249 (million)
% 17.99/3.40 % (2258040)Instruction limit reached!
% 17.99/3.40 % (2258040)------------------------------
% 17.99/3.40 % (2258040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.40 % (2258040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.40 % (2258040)CaDiCaL version: 2.1.3
% 17.99/3.40 % (2258040)Termination reason: Instruction limit
% 17.99/3.40 % (2258040)Termination phase: Saturation
% 17.99/3.40 % (2258040)Time elapsed: 0.100 s
% 17.99/3.40 % (2258040)Peak memory usage: 91 MB
% 17.99/3.40 % (2258040)Instructions burned: 295 (million)
% 17.99/3.40 % (2258034)Instruction limit reached!
% 17.99/3.40 % (2258034)------------------------------
% 17.99/3.40 % (2258034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.40 % (2258034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.40 % (2258034)CaDiCaL version: 2.1.3
% 17.99/3.40 % (2258034)Termination reason: Instruction limit
% 17.99/3.40 % (2258034)Termination phase: Saturation
% 17.99/3.40 % (2258034)Time elapsed: 0.229 s
% 17.99/3.40 % (2258034)Peak memory usage: 94 MB
% 17.99/3.40 % (2258034)Instructions burned: 325 (million)
% 17.99/3.40 % (2258041)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1321376266:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 17.99/3.40 % (2258043)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3095611155:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 17.99/3.40 % (2258044)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1999347582:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 17.99/3.41 % (2258043)Instruction limit reached!
% 17.99/3.41 % (2258043)------------------------------
% 17.99/3.41 % (2258043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.41 % (2258043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.41 % (2258043)CaDiCaL version: 2.1.3
% 17.99/3.41 % (2258043)Termination reason: Instruction limit
% 17.99/3.41 % (2258043)Termination phase: Saturation
% 17.99/3.41 % (2258043)Time elapsed: 0.073 s
% 17.99/3.41 % (2258043)Peak memory usage: 90 MB
% 17.99/3.41 % (2258043)Instructions burned: 115 (million)
% 17.99/3.41 % (2258044)Instruction limit reached!
% 17.99/3.41 % (2258044)------------------------------
% 17.99/3.41 % (2258044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.99/3.41 % (2258044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.99/3.41 % (2258044)CaDiCaL version: 2.1.3
% 17.99/3.41 % (2258044)Termination reason: Instruction limit
% 17.99/3.41 % (2258044)Termination phase: Saturation
% 26.65/4.65 % (2258044)Time elapsed: 0.037 s
% 26.65/4.65 % (2258044)Peak memory usage: 90 MB
% 26.65/4.65 % (2258044)Instructions burned: 129 (million)
% 26.65/4.65 % (2258045)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4031919259:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 26.65/4.65 % (2258045)Instruction limit reached!
% 26.65/4.65 % (2258045)------------------------------
% 26.65/4.65 % (2258045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.65 % (2258045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.65 % (2258045)CaDiCaL version: 2.1.3
% 26.65/4.65 % (2258045)Termination reason: Instruction limit
% 26.65/4.65 % (2258045)Termination phase: Saturation
% 26.65/4.65 % (2258045)Time elapsed: 0.066 s
% 26.65/4.65 % (2258045)Peak memory usage: 89 MB
% 26.65/4.65 % (2258045)Instructions burned: 114 (million)
% 26.65/4.65 % (2258050)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1042116551:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 26.65/4.65 % (2258049)lrs+10_1_sil=8000:sp=occurrence:random_seed=2258292502:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 26.65/4.65 % (2258050)Instruction limit reached!
% 26.65/4.65 % (2258050)------------------------------
% 26.65/4.65 % (2258050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.65 % (2258050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.65 % (2258050)CaDiCaL version: 2.1.3
% 26.65/4.65 % (2258050)Termination reason: Instruction limit
% 26.65/4.65 % (2258050)Termination phase: Saturation
% 26.65/4.65 % (2258050)Time elapsed: 0.143 s
% 26.65/4.65 % (2258050)Peak memory usage: 94 MB
% 26.65/4.65 % (2258050)Instructions burned: 439 (million)
% 26.65/4.65 % (2258052)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=483101200:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 26.65/4.65 % (2258055)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3984390627:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 26.65/4.65 % (2258055)Instruction limit reached!
% 26.65/4.65 % (2258055)------------------------------
% 26.65/4.65 % (2258055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.65 % (2258055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.65 % (2258055)CaDiCaL version: 2.1.3
% 26.65/4.65 % (2258055)Termination reason: Instruction limit
% 26.65/4.65 % (2258055)Termination phase: Saturation
% 26.65/4.65 % (2258055)Time elapsed: 0.044 s
% 26.65/4.65 % (2258055)Peak memory usage: 92 MB
% 26.65/4.65 % (2258055)Instructions burned: 136 (million)
% 26.65/4.65 % (2258058)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4183089369:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 26.65/4.65 % (2258049)Instruction limit reached!
% 26.65/4.65 % (2258049)------------------------------
% 26.65/4.65 % (2258049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.65 % (2258049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.65 % (2258049)CaDiCaL version: 2.1.3
% 26.65/4.65 % (2258049)Termination reason: Instruction limit
% 26.65/4.65 % (2258049)Termination phase: Saturation
% 26.65/4.65 % (2258049)Time elapsed: 0.565 s
% 26.65/4.65 % (2258049)Peak memory usage: 102 MB
% 26.65/4.65 % (2258049)Instructions burned: 908 (million)
% 26.65/4.65 % (2258058)Instruction limit reached!
% 26.65/4.65 % (2258058)------------------------------
% 26.65/4.65 % (2258058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.65 % (2258058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.65 % (2258058)CaDiCaL version: 2.1.3
% 26.65/4.65 % (2258058)Termination reason: Instruction limit
% 26.65/4.65 % (2258058)Termination phase: Saturation
% 26.65/4.65 % (2258058)Time elapsed: 0.208 s
% 26.65/4.65 % (2258058)Peak memory usage: 99 MB
% 26.65/4.65 % (2258058)Instructions burned: 593 (million)
% 26.65/4.65 % (2258060)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1116331897:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 26.65/4.65 % (2258061)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=662533575:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 26.65/4.65 % (2258061)Instruction limit reached!
% 26.65/4.65 % (2258061)------------------------------
% 26.65/4.65 % (2258061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.65 % (2258061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.65 % (2258061)CaDiCaL version: 2.1.3
% 26.65/4.65 % (2258061)Termination reason: Instruction limit
% 26.65/4.65 % (2258061)Termination phase: Saturation
% 26.65/4.65 % (2258061)Time elapsed: 0.051 s
% 26.65/4.65 % (2258061)Peak memory usage: 91 MB
% 26.65/4.65 % (2258061)Instructions burned: 126 (million)
% 26.65/4.65 % (2258064)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=768876742:i=134:gtgl=5:slsql=off:gtg=exists_sym_2982 on theBenchmark for (2982ds/134Mi)
% 26.65/4.65 % (2258064)Instruction limit reached!
% 26.65/4.65 % (2258064)------------------------------
% 26.65/4.65 % (2258064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.65 % (2258064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.65 % (2258064)CaDiCaL version: 2.1.3
% 26.65/4.65 % (2258064)Termination reason: Instruction limit
% 26.65/4.65 % (2258064)Termination phase: Saturation
% 26.65/4.65 % (2258064)Time elapsed: 0.045 s
% 26.65/4.65 % (2258064)Peak memory usage: 91 MB
% 26.65/4.65 % (2258064)Instructions burned: 136 (million)
% 26.65/4.65 % (2258066)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2124279707:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi)
% 26.65/4.65 % (2258066)Instruction limit reached!
% 26.65/4.65 % (2258066)------------------------------
% 26.65/4.65 % (2258066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.65 % (2258066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.65 % (2258066)CaDiCaL version: 2.1.3
% 26.65/4.65 % (2258066)Termination reason: Instruction limit
% 26.65/4.65 % (2258066)Termination phase: Saturation
% 26.65/4.65 % (2258066)Time elapsed: 0.046 s
% 26.65/4.65 % (2258066)Peak memory usage: 91 MB
% 26.65/4.65 % (2258066)Instructions burned: 143 (million)
% 26.65/4.65 % (2258041)Instruction limit reached!
% 26.65/4.65 % (2258041)------------------------------
% 26.65/4.65 % (2258041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.65 % (2258041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.65 % (2258041)CaDiCaL version: 2.1.3
% 26.65/4.65 % (2258041)Termination reason: Instruction limit
% 26.65/4.65 % (2258041)Termination phase: Saturation
% 26.65/4.65 % (2258041)Time elapsed: 1.448 s
% 26.65/4.65 % (2258041)Peak memory usage: 145 MB
% 26.65/4.65 % (2258041)Instructions burned: 2351 (million)
% 26.65/4.65 % (2258068)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2792894127:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi)
% 26.65/4.65 % (2258069)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3275981682:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi)
% 26.65/4.65 % (2258068)Instruction limit reached!
% 26.65/4.65 % (2258068)------------------------------
% 26.65/4.65 % (2258068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.65 % (2258068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.65 % (2258068)CaDiCaL version: 2.1.3
% 26.65/4.65 % (2258068)Termination reason: Instruction limit
% 26.65/4.65 % (2258068)Termination phase: Saturation
% 26.65/4.65 % (2258068)Time elapsed: 0.138 s
% 26.65/4.65 % (2258068)Peak memory usage: 94 MB
% 26.65/4.65 % (2258068)Instructions burned: 433 (million)
% 26.65/4.65 % (2258072)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2087964339:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2976 on theBenchmark for (2976ds/150Mi)
% 26.65/4.65 % (2258072)Instruction limit reached!
% 26.65/4.65 % (2258072)------------------------------
% 26.65/4.65 % (2258072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.65 % (2258072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.65 % (2258072)CaDiCaL version: 2.1.3
% 26.65/4.65 % (2258072)Termination reason: Instruction limit
% 26.65/4.65 % (2258072)Termination phase: Saturation
% 26.65/4.65 % (2258072)Time elapsed: 0.049 s
% 26.65/4.65 % (2258072)Peak memory usage: 92 MB
% 26.65/4.65 % (2258072)Instructions burned: 152 (million)
% 26.65/4.65 % (2258074)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=957345978:i=14155:bd=all_2974 on theBenchmark for (2974ds/14155Mi)
% 26.65/4.65 % (2258074)First to succeed.
% 26.65/4.65 % (2258074)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2258013"
% 26.65/4.65 % (2258074)Refutation found. Thanks to Tanya!
% 26.65/4.65 % SZS status Theorem for theBenchmark
% 26.65/4.65 % SZS output start Proof for theBenchmark
% See solution above
% 27.18/4.84 % (2258074)------------------------------
% 27.18/4.84 % (2258074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.18/4.84 % (2258074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.18/4.84 % (2258074)CaDiCaL version: 2.1.3
% 27.18/4.84 % (2258074)Termination reason: Refutation
% 27.18/4.84 % (2258074)Time elapsed: 0.813 s
% 27.18/4.84 % (2258074)Peak memory usage: 140 MB
% 27.18/4.84 % (2258074)Instructions burned: 1304 (million)
% 27.18/4.84 % (2258074)------------------------------
% 27.18/4.84 % (2258074)------------------------------
% 27.18/4.84 % (2258013)Success in time 3.765 s
% 27.18/4.84 % Vampire exiting
%------------------------------------------------------------------------------