%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR081+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:42:44 AM UTC 2026
% Result : Theorem 2.16s 1.89s
% Output : Refutation 5.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 20
% Syntax : Number of formulae : 99 ( 28 unt; 5 def)
% Number of atoms : 291 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 358 ( 166 ~; 160 |; 14 &)
% ( 5 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 6 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 8 con; 0-0 aty)
% Number of variables : 77 ( 0 sgn 77 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_26) ).
fof(f27,axiom,
! [X0,X1,X2] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__instance(X2,X0) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_27) ).
fof(f65,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( s__mother(X0,X1)
=> s__parent(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_65) ).
fof(f1313,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( s__sibling(X0,X1)
=> s__sibling(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_1316) ).
fof(f7724,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( s__mother(X1,X0)
=> s__attribute(X0,s__Female) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_7806) ).
fof(f7749,axiom,
! [X0,X1,X2] :
( ( s__instance(X2,s__Organism)
& s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( ( s__sibling(X0,X1)
& s__parent(X0,X2) )
=> s__parent(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_7831) ).
fof(f7751,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( ( s__parent(X0,X1)
& s__attribute(X1,s__Female) )
=> s__mother(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_7833) ).
fof(f24362,axiom,
s__subclass(s__Woman,s__Organism),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_7614) ).
fof(f35351,axiom,
s__subclass(s__Man,s__Organism),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_18603) ).
fof(f37982,axiom,
s__instance(s__Bill7_1,s__Man),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_1) ).
fof(f37983,axiom,
s__instance(s__Jane7_1,s__Woman),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_2) ).
fof(f37984,axiom,
s__instance(s__Bob7_1,s__Man),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_3) ).
fof(f37985,axiom,
s__mother(s__Bill7_1,s__Jane7_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_4) ).
fof(f37986,axiom,
s__sibling(s__Bob7_1,s__Bill7_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_5) ).
fof(f37987,conjecture,
( s__mother(s__Bill7_1,s__Jane7_1)
& s__mother(s__Bob7_1,s__Jane7_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_SUMO_MILO) ).
fof(f37988,negated_conjecture,
~ ( s__mother(s__Bill7_1,s__Jane7_1)
& s__mother(s__Bob7_1,s__Jane7_1) ),
inference(negated_conjecture,[status(cth)],[f37987]) ).
fof(f38010,plain,
( ~ s__mother(s__Bill7_1,s__Jane7_1)
| ~ s__mother(s__Bob7_1,s__Jane7_1) ),
inference(ennf_transformation,[],[f37988]) ).
fof(f38011,plain,
! [X0,X1] :
( s__mother(X0,X1)
| ~ s__parent(X0,X1)
| ~ s__attribute(X1,s__Female)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f7751]) ).
fof(f38012,plain,
! [X0,X1] :
( s__mother(X0,X1)
| ~ s__parent(X0,X1)
| ~ s__attribute(X1,s__Female)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f38011]) ).
fof(f38013,plain,
! [X0,X1] :
( s__attribute(X0,s__Female)
| ~ s__mother(X1,X0)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f7724]) ).
fof(f38014,plain,
! [X0,X1] :
( s__attribute(X0,s__Female)
| ~ s__mother(X1,X0)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f38013]) ).
fof(f38023,plain,
! [X0,X1] :
( s__parent(X0,X1)
| ~ s__mother(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f65]) ).
fof(f38024,plain,
! [X0,X1] :
( s__parent(X0,X1)
| ~ s__mother(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f38023]) ).
fof(f38072,plain,
! [X0,X1,X2] :
( s__parent(X1,X2)
| ~ s__sibling(X0,X1)
| ~ s__parent(X0,X2)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f7749]) ).
fof(f38073,plain,
! [X0,X1,X2] :
( s__parent(X1,X2)
| ~ s__sibling(X0,X1)
| ~ s__parent(X0,X2)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f38072]) ).
fof(f38082,plain,
! [X0,X1] :
( s__sibling(X1,X0)
| ~ s__sibling(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f1313]) ).
fof(f38083,plain,
! [X0,X1] :
( s__sibling(X1,X0)
| ~ s__sibling(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f38082]) ).
fof(f38090,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f27]) ).
fof(f38091,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f38090]) ).
fof(f38092,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f38112,plain,
( ~ s__mother(s__Bill7_1,s__Jane7_1)
| ~ s__mother(s__Bob7_1,s__Jane7_1) ),
inference(cnf_transformation,[],[f38010]) ).
fof(f38113,plain,
! [X0,X1] :
( ~ s__attribute(X1,s__Female)
| ~ s__parent(X0,X1)
| s__mother(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f38012]) ).
fof(f38114,plain,
! [X0,X1] :
( ~ s__mother(X1,X0)
| s__attribute(X0,s__Female)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f38014]) ).
fof(f38119,plain,
! [X0,X1] :
( ~ s__mother(X0,X1)
| s__parent(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f38024]) ).
fof(f38120,plain,
s__sibling(s__Bob7_1,s__Bill7_1),
inference(cnf_transformation,[],[f37986]) ).
fof(f38121,plain,
s__mother(s__Bill7_1,s__Jane7_1),
inference(cnf_transformation,[],[f37985]) ).
fof(f38122,plain,
s__instance(s__Bill7_1,s__Man),
inference(cnf_transformation,[],[f37982]) ).
fof(f38123,plain,
s__instance(s__Jane7_1,s__Woman),
inference(cnf_transformation,[],[f37983]) ).
fof(f38124,plain,
s__instance(s__Bob7_1,s__Man),
inference(cnf_transformation,[],[f37984]) ).
fof(f38169,plain,
! [X2,X0,X1] :
( ~ s__parent(X0,X2)
| ~ s__sibling(X0,X1)
| s__parent(X1,X2)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f38073]) ).
fof(f38174,plain,
! [X0,X1] :
( ~ s__sibling(X0,X1)
| s__sibling(X1,X0)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f38083]) ).
fof(f38180,plain,
s__subclass(s__Man,s__Organism),
inference(cnf_transformation,[],[f35351]) ).
fof(f38192,plain,
s__subclass(s__Woman,s__Organism),
inference(cnf_transformation,[],[f24362]) ).
fof(f38227,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f38091]) ).
fof(f38228,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f38092]) ).
fof(f38229,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f38092]) ).
fof(f38312,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f38227,f38228]) ).
fof(f38319,plain,
~ s__mother(s__Bob7_1,s__Jane7_1),
inference(forward_subsumption_resolution,[],[f38112,f38121]) ).
fof(f38320,plain,
! [X2,X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X2,X1)
| ~ s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f38312,f38229]) ).
fof(f38552,plain,
! [X0] :
( ~ s__instance(X0,s__Woman)
| s__instance(X0,s__Organism) ),
inference(resolution,[],[f38320,f38192]) ).
fof(f38564,plain,
! [X0] :
( ~ s__instance(X0,s__Man)
| s__instance(X0,s__Organism) ),
inference(resolution,[],[f38320,f38180]) ).
fof(f39905,plain,
( s__attribute(s__Jane7_1,s__Female)
| ~ s__instance(s__Bill7_1,s__Organism)
| ~ s__instance(s__Jane7_1,s__Organism) ),
inference(resolution,[],[f38114,f38121]) ).
fof(f39907,definition,
( spl2_209
<=> s__instance(s__Jane7_1,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_209])],[avatar_definition]) ).
fof(f39908,plain,
( s__instance(s__Jane7_1,s__Organism)
| ~ spl2_209 ),
inference(avatar_component_clause,[],[f39907]) ).
fof(f39909,plain,
( ~ s__instance(s__Jane7_1,s__Organism)
| spl2_209 ),
inference(avatar_component_clause,[],[f39907]) ).
fof(f39911,definition,
( spl2_210
<=> s__instance(s__Bill7_1,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_210])],[avatar_definition]) ).
fof(f39912,plain,
( s__instance(s__Bill7_1,s__Organism)
| ~ spl2_210 ),
inference(avatar_component_clause,[],[f39911]) ).
fof(f39913,plain,
( ~ s__instance(s__Bill7_1,s__Organism)
| spl2_210 ),
inference(avatar_component_clause,[],[f39911]) ).
fof(f39915,definition,
( spl2_211
<=> s__attribute(s__Jane7_1,s__Female) ),
introduced(definition,[new_symbols(definition,[spl2_211])],[avatar_definition]) ).
fof(f39917,plain,
( s__attribute(s__Jane7_1,s__Female)
| ~ spl2_211 ),
inference(avatar_component_clause,[],[f39915]) ).
fof(f39918,plain,
( ~ spl2_209
| ~ spl2_210
| spl2_211 ),
inference(avatar_split_clause,[],[f39905,f39915,f39911,f39907]) ).
fof(f39920,plain,
( s__parent(s__Bill7_1,s__Jane7_1)
| ~ s__instance(s__Jane7_1,s__Organism)
| ~ s__instance(s__Bill7_1,s__Organism) ),
inference(resolution,[],[f38119,f38121]) ).
fof(f39943,plain,
( s__sibling(s__Bill7_1,s__Bob7_1)
| ~ s__instance(s__Bill7_1,s__Organism)
| ~ s__instance(s__Bob7_1,s__Organism) ),
inference(resolution,[],[f38174,f38120]) ).
fof(f39945,definition,
( spl2_212
<=> s__instance(s__Bob7_1,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_212])],[avatar_definition]) ).
fof(f39946,plain,
( s__instance(s__Bob7_1,s__Organism)
| ~ spl2_212 ),
inference(avatar_component_clause,[],[f39945]) ).
fof(f39949,definition,
( spl2_213
<=> s__sibling(s__Bill7_1,s__Bob7_1) ),
introduced(definition,[new_symbols(definition,[spl2_213])],[avatar_definition]) ).
fof(f39951,plain,
( s__sibling(s__Bill7_1,s__Bob7_1)
| ~ spl2_213 ),
inference(avatar_component_clause,[],[f39949]) ).
fof(f39952,plain,
( ~ spl2_212
| ~ spl2_210
| spl2_213 ),
inference(avatar_split_clause,[],[f39943,f39949,f39911,f39945]) ).
fof(f40081,plain,
s__instance(s__Jane7_1,s__Organism),
inference(resolution,[],[f38552,f38123]) ).
fof(f40082,plain,
( $false
| spl2_209 ),
inference(forward_subsumption_resolution,[],[f40081,f39909]) ).
fof(f40083,plain,
spl2_209,
inference(avatar_contradiction_clause,[],[f40082]) ).
fof(f40161,plain,
s__instance(s__Bill7_1,s__Organism),
inference(resolution,[],[f38564,f38122]) ).
fof(f40162,plain,
s__instance(s__Bob7_1,s__Organism),
inference(resolution,[],[f38564,f38124]) ).
fof(f40163,plain,
spl2_212,
inference(avatar_split_clause,[],[f40162,f39945]) ).
fof(f40164,plain,
( $false
| spl2_210 ),
inference(forward_subsumption_resolution,[],[f40161,f39913]) ).
fof(f40165,plain,
spl2_210,
inference(avatar_contradiction_clause,[],[f40164]) ).
fof(f40168,plain,
( s__parent(s__Bill7_1,s__Jane7_1)
| ~ s__instance(s__Bill7_1,s__Organism)
| ~ spl2_209 ),
inference(forward_subsumption_resolution,[],[f39920,f39908]) ).
fof(f40173,plain,
( s__parent(s__Bill7_1,s__Jane7_1)
| ~ spl2_209
| ~ spl2_210 ),
inference(forward_subsumption_resolution,[],[f40168,f39912]) ).
fof(f40177,plain,
( ! [X0] :
( ~ s__parent(X0,s__Jane7_1)
| s__mother(X0,s__Jane7_1)
| ~ s__instance(s__Jane7_1,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_211 ),
inference(resolution,[],[f39917,f38113]) ).
fof(f40183,plain,
( ! [X0] :
( ~ s__parent(X0,s__Jane7_1)
| s__mother(X0,s__Jane7_1)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_209
| ~ spl2_211 ),
inference(forward_subsumption_resolution,[],[f40177,f39908]) ).
fof(f40219,plain,
( ! [X0] :
( ~ s__sibling(s__Bill7_1,X0)
| s__parent(X0,s__Jane7_1)
| ~ s__instance(s__Jane7_1,s__Organism)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Bill7_1,s__Organism) )
| ~ spl2_209
| ~ spl2_210 ),
inference(resolution,[],[f40173,f38169]) ).
fof(f40226,plain,
( ! [X0] :
( ~ s__sibling(s__Bill7_1,X0)
| s__parent(X0,s__Jane7_1)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Bill7_1,s__Organism) )
| ~ spl2_209
| ~ spl2_210 ),
inference(forward_subsumption_resolution,[],[f40219,f39908]) ).
fof(f40232,plain,
( ! [X0] :
( ~ s__sibling(s__Bill7_1,X0)
| s__parent(X0,s__Jane7_1)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_209
| ~ spl2_210 ),
inference(forward_subsumption_resolution,[],[f40226,f39912]) ).
fof(f42935,plain,
( s__parent(s__Bob7_1,s__Jane7_1)
| ~ s__instance(s__Bob7_1,s__Organism)
| ~ spl2_209
| ~ spl2_210
| ~ spl2_213 ),
inference(resolution,[],[f40232,f39951]) ).
fof(f42936,plain,
( s__parent(s__Bob7_1,s__Jane7_1)
| ~ spl2_209
| ~ spl2_210
| ~ spl2_212
| ~ spl2_213 ),
inference(forward_subsumption_resolution,[],[f42935,f39946]) ).
fof(f42951,plain,
( s__mother(s__Bob7_1,s__Jane7_1)
| ~ s__instance(s__Bob7_1,s__Organism)
| ~ spl2_209
| ~ spl2_210
| ~ spl2_211
| ~ spl2_212
| ~ spl2_213 ),
inference(resolution,[],[f42936,f40183]) ).
fof(f42966,plain,
( ~ s__instance(s__Bob7_1,s__Organism)
| ~ spl2_209
| ~ spl2_210
| ~ spl2_211
| ~ spl2_212
| ~ spl2_213 ),
inference(forward_subsumption_resolution,[],[f42951,f38319]) ).
fof(f42975,plain,
( $false
| ~ spl2_209
| ~ spl2_210
| ~ spl2_211
| ~ spl2_212
| ~ spl2_213 ),
inference(forward_subsumption_resolution,[],[f42966,f39946]) ).
fof(f42976,plain,
( ~ spl2_209
| ~ spl2_210
| ~ spl2_211
| ~ spl2_212
| ~ spl2_213 ),
inference(avatar_contradiction_clause,[],[f42975]) ).
cnf(s105,plain,
( ~ spl2_209
| ~ spl2_210
| spl2_211 ),
inference(sat_conversion,[],[f39918]) ).
cnf(s106,plain,
( ~ spl2_210
| ~ spl2_212
| spl2_213 ),
inference(sat_conversion,[],[f39952]) ).
cnf(s107,plain,
spl2_209,
inference(sat_conversion,[],[f40083]) ).
cnf(s108,plain,
spl2_212,
inference(sat_conversion,[],[f40163]) ).
cnf(s109,plain,
spl2_210,
inference(sat_conversion,[],[f40165]) ).
cnf(s122,plain,
( ~ spl2_209
| ~ spl2_210
| ~ spl2_211
| ~ spl2_212
| ~ spl2_213 ),
inference(sat_conversion,[],[f42976]) ).
cnf(s126,plain,
spl2_213,
inference(rat,[],[s106,s108,s109]) ).
cnf(s127,plain,
~ spl2_211,
inference(rat,[],[s122,s107,s108,s109,s126]) ).
cnf(s128,plain,
$false,
inference(rat,[],[s105,s127,s109,s107]) ).
fof(f42986,plain,
$false,
inference(avatar_sat_refutation,[],[s128]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR081+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n014.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 22:31:30 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 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
% 2.16/1.89 % (2259578)Detected formulas, will run a generic FOF schedule.
% 2.16/1.89 % (2259587)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1009675934:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 2.16/1.89 % (2259585)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=1688541004:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 2.16/1.89 % (2259584)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=3233535173:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 2.16/1.89 % (2259586)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2574911767:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 2.16/1.89 % (2259588)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1673749476:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 2.16/1.89 % (2259589)dis-21_1_sil=8000:lcm=predicate:random_seed=33971381:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2993 on theBenchmark for (2993ds/129Mi)
% 2.16/1.89 % (2259583)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=3184594239:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 2.16/1.89 % (2259587)Instruction limit reached!
% 2.16/1.89 % (2259587)------------------------------
% 2.16/1.89 % (2259587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.16/1.89 % (2259587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.16/1.89 % (2259587)CaDiCaL version: 2.1.3
% 2.16/1.89 % (2259587)Termination reason: Instruction limit
% 2.16/1.89 % (2259587)Termination phase: Saturation
% 2.16/1.89 % (2259587)Time elapsed: 0.048 s
% 2.16/1.89 % (2259587)Peak memory usage: 108 MB
% 2.16/1.89 % (2259587)Instructions burned: 122 (million)
% 2.16/1.89 % (2259586)Refutation not found, incomplete strategy
% 2.16/1.89 % (2259586)------------------------------
% 2.16/1.89 % (2259586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.16/1.89 % (2259586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.16/1.89 % (2259586)CaDiCaL version: 2.1.3
% 2.16/1.89 % (2259586)Termination reason: Refutation not found, incomplete strategy
% 2.16/1.89 % (2259586)Time elapsed: 0.061 s
% 2.16/1.89 % (2259586)Peak memory usage: 108 MB
% 2.16/1.89 % (2259586)Instructions burned: 98 (million)
% 2.16/1.89 % (2259588)Instruction limit reached!
% 2.16/1.89 % (2259588)------------------------------
% 2.16/1.89 % (2259588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.16/1.89 % (2259588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.16/1.89 % (2259588)CaDiCaL version: 2.1.3
% 2.16/1.89 % (2259588)Termination reason: Instruction limit
% 2.16/1.89 % (2259588)Termination phase: Property scanning
% 2.16/1.89 % (2259588)Time elapsed: 0.062 s
% 2.16/1.89 % (2259588)Peak memory usage: 104 MB
% 2.16/1.89 % (2259588)Instructions burned: 139 (million)
% 2.16/1.89 % (2259589)Instruction limit reached!
% 2.16/1.89 % (2259589)------------------------------
% 2.16/1.89 % (2259589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.16/1.89 % (2259589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.16/1.89 % (2259589)CaDiCaL version: 2.1.3
% 2.16/1.89 % (2259589)Termination reason: Instruction limit
% 2.16/1.89 % (2259589)Termination phase: Preprocessing 1
% 2.16/1.89 % (2259589)Time elapsed: 0.080 s
% 2.16/1.89 % (2259589)Peak memory usage: 105 MB
% 2.16/1.89 % (2259589)Instructions burned: 129 (million)
% 2.16/1.89 % (2259597)lrs+10_1_sil=8000:sp=occurrence:random_seed=3065088903:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 2.16/1.89 % (2259598)lrs+10_1_sil=32000:urr=on:br=off:random_seed=5206527:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 2.16/1.89 % (2259597)First to succeed.
% 2.16/1.89 % (2259597)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2259578"
% 2.16/1.89 % (2259599)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2661427064:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 2.16/1.89 % (2259598)Instruction limit reached!
% 2.16/1.89 % (2259598)------------------------------
% 2.16/1.89 % (2259598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.16/1.89 % (2259598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.16/1.89 % (2259598)CaDiCaL version: 2.1.3
% 2.16/1.89 % (2259598)Termination reason: Instruction limit
% 2.16/1.89 % (2259598)Termination phase: SInE selection
% 2.16/1.89 % (2259598)Time elapsed: 0.069 s
% 2.16/1.89 % (2259598)Peak memory usage: 104 MB
% 2.16/1.89 % (2259598)Instructions burned: 157 (million)
% 2.16/1.89 % (2259586)------------------------------
% 2.16/1.89 % (2259586)------------------------------
% 2.16/1.89 % (2259599)Refutation not found, incomplete strategy
% 2.16/1.89 % (2259599)------------------------------
% 2.16/1.89 % (2259599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.16/1.89 % (2259599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.16/1.89 % (2259599)CaDiCaL version: 2.1.3
% 2.16/1.89 % (2259599)Termination reason: Refutation not found, incomplete strategy
% 2.16/1.89 % (2259599)Time elapsed: 0.074 s
% 2.16/1.89 % (2259599)Peak memory usage: 109 MB
% 2.16/1.89 % (2259599)Instructions burned: 109 (million)
% 2.16/1.89 % (2259597)Refutation found. Thanks to Tanya!
% 2.16/1.89 % SZS status Theorem for theBenchmark
% 2.16/1.89 % SZS output start Proof for theBenchmark
% See solution above
% 5.30/2.10 % (2259597)------------------------------
% 5.30/2.10 % (2259597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.30/2.10 % (2259597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/2.10 % (2259597)CaDiCaL version: 2.1.3
% 5.30/2.10 % (2259597)Termination reason: Refutation
% 5.30/2.10 % (2259597)Time elapsed: 0.078 s
% 5.30/2.10 % (2259597)Peak memory usage: 111 MB
% 5.30/2.10 % (2259597)Instructions burned: 213 (million)
% 5.30/2.10 % (2259597)------------------------------
% 5.30/2.10 % (2259597)------------------------------
% 5.30/2.10 % (2259578)Success in time 1.238 s
% 5.30/2.10 % Vampire exiting
%------------------------------------------------------------------------------