%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU170+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:52:14 PM UTC 2026
% Result : Theorem 15.50s 5.43s
% Output : Refutation 15.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 21
% Syntax : Number of formulae : 121 ( 50 unt; 2 def)
% Number of atoms : 289 ( 57 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 260 ( 92 ~; 103 |; 40 &)
% ( 11 <=>; 13 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-2 aty)
% Number of variables : 175 ( 157 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_xboole_0) ).
fof(f5,axiom,
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(f10,axiom,
! [X0,X1] :
( ( ~ empty(X0)
=> ( element(X1,X0)
<=> in(X1,X0) ) )
& ( empty(X0)
=> ( element(X1,X0)
<=> empty(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f14,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f16,axiom,
! [X0,X1] :
( X1 = union(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] :
( in(X2,X3)
& in(X3,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_tarski) ).
fof(f18,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> subset_complement(X0,X1) = set_difference(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_subset_1) ).
fof(f35,axiom,
! [X0] : ~ empty(powerset(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f60,axiom,
! [X0,X1] :
( disjoint(X0,X1)
=> disjoint(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_r1_xboole_0) ).
fof(f65,axiom,
! [X0,X1] :
( subset(X0,X1)
=> set_union2(X0,X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_xboole_1) ).
fof(f73,axiom,
! [X0,X1] :
( subset(X0,X1)
=> set_intersection2(X0,X1) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t28_xboole_1) ).
fof(f77,axiom,
! [X0,X1,X2] :
( subset(X0,X1)
=> subset(set_difference(X0,X2),set_difference(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t33_xboole_1) ).
fof(f79,axiom,
! [X0,X1] : subset(set_difference(X0,X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t36_xboole_1) ).
fof(f83,axiom,
! [X0,X1] : set_union2(X0,set_difference(X1,X0)) = set_union2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t39_xboole_1) ).
fof(f88,axiom,
! [X0,X1] : set_difference(set_union2(X0,X1),X1) = set_difference(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t40_xboole_1) ).
fof(f89,conjecture,
! [X0,X1] :
( element(X1,powerset(X0))
=> ! [X2] :
( element(X2,powerset(X0))
=> ( disjoint(X1,X2)
<=> subset(X1,subset_complement(X0,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t43_subset_1) ).
fof(f90,negated_conjecture,
~ ! [X0,X1] :
( element(X1,powerset(X0))
=> ! [X2] :
( element(X2,powerset(X0))
=> ( disjoint(X1,X2)
<=> subset(X1,subset_complement(X0,X2)) ) ) ),
inference(negated_conjecture,[status(cth)],[f89]) ).
fof(f93,axiom,
! [X0,X1] : set_difference(X0,set_difference(X0,X1)) = set_intersection2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f97,axiom,
! [X0,X1,X2] :
( ( subset(X0,X1)
& disjoint(X1,X2) )
=> disjoint(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_xboole_1) ).
fof(f104,axiom,
! [X0,X1] :
( disjoint(X0,X1)
<=> set_difference(X0,X1) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t83_xboole_1) ).
fof(f109,axiom,
! [X0] : union(powerset(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t99_zfmisc_1) ).
fof(f125,plain,
! [X0,X1] :
( ( ( element(X1,X0)
<=> in(X1,X0) )
| empty(X0) )
& ( ( element(X1,X0)
<=> empty(X1) )
| ~ empty(X0) ) ),
inference(ennf_transformation,[],[f10]) ).
fof(f126,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f14]) ).
fof(f127,plain,
! [X0,X1] :
( subset_complement(X0,X1) = set_difference(X0,X1)
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f18]) ).
fof(f142,plain,
! [X0,X1] :
( disjoint(X1,X0)
| ~ disjoint(X0,X1) ),
inference(ennf_transformation,[],[f60]) ).
fof(f147,plain,
! [X0,X1] :
( set_union2(X0,X1) = X1
| ~ subset(X0,X1) ),
inference(ennf_transformation,[],[f65]) ).
fof(f155,plain,
! [X0,X1] :
( set_intersection2(X0,X1) = X0
| ~ subset(X0,X1) ),
inference(ennf_transformation,[],[f73]) ).
fof(f157,plain,
! [X0,X1,X2] :
( subset(set_difference(X0,X2),set_difference(X1,X2))
| ~ subset(X0,X1) ),
inference(ennf_transformation,[],[f77]) ).
fof(f161,plain,
? [X0,X1] :
( ? [X2] :
( ( disjoint(X1,X2)
<~> subset(X1,subset_complement(X0,X2)) )
& element(X2,powerset(X0)) )
& element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f90]) ).
fof(f166,plain,
! [X0,X1,X2] :
( disjoint(X0,X2)
| ~ subset(X0,X1)
| ~ disjoint(X1,X2) ),
inference(ennf_transformation,[],[f97]) ).
fof(f167,plain,
! [X0,X1,X2] :
( disjoint(X0,X2)
| ~ subset(X0,X1)
| ~ disjoint(X1,X2) ),
inference(flattening,[],[f166]) ).
fof(f190,plain,
! [X0,X1] :
( ( ( ( element(X1,X0)
| ~ in(X1,X0) )
& ( in(X1,X0)
| ~ element(X1,X0) ) )
| empty(X0) )
& ( ( ( element(X1,X0)
| ~ empty(X1) )
& ( empty(X1)
| ~ element(X1,X0) ) )
| ~ empty(X0) ) ),
inference(nnf_transformation,[],[f125]) ).
fof(f202,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) )
| ~ subset(X0,X1) ) ),
inference(nnf_transformation,[],[f126]) ).
fof(f203,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(rectify,[],[f202]) ).
fof(f204,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ( ~ in(sK10(X0,X1),X1)
& in(sK10(X0,X1),X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X2,sK10(X0,X1))],[f203]) ).
fof(f209,plain,
! [X0,X1] :
( ( X1 = union(X0)
| ? [X2] :
( ( ! [X3] :
( ~ in(X2,X3)
| ~ in(X3,X0) )
| ~ in(X2,X1) )
& ( ? [X3] :
( in(X2,X3)
& in(X3,X0) )
| in(X2,X1) ) ) )
& ( ! [X2] :
( ( in(X2,X1)
| ! [X3] :
( ~ in(X2,X3)
| ~ in(X3,X0) ) )
& ( ? [X3] :
( in(X2,X3)
& in(X3,X0) )
| ~ in(X2,X1) ) )
| union(X0) != X1 ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f210,plain,
! [X0,X1] :
( ( X1 = union(X0)
| ? [X2] :
( ( ! [X3] :
( ~ in(X2,X3)
| ~ in(X3,X0) )
| ~ in(X2,X1) )
& ( ? [X4] :
( in(X2,X4)
& in(X4,X0) )
| in(X2,X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] :
( ~ in(X5,X6)
| ~ in(X6,X0) ) )
& ( ? [X7] :
( in(X5,X7)
& in(X7,X0) )
| ~ in(X5,X1) ) )
| union(X0) != X1 ) ),
inference(rectify,[],[f209]) ).
fof(f211,plain,
! [X0,X1] :
( ( X1 = union(X0)
| ( ( ! [X3] :
( ~ in(sK12(X0,X1),X3)
| ~ in(X3,X0) )
| ~ in(sK12(X0,X1),X1) )
& ( ( in(sK12(X0,X1),sK13(X0,X1))
& in(sK13(X0,X1),X0) )
| in(sK12(X0,X1),X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] :
( ~ in(X5,X6)
| ~ in(X6,X0) ) )
& ( ( in(X5,sK14(X0,X5))
& in(sK14(X0,X5),X0) )
| ~ in(X5,X1) ) )
| union(X0) != X1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14]),skolemize(X2,sK12(X0,X1)),skolemize(X4,sK13(X0,X1)),skolemize(X7,sK14(X0,X5))],[f210]) ).
fof(f240,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ subset(X1,subset_complement(X0,X2))
| ~ disjoint(X1,X2) )
& ( subset(X1,subset_complement(X0,X2))
| disjoint(X1,X2) )
& element(X2,powerset(X0)) )
& element(X1,powerset(X0)) ),
inference(nnf_transformation,[],[f161]) ).
fof(f241,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ subset(X1,subset_complement(X0,X2))
| ~ disjoint(X1,X2) )
& ( subset(X1,subset_complement(X0,X2))
| disjoint(X1,X2) )
& element(X2,powerset(X0)) )
& element(X1,powerset(X0)) ),
inference(flattening,[],[f240]) ).
fof(f242,plain,
( ( ~ subset(sK25,subset_complement(sK24,sK26))
| ~ disjoint(sK25,sK26) )
& ( subset(sK25,subset_complement(sK24,sK26))
| disjoint(sK25,sK26) )
& element(sK26,powerset(sK24))
& element(sK25,powerset(sK24)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24,sK25,sK26]),skolemize(X0,sK24),skolemize(X1,sK25),skolemize(X2,sK26)],[f241]) ).
fof(f245,plain,
! [X0,X1] :
( ( disjoint(X0,X1)
| set_difference(X0,X1) != X0 )
& ( set_difference(X0,X1) = X0
| ~ disjoint(X0,X1) ) ),
inference(nnf_transformation,[],[f104]) ).
fof(f250,plain,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
inference(cnf_transformation,[],[f4]) ).
fof(f251,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[],[f5]) ).
fof(f267,plain,
! [X0,X1] :
( ~ element(X1,X0)
| in(X1,X0)
| empty(X0) ),
inference(cnf_transformation,[],[f190]) ).
fof(f290,plain,
! [X0,X1] :
( in(sK10(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f204]) ).
fof(f291,plain,
! [X0,X1] :
( ~ in(sK10(X0,X1),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f204]) ).
fof(f300,plain,
! [X0,X1,X6,X5] :
( in(X5,X1)
| ~ in(X5,X6)
| ~ in(X6,X0)
| union(X0) != X1 ),
inference(cnf_transformation,[],[f211]) ).
fof(f310,plain,
! [X0,X1] :
( ~ element(X1,powerset(X0))
| set_difference(X0,X1) = subset_complement(X0,X1) ),
inference(cnf_transformation,[],[f127]) ).
fof(f317,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[],[f35]) ).
fof(f350,plain,
! [X0,X1] :
( ~ disjoint(X0,X1)
| disjoint(X1,X0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f358,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| set_union2(X0,X1) = X1 ),
inference(cnf_transformation,[],[f147]) ).
fof(f368,plain,
! [X0,X1] :
( set_intersection2(X0,X1) = X0
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f155]) ).
fof(f373,plain,
! [X2,X0,X1] :
( subset(set_difference(X0,X2),set_difference(X1,X2))
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f157]) ).
fof(f376,plain,
! [X0,X1] : subset(set_difference(X0,X1),X0),
inference(cnf_transformation,[],[f79]) ).
fof(f384,plain,
! [X0,X1] : set_union2(X0,X1) = set_union2(X0,set_difference(X1,X0)),
inference(cnf_transformation,[],[f83]) ).
fof(f393,plain,
! [X0,X1] : set_difference(X0,X1) = set_difference(set_union2(X0,X1),X1),
inference(cnf_transformation,[],[f88]) ).
fof(f394,plain,
element(sK25,powerset(sK24)),
inference(cnf_transformation,[],[f242]) ).
fof(f395,plain,
element(sK26,powerset(sK24)),
inference(cnf_transformation,[],[f242]) ).
fof(f396,plain,
( subset(sK25,subset_complement(sK24,sK26))
| disjoint(sK25,sK26) ),
inference(cnf_transformation,[],[f242]) ).
fof(f397,plain,
( ~ subset(sK25,subset_complement(sK24,sK26))
| ~ disjoint(sK25,sK26) ),
inference(cnf_transformation,[],[f242]) ).
fof(f400,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_difference(X0,set_difference(X0,X1)),
inference(cnf_transformation,[],[f93]) ).
fof(f405,plain,
! [X2,X0,X1] :
( ~ disjoint(X1,X2)
| ~ subset(X0,X1)
| disjoint(X0,X2) ),
inference(cnf_transformation,[],[f167]) ).
fof(f413,plain,
! [X0,X1] :
( ~ disjoint(X0,X1)
| set_difference(X0,X1) = X0 ),
inference(cnf_transformation,[],[f245]) ).
fof(f414,plain,
! [X0,X1] :
( set_difference(X0,X1) != X0
| disjoint(X0,X1) ),
inference(cnf_transformation,[],[f245]) ).
fof(f419,plain,
! [X0] : union(powerset(X0)) = X0,
inference(cnf_transformation,[],[f109]) ).
fof(f426,plain,
! [X0,X1] : set_difference(X0,set_difference(X0,X1)) = set_difference(X1,set_difference(X1,X0)),
inference(definition_unfolding,[],[f251,f400,f400]) ).
fof(f465,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| set_difference(X0,set_difference(X0,X1)) = X0 ),
inference(definition_unfolding,[],[f368,f400]) ).
fof(f506,plain,
! [X0,X6,X5] :
( ~ in(X6,X0)
| ~ in(X5,X6)
| in(X5,union(X0)) ),
inference(equality_resolution,[],[f300]) ).
fof(f516,definition,
sF30 = subset_complement(sK24,sK26),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f517,plain,
subset_complement(sK24,sK26) = sF30,
inference(reorient_equations,[],[f516]) ).
fof(f518,plain,
( ~ disjoint(sK25,sK26)
| ~ subset(sK25,sF30) ),
inference(definition_folding,[],[f397,f517]) ).
fof(f519,plain,
( disjoint(sK25,sK26)
| subset(sK25,sF30) ),
inference(definition_folding,[],[f396,f517]) ).
fof(f520,definition,
sF31 = powerset(sK24),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f521,plain,
powerset(sK24) = sF31,
inference(reorient_equations,[],[f520]) ).
fof(f522,plain,
element(sK26,sF31),
inference(definition_folding,[],[f395,f521]) ).
fof(f523,plain,
element(sK25,sF31),
inference(definition_folding,[],[f394,f521]) ).
fof(f527,plain,
~ empty(sF31),
inference(superposition,[],[f317,f521]) ).
fof(f528,plain,
sK24 = union(sF31),
inference(superposition,[],[f419,f521]) ).
fof(f569,plain,
( disjoint(sK26,sK25)
| subset(sK25,sF30) ),
inference(resolution,[],[f350,f519]) ).
fof(f802,plain,
( in(sK25,sF31)
| empty(sF31) ),
inference(resolution,[],[f267,f523]) ).
fof(f803,plain,
( in(sK26,sF31)
| empty(sF31) ),
inference(resolution,[],[f267,f522]) ).
fof(f804,plain,
in(sK26,sF31),
inference(forward_subsumption_resolution,[],[f803,f527]) ).
fof(f805,plain,
in(sK25,sF31),
inference(forward_subsumption_resolution,[],[f802,f527]) ).
fof(f942,plain,
! [X0,X1] : set_difference(X1,X0) = set_difference(set_union2(X0,X1),X0),
inference(superposition,[],[f393,f250]) ).
fof(f978,plain,
! [X0] :
( ~ subset(X0,sK26)
| disjoint(X0,sK25)
| subset(sK25,sF30) ),
inference(resolution,[],[f405,f569]) ).
fof(f1038,plain,
! [X0] :
( disjoint(set_difference(sK26,X0),sK25)
| subset(sK25,sF30) ),
inference(resolution,[],[f978,f376]) ).
fof(f1046,plain,
! [X0] :
( disjoint(sK25,set_difference(sK26,X0))
| subset(sK25,sF30) ),
inference(resolution,[],[f1038,f350]) ).
fof(f1449,plain,
! [X0] :
( ~ in(X0,sK25)
| in(X0,union(sF31)) ),
inference(resolution,[],[f506,f805]) ).
fof(f1450,plain,
! [X0] :
( ~ in(X0,sK26)
| in(X0,union(sF31)) ),
inference(resolution,[],[f506,f804]) ).
fof(f1454,plain,
! [X0] :
( ~ in(X0,sK26)
| in(X0,sK24) ),
inference(forward_demodulation,[],[f1450,f528]) ).
fof(f1455,plain,
! [X0] :
( ~ in(X0,sK25)
| in(X0,sK24) ),
inference(forward_demodulation,[],[f1449,f528]) ).
fof(f1498,plain,
! [X0] :
( in(sK10(sK26,X0),sK24)
| subset(sK26,X0) ),
inference(resolution,[],[f1454,f290]) ).
fof(f1529,plain,
! [X0] :
( in(sK10(sK25,X0),sK24)
| subset(sK25,X0) ),
inference(resolution,[],[f1455,f290]) ).
fof(f1619,plain,
! [X0] :
( ~ element(X0,sF31)
| subset_complement(sK24,X0) = set_difference(sK24,X0) ),
inference(superposition,[],[f310,f521]) ).
fof(f2413,plain,
( subset(sK26,sK24)
| subset(sK26,sK24) ),
inference(resolution,[],[f1498,f291]) ).
fof(f2419,plain,
subset(sK26,sK24),
inference(duplicate_literal_removal,[],[f2413]) ).
fof(f2438,plain,
sK24 = set_union2(sK26,sK24),
inference(resolution,[],[f2419,f358]) ).
fof(f2443,plain,
sK26 = set_difference(sK26,set_difference(sK26,sK24)),
inference(resolution,[],[f2419,f465]) ).
fof(f4477,plain,
( subset(sK25,sK24)
| subset(sK25,sK24) ),
inference(resolution,[],[f1529,f291]) ).
fof(f4483,plain,
subset(sK25,sK24),
inference(duplicate_literal_removal,[],[f4477]) ).
fof(f8617,plain,
subset_complement(sK24,sK26) = set_difference(sK24,sK26),
inference(resolution,[],[f1619,f522]) ).
fof(f8628,plain,
sF30 = set_difference(sK24,sK26),
inference(forward_demodulation,[],[f8617,f517]) ).
fof(f8638,plain,
! [X0] :
( subset(set_difference(X0,sK26),sF30)
| ~ subset(X0,sK24) ),
inference(superposition,[],[f373,f8628]) ).
fof(f8641,plain,
set_union2(sK26,sK24) = set_union2(sK26,sF30),
inference(superposition,[],[f384,f8628]) ).
fof(f8644,plain,
set_difference(sK26,set_difference(sK26,sK24)) = set_difference(sK24,sF30),
inference(superposition,[],[f426,f8628]) ).
fof(f8691,plain,
sK26 = set_difference(sK24,sF30),
inference(forward_demodulation,[],[f8644,f2443]) ).
fof(f8693,plain,
sK24 = set_union2(sK26,sF30),
inference(forward_demodulation,[],[f8641,f2438]) ).
fof(f9028,plain,
set_difference(sK24,sF30) = set_difference(sK26,sF30),
inference(superposition,[],[f393,f8693]) ).
fof(f9047,plain,
set_difference(sK24,sK26) = set_difference(sF30,sK26),
inference(superposition,[],[f942,f8693]) ).
fof(f9052,plain,
sF30 = set_difference(sF30,sK26),
inference(forward_demodulation,[],[f9047,f8628]) ).
fof(f9053,plain,
sK26 = set_difference(sK26,sF30),
inference(forward_demodulation,[],[f9028,f8691]) ).
fof(f9131,plain,
( sF30 != sF30
| disjoint(sF30,sK26) ),
inference(superposition,[],[f414,f9052]) ).
fof(f9169,plain,
disjoint(sF30,sK26),
inference(trivial_inequality_removal,[],[f9131]) ).
fof(f9217,plain,
! [X0] :
( ~ subset(X0,sF30)
| disjoint(X0,sK26) ),
inference(resolution,[],[f9169,f405]) ).
fof(f9306,plain,
( disjoint(sK25,sK26)
| subset(sK25,sF30) ),
inference(superposition,[],[f1046,f9053]) ).
fof(f9372,plain,
disjoint(sK25,sK26),
inference(forward_subsumption_resolution,[],[f9306,f9217]) ).
fof(f9386,plain,
~ subset(sK25,sF30),
inference(resolution,[],[f9372,f518]) ).
fof(f9390,plain,
sK25 = set_difference(sK25,sK26),
inference(resolution,[],[f9372,f413]) ).
fof(f38677,plain,
( subset(sK25,sF30)
| ~ subset(sK25,sK24) ),
inference(superposition,[],[f8638,f9390]) ).
fof(f38679,plain,
~ subset(sK25,sK24),
inference(forward_subsumption_resolution,[],[f38677,f9386]) ).
fof(f38688,plain,
$false,
inference(forward_subsumption_resolution,[],[f38679,f4483]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU170+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.37 % Computer : n015.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 28 03:55:31 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.44/2.64 % (2243119)Will run a generic schedule for satisfiability detection.
% 15.44/2.64 % (2243129)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4149904053:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.44/2.64 % (2243125)% WARNING: option uhcvi not known.
% 15.44/2.64 % (2243124)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1337832417_2999 on theBenchmark for (2999ds/0Mi)
% 15.44/2.64 % (2243128)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1906282356:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.44/2.64 % (2243125)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2875241450:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.44/2.64 % (2243126)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2190522235:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.44/2.64 % (2243127)dis+10_1_sil=32000:sp=arity:random_seed=2613857327:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.44/2.64 % (2243130)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1113717197:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.44/2.64 % TRYING [1]
% 15.44/2.64 % TRYING [2]
% 15.44/2.64 % TRYING [3]
% 15.44/2.64 % (2243129)Instruction limit reached!
% 15.44/2.64 % (2243129)------------------------------
% 15.44/2.64 % (2243129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.44/2.64 % (2243129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/2.64 % (2243129)CaDiCaL version: 2.1.3
% 15.44/2.64 % (2243129)Termination reason: Instruction limit
% 15.44/2.64 % (2243129)Termination phase: Saturation
% 15.44/2.64 % (2243129)Time elapsed: 0.047 s
% 15.44/2.64 % (2243129)Peak memory usage: 13 MB
% 15.44/2.64 % (2243129)Instructions burned: 132 (million)
% 15.44/2.64 % TRYING [4]
% 15.44/2.64 % (2243138)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3919170423:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.44/2.64 % TRYING [1]
% 15.44/2.64 % TRYING [2]
% 15.44/2.64 % TRYING [3]
% 15.44/2.64 % (2243127)Instruction limit reached!
% 15.44/2.64 % (2243127)------------------------------
% 15.44/2.64 % (2243127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.44/2.64 % (2243127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/2.64 % (2243127)CaDiCaL version: 2.1.3
% 15.44/2.64 % (2243127)Termination reason: Instruction limit
% 15.44/2.64 % (2243127)Termination phase: Saturation
% 15.44/2.64 % (2243127)Time elapsed: 0.068 s
% 15.44/2.64 % (2243127)Peak memory usage: 12 MB
% 15.44/2.64 % (2243127)Instructions burned: 104 (million)
% 15.44/2.64 % TRYING [4]
% 15.44/2.64 % (2243128)Instruction limit reached!
% 15.44/2.64 % (2243128)------------------------------
% 15.44/2.64 % (2243128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.44/2.64 % (2243128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/2.64 % (2243128)CaDiCaL version: 2.1.3
% 15.44/2.64 % (2243128)Termination reason: Instruction limit
% 15.44/2.64 % (2243128)Termination phase: Saturation
% 15.44/2.64 % (2243128)Time elapsed: 0.076 s
% 15.44/2.64 % (2243128)Peak memory usage: 13 MB
% 15.44/2.64 % (2243128)Instructions burned: 116 (million)
% 15.44/2.64 % (2243140)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=703640522:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.44/2.64 % (2243141)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=2557172899:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.44/2.64 % (2243130)Instruction limit reached!
% 15.44/2.64 % (2243130)------------------------------
% 15.44/2.64 % (2243130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.44/2.64 % (2243130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/2.64 % (2243130)CaDiCaL version: 2.1.3
% 15.44/2.64 % (2243130)Termination reason: Instruction limit
% 15.44/2.64 % (2243130)Termination phase: Saturation
% 15.44/2.64 % (2243130)Time elapsed: 0.097 s
% 15.44/2.64 % (2243130)Peak memory usage: 13 MB
% 15.44/2.64 % (2243130)Instructions burned: 160 (million)
% 15.44/2.64 % TRYING [5]
% 15.44/2.64 % (2243144)ott-21_1_sil=16000:fs=off:random_seed=1673179157:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.44/2.64 % TRYING [5]
% 15.44/2.64 % (2243140)Instruction limit reached!
% 15.44/2.64 % (2243140)------------------------------
% 15.44/2.64 % (2243140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243140)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243140)Termination reason: Instruction limit
% 15.50/5.43 % (2243140)Termination phase: Saturation
% 15.50/5.43 % (2243140)Time elapsed: 0.086 s
% 15.50/5.43 % (2243140)Peak memory usage: 13 MB
% 15.50/5.43 % (2243140)Instructions burned: 131 (million)
% 15.50/5.43 % (2243146)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2798861355:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 15.50/5.43 % TRYING [6]
% 15.50/5.43 % (2243138)Instruction limit reached!
% 15.50/5.43 % (2243138)------------------------------
% 15.50/5.43 % (2243138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243138)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243138)Termination reason: Instruction limit
% 15.50/5.43 % (2243138)Termination phase: Finite model building constraint generation
% 15.50/5.43 % (2243138)Time elapsed: 0.153 s
% 15.50/5.43 % (2243138)Peak memory usage: 36 MB
% 15.50/5.43 % (2243138)Instructions burned: 722 (million)
% 15.50/5.43 % (2243144)Instruction limit reached!
% 15.50/5.43 % (2243144)------------------------------
% 15.50/5.43 % (2243144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243144)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243144)Termination reason: Instruction limit
% 15.50/5.43 % (2243144)Termination phase: Saturation
% 15.50/5.43 % (2243144)Time elapsed: 0.097 s
% 15.50/5.43 % (2243144)Peak memory usage: 13 MB
% 15.50/5.43 % (2243144)Instructions burned: 181 (million)
% 15.50/5.43 % (2243148)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=183593732:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 15.50/5.43 % TRYING [1]
% 15.50/5.43 % TRYING [2]
% 15.50/5.43 % TRYING [3]
% 15.50/5.43 % (2243149)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3866955986:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 15.50/5.43 % TRYING [4]
% 15.50/5.43 % TRYING [5]
% 15.50/5.43 % (2243148)Instruction limit reached!
% 15.50/5.43 % (2243148)------------------------------
% 15.50/5.43 % (2243148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243148)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243148)Termination reason: Instruction limit
% 15.50/5.43 % (2243148)Termination phase: Finite model building constraint generation
% 15.50/5.43 % (2243148)Time elapsed: 0.185 s
% 15.50/5.43 % (2243148)Peak memory usage: 25 MB
% 15.50/5.43 % (2243148)Instructions burned: 870 (million)
% 15.50/5.43 % (2243152)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4227040302:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 15.50/5.43 % TRYING [6]
% 15.50/5.43 % (2243146)Instruction limit reached!
% 15.50/5.43 % (2243146)------------------------------
% 15.50/5.43 % (2243146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243146)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243146)Termination reason: Instruction limit
% 15.50/5.43 % (2243146)Termination phase: Saturation
% 15.50/5.43 % (2243146)Time elapsed: 0.337 s
% 15.50/5.43 % (2243146)Peak memory usage: 15 MB
% 15.50/5.43 % (2243146)Instructions burned: 478 (million)
% 15.50/5.43 % (2243141)Instruction limit reached!
% 15.50/5.43 % (2243141)------------------------------
% 15.50/5.43 % (2243141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243141)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243141)Termination reason: Instruction limit
% 15.50/5.43 % (2243141)Termination phase: Saturation
% 15.50/5.43 % (2243141)Time elapsed: 0.442 s
% 15.50/5.43 % (2243141)Peak memory usage: 18 MB
% 15.50/5.43 % (2243141)Instructions burned: 684 (million)
% 15.50/5.43 % (2243154)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=1319944978:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 15.50/5.43 % (2243155)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=947740117:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 15.50/5.43 % (2243152)Instruction limit reached!
% 15.50/5.43 % (2243152)------------------------------
% 15.50/5.43 % (2243152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243152)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243152)Termination reason: Instruction limit
% 15.50/5.43 % (2243152)Termination phase: Finite model building constraint generation
% 15.50/5.43 % (2243152)Time elapsed: 0.240 s
% 15.50/5.43 % (2243152)Peak memory usage: 109 MB
% 15.50/5.43 % (2243152)Instructions burned: 892 (million)
% 15.50/5.43 % (2243158)fmb+10_1_sil=64000:random_seed=1421214343:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 15.50/5.43 % TRYING [1]
% 15.50/5.43 % TRYING [2]
% 15.50/5.43 % TRYING [3]
% 15.50/5.43 % TRYING [4]
% 15.50/5.43 % TRYING [5]
% 15.50/5.43 % (2243149)Instruction limit reached!
% 15.50/5.43 % (2243149)------------------------------
% 15.50/5.43 % (2243149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243149)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243149)Termination reason: Instruction limit
% 15.50/5.43 % (2243149)Termination phase: Saturation
% 15.50/5.43 % (2243149)Time elapsed: 0.734 s
% 15.50/5.43 % (2243149)Peak memory usage: 23 MB
% 15.50/5.43 % (2243149)Instructions burned: 1180 (million)
% 15.50/5.43 % (2243160)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2047985169:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 15.50/5.43 % TRYING [20]
% 15.50/5.43 % TRYING [6]
% 15.50/5.43 % (2243154)Instruction limit reached!
% 15.50/5.43 % (2243154)------------------------------
% 15.50/5.43 % (2243154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243154)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243154)Termination reason: Instruction limit
% 15.50/5.43 % (2243154)Termination phase: Saturation
% 15.50/5.43 % (2243154)Time elapsed: 0.476 s
% 15.50/5.43 % (2243154)Peak memory usage: 22 MB
% 15.50/5.43 % (2243154)Instructions burned: 693 (million)
% 15.50/5.43 % (2243155)Instruction limit reached!
% 15.50/5.43 % (2243155)------------------------------
% 15.50/5.43 % (2243155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243155)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243155)Termination reason: Instruction limit
% 15.50/5.43 % (2243155)Termination phase: Saturation
% 15.50/5.43 % (2243155)Time elapsed: 0.482 s
% 15.50/5.43 % (2243155)Peak memory usage: 19 MB
% 15.50/5.43 % (2243155)Instructions burned: 880 (million)
% 15.50/5.43 % (2243162)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3252063361:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 15.50/5.43 % (2243163)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3782286643:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 15.50/5.43 % TRYING [8]
% 15.50/5.43 % TRYING [7]
% 15.50/5.43 % (2243162)Instruction limit reached!
% 15.50/5.43 % (2243162)------------------------------
% 15.50/5.43 % (2243162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243162)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243162)Termination reason: Instruction limit
% 15.50/5.43 % (2243162)Termination phase: Finite model building constraint generation
% 15.50/5.43 % (2243162)Time elapsed: 0.314 s
% 15.50/5.43 % (2243162)Peak memory usage: 66 MB
% 15.50/5.43 % (2243162)Instructions burned: 920 (million)
% 15.50/5.43 % (2243166)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2530507125:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 15.50/5.43 % TRYING [7]
% 15.50/5.43 % (2243166)Instruction limit reached!
% 15.50/5.43 % (2243166)------------------------------
% 15.50/5.43 % (2243166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243166)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243166)Termination reason: Instruction limit
% 15.50/5.43 % (2243166)Termination phase: Saturation
% 15.50/5.43 % (2243166)Time elapsed: 0.775 s
% 15.50/5.43 % (2243166)Peak memory usage: 29 MB
% 15.50/5.43 % (2243166)Instructions burned: 1473 (million)
% 15.50/5.43 % (2243168)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1798056465:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 15.50/5.43 % (2243168)Cannot represent all propositional literals internally
% 15.50/5.43 % (2243168)Refutation not found, incomplete strategy
% 15.50/5.43 % (2243168)------------------------------
% 15.50/5.43 % (2243168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243168)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243168)Termination reason: Refutation not found, incomplete strategy
% 15.50/5.43 % (2243168)Time elapsed: 0.012 s
% 15.50/5.43 % (2243168)Peak memory usage: 11 MB
% 15.50/5.43 % (2243168)Instructions burned: 22 (million)
% 15.50/5.43 % (2243168)------------------------------
% 15.50/5.43 % (2243168)------------------------------
% 15.50/5.43 % (2243170)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2869761047:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 15.50/5.43 % TRYING [16]
% 15.50/5.43 % TRYING [8]
% 15.50/5.43 % (2243170)Instruction limit reached!
% 15.50/5.43 % (2243170)------------------------------
% 15.50/5.43 % (2243170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243170)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243170)Termination reason: Instruction limit
% 15.50/5.43 % (2243170)Termination phase: Finite model building constraint generation
% 15.50/5.43 % (2243170)Time elapsed: 0.770 s
% 15.50/5.43 % (2243170)Peak memory usage: 141 MB
% 15.50/5.43 % (2243170)Instructions burned: 2174 (million)
% 15.50/5.43 % (2243173)ott-2_1_sil=16000:newcnf=on:random_seed=513349308:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2969 on theBenchmark for (2969ds/869Mi)
% 15.50/5.43 % TRYING [8]
% 15.50/5.43 % (2243173)Instruction limit reached!
% 15.50/5.43 % (2243173)------------------------------
% 15.50/5.43 % (2243173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243173)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243173)Termination reason: Instruction limit
% 15.50/5.43 % (2243173)Termination phase: Saturation
% 15.50/5.43 % (2243173)Time elapsed: 0.568 s
% 15.50/5.43 % (2243173)Peak memory usage: 19 MB
% 15.50/5.43 % (2243173)Instructions burned: 870 (million)
% 15.50/5.43 % (2243175)ott+10_1_sil=32000:tgt=ground:random_seed=2658552647:i=5114:av=off_2963 on theBenchmark for (2963ds/5114Mi)
% 15.50/5.43 % (2243163)Instruction limit reached!
% 15.50/5.43 % (2243163)------------------------------
% 15.50/5.43 % (2243163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243163)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243163)Termination reason: Instruction limit
% 15.50/5.43 % (2243163)Termination phase: Saturation
% 15.50/5.43 % (2243163)Time elapsed: 2.897 s
% 15.50/5.43 % (2243163)Peak memory usage: 40 MB
% 15.50/5.43 % (2243163)Instructions burned: 5132 (million)
% 15.50/5.43 % (2243177)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2144521073:i=54282_2959 on theBenchmark for (2959ds/54282Mi)
% 15.50/5.43 % TRYING [1]
% 15.50/5.43 % TRYING [2]
% 15.50/5.43 % TRYING [3]
% 15.50/5.43 % TRYING [4]
% 15.50/5.43 % TRYING [5]
% 15.50/5.43 % (2243160)Instruction limit reached!
% 15.50/5.43 % (2243160)------------------------------
% 15.50/5.43 % (2243160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243160)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243160)Termination reason: Instruction limit
% 15.50/5.43 % (2243160)Termination phase: Finite model building constraint generation
% 15.50/5.43 % (2243160)Time elapsed: 3.436 s
% 15.50/5.43 % (2243160)Peak memory usage: 658 MB
% 15.50/5.43 % (2243160)Instructions burned: 9517 (million)
% 15.50/5.43 % TRYING [6]
% 15.50/5.43 % (2243179)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2843911243:i=3512:aac=none_2954 on theBenchmark for (2954ds/3512Mi)
% 15.50/5.43 % (2243175) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2243119-2243175"...
% 15.50/5.43 % (2243175)...printing done.
% 15.50/5.43 % (2243175)Refutation found. Thanks to Tanya!
% 15.50/5.43 % SZS status Theorem for theBenchmark
% 15.50/5.43 % SZS output start Proof for theBenchmark
% See solution above
% 15.50/5.43 % (2243175)------------------------------
% 15.50/5.43 % (2243175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/5.43 % (2243175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/5.43 % (2243175)CaDiCaL version: 2.1.3
% 15.50/5.43 % (2243175)Termination reason: Refutation
% 15.50/5.43 % (2243175)Time elapsed: 1.300 s
% 15.50/5.43 % (2243175)Peak memory usage: 30 MB
% 15.50/5.43 % (2243175)Instructions burned: 2086 (million)
% 15.50/5.43 % (2243119)Success in time 5.01 s
% 15.50/5.43 % Vampire exiting
%------------------------------------------------------------------------------