%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU135+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 : 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 12:52:02 PM UTC 2026
% Result : Theorem 10.22s 5.28s
% Output : Refutation 10.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 17
% Syntax : Number of formulae : 111 ( 35 unt; 3 def)
% Number of atoms : 386 ( 65 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 438 ( 163 ~; 185 |; 75 &)
% ( 9 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 232 ( 219 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_xboole_0) ).
fof(f4,axiom,
! [X0,X1] :
( X0 = X1
<=> ( subset(X0,X1)
& subset(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f6,axiom,
! [X0,X1,X2] :
( X2 = set_union2(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,X0)
| in(X3,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_xboole_0) ).
fof(f7,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f8,axiom,
! [X0,X1,X2] :
( X2 = set_intersection2(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,X0)
& in(X3,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_xboole_0) ).
fof(f9,axiom,
! [X0,X1,X2] :
( X2 = set_difference(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,X0)
& ~ in(X3,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f25,axiom,
! [X0,X1] :
( subset(X0,X1)
=> set_union2(X0,X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_xboole_1) ).
fof(f29,axiom,
! [X0,X1,X2] :
( ( subset(X0,X1)
& subset(X1,X2) )
=> subset(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_xboole_1) ).
fof(f31,axiom,
! [X0,X1] :
( subset(X0,X1)
=> set_intersection2(X0,X1) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t28_xboole_1) ).
fof(f35,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(f36,axiom,
! [X0,X1] : subset(set_difference(X0,X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t36_xboole_1) ).
fof(f38,conjecture,
! [X0,X1] : set_union2(X0,set_difference(X1,X0)) = set_union2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t39_xboole_1) ).
fof(f39,negated_conjecture,
~ ! [X0,X1] : set_union2(X0,set_difference(X1,X0)) = set_union2(X0,X1),
inference(negated_conjecture,[status(cth)],[f38]) ).
fof(f47,axiom,
! [X0,X1] : subset(X0,set_union2(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_xboole_1) ).
fof(f49,axiom,
! [X0,X1,X2] :
( ( subset(X0,X1)
& subset(X2,X1) )
=> subset(set_union2(X0,X2),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_xboole_1) ).
fof(f56,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f60,plain,
! [X0,X1] :
( set_union2(X0,X1) = X1
| ~ subset(X0,X1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f63,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ subset(X0,X1)
| ~ subset(X1,X2) ),
inference(ennf_transformation,[],[f29]) ).
fof(f64,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ subset(X0,X1)
| ~ subset(X1,X2) ),
inference(flattening,[],[f63]) ).
fof(f66,plain,
! [X0,X1] :
( set_intersection2(X0,X1) = X0
| ~ subset(X0,X1) ),
inference(ennf_transformation,[],[f31]) ).
fof(f68,plain,
! [X0,X1,X2] :
( subset(set_difference(X0,X2),set_difference(X1,X2))
| ~ subset(X0,X1) ),
inference(ennf_transformation,[],[f35]) ).
fof(f69,plain,
? [X0,X1] : set_union2(X0,X1) != set_union2(X0,set_difference(X1,X0)),
inference(ennf_transformation,[],[f39]) ).
fof(f76,plain,
! [X0,X1,X2] :
( subset(set_union2(X0,X2),X1)
| ~ subset(X0,X1)
| ~ subset(X2,X1) ),
inference(ennf_transformation,[],[f49]) ).
fof(f77,plain,
! [X0,X1,X2] :
( subset(set_union2(X0,X2),X1)
| ~ subset(X0,X1)
| ~ subset(X2,X1) ),
inference(flattening,[],[f76]) ).
fof(f78,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subset(X0,X1)
| ~ subset(X1,X0) )
& ( ( subset(X0,X1)
& subset(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f79,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subset(X0,X1)
| ~ subset(X1,X0) )
& ( ( subset(X0,X1)
& subset(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f78]) ).
fof(f83,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ? [X3] :
( ( ( ~ in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) )
& ( in(X3,X0)
| in(X3,X1)
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ( ~ in(X3,X0)
& ~ in(X3,X1) ) )
& ( in(X3,X0)
| in(X3,X1)
| ~ in(X3,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f6]) ).
fof(f84,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ? [X3] :
( ( ( ~ in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) )
& ( in(X3,X0)
| in(X3,X1)
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ( ~ in(X3,X0)
& ~ in(X3,X1) ) )
& ( in(X3,X0)
| in(X3,X1)
| ~ in(X3,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(flattening,[],[f83]) ).
fof(f85,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ? [X3] :
( ( ( ~ in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) )
& ( in(X3,X0)
| in(X3,X1)
| in(X3,X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ( ~ in(X4,X0)
& ~ in(X4,X1) ) )
& ( in(X4,X0)
| in(X4,X1)
| ~ in(X4,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(rectify,[],[f84]) ).
fof(f86,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ( ( ( ~ in(sK1(X0,X1,X2),X0)
& ~ in(sK1(X0,X1,X2),X1) )
| ~ in(sK1(X0,X1,X2),X2) )
& ( in(sK1(X0,X1,X2),X0)
| in(sK1(X0,X1,X2),X1)
| in(sK1(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ( ~ in(X4,X0)
& ~ in(X4,X1) ) )
& ( in(X4,X0)
| in(X4,X1)
| ~ in(X4,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X0,X1,X2))],[f85]) ).
fof(f87,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,[],[f56]) ).
fof(f88,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,[],[f87]) ).
fof(f89,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ( ~ in(sK2(X0,X1),X1)
& in(sK2(X0,X1),X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X2,sK2(X0,X1))],[f88]) ).
fof(f90,plain,
! [X0,X1,X2] :
( ( X2 = set_intersection2(X0,X1)
| ? [X3] :
( ( ~ in(X3,X0)
| ~ in(X3,X1)
| ~ in(X3,X2) )
& ( ( in(X3,X0)
& in(X3,X1) )
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ~ in(X3,X0)
| ~ in(X3,X1) )
& ( ( in(X3,X0)
& in(X3,X1) )
| ~ in(X3,X2) ) )
| set_intersection2(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f91,plain,
! [X0,X1,X2] :
( ( X2 = set_intersection2(X0,X1)
| ? [X3] :
( ( ~ in(X3,X0)
| ~ in(X3,X1)
| ~ in(X3,X2) )
& ( ( in(X3,X0)
& in(X3,X1) )
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ~ in(X3,X0)
| ~ in(X3,X1) )
& ( ( in(X3,X0)
& in(X3,X1) )
| ~ in(X3,X2) ) )
| set_intersection2(X0,X1) != X2 ) ),
inference(flattening,[],[f90]) ).
fof(f92,plain,
! [X0,X1,X2] :
( ( X2 = set_intersection2(X0,X1)
| ? [X3] :
( ( ~ in(X3,X0)
| ~ in(X3,X1)
| ~ in(X3,X2) )
& ( ( in(X3,X0)
& in(X3,X1) )
| in(X3,X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ~ in(X4,X0)
| ~ in(X4,X1) )
& ( ( in(X4,X0)
& in(X4,X1) )
| ~ in(X4,X2) ) )
| set_intersection2(X0,X1) != X2 ) ),
inference(rectify,[],[f91]) ).
fof(f93,plain,
! [X0,X1,X2] :
( ( X2 = set_intersection2(X0,X1)
| ( ( ~ in(sK3(X0,X1,X2),X0)
| ~ in(sK3(X0,X1,X2),X1)
| ~ in(sK3(X0,X1,X2),X2) )
& ( ( in(sK3(X0,X1,X2),X0)
& in(sK3(X0,X1,X2),X1) )
| in(sK3(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ~ in(X4,X0)
| ~ in(X4,X1) )
& ( ( in(X4,X0)
& in(X4,X1) )
| ~ in(X4,X2) ) )
| set_intersection2(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X3,sK3(X0,X1,X2))],[f92]) ).
fof(f94,plain,
! [X0,X1,X2] :
( ( X2 = set_difference(X0,X1)
| ? [X3] :
( ( ~ in(X3,X0)
| in(X3,X1)
| ~ in(X3,X2) )
& ( ( in(X3,X0)
& ~ in(X3,X1) )
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ~ in(X3,X0)
| in(X3,X1) )
& ( ( in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) ) )
| set_difference(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f95,plain,
! [X0,X1,X2] :
( ( X2 = set_difference(X0,X1)
| ? [X3] :
( ( ~ in(X3,X0)
| in(X3,X1)
| ~ in(X3,X2) )
& ( ( in(X3,X0)
& ~ in(X3,X1) )
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ~ in(X3,X0)
| in(X3,X1) )
& ( ( in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) ) )
| set_difference(X0,X1) != X2 ) ),
inference(flattening,[],[f94]) ).
fof(f96,plain,
! [X0,X1,X2] :
( ( X2 = set_difference(X0,X1)
| ? [X3] :
( ( ~ in(X3,X0)
| in(X3,X1)
| ~ in(X3,X2) )
& ( ( in(X3,X0)
& ~ in(X3,X1) )
| in(X3,X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ~ in(X4,X0)
| in(X4,X1) )
& ( ( in(X4,X0)
& ~ in(X4,X1) )
| ~ in(X4,X2) ) )
| set_difference(X0,X1) != X2 ) ),
inference(rectify,[],[f95]) ).
fof(f97,plain,
! [X0,X1,X2] :
( ( X2 = set_difference(X0,X1)
| ( ( ~ in(sK4(X0,X1,X2),X0)
| in(sK4(X0,X1,X2),X1)
| ~ in(sK4(X0,X1,X2),X2) )
& ( ( in(sK4(X0,X1,X2),X0)
& ~ in(sK4(X0,X1,X2),X1) )
| in(sK4(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ~ in(X4,X0)
| in(X4,X1) )
& ( ( in(X4,X0)
& ~ in(X4,X1) )
| ~ in(X4,X2) ) )
| set_difference(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X3,sK4(X0,X1,X2))],[f96]) ).
fof(f105,plain,
set_union2(sK8,sK9) != set_union2(sK8,set_difference(sK9,sK8)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9]),skolemize(X0,sK8),skolemize(X1,sK9)],[f69]) ).
fof(f109,plain,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
inference(cnf_transformation,[],[f2]) ).
fof(f113,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f79]) ).
fof(f116,plain,
! [X2,X0,X1,X4] :
( in(X4,X0)
| in(X4,X1)
| ~ in(X4,X2)
| set_union2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f86]) ).
fof(f117,plain,
! [X2,X0,X1,X4] :
( in(X4,X2)
| ~ in(X4,X1)
| set_union2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f86]) ).
fof(f118,plain,
! [X2,X0,X1,X4] :
( in(X4,X2)
| ~ in(X4,X0)
| set_union2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f86]) ).
fof(f123,plain,
! [X0,X1] :
( in(sK2(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f89]) ).
fof(f124,plain,
! [X0,X1] :
( ~ in(sK2(X0,X1),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f89]) ).
fof(f125,plain,
! [X2,X0,X1,X4] :
( in(X4,X1)
| ~ in(X4,X2)
| set_intersection2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f93]) ).
fof(f133,plain,
! [X2,X0,X1,X4] :
( in(X4,X2)
| ~ in(X4,X0)
| in(X4,X1)
| set_difference(X0,X1) != X2 ),
inference(cnf_transformation,[],[f97]) ).
fof(f150,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| set_union2(X0,X1) = X1 ),
inference(cnf_transformation,[],[f60]) ).
fof(f154,plain,
! [X2,X0,X1] :
( ~ subset(X1,X2)
| ~ subset(X0,X1)
| subset(X0,X2) ),
inference(cnf_transformation,[],[f64]) ).
fof(f156,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| set_intersection2(X0,X1) = X0 ),
inference(cnf_transformation,[],[f66]) ).
fof(f161,plain,
! [X2,X0,X1] :
( subset(set_difference(X0,X2),set_difference(X1,X2))
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f68]) ).
fof(f162,plain,
! [X0,X1] : subset(set_difference(X0,X1),X0),
inference(cnf_transformation,[],[f36]) ).
fof(f165,plain,
set_union2(sK8,sK9) != set_union2(sK8,set_difference(sK9,sK8)),
inference(cnf_transformation,[],[f105]) ).
fof(f176,plain,
! [X0,X1] : subset(X0,set_union2(X0,X1)),
inference(cnf_transformation,[],[f47]) ).
fof(f178,plain,
! [X2,X0,X1] :
( subset(set_union2(X0,X2),X1)
| ~ subset(X0,X1)
| ~ subset(X2,X1) ),
inference(cnf_transformation,[],[f77]) ).
fof(f182,plain,
! [X0,X1,X4] :
( in(X4,set_union2(X0,X1))
| ~ in(X4,X0) ),
inference(equality_resolution,[],[f118]) ).
fof(f183,plain,
! [X0,X1,X4] :
( in(X4,set_union2(X0,X1))
| ~ in(X4,X1) ),
inference(equality_resolution,[],[f117]) ).
fof(f184,plain,
! [X0,X1,X4] :
( ~ in(X4,set_union2(X0,X1))
| in(X4,X1)
| in(X4,X0) ),
inference(equality_resolution,[],[f116]) ).
fof(f187,plain,
! [X0,X1,X4] :
( ~ in(X4,set_intersection2(X0,X1))
| in(X4,X1) ),
inference(equality_resolution,[],[f125]) ).
fof(f188,plain,
! [X0,X1,X4] :
( in(X4,set_difference(X0,X1))
| ~ in(X4,X0)
| in(X4,X1) ),
inference(equality_resolution,[],[f133]) ).
fof(f191,definition,
sF12 = set_union2(sK8,sK9),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f192,plain,
set_union2(sK8,sK9) = sF12,
inference(reorient_equations,[],[f191]) ).
fof(f193,definition,
sF13 = set_difference(sK9,sK8),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f194,plain,
set_difference(sK9,sK8) = sF13,
inference(reorient_equations,[],[f193]) ).
fof(f195,definition,
sF14 = set_union2(sK8,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f196,plain,
set_union2(sK8,sF13) = sF14,
inference(reorient_equations,[],[f195]) ).
fof(f197,plain,
sF12 != sF14,
inference(definition_folding,[],[f165,f196,f194,f192]) ).
fof(f207,plain,
subset(sK8,sF12),
inference(superposition,[],[f176,f192]) ).
fof(f209,plain,
subset(sK8,sF14),
inference(superposition,[],[f176,f196]) ).
fof(f231,plain,
! [X0,X1] : subset(X1,set_union2(X0,X1)),
inference(superposition,[],[f176,f109]) ).
fof(f250,plain,
subset(sK9,sF12),
inference(superposition,[],[f231,f192]) ).
fof(f264,plain,
sF14 = set_union2(sK8,sF14),
inference(resolution,[],[f150,f209]) ).
fof(f278,plain,
sK8 = set_intersection2(sK8,sF14),
inference(resolution,[],[f156,f209]) ).
fof(f377,plain,
! [X0] :
( ~ in(X0,sK8)
| in(X0,sF14) ),
inference(superposition,[],[f182,f264]) ).
fof(f386,plain,
! [X2,X0,X1] :
( ~ in(sK2(X0,set_union2(X1,X2)),X2)
| subset(X0,set_union2(X1,X2)) ),
inference(resolution,[],[f183,f124]) ).
fof(f394,plain,
! [X0] :
( ~ in(X0,sF13)
| in(X0,sF14) ),
inference(superposition,[],[f183,f196]) ).
fof(f412,plain,
! [X2,X0,X1] :
( in(sK2(set_intersection2(X0,X1),X2),X1)
| subset(set_intersection2(X0,X1),X2) ),
inference(resolution,[],[f187,f123]) ).
fof(f457,plain,
! [X2,X0,X1] :
( ~ subset(X0,set_difference(X1,X2))
| subset(X0,X1) ),
inference(resolution,[],[f154,f162]) ).
fof(f560,plain,
! [X0] :
( subset(sF13,set_difference(X0,sK8))
| ~ subset(sK9,X0) ),
inference(superposition,[],[f161,f194]) ).
fof(f627,plain,
! [X2,X0,X1] :
( ~ subset(X1,set_union2(X0,X2))
| ~ subset(X2,X1)
| ~ subset(X0,X1)
| set_union2(X0,X2) = X1 ),
inference(resolution,[],[f178,f113]) ).
fof(f637,plain,
! [X0] :
( ~ subset(sK9,X0)
| ~ subset(sK8,X0)
| subset(sF12,X0) ),
inference(superposition,[],[f178,f192]) ).
fof(f639,plain,
! [X0] :
( ~ subset(sF13,X0)
| ~ subset(sK8,X0)
| subset(sF14,X0) ),
inference(superposition,[],[f178,f196]) ).
fof(f649,plain,
! [X2,X0,X1] :
( in(sK2(set_union2(X0,X1),X2),X1)
| in(sK2(set_union2(X0,X1),X2),X0)
| subset(set_union2(X0,X1),X2) ),
inference(resolution,[],[f184,f123]) ).
fof(f696,plain,
! [X0] :
( ~ in(X0,sK9)
| in(X0,sF13)
| in(X0,sK8) ),
inference(superposition,[],[f188,f194]) ).
fof(f1496,plain,
! [X0] :
( ~ subset(sK9,X0)
| subset(sF13,X0) ),
inference(resolution,[],[f560,f457]) ).
fof(f1872,plain,
! [X0] :
( ~ subset(sK8,set_union2(sK9,X0))
| subset(sF12,set_union2(sK9,X0)) ),
inference(resolution,[],[f637,f176]) ).
fof(f2106,plain,
subset(sF13,sF12),
inference(resolution,[],[f1496,f250]) ).
fof(f2130,plain,
( ~ subset(sK8,sF12)
| subset(sF14,sF12) ),
inference(resolution,[],[f2106,f639]) ).
fof(f2139,plain,
subset(sF14,sF12),
inference(forward_subsumption_resolution,[],[f2130,f207]) ).
fof(f2160,plain,
( ~ subset(sF12,sF14)
| sF12 = sF14 ),
inference(resolution,[],[f2139,f113]) ).
fof(f2167,plain,
~ subset(sF12,sF14),
inference(forward_subsumption_resolution,[],[f2160,f197]) ).
fof(f3595,plain,
! [X2,X0,X1] :
( subset(set_intersection2(X0,X1),set_union2(X2,X1))
| subset(set_intersection2(X0,X1),set_union2(X2,X1)) ),
inference(resolution,[],[f412,f386]) ).
fof(f3636,plain,
! [X2,X0,X1] : subset(set_intersection2(X0,X1),set_union2(X2,X1)),
inference(duplicate_literal_removal,[],[f3595]) ).
fof(f6876,plain,
! [X0,X1] :
( in(sK2(set_union2(X0,X1),X1),X0)
| subset(set_union2(X0,X1),X1)
| subset(set_union2(X0,X1),X1) ),
inference(resolution,[],[f649,f124]) ).
fof(f6982,plain,
! [X0,X1] :
( in(sK2(set_union2(X0,X1),X1),X0)
| subset(set_union2(X0,X1),X1) ),
inference(duplicate_literal_removal,[],[f6876]) ).
fof(f16557,plain,
! [X0] : subset(sK8,set_union2(X0,sF14)),
inference(superposition,[],[f3636,f278]) ).
fof(f30696,plain,
subset(sF12,set_union2(sK9,sF14)),
inference(resolution,[],[f1872,f16557]) ).
fof(f30725,plain,
( ~ subset(sF14,sF12)
| ~ subset(sK9,sF12)
| sF12 = set_union2(sK9,sF14) ),
inference(resolution,[],[f30696,f627]) ).
fof(f30757,plain,
( ~ subset(sK9,sF12)
| sF12 = set_union2(sK9,sF14) ),
inference(forward_subsumption_resolution,[],[f30725,f2139]) ).
fof(f30759,plain,
sF12 = set_union2(sK9,sF14),
inference(forward_subsumption_resolution,[],[f30757,f250]) ).
fof(f77583,plain,
( in(sK2(sF12,sF14),sK9)
| subset(sF12,sF14) ),
inference(superposition,[],[f6982,f30759]) ).
fof(f77610,plain,
in(sK2(sF12,sF14),sK9),
inference(forward_subsumption_resolution,[],[f77583,f2167]) ).
fof(f77631,plain,
( in(sK2(sF12,sF14),sF13)
| in(sK2(sF12,sF14),sK8) ),
inference(resolution,[],[f77610,f696]) ).
fof(f78863,plain,
( in(sK2(sF12,sF14),sK8)
| in(sK2(sF12,sF14),sF14) ),
inference(resolution,[],[f77631,f394]) ).
fof(f78866,plain,
in(sK2(sF12,sF14),sF14),
inference(forward_subsumption_resolution,[],[f78863,f377]) ).
fof(f78939,plain,
subset(sF12,sF14),
inference(resolution,[],[f78866,f124]) ).
fof(f78944,plain,
$false,
inference(forward_subsumption_resolution,[],[f78939,f2167]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU135+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.11/0.38 % Computer : n020.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 03:42:08 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/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
% 8.18/2.03 % (4005206)Will run a generic schedule for satisfiability detection.
% 8.18/2.03 % (4005215)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=772748899:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.18/2.03 % (4005212)% WARNING: option uhcvi not known.
% 8.18/2.03 % (4005214)dis+10_1_sil=32000:sp=arity:random_seed=2166192936:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.18/2.03 % (4005211)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2410604983_2999 on theBenchmark for (2999ds/0Mi)
% 8.18/2.03 % (4005212)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4285606676:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.18/2.03 % (4005216)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2520657957:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.18/2.03 % (4005217)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2610163648:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.18/2.03 % (4005213)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=925236642:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.18/2.03 % TRYING [1]
% 8.18/2.03 % TRYING [2]
% 8.18/2.03 % TRYING [3]
% 8.18/2.03 % TRYING [4]
% 8.18/2.03 % (4005215)Instruction limit reached!
% 8.18/2.03 % (4005215)------------------------------
% 8.18/2.03 % (4005215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/2.03 % (4005215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/2.03 % (4005215)CaDiCaL version: 2.1.3
% 8.18/2.03 % (4005215)Termination reason: Instruction limit
% 8.18/2.03 % (4005215)Termination phase: Saturation
% 8.18/2.03 % (4005215)Time elapsed: 0.040 s
% 8.18/2.03 % (4005215)Peak memory usage: 12 MB
% 8.18/2.03 % (4005215)Instructions burned: 117 (million)
% 8.18/2.03 % (4005225)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3627119553:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 8.18/2.03 % TRYING [1]
% 8.18/2.03 % TRYING [2]
% 8.18/2.03 % TRYING [3]
% 8.18/2.03 % TRYING [4]
% 8.18/2.03 % TRYING [5]
% 8.18/2.03 % (4005214)Instruction limit reached!
% 8.18/2.03 % (4005214)------------------------------
% 8.18/2.03 % (4005214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/2.03 % (4005214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/2.03 % (4005214)CaDiCaL version: 2.1.3
% 8.18/2.03 % (4005214)Termination reason: Instruction limit
% 8.18/2.03 % (4005214)Termination phase: Saturation
% 8.18/2.03 % (4005214)Time elapsed: 0.064 s
% 8.18/2.03 % (4005214)Peak memory usage: 12 MB
% 8.18/2.03 % (4005214)Instructions burned: 104 (million)
% 8.18/2.03 % TRYING [5]
% 8.18/2.03 % (4005216)Instruction limit reached!
% 8.18/2.03 % (4005216)------------------------------
% 8.18/2.03 % (4005216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/2.03 % (4005216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/2.03 % (4005216)CaDiCaL version: 2.1.3
% 8.18/2.03 % (4005216)Termination reason: Instruction limit
% 8.18/2.03 % (4005216)Termination phase: Saturation
% 8.18/2.03 % (4005216)Time elapsed: 0.083 s
% 8.18/2.03 % (4005216)Peak memory usage: 13 MB
% 8.18/2.03 % (4005216)Instructions burned: 137 (million)
% 8.18/2.03 % (4005227)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=76127158:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 8.18/2.03 % (4005217)Instruction limit reached!
% 8.18/2.03 % (4005217)------------------------------
% 8.18/2.03 % (4005217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/2.03 % (4005217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/2.03 % (4005217)CaDiCaL version: 2.1.3
% 8.18/2.03 % (4005217)Termination reason: Instruction limit
% 8.18/2.03 % (4005217)Termination phase: Saturation
% 8.18/2.03 % (4005217)Time elapsed: 0.092 s
% 8.18/2.03 % (4005217)Peak memory usage: 12 MB
% 8.18/2.03 % (4005217)Instructions burned: 160 (million)
% 8.18/2.03 % (4005229)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=3022497022:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.18/2.03 % TRYING [6]
% 8.18/2.03 % (4005230)ott-21_1_sil=16000:fs=off:random_seed=478249391:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.18/2.03 % TRYING [6]
% 8.18/2.03 % (4005227)Instruction limit reached!
% 8.18/2.03 % (4005227)------------------------------
% 8.18/2.03 % (4005227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005227)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005227)Termination reason: Instruction limit
% 10.22/5.28 % (4005227)Termination phase: Saturation
% 10.22/5.28 % (4005227)Time elapsed: 0.088 s
% 10.22/5.28 % (4005227)Peak memory usage: 13 MB
% 10.22/5.28 % (4005227)Instructions burned: 132 (million)
% 10.22/5.28 % (4005233)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2917963714:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 10.22/5.28 % (4005230)Instruction limit reached!
% 10.22/5.28 % (4005230)------------------------------
% 10.22/5.28 % (4005230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005230)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005230)Termination reason: Instruction limit
% 10.22/5.28 % (4005230)Termination phase: Saturation
% 10.22/5.28 % (4005230)Time elapsed: 0.086 s
% 10.22/5.28 % (4005230)Peak memory usage: 13 MB
% 10.22/5.28 % (4005230)Instructions burned: 182 (million)
% 10.22/5.28 % (4005225)Instruction limit reached!
% 10.22/5.28 % (4005225)------------------------------
% 10.22/5.28 % (4005225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005225)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005225)Termination reason: Instruction limit
% 10.22/5.28 % (4005225)Termination phase: Finite model building SAT solving
% 10.22/5.28 % (4005225)Time elapsed: 0.169 s
% 10.22/5.28 % (4005225)Peak memory usage: 23 MB
% 10.22/5.28 % (4005225)Instructions burned: 716 (million)
% 10.22/5.28 % (4005235)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4172466835:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 10.22/5.28 % TRYING [1]
% 10.22/5.28 % TRYING [2]
% 10.22/5.28 % TRYING [3]
% 10.22/5.28 % (4005236)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=389196754:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 10.22/5.28 % TRYING [4]
% 10.22/5.28 % TRYING [7]
% 10.22/5.28 % TRYING [5]
% 10.22/5.28 % TRYING [6]
% 10.22/5.28 % (4005229)Instruction limit reached!
% 10.22/5.28 % (4005229)------------------------------
% 10.22/5.28 % (4005229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005229)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005229)Termination reason: Instruction limit
% 10.22/5.28 % (4005229)Termination phase: Saturation
% 10.22/5.28 % (4005229)Time elapsed: 0.372 s
% 10.22/5.28 % (4005229)Peak memory usage: 17 MB
% 10.22/5.28 % (4005229)Instructions burned: 686 (million)
% 10.22/5.28 % (4005239)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3847726739:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 10.22/5.28 % (4005233)Instruction limit reached!
% 10.22/5.28 % (4005233)------------------------------
% 10.22/5.28 % (4005233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005233)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005233)Termination reason: Instruction limit
% 10.22/5.28 % (4005233)Termination phase: Saturation
% 10.22/5.28 % (4005233)Time elapsed: 0.309 s
% 10.22/5.28 % (4005233)Peak memory usage: 14 MB
% 10.22/5.28 % (4005233)Instructions burned: 478 (million)
% 10.22/5.28 % (4005241)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=596110850: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)
% 10.22/5.28 % (4005235)Instruction limit reached!
% 10.22/5.28 % (4005235)------------------------------
% 10.22/5.28 % (4005235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005236)Instruction limit reached!
% 10.22/5.28 % (4005236)------------------------------
% 10.22/5.28 % (4005236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005235)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005235)Termination reason: Instruction limit
% 10.22/5.28 % (4005235)Termination phase: Finite model building SAT solving
% 10.22/5.28 % (4005235)Time elapsed: 0.360 s
% 10.22/5.28 % (4005235)Peak memory usage: 22 MB
% 10.22/5.28 % (4005236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005235)Instructions burned: 865 (million)
% 10.22/5.28 % (4005236)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005236)Termination reason: Instruction limit
% 10.22/5.28 % (4005236)Termination phase: Saturation
% 10.22/5.28 % (4005236)Time elapsed: 0.351 s
% 10.22/5.28 % (4005236)Peak memory usage: 22 MB
% 10.22/5.28 % (4005236)Instructions burned: 1180 (million)
% 10.22/5.28 % (4005243)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3810922751:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 10.22/5.28 % TRYING [14]
% 10.22/5.28 % (4005244)fmb+10_1_sil=64000:random_seed=2700975945:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 10.22/5.28 % TRYING [1]
% 10.22/5.28 % TRYING [2]
% 10.22/5.28 % TRYING [3]
% 10.22/5.28 % TRYING [4]
% 10.22/5.28 % TRYING [5]
% 10.22/5.28 % TRYING [6]
% 10.22/5.28 % (4005239)Instruction limit reached!
% 10.22/5.28 % (4005239)------------------------------
% 10.22/5.28 % (4005239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005239)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005239)Termination reason: Instruction limit
% 10.22/5.28 % (4005239)Termination phase: Finite model building constraint generation
% 10.22/5.28 % (4005239)Time elapsed: 0.321 s
% 10.22/5.28 % (4005239)Peak memory usage: 75 MB
% 10.22/5.28 % (4005239)Instructions burned: 889 (million)
% 10.22/5.28 % TRYING [8]
% 10.22/5.28 % (4005247)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3780398886:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 10.22/5.28 % TRYING [20]
% 10.22/5.28 % (4005243)Instruction limit reached!
% 10.22/5.28 % (4005243)------------------------------
% 10.22/5.28 % (4005243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005243)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005243)Termination reason: Instruction limit
% 10.22/5.28 % (4005243)Termination phase: Saturation
% 10.22/5.28 % (4005243)Time elapsed: 0.262 s
% 10.22/5.28 % (4005243)Peak memory usage: 19 MB
% 10.22/5.28 % (4005243)Instructions burned: 879 (million)
% 10.22/5.28 % (4005249)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=851462021:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 10.22/5.28 % TRYING [8]
% 10.22/5.28 % TRYING [7]
% 10.22/5.28 % (4005241)Instruction limit reached!
% 10.22/5.28 % (4005241)------------------------------
% 10.22/5.28 % (4005241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005241)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005241)Termination reason: Instruction limit
% 10.22/5.28 % (4005241)Termination phase: Saturation
% 10.22/5.28 % (4005241)Time elapsed: 0.440 s
% 10.22/5.28 % (4005241)Peak memory usage: 19 MB
% 10.22/5.28 % (4005241)Instructions burned: 692 (million)
% 10.22/5.28 % (4005251)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1126639351:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 10.22/5.28 % (4005249)Instruction limit reached!
% 10.22/5.28 % (4005249)------------------------------
% 10.22/5.28 % (4005249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005249)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005249)Termination reason: Instruction limit
% 10.22/5.28 % (4005249)Termination phase: Finite model building SAT solving
% 10.22/5.28 % (4005249)Time elapsed: 0.227 s
% 10.22/5.28 % (4005249)Peak memory usage: 52 MB
% 10.22/5.28 % (4005249)Instructions burned: 921 (million)
% 10.22/5.28 % (4005253)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3862505513:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 10.22/5.28 % (4005253)Instruction limit reached!
% 10.22/5.28 % (4005253)------------------------------
% 10.22/5.28 % (4005253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005253)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005253)Termination reason: Instruction limit
% 10.22/5.28 % (4005253)Termination phase: Saturation
% 10.22/5.28 % (4005253)Time elapsed: 0.463 s
% 10.22/5.28 % (4005253)Peak memory usage: 31 MB
% 10.22/5.28 % (4005253)Instructions burned: 1473 (million)
% 10.22/5.28 % (4005255)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1760885247:i=6324_2983 on theBenchmark for (2983ds/6324Mi)
% 10.22/5.28 % TRYING [77]
% 10.22/5.28 % TRYING [8]
% 10.22/5.28 % (4005255)Instruction limit reached!
% 10.22/5.28 % (4005255)------------------------------
% 10.22/5.28 % (4005255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005255)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005255)Termination reason: Instruction limit
% 10.22/5.28 % (4005255)Termination phase: Finite model building constraint generation
% 10.22/5.28 % (4005255)Time elapsed: 1.297 s
% 10.22/5.28 % (4005255)Peak memory usage: 523 MB
% 10.22/5.28 % (4005255)Instructions burned: 6327 (million)
% 10.22/5.28 % (4005259)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2153118484:fmbsr=2.30978:i=2174_2970 on theBenchmark for (2970ds/2174Mi)
% 10.22/5.28 % TRYING [16]
% 10.22/5.28 % TRYING [9]
% 10.22/5.28 % (4005259)Instruction limit reached!
% 10.22/5.28 % (4005259)------------------------------
% 10.22/5.28 % (4005259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005259)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005259)Termination reason: Instruction limit
% 10.22/5.28 % (4005259)Termination phase: Finite model building constraint generation
% 10.22/5.28 % (4005259)Time elapsed: 0.413 s
% 10.22/5.28 % (4005259)Peak memory usage: 143 MB
% 10.22/5.28 % (4005259)Instructions burned: 2181 (million)
% 10.22/5.28 % (4005261)ott-2_1_sil=16000:newcnf=on:random_seed=664385544:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2966 on theBenchmark for (2966ds/869Mi)
% 10.22/5.28 % (4005261)Instruction limit reached!
% 10.22/5.28 % (4005261)------------------------------
% 10.22/5.28 % (4005261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005261)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005261)Termination reason: Instruction limit
% 10.22/5.28 % (4005261)Termination phase: Saturation
% 10.22/5.28 % (4005261)Time elapsed: 0.258 s
% 10.22/5.28 % (4005261)Peak memory usage: 17 MB
% 10.22/5.28 % (4005261)Instructions burned: 870 (million)
% 10.22/5.28 % (4005263)ott+10_1_sil=32000:tgt=ground:random_seed=711936701:i=5114:av=off_2963 on theBenchmark for (2963ds/5114Mi)
% 10.22/5.28 % (4005251)Instruction limit reached!
% 10.22/5.28 % (4005251)------------------------------
% 10.22/5.28 % (4005251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005251)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005251)Termination reason: Instruction limit
% 10.22/5.28 % (4005251)Termination phase: Saturation
% 10.22/5.28 % (4005251)Time elapsed: 2.701 s
% 10.22/5.28 % (4005251)Peak memory usage: 30 MB
% 10.22/5.28 % (4005251)Instructions burned: 5134 (million)
% 10.22/5.28 % (4005265)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3632326407:i=54282_2962 on theBenchmark for (2962ds/54282Mi)
% 10.22/5.28 % TRYING [1]
% 10.22/5.28 % TRYING [2]
% 10.22/5.28 % TRYING [3]
% 10.22/5.28 % TRYING [4]
% 10.22/5.28 % TRYING [5]
% 10.22/5.28 % TRYING [6]
% 10.22/5.28 % TRYING [7]
% 10.22/5.28 % TRYING [8]
% 10.22/5.28 % TRYING [9]
% 10.22/5.28 % (4005263) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4005206-4005263"...
% 10.22/5.28 % (4005263)...printing done.
% 10.22/5.28 % (4005263)Refutation found. Thanks to Tanya!
% 10.22/5.28 % SZS status Theorem for theBenchmark
% 10.22/5.28 % SZS output start Proof for theBenchmark
% See solution above
% 10.22/5.28 % (4005263)------------------------------
% 10.22/5.28 % (4005263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.22/5.28 % (4005263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/5.28 % (4005263)CaDiCaL version: 2.1.3
% 10.22/5.28 % (4005263)Termination reason: Refutation
% 10.22/5.28 % (4005263)Time elapsed: 1.098 s
% 10.22/5.28 % (4005263)Peak memory usage: 43 MB
% 10.22/5.28 % (4005263)Instructions burned: 3506 (million)
% 10.22/5.28 % (4005206)Success in time 4.863 s
% 10.22/5.28 % Vampire exiting
%------------------------------------------------------------------------------