%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR219+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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:46:28 AM UTC 2026
% Result : Theorem 184.13s 39.71s
% Output : Refutation 184.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 34
% Syntax : Number of formulae : 130 ( 24 unt; 19 def)
% Number of atoms : 591 ( 10 equ)
% Maximal formula atoms : 50 ( 4 avg)
% Number of connectives : 802 ( 341 ~; 257 |; 135 &)
% ( 29 <=>; 40 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 6 prp; 0-4 aty)
% Number of functors : 15 ( 15 usr; 12 con; 0-2 aty)
% Number of variables : 234 ( 0 sgn 225 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( p__d__subclass(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__subclass(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',predefinitionsA8) ).
fof(f61,axiom,
( ! [X0,X1] :
( ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Attribute) )
=> ( p__contraryAttribute2(X0,X1)
<=> ( ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
=> ~ p__attribute(X2,X1) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X1) )
=> ~ p__attribute(X2,X0) ) ) ) )
& ! [X0,X1,X3,X4] :
( ( p__d__instance(X4,c__Attribute)
& p__d__instance(X3,c__Attribute)
& p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Attribute) )
=> ( p__contraryAttribute4(X0,X1,X3,X4)
<=> ( ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
=> ~ p__attribute(X2,X1) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X1) )
=> ~ p__attribute(X2,X0) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
=> ~ p__attribute(X2,X3) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X3) )
=> ~ p__attribute(X2,X0) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
=> ~ p__attribute(X2,X4) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X4) )
=> ~ p__attribute(X2,X0) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X1) )
=> ~ p__attribute(X2,X3) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X3) )
=> ~ p__attribute(X2,X1) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X1) )
=> ~ p__attribute(X2,X4) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X4) )
=> ~ p__attribute(X2,X1) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X3) )
=> ~ p__attribute(X2,X4) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X4) )
=> ~ p__attribute(X2,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA90) ).
fof(f110,axiom,
! [X0] :
( p__d__subclass(X0,c__Entity)
=> ? [X1] : p__d__instance(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA176) ).
fof(f111,axiom,
! [X0] :
( p__d__instance(X0,c__Class)
<=> p__d__subclass(X0,c__Entity) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA177) ).
fof(f112,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA178) ).
fof(f115,axiom,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA181) ).
fof(f2267,axiom,
p__d__subclass(c__Artifact,c__Object),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA3134) ).
fof(f2305,axiom,
p__d__subclass(c__Device,c__Artifact),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA3181) ).
fof(f2622,axiom,
p__contraryAttribute2(c__Rigid,c__Pliable),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',mergeA3601) ).
fof(f3239,axiom,
p__d__subclass(c__Holder,c__Device),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',miloA698) ).
fof(f3248,axiom,
p__d__subclass(c__Container,c__Holder),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',miloA711) ).
fof(f3249,axiom,
p__d__subclass(c__Bag,c__Container),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',miloA713) ).
fof(f3250,axiom,
! [X0] :
( p__d__instance(X0,c__Bag)
=> p__attribute(X0,c__Pliable) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',miloA714) ).
fof(f6921,axiom,
! [X0,X1] :
( p__attribute(X0,X1)
=> ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Object) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR006+0.ax',typeA68) ).
fof(f7433,conjecture,
? [X0] :
( p__d__instance(X0,c__Object)
& p__attribute(X0,c__Pliable)
& ! [X1] :
( p__d__instance(X1,c__Object)
=> ( p__attribute(X1,c__Rigid)
=> X0 != X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antonymPattern20012) ).
fof(f7434,negated_conjecture,
~ ? [X0] :
( p__d__instance(X0,c__Object)
& p__attribute(X0,c__Pliable)
& ! [X1] :
( p__d__instance(X1,c__Object)
=> ( p__attribute(X1,c__Rigid)
=> X0 != X1 ) ) ),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7438,plain,
( ! [X0,X1] :
( ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Attribute) )
=> ( p__contraryAttribute2(X0,X1)
<=> ( ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
=> ~ p__attribute(X2,X1) )
& ! [X3] :
( ( p__d__instance(X3,c__Object)
& p__attribute(X3,X1) )
=> ~ p__attribute(X3,X0) ) ) ) )
& ! [X4,X5,X6,X7] :
( ( p__d__instance(X7,c__Attribute)
& p__d__instance(X6,c__Attribute)
& p__d__instance(X5,c__Attribute)
& p__d__instance(X4,c__Attribute) )
=> ( p__contraryAttribute4(X4,X5,X6,X7)
<=> ( ! [X8] :
( ( p__d__instance(X8,c__Object)
& p__attribute(X8,X4) )
=> ~ p__attribute(X8,X5) )
& ! [X9] :
( ( p__d__instance(X9,c__Object)
& p__attribute(X9,X5) )
=> ~ p__attribute(X9,X4) )
& ! [X10] :
( ( p__d__instance(X10,c__Object)
& p__attribute(X10,X4) )
=> ~ p__attribute(X10,X6) )
& ! [X11] :
( ( p__d__instance(X11,c__Object)
& p__attribute(X11,X6) )
=> ~ p__attribute(X11,X4) )
& ! [X12] :
( ( p__d__instance(X12,c__Object)
& p__attribute(X12,X4) )
=> ~ p__attribute(X12,X7) )
& ! [X13] :
( ( p__d__instance(X13,c__Object)
& p__attribute(X13,X7) )
=> ~ p__attribute(X13,X4) )
& ! [X14] :
( ( p__d__instance(X14,c__Object)
& p__attribute(X14,X5) )
=> ~ p__attribute(X14,X6) )
& ! [X15] :
( ( p__d__instance(X15,c__Object)
& p__attribute(X15,X6) )
=> ~ p__attribute(X15,X5) )
& ! [X16] :
( ( p__d__instance(X16,c__Object)
& p__attribute(X16,X5) )
=> ~ p__attribute(X16,X7) )
& ! [X17] :
( ( p__d__instance(X17,c__Object)
& p__attribute(X17,X7) )
=> ~ p__attribute(X17,X5) )
& ! [X18] :
( ( p__d__instance(X18,c__Object)
& p__attribute(X18,X6) )
=> ~ p__attribute(X18,X7) )
& ! [X19] :
( ( p__d__instance(X19,c__Object)
& p__attribute(X19,X7) )
=> ~ p__attribute(X19,X6) ) ) ) ) ),
inference(rectify,[],[f61]) ).
fof(f7449,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7450,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7449]) ).
fof(f7487,plain,
( ! [X0,X1] :
( ( p__contraryAttribute2(X0,X1)
<=> ( ! [X2] :
( ~ p__attribute(X2,X1)
| ~ p__d__instance(X2,c__Object)
| ~ p__attribute(X2,X0) )
& ! [X3] :
( ~ p__attribute(X3,X0)
| ~ p__d__instance(X3,c__Object)
| ~ p__attribute(X3,X1) ) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) )
& ! [X4,X5,X6,X7] :
( ( p__contraryAttribute4(X4,X5,X6,X7)
<=> ( ! [X8] :
( ~ p__attribute(X8,X5)
| ~ p__d__instance(X8,c__Object)
| ~ p__attribute(X8,X4) )
& ! [X9] :
( ~ p__attribute(X9,X4)
| ~ p__d__instance(X9,c__Object)
| ~ p__attribute(X9,X5) )
& ! [X10] :
( ~ p__attribute(X10,X6)
| ~ p__d__instance(X10,c__Object)
| ~ p__attribute(X10,X4) )
& ! [X11] :
( ~ p__attribute(X11,X4)
| ~ p__d__instance(X11,c__Object)
| ~ p__attribute(X11,X6) )
& ! [X12] :
( ~ p__attribute(X12,X7)
| ~ p__d__instance(X12,c__Object)
| ~ p__attribute(X12,X4) )
& ! [X13] :
( ~ p__attribute(X13,X4)
| ~ p__d__instance(X13,c__Object)
| ~ p__attribute(X13,X7) )
& ! [X14] :
( ~ p__attribute(X14,X6)
| ~ p__d__instance(X14,c__Object)
| ~ p__attribute(X14,X5) )
& ! [X15] :
( ~ p__attribute(X15,X5)
| ~ p__d__instance(X15,c__Object)
| ~ p__attribute(X15,X6) )
& ! [X16] :
( ~ p__attribute(X16,X7)
| ~ p__d__instance(X16,c__Object)
| ~ p__attribute(X16,X5) )
& ! [X17] :
( ~ p__attribute(X17,X5)
| ~ p__d__instance(X17,c__Object)
| ~ p__attribute(X17,X7) )
& ! [X18] :
( ~ p__attribute(X18,X7)
| ~ p__d__instance(X18,c__Object)
| ~ p__attribute(X18,X6) )
& ! [X19] :
( ~ p__attribute(X19,X6)
| ~ p__d__instance(X19,c__Object)
| ~ p__attribute(X19,X7) ) ) )
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ) ),
inference(ennf_transformation,[],[f7438]) ).
fof(f7488,plain,
( ! [X0,X1] :
( ( p__contraryAttribute2(X0,X1)
<=> ( ! [X2] :
( ~ p__attribute(X2,X1)
| ~ p__d__instance(X2,c__Object)
| ~ p__attribute(X2,X0) )
& ! [X3] :
( ~ p__attribute(X3,X0)
| ~ p__d__instance(X3,c__Object)
| ~ p__attribute(X3,X1) ) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) )
& ! [X4,X5,X6,X7] :
( ( p__contraryAttribute4(X4,X5,X6,X7)
<=> ( ! [X8] :
( ~ p__attribute(X8,X5)
| ~ p__d__instance(X8,c__Object)
| ~ p__attribute(X8,X4) )
& ! [X9] :
( ~ p__attribute(X9,X4)
| ~ p__d__instance(X9,c__Object)
| ~ p__attribute(X9,X5) )
& ! [X10] :
( ~ p__attribute(X10,X6)
| ~ p__d__instance(X10,c__Object)
| ~ p__attribute(X10,X4) )
& ! [X11] :
( ~ p__attribute(X11,X4)
| ~ p__d__instance(X11,c__Object)
| ~ p__attribute(X11,X6) )
& ! [X12] :
( ~ p__attribute(X12,X7)
| ~ p__d__instance(X12,c__Object)
| ~ p__attribute(X12,X4) )
& ! [X13] :
( ~ p__attribute(X13,X4)
| ~ p__d__instance(X13,c__Object)
| ~ p__attribute(X13,X7) )
& ! [X14] :
( ~ p__attribute(X14,X6)
| ~ p__d__instance(X14,c__Object)
| ~ p__attribute(X14,X5) )
& ! [X15] :
( ~ p__attribute(X15,X5)
| ~ p__d__instance(X15,c__Object)
| ~ p__attribute(X15,X6) )
& ! [X16] :
( ~ p__attribute(X16,X7)
| ~ p__d__instance(X16,c__Object)
| ~ p__attribute(X16,X5) )
& ! [X17] :
( ~ p__attribute(X17,X5)
| ~ p__d__instance(X17,c__Object)
| ~ p__attribute(X17,X7) )
& ! [X18] :
( ~ p__attribute(X18,X7)
| ~ p__d__instance(X18,c__Object)
| ~ p__attribute(X18,X6) )
& ! [X19] :
( ~ p__attribute(X19,X6)
| ~ p__d__instance(X19,c__Object)
| ~ p__attribute(X19,X7) ) ) )
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ) ),
inference(flattening,[],[f7487]) ).
fof(f7503,plain,
! [X0] :
( ? [X1] : p__d__instance(X1,X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(ennf_transformation,[],[f110]) ).
fof(f8767,plain,
! [X0] :
( p__attribute(X0,c__Pliable)
| ~ p__d__instance(X0,c__Bag) ),
inference(ennf_transformation,[],[f3250]) ).
fof(f11093,plain,
! [X0,X1] :
( ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Object) )
| ~ p__attribute(X0,X1) ),
inference(ennf_transformation,[],[f6921]) ).
fof(f11600,plain,
! [X0] :
( ~ p__d__instance(X0,c__Object)
| ~ p__attribute(X0,c__Pliable)
| ? [X1] :
( X0 = X1
& p__attribute(X1,c__Rigid)
& p__d__instance(X1,c__Object) ) ),
inference(ennf_transformation,[],[f7434]) ).
fof(f11601,plain,
! [X0] :
( ~ p__d__instance(X0,c__Object)
| ~ p__attribute(X0,c__Pliable)
| ? [X1] :
( X0 = X1
& p__attribute(X1,c__Rigid)
& p__d__instance(X1,c__Object) ) ),
inference(flattening,[],[f11600]) ).
fof(f11602,definition,
! [X6,X7] :
( sP0(X6,X7)
<=> ! [X19] :
( ~ p__attribute(X19,X6)
| ~ p__d__instance(X19,c__Object)
| ~ p__attribute(X19,X7) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11603,definition,
! [X7,X6] :
( sP1(X7,X6)
<=> ! [X18] :
( ~ p__attribute(X18,X7)
| ~ p__d__instance(X18,c__Object)
| ~ p__attribute(X18,X6) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f11604,definition,
! [X5,X7] :
( sP2(X5,X7)
<=> ! [X17] :
( ~ p__attribute(X17,X5)
| ~ p__d__instance(X17,c__Object)
| ~ p__attribute(X17,X7) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f11605,definition,
! [X7,X5] :
( sP3(X7,X5)
<=> ! [X16] :
( ~ p__attribute(X16,X7)
| ~ p__d__instance(X16,c__Object)
| ~ p__attribute(X16,X5) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f11606,definition,
! [X5,X6] :
( sP4(X5,X6)
<=> ! [X15] :
( ~ p__attribute(X15,X5)
| ~ p__d__instance(X15,c__Object)
| ~ p__attribute(X15,X6) ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f11607,definition,
! [X6,X5] :
( sP5(X6,X5)
<=> ! [X14] :
( ~ p__attribute(X14,X6)
| ~ p__d__instance(X14,c__Object)
| ~ p__attribute(X14,X5) ) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f11608,definition,
! [X4,X7] :
( sP6(X4,X7)
<=> ! [X13] :
( ~ p__attribute(X13,X4)
| ~ p__d__instance(X13,c__Object)
| ~ p__attribute(X13,X7) ) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f11609,definition,
! [X7,X4] :
( sP7(X7,X4)
<=> ! [X12] :
( ~ p__attribute(X12,X7)
| ~ p__d__instance(X12,c__Object)
| ~ p__attribute(X12,X4) ) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f11610,definition,
! [X4,X6] :
( sP8(X4,X6)
<=> ! [X11] :
( ~ p__attribute(X11,X4)
| ~ p__d__instance(X11,c__Object)
| ~ p__attribute(X11,X6) ) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f11611,definition,
! [X6,X4] :
( sP9(X6,X4)
<=> ! [X10] :
( ~ p__attribute(X10,X6)
| ~ p__d__instance(X10,c__Object)
| ~ p__attribute(X10,X4) ) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f11612,definition,
! [X4,X5] :
( sP10(X4,X5)
<=> ! [X9] :
( ~ p__attribute(X9,X4)
| ~ p__d__instance(X9,c__Object)
| ~ p__attribute(X9,X5) ) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f11613,definition,
! [X5,X4,X6,X7] :
( sP11(X5,X4,X6,X7)
<=> ( ! [X8] :
( ~ p__attribute(X8,X5)
| ~ p__d__instance(X8,c__Object)
| ~ p__attribute(X8,X4) )
& sP10(X4,X5)
& sP9(X6,X4)
& sP8(X4,X6)
& sP7(X7,X4)
& sP6(X4,X7)
& sP5(X6,X5)
& sP4(X5,X6)
& sP3(X7,X5)
& sP2(X5,X7)
& sP1(X7,X6)
& sP0(X6,X7) ) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f11614,definition,
! [X7,X6,X4,X5] :
( ( p__contraryAttribute4(X4,X5,X6,X7)
<=> sP11(X5,X4,X6,X7) )
| ~ sP12(X7,X6,X4,X5) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f11615,definition,
! [X0,X1] :
( sP13(X0,X1)
<=> ! [X3] :
( ~ p__attribute(X3,X0)
| ~ p__d__instance(X3,c__Object)
| ~ p__attribute(X3,X1) ) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f11616,plain,
( ! [X0,X1] :
( ( p__contraryAttribute2(X0,X1)
<=> ( ! [X2] :
( ~ p__attribute(X2,X1)
| ~ p__d__instance(X2,c__Object)
| ~ p__attribute(X2,X0) )
& sP13(X0,X1) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) )
& ! [X4,X5,X6,X7] :
( sP12(X7,X6,X4,X5)
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ) ),
inference(definition_folding,[],[f7488,f11615,f11614,f11613,f11612,f11611,f11610,f11609,f11608,f11607,f11606,f11605,f11604,f11603,f11602]) ).
fof(f11714,plain,
( ! [X0,X1] :
( ( ( p__contraryAttribute2(X0,X1)
| ? [X2] :
( p__attribute(X2,X1)
& p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
| ~ sP13(X0,X1) )
& ( ( ! [X2] :
( ~ p__attribute(X2,X1)
| ~ p__d__instance(X2,c__Object)
| ~ p__attribute(X2,X0) )
& sP13(X0,X1) )
| ~ p__contraryAttribute2(X0,X1) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) )
& ! [X4,X5,X6,X7] :
( sP12(X7,X6,X4,X5)
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ) ),
inference(nnf_transformation,[],[f11616]) ).
fof(f11715,plain,
( ! [X0,X1] :
( ( ( p__contraryAttribute2(X0,X1)
| ? [X2] :
( p__attribute(X2,X1)
& p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
| ~ sP13(X0,X1) )
& ( ( ! [X2] :
( ~ p__attribute(X2,X1)
| ~ p__d__instance(X2,c__Object)
| ~ p__attribute(X2,X0) )
& sP13(X0,X1) )
| ~ p__contraryAttribute2(X0,X1) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) )
& ! [X4,X5,X6,X7] :
( sP12(X7,X6,X4,X5)
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ) ),
inference(flattening,[],[f11714]) ).
fof(f11716,plain,
( ! [X0,X1] :
( ( ( p__contraryAttribute2(X0,X1)
| ? [X2] :
( p__attribute(X2,X1)
& p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
| ~ sP13(X0,X1) )
& ( ( ! [X3] :
( ~ p__attribute(X3,X1)
| ~ p__d__instance(X3,c__Object)
| ~ p__attribute(X3,X0) )
& sP13(X0,X1) )
| ~ p__contraryAttribute2(X0,X1) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) )
& ! [X4,X5,X6,X7] :
( sP12(X7,X6,X4,X5)
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ) ),
inference(rectify,[],[f11715]) ).
fof(f11717,plain,
( ! [X0,X1] :
( ( ( p__contraryAttribute2(X0,X1)
| ( p__attribute(sK56(X0,X1),X1)
& p__d__instance(sK56(X0,X1),c__Object)
& p__attribute(sK56(X0,X1),X0) )
| ~ sP13(X0,X1) )
& ( ( ! [X3] :
( ~ p__attribute(X3,X1)
| ~ p__d__instance(X3,c__Object)
| ~ p__attribute(X3,X0) )
& sP13(X0,X1) )
| ~ p__contraryAttribute2(X0,X1) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) )
& ! [X4,X5,X6,X7] :
( sP12(X7,X6,X4,X5)
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56]),skolemize(X2,sK56(X0,X1))],[f11716]) ).
fof(f11722,plain,
! [X0] :
( p__d__instance(sK60(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK60]),skolemize(X1,sK60(X0))],[f7503]) ).
fof(f11723,plain,
! [X0] :
( ( p__d__instance(X0,c__Class)
| ~ p__d__subclass(X0,c__Entity) )
& ( p__d__subclass(X0,c__Entity)
| ~ p__d__instance(X0,c__Class) ) ),
inference(nnf_transformation,[],[f111]) ).
fof(f13400,plain,
! [X0] :
( ~ p__d__instance(X0,c__Object)
| ~ p__attribute(X0,c__Pliable)
| ( sK1263(X0) = X0
& p__attribute(sK1263(X0),c__Rigid)
& p__d__instance(sK1263(X0),c__Object) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1263]),skolemize(X1,sK1263(X0))],[f11601]) ).
fof(f13402,plain,
! [X2,X0,X1] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7450]) ).
fof(f13619,plain,
! [X3,X0,X1] :
( ~ p__attribute(X3,X1)
| ~ p__d__instance(X3,c__Object)
| ~ p__attribute(X3,X0)
| ~ p__contraryAttribute2(X0,X1)
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) ),
inference(cnf_transformation,[],[f11717]) ).
fof(f13682,plain,
! [X0] :
( p__d__instance(sK60(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(cnf_transformation,[],[f11722]) ).
fof(f13683,plain,
! [X0] :
( p__d__subclass(X0,c__Entity)
| ~ p__d__instance(X0,c__Class) ),
inference(cnf_transformation,[],[f11723]) ).
fof(f13684,plain,
! [X0] :
( p__d__instance(X0,c__Class)
| ~ p__d__subclass(X0,c__Entity) ),
inference(cnf_transformation,[],[f11723]) ).
fof(f13685,plain,
p__d__subclass(c__Physical,c__Entity),
inference(cnf_transformation,[],[f112]) ).
fof(f13691,plain,
p__d__subclass(c__Object,c__Physical),
inference(cnf_transformation,[],[f115]) ).
fof(f16457,plain,
p__d__subclass(c__Artifact,c__Object),
inference(cnf_transformation,[],[f2267]) ).
fof(f16506,plain,
p__d__subclass(c__Device,c__Artifact),
inference(cnf_transformation,[],[f2305]) ).
fof(f16888,plain,
p__contraryAttribute2(c__Rigid,c__Pliable),
inference(cnf_transformation,[],[f2622]) ).
fof(f17731,plain,
p__d__subclass(c__Holder,c__Device),
inference(cnf_transformation,[],[f3239]) ).
fof(f17743,plain,
p__d__subclass(c__Container,c__Holder),
inference(cnf_transformation,[],[f3248]) ).
fof(f17744,plain,
p__d__subclass(c__Bag,c__Container),
inference(cnf_transformation,[],[f3249]) ).
fof(f17745,plain,
! [X0] :
( p__attribute(X0,c__Pliable)
| ~ p__d__instance(X0,c__Bag) ),
inference(cnf_transformation,[],[f8767]) ).
fof(f23241,plain,
! [X0,X1] :
( p__d__instance(X0,c__Object)
| ~ p__attribute(X0,X1) ),
inference(cnf_transformation,[],[f11093]) ).
fof(f23242,plain,
! [X0,X1] :
( p__d__instance(X1,c__Attribute)
| ~ p__attribute(X0,X1) ),
inference(cnf_transformation,[],[f11093]) ).
fof(f24208,plain,
! [X0] :
( p__attribute(sK1263(X0),c__Rigid)
| ~ p__attribute(X0,c__Pliable)
| ~ p__d__instance(X0,c__Object) ),
inference(cnf_transformation,[],[f13400]) ).
fof(f24209,plain,
! [X0] :
( ~ p__attribute(X0,c__Pliable)
| ~ p__d__instance(X0,c__Object)
| sK1263(X0) = X0 ),
inference(cnf_transformation,[],[f13400]) ).
fof(f26101,plain,
! [X3,X0,X1] :
( ~ p__attribute(X3,X1)
| ~ p__attribute(X3,X0)
| ~ p__contraryAttribute2(X0,X1)
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) ),
inference(forward_subsumption_resolution,[],[f13619,f23241]) ).
fof(f27276,plain,
! [X3,X0,X1] :
( ~ p__attribute(X3,X1)
| ~ p__attribute(X3,X0)
| ~ p__contraryAttribute2(X0,X1)
| ~ p__d__instance(X0,c__Attribute) ),
inference(forward_subsumption_resolution,[],[f26101,f23242]) ).
fof(f27500,plain,
! [X3,X0,X1] :
( ~ p__attribute(X3,X1)
| ~ p__attribute(X3,X0)
| ~ p__contraryAttribute2(X0,X1) ),
inference(forward_subsumption_resolution,[],[f27276,f23242]) ).
fof(f27572,plain,
! [X0] :
( ~ p__d__instance(X0,c__Bag)
| ~ p__d__instance(X0,c__Object)
| sK1263(X0) = X0 ),
inference(resolution,[],[f17745,f24209]) ).
fof(f27592,plain,
( ~ p__d__subclass(c__Bag,c__Entity)
| ~ p__d__instance(sK60(c__Bag),c__Object)
| sK60(c__Bag) = sK1263(sK60(c__Bag)) ),
inference(resolution,[],[f13682,f27572]) ).
fof(f27595,definition,
( spl1264_1
<=> sK60(c__Bag) = sK1263(sK60(c__Bag)) ),
introduced(definition,[new_symbols(definition,[spl1264_1])],[avatar_definition]) ).
fof(f27597,plain,
( sK60(c__Bag) = sK1263(sK60(c__Bag))
| ~ spl1264_1 ),
inference(avatar_component_clause,[],[f27595]) ).
fof(f27599,definition,
( spl1264_2
<=> p__d__instance(sK60(c__Bag),c__Object) ),
introduced(definition,[new_symbols(definition,[spl1264_2])],[avatar_definition]) ).
fof(f27601,plain,
( ~ p__d__instance(sK60(c__Bag),c__Object)
| spl1264_2 ),
inference(avatar_component_clause,[],[f27599]) ).
fof(f27603,definition,
( spl1264_3
<=> p__d__subclass(c__Bag,c__Entity) ),
introduced(definition,[new_symbols(definition,[spl1264_3])],[avatar_definition]) ).
fof(f27604,plain,
( p__d__subclass(c__Bag,c__Entity)
| ~ spl1264_3 ),
inference(avatar_component_clause,[],[f27603]) ).
fof(f27605,plain,
( ~ p__d__subclass(c__Bag,c__Entity)
| spl1264_3 ),
inference(avatar_component_clause,[],[f27603]) ).
fof(f27606,plain,
( spl1264_1
| ~ spl1264_2
| ~ spl1264_3 ),
inference(avatar_split_clause,[],[f27592,f27603,f27599,f27595]) ).
fof(f27626,plain,
( ! [X0] : ~ p__attribute(sK60(c__Bag),X0)
| spl1264_2 ),
inference(resolution,[],[f27601,f23241]) ).
fof(f27730,plain,
( ~ p__d__instance(sK60(c__Bag),c__Bag)
| spl1264_2 ),
inference(resolution,[],[f27626,f17745]) ).
fof(f27772,plain,
( ~ p__d__subclass(c__Bag,c__Entity)
| spl1264_2 ),
inference(resolution,[],[f27730,f13682]) ).
fof(f27773,plain,
( ~ spl1264_3
| spl1264_2 ),
inference(avatar_split_clause,[],[f27772,f27599,f27603]) ).
fof(f32107,plain,
( ! [X0] :
( ~ p__d__subclass(c__Bag,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl1264_3 ),
inference(resolution,[],[f13402,f27605]) ).
fof(f32108,plain,
( ~ p__d__subclass(c__Container,c__Entity)
| spl1264_3 ),
inference(resolution,[],[f32107,f17744]) ).
fof(f41675,definition,
( spl1264_453
<=> p__d__subclass(c__Object,c__Entity) ),
introduced(definition,[new_symbols(definition,[spl1264_453])],[avatar_definition]) ).
fof(f41676,plain,
( p__d__subclass(c__Object,c__Entity)
| ~ spl1264_453 ),
inference(avatar_component_clause,[],[f41675]) ).
fof(f41677,plain,
( ~ p__d__subclass(c__Object,c__Entity)
| spl1264_453 ),
inference(avatar_component_clause,[],[f41675]) ).
fof(f42220,plain,
( ! [X0] :
( ~ p__d__subclass(c__Object,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl1264_453 ),
inference(resolution,[],[f41677,f13402]) ).
fof(f42365,plain,
( ~ p__d__subclass(c__Object,c__Physical)
| spl1264_453 ),
inference(resolution,[],[f42220,f13685]) ).
fof(f42368,plain,
( $false
| spl1264_453 ),
inference(forward_subsumption_resolution,[],[f42365,f13691]) ).
fof(f42369,plain,
spl1264_453,
inference(avatar_contradiction_clause,[],[f42368]) ).
fof(f50153,plain,
! [X0,X1] :
( ~ p__attribute(sK1263(X0),X1)
| ~ p__contraryAttribute2(c__Rigid,X1)
| ~ p__attribute(X0,c__Pliable)
| ~ p__d__instance(X0,c__Object) ),
inference(resolution,[],[f27500,f24208]) ).
fof(f50184,plain,
! [X0,X1] :
( ~ p__attribute(sK1263(X0),X1)
| ~ p__contraryAttribute2(c__Rigid,X1)
| ~ p__attribute(X0,c__Pliable) ),
inference(forward_subsumption_resolution,[],[f50153,f23241]) ).
fof(f51240,definition,
( spl1264_562
<=> p__d__subclass(c__Artifact,c__Entity) ),
introduced(definition,[new_symbols(definition,[spl1264_562])],[avatar_definition]) ).
fof(f51241,plain,
( p__d__subclass(c__Artifact,c__Entity)
| ~ spl1264_562 ),
inference(avatar_component_clause,[],[f51240]) ).
fof(f51242,plain,
( ~ p__d__subclass(c__Artifact,c__Entity)
| spl1264_562 ),
inference(avatar_component_clause,[],[f51240]) ).
fof(f51487,plain,
( ! [X0] :
( ~ p__d__subclass(c__Artifact,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl1264_562 ),
inference(resolution,[],[f51242,f13402]) ).
fof(f51575,plain,
( ~ p__d__subclass(c__Object,c__Entity)
| spl1264_562 ),
inference(resolution,[],[f51487,f16457]) ).
fof(f51655,plain,
( $false
| ~ spl1264_453
| spl1264_562 ),
inference(forward_subsumption_resolution,[],[f51575,f41676]) ).
fof(f51656,plain,
( ~ spl1264_453
| spl1264_562 ),
inference(avatar_contradiction_clause,[],[f51655]) ).
fof(f86709,plain,
! [X0] :
( ~ p__contraryAttribute2(c__Rigid,c__Pliable)
| ~ p__attribute(X0,c__Pliable)
| ~ p__d__instance(sK1263(X0),c__Bag) ),
inference(resolution,[],[f50184,f17745]) ).
fof(f95506,plain,
! [X0] :
( ~ p__d__instance(sK1263(X0),c__Bag)
| ~ p__attribute(X0,c__Pliable) ),
inference(forward_subsumption_resolution,[],[f86709,f16888]) ).
fof(f107432,plain,
( ~ p__d__instance(sK60(c__Bag),c__Bag)
| ~ p__attribute(sK60(c__Bag),c__Pliable)
| ~ spl1264_1 ),
inference(superposition,[],[f95506,f27597]) ).
fof(f107433,plain,
( ~ p__d__instance(sK60(c__Bag),c__Bag)
| ~ spl1264_1 ),
inference(forward_subsumption_resolution,[],[f107432,f17745]) ).
fof(f107445,plain,
( ~ p__d__subclass(c__Bag,c__Entity)
| ~ spl1264_1 ),
inference(resolution,[],[f107433,f13682]) ).
fof(f107458,plain,
( $false
| ~ spl1264_1
| ~ spl1264_3 ),
inference(forward_subsumption_resolution,[],[f107445,f27604]) ).
fof(f107459,plain,
( ~ spl1264_1
| ~ spl1264_3 ),
inference(avatar_contradiction_clause,[],[f107458]) ).
fof(f107537,plain,
( ! [X0] :
( ~ p__d__subclass(c__Container,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl1264_3 ),
inference(resolution,[],[f32108,f13402]) ).
fof(f109170,plain,
( ! [X0] :
( ~ p__d__subclass(c__Container,X0)
| ~ p__d__instance(X0,c__Class) )
| spl1264_3 ),
inference(resolution,[],[f107537,f13683]) ).
fof(f110409,plain,
( ~ p__d__instance(c__Holder,c__Class)
| spl1264_3 ),
inference(resolution,[],[f109170,f17743]) ).
fof(f110477,plain,
( ~ p__d__subclass(c__Holder,c__Entity)
| spl1264_3 ),
inference(resolution,[],[f110409,f13684]) ).
fof(f110492,plain,
( ! [X0] :
( ~ p__d__subclass(c__Holder,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl1264_3 ),
inference(resolution,[],[f110477,f13402]) ).
fof(f114294,plain,
( ~ p__d__subclass(c__Device,c__Entity)
| spl1264_3 ),
inference(resolution,[],[f110492,f17731]) ).
fof(f114427,plain,
( ! [X0] :
( ~ p__d__subclass(c__Device,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl1264_3 ),
inference(resolution,[],[f114294,f13402]) ).
fof(f117558,plain,
( ~ p__d__subclass(c__Device,c__Artifact)
| spl1264_3
| ~ spl1264_562 ),
inference(resolution,[],[f114427,f51241]) ).
fof(f117561,plain,
( $false
| spl1264_3
| ~ spl1264_562 ),
inference(forward_subsumption_resolution,[],[f117558,f16506]) ).
fof(f117562,plain,
( spl1264_3
| ~ spl1264_562 ),
inference(avatar_contradiction_clause,[],[f117561]) ).
cnf(s1,plain,
( spl1264_1
| ~ spl1264_2
| ~ spl1264_3 ),
inference(sat_conversion,[],[f27606]) ).
cnf(s2,plain,
( spl1264_2
| ~ spl1264_3 ),
inference(sat_conversion,[],[f27773]) ).
cnf(s240,plain,
spl1264_453,
inference(sat_conversion,[],[f42369]) ).
cnf(s323,plain,
( ~ spl1264_453
| spl1264_562 ),
inference(sat_conversion,[],[f51656]) ).
cnf(s807,plain,
( ~ spl1264_1
| ~ spl1264_3 ),
inference(sat_conversion,[],[f107459]) ).
cnf(s1339,plain,
( spl1264_3
| ~ spl1264_562 ),
inference(sat_conversion,[],[f117562]) ).
cnf(s1463,plain,
spl1264_562,
inference(rat,[],[s323,s240]) ).
cnf(s1466,plain,
spl1264_3,
inference(rat,[],[s1339,s1463]) ).
cnf(s1469,plain,
~ spl1264_1,
inference(rat,[],[s807,s1466]) ).
cnf(s1488,plain,
spl1264_2,
inference(rat,[],[s2,s1466]) ).
cnf(s1489,plain,
$false,
inference(rat,[],[s1,s1466,s1488,s1469]) ).
fof(f117599,plain,
$false,
inference(avatar_sat_refutation,[],[s1489]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR219+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 % Computer : n020.cluster.edu
% 0.08/0.21 % Model : x86_64 x86_64
% 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.21 % Memory : 8046.5625MB
% 0.08/0.21 % OS : Linux 6.8.0-71-generic
% 0.08/0.21 % CPULimit : 300
% 0.08/0.21 % WCLimit : 300
% 0.08/0.21 % DateTime : Mon Sep 28 23:48:20 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.24 Running first-order model finding
% 0.08/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.79/2.61 % (689676)Will run a generic schedule for satisfiability detection.
% 15.79/2.61 % (689681)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3055320_2998 on theBenchmark for (2998ds/0Mi)
% 15.79/2.61 % (689682)% WARNING: option uhcvi not known.
% 15.79/2.61 % (689682)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2235860106:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 15.79/2.61 % (689683)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2901254192:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 15.79/2.61 % (689684)dis+10_1_sil=32000:sp=arity:random_seed=2142742673:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 15.79/2.61 % (689685)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=233013440:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 15.79/2.61 % (689686)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=760839669:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 15.79/2.61 % (689687)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1765931982:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 15.79/2.61 % (689684)Instruction limit reached!
% 15.79/2.61 % (689684)------------------------------
% 15.79/2.61 % (689684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.79/2.61 % (689684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.79/2.61 % (689684)CaDiCaL version: 2.1.3
% 15.79/2.61 % (689684)Termination reason: Instruction limit
% 15.79/2.61 % (689684)Termination phase: Clausification
% 15.79/2.61 % (689684)Time elapsed: 0.065 s
% 15.79/2.61 % (689684)Peak memory usage: 23 MB
% 15.79/2.61 % (689684)Instructions burned: 104 (million)
% 15.79/2.61 % (689685)Instruction limit reached!
% 15.79/2.61 % (689685)------------------------------
% 15.79/2.61 % (689685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.79/2.61 % (689685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.79/2.61 % (689685)CaDiCaL version: 2.1.3
% 15.79/2.61 % (689685)Termination reason: Instruction limit
% 15.79/2.61 % (689685)Termination phase: NewCNF
% 15.79/2.61 % (689685)Time elapsed: 0.068 s
% 15.79/2.61 % (689685)Peak memory usage: 23 MB
% 15.79/2.61 % (689685)Instructions burned: 118 (million)
% 15.79/2.61 % (689686)Instruction limit reached!
% 15.79/2.61 % (689686)------------------------------
% 15.79/2.61 % (689686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.79/2.61 % (689686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.79/2.61 % (689686)CaDiCaL version: 2.1.3
% 15.79/2.61 % (689686)Termination reason: Instruction limit
% 15.79/2.61 % (689686)Termination phase: Property scanning
% 15.79/2.61 % (689686)Time elapsed: 0.081 s
% 15.79/2.61 % (689686)Peak memory usage: 24 MB
% 15.79/2.61 % (689686)Instructions burned: 132 (million)
% 15.79/2.61 % (689695)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1587019677:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 15.79/2.61 % (689696)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2324565173:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 15.79/2.61 % (689687)Instruction limit reached!
% 15.79/2.61 % (689687)------------------------------
% 15.79/2.61 % (689687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.79/2.61 % (689687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.79/2.61 % (689687)CaDiCaL version: 2.1.3
% 15.79/2.61 % (689687)Termination reason: Instruction limit
% 15.79/2.61 % (689687)Termination phase: Property scanning
% 15.79/2.61 % (689687)Time elapsed: 0.099 s
% 15.79/2.61 % (689687)Peak memory usage: 24 MB
% 15.79/2.61 % (689687)Instructions burned: 161 (million)
% 15.79/2.61 % (689697)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1777646233:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 15.79/2.61 % (689700)ott-21_1_sil=16000:fs=off:random_seed=4086484053:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 15.79/2.61 % (689696)Instruction limit reached!
% 15.79/2.61 % (689696)------------------------------
% 15.79/2.61 % (689696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.79/2.61 % (689696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.79/2.61 % (689696)CaDiCaL version: 2.1.3
% 15.79/2.61 % (689696)Termination reason: Instruction limit
% 39.15/5.93 % (689696)Termination phase: Property scanning
% 39.15/5.93 % (689696)Time elapsed: 0.081 s
% 39.15/5.93 % (689696)Peak memory usage: 24 MB
% 39.15/5.93 % (689696)Instructions burned: 132 (million)
% 39.15/5.93 % (689703)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3791938611:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 39.15/5.93 % (689700)Instruction limit reached!
% 39.15/5.93 % (689700)------------------------------
% 39.15/5.93 % (689700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.15/5.93 % (689700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.15/5.93 % (689700)CaDiCaL version: 2.1.3
% 39.15/5.93 % (689700)Termination reason: Instruction limit
% 39.15/5.93 % (689700)Termination phase: Property scanning
% 39.15/5.93 % (689700)Time elapsed: 0.103 s
% 39.15/5.93 % (689700)Peak memory usage: 24 MB
% 39.15/5.93 % (689700)Instructions burned: 180 (million)
% 39.15/5.93 % (689705)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1857631851:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 39.15/5.93 % TRYING [1]
% 39.15/5.93 % TRYING [2]
% 39.15/5.93 % (689695)Instruction limit reached!
% 39.15/5.93 % (689695)------------------------------
% 39.15/5.93 % (689695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.15/5.93 % (689695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.15/5.93 % (689695)CaDiCaL version: 2.1.3
% 39.15/5.93 % (689695)Termination reason: Instruction limit
% 39.15/5.93 % (689695)Termination phase: Finite model building preprocessing
% 39.15/5.93 % (689695)Time elapsed: 0.352 s
% 39.15/5.93 % (689695)Peak memory usage: 37 MB
% 39.15/5.93 % (689695)Instructions burned: 715 (million)
% 39.15/5.93 % (689703)Instruction limit reached!
% 39.15/5.93 % (689703)------------------------------
% 39.15/5.93 % (689703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.15/5.93 % (689703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.15/5.93 % (689703)CaDiCaL version: 2.1.3
% 39.15/5.93 % (689703)Termination reason: Instruction limit
% 39.15/5.93 % (689703)Termination phase: Saturation
% 39.15/5.93 % (689703)Time elapsed: 0.252 s
% 39.15/5.93 % (689703)Peak memory usage: 30 MB
% 39.15/5.93 % (689703)Instructions burned: 479 (million)
% 39.15/5.93 % (689697)Instruction limit reached!
% 39.15/5.93 % (689697)------------------------------
% 39.15/5.93 % (689697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.15/5.93 % (689697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.15/5.93 % (689697)CaDiCaL version: 2.1.3
% 39.15/5.93 % (689697)Termination reason: Instruction limit
% 39.15/5.93 % (689697)Termination phase: Saturation
% 39.15/5.93 % (689697)Time elapsed: 0.341 s
% 39.15/5.93 % (689697)Peak memory usage: 31 MB
% 39.15/5.93 % (689697)Instructions burned: 684 (million)
% 39.15/5.93 % TRYING [3]
% 39.15/5.93 % (689707)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2552789233:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 39.15/5.93 % (689708)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2561970830:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 39.15/5.93 % (689709)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3851208676:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 39.15/5.93 % (689705)Instruction limit reached!
% 39.15/5.93 % (689705)------------------------------
% 39.15/5.93 % (689705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.15/5.93 % (689705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.15/5.93 % (689705)CaDiCaL version: 2.1.3
% 39.15/5.93 % (689705)Termination reason: Instruction limit
% 39.15/5.93 % (689705)Termination phase: Finite model building preprocessing
% 39.15/5.93 % (689705)Time elapsed: 0.427 s
% 39.15/5.93 % (689705)Peak memory usage: 42 MB
% 39.15/5.93 % (689705)Instructions burned: 866 (million)
% 39.15/5.93 % (689713)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2531528734:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 39.15/5.93 % (689709)Instruction limit reached!
% 39.15/5.93 % (689709)------------------------------
% 39.15/5.93 % (689709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.15/5.93 % (689709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.15/5.93 % (689709)CaDiCaL version: 2.1.3
% 92.39/13.48 % (689709)Termination reason: Instruction limit
% 92.39/13.48 % (689709)Termination phase: Saturation
% 92.39/13.48 % (689709)Time elapsed: 0.376 s
% 92.39/13.48 % (689709)Peak memory usage: 35 MB
% 92.39/13.48 % (689709)Instructions burned: 693 (million)
% 92.39/13.48 % TRYING [4]
% 92.39/13.48 % (689715)fmb+10_1_sil=64000:random_seed=3562231239:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 92.39/13.48 % (689708)Instruction limit reached!
% 92.39/13.48 % (689708)------------------------------
% 92.39/13.48 % (689708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.39/13.48 % (689708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.39/13.48 % (689708)CaDiCaL version: 2.1.3
% 92.39/13.48 % (689708)Termination reason: Instruction limit
% 92.39/13.48 % (689708)Termination phase: Finite model building preprocessing
% 92.39/13.48 % (689708)Time elapsed: 0.430 s
% 92.39/13.48 % (689708)Peak memory usage: 40 MB
% 92.39/13.48 % (689708)Instructions burned: 891 (million)
% 92.39/13.48 % (689717)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1648071823:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 92.39/13.48 % (689707)Instruction limit reached!
% 92.39/13.48 % (689707)------------------------------
% 92.39/13.48 % (689707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.39/13.48 % (689707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.39/13.48 % (689707)CaDiCaL version: 2.1.3
% 92.39/13.48 % (689707)Termination reason: Instruction limit
% 92.39/13.48 % (689707)Termination phase: Saturation
% 92.39/13.48 % (689707)Time elapsed: 0.613 s
% 92.39/13.48 % (689707)Peak memory usage: 35 MB
% 92.39/13.48 % (689707)Instructions burned: 1179 (million)
% 92.39/13.48 % (689713)Instruction limit reached!
% 92.39/13.48 % (689713)------------------------------
% 92.39/13.48 % (689713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.39/13.48 % (689713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.39/13.48 % (689713)CaDiCaL version: 2.1.3
% 92.39/13.48 % (689713)Termination reason: Instruction limit
% 92.39/13.48 % (689713)Termination phase: Saturation
% 92.39/13.48 % (689713)Time elapsed: 0.403 s
% 92.39/13.48 % (689713)Peak memory usage: 38 MB
% 92.39/13.48 % (689713)Instructions burned: 880 (million)
% 92.39/13.48 % (689719)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2417846941:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 92.39/13.48 % (689721)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=656779159:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 92.39/13.48 % TRYING [1]
% 92.39/13.48 % (689717)Cannot represent all propositional literals internally
% 92.39/13.48 % (689717)Refutation not found, incomplete strategy
% 92.39/13.48 % (689717)------------------------------
% 92.39/13.48 % (689717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.39/13.48 % (689717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.39/13.48 % (689717)CaDiCaL version: 2.1.3
% 92.39/13.48 % (689717)Termination reason: Refutation not found, incomplete strategy
% 92.39/13.48 % (689717)Time elapsed: 0.553 s
% 92.39/13.48 % (689717)Peak memory usage: 44 MB
% 92.39/13.48 % (689717)Instructions burned: 1161 (million)
% 92.39/13.48 % (689717)------------------------------
% 92.39/13.48 % (689717)------------------------------
% 92.39/13.48 % TRYING [2]
% 92.39/13.48 % (689723)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=648986888:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 92.39/13.48 % (689719)Instruction limit reached!
% 92.39/13.48 % (689719)------------------------------
% 92.39/13.48 % (689719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.39/13.48 % (689719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.39/13.48 % (689719)CaDiCaL version: 2.1.3
% 92.39/13.48 % (689719)Termination reason: Instruction limit
% 92.39/13.48 % (689719)Termination phase: Finite model building preprocessing
% 92.39/13.48 % (689719)Time elapsed: 0.453 s
% 92.39/13.48 % (689719)Peak memory usage: 41 MB
% 92.39/13.48 % (689719)Instructions burned: 920 (million)
% 92.39/13.48 % (689725)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4169848409:i=6324_2982 on theBenchmark for (2982ds/6324Mi)
% 92.39/13.48 % (689725)Cannot represent all propositional literals internally
% 92.39/13.48 % (689725)Refutation not found, incomplete strategy
% 92.39/13.48 % (689725)------------------------------
% 92.39/13.48 % (689725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.39/13.48 % (689725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 230.75/33.01 % (689725)CaDiCaL version: 2.1.3
% 230.75/33.01 % (689725)Termination reason: Refutation not found, incomplete strategy
% 230.75/33.01 % (689725)Time elapsed: 0.601 s
% 230.75/33.01 % (689725)Peak memory usage: 44 MB
% 230.75/33.01 % (689725)Instructions burned: 1216 (million)
% 230.75/33.01 % (689725)------------------------------
% 230.75/33.01 % (689725)------------------------------
% 230.75/33.01 % (689727)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=334129686:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi)
% 230.75/33.01 % (689723)Instruction limit reached!
% 230.75/33.01 % (689723)------------------------------
% 230.75/33.01 % (689723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 230.75/33.01 % (689723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 230.75/33.01 % (689723)CaDiCaL version: 2.1.3
% 230.75/33.01 % (689723)Termination reason: Instruction limit
% 230.75/33.01 % (689723)Termination phase: Saturation
% 230.75/33.01 % (689723)Time elapsed: 0.755 s
% 230.75/33.01 % (689723)Peak memory usage: 38 MB
% 230.75/33.01 % (689723)Instructions burned: 1472 (million)
% 230.75/33.01 % (689729)ott-2_1_sil=16000:newcnf=on:random_seed=2152776973:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2975 on theBenchmark for (2975ds/869Mi)
% 230.75/33.01 % TRYING [3]
% 230.75/33.01 % (689729)Instruction limit reached!
% 230.75/33.01 % (689729)------------------------------
% 230.75/33.01 % (689729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 230.75/33.01 % (689729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 230.75/33.01 % (689729)CaDiCaL version: 2.1.3
% 230.75/33.01 % (689729)Termination reason: Instruction limit
% 230.75/33.01 % (689729)Termination phase: Saturation
% 230.75/33.01 % (689729)Time elapsed: 0.457 s
% 230.75/33.01 % (689729)Peak memory usage: 35 MB
% 230.75/33.01 % (689729)Instructions burned: 869 (million)
% 230.75/33.01 % (689731)ott+10_1_sil=32000:tgt=ground:random_seed=2160552994:i=5114:av=off_2970 on theBenchmark for (2970ds/5114Mi)
% 230.75/33.01 % (689727)Instruction limit reached!
% 230.75/33.01 % (689727)------------------------------
% 230.75/33.01 % (689727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 230.75/33.01 % (689727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 230.75/33.01 % (689727)CaDiCaL version: 2.1.3
% 230.75/33.01 % (689727)Termination reason: Instruction limit
% 230.75/33.01 % (689727)Termination phase: Finite model building preprocessing
% 230.75/33.01 % (689727)Time elapsed: 1.059 s
% 230.75/33.01 % (689727)Peak memory usage: 67 MB
% 230.75/33.01 % (689727)Instructions burned: 2175 (million)
% 230.75/33.01 % (689733)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3614827984:i=54282_2965 on theBenchmark for (2965ds/54282Mi)
% 230.75/33.01 % TRYING [5]
% 230.75/33.01 % (689721)Instruction limit reached!
% 230.75/33.01 % (689721)------------------------------
% 230.75/33.01 % (689721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 230.75/33.01 % (689721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 230.75/33.01 % (689721)CaDiCaL version: 2.1.3
% 230.75/33.01 % (689721)Termination reason: Instruction limit
% 230.75/33.01 % (689721)Termination phase: Saturation
% 230.75/33.01 % (689721)Time elapsed: 2.681 s
% 230.75/33.01 % (689721)Peak memory usage: 56 MB
% 230.75/33.01 % (689721)Instructions burned: 5132 (million)
% 230.75/33.01 % (689735)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2312319554:i=3512:aac=none_2960 on theBenchmark for (2960ds/3512Mi)
% 230.75/33.01 % TRYING [1]
% 230.75/33.01 % TRYING [2]
% 230.75/33.01 % TRYING [3]
% 230.75/33.01 % TRYING [4]
% 230.75/33.01 % (689731)Instruction limit reached!
% 230.75/33.01 % (689731)------------------------------
% 230.75/33.01 % (689731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 230.75/33.01 % (689731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 230.75/33.01 % (689731)CaDiCaL version: 2.1.3
% 230.75/33.01 % (689731)Termination reason: Instruction limit
% 230.75/33.01 % (689731)Termination phase: Saturation
% 230.75/33.01 % (689731)Time elapsed: 2.628 s
% 230.75/33.01 % (689731)Peak memory usage: 75 MB
% 230.75/33.01 % (689731)Instructions burned: 5114 (million)
% 230.75/33.01 % (689737)dis+21_1_sil=32000:sas=cadical:random_seed=3596212454:i=3773:amm=off_2944 on theBenchmark for (2944ds/3773Mi)
% 230.75/33.01 % (689735)Instruction limit reached!
% 230.75/33.01 % (689735)------------------------------
% 230.75/33.01 % (689735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 230.75/33.01 % (689735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 230.75/33.01 % (689735)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689735)Termination reason: Instruction limit
% 184.13/39.71 % (689735)Termination phase: Saturation
% 184.13/39.71 % (689735)Time elapsed: 1.665 s
% 184.13/39.71 % (689735)Peak memory usage: 57 MB
% 184.13/39.71 % (689735)Instructions burned: 3513 (million)
% 184.13/39.71 % (689739)ott+11_1_sil=16000:gs=on:random_seed=3374240637:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2943 on theBenchmark for (2943ds/2251Mi)
% 184.13/39.71 % TRYING [4]
% 184.13/39.71 % (689739)Instruction limit reached!
% 184.13/39.71 % (689739)------------------------------
% 184.13/39.71 % (689739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689739)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689739)Termination reason: Instruction limit
% 184.13/39.71 % (689739)Termination phase: Saturation
% 184.13/39.71 % (689739)Time elapsed: 1.240 s
% 184.13/39.71 % (689739)Peak memory usage: 100 MB
% 184.13/39.71 % (689739)Instructions burned: 2253 (million)
% 184.13/39.71 % (689741)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4226375416:fmbsr=1.6:i=67534_2930 on theBenchmark for (2930ds/67534Mi)
% 184.13/39.71 % (689737)Instruction limit reached!
% 184.13/39.71 % (689737)------------------------------
% 184.13/39.71 % (689737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689737)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689737)Termination reason: Instruction limit
% 184.13/39.71 % (689737)Termination phase: Saturation
% 184.13/39.71 % (689737)Time elapsed: 1.821 s
% 184.13/39.71 % (689737)Peak memory usage: 57 MB
% 184.13/39.71 % (689737)Instructions burned: 3774 (million)
% 184.13/39.71 % (689743)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=554855691:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2925 on theBenchmark for (2925ds/4591Mi)
% 184.13/39.71 % (689743)Instruction limit reached!
% 184.13/39.71 % (689743)------------------------------
% 184.13/39.71 % (689743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689743)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689743)Termination reason: Instruction limit
% 184.13/39.71 % (689743)Termination phase: Saturation
% 184.13/39.71 % (689743)Time elapsed: 1.918 s
% 184.13/39.71 % (689743)Peak memory usage: 51 MB
% 184.13/39.71 % (689743)Instructions burned: 4592 (million)
% 184.13/39.71 % (689745)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3420030926:i=29340_2906 on theBenchmark for (2906ds/29340Mi)
% 184.13/39.71 % TRYING [5]
% 184.13/39.71 % (689715)Instruction limit reached!
% 184.13/39.71 % (689715)------------------------------
% 184.13/39.71 % (689715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689715)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689715)Termination reason: Instruction limit
% 184.13/39.71 % (689715)Termination phase: Finite model building SAT solving
% 184.13/39.71 % (689715)Time elapsed: 9.656 s
% 184.13/39.71 % (689715)Peak memory usage: 369 MB
% 184.13/39.71 % (689715)Instructions burned: 22062 (million)
% 184.13/39.71 % (689747)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3631600509:i=5211_2892 on theBenchmark for (2892ds/5211Mi)
% 184.13/39.71 % TRYING [7]
% 184.13/39.71 % (689747)Instruction limit reached!
% 184.13/39.71 % (689747)------------------------------
% 184.13/39.71 % (689747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689747)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689747)Termination reason: Instruction limit
% 184.13/39.71 % (689747)Termination phase: Saturation
% 184.13/39.71 % (689747)Time elapsed: 1.861 s
% 184.13/39.71 % (689747)Peak memory usage: 45 MB
% 184.13/39.71 % (689747)Instructions burned: 5214 (million)
% 184.13/39.71 % (689749)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2147235669:i=5497:nm=2_2873 on theBenchmark for (2873ds/5497Mi)
% 184.13/39.71 % (689749)Cannot represent all propositional literals internally
% 184.13/39.71 % (689749)Refutation not found, incomplete strategy
% 184.13/39.71 % (689749)------------------------------
% 184.13/39.71 % (689749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689749)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689749)Termination reason: Refutation not found, incomplete strategy
% 184.13/39.71 % (689749)Time elapsed: 0.560 s
% 184.13/39.71 % (689749)Peak memory usage: 43 MB
% 184.13/39.71 % (689749)Instructions burned: 1052 (million)
% 184.13/39.71 % (689749)------------------------------
% 184.13/39.71 % (689749)------------------------------
% 184.13/39.71 % (689751)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=501783611:fmbsr=2:i=46332_2867 on theBenchmark for (2867ds/46332Mi)
% 184.13/39.71 % (689751)Cannot represent all propositional literals internally
% 184.13/39.71 % (689751)Refutation not found, incomplete strategy
% 184.13/39.71 % (689751)------------------------------
% 184.13/39.71 % (689751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689751)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689751)Termination reason: Refutation not found, incomplete strategy
% 184.13/39.71 % (689751)Time elapsed: 0.639 s
% 184.13/39.71 % (689751)Peak memory usage: 44 MB
% 184.13/39.71 % (689751)Instructions burned: 1351 (million)
% 184.13/39.71 % (689751)------------------------------
% 184.13/39.71 % (689751)------------------------------
% 184.13/39.71 % (689753)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1645332400:i=14071_2860 on theBenchmark for (2860ds/14071Mi)
% 184.13/39.71 % TRYING [12]
% 184.13/39.71 % (689753)Instruction limit reached!
% 184.13/39.71 % (689753)------------------------------
% 184.13/39.71 % (689753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689753)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689753)Termination reason: Instruction limit
% 184.13/39.71 % (689753)Termination phase: Finite model building constraint generation
% 184.13/39.71 % (689753)Time elapsed: 5.010 s
% 184.13/39.71 % (689753)Peak memory usage: 761 MB
% 184.13/39.71 % (689753)Instructions burned: 14072 (million)
% 184.13/39.71 % (689755)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3572605230:i=22565:add=on:rawr=on_2809 on theBenchmark for (2809ds/22565Mi)
% 184.13/39.71 % (689745)Instruction limit reached!
% 184.13/39.71 % (689745)------------------------------
% 184.13/39.71 % (689745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689745)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689745)Termination reason: Instruction limit
% 184.13/39.71 % (689745)Termination phase: Saturation
% 184.13/39.71 % (689745)Time elapsed: 14.358 s
% 184.13/39.71 % (689745)Peak memory usage: 246 MB
% 184.13/39.71 % (689745)Instructions burned: 29341 (million)
% 184.13/39.71 % (689757)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1152715094:i=8173:av=off_2761 on theBenchmark for (2761ds/8173Mi)
% 184.13/39.71 % TRYING [6]
% 184.13/39.71 % (689757)Instruction limit reached!
% 184.13/39.71 % (689757)------------------------------
% 184.13/39.71 % (689757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689757)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689757)Termination reason: Instruction limit
% 184.13/39.71 % (689757)Termination phase: Saturation
% 184.13/39.71 % (689757)Time elapsed: 4.623 s
% 184.13/39.71 % (689757)Peak memory usage: 104 MB
% 184.13/39.71 % (689757)Instructions burned: 8174 (million)
% 184.13/39.71 % (689759)dis+10_16:1_sil=16000:random_seed=1159112615:i=9155:fsr=off_2715 on theBenchmark for (2715ds/9155Mi)
% 184.13/39.71 % (689741)Instruction limit reached!
% 184.13/39.71 % (689741)------------------------------
% 184.13/39.71 % (689741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689741)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689741)Termination reason: Instruction limit
% 184.13/39.71 % (689741)Termination phase: Finite model building constraint generation
% 184.13/39.71 % (689741)Time elapsed: 24.057 s
% 184.13/39.71 % (689741)Peak memory usage: 3470 MB
% 184.13/39.71 % (689741)Instructions burned: 67537 (million)
% 184.13/39.71 % (689761)ott-3_8_sil=64000:random_seed=246473234:i=20139:bs=on_2684 on theBenchmark for (2684ds/20139Mi)
% 184.13/39.71 % (689759)Instruction limit reached!
% 184.13/39.71 % (689759)------------------------------
% 184.13/39.71 % (689759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689759)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689759)Termination reason: Instruction limit
% 184.13/39.71 % (689759)Termination phase: Saturation
% 184.13/39.71 % (689759)Time elapsed: 4.270 s
% 184.13/39.71 % (689759)Peak memory usage: 98 MB
% 184.13/39.71 % (689759)Instructions burned: 9157 (million)
% 184.13/39.71 % (689763)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=819485626:fmbsr=2:i=32576_2672 on theBenchmark for (2672ds/32576Mi)
% 184.13/39.71 % (689755)Instruction limit reached!
% 184.13/39.71 % (689755)------------------------------
% 184.13/39.71 % (689755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689755)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689755)Termination reason: Instruction limit
% 184.13/39.71 % (689755)Termination phase: Saturation
% 184.13/39.71 % (689755)Time elapsed: 13.973 s
% 184.13/39.71 % (689755)Peak memory usage: 389 MB
% 184.13/39.71 % (689755)Instructions burned: 22565 (million)
% 184.13/39.71 % (689765)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1666724312:i=11404_2668 on theBenchmark for (2668ds/11404Mi)
% 184.13/39.71 % TRYING [9]
% 184.13/39.71 % (689733)Instruction limit reached!
% 184.13/39.71 % (689733)------------------------------
% 184.13/39.71 % (689733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689733)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689733)Termination reason: Instruction limit
% 184.13/39.71 % (689733)Termination phase: Finite model building SAT solving
% 184.13/39.71 % (689733)Time elapsed: 31.133 s
% 184.13/39.71 % (689733)Peak memory usage: 1760 MB
% 184.13/39.71 % (689733)Instructions burned: 54282 (million)
% 184.13/39.71 % (689767)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1383101519:i=14134_2651 on theBenchmark for (2651ds/14134Mi)
% 184.13/39.71 % (689765)Instruction limit reached!
% 184.13/39.71 % (689765)------------------------------
% 184.13/39.71 % (689765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.71 % (689765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.71 % (689765)CaDiCaL version: 2.1.3
% 184.13/39.71 % (689765)Termination reason: Instruction limit
% 184.13/39.71 % (689765)Termination phase: Saturation
% 184.13/39.71 % (689765)Time elapsed: 5.939 s
% 184.13/39.71 % (689765)Peak memory usage: 181 MB
% 184.13/39.71 % (689765)Instructions burned: 11405 (million)
% 184.13/39.71 % (689770)dis+33_16_sil=32000:sac=on:random_seed=3143009977:i=15851:nm=0_2609 on theBenchmark for (2609ds/15851Mi)
% 184.13/39.71 % (689767) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-689676-689767"...
% 184.13/39.71 % (689767)...printing done.
% 184.13/39.71 % (689767)Refutation found. Thanks to Tanya!
% 184.13/39.71 % SZS status Theorem for theBenchmark
% 184.13/39.71 % SZS output start Proof for theBenchmark
% See solution above
% 184.13/39.72 % (689767)------------------------------
% 184.13/39.72 % (689767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.13/39.72 % (689767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.13/39.72 % (689767)CaDiCaL version: 2.1.3
% 184.13/39.72 % (689767)Termination reason: Refutation
% 184.13/39.72 % (689767)Time elapsed: 4.265 s
% 184.13/39.72 % (689767)Peak memory usage: 86 MB
% 184.13/39.72 % (689767)Instructions burned: 7600 (million)
% 184.13/39.72 % (689676)Success in time 39.456 s
% 184.13/39.72 % Vampire exiting
%------------------------------------------------------------------------------