%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR076+6 : 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 : n007.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:40 AM UTC 2026
% Result : Theorem 56.60s 15.92s
% Output : Refutation 0.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 19
% Syntax : Number of formulae : 101 ( 31 unt; 0 def)
% Number of atoms : 367 ( 0 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 562 ( 296 ~; 245 |; 10 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 14 con; 0-0 aty)
% Number of variables : 126 ( 126 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26456,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_26635) ).
fof(f26457,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_26636) ).
fof(f26626,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Attribute)
& s__instance(X0,s__Object) )
=> ( s__attribute(X0,X1)
=> s__property(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_26805) ).
fof(f27412,axiom,
s__subclass(s__Agent,s__Object),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_27592) ).
fof(f27469,axiom,
s__subclass(s__InternalAttribute,s__Attribute),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_27651) ).
fof(f34802,axiom,
s__subclass(s__Organism,s__Agent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_35054) ).
fof(f35470,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_35731) ).
fof(f35476,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( s__father(X1,X0)
=> s__attribute(X0,s__Male) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_35737) ).
fof(f36065,axiom,
s__subclass(s__BiologicalAttribute,s__InternalAttribute),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_36330) ).
fof(f36090,axiom,
s__subclass(s__SexAttribute,s__BiologicalAttribute),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_36356) ).
fof(f36093,axiom,
s__instance(s__Female,s__SexAttribute),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_36359) ).
fof(f36096,axiom,
s__instance(s__Male,s__SexAttribute),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_36362) ).
fof(f36098,axiom,
s__contraryAttribute_2(s__Male,s__Female),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_36364) ).
fof(f55589,axiom,
! [X0,X1,X2] :
( ( s__instance(X0,s__Attribute)
& s__instance(X1,s__Attribute) )
=> ( ( s__contraryAttribute_2(X0,X1)
& s__property(X2,X0)
& s__property(X2,X1) )
=> s__property(s__TheKB2_1,s__Inconsistent) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_3) ).
fof(f55590,axiom,
s__instance(s__Entity2_1,s__Organism),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_4) ).
fof(f55591,axiom,
s__instance(s__Entity2_2,s__Organism),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_5) ).
fof(f55592,axiom,
s__mother(s__Entity2_1,s__Entity2_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_6) ).
fof(f55593,axiom,
s__father(s__Entity2_1,s__Entity2_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_7) ).
fof(f55594,conjecture,
s__property(s__TheKB2_1,s__Inconsistent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_ALL) ).
fof(f55595,negated_conjecture,
~ s__property(s__TheKB2_1,s__Inconsistent),
inference(negated_conjecture,[status(cth)],[f55594]) ).
fof(f55596,plain,
~ s__property(s__TheKB2_1,s__Inconsistent),
inference(flattening,[],[f55595]) ).
fof(f60001,plain,
! [X0,X1,X2] :
( s__property(s__TheKB2_1,s__Inconsistent)
| ~ s__contraryAttribute_2(X0,X1)
| ~ s__property(X2,X0)
| ~ s__property(X2,X1)
| ~ s__instance(X0,s__Attribute)
| ~ s__instance(X1,s__Attribute) ),
inference(ennf_transformation,[],[f55589]) ).
fof(f60002,plain,
! [X0,X1,X2] :
( s__property(s__TheKB2_1,s__Inconsistent)
| ~ s__contraryAttribute_2(X0,X1)
| ~ s__property(X2,X0)
| ~ s__property(X2,X1)
| ~ s__instance(X0,s__Attribute)
| ~ s__instance(X1,s__Attribute) ),
inference(flattening,[],[f60001]) ).
fof(f60013,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,[],[f26457]) ).
fof(f60014,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,[],[f60013]) ).
fof(f60015,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26456]) ).
fof(f60046,plain,
! [X0,X1] :
( s__property(X0,X1)
| ~ s__attribute(X0,X1)
| ~ s__instance(X1,s__Attribute)
| ~ s__instance(X0,s__Object) ),
inference(ennf_transformation,[],[f26626]) ).
fof(f60047,plain,
! [X0,X1] :
( s__property(X0,X1)
| ~ s__attribute(X0,X1)
| ~ s__instance(X1,s__Attribute)
| ~ s__instance(X0,s__Object) ),
inference(flattening,[],[f60046]) ).
fof(f60106,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,[],[f35470]) ).
fof(f60107,plain,
! [X0,X1] :
( s__attribute(X0,s__Female)
| ~ s__mother(X1,X0)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f60106]) ).
fof(f60124,plain,
! [X0,X1] :
( s__attribute(X0,s__Male)
| ~ s__father(X1,X0)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f35476]) ).
fof(f60125,plain,
! [X0,X1] :
( s__attribute(X0,s__Male)
| ~ s__father(X1,X0)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f60124]) ).
fof(f66233,plain,
! [X2,X0,X1] :
( s__property(s__TheKB2_1,s__Inconsistent)
| ~ s__contraryAttribute_2(X0,X1)
| ~ s__property(X2,X0)
| ~ s__property(X2,X1)
| ~ s__instance(X0,s__Attribute)
| ~ s__instance(X1,s__Attribute) ),
inference(cnf_transformation,[],[f60002]) ).
fof(f66234,plain,
s__instance(s__Entity2_1,s__Organism),
inference(cnf_transformation,[],[f55590]) ).
fof(f66235,plain,
s__instance(s__Entity2_2,s__Organism),
inference(cnf_transformation,[],[f55591]) ).
fof(f66236,plain,
s__mother(s__Entity2_1,s__Entity2_2),
inference(cnf_transformation,[],[f55592]) ).
fof(f66237,plain,
s__father(s__Entity2_1,s__Entity2_2),
inference(cnf_transformation,[],[f55593]) ).
fof(f66238,plain,
~ s__property(s__TheKB2_1,s__Inconsistent),
inference(cnf_transformation,[],[f55596]) ).
fof(f66247,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,[],[f60014]) ).
fof(f66248,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f60015]) ).
fof(f66249,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f60015]) ).
fof(f66269,plain,
! [X0,X1] :
( s__property(X0,X1)
| ~ s__attribute(X0,X1)
| ~ s__instance(X1,s__Attribute)
| ~ s__instance(X0,s__Object) ),
inference(cnf_transformation,[],[f60047]) ).
fof(f66297,plain,
s__subclass(s__Organism,s__Agent),
inference(cnf_transformation,[],[f34802]) ).
fof(f66328,plain,
! [X0,X1] :
( s__attribute(X0,s__Female)
| ~ s__mother(X1,X0)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f60107]) ).
fof(f66342,plain,
! [X0,X1] :
( s__attribute(X0,s__Male)
| ~ s__father(X1,X0)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f60125]) ).
fof(f66346,plain,
s__subclass(s__Agent,s__Object),
inference(cnf_transformation,[],[f27412]) ).
fof(f66893,plain,
s__contraryAttribute_2(s__Male,s__Female),
inference(cnf_transformation,[],[f36098]) ).
fof(f66895,plain,
s__instance(s__Female,s__SexAttribute),
inference(cnf_transformation,[],[f36093]) ).
fof(f66959,plain,
s__instance(s__Male,s__SexAttribute),
inference(cnf_transformation,[],[f36096]) ).
fof(f67058,plain,
s__subclass(s__BiologicalAttribute,s__InternalAttribute),
inference(cnf_transformation,[],[f36065]) ).
fof(f67063,plain,
s__subclass(s__InternalAttribute,s__Attribute),
inference(cnf_transformation,[],[f27469]) ).
fof(f68822,plain,
s__subclass(s__SexAttribute,s__BiologicalAttribute),
inference(cnf_transformation,[],[f36090]) ).
fof(f75722,plain,
! [X2,X0,X1] :
( ~ s__property(X2,X0)
| ~ s__contraryAttribute_2(X0,X1)
| ~ s__property(X2,X1)
| ~ s__instance(X0,s__Attribute)
| ~ s__instance(X1,s__Attribute) ),
inference(resolution,[],[f66238,f66233]) ).
fof(f75769,plain,
! [X2,X0,X1] :
( ~ s__contraryAttribute_2(X0,X1)
| ~ s__property(X2,X1)
| ~ s__instance(X0,s__Attribute)
| ~ s__instance(X1,s__Attribute)
| ~ s__attribute(X2,X0)
| ~ s__instance(X0,s__Attribute)
| ~ s__instance(X2,s__Object) ),
inference(resolution,[],[f75722,f66269]) ).
fof(f75776,plain,
! [X2,X0,X1] :
( ~ s__property(X2,X1)
| ~ s__contraryAttribute_2(X0,X1)
| ~ s__instance(X0,s__Attribute)
| ~ s__instance(X1,s__Attribute)
| ~ s__attribute(X2,X0)
| ~ s__instance(X2,s__Object) ),
inference(duplicate_literal_removal,[],[f75769]) ).
fof(f76010,plain,
! [X2,X0,X1] :
( ~ s__contraryAttribute_2(X0,X1)
| ~ s__instance(X0,s__Attribute)
| ~ s__instance(X1,s__Attribute)
| ~ s__attribute(X2,X0)
| ~ s__instance(X2,s__Object)
| ~ s__attribute(X2,X1)
| ~ s__instance(X1,s__Attribute)
| ~ s__instance(X2,s__Object) ),
inference(resolution,[],[f75776,f66269]) ).
fof(f76017,plain,
! [X2,X0,X1] :
( ~ s__contraryAttribute_2(X0,X1)
| ~ s__instance(X0,s__Attribute)
| ~ s__instance(X1,s__Attribute)
| ~ s__attribute(X2,X0)
| ~ s__instance(X2,s__Object)
| ~ s__attribute(X2,X1) ),
inference(duplicate_literal_removal,[],[f76010]) ).
fof(f76060,plain,
! [X0] :
( ~ s__instance(s__Female,s__Attribute)
| ~ s__instance(s__Male,s__Attribute)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female) ),
inference(resolution,[],[f76017,f66893]) ).
fof(f76119,plain,
! [X0,X1] :
( ~ s__instance(s__Male,s__Attribute)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__subclass(X1,s__Attribute)
| ~ s__instance(s__Female,X1)
| ~ s__instance(s__Attribute,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass) ),
inference(resolution,[],[f76060,f66247]) ).
fof(f76136,plain,
! [X0,X1] :
( ~ s__instance(s__Male,s__Attribute)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__subclass(X1,s__Attribute)
| ~ s__instance(s__Female,X1)
| ~ s__instance(s__Attribute,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f76119,f66249]) ).
fof(f76139,plain,
! [X0,X1] :
( ~ s__subclass(X1,s__Attribute)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__instance(s__Male,s__Attribute)
| ~ s__instance(s__Female,X1) ),
inference(forward_subsumption_resolution,[],[f76136,f66248]) ).
fof(f76743,plain,
! [X0] :
( ~ s__instance(s__Female,s__InternalAttribute)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__instance(s__Male,s__Attribute)
| ~ s__attribute(X0,s__Male) ),
inference(resolution,[],[f76139,f67063]) ).
fof(f76773,plain,
! [X0,X1] :
( ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__instance(s__Male,s__Attribute)
| ~ s__attribute(X0,s__Male)
| ~ s__subclass(X1,s__InternalAttribute)
| ~ s__instance(s__Female,X1)
| ~ s__instance(s__InternalAttribute,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass) ),
inference(resolution,[],[f76743,f66247]) ).
fof(f76789,plain,
! [X0,X1] :
( ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__instance(s__Male,s__Attribute)
| ~ s__attribute(X0,s__Male)
| ~ s__subclass(X1,s__InternalAttribute)
| ~ s__instance(s__Female,X1)
| ~ s__instance(s__InternalAttribute,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f76773,f66249]) ).
fof(f76790,plain,
! [X0,X1] :
( ~ s__subclass(X1,s__InternalAttribute)
| ~ s__attribute(X0,s__Female)
| ~ s__instance(s__Male,s__Attribute)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__instance(s__Female,X1) ),
inference(forward_subsumption_resolution,[],[f76789,f66248]) ).
fof(f76900,plain,
! [X0] :
( ~ s__instance(s__Female,s__BiologicalAttribute)
| ~ s__instance(s__Male,s__Attribute)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female) ),
inference(resolution,[],[f76790,f67058]) ).
fof(f77017,plain,
! [X0,X1] :
( ~ s__instance(s__Male,s__Attribute)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__subclass(X1,s__BiologicalAttribute)
| ~ s__instance(s__Female,X1)
| ~ s__instance(s__BiologicalAttribute,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass) ),
inference(resolution,[],[f76900,f66247]) ).
fof(f77033,plain,
! [X0,X1] :
( ~ s__instance(s__Male,s__Attribute)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__subclass(X1,s__BiologicalAttribute)
| ~ s__instance(s__Female,X1)
| ~ s__instance(s__BiologicalAttribute,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f77017,f66249]) ).
fof(f77034,plain,
! [X0,X1] :
( ~ s__subclass(X1,s__BiologicalAttribute)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__instance(s__Male,s__Attribute)
| ~ s__instance(s__Female,X1) ),
inference(forward_subsumption_resolution,[],[f77033,f66248]) ).
fof(f77313,plain,
! [X0] :
( ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__instance(s__Male,s__Attribute)
| ~ s__instance(s__Female,s__SexAttribute) ),
inference(resolution,[],[f77034,f68822]) ).
fof(f77317,plain,
! [X0] :
( ~ s__instance(s__Male,s__Attribute)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__attribute(X0,s__Male) ),
inference(forward_subsumption_resolution,[],[f77313,f66895]) ).
fof(f77334,plain,
! [X0,X1] :
( ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__attribute(X0,s__Male)
| ~ s__subclass(X1,s__Attribute)
| ~ s__instance(s__Male,X1)
| ~ s__instance(s__Attribute,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass) ),
inference(resolution,[],[f77317,f66247]) ).
fof(f77351,plain,
! [X0,X1] :
( ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__attribute(X0,s__Male)
| ~ s__subclass(X1,s__Attribute)
| ~ s__instance(s__Male,X1)
| ~ s__instance(s__Attribute,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f77334,f66249]) ).
fof(f77354,plain,
! [X0,X1] :
( ~ s__subclass(X1,s__Attribute)
| ~ s__attribute(X0,s__Female)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__instance(s__Male,X1) ),
inference(forward_subsumption_resolution,[],[f77351,f66248]) ).
fof(f77370,plain,
! [X0] :
( ~ s__instance(s__Male,s__InternalAttribute)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female) ),
inference(resolution,[],[f77354,f67063]) ).
fof(f77400,plain,
! [X0,X1] :
( ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__subclass(X1,s__InternalAttribute)
| ~ s__instance(s__Male,X1)
| ~ s__instance(s__InternalAttribute,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass) ),
inference(resolution,[],[f77370,f66247]) ).
fof(f77416,plain,
! [X0,X1] :
( ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__subclass(X1,s__InternalAttribute)
| ~ s__instance(s__Male,X1)
| ~ s__instance(s__InternalAttribute,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f77400,f66249]) ).
fof(f77417,plain,
! [X0,X1] :
( ~ s__subclass(X1,s__InternalAttribute)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(s__Male,X1) ),
inference(forward_subsumption_resolution,[],[f77416,f66248]) ).
fof(f77489,plain,
! [X0] :
( ~ s__instance(s__Male,s__BiologicalAttribute)
| ~ s__attribute(X0,s__Female)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object) ),
inference(resolution,[],[f77417,f67058]) ).
fof(f77606,plain,
! [X0,X1] :
( ~ s__attribute(X0,s__Female)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__subclass(X1,s__BiologicalAttribute)
| ~ s__instance(s__Male,X1)
| ~ s__instance(s__BiologicalAttribute,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass) ),
inference(resolution,[],[f77489,f66247]) ).
fof(f77622,plain,
! [X0,X1] :
( ~ s__attribute(X0,s__Female)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__subclass(X1,s__BiologicalAttribute)
| ~ s__instance(s__Male,X1)
| ~ s__instance(s__BiologicalAttribute,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f77606,f66249]) ).
fof(f77623,plain,
! [X0,X1] :
( ~ s__subclass(X1,s__BiologicalAttribute)
| ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__instance(s__Male,X1) ),
inference(forward_subsumption_resolution,[],[f77622,f66248]) ).
fof(f78871,plain,
! [X0] :
( ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female)
| ~ s__instance(s__Male,s__SexAttribute) ),
inference(resolution,[],[f77623,f68822]) ).
fof(f78875,plain,
! [X0] :
( ~ s__attribute(X0,s__Male)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Female) ),
inference(forward_subsumption_resolution,[],[f78871,f66959]) ).
fof(f78883,plain,
! [X0,X1] :
( ~ s__father(X1,X0)
| ~ s__attribute(X0,s__Female)
| ~ s__instance(X0,s__Object)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f78875,f66342]) ).
fof(f81716,plain,
( ~ s__attribute(s__Entity2_2,s__Female)
| ~ s__instance(s__Entity2_2,s__Object)
| ~ s__instance(s__Entity2_1,s__Organism)
| ~ s__instance(s__Entity2_2,s__Organism) ),
inference(resolution,[],[f78883,f66237]) ).
fof(f81736,plain,
( ~ s__attribute(s__Entity2_2,s__Female)
| ~ s__instance(s__Entity2_2,s__Object)
| ~ s__instance(s__Entity2_2,s__Organism) ),
inference(forward_subsumption_resolution,[],[f81716,f66234]) ).
fof(f81737,plain,
( ~ s__instance(s__Entity2_2,s__Object)
| ~ s__attribute(s__Entity2_2,s__Female) ),
inference(forward_subsumption_resolution,[],[f81736,f66235]) ).
fof(f81745,plain,
! [X0] :
( ~ s__attribute(s__Entity2_2,s__Female)
| ~ s__subclass(X0,s__Object)
| ~ s__instance(s__Entity2_2,X0)
| ~ s__instance(s__Object,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[],[f81737,f66247]) ).
fof(f81761,plain,
! [X0] :
( ~ s__attribute(s__Entity2_2,s__Female)
| ~ s__subclass(X0,s__Object)
| ~ s__instance(s__Entity2_2,X0)
| ~ s__instance(s__Object,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f81745,f66249]) ).
fof(f81763,plain,
! [X0] :
( ~ s__subclass(X0,s__Object)
| ~ s__attribute(s__Entity2_2,s__Female)
| ~ s__instance(s__Entity2_2,X0) ),
inference(forward_subsumption_resolution,[],[f81761,f66248]) ).
fof(f81832,plain,
( ~ s__attribute(s__Entity2_2,s__Female)
| ~ s__instance(s__Entity2_2,s__Agent) ),
inference(resolution,[],[f81763,f66346]) ).
fof(f81847,plain,
! [X0] :
( ~ s__instance(s__Entity2_2,s__Agent)
| ~ s__mother(X0,s__Entity2_2)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Entity2_2,s__Organism) ),
inference(resolution,[],[f81832,f66328]) ).
fof(f81883,plain,
! [X0] :
( ~ s__mother(X0,s__Entity2_2)
| ~ s__instance(s__Entity2_2,s__Agent)
| ~ s__instance(X0,s__Organism) ),
inference(forward_subsumption_resolution,[],[f81847,f66235]) ).
fof(f82149,plain,
( ~ s__instance(s__Entity2_2,s__Agent)
| ~ s__instance(s__Entity2_1,s__Organism) ),
inference(resolution,[],[f81883,f66236]) ).
fof(f82158,plain,
~ s__instance(s__Entity2_2,s__Agent),
inference(forward_subsumption_resolution,[],[f82149,f66234]) ).
fof(f82190,plain,
! [X0] :
( ~ s__subclass(X0,s__Agent)
| ~ s__instance(s__Entity2_2,X0)
| ~ s__instance(s__Agent,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[],[f82158,f66247]) ).
fof(f82205,plain,
! [X0] :
( ~ s__subclass(X0,s__Agent)
| ~ s__instance(s__Entity2_2,X0)
| ~ s__instance(s__Agent,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f82190,f66249]) ).
fof(f82207,plain,
! [X0] :
( ~ s__subclass(X0,s__Agent)
| ~ s__instance(s__Entity2_2,X0) ),
inference(forward_subsumption_resolution,[],[f82205,f66248]) ).
fof(f82346,plain,
~ s__instance(s__Entity2_2,s__Organism),
inference(resolution,[],[f82207,f66297]) ).
fof(f82352,plain,
$false,
inference(forward_subsumption_resolution,[],[f82346,f66235]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR076+6 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.29 % Computer : n007.cluster.edu
% 0.12/0.29 % Model : x86_64 x86_64
% 0.12/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.29 % Memory : 8046.5625MB
% 0.12/0.29 % OS : Linux 6.8.0-71-generic
% 0.12/0.29 % CPULimit : 300
% 0.12/0.29 % WCLimit : 300
% 0.12/0.29 % DateTime : Mon Sep 28 22:24:55 UTC 2026
% 0.12/0.30 % CPUTime :
% 0.12/0.30 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.31/0.36 Running first-order theorem proving
% 0.31/0.36 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
% 28.12/7.81 % (2927930)Detected formulas, will run a generic FOF schedule.
% 28.12/7.81 % (2927938)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3208392837:i=109:sd=1:ins=1:gsp=on:ss=axioms_2967 on theBenchmark for (2967ds/109Mi)
% 28.12/7.81 % (2927935)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=1516171678:i=141193_2967 on theBenchmark for (2967ds/141193Mi)
% 28.12/7.81 % (2927936)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=1496999597:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2967 on theBenchmark for (2967ds/134677Mi)
% 28.12/7.81 % (2927937)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=128895352:i=141695:sd=1:nm=32:gsp=on:ss=included_2967 on theBenchmark for (2967ds/141695Mi)
% 28.12/7.81 % (2927938)Instruction limit reached!
% 28.12/7.81 % (2927938)------------------------------
% 28.12/7.81 % (2927938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.12/7.81 % (2927938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.12/7.81 % (2927938)CaDiCaL version: 2.1.3
% 28.12/7.81 % (2927938)Termination reason: Instruction limit
% 28.12/7.81 % (2927938)Termination phase: SInE selection
% 28.12/7.81 % (2927938)Time elapsed: 0.067 s
% 28.12/7.81 % (2927938)Peak memory usage: 139 MB
% 28.12/7.81 % (2927938)Instructions burned: 110 (million)
% 28.12/7.81 % (2927939)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2747032949:i=119:av=off:ss=axioms_2967 on theBenchmark for (2967ds/119Mi)
% 28.12/7.81 % (2927941)dis-21_1_sil=8000:lcm=predicate:random_seed=2946380714:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2967 on theBenchmark for (2967ds/129Mi)
% 28.12/7.81 % (2927940)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1278534941:s2a=on:i=139:gtg=position_2967 on theBenchmark for (2967ds/139Mi)
% 28.12/7.81 % (2927939)Instruction limit reached!
% 28.12/7.81 % (2927939)------------------------------
% 28.12/7.81 % (2927939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.12/7.81 % (2927939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.12/7.81 % (2927939)CaDiCaL version: 2.1.3
% 28.12/7.81 % (2927939)Termination reason: Instruction limit
% 28.12/7.81 % (2927939)Termination phase: SInE selection
% 28.12/7.81 % (2927939)Time elapsed: 0.117 s
% 28.12/7.81 % (2927939)Peak memory usage: 139 MB
% 28.12/7.81 % (2927939)Instructions burned: 120 (million)
% 28.12/7.81 % (2927941)Instruction limit reached!
% 28.12/7.81 % (2927941)------------------------------
% 28.12/7.81 % (2927941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.12/7.81 % (2927941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.12/7.81 % (2927941)CaDiCaL version: 2.1.3
% 28.12/7.81 % (2927941)Termination reason: Instruction limit
% 28.12/7.81 % (2927941)Termination phase: SInE selection
% 28.12/7.81 % (2927941)Time elapsed: 0.123 s
% 28.12/7.81 % (2927941)Peak memory usage: 139 MB
% 28.12/7.81 % (2927941)Instructions burned: 130 (million)
% 28.12/7.81 % (2927940)Instruction limit reached!
% 28.12/7.81 % (2927940)------------------------------
% 28.12/7.81 % (2927940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.12/7.81 % (2927940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.12/7.81 % (2927940)CaDiCaL version: 2.1.3
% 28.12/7.81 % (2927940)Termination reason: Instruction limit
% 28.12/7.81 % (2927940)Termination phase: Property scanning
% 28.12/7.81 % (2927940)Time elapsed: 0.134 s
% 28.12/7.81 % (2927940)Peak memory usage: 137 MB
% 28.12/7.81 % (2927940)Instructions burned: 139 (million)
% 28.12/7.81 % (2927946)lrs+10_1_sil=8000:sp=occurrence:random_seed=513473597:i=285:sd=3:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/285Mi)
% 28.12/7.81 % (2927946)Refutation not found, incomplete strategy
% 28.12/7.81 % (2927946)------------------------------
% 28.12/7.81 % (2927946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.12/7.81 % (2927946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.12/7.81 % (2927946)CaDiCaL version: 2.1.3
% 28.12/7.81 % (2927946)Termination reason: Refutation not found, incomplete strategy
% 28.12/7.81 % (2927946)Time elapsed: 0.147 s
% 28.12/7.81 % (2927946)Peak memory usage: 144 MB
% 28.12/7.81 % (2927946)Instructions burned: 205 (million)
% 43.40/10.03 % (2927951)lrs+1011_1_sil=32000:sp=occurrence:random_seed=481935142:i=325:sd=1:ss=axioms:sgt=32_2963 on theBenchmark for (2963ds/325Mi)
% 43.40/10.03 % (2927950)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4006720862:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/157Mi)
% 43.40/10.03 % (2927952)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=1951528140:s2a=on:i=248:s2at=1.23:gtg=position_2963 on theBenchmark for (2963ds/248Mi)
% 43.40/10.03 % (2927950)Instruction limit reached!
% 43.40/10.03 % (2927950)------------------------------
% 43.40/10.03 % (2927950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.40/10.03 % (2927950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.40/10.03 % (2927950)CaDiCaL version: 2.1.3
% 43.40/10.03 % (2927950)Termination reason: Instruction limit
% 43.40/10.03 % (2927950)Termination phase: Property scanning
% 43.40/10.03 % (2927950)Time elapsed: 0.146 s
% 43.40/10.03 % (2927950)Peak memory usage: 138 MB
% 43.40/10.03 % (2927950)Instructions burned: 158 (million)
% 43.40/10.03 % (2927951)Refutation not found, incomplete strategy
% 43.40/10.03 % (2927951)------------------------------
% 43.40/10.03 % (2927951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.40/10.03 % (2927951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.40/10.03 % (2927951)CaDiCaL version: 2.1.3
% 43.40/10.03 % (2927951)Termination reason: Refutation not found, incomplete strategy
% 43.40/10.03 % (2927951)Time elapsed: 0.238 s
% 43.40/10.03 % (2927951)Peak memory usage: 144 MB
% 43.40/10.03 % (2927951)Instructions burned: 202 (million)
% 43.40/10.03 % (2927952)Instruction limit reached!
% 43.40/10.03 % (2927952)------------------------------
% 43.40/10.03 % (2927952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.40/10.03 % (2927952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.40/10.03 % (2927952)CaDiCaL version: 2.1.3
% 43.40/10.03 % (2927952)Termination reason: Instruction limit
% 43.40/10.03 % (2927952)Termination phase: Property scanning
% 43.40/10.03 % (2927952)Time elapsed: 0.223 s
% 43.40/10.03 % (2927952)Peak memory usage: 138 MB
% 43.40/10.03 % (2927952)Instructions burned: 249 (million)
% 43.40/10.03 % (2927946)------------------------------
% 43.40/10.03 % (2927946)------------------------------
% 43.40/10.03 % (2927957)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2379138702:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2959 on theBenchmark for (2959ds/294Mi)
% 43.40/10.03 % (2927959)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1292746863:cts=off:i=113:fsr=off:ss=included:sgt=4_2957 on theBenchmark for (2957ds/113Mi)
% 43.40/10.03 % (2927958)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1295149622:i=2350_2958 on theBenchmark for (2958ds/2350Mi)
% 43.40/10.03 % (2927959)Instruction limit reached!
% 43.40/10.03 % (2927959)------------------------------
% 43.40/10.03 % (2927959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.40/10.03 % (2927959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.40/10.03 % (2927959)CaDiCaL version: 2.1.3
% 43.40/10.03 % (2927959)Termination reason: Instruction limit
% 43.40/10.03 % (2927959)Termination phase: SInE selection
% 43.40/10.03 % (2927959)Time elapsed: 0.067 s
% 43.40/10.03 % (2927959)Peak memory usage: 139 MB
% 43.40/10.03 % (2927959)Instructions burned: 113 (million)
% 43.40/10.03 % (2927951)------------------------------
% 43.40/10.03 % (2927951)------------------------------
% 43.40/10.03 % (2927957)Instruction limit reached!
% 43.40/10.03 % (2927957)------------------------------
% 43.40/10.03 % (2927957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.40/10.03 % (2927957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.40/10.03 % (2927957)CaDiCaL version: 2.1.3
% 43.40/10.03 % (2927957)Termination reason: Instruction limit
% 43.40/10.03 % (2927957)Termination phase: Saturation
% 43.40/10.03 % (2927957)Time elapsed: 0.309 s
% 43.40/10.03 % (2927957)Peak memory usage: 142 MB
% 43.40/10.03 % (2927957)Instructions burned: 295 (million)
% 43.40/10.03 % (2927963)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2915012072:i=127:av=off:fsr=off:sup=off_2954 on theBenchmark for (2954ds/127Mi)
% 43.40/10.03 % (2927963)Instruction limit reached!
% 43.40/10.03 % (2927963)------------------------------
% 43.40/10.03 % (2927963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.33/15.63 % (2927963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.33/15.63 % (2927963)CaDiCaL version: 2.1.3
% 84.33/15.63 % (2927963)Termination reason: Instruction limit
% 84.33/15.63 % (2927963)Termination phase: Preprocessing 1
% 84.33/15.63 % (2927963)Time elapsed: 0.076 s
% 84.33/15.63 % (2927963)Peak memory usage: 138 MB
% 84.33/15.63 % (2927963)Instructions burned: 128 (million)
% 84.33/15.63 % (2927964)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3857278211:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2953 on theBenchmark for (2953ds/114Mi)
% 84.33/15.63 % (2927965)lrs+10_1_sil=8000:sp=occurrence:random_seed=4279750290:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2952 on theBenchmark for (2952ds/907Mi)
% 84.33/15.63 % (2927964)Instruction limit reached!
% 84.33/15.63 % (2927964)------------------------------
% 84.33/15.63 % (2927964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.33/15.63 % (2927964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.33/15.63 % (2927964)CaDiCaL version: 2.1.3
% 84.33/15.63 % (2927964)Termination reason: Instruction limit
% 84.33/15.63 % (2927964)Termination phase: Property scanning
% 84.33/15.63 % (2927964)Time elapsed: 0.113 s
% 84.33/15.63 % (2927964)Peak memory usage: 138 MB
% 84.33/15.63 % (2927964)Instructions burned: 115 (million)
% 84.33/15.63 % (2927967)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3875372730:i=437:sd=1:aac=none:ss=included_2951 on theBenchmark for (2951ds/437Mi)
% 84.33/15.63 % (2927965)Refutation not found, incomplete strategy
% 84.33/15.63 % (2927965)------------------------------
% 84.33/15.63 % (2927965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.33/15.63 % (2927965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.33/15.63 % (2927965)CaDiCaL version: 2.1.3
% 84.33/15.63 % (2927965)Termination reason: Refutation not found, incomplete strategy
% 84.33/15.63 % (2927965)Time elapsed: 0.278 s
% 84.33/15.63 % (2927965)Peak memory usage: 144 MB
% 84.33/15.63 % (2927965)Instructions burned: 237 (million)
% 84.33/15.63 % (2927970)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1334257436:i=5202:ss=axioms:sgt=16_2949 on theBenchmark for (2949ds/5202Mi)
% 84.33/15.63 % (2927967)Instruction limit reached!
% 84.33/15.63 % (2927967)------------------------------
% 84.33/15.63 % (2927967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.33/15.63 % (2927967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.33/15.63 % (2927967)CaDiCaL version: 2.1.3
% 84.33/15.63 % (2927967)Termination reason: Instruction limit
% 84.33/15.63 % (2927967)Termination phase: Saturation
% 84.33/15.63 % (2927967)Time elapsed: 0.375 s
% 84.33/15.63 % (2927967)Peak memory usage: 143 MB
% 84.33/15.63 % (2927967)Instructions burned: 438 (million)
% 84.33/15.63 % (2927965)------------------------------
% 84.33/15.63 % (2927965)------------------------------
% 84.33/15.63 % (2927973)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3827106050:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2944 on theBenchmark for (2944ds/134Mi)
% 84.33/15.63 % (2927973)Instruction limit reached!
% 84.33/15.63 % (2927973)------------------------------
% 84.33/15.63 % (2927973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.33/15.63 % (2927973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.33/15.63 % (2927973)CaDiCaL version: 2.1.3
% 84.33/15.63 % (2927973)Termination reason: Instruction limit
% 84.33/15.63 % (2927973)Termination phase: SInE selection
% 84.33/15.63 % (2927973)Time elapsed: 0.135 s
% 84.33/15.63 % (2927973)Peak memory usage: 139 MB
% 84.33/15.63 % (2927973)Instructions burned: 134 (million)
% 84.33/15.63 % (2927974)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2325098824:st=8:i=592:sd=3:ep=RST:ss=axioms_2942 on theBenchmark for (2942ds/592Mi)
% 84.33/15.63 % (2927976)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1565061273:st=3:i=13193:sd=3:ss=axioms_2939 on theBenchmark for (2939ds/13193Mi)
% 84.33/15.63 % (2927974)Instruction limit reached!
% 84.33/15.63 % (2927974)------------------------------
% 84.33/15.63 % (2927974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.33/15.63 % (2927974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.33/15.63 % (2927974)CaDiCaL version: 2.1.3
% 84.33/15.63 % (2927974)Termination reason: Instruction limit
% 84.33/15.63 % (2927974)Termination phase: Saturation
% 84.33/15.63 % (2927974)Time elapsed: 0.613 s
% 56.60/15.92 % (2927974)Peak memory usage: 148 MB
% 56.60/15.92 % (2927974)Instructions burned: 593 (million)
% 56.60/15.92 % (2927958)Instruction limit reached!
% 56.60/15.92 % (2927958)------------------------------
% 56.60/15.92 % (2927958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.60/15.92 % (2927958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.60/15.92 % (2927958)CaDiCaL version: 2.1.3
% 56.60/15.92 % (2927958)Termination reason: Instruction limit
% 56.60/15.92 % (2927958)Termination phase: Saturation
% 56.60/15.92 % (2927958)Time elapsed: 2.488 s
% 56.60/15.92 % (2927958)Peak memory usage: 248 MB
% 56.60/15.92 % (2927958)Instructions burned: 2350 (million)
% 56.60/15.92 % (2927979)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=514521517:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2932 on theBenchmark for (2932ds/125Mi)
% 56.60/15.92 % (2927979)Instruction limit reached!
% 56.60/15.92 % (2927979)------------------------------
% 56.60/15.92 % (2927979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.60/15.92 % (2927979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.60/15.92 % (2927979)CaDiCaL version: 2.1.3
% 56.60/15.92 % (2927979)Termination reason: Instruction limit
% 56.60/15.92 % (2927979)Termination phase: Property scanning
% 56.60/15.92 % (2927979)Time elapsed: 0.122 s
% 56.60/15.92 % (2927979)Peak memory usage: 138 MB
% 56.60/15.92 % (2927979)Instructions burned: 125 (million)
% 56.60/15.92 % (2927980)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2310132297:i=134:gtgl=5:slsql=off:gtg=exists_sym_2930 on theBenchmark for (2930ds/134Mi)
% 56.60/15.92 % (2927980)Instruction limit reached!
% 56.60/15.92 % (2927980)------------------------------
% 56.60/15.92 % (2927980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.60/15.92 % (2927980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.60/15.92 % (2927980)CaDiCaL version: 2.1.3
% 56.60/15.92 % (2927980)Termination reason: Instruction limit
% 56.60/15.92 % (2927980)Termination phase: Property scanning
% 56.60/15.92 % (2927980)Time elapsed: 0.135 s
% 56.60/15.92 % (2927980)Peak memory usage: 138 MB
% 56.60/15.92 % (2927980)Instructions burned: 134 (million)
% 56.60/15.92 % (2927982)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3507709360:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2928 on theBenchmark for (2928ds/141Mi)
% 56.60/15.92 % (2927982)Instruction limit reached!
% 56.60/15.92 % (2927982)------------------------------
% 56.60/15.92 % (2927982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.60/15.92 % (2927982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.60/15.92 % (2927982)CaDiCaL version: 2.1.3
% 56.60/15.92 % (2927982)Termination reason: Instruction limit
% 56.60/15.92 % (2927982)Termination phase: SInE selection
% 56.60/15.92 % (2927982)Time elapsed: 0.145 s
% 56.60/15.92 % (2927982)Peak memory usage: 139 MB
% 56.60/15.92 % (2927982)Instructions burned: 141 (million)
% 56.60/15.92 % (2927984)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3593718538:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2925 on theBenchmark for (2925ds/431Mi)
% 56.60/15.92 % (2927986)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=870529167:i=6060:aac=none:ins=25_2923 on theBenchmark for (2923ds/6060Mi)
% 56.60/15.92 % (2927984)Refutation not found, incomplete strategy
% 56.60/15.92 % (2927984)------------------------------
% 56.60/15.92 % (2927984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.60/15.92 % (2927984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.60/15.92 % (2927984)CaDiCaL version: 2.1.3
% 56.60/15.92 % (2927984)Termination reason: Refutation not found, incomplete strategy
% 56.60/15.92 % (2927984)Time elapsed: 0.252 s
% 56.60/15.92 % (2927984)Peak memory usage: 144 MB
% 56.60/15.92 % (2927984)Instructions burned: 202 (million)
% 56.60/15.92 % (2927984)------------------------------
% 56.60/15.92 % (2927984)------------------------------
% 56.60/15.92 % (2927989)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=1055135511:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2915 on theBenchmark for (2915ds/150Mi)
% 56.60/15.92 % (2927989)Instruction limit reached!
% 56.60/15.92 % (2927989)------------------------------
% 56.60/15.92 % (2927989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.60/15.92 % (2927989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.60/15.92 % (2927989)CaDiCaL version: 2.1.3
% 56.60/15.92 % (2927989)Termination reason: Instruction limit
% 56.60/15.92 % (2927989)Termination phase: SInE selection
% 56.60/15.92 % (2927989)Time elapsed: 0.151 s
% 56.60/15.92 % (2927989)Peak memory usage: 139 MB
% 56.60/15.92 % (2927989)Instructions burned: 150 (million)
% 56.60/15.92 % (2927991)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3514448068:i=14155:bd=all_2910 on theBenchmark for (2910ds/14155Mi)
% 56.60/15.92 % (2927970)Instruction limit reached!
% 56.60/15.92 % (2927970)------------------------------
% 56.60/15.92 % (2927970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.60/15.92 % (2927970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.60/15.92 % (2927970)CaDiCaL version: 2.1.3
% 56.60/15.92 % (2927970)Termination reason: Instruction limit
% 56.60/15.92 % (2927970)Termination phase: Saturation
% 56.60/15.92 % (2927970)Time elapsed: 4.748 s
% 56.60/15.92 % (2927970)Peak memory usage: 215 MB
% 56.60/15.92 % (2927970)Instructions burned: 5203 (million)
% 56.60/15.92 % (2927993)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2226410826:i=667:av=off:fsr=off_2898 on theBenchmark for (2898ds/667Mi)
% 56.60/15.92 % (2927993)Instruction limit reached!
% 56.60/15.92 % (2927993)------------------------------
% 56.60/15.92 % (2927993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.60/15.92 % (2927993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.60/15.92 % (2927993)CaDiCaL version: 2.1.3
% 56.60/15.92 % (2927993)Termination reason: Instruction limit
% 56.60/15.92 % (2927993)Termination phase: NewCNF
% 56.60/15.92 % (2927993)Time elapsed: 0.758 s
% 56.60/15.92 % (2927993)Peak memory usage: 162 MB
% 56.60/15.92 % (2927993)Instructions burned: 667 (million)
% 56.60/15.92 % (2927995)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3823050766:s2a=on:i=185:s2at=1.8:fdi=4_2887 on theBenchmark for (2887ds/185Mi)
% 56.60/15.92 % (2927995)Instruction limit reached!
% 56.60/15.92 % (2927995)------------------------------
% 56.60/15.92 % (2927995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.60/15.92 % (2927995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.60/15.92 % (2927995)CaDiCaL version: 2.1.3
% 56.60/15.92 % (2927995)Termination reason: Instruction limit
% 56.60/15.92 % (2927995)Termination phase: SInE selection
% 56.60/15.92 % (2927995)Time elapsed: 0.174 s
% 56.60/15.92 % (2927995)Peak memory usage: 139 MB
% 56.60/15.92 % (2927995)Instructions burned: 186 (million)
% 56.60/15.92 % (2927997)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1388718787:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2882 on theBenchmark for (2882ds/193Mi)
% 56.60/15.92 % (2927997)Instruction limit reached!
% 56.60/15.92 % (2927997)------------------------------
% 56.60/15.92 % (2927997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.60/15.92 % (2927997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.60/15.92 % (2927997)CaDiCaL version: 2.1.3
% 56.60/15.92 % (2927997)Termination reason: Instruction limit
% 56.60/15.92 % (2927997)Termination phase: SInE selection
% 56.60/15.92 % (2927997)Time elapsed: 0.195 s
% 56.60/15.92 % (2927997)Peak memory usage: 139 MB
% 56.60/15.92 % (2927997)Instructions burned: 193 (million)
% 56.60/15.92 % (2927999)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2762770500:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2877 on theBenchmark for (2877ds/4850Mi)
% 56.60/15.92 % (2927999)First to succeed.
% 56.60/15.92 % (2927999)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2927930"
% 56.60/15.92 % (2927986)Instruction limit reached!
% 56.60/15.92 % (2927986)------------------------------
% 56.60/15.92 % (2927986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.60/15.92 % (2927986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.60/15.92 % (2927986)CaDiCaL version: 2.1.3
% 56.60/15.92 % (2927986)Termination reason: Instruction limit
% 56.60/15.92 % (2927986)Termination phase: Saturation
% 56.60/15.92 % (2927986)Time elapsed: 6.606 s
% 56.60/15.92 % (2927986)Peak memory usage: 565 MB
% 56.60/15.92 % (2927986)Instructions burned: 6064 (million)
% 56.60/15.92 % (2927999)Refutation found. Thanks to Tanya!
% 56.60/15.92 % SZS status Theorem for theBenchmark
% 56.60/15.92 % SZS output start Proof for theBenchmark
% See solution above
% 0.35/16.30 % (2927999)------------------------------
% 0.35/16.30 % (2927999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.35/16.30 % (2927999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/16.30 % (2927999)CaDiCaL version: 2.1.3
% 0.35/16.30 % (2927999)Termination reason: Refutation
% 0.35/16.30 % (2927999)Time elapsed: 1.641 s
% 0.35/16.30 % (2927999)Peak memory usage: 156 MB
% 0.35/16.30 % (2927999)Instructions burned: 1642 (million)
% 0.35/16.30 % (2927999)------------------------------
% 0.35/16.30 % (2927999)------------------------------
% 0.35/16.30 % (2927930)Success in time 14.819 s
% 0.35/16.30 % Vampire exiting
%------------------------------------------------------------------------------